Model Elimination
Max time of proof
Max length of proof
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)
Proof
1: s(a, z) -r(x, x, b) Hypothesis 2: -s(a, b) [s(a, v1)]^0 -r(x, x, b) Expansion on literal 1 with hypothesis -s(v0, v1) -s(a, b) by substitution z := v1; v0 := a 3: [s(a, b)]^0 -r(x, x, b) Reduction of the literal 2 by substitution v1 := b 4: -r(x, x, b) Remove 5: q(a, a) s(a, b) [-r(v0, v0, b)]^0 Expansion on literal 2 with hypothesis q(a, a) r(v0, v0, b) s(a, b) by substitution x := v0 6: p(f(v1)) [q(a, a)]^0 s(a, b) [-r(v0, v0, b)]^0 Expansion on literal 2 with hypothesis p(f(v1)) -q(v2, a) by substitution v2 := a 7: r(v2, a, b) [p(f(a))]^0 [q(a, a)]^0 s(a, b) [-r(v0, v0, b)]^2 Expansion on literal 1 with hypothesis -p(f(a)) r(v2, a, b) by substitution v1 := a 8: [p(f(a))]^0 [q(a, a)]^0 s(a, b) [-r(a, a, b)]^1 Reduction of the literal 5 by substitution v0 := a; v2 := a 9: [q(a, a)]^0 s(a, b) [-r(a, a, b)]^1 Remove 10: s(a, b) [-r(a, a, b)]^1 Remove 11: -s(a, b) [s(a, b)]^0 [-r(a, a, b)]^2 Expansion on literal 1 with hypothesis -s(v0, v1) -s(a, b) by substitution v1 := b; v0 := a 12: [s(a, b)]^0 [-r(a, a, b)]^2 Reduction of the literal 2 13: [-r(a, a, b)]^2 Remove 14: F Remove Proof duration (in seconds): 0.0217571258545
examples
|
syntax
|
info
|
home
|
download
Last Modified : 02-Dec-2019