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