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