Model Elimination
Max time of proof
Max length of proof
Clauses
p(x) p(a),-p(x)
Proof
1: p(x) p(a) Hypothesis 2: [p(v0)]^0 p(a) Expansion on literal 1 with hypothesis -p(v0) by substitution x := v0 3: p(a) Remove 4: [p(a)]^0 Expansion on literal 1 with hypothesis -p(v0) by substitution v0 := a 5: F Remove Proof duration (in seconds): 4.29153442383e-05
examples
|
syntax
|
info
|
home
|
download
Last Modified : 02-Dec-2019