Resolution
Chosen clause
size
length
height
Max time of proof
Max size of clauses
notrace
trace
Support Clauses
p(f(x)) -q(y,a),q(a,a) r(x,x,b) s(a,b),s(a,z) -r(x,x,b),-p(f(a)) r(x,a,b),-s(y,z) -s(a,b)
Usable Clauses
Proof
(1) [q(a, a) r(x, x, b) s(a, b)] Hyp (2) [-s(y, z) -s(a, b)] Hyp (3) [-s(a, b)] Factor 2 z := b; y := a (4) [s(a, z) -r(x, x, b)] Hyp (5) [s(a, v0) -r(v1, v1, b)] Copy 4 z := v0; x := v1 (6) [-r(v1, v1, b)] Res Bin 3, 5 v0 := b (7) [q(a, a) s(a, b)] Res Bin 1, 6 x := v1 (8) [-s(a, b)] Factor 2 z := b; y := a (9) [-p(f(a)) r(x, a, b)] Hyp (10) [s(a, v0) -r(v1, v1, b)] Copy 4 z := v0; x := v1 (11) [-p(f(a)) s(a, v0)] Res Bin 9, 10 v1 := a; x := a (12) [p(f(x)) -q(y, a)] Hyp (13) [s(a, v0) -q(y, a)] Res Bin 11, 12 x := a (14) [s(a, v1) -q(v2, a)] Copy 13 v0 := v1; y := v2 (15) [-q(v2, a)] Res Bin 8, 14 v1 := b (16) [s(a, b)] Res Bin 7, 15 v2 := a (17) [-s(a, b)] Factor 2 z := b; y := a (18) [] Res Bin 16, 17 Proof duration (in seconds): 0.000288963317871
examples
|
syntax
|
info
|
home
|
download
Last Modified : 18-Dec-2019