Resolution
Type of resolution
nor
pos
neg
Max time of proof
Max length of clauses
Max height of clauses
Max size of clauses
notrace
trace
Clauses
-A(x) B(x),-B(y) C(y),A(a),-C(a)
Proof
(1) [-A(x) B(x)] Hyp (2) [A(a)] Hyp (3) [B(a)] Res Bin 1, 2 x := a (4) [-B(y) C(y)] Hyp (5) [C(a)] Res Bin 3, 4 y := a (6) [-C(a)] Hyp (7) [] Res Bin 5, 6 Proof duration (in seconds): 4.41074371338e-05
examples
|
syntax
|
info
|
home
|
download
Last Modified : 02-Dec-2019