%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN720-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:20:24 PM UTC 2026
% Result : Satisfiable 0.13s 0.82s
% Output : Saturation 0.13s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
s0(d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
n0(d,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
s0(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
q0(b,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
n0(d,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
r0(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
n0(e,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : m0(a,X,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
r0(e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X] : p0(b,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
n0(a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
m0(c,b,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X] : q0(X,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
p0(c,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X,Y] : m0(X,d,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
l0(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
q0(b,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
m0(a,e,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
l0(c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
n0(d,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
m0(e,b,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
k0(e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
q0(d,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
n0(e,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
m0(b,b,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
k0(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
q0(d,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
n0(c,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
m0(d,e,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
q0(a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
n0(b,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
m0(b,a,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [I,J] :
( ~ n0(J,I)
| k1(I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [G,H] :
( ~ n0(H,G)
| l1(G,G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [C,D,E,F] :
( ~ m0(D,C,E)
| ~ r0(F)
| ~ p0(E,C)
| l1(C,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [A,B] :
( ~ l1(B,B)
| ~ l0(B)
| ~ k1(A)
| l1(A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [B,C] :
( ~ m0(C,C,B)
| m1(B,C,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [J,A] :
( ~ m0(A,A,J)
| m1(J,J,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [G,H,I] :
( ~ r0(G)
| ~ p0(I,H)
| m1(G,H,G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [B,C] :
( ~ p0(C,B)
| ~ l1(c,c)
| ~ n0(C,C)
| m1(B,B,c) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [J,A] :
( ~ n0(A,A)
| ~ k0(J)
| m1(J,J,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [B,C,D] :
( ~ m0(C,C,B)
| ~ l0(D)
| m1(B,C,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [H,I,J,A] :
( ~ m1(J,A,I)
| ~ m1(J,I,H)
| m1(H,I,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A,B] :
( ~ p0(A,B)
| ~ q0(B,d)
| ~ s0(d)
| ~ r0(c)
| m1(A,B,c) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [I,J] :
( ~ k0(J)
| ~ l0(I)
| m1(I,J,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [F,G,H] :
( ~ m1(G,c,G)
| ~ q0(F,G)
| ~ m0(a,H,a)
| m1(F,a,G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [H,I] :
( ~ s0(H)
| ~ p0(H,I)
| m1(H,I,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [G] :
( ~ k0(e)
| ~ r0(G)
| ~ m0(a,e,c)
| ~ r0(e)
| m1(c,a,c) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [A,B] :
( ~ q0(A,A)
| ~ k1(B)
| ~ k1(a)
| m1(A,B,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [I,J] :
( ~ l0(J)
| ~ r0(I)
| m1(I,J,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [A,B] :
( ~ m0(b,B,A)
| n1(A,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [H,I,J] :
( ~ r0(H)
| ~ l0(I)
| ~ p0(J,H)
| n1(H,I,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [E,F] :
( ~ m0(F,E,c)
| n1(E,c,E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [C,D] :
( ~ k1(C)
| ~ m0(C,D,e)
| n1(C,e,e) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [D,E,F] :
( ~ p0(E,F)
| ~ p0(D,D)
| n1(D,E,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [I,J] :
( ~ l1(J,d)
| ~ r0(I)
| ~ p0(J,J)
| n1(I,d,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [D,E] :
( ~ p0(b,E)
| ~ l0(D)
| ~ s0(b)
| n1(D,E,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [H] :
( ~ p0(a,b)
| ~ p0(H,d)
| n1(a,H,b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [E,F,G] :
( ~ n1(E,F,E)
| ~ l1(G,E)
| ~ l0(G)
| n1(E,F,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [H,I,J,A] :
( ~ m0(I,J,H)
| ~ m0(J,A,A)
| n1(H,H,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [D,E] :
( ~ k0(E)
| ~ n0(d,D)
| p1(D,D,E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,axiom,
! [B,C] :
( ~ p0(C,B)
| p1(B,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [H,I,J,A] :
( ~ s0(b)
| ~ p1(I,A,H)
| ~ l0(J)
| p1(H,I,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,axiom,
( ~ p0(b,a)
| p1(a,a,a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,axiom,
( ~ m0(b,c,e)
| p1(c,e,b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,axiom,
! [H,I,J,A] :
( ~ p1(J,H,A)
| ~ m0(J,H,A)
| p1(H,I,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,axiom,
! [F,G] :
( ~ k0(G)
| ~ m1(F,G,b)
| p1(F,b,G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,axiom,
! [B,C] :
( ~ p0(C,B)
| p1(B,B,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f130,axiom,
! [J,A,B,C] :
( ~ p0(C,J)
| ~ n0(B,A)
| q1(J,A,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f132,axiom,
( ~ l0(c)
| ~ k0(b)
| ~ s0(e)
| q1(b,e,e) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f133,axiom,
! [F,G] :
( ~ p0(G,F)
| q1(F,G,G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f137,axiom,
! [E,F,G] :
( ~ q1(F,F,G)
| ~ l0(E)
| ~ k0(G)
| q1(E,F,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,axiom,
! [E,F,G,H] :
( ~ q0(F,F)
| ~ p0(H,E)
| ~ r0(G)
| ~ l0(E)
| q1(E,F,E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f143,axiom,
! [C,D] :
( ~ p0(D,d)
| ~ s0(C)
| q1(C,C,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f145,axiom,
! [A] :
( ~ m0(e,d,A)
| ~ m0(A,d,A)
| q1(e,A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,axiom,
! [E,F,G] :
( ~ k1(E)
| ~ q0(F,E)
| ~ p0(G,G)
| q1(E,E,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f148,axiom,
! [B,C,D] :
( ~ m0(C,D,B)
| q1(B,B,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [H,I,J] :
( ~ m1(H,I,I)
| ~ r0(J)
| q1(H,H,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f162,axiom,
! [D,E] :
( ~ q1(d,E,d)
| ~ s0(d)
| ~ q0(D,E)
| r1(D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f163,axiom,
! [I] :
( ~ p0(I,I)
| s1(I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f164,axiom,
! [F,G,H] :
( ~ s1(H)
| ~ q0(F,G)
| s1(F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f165,axiom,
! [C,D,E,F] :
( ~ k2(F,D)
| ~ k1(F)
| ~ m1(E,D,C)
| k2(C,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f167,axiom,
! [J,A] :
( ~ q1(A,J,J)
| k2(J,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,axiom,
! [D,E] :
( ~ l2(E,E)
| ~ n0(e,E)
| ~ s1(D)
| l2(D,E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f171,axiom,
! [J,A,B,C] :
( ~ m0(C,B,J)
| ~ s1(B)
| ~ p0(A,A)
| l2(J,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [F,G,H] :
( ~ l1(G,H)
| ~ s0(F)
| m2(F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f174,axiom,
( ~ k1(b)
| m2(b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f175,axiom,
! [A,B,C] :
( ~ p1(B,C,A)
| n2(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,axiom,
! [B] :
( ~ q1(B,a,B)
| p2(B,a,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f182,axiom,
! [I] :
( ~ k2(c,a)
| ~ p0(b,I)
| ~ n1(c,I,I)
| ~ r0(e)
| p2(b,c,a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f183,axiom,
! [G,H] :
( ~ p1(G,H,e)
| ~ r0(e)
| p2(e,G,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f184,axiom,
! [C,D,E,F] :
( ~ p2(C,D,C)
| ~ l1(E,F)
| ~ p1(C,E,F)
| p2(C,D,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f187,axiom,
! [H,I] :
( ~ m0(I,H,d)
| ~ r1(a)
| p2(H,H,d) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f188,axiom,
! [F,G] :
( ~ m1(G,G,F)
| p2(F,F,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,axiom,
! [H,I,J] :
( ~ p2(e,H,I)
| ~ k1(J)
| p2(H,I,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,axiom,
! [F,G] :
( ~ q1(a,G,F)
| ~ n1(e,F,a)
| p2(F,e,G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,axiom,
! [B,C,D] :
( ~ p2(B,D,B)
| ~ s0(e)
| ~ s1(c)
| ~ q1(c,B,D)
| p2(B,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,axiom,
! [G] :
( ~ q1(e,c,G)
| ~ n1(e,e,G)
| ~ p1(G,b,b)
| p2(b,c,c) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f204,axiom,
! [H] :
( ~ m1(a,H,d)
| ~ n0(H,d)
| p2(a,H,d) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f206,axiom,
( ~ m1(d,a,c)
| ~ r1(e)
| ~ l2(e,b)
| ~ l1(e,c)
| p2(a,c,b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f214,axiom,
! [D,E] :
( ~ m1(E,D,E)
| p2(D,E,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f215,axiom,
! [E,F] :
( ~ p1(E,E,E)
| ~ k0(F)
| q2(E,F,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f217,axiom,
! [J,A] :
( ~ n1(J,J,A)
| ~ k1(A)
| q2(J,J,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f218,axiom,
( ~ q0(e,c)
| ~ s1(c)
| ~ q2(d,c,a)
| q2(d,a,a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f220,axiom,
! [F,G,H] :
( ~ q2(G,H,F)
| ~ n1(G,F,H)
| ~ p1(F,F,H)
| q2(F,G,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f221,axiom,
! [D,E] :
( ~ l2(E,D)
| ~ l0(c)
| ~ k1(E)
| q2(D,c,E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f224,axiom,
! [G,H] :
( ~ l1(H,G)
| q2(G,G,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f225,axiom,
! [C,D,E,F] :
( ~ q2(D,D,D)
| ~ k0(D)
| ~ m0(E,F,C)
| ~ r1(D)
| q2(C,D,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f226,axiom,
! [G] :
( ~ l0(G)
| ~ r1(G)
| r2(G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f227,axiom,
! [H] :
( ~ s1(b)
| ~ q2(b,H,b)
| s2(H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f228,axiom,
( ~ s0(d)
| ~ s1(a)
| s2(d) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f230,axiom,
! [J,A,B,C] :
( ~ n0(J,C)
| ~ p2(B,A,C)
| ~ s1(A)
| k3(J,A,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f232,axiom,
! [F,G] :
( ~ k2(G,F)
| k3(F,F,G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f239,axiom,
! [B,C,D,E] :
( ~ m2(D)
| ~ m2(E)
| ~ p1(C,D,B)
| k3(B,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f240,axiom,
! [G,H,I,J,A] :
( ~ k3(H,A,J)
| ~ k2(G,J)
| ~ q0(I,H)
| k3(G,G,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f244,axiom,
! [C,D] :
( ~ p2(D,C,C)
| k3(C,D,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f248,axiom,
! [D] :
( ~ n2(D)
| k3(D,D,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f253,axiom,
! [G,H] :
( ~ p2(G,H,G)
| ~ r0(G)
| l3(G,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f255,axiom,
! [C] :
( ~ m2(b)
| ~ n2(C)
| l3(C,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f262,axiom,
( ~ r0(b)
| ~ k3(a,c,a)
| ~ s2(d)
| l3(d,c) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f263,axiom,
! [J,A,B,C] :
( ~ s2(B)
| ~ m0(J,C,C)
| ~ l2(C,J)
| ~ m0(B,B,A)
| m3(J,A,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f266,axiom,
! [J,A,B] :
( ~ m3(B,J,B)
| ~ m2(A)
| ~ n2(J)
| m3(J,A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f268,axiom,
( ~ q2(b,c,d)
| ~ m2(d)
| ~ l1(d,b)
| m3(c,b,d) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f269,axiom,
! [H,I] :
( ~ k2(c,I)
| ~ r2(H)
| m3(H,I,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f272,axiom,
! [D] :
( ~ p2(D,e,e)
| ~ n2(e)
| m3(D,e,e) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f273,axiom,
! [B,C] :
( ~ k3(B,C,B)
| ~ r2(C)
| m3(B,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f274,axiom,
! [A] :
( ~ n2(A)
| m3(A,A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f275,axiom,
! [J] :
( ~ q2(J,c,c)
| ~ s2(c)
| m3(J,c,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f278,axiom,
! [D,E,F] :
( ~ p2(E,F,D)
| n3(D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f279,axiom,
! [C,D,E,F] :
( ~ k2(D,E)
| ~ q2(F,d,C)
| p3(C,D,E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f280,axiom,
! [J,A,B] :
( ~ k3(A,B,J)
| ~ r2(A)
| p3(J,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f281,axiom,
! [I] :
( ~ q2(I,d,I)
| ~ n3(I)
| ~ p2(d,b,c)
| ~ l3(b,e)
| p3(I,d,e) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f282,axiom,
! [H] :
( ~ n2(H)
| p3(H,H,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f289,axiom,
! [A,B,C,D] :
( ~ p2(A,B,D)
| ~ m3(B,C,D)
| p3(A,B,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f291,axiom,
( ~ k2(c,b)
| p3(b,c,b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f292,axiom,
! [G] :
( ~ q2(G,G,b)
| ~ m3(e,G,e)
| p3(e,b,e) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f293,axiom,
! [G,H,I] :
( ~ n0(I,G)
| ~ q2(I,G,H)
| q3(G,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f294,axiom,
! [E,F] :
( ~ q3(F,E)
| ~ p2(F,E,E)
| q3(E,E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f295,axiom,
! [B,C,D] :
( ~ q3(C,B)
| ~ s2(B)
| ~ n1(D,B,C)
| q3(B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f296,axiom,
! [I,J,A] :
( ~ l2(A,A)
| ~ s1(J)
| ~ r2(I)
| q3(I,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f297,axiom,
! [G,H] :
( ~ q3(H,G)
| ~ r2(d)
| ~ k1(G)
| ~ m0(H,d,H)
| q3(G,G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f298,axiom,
! [G,H] :
( ~ l2(c,G)
| ~ s2(H)
| r3(G,H,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f305,axiom,
! [B,C,D] :
( ~ p2(B,D,C)
| r3(B,C,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f306,axiom,
! [H,I,J,A] :
( ~ r3(I,A,A)
| ~ m3(J,b,H)
| ~ m2(I)
| r3(H,H,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f307,axiom,
! [G] :
( ~ m3(a,G,G)
| ~ m2(b)
| ~ q2(G,e,G)
| ~ k2(a,a)
| r3(a,a,e) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f310,axiom,
! [J,A,B] :
( ~ r3(B,J,J)
| ~ r2(B)
| ~ k2(A,B)
| r3(J,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f311,axiom,
! [I,J,A,B] :
( ~ m0(A,B,J)
| ~ s2(I)
| ~ q2(A,I,A)
| s3(I,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f312,axiom,
( ~ n3(e)
| ~ q3(e,b)
| ~ n0(c,d)
| k4(c) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f314,axiom,
! [C,D] :
( ~ r3(C,e,D)
| ~ q1(a,a,D)
| ~ q3(C,C)
| k4(e) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f315,axiom,
! [J,A,B] :
( ~ p3(A,B,J)
| l4(J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f317,axiom,
! [E,F,G] :
( ~ s3(a,E)
| ~ l2(G,F)
| m4(E,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f319,axiom,
! [J,A] :
( ~ n4(J,J)
| ~ p3(J,A,A)
| n4(J,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f322,axiom,
! [H,I] :
( ~ m3(H,H,H)
| ~ k4(I)
| n4(H,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f323,axiom,
! [G,H] :
( ~ r3(H,G,H)
| ~ r0(G)
| p4(G,G,H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f325,axiom,
! [B,C] :
( ~ k3(B,B,C)
| p4(B,C,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f326,axiom,
! [H,I,J,A] :
( ~ p4(J,J,A)
| ~ r3(I,I,H)
| p4(H,I,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f332,axiom,
! [B] :
( ~ m3(B,c,a)
| ~ n3(a)
| p4(c,c,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f333,axiom,
! [B,C,D,E,F] :
( ~ m3(E,F,E)
| ~ q2(E,C,B)
| ~ k3(D,D,B)
| q4(B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f334,axiom,
! [I,J,A] :
( ~ q4(J,A)
| ~ l4(J)
| ~ r1(I)
| q4(I,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f336,axiom,
! [G,H,I,J] :
( ~ p0(J,G)
| ~ q3(H,I)
| ~ n3(G)
| r4(G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f337,axiom,
! [A,B,C,D] :
( ~ l1(A,C)
| ~ p3(B,C,D)
| s4(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f338,axiom,
! [E,F,G] :
( ~ r3(G,E,E)
| ~ s4(F)
| k5(E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f340,axiom,
! [H,I] :
( ~ k1(H)
| ~ q4(I,I)
| l5(H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f341,axiom,
! [D,E,F] :
( ~ p4(D,F,E)
| ~ r0(D)
| m5(D,E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f342,axiom,
! [C] :
( ~ k4(C)
| m5(C,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f343,axiom,
! [B] :
( ~ m4(e,e)
| ~ s4(B)
| m5(B,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f344,axiom,
! [J,A] :
( ~ r0(J)
| ~ s4(A)
| m5(J,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f345,axiom,
! [B,C,D,E,F] :
( ~ n5(F,C)
| ~ p4(F,F,C)
| ~ n4(B,E)
| ~ q4(D,E)
| n5(B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f352,axiom,
! [B] :
( ~ r4(B)
| n5(B,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f356,axiom,
! [E,F] :
( ~ l2(E,E)
| ~ s4(F)
| p5(E,E,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f357,axiom,
! [B,C,D] :
( ~ m4(D,C)
| ~ p5(B,D,B)
| ~ l2(B,D)
| p5(B,C,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f358,axiom,
! [I,J,A] :
( ~ s1(I)
| ~ q4(J,A)
| p5(I,J,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f360,axiom,
! [J,A] :
( ~ m2(A)
| ~ s4(J)
| q5(J,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f362,axiom,
! [I] :
( ~ l4(I)
| q5(I,I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f365,axiom,
! [C,D] :
( ~ n3(D)
| ~ k0(b)
| ~ s4(C)
| r5(C,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f366,axiom,
! [B] :
( ~ k4(B)
| r5(B,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f367,axiom,
! [H,I] :
( ~ r4(I)
| ~ l4(H)
| s5(H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f369,plain,
s0(d),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f371,plain,
n0(d,e),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f373,plain,
s0(b),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f374,plain,
q0(b,b),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f375,plain,
n0(d,b),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f377,plain,
r0(b),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f379,plain,
n0(e,b),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f380,plain,
! [X0] : m0(a,X0,a),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f381,plain,
r0(e),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f382,plain,
! [X0] : p0(b,X0),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f383,plain,
n0(a,b),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f384,plain,
m0(c,b,a),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f385,plain,
! [X0] : q0(X0,d),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f386,plain,
p0(c,b),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f387,plain,
! [X0,X1] : m0(X0,d,X1),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f388,plain,
l0(a),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f389,plain,
q0(b,e),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f391,plain,
m0(a,e,e),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f392,plain,
l0(c),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f394,plain,
n0(d,c),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f395,plain,
m0(e,b,c),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f396,plain,
k0(e),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f397,plain,
q0(d,b),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f398,plain,
n0(e,e),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f399,plain,
m0(b,b,e),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f400,plain,
k0(b),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f401,plain,
q0(d,c),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f402,plain,
n0(c,d),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f403,plain,
m0(d,e,c),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f404,plain,
q0(a,b),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f405,plain,
n0(b,a),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f406,plain,
m0(b,a,a),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f407,plain,
! [I] :
( ! [J] : ~ n0(J,I)
| k1(I) ),
inference(miniscoping,[status(thm)],[f39]) ).
fof(f408,plain,
! [X0,X1] :
( ~ n0(X1,X0)
| k1(X0) ),
inference(cnf_transformation,[status(thm)],[f407]) ).
fof(f409,plain,
! [G] :
( ! [H] : ~ n0(H,G)
| l1(G,G) ),
inference(miniscoping,[status(thm)],[f40]) ).
fof(f410,plain,
! [X0,X1] :
( ~ n0(X1,X0)
| l1(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f409]) ).
fof(f411,plain,
! [C,D,E] :
( ~ m0(D,C,E)
| ! [F] : ~ r0(F)
| ~ p0(E,C)
| l1(C,D) ),
inference(miniscoping,[status(thm)],[f41]) ).
fof(f412,plain,
! [X0,X1,X2,X3] :
( ~ m0(X1,X0,X2)
| ~ r0(X3)
| ~ p0(X2,X0)
| l1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f411]) ).
fof(f413,plain,
! [B] :
( ~ l1(B,B)
| ~ l0(B)
| ! [A] :
( ~ k1(A)
| l1(A,A) ) ),
inference(miniscoping,[status(thm)],[f42]) ).
fof(f414,plain,
! [X0,X1] :
( ~ l1(X1,X1)
| ~ l0(X1)
| ~ k1(X0)
| l1(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f413]) ).
fof(f415,plain,
! [X0,X1] :
( ~ m0(X1,X1,X0)
| m1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f416,plain,
! [J] :
( ! [A] : ~ m0(A,A,J)
| m1(J,J,J) ),
inference(miniscoping,[status(thm)],[f44]) ).
fof(f417,plain,
! [X0,X1] :
( ~ m0(X1,X1,X0)
| m1(X0,X0,X0) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f418,plain,
! [G] :
( ~ r0(G)
| ! [H] :
( ! [I] : ~ p0(I,H)
| m1(G,H,G) ) ),
inference(miniscoping,[status(thm)],[f45]) ).
fof(f419,plain,
! [X0,X1,X2] :
( ~ r0(X0)
| ~ p0(X2,X1)
| m1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f423,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| ~ l1(c,c)
| ~ n0(X1,X1)
| m1(X0,X0,c) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f424,plain,
! [A] :
( ~ n0(A,A)
| ! [J] :
( ~ k0(J)
| m1(J,J,A) ) ),
inference(miniscoping,[status(thm)],[f49]) ).
fof(f425,plain,
! [X0,X1] :
( ~ n0(X1,X1)
| ~ k0(X0)
| m1(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f424]) ).
fof(f431,plain,
! [B,C] :
( ~ m0(C,C,B)
| ! [D] : ~ l0(D)
| m1(B,C,C) ),
inference(miniscoping,[status(thm)],[f53]) ).
fof(f432,plain,
! [X0,X1,X2] :
( ~ m0(X1,X1,X0)
| ~ l0(X2)
| m1(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f433,plain,
! [I,J] :
( ! [A] : ~ m1(J,A,I)
| ! [H] :
( ~ m1(J,I,H)
| m1(H,I,I) ) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f434,plain,
! [X0,X1,X2,X3] :
( ~ m1(X2,X3,X1)
| ~ m1(X2,X1,X0)
| m1(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f433]) ).
fof(f439,plain,
! [X0,X1] :
( ~ p0(X0,X1)
| ~ q0(X1,d)
| ~ s0(d)
| ~ r0(c)
| m1(X0,X1,c) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f441,plain,
! [J] :
( ~ k0(J)
| ! [I] :
( ~ l0(I)
| m1(I,J,I) ) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f442,plain,
! [X0,X1] :
( ~ k0(X1)
| ~ l0(X0)
| m1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f441]) ).
fof(f445,plain,
! [G] :
( ~ m1(G,c,G)
| ! [F] :
( ~ q0(F,G)
| ! [H] : ~ m0(a,H,a)
| m1(F,a,G) ) ),
inference(miniscoping,[status(thm)],[f62]) ).
fof(f446,plain,
! [X0,X1,X2] :
( ~ m1(X1,c,X1)
| ~ q0(X0,X1)
| ~ m0(a,X2,a)
| m1(X0,a,X1) ),
inference(cnf_transformation,[status(thm)],[f445]) ).
fof(f453,plain,
! [H] :
( ~ s0(H)
| ! [I] :
( ~ p0(H,I)
| m1(H,I,H) ) ),
inference(miniscoping,[status(thm)],[f67]) ).
fof(f454,plain,
! [X0,X1] :
( ~ s0(X0)
| ~ p0(X0,X1)
| m1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f453]) ).
fof(f456,plain,
( ~ k0(e)
| ! [G] : ~ r0(G)
| ~ m0(a,e,c)
| ~ r0(e)
| m1(c,a,c) ),
inference(miniscoping,[status(thm)],[f69]) ).
fof(f457,plain,
! [X0] :
( ~ k0(e)
| ~ r0(X0)
| ~ m0(a,e,c)
| ~ r0(e)
| m1(c,a,c) ),
inference(cnf_transformation,[status(thm)],[f456]) ).
fof(f461,plain,
! [A] :
( ~ q0(A,A)
| ! [B] :
( ~ k1(B)
| ~ k1(a)
| m1(A,B,B) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f462,plain,
! [X0,X1] :
( ~ q0(X0,X0)
| ~ k1(X1)
| ~ k1(a)
| m1(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f461]) ).
fof(f463,plain,
! [J] :
( ~ l0(J)
| ! [I] :
( ~ r0(I)
| m1(I,J,I) ) ),
inference(miniscoping,[status(thm)],[f73]) ).
fof(f464,plain,
! [X0,X1] :
( ~ l0(X1)
| ~ r0(X0)
| m1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f463]) ).
fof(f465,plain,
! [X0,X1] :
( ~ m0(b,X1,X0)
| n1(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f466,plain,
! [H] :
( ~ r0(H)
| ! [I] :
( ~ l0(I)
| ! [J] : ~ p0(J,H)
| n1(H,I,H) ) ),
inference(miniscoping,[status(thm)],[f75]) ).
fof(f467,plain,
! [X0,X1,X2] :
( ~ r0(X0)
| ~ l0(X1)
| ~ p0(X2,X0)
| n1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f466]) ).
fof(f469,plain,
! [E] :
( ! [F] : ~ m0(F,E,c)
| n1(E,c,E) ),
inference(miniscoping,[status(thm)],[f77]) ).
fof(f470,plain,
! [X0,X1] :
( ~ m0(X1,X0,c)
| n1(X0,c,X0) ),
inference(cnf_transformation,[status(thm)],[f469]) ).
fof(f471,plain,
! [C] :
( ~ k1(C)
| ! [D] : ~ m0(C,D,e)
| n1(C,e,e) ),
inference(miniscoping,[status(thm)],[f78]) ).
fof(f472,plain,
! [X0,X1] :
( ~ k1(X0)
| ~ m0(X0,X1,e)
| n1(X0,e,e) ),
inference(cnf_transformation,[status(thm)],[f471]) ).
fof(f477,plain,
! [E] :
( ! [F] : ~ p0(E,F)
| ! [D] :
( ~ p0(D,D)
| n1(D,E,D) ) ),
inference(miniscoping,[status(thm)],[f82]) ).
fof(f478,plain,
! [X0,X1,X2] :
( ~ p0(X1,X2)
| ~ p0(X0,X0)
| n1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f477]) ).
fof(f482,plain,
! [J] :
( ~ l1(J,d)
| ! [I] :
( ~ r0(I)
| ~ p0(J,J)
| n1(I,d,J) ) ),
inference(miniscoping,[status(thm)],[f85]) ).
fof(f483,plain,
! [X0,X1] :
( ~ l1(X1,d)
| ~ r0(X0)
| ~ p0(X1,X1)
| n1(X0,d,X1) ),
inference(cnf_transformation,[status(thm)],[f482]) ).
fof(f487,plain,
! [E] :
( ~ p0(b,E)
| ! [D] :
( ~ l0(D)
| ~ s0(b)
| n1(D,E,D) ) ),
inference(miniscoping,[status(thm)],[f88]) ).
fof(f488,plain,
! [X0,X1] :
( ~ p0(b,X1)
| ~ l0(X0)
| ~ s0(b)
| n1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f487]) ).
fof(f492,plain,
( ~ p0(a,b)
| ! [H] :
( ~ p0(H,d)
| n1(a,H,b) ) ),
inference(miniscoping,[status(thm)],[f91]) ).
fof(f493,plain,
! [X0] :
( ~ p0(a,b)
| ~ p0(X0,d)
| n1(a,X0,b) ),
inference(cnf_transformation,[status(thm)],[f492]) ).
fof(f494,plain,
! [E,F] :
( ~ n1(E,F,E)
| ! [G] :
( ~ l1(G,E)
| ~ l0(G)
| n1(E,F,F) ) ),
inference(miniscoping,[status(thm)],[f92]) ).
fof(f495,plain,
! [X0,X1,X2] :
( ~ n1(X0,X1,X0)
| ~ l1(X2,X0)
| ~ l0(X2)
| n1(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f494]) ).
fof(f500,plain,
! [H,I,J] :
( ~ m0(I,J,H)
| ! [A] : ~ m0(J,A,A)
| n1(H,H,I) ),
inference(miniscoping,[status(thm)],[f97]) ).
fof(f501,plain,
! [X0,X1,X2,X3] :
( ~ m0(X1,X2,X0)
| ~ m0(X2,X3,X3)
| n1(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f500]) ).
fof(f506,plain,
! [E] :
( ~ k0(E)
| ! [D] :
( ~ n0(d,D)
| p1(D,D,E) ) ),
inference(miniscoping,[status(thm)],[f101]) ).
fof(f507,plain,
! [X0,X1] :
( ~ k0(X1)
| ~ n0(d,X0)
| p1(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f506]) ).
fof(f517,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| p1(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f519,plain,
( ~ s0(b)
| ! [H,I] :
( ! [A] : ~ p1(I,A,H)
| ! [J] : ~ l0(J)
| p1(H,I,H) ) ),
inference(miniscoping,[status(thm)],[f109]) ).
fof(f520,plain,
! [X0,X1,X2,X3] :
( ~ s0(b)
| ~ p1(X1,X3,X0)
| ~ l0(X2)
| p1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f519]) ).
fof(f527,plain,
( ~ p0(b,a)
| p1(a,a,a) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f529,plain,
( ~ m0(b,c,e)
| p1(c,e,b) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f537,plain,
! [H,J,A] :
( ~ p1(J,H,A)
| ~ m0(J,H,A)
| ! [I] : p1(H,I,J) ),
inference(miniscoping,[status(thm)],[f120]) ).
fof(f538,plain,
! [X0,X1,X2,X3] :
( ~ p1(X2,X0,X3)
| ~ m0(X2,X0,X3)
| p1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f537]) ).
fof(f539,plain,
! [G] :
( ~ k0(G)
| ! [F] :
( ~ m1(F,G,b)
| p1(F,b,G) ) ),
inference(miniscoping,[status(thm)],[f121]) ).
fof(f540,plain,
! [X0,X1] :
( ~ k0(X1)
| ~ m1(X0,X1,b)
| p1(X0,b,X1) ),
inference(cnf_transformation,[status(thm)],[f539]) ).
fof(f543,plain,
! [B] :
( ! [C] : ~ p0(C,B)
| p1(B,B,B) ),
inference(miniscoping,[status(thm)],[f123]) ).
fof(f544,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| p1(X0,X0,X0) ),
inference(cnf_transformation,[status(thm)],[f543]) ).
fof(f553,plain,
! [J] :
( ! [C] : ~ p0(C,J)
| ! [A] :
( ! [B] : ~ n0(B,A)
| q1(J,A,J) ) ),
inference(miniscoping,[status(thm)],[f130]) ).
fof(f554,plain,
! [X0,X1,X2,X3] :
( ~ p0(X3,X0)
| ~ n0(X2,X1)
| q1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f553]) ).
fof(f557,plain,
( ~ l0(c)
| ~ k0(b)
| ~ s0(e)
| q1(b,e,e) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f558,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| q1(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f564,plain,
! [F,G] :
( ~ q1(F,F,G)
| ! [E] :
( ~ l0(E)
| ~ k0(G)
| q1(E,F,F) ) ),
inference(miniscoping,[status(thm)],[f137]) ).
fof(f565,plain,
! [X0,X1,X2] :
( ~ q1(X1,X1,X2)
| ~ l0(X0)
| ~ k0(X2)
| q1(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f564]) ).
fof(f572,plain,
! [F] :
( ~ q0(F,F)
| ! [E] :
( ! [H] : ~ p0(H,E)
| ! [G] : ~ r0(G)
| ~ l0(E)
| q1(E,F,E) ) ),
inference(miniscoping,[status(thm)],[f142]) ).
fof(f573,plain,
! [X0,X1,X2,X3] :
( ~ q0(X1,X1)
| ~ p0(X3,X0)
| ~ r0(X2)
| ~ l0(X0)
| q1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f572]) ).
fof(f574,plain,
! [D] :
( ~ p0(D,d)
| ! [C] :
( ~ s0(C)
| q1(C,C,D) ) ),
inference(miniscoping,[status(thm)],[f143]) ).
fof(f575,plain,
! [X0,X1] :
( ~ p0(X1,d)
| ~ s0(X0)
| q1(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f574]) ).
fof(f577,plain,
! [X0] :
( ~ m0(e,d,X0)
| ~ m0(X0,d,X0)
| q1(e,X0,X0) ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f580,plain,
! [E] :
( ~ k1(E)
| ! [F] :
( ~ q0(F,E)
| ! [G] : ~ p0(G,G)
| q1(E,E,F) ) ),
inference(miniscoping,[status(thm)],[f147]) ).
fof(f581,plain,
! [X0,X1,X2] :
( ~ k1(X0)
| ~ q0(X1,X0)
| ~ p0(X2,X2)
| q1(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f580]) ).
fof(f582,plain,
! [B] :
( ! [C,D] : ~ m0(C,D,B)
| q1(B,B,B) ),
inference(miniscoping,[status(thm)],[f148]) ).
fof(f583,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| q1(X0,X0,X0) ),
inference(cnf_transformation,[status(thm)],[f582]) ).
fof(f587,plain,
! [H,I] :
( ~ m1(H,I,I)
| ! [J] : ~ r0(J)
| q1(H,H,I) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f588,plain,
! [X0,X1,X2] :
( ~ m1(X0,X1,X1)
| ~ r0(X2)
| q1(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f587]) ).
fof(f604,plain,
! [E] :
( ~ q1(d,E,d)
| ~ s0(d)
| ! [D] :
( ~ q0(D,E)
| r1(D) ) ),
inference(miniscoping,[status(thm)],[f162]) ).
fof(f605,plain,
! [X0,X1] :
( ~ q1(d,X1,d)
| ~ s0(d)
| ~ q0(X0,X1)
| r1(X0) ),
inference(cnf_transformation,[status(thm)],[f604]) ).
fof(f606,plain,
! [X0] :
( ~ p0(X0,X0)
| s1(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f607,plain,
( ! [H] : ~ s1(H)
| ! [F] :
( ! [G] : ~ q0(F,G)
| s1(F) ) ),
inference(miniscoping,[status(thm)],[f164]) ).
fof(f608,plain,
! [X0,X1,X2] :
( ~ s1(X2)
| ~ q0(X0,X1)
| s1(X0) ),
inference(cnf_transformation,[status(thm)],[f607]) ).
fof(f609,plain,
! [D,F] :
( ~ k2(F,D)
| ~ k1(F)
| ! [C] :
( ! [E] : ~ m1(E,D,C)
| k2(C,D) ) ),
inference(miniscoping,[status(thm)],[f165]) ).
fof(f610,plain,
! [X0,X1,X2,X3] :
( ~ k2(X3,X1)
| ~ k1(X3)
| ~ m1(X2,X1,X0)
| k2(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f609]) ).
fof(f612,plain,
! [J] :
( ! [A] : ~ q1(A,J,J)
| k2(J,J) ),
inference(miniscoping,[status(thm)],[f167]) ).
fof(f613,plain,
! [X0,X1] :
( ~ q1(X1,X0,X0)
| k2(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f612]) ).
fof(f615,plain,
! [E] :
( ~ l2(E,E)
| ~ n0(e,E)
| ! [D] :
( ~ s1(D)
| l2(D,E) ) ),
inference(miniscoping,[status(thm)],[f169]) ).
fof(f616,plain,
! [X0,X1] :
( ~ l2(X1,X1)
| ~ n0(e,X1)
| ~ s1(X0)
| l2(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f618,plain,
! [J,B] :
( ! [C] : ~ m0(C,B,J)
| ~ s1(B)
| ! [A] : ~ p0(A,A)
| l2(J,J) ),
inference(miniscoping,[status(thm)],[f171]) ).
fof(f619,plain,
! [X0,X1,X2,X3] :
( ~ m0(X3,X2,X0)
| ~ s1(X2)
| ~ p0(X1,X1)
| l2(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f618]) ).
fof(f622,plain,
( ! [G,H] : ~ l1(G,H)
| ! [F] :
( ~ s0(F)
| m2(F) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f623,plain,
! [X0,X1,X2] :
( ~ l1(X1,X2)
| ~ s0(X0)
| m2(X0) ),
inference(cnf_transformation,[status(thm)],[f622]) ).
fof(f624,plain,
( ~ k1(b)
| m2(b) ),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f625,plain,
! [A] :
( ! [B,C] : ~ p1(B,C,A)
| n2(A) ),
inference(miniscoping,[status(thm)],[f175]) ).
fof(f626,plain,
! [X0,X1,X2] :
( ~ p1(X1,X2,X0)
| n2(X0) ),
inference(cnf_transformation,[status(thm)],[f625]) ).
fof(f631,plain,
! [X0] :
( ~ q1(X0,a,X0)
| p2(X0,a,X0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f635,plain,
( ~ k2(c,a)
| ! [I] :
( ~ p0(b,I)
| ~ n1(c,I,I)
| ~ r0(e)
| p2(b,c,a) ) ),
inference(miniscoping,[status(thm)],[f182]) ).
fof(f636,plain,
! [X0] :
( ~ k2(c,a)
| ~ p0(b,X0)
| ~ n1(c,X0,X0)
| ~ r0(e)
| p2(b,c,a) ),
inference(cnf_transformation,[status(thm)],[f635]) ).
fof(f637,plain,
! [X0,X1] :
( ~ p1(X0,X1,e)
| ~ r0(e)
| p2(e,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f638,plain,
! [C,D] :
( ~ p2(C,D,C)
| ! [E,F] :
( ~ l1(E,F)
| ~ p1(C,E,F)
| p2(C,D,D) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f639,plain,
! [X0,X1,X2,X3] :
( ~ p2(X0,X1,X0)
| ~ l1(X2,X3)
| ~ p1(X0,X2,X3)
| p2(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f638]) ).
fof(f643,plain,
! [H] :
( ! [I] : ~ m0(I,H,d)
| ~ r1(a)
| p2(H,H,d) ),
inference(miniscoping,[status(thm)],[f187]) ).
fof(f644,plain,
! [X0,X1] :
( ~ m0(X1,X0,d)
| ~ r1(a)
| p2(X0,X0,d) ),
inference(cnf_transformation,[status(thm)],[f643]) ).
fof(f645,plain,
! [F] :
( ! [G] : ~ m1(G,G,F)
| p2(F,F,F) ),
inference(miniscoping,[status(thm)],[f188]) ).
fof(f646,plain,
! [X0,X1] :
( ~ m1(X1,X1,X0)
| p2(X0,X0,X0) ),
inference(cnf_transformation,[status(thm)],[f645]) ).
fof(f652,plain,
! [H,I] :
( ~ p2(e,H,I)
| ! [J] : ~ k1(J)
| p2(H,I,I) ),
inference(miniscoping,[status(thm)],[f193]) ).
fof(f653,plain,
! [X0,X1,X2] :
( ~ p2(e,X0,X1)
| ~ k1(X2)
| p2(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f652]) ).
fof(f654,plain,
! [X0,X1] :
( ~ q1(a,X1,X0)
| ~ n1(e,X0,a)
| p2(X0,e,X1) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f656,plain,
! [B,D] :
( ~ p2(B,D,B)
| ~ s0(e)
| ~ s1(c)
| ~ q1(c,B,D)
| ! [C] : p2(B,B,C) ),
inference(miniscoping,[status(thm)],[f196]) ).
fof(f657,plain,
! [X0,X1,X2] :
( ~ p2(X0,X2,X0)
| ~ s0(e)
| ~ s1(c)
| ~ q1(c,X0,X2)
| p2(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f656]) ).
fof(f662,plain,
! [X0] :
( ~ q1(e,c,X0)
| ~ n1(e,e,X0)
| ~ p1(X0,b,b)
| p2(b,c,c) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f669,plain,
! [X0] :
( ~ m1(a,X0,d)
| ~ n0(X0,d)
| p2(a,X0,d) ),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f671,plain,
( ~ m1(d,a,c)
| ~ r1(e)
| ~ l2(e,b)
| ~ l1(e,c)
| p2(a,c,b) ),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f684,plain,
! [X0,X1] :
( ~ m1(X1,X0,X1)
| p2(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f685,plain,
! [E] :
( ~ p1(E,E,E)
| ! [F] :
( ~ k0(F)
| q2(E,F,F) ) ),
inference(miniscoping,[status(thm)],[f215]) ).
fof(f686,plain,
! [X0,X1] :
( ~ p1(X0,X0,X0)
| ~ k0(X1)
| q2(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f685]) ).
fof(f689,plain,
! [X0,X1] :
( ~ n1(X0,X0,X1)
| ~ k1(X1)
| q2(X0,X0,X0) ),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f690,plain,
( ~ q0(e,c)
| ~ s1(c)
| ~ q2(d,c,a)
| q2(d,a,a) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f692,plain,
! [X0,X1,X2] :
( ~ q2(X1,X2,X0)
| ~ n1(X1,X0,X2)
| ~ p1(X0,X0,X2)
| q2(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f693,plain,
! [X0,X1] :
( ~ l2(X1,X0)
| ~ l0(c)
| ~ k1(X1)
| q2(X0,c,X1) ),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f698,plain,
! [X0,X1] :
( ~ l1(X1,X0)
| q2(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f699,plain,
! [D] :
( ~ q2(D,D,D)
| ~ k0(D)
| ! [C] :
( ! [E,F] : ~ m0(E,F,C)
| ~ r1(D)
| q2(C,D,C) ) ),
inference(miniscoping,[status(thm)],[f225]) ).
fof(f700,plain,
! [X0,X1,X2,X3] :
( ~ q2(X1,X1,X1)
| ~ k0(X1)
| ~ m0(X2,X3,X0)
| ~ r1(X1)
| q2(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f701,plain,
! [X0] :
( ~ l0(X0)
| ~ r1(X0)
| r2(X0) ),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f702,plain,
( ~ s1(b)
| ! [H] :
( ~ q2(b,H,b)
| s2(H) ) ),
inference(miniscoping,[status(thm)],[f227]) ).
fof(f703,plain,
! [X0] :
( ~ s1(b)
| ~ q2(b,X0,b)
| s2(X0) ),
inference(cnf_transformation,[status(thm)],[f702]) ).
fof(f704,plain,
( ~ s0(d)
| ~ s1(a)
| s2(d) ),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f706,plain,
! [J,C] :
( ~ n0(J,C)
| ! [A] :
( ! [B] : ~ p2(B,A,C)
| ~ s1(A)
| k3(J,A,J) ) ),
inference(miniscoping,[status(thm)],[f230]) ).
fof(f707,plain,
! [X0,X1,X2,X3] :
( ~ n0(X0,X3)
| ~ p2(X2,X1,X3)
| ~ s1(X1)
| k3(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f706]) ).
fof(f710,plain,
! [X0,X1] :
( ~ k2(X1,X0)
| k3(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f720,plain,
! [D] :
( ~ m2(D)
| ! [E] : ~ m2(E)
| ! [B,C] :
( ~ p1(C,D,B)
| k3(B,B,C) ) ),
inference(miniscoping,[status(thm)],[f239]) ).
fof(f721,plain,
! [X0,X1,X2,X3] :
( ~ m2(X2)
| ~ m2(X3)
| ~ p1(X1,X2,X0)
| k3(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f720]) ).
fof(f722,plain,
! [H,J] :
( ! [A] : ~ k3(H,A,J)
| ! [G] :
( ~ k2(G,J)
| ! [I] : ~ q0(I,H)
| k3(G,G,H) ) ),
inference(miniscoping,[status(thm)],[f240]) ).
fof(f723,plain,
! [X0,X1,X2,X3,X4] :
( ~ k3(X1,X4,X3)
| ~ k2(X0,X3)
| ~ q0(X2,X1)
| k3(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f722]) ).
fof(f728,plain,
! [X0,X1] :
( ~ p2(X1,X0,X0)
| k3(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f734,plain,
! [X0] :
( ~ n2(X0)
| k3(X0,X0,X0) ),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f741,plain,
! [X0,X1] :
( ~ p2(X0,X1,X0)
| ~ r0(X0)
| l3(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f744,plain,
( ~ m2(b)
| ! [C] :
( ~ n2(C)
| l3(C,C) ) ),
inference(miniscoping,[status(thm)],[f255]) ).
fof(f745,plain,
! [X0] :
( ~ m2(b)
| ~ n2(X0)
| l3(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f744]) ).
fof(f755,plain,
( ~ r0(b)
| ~ k3(a,c,a)
| ~ s2(d)
| l3(d,c) ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f756,plain,
! [B] :
( ~ s2(B)
| ! [J,C] :
( ~ m0(J,C,C)
| ~ l2(C,J)
| ! [A] :
( ~ m0(B,B,A)
| m3(J,A,J) ) ) ),
inference(miniscoping,[status(thm)],[f263]) ).
fof(f757,plain,
! [X0,X1,X2,X3] :
( ~ s2(X2)
| ~ m0(X0,X3,X3)
| ~ l2(X3,X0)
| ~ m0(X2,X2,X1)
| m3(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f756]) ).
fof(f762,plain,
! [J] :
( ! [B] : ~ m3(B,J,B)
| ! [A] :
( ~ m2(A)
| ~ n2(J)
| m3(J,A,A) ) ),
inference(miniscoping,[status(thm)],[f266]) ).
fof(f763,plain,
! [X0,X1,X2] :
( ~ m3(X2,X0,X2)
| ~ m2(X1)
| ~ n2(X0)
| m3(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f762]) ).
fof(f765,plain,
( ~ q2(b,c,d)
| ~ m2(d)
| ~ l1(d,b)
| m3(c,b,d) ),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f766,plain,
! [I] :
( ~ k2(c,I)
| ! [H] :
( ~ r2(H)
| m3(H,I,H) ) ),
inference(miniscoping,[status(thm)],[f269]) ).
fof(f767,plain,
! [X0,X1] :
( ~ k2(c,X1)
| ~ r2(X0)
| m3(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f766]) ).
fof(f771,plain,
! [X0] :
( ~ p2(X0,e,e)
| ~ n2(e)
| m3(X0,e,e) ),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f772,plain,
! [X0,X1] :
( ~ k3(X0,X1,X0)
| ~ r2(X1)
| m3(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f773,plain,
! [X0] :
( ~ n2(X0)
| m3(X0,X0,X0) ),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f774,plain,
! [X0] :
( ~ q2(X0,c,c)
| ~ s2(c)
| m3(X0,c,X0) ),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f777,plain,
! [D] :
( ! [E,F] : ~ p2(E,F,D)
| n3(D) ),
inference(miniscoping,[status(thm)],[f278]) ).
fof(f778,plain,
! [X0,X1,X2] :
( ~ p2(X1,X2,X0)
| n3(X0) ),
inference(cnf_transformation,[status(thm)],[f777]) ).
fof(f779,plain,
! [D,E] :
( ~ k2(D,E)
| ! [C] :
( ! [F] : ~ q2(F,d,C)
| p3(C,D,E) ) ),
inference(miniscoping,[status(thm)],[f279]) ).
fof(f780,plain,
! [X0,X1,X2,X3] :
( ~ k2(X1,X2)
| ~ q2(X3,d,X0)
| p3(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f779]) ).
fof(f781,plain,
! [X0,X1,X2] :
( ~ k3(X1,X2,X0)
| ~ r2(X1)
| p3(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f782,plain,
! [X0] :
( ~ q2(X0,d,X0)
| ~ n3(X0)
| ~ p2(d,b,c)
| ~ l3(b,e)
| p3(X0,d,e) ),
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f783,plain,
! [X0] :
( ~ n2(X0)
| p3(X0,X0,X0) ),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f794,plain,
! [A,B,D] :
( ~ p2(A,B,D)
| ! [C] : ~ m3(B,C,D)
| p3(A,B,B) ),
inference(miniscoping,[status(thm)],[f289]) ).
fof(f795,plain,
! [X0,X1,X2,X3] :
( ~ p2(X0,X1,X3)
| ~ m3(X1,X2,X3)
| p3(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f794]) ).
fof(f798,plain,
( ~ k2(c,b)
| p3(b,c,b) ),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f799,plain,
! [X0] :
( ~ q2(X0,X0,b)
| ~ m3(e,X0,e)
| p3(e,b,e) ),
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f800,plain,
! [G,I] :
( ~ n0(I,G)
| ! [H] :
( ~ q2(I,G,H)
| q3(G,H) ) ),
inference(miniscoping,[status(thm)],[f293]) ).
fof(f801,plain,
! [X0,X1,X2] :
( ~ n0(X2,X0)
| ~ q2(X2,X0,X1)
| q3(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f800]) ).
fof(f802,plain,
! [X0,X1] :
( ~ q3(X1,X0)
| ~ p2(X1,X0,X0)
| q3(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f803,plain,
! [B,C] :
( ~ q3(C,B)
| ~ s2(B)
| ! [D] : ~ n1(D,B,C)
| q3(B,C) ),
inference(miniscoping,[status(thm)],[f295]) ).
fof(f804,plain,
! [X0,X1,X2] :
( ~ q3(X1,X0)
| ~ s2(X0)
| ~ n1(X2,X0,X1)
| q3(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f803]) ).
fof(f805,plain,
( ! [A] : ~ l2(A,A)
| ! [J] : ~ s1(J)
| ! [I] :
( ~ r2(I)
| q3(I,I) ) ),
inference(miniscoping,[status(thm)],[f296]) ).
fof(f806,plain,
! [X0,X1,X2] :
( ~ l2(X2,X2)
| ~ s1(X1)
| ~ r2(X0)
| q3(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f805]) ).
fof(f807,plain,
! [X0,X1] :
( ~ q3(X1,X0)
| ~ r2(d)
| ~ k1(X0)
| ~ m0(X1,d,X1)
| q3(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f808,plain,
! [G] :
( ~ l2(c,G)
| ! [H] :
( ~ s2(H)
| r3(G,H,H) ) ),
inference(miniscoping,[status(thm)],[f298]) ).
fof(f809,plain,
! [X0,X1] :
( ~ l2(c,X0)
| ~ s2(X1)
| r3(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f808]) ).
fof(f819,plain,
! [B,C] :
( ! [D] : ~ p2(B,D,C)
| r3(B,C,B) ),
inference(miniscoping,[status(thm)],[f305]) ).
fof(f820,plain,
! [X0,X1,X2] :
( ~ p2(X0,X2,X1)
| r3(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f819]) ).
fof(f821,plain,
! [I] :
( ! [A] : ~ r3(I,A,A)
| ! [H] :
( ! [J] : ~ m3(J,b,H)
| ~ m2(I)
| r3(H,H,I) ) ),
inference(miniscoping,[status(thm)],[f306]) ).
fof(f822,plain,
! [X0,X1,X2,X3] :
( ~ r3(X1,X3,X3)
| ~ m3(X2,b,X0)
| ~ m2(X1)
| r3(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f821]) ).
fof(f823,plain,
! [X0] :
( ~ m3(a,X0,X0)
| ~ m2(b)
| ~ q2(X0,e,X0)
| ~ k2(a,a)
| r3(a,a,e) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f827,plain,
! [J,B] :
( ~ r3(B,J,J)
| ~ r2(B)
| ! [A] :
( ~ k2(A,B)
| r3(J,A,B) ) ),
inference(miniscoping,[status(thm)],[f310]) ).
fof(f828,plain,
! [X0,X1,X2] :
( ~ r3(X2,X0,X0)
| ~ r2(X2)
| ~ k2(X1,X2)
| r3(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f827]) ).
fof(f829,plain,
! [J,A] :
( ! [B] : ~ m0(A,B,J)
| ! [I] :
( ~ s2(I)
| ~ q2(A,I,A)
| s3(I,J) ) ),
inference(miniscoping,[status(thm)],[f311]) ).
fof(f830,plain,
! [X0,X1,X2,X3] :
( ~ m0(X2,X3,X1)
| ~ s2(X0)
| ~ q2(X2,X0,X2)
| s3(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f829]) ).
fof(f831,plain,
( ~ n3(e)
| ~ q3(e,b)
| ~ n0(c,d)
| k4(c) ),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f834,plain,
! [X0,X1] :
( ~ r3(X0,e,X1)
| ~ q1(a,a,X1)
| ~ q3(X0,X0)
| k4(e) ),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f835,plain,
! [J] :
( ! [A,B] : ~ p3(A,B,J)
| l4(J) ),
inference(miniscoping,[status(thm)],[f315]) ).
fof(f836,plain,
! [X0,X1,X2] :
( ~ p3(X1,X2,X0)
| l4(X0) ),
inference(cnf_transformation,[status(thm)],[f835]) ).
fof(f839,plain,
! [E] :
( ~ s3(a,E)
| ! [F] :
( ! [G] : ~ l2(G,F)
| m4(E,F) ) ),
inference(miniscoping,[status(thm)],[f317]) ).
fof(f840,plain,
! [X0,X1,X2] :
( ~ s3(a,X0)
| ~ l2(X2,X1)
| m4(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f839]) ).
fof(f843,plain,
! [J] :
( ~ n4(J,J)
| ! [A] :
( ~ p3(J,A,A)
| n4(J,A) ) ),
inference(miniscoping,[status(thm)],[f319]) ).
fof(f844,plain,
! [X0,X1] :
( ~ n4(X0,X0)
| ~ p3(X0,X1,X1)
| n4(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f843]) ).
fof(f847,plain,
! [H] :
( ~ m3(H,H,H)
| ! [I] : ~ k4(I)
| n4(H,H) ),
inference(miniscoping,[status(thm)],[f322]) ).
fof(f848,plain,
! [X0,X1] :
( ~ m3(X0,X0,X0)
| ~ k4(X1)
| n4(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f847]) ).
fof(f849,plain,
! [X0,X1] :
( ~ r3(X1,X0,X1)
| ~ r0(X0)
| p4(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f852,plain,
! [X0,X1] :
( ~ k3(X0,X0,X1)
| p4(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f853,plain,
( ! [J,A] : ~ p4(J,J,A)
| ! [H,I] :
( ~ r3(I,I,H)
| p4(H,I,I) ) ),
inference(miniscoping,[status(thm)],[f326]) ).
fof(f854,plain,
! [X0,X1,X2,X3] :
( ~ p4(X2,X2,X3)
| ~ r3(X1,X1,X0)
| p4(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f853]) ).
fof(f864,plain,
! [X0] :
( ~ m3(X0,c,a)
| ~ n3(a)
| p4(c,c,X0) ),
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f865,plain,
! [E] :
( ! [F] : ~ m3(E,F,E)
| ! [B,C] :
( ~ q2(E,C,B)
| ! [D] : ~ k3(D,D,B)
| q4(B,C) ) ),
inference(miniscoping,[status(thm)],[f333]) ).
fof(f866,plain,
! [X0,X1,X2,X3,X4] :
( ~ m3(X3,X4,X3)
| ~ q2(X3,X1,X0)
| ~ k3(X2,X2,X0)
| q4(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f865]) ).
fof(f867,plain,
! [J] :
( ! [A] : ~ q4(J,A)
| ~ l4(J)
| ! [I] :
( ~ r1(I)
| q4(I,I) ) ),
inference(miniscoping,[status(thm)],[f334]) ).
fof(f868,plain,
! [X0,X1,X2] :
( ~ q4(X1,X2)
| ~ l4(X1)
| ~ r1(X0)
| q4(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f867]) ).
fof(f870,plain,
! [G] :
( ! [J] : ~ p0(J,G)
| ! [H,I] : ~ q3(H,I)
| ~ n3(G)
| r4(G) ),
inference(miniscoping,[status(thm)],[f336]) ).
fof(f871,plain,
! [X0,X1,X2,X3] :
( ~ p0(X3,X0)
| ~ q3(X1,X2)
| ~ n3(X0)
| r4(X0) ),
inference(cnf_transformation,[status(thm)],[f870]) ).
fof(f872,plain,
! [A,C] :
( ~ l1(A,C)
| ! [B,D] : ~ p3(B,C,D)
| s4(A) ),
inference(miniscoping,[status(thm)],[f337]) ).
fof(f873,plain,
! [X0,X1,X2,X3] :
( ~ l1(X0,X2)
| ~ p3(X1,X2,X3)
| s4(X0) ),
inference(cnf_transformation,[status(thm)],[f872]) ).
fof(f874,plain,
! [E] :
( ! [G] : ~ r3(G,E,E)
| ! [F] : ~ s4(F)
| k5(E) ),
inference(miniscoping,[status(thm)],[f338]) ).
fof(f875,plain,
! [X0,X1,X2] :
( ~ r3(X2,X0,X0)
| ~ s4(X1)
| k5(X0) ),
inference(cnf_transformation,[status(thm)],[f874]) ).
fof(f877,plain,
! [H] :
( ~ k1(H)
| ! [I] : ~ q4(I,I)
| l5(H) ),
inference(miniscoping,[status(thm)],[f340]) ).
fof(f878,plain,
! [X0,X1] :
( ~ k1(X0)
| ~ q4(X1,X1)
| l5(X0) ),
inference(cnf_transformation,[status(thm)],[f877]) ).
fof(f879,plain,
! [D,E] :
( ! [F] : ~ p4(D,F,E)
| ~ r0(D)
| m5(D,E) ),
inference(miniscoping,[status(thm)],[f341]) ).
fof(f880,plain,
! [X0,X1,X2] :
( ~ p4(X0,X2,X1)
| ~ r0(X0)
| m5(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f879]) ).
fof(f881,plain,
! [X0] :
( ~ k4(X0)
| m5(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f882,plain,
( ~ m4(e,e)
| ! [B] :
( ~ s4(B)
| m5(B,B) ) ),
inference(miniscoping,[status(thm)],[f343]) ).
fof(f883,plain,
! [X0] :
( ~ m4(e,e)
| ~ s4(X0)
| m5(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f882]) ).
fof(f884,plain,
! [J] :
( ~ r0(J)
| ! [A] : ~ s4(A)
| m5(J,J) ),
inference(miniscoping,[status(thm)],[f344]) ).
fof(f885,plain,
! [X0,X1] :
( ~ r0(X0)
| ~ s4(X1)
| m5(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f884]) ).
fof(f886,plain,
! [C,F] :
( ~ n5(F,C)
| ~ p4(F,F,C)
| ! [B,E] :
( ~ n4(B,E)
| ! [D] : ~ q4(D,E)
| n5(B,C) ) ),
inference(miniscoping,[status(thm)],[f345]) ).
fof(f887,plain,
! [X0,X1,X2,X3,X4] :
( ~ n5(X4,X1)
| ~ p4(X4,X4,X1)
| ~ n4(X0,X3)
| ~ q4(X2,X3)
| n5(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f886]) ).
fof(f897,plain,
! [X0] :
( ~ r4(X0)
| n5(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f352]) ).
fof(f902,plain,
! [E] :
( ~ l2(E,E)
| ! [F] :
( ~ s4(F)
| p5(E,E,F) ) ),
inference(miniscoping,[status(thm)],[f356]) ).
fof(f903,plain,
! [X0,X1] :
( ~ l2(X0,X0)
| ~ s4(X1)
| p5(X0,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f902]) ).
fof(f904,plain,
! [C,D] :
( ~ m4(D,C)
| ! [B] :
( ~ p5(B,D,B)
| ~ l2(B,D)
| p5(B,C,C) ) ),
inference(miniscoping,[status(thm)],[f357]) ).
fof(f905,plain,
! [X0,X1,X2] :
( ~ m4(X2,X1)
| ~ p5(X0,X2,X0)
| ~ l2(X0,X2)
| p5(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f904]) ).
fof(f906,plain,
! [I] :
( ~ s1(I)
| ! [J] :
( ! [A] : ~ q4(J,A)
| p5(I,J,I) ) ),
inference(miniscoping,[status(thm)],[f358]) ).
fof(f907,plain,
! [X0,X1,X2] :
( ~ s1(X0)
| ~ q4(X1,X2)
| p5(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f906]) ).
fof(f910,plain,
! [A] :
( ~ m2(A)
| ! [J] :
( ~ s4(J)
| q5(J,A) ) ),
inference(miniscoping,[status(thm)],[f360]) ).
fof(f911,plain,
! [X0,X1] :
( ~ m2(X1)
| ~ s4(X0)
| q5(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f910]) ).
fof(f913,plain,
! [X0] :
( ~ l4(X0)
| q5(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f916,plain,
! [D] :
( ~ n3(D)
| ~ k0(b)
| ! [C] :
( ~ s4(C)
| r5(C,D) ) ),
inference(miniscoping,[status(thm)],[f365]) ).
fof(f917,plain,
! [X0,X1] :
( ~ n3(X1)
| ~ k0(b)
| ~ s4(X0)
| r5(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f916]) ).
fof(f918,plain,
! [X0] :
( ~ k4(X0)
| r5(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f919,plain,
( ! [I] : ~ r4(I)
| ! [H] :
( ~ l4(H)
| s5(H) ) ),
inference(miniscoping,[status(thm)],[f367]) ).
fof(f920,plain,
! [X0,X1] :
( ~ r4(X1)
| ~ l4(X0)
| s5(X0) ),
inference(cnf_transformation,[status(thm)],[f919]) ).
fof(f923,plain,
k1(a),
inference(resolution,[status(thm)],[f408,f405]) ).
fof(f924,plain,
k1(d),
inference(resolution,[status(thm)],[f408,f402]) ).
fof(f925,plain,
k1(b),
inference(resolution,[status(thm)],[f408,f383]) ).
fof(f926,plain,
k1(e),
inference(resolution,[status(thm)],[f408,f398]) ).
fof(f928,plain,
k1(c),
inference(resolution,[status(thm)],[f408,f394]) ).
fof(f931,plain,
l1(a,a),
inference(resolution,[status(thm)],[f410,f405]) ).
fof(f932,plain,
l1(d,d),
inference(resolution,[status(thm)],[f410,f402]) ).
fof(f933,plain,
l1(b,b),
inference(resolution,[status(thm)],[f410,f383]) ).
fof(f934,plain,
l1(e,e),
inference(resolution,[status(thm)],[f410,f398]) ).
fof(f936,plain,
l1(c,c),
inference(resolution,[status(thm)],[f410,f394]) ).
fof(f939,plain,
! [X0,X1,X2] :
( ~ m0(X1,X0,X2)
| ~ p0(X2,X0)
| l1(X0,X1) ),
inference(resolution,[status(thm)],[f412,f381]) ).
fof(f945,plain,
! [X0] : m1(X0,d,X0),
inference(resolution,[status(thm)],[f415,f387]) ).
fof(f949,plain,
! [X0] : m1(X0,X0,X0),
inference(resolution,[status(thm)],[f417,f387]) ).
fof(f950,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| m1(e,X0,e) ),
inference(resolution,[status(thm)],[f419,f381]) ).
fof(f956,plain,
! [X0] :
( ~ n0(X0,X0)
| m1(b,b,X0) ),
inference(resolution,[status(thm)],[f425,f400]) ).
fof(f957,plain,
! [X0] :
( ~ n0(X0,X0)
| m1(e,e,X0) ),
inference(resolution,[status(thm)],[f425,f396]) ).
fof(f974,plain,
! [X0,X1] :
( ~ m0(X1,X1,X0)
| m1(X0,X1,X1) ),
inference(resolution,[status(thm)],[f432,f392]) ).
fof(f983,plain,
! [X0,X1] :
( ~ m1(X1,X1,X0)
| m1(X0,X1,X1) ),
inference(resolution,[status(thm)],[f949,f434]) ).
fof(f986,plain,
! [X0,X1] :
( ~ p0(X0,X1)
| ~ q0(X1,d)
| ~ r0(c)
| m1(X0,X1,c) ),
inference(forward_subsumption_resolution,[status(thm)],[f439,f369]) ).
fof(f987,plain,
! [X0] :
( ~ l0(X0)
| m1(X0,b,X0) ),
inference(resolution,[status(thm)],[f442,f400]) ).
fof(f988,plain,
! [X0] :
( ~ l0(X0)
| m1(X0,e,X0) ),
inference(resolution,[status(thm)],[f442,f396]) ).
fof(f989,plain,
! [X0,X1] :
( ~ m1(X1,c,X1)
| ~ q0(X0,X1)
| m1(X0,a,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f446,f380]) ).
fof(f990,plain,
! [X0] :
( ~ q0(X0,c)
| m1(X0,a,c) ),
inference(resolution,[status(thm)],[f989,f949]) ).
fof(f991,plain,
! [X0] :
( ~ p0(b,X0)
| m1(b,X0,b) ),
inference(resolution,[status(thm)],[f454,f373]) ).
fof(f992,plain,
! [X0] :
( ~ p0(d,X0)
| m1(d,X0,d) ),
inference(resolution,[status(thm)],[f454,f369]) ).
fof(f993,plain,
! [X0] : m1(b,X0,b),
inference(forward_subsumption_resolution,[status(thm)],[f991,f382]) ).
fof(f994,plain,
! [X0] :
( ~ k0(e)
| ~ r0(X0)
| ~ m0(a,e,c)
| m1(c,a,c) ),
inference(forward_subsumption_resolution,[status(thm)],[f457,f381]) ).
fof(f995,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| ~ n0(X1,X1)
| m1(X0,X0,c) ),
inference(backward_subsumption_resolution,[status(thm)],[f423,f936]) ).
fof(f996,plain,
! [X0,X1] :
( ~ q0(X0,X0)
| ~ k1(X1)
| m1(X0,X1,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f462,f923]) ).
fof(f997,plain,
! [X0] :
( ~ q0(X0,X0)
| m1(X0,c,c) ),
inference(resolution,[status(thm)],[f996,f928]) ).
fof(f998,plain,
! [X0] :
( ~ q0(X0,X0)
| m1(X0,e,e) ),
inference(resolution,[status(thm)],[f996,f926]) ).
fof(f999,plain,
! [X0] :
( ~ q0(X0,X0)
| m1(X0,b,b) ),
inference(resolution,[status(thm)],[f996,f925]) ).
fof(f1001,plain,
! [X0] :
( ~ q0(X0,X0)
| m1(X0,a,a) ),
inference(resolution,[status(thm)],[f996,f923]) ).
fof(f1002,plain,
! [X0] :
( ~ r0(X0)
| m1(X0,c,X0) ),
inference(resolution,[status(thm)],[f464,f392]) ).
fof(f1003,plain,
! [X0] :
( ~ r0(X0)
| m1(X0,a,X0) ),
inference(resolution,[status(thm)],[f464,f388]) ).
fof(f1006,plain,
! [X0] : n1(X0,X0,d),
inference(resolution,[status(thm)],[f465,f387]) ).
fof(f1007,plain,
! [X0,X1] :
( ~ r0(X0)
| ~ p0(X1,X0)
| n1(X0,c,X0) ),
inference(resolution,[status(thm)],[f467,f392]) ).
fof(f1008,plain,
! [X0,X1] :
( ~ r0(X0)
| ~ p0(X1,X0)
| n1(X0,a,X0) ),
inference(resolution,[status(thm)],[f467,f388]) ).
fof(f1015,plain,
n1(e,c,e),
inference(resolution,[status(thm)],[f470,f403]) ).
fof(f1016,plain,
n1(b,c,b),
inference(resolution,[status(thm)],[f470,f395]) ).
fof(f1017,plain,
n1(d,c,d),
inference(resolution,[status(thm)],[f470,f387]) ).
fof(f1018,plain,
( ~ k1(b)
| n1(b,e,e) ),
inference(resolution,[status(thm)],[f472,f399]) ).
fof(f1020,plain,
! [X0] :
( ~ k1(X0)
| n1(X0,e,e) ),
inference(resolution,[status(thm)],[f472,f387]) ).
fof(f1021,plain,
n1(b,e,e),
inference(forward_subsumption_resolution,[status(thm)],[f1018,f925]) ).
fof(f1024,plain,
s1(b),
inference(resolution,[status(thm)],[f606,f382]) ).
fof(f1033,plain,
! [X0] :
( ~ p0(X0,X0)
| n1(X0,c,X0) ),
inference(resolution,[status(thm)],[f478,f386]) ).
fof(f1034,plain,
! [X0] :
( ~ p0(X0,X0)
| n1(X0,b,X0) ),
inference(resolution,[status(thm)],[f478,f382]) ).
fof(f1037,plain,
! [X0] :
( ~ r0(X0)
| ~ p0(d,d)
| n1(X0,d,d) ),
inference(resolution,[status(thm)],[f483,f932]) ).
fof(f1039,plain,
! [X0,X1] :
( ~ p0(b,X1)
| ~ l0(X0)
| n1(X0,X1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f488,f373]) ).
fof(f1040,plain,
! [X0,X1] :
( ~ l0(X0)
| n1(X0,X1,X0) ),
inference(resolution,[status(thm)],[f1039,f382]) ).
fof(f1048,plain,
! [X0,X1] :
( ~ n1(X0,X1,X0)
| ~ l1(c,X0)
| n1(X0,X1,X1) ),
inference(resolution,[status(thm)],[f495,f392]) ).
fof(f1049,plain,
! [X0,X1] :
( ~ n1(X0,X1,X0)
| ~ l1(a,X0)
| n1(X0,X1,X1) ),
inference(resolution,[status(thm)],[f495,f388]) ).
fof(f1052,plain,
! [X0] :
( ~ q0(X0,b)
| m1(X0,a,b) ),
inference(resolution,[status(thm)],[f993,f989]) ).
fof(f1056,plain,
! [X0,X1] :
( ~ m1(b,X1,X0)
| m1(b,X0,X0) ),
inference(resolution,[status(thm)],[f993,f434]) ).
fof(f1073,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| n1(X0,X0,X1) ),
inference(resolution,[status(thm)],[f501,f387]) ).
fof(f1082,plain,
! [X0] :
( ~ k0(X0)
| p1(c,c,X0) ),
inference(resolution,[status(thm)],[f507,f394]) ).
fof(f1083,plain,
! [X0] :
( ~ k0(X0)
| p1(b,b,X0) ),
inference(resolution,[status(thm)],[f507,f375]) ).
fof(f1084,plain,
! [X0] :
( ~ k0(X0)
| p1(e,e,X0) ),
inference(resolution,[status(thm)],[f507,f371]) ).
fof(f1099,plain,
m2(b),
inference(forward_subsumption_resolution,[status(thm)],[f624,f925]) ).
fof(f1106,plain,
p1(b,b,c),
inference(resolution,[status(thm)],[f517,f386]) ).
fof(f1107,plain,
! [X0] : p1(X0,X0,b),
inference(resolution,[status(thm)],[f517,f382]) ).
fof(f1108,plain,
! [X0,X1,X2,X3] :
( ~ p1(X1,X3,X0)
| ~ l0(X2)
| p1(X0,X1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f520,f373]) ).
fof(f1109,plain,
! [X0,X1,X2] :
( ~ p1(X1,X2,X0)
| p1(X0,X1,X0) ),
inference(resolution,[status(thm)],[f1108,f392]) ).
fof(f1114,plain,
p1(a,a,a),
inference(forward_subsumption_resolution,[status(thm)],[f527,f382]) ).
fof(f1129,plain,
! [X0] :
( ~ m0(a,a,a)
| p1(a,X0,a) ),
inference(resolution,[status(thm)],[f538,f1114]) ).
fof(f1130,plain,
! [X0,X1] :
( ~ m0(X0,X0,b)
| p1(X0,X1,X0) ),
inference(resolution,[status(thm)],[f538,f1107]) ).
fof(f1131,plain,
! [X0] : p1(a,X0,a),
inference(forward_subsumption_resolution,[status(thm)],[f1129,f380]) ).
fof(f1132,plain,
! [X0,X1] :
( ~ m0(a,X0,a)
| p1(X0,X1,a) ),
inference(resolution,[status(thm)],[f1131,f538]) ).
fof(f1134,plain,
! [X0,X1] : p1(X0,X1,a),
inference(forward_subsumption_resolution,[status(thm)],[f1132,f380]) ).
fof(f1135,plain,
! [X0] :
( ~ m1(X0,b,b)
| p1(X0,b,b) ),
inference(resolution,[status(thm)],[f540,f400]) ).
fof(f1136,plain,
! [X0] :
( ~ m1(X0,e,b)
| p1(X0,b,e) ),
inference(resolution,[status(thm)],[f540,f396]) ).
fof(f1138,plain,
! [X0,X1,X2] :
( ~ m0(X2,X0,a)
| p1(X0,X1,X2) ),
inference(resolution,[status(thm)],[f1134,f538]) ).
fof(f1141,plain,
! [X0] : p1(X0,X0,X0),
inference(resolution,[status(thm)],[f544,f382]) ).
fof(f1144,plain,
! [X0,X1] :
( ~ m0(X0,X0,X0)
| p1(X0,X1,X0) ),
inference(resolution,[status(thm)],[f1141,f538]) ).
fof(f1145,plain,
! [X0] : n2(X0),
inference(resolution,[status(thm)],[f1141,f626]) ).
fof(f1146,plain,
! [X0] : k3(X0,X0,X0),
inference(backward_subsumption_resolution,[status(thm)],[f734,f1145]) ).
fof(f1147,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| q1(X0,a,X0) ),
inference(resolution,[status(thm)],[f554,f405]) ).
fof(f1148,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| q1(X0,d,X0) ),
inference(resolution,[status(thm)],[f554,f402]) ).
fof(f1149,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| q1(X0,b,X0) ),
inference(resolution,[status(thm)],[f554,f383]) ).
fof(f1150,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| q1(X0,e,X0) ),
inference(resolution,[status(thm)],[f554,f398]) ).
fof(f1152,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| q1(X0,c,X0) ),
inference(resolution,[status(thm)],[f554,f394]) ).
fof(f1161,plain,
( ~ l0(c)
| ~ s0(e)
| q1(b,e,e) ),
inference(forward_subsumption_resolution,[status(thm)],[f557,f400]) ).
fof(f1162,plain,
( ~ s0(e)
| q1(b,e,e) ),
inference(resolution,[status(thm)],[f1161,f392]) ).
fof(f1163,plain,
! [X0] : m3(X0,X0,X0),
inference(forward_subsumption_resolution,[status(thm)],[f773,f1145]) ).
fof(f1164,plain,
q1(b,c,c),
inference(resolution,[status(thm)],[f558,f386]) ).
fof(f1165,plain,
! [X0] : q1(X0,b,b),
inference(resolution,[status(thm)],[f558,f382]) ).
fof(f1168,plain,
! [X0,X1] :
( ~ q1(X1,X1,b)
| ~ l0(X0)
| q1(X0,X1,X1) ),
inference(resolution,[status(thm)],[f565,f400]) ).
fof(f1169,plain,
! [X0,X1] :
( ~ q1(X1,X1,e)
| ~ l0(X0)
| q1(X0,X1,X1) ),
inference(resolution,[status(thm)],[f565,f396]) ).
fof(f1182,plain,
! [X0] : p3(X0,X0,X0),
inference(forward_subsumption_resolution,[status(thm)],[f783,f1145]) ).
fof(f1185,plain,
! [X0,X1,X2] :
( ~ q0(X0,X0)
| ~ p0(X2,c)
| ~ r0(X1)
| q1(c,X0,c) ),
inference(resolution,[status(thm)],[f573,f392]) ).
fof(f1186,plain,
! [X0,X1,X2] :
( ~ q0(X0,X0)
| ~ p0(X2,a)
| ~ r0(X1)
| q1(a,X0,a) ),
inference(resolution,[status(thm)],[f573,f388]) ).
fof(f1187,plain,
! [X0] :
( ~ s0(X0)
| q1(X0,X0,b) ),
inference(resolution,[status(thm)],[f575,f382]) ).
fof(f1188,plain,
! [X0] :
( ~ m0(e,d,X0)
| q1(e,X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f577,f387]) ).
fof(f1189,plain,
! [X0] : q1(e,X0,X0),
inference(resolution,[status(thm)],[f1188,f387]) ).
fof(f1193,plain,
! [X0,X1] :
( ~ q0(X0,c)
| ~ p0(X1,X1)
| q1(c,c,X0) ),
inference(resolution,[status(thm)],[f581,f928]) ).
fof(f1194,plain,
! [X0,X1] :
( ~ q0(X0,e)
| ~ p0(X1,X1)
| q1(e,e,X0) ),
inference(resolution,[status(thm)],[f581,f926]) ).
fof(f1195,plain,
! [X0,X1] :
( ~ q0(X0,b)
| ~ p0(X1,X1)
| q1(b,b,X0) ),
inference(resolution,[status(thm)],[f581,f925]) ).
fof(f1196,plain,
! [X0,X1] :
( ~ q0(X0,d)
| ~ p0(X1,X1)
| q1(d,d,X0) ),
inference(resolution,[status(thm)],[f581,f924]) ).
fof(f1197,plain,
! [X0,X1] :
( ~ q0(X0,a)
| ~ p0(X1,X1)
| q1(a,a,X0) ),
inference(resolution,[status(thm)],[f581,f923]) ).
fof(f1198,plain,
! [X0,X1] :
( ~ p0(X1,X1)
| q1(d,d,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1196,f385]) ).
fof(f1206,plain,
! [X0] : q1(X0,X0,X0),
inference(resolution,[status(thm)],[f583,f387]) ).
fof(f1208,plain,
! [X0] : l4(X0),
inference(resolution,[status(thm)],[f836,f1182]) ).
fof(f1209,plain,
! [X0,X1] :
( ~ m1(X0,X1,X1)
| q1(X0,X0,X1) ),
inference(resolution,[status(thm)],[f588,f381]) ).
fof(f1211,plain,
! [X0] : q5(X0,X0),
inference(backward_subsumption_resolution,[status(thm)],[f913,f1208]) ).
fof(f1212,plain,
! [X0,X1] :
( ~ q1(d,X1,d)
| ~ q0(X0,X1)
| r1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f605,f369]) ).
fof(f1213,plain,
! [X0] :
( ~ q0(X0,d)
| r1(X0) ),
inference(resolution,[status(thm)],[f1212,f1206]) ).
fof(f1214,plain,
! [X0] : r1(X0),
inference(forward_subsumption_resolution,[status(thm)],[f1213,f385]) ).
fof(f1215,plain,
! [X0,X1] :
( ~ q0(X0,X1)
| s1(X0) ),
inference(resolution,[status(thm)],[f608,f1024]) ).
fof(f1216,plain,
! [X0,X1,X2] :
( ~ k2(c,X1)
| ~ m1(X2,X1,X0)
| k2(X0,X1) ),
inference(resolution,[status(thm)],[f610,f928]) ).
fof(f1217,plain,
! [X0,X1,X2] :
( ~ k2(e,X1)
| ~ m1(X2,X1,X0)
| k2(X0,X1) ),
inference(resolution,[status(thm)],[f610,f926]) ).
fof(f1218,plain,
! [X0,X1,X2] :
( ~ k2(b,X1)
| ~ m1(X2,X1,X0)
| k2(X0,X1) ),
inference(resolution,[status(thm)],[f610,f925]) ).
fof(f1219,plain,
! [X0,X1,X2] :
( ~ k2(d,X1)
| ~ m1(X2,X1,X0)
| k2(X0,X1) ),
inference(resolution,[status(thm)],[f610,f924]) ).
fof(f1220,plain,
! [X0,X1,X2] :
( ~ k2(a,X1)
| ~ m1(X2,X1,X0)
| k2(X0,X1) ),
inference(resolution,[status(thm)],[f610,f923]) ).
fof(f1226,plain,
! [X0] : s1(X0),
inference(resolution,[status(thm)],[f1215,f385]) ).
fof(f1227,plain,
! [X0] : k2(X0,X0),
inference(resolution,[status(thm)],[f613,f1189]) ).
fof(f1231,plain,
! [X0,X1] :
( ~ l2(X1,X1)
| ~ n0(e,X1)
| l2(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f616,f1226]) ).
fof(f1232,plain,
! [X0] :
( ~ l2(e,e)
| l2(X0,e) ),
inference(resolution,[status(thm)],[f1231,f398]) ).
fof(f1233,plain,
! [X0] :
( ~ l2(b,b)
| l2(X0,b) ),
inference(resolution,[status(thm)],[f1231,f379]) ).
fof(f1234,plain,
! [X0,X1,X2,X3] :
( ~ m0(X2,X3,X0)
| ~ p0(X1,X1)
| l2(X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f619,f1226]) ).
fof(f1235,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| l2(X0,X0) ),
inference(resolution,[status(thm)],[f1234,f382]) ).
fof(f1241,plain,
! [X0,X1] :
( ~ l1(X0,X1)
| m2(d) ),
inference(resolution,[status(thm)],[f623,f369]) ).
fof(f1245,plain,
! [X0] :
( ~ k2(c,a)
| ~ p0(b,X0)
| ~ n1(c,X0,X0)
| p2(b,c,a) ),
inference(forward_subsumption_resolution,[status(thm)],[f636,f381]) ).
fof(f1248,plain,
! [X0,X1] :
( ~ p1(X0,X1,e)
| p2(e,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f637,f381]) ).
fof(f1253,plain,
! [X0,X1] :
( ~ p2(X0,X1,X0)
| ~ p1(X0,d,d)
| p2(X0,X1,X1) ),
inference(resolution,[status(thm)],[f639,f932]) ).
fof(f1254,plain,
! [X0,X1] :
( ~ p2(X0,X1,X0)
| ~ p1(X0,a,a)
| p2(X0,X1,X1) ),
inference(resolution,[status(thm)],[f639,f931]) ).
fof(f1255,plain,
! [X0,X1] :
( ~ p2(X0,X1,X0)
| p2(X0,X1,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1254,f1134]) ).
fof(f1260,plain,
! [X0,X1] :
( ~ m0(X1,X0,d)
| p2(X0,X0,d) ),
inference(forward_subsumption_resolution,[status(thm)],[f644,f1214]) ).
fof(f1267,plain,
! [X0] : p2(X0,X0,X0),
inference(resolution,[status(thm)],[f646,f949]) ).
fof(f1268,plain,
! [X0] : n3(X0),
inference(resolution,[status(thm)],[f1267,f778]) ).
fof(f1271,plain,
! [X0,X1] :
( ~ p2(e,X0,X1)
| p2(X0,X1,X1) ),
inference(resolution,[status(thm)],[f653,f928]) ).
fof(f1276,plain,
! [X0,X1,X2] :
( ~ p2(X0,X2,X0)
| ~ s0(e)
| ~ q1(c,X0,X2)
| p2(X0,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f1226]) ).
fof(f1278,plain,
( ~ m1(d,a,c)
| ~ l2(e,b)
| ~ l1(e,c)
| p2(a,c,b) ),
inference(forward_subsumption_resolution,[status(thm)],[f671,f1214]) ).
fof(f1280,plain,
! [X0] : p2(X0,b,X0),
inference(resolution,[status(thm)],[f684,f993]) ).
fof(f1281,plain,
! [X0] : p2(d,X0,d),
inference(resolution,[status(thm)],[f684,f945]) ).
fof(f1283,plain,
! [X0,X1] :
( ~ k0(X1)
| q2(X0,X1,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f686,f1141]) ).
fof(f1284,plain,
! [X0] : q2(X0,b,b),
inference(resolution,[status(thm)],[f1283,f400]) ).
fof(f1285,plain,
! [X0] : q2(X0,e,e),
inference(resolution,[status(thm)],[f1283,f396]) ).
fof(f1295,plain,
! [X0] :
( ~ n1(X0,X0,d)
| q2(X0,X0,X0) ),
inference(resolution,[status(thm)],[f689,f924]) ).
fof(f1297,plain,
! [X0] : q2(X0,X0,X0),
inference(forward_subsumption_resolution,[status(thm)],[f1295,f1006]) ).
fof(f1298,plain,
( ~ q0(e,c)
| ~ q2(d,c,a)
| q2(d,a,a) ),
inference(forward_subsumption_resolution,[status(thm)],[f690,f1226]) ).
fof(f1300,plain,
! [X0] :
( ~ n1(X0,b,b)
| ~ p1(b,b,b)
| q2(b,X0,b) ),
inference(resolution,[status(thm)],[f1284,f692]) ).
fof(f1301,plain,
! [X0] :
( ~ n1(X0,b,b)
| q2(b,X0,b) ),
inference(forward_subsumption_resolution,[status(thm)],[f1300,f1107]) ).
fof(f1302,plain,
! [X0,X1] :
( ~ l2(X1,X0)
| ~ k1(X1)
| q2(X0,c,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f693,f392]) ).
fof(f1303,plain,
! [X0] :
( ~ l2(c,X0)
| q2(X0,c,c) ),
inference(resolution,[status(thm)],[f1302,f928]) ).
fof(f1304,plain,
! [X0] :
( ~ l2(e,X0)
| q2(X0,c,e) ),
inference(resolution,[status(thm)],[f1302,f926]) ).
fof(f1305,plain,
! [X0] :
( ~ l2(b,X0)
| q2(X0,c,b) ),
inference(resolution,[status(thm)],[f1302,f925]) ).
fof(f1306,plain,
! [X0] :
( ~ l2(d,X0)
| q2(X0,c,d) ),
inference(resolution,[status(thm)],[f1302,f924]) ).
fof(f1307,plain,
! [X0] :
( ~ l2(a,X0)
| q2(X0,c,a) ),
inference(resolution,[status(thm)],[f1302,f923]) ).
fof(f1308,plain,
! [X0] :
( ~ n1(X0,e,e)
| ~ p1(e,e,e)
| q2(e,X0,e) ),
inference(resolution,[status(thm)],[f1285,f692]) ).
fof(f1309,plain,
! [X0] :
( ~ n1(X0,e,e)
| q2(e,X0,e) ),
inference(forward_subsumption_resolution,[status(thm)],[f1308,f1141]) ).
fof(f1315,plain,
! [X0,X1,X2,X3] :
( ~ q2(X1,X1,X1)
| ~ k0(X1)
| ~ m0(X2,X3,X0)
| q2(X0,X1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f700,f1214]) ).
fof(f1316,plain,
! [X0,X1,X2] :
( ~ q2(b,b,b)
| ~ m0(X1,X2,X0)
| q2(X0,b,X0) ),
inference(resolution,[status(thm)],[f1315,f400]) ).
fof(f1317,plain,
! [X0,X1,X2] :
( ~ q2(e,e,e)
| ~ m0(X1,X2,X0)
| q2(X0,e,X0) ),
inference(resolution,[status(thm)],[f1315,f396]) ).
fof(f1318,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| q2(X0,b,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1316,f1284]) ).
fof(f1319,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| q2(X0,e,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1317,f1285]) ).
fof(f1320,plain,
! [X0] :
( ~ l0(X0)
| r2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f701,f1214]) ).
fof(f1321,plain,
r2(c),
inference(resolution,[status(thm)],[f1320,f392]) ).
fof(f1322,plain,
r2(a),
inference(resolution,[status(thm)],[f1320,f388]) ).
fof(f1325,plain,
! [X0] :
( ~ q2(b,X0,b)
| s2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f703,f1226]) ).
fof(f1326,plain,
s2(b),
inference(resolution,[status(thm)],[f1325,f1284]) ).
fof(f1328,plain,
( ~ s0(d)
| s2(d) ),
inference(forward_subsumption_resolution,[status(thm)],[f704,f1226]) ).
fof(f1329,plain,
s2(d),
inference(resolution,[status(thm)],[f1328,f369]) ).
fof(f1334,plain,
! [X0,X1,X2,X3] :
( ~ n0(X0,X3)
| ~ p2(X2,X1,X3)
| k3(X0,X1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f707,f1226]) ).
fof(f1336,plain,
! [X0,X1] :
( ~ p2(X1,X0,d)
| k3(c,X0,c) ),
inference(resolution,[status(thm)],[f1334,f402]) ).
fof(f1340,plain,
! [X0,X1] :
( ~ p2(X1,X0,c)
| k3(d,X0,d) ),
inference(resolution,[status(thm)],[f1334,f394]) ).
fof(f1341,plain,
! [X0,X1] :
( ~ p2(X1,X0,b)
| k3(d,X0,d) ),
inference(resolution,[status(thm)],[f1334,f375]) ).
fof(f1342,plain,
! [X0,X1] :
( ~ p2(X1,X0,e)
| k3(d,X0,d) ),
inference(resolution,[status(thm)],[f1334,f371]) ).
fof(f1346,plain,
! [X0,X1,X2] :
( ~ m2(X2)
| ~ p1(X1,X2,X0)
| k3(X0,X0,X1) ),
inference(resolution,[status(thm)],[f721,f1099]) ).
fof(f1351,plain,
! [X0] :
( ~ p2(e,X0,e)
| l3(e,X0) ),
inference(resolution,[status(thm)],[f741,f381]) ).
fof(f1352,plain,
! [X0] :
( ~ p2(b,X0,b)
| l3(b,X0) ),
inference(resolution,[status(thm)],[f741,f377]) ).
fof(f1357,plain,
! [X0] :
( ~ m2(b)
| l3(X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f745,f1145]) ).
fof(f1358,plain,
! [X0] : l3(X0,X0),
inference(resolution,[status(thm)],[f1357,f1099]) ).
fof(f1363,plain,
( ~ r0(b)
| ~ k3(a,c,a)
| l3(d,c) ),
inference(forward_subsumption_resolution,[status(thm)],[f755,f1329]) ).
fof(f1364,plain,
! [X0,X1,X2] :
( ~ m0(X0,X2,X2)
| ~ l2(X2,X0)
| ~ m0(d,d,X1)
| m3(X0,X1,X0) ),
inference(resolution,[status(thm)],[f757,f1329]) ).
fof(f1366,plain,
! [X0,X1,X2] :
( ~ m0(X0,X2,X2)
| ~ l2(X2,X0)
| m3(X0,X1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1364,f387]) ).
fof(f1369,plain,
! [X0,X1,X2] :
( ~ m3(X2,X0,X2)
| ~ m2(X1)
| m3(X0,X1,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f763,f1145]) ).
fof(f1370,plain,
! [X0,X1] :
( ~ m3(X1,X0,X1)
| m3(X0,b,b) ),
inference(resolution,[status(thm)],[f1369,f1099]) ).
fof(f1372,plain,
! [X0] :
( ~ r2(X0)
| m3(X0,c,X0) ),
inference(resolution,[status(thm)],[f767,f1227]) ).
fof(f1375,plain,
! [X0] :
( ~ p2(X0,e,e)
| m3(X0,e,e) ),
inference(forward_subsumption_resolution,[status(thm)],[f771,f1145]) ).
fof(f1377,plain,
! [X0] :
( ~ k3(X0,a,X0)
| m3(X0,X0,a) ),
inference(resolution,[status(thm)],[f772,f1322]) ).
fof(f1378,plain,
! [X0] :
( ~ k3(X0,c,X0)
| m3(X0,X0,c) ),
inference(resolution,[status(thm)],[f772,f1321]) ).
fof(f1379,plain,
! [X0] : n1(c,X0,c),
inference(resolution,[status(thm)],[f1040,f392]) ).
fof(f1380,plain,
! [X0] : n1(a,X0,a),
inference(resolution,[status(thm)],[f1040,f388]) ).
fof(f1384,plain,
! [X0,X1] :
( ~ k2(X0,X1)
| p3(d,X0,X1) ),
inference(resolution,[status(thm)],[f780,f1297]) ).
fof(f1386,plain,
! [X0,X1] :
( ~ k3(a,X1,X0)
| p3(X0,a,X1) ),
inference(resolution,[status(thm)],[f781,f1322]) ).
fof(f1387,plain,
! [X0,X1] :
( ~ k3(c,X1,X0)
| p3(X0,c,X1) ),
inference(resolution,[status(thm)],[f781,f1321]) ).
fof(f1388,plain,
! [X0] :
( ~ q2(X0,d,X0)
| ~ p2(d,b,c)
| ~ l3(b,e)
| p3(X0,d,e) ),
inference(forward_subsumption_resolution,[status(thm)],[f782,f1268]) ).
fof(f1392,plain,
! [X0,X1] :
( ~ p2(X0,X1,X1)
| p3(X0,X1,X1) ),
inference(resolution,[status(thm)],[f795,f1163]) ).
fof(f1393,plain,
( ~ q2(e,e,b)
| p3(e,b,e) ),
inference(resolution,[status(thm)],[f799,f1163]) ).
fof(f1395,plain,
! [X0] :
( ~ n0(X0,b)
| q3(b,b) ),
inference(resolution,[status(thm)],[f801,f1284]) ).
fof(f1396,plain,
! [X0] :
( ~ n0(X0,X0)
| q3(X0,X0) ),
inference(resolution,[status(thm)],[f801,f1297]) ).
fof(f1397,plain,
! [X0,X1] :
( ~ q3(X0,d)
| ~ n1(X1,d,X0)
| q3(d,X0) ),
inference(resolution,[status(thm)],[f804,f1329]) ).
fof(f1398,plain,
! [X0,X1] :
( ~ q3(X0,b)
| ~ n1(X1,b,X0)
| q3(b,X0) ),
inference(resolution,[status(thm)],[f804,f1326]) ).
fof(f1399,plain,
! [X0,X1] :
( ~ l2(X1,X1)
| ~ r2(X0)
| q3(X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f806,f1226]) ).
fof(f1402,plain,
! [X0,X1] :
( ~ q3(X1,X0)
| ~ r2(d)
| ~ k1(X0)
| q3(X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f807,f387]) ).
fof(f1406,plain,
! [X0] : r3(X0,X0,X0),
inference(resolution,[status(thm)],[f820,f1280]) ).
fof(f1408,plain,
! [X0,X1,X2] :
( ~ r3(b,X2,X2)
| ~ m3(X1,b,X0)
| r3(X0,X0,b) ),
inference(resolution,[status(thm)],[f822,f1099]) ).
fof(f1409,plain,
! [X0] :
( ~ m3(a,X0,X0)
| ~ m2(b)
| ~ q2(X0,e,X0)
| r3(a,a,e) ),
inference(forward_subsumption_resolution,[status(thm)],[f823,f1227]) ).
fof(f1410,plain,
( ~ m2(b)
| ~ q2(a,e,a)
| r3(a,a,e) ),
inference(resolution,[status(thm)],[f1409,f1163]) ).
fof(f1411,plain,
( ~ q2(a,e,a)
| r3(a,a,e) ),
inference(forward_subsumption_resolution,[status(thm)],[f1410,f1099]) ).
fof(f1414,plain,
! [X0,X1] :
( ~ r3(a,X0,X0)
| ~ k2(X1,a)
| r3(X0,X1,a) ),
inference(resolution,[status(thm)],[f828,f1322]) ).
fof(f1415,plain,
! [X0,X1] :
( ~ r3(c,X0,X0)
| ~ k2(X1,c)
| r3(X0,X1,c) ),
inference(resolution,[status(thm)],[f828,f1321]) ).
fof(f1416,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| ~ q2(X1,d,X1)
| s3(d,X0) ),
inference(resolution,[status(thm)],[f830,f1329]) ).
fof(f1417,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| ~ q2(X1,b,X1)
| s3(b,X0) ),
inference(resolution,[status(thm)],[f830,f1326]) ).
fof(f1418,plain,
( ~ n3(e)
| ~ q3(e,b)
| k4(c) ),
inference(forward_subsumption_resolution,[status(thm)],[f831,f402]) ).
fof(f1421,plain,
! [X0,X1] :
( ~ k4(X1)
| n4(X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f848,f1163]) ).
fof(f1422,plain,
! [X0] :
( ~ r3(X0,e,X0)
| p4(e,e,X0) ),
inference(resolution,[status(thm)],[f849,f381]) ).
fof(f1423,plain,
! [X0] :
( ~ r3(X0,b,X0)
| p4(b,b,X0) ),
inference(resolution,[status(thm)],[f849,f377]) ).
fof(f1425,plain,
! [X0] : p4(X0,X0,X0),
inference(resolution,[status(thm)],[f852,f1146]) ).
fof(f1426,plain,
! [X0,X1] :
( ~ r3(X1,X1,X0)
| p4(X0,X1,X1) ),
inference(resolution,[status(thm)],[f854,f1425]) ).
fof(f1427,plain,
! [X0] :
( ~ m3(X0,c,a)
| p4(c,c,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f864,f1268]) ).
fof(f1431,plain,
! [X0,X1,X2,X3] :
( ~ q2(X3,X1,X0)
| ~ k3(X2,X2,X0)
| q4(X0,X1) ),
inference(resolution,[status(thm)],[f866,f1163]) ).
fof(f1432,plain,
! [X0,X1,X2] :
( ~ q4(X1,X2)
| ~ l4(X1)
| q4(X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f868,f1214]) ).
fof(f1433,plain,
! [X0,X1,X2] :
( ~ q4(X1,X2)
| q4(X0,X0) ),
inference(resolution,[status(thm)],[f1432,f1208]) ).
fof(f1434,plain,
! [X0,X1,X2,X3] :
( ~ p0(X3,X0)
| ~ q3(X1,X2)
| r4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f871,f1268]) ).
fof(f1435,plain,
! [X0,X1] :
( ~ p3(X0,c,X1)
| s4(c) ),
inference(resolution,[status(thm)],[f873,f936]) ).
fof(f1436,plain,
! [X0,X1] :
( ~ p3(X0,e,X1)
| s4(e) ),
inference(resolution,[status(thm)],[f873,f934]) ).
fof(f1437,plain,
! [X0,X1] :
( ~ p3(X0,b,X1)
| s4(b) ),
inference(resolution,[status(thm)],[f873,f933]) ).
fof(f1438,plain,
! [X0,X1] :
( ~ p3(X0,d,X1)
| s4(d) ),
inference(resolution,[status(thm)],[f873,f932]) ).
fof(f1439,plain,
! [X0,X1] :
( ~ p3(X0,a,X1)
| s4(a) ),
inference(resolution,[status(thm)],[f873,f931]) ).
fof(f1441,plain,
! [X0] :
( ~ q4(X0,X0)
| l5(c) ),
inference(resolution,[status(thm)],[f878,f928]) ).
fof(f1442,plain,
! [X0] :
( ~ q4(X0,X0)
| l5(e) ),
inference(resolution,[status(thm)],[f878,f926]) ).
fof(f1443,plain,
! [X0] :
( ~ q4(X0,X0)
| l5(b) ),
inference(resolution,[status(thm)],[f878,f925]) ).
fof(f1444,plain,
! [X0] :
( ~ q4(X0,X0)
| l5(d) ),
inference(resolution,[status(thm)],[f878,f924]) ).
fof(f1445,plain,
! [X0] :
( ~ q4(X0,X0)
| l5(a) ),
inference(resolution,[status(thm)],[f878,f923]) ).
fof(f1446,plain,
! [X0,X1] :
( ~ p4(e,X1,X0)
| m5(e,X0) ),
inference(resolution,[status(thm)],[f880,f381]) ).
fof(f1447,plain,
! [X0,X1] :
( ~ p4(b,X1,X0)
| m5(b,X0) ),
inference(resolution,[status(thm)],[f880,f377]) ).
fof(f1452,plain,
! [X0,X1,X2] :
( ~ q4(X1,X2)
| p5(X0,X1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f907,f1226]) ).
fof(f1454,plain,
! [X0,X1] :
( ~ n3(X1)
| ~ s4(X0)
| r5(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f917,f400]) ).
fof(f1455,plain,
! [X0,X1] :
( ~ r4(X1)
| s5(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f920,f1208]) ).
fof(f1456,plain,
! [X0] :
( ~ p0(e,X0)
| m1(X0,X0,c) ),
inference(resolution,[status(thm)],[f995,f398]) ).
fof(f1457,plain,
( ~ p0(c,e)
| l1(e,d) ),
inference(resolution,[status(thm)],[f939,f403]) ).
fof(f1458,plain,
( ~ p0(a,a)
| l1(a,b) ),
inference(resolution,[status(thm)],[f939,f406]) ).
fof(f1460,plain,
( ~ p0(c,b)
| l1(b,e) ),
inference(resolution,[status(thm)],[f939,f395]) ).
fof(f1461,plain,
( ~ p0(a,b)
| l1(b,c) ),
inference(resolution,[status(thm)],[f939,f384]) ).
fof(f1462,plain,
( ~ p0(e,e)
| l1(e,a) ),
inference(resolution,[status(thm)],[f939,f391]) ).
fof(f1463,plain,
! [X0] :
( ~ p0(a,X0)
| l1(X0,a) ),
inference(resolution,[status(thm)],[f939,f380]) ).
fof(f1464,plain,
! [X0,X1] :
( ~ p0(X1,d)
| l1(d,X0) ),
inference(resolution,[status(thm)],[f939,f387]) ).
fof(f1465,plain,
l1(b,e),
inference(forward_subsumption_resolution,[status(thm)],[f1460,f386]) ).
fof(f1467,plain,
q2(e,e,b),
inference(resolution,[status(thm)],[f1465,f698]) ).
fof(f1470,plain,
! [X0] : m1(e,X0,e),
inference(resolution,[status(thm)],[f950,f382]) ).
fof(f1471,plain,
! [X0] :
( ~ q0(X0,e)
| m1(X0,a,e) ),
inference(resolution,[status(thm)],[f1470,f989]) ).
fof(f1472,plain,
! [X0] : p2(X0,e,X0),
inference(resolution,[status(thm)],[f1470,f684]) ).
fof(f1477,plain,
! [X0,X1] :
( ~ m1(e,X1,X0)
| m1(e,X0,X0) ),
inference(resolution,[status(thm)],[f1470,f434]) ).
fof(f1483,plain,
m1(b,b,e),
inference(resolution,[status(thm)],[f956,f398]) ).
fof(f1485,plain,
m1(e,b,b),
inference(resolution,[status(thm)],[f974,f399]) ).
fof(f1487,plain,
! [X0] : m1(X0,d,d),
inference(resolution,[status(thm)],[f974,f387]) ).
fof(f1488,plain,
( ~ n0(d,d)
| p2(a,d,d) ),
inference(resolution,[status(thm)],[f1487,f669]) ).
fof(f1497,plain,
m1(c,b,c),
inference(resolution,[status(thm)],[f987,f392]) ).
fof(f1498,plain,
m1(a,b,a),
inference(resolution,[status(thm)],[f987,f388]) ).
fof(f1499,plain,
m1(c,e,c),
inference(resolution,[status(thm)],[f988,f392]) ).
fof(f1500,plain,
m1(a,e,a),
inference(resolution,[status(thm)],[f988,f388]) ).
fof(f1507,plain,
! [X0] :
( ~ p0(X0,e)
| n1(e,a,e) ),
inference(resolution,[status(thm)],[f1008,f381]) ).
fof(f1508,plain,
! [X0] :
( ~ p0(X0,b)
| n1(b,a,b) ),
inference(resolution,[status(thm)],[f1008,f377]) ).
fof(f1512,plain,
n1(d,e,e),
inference(resolution,[status(thm)],[f1020,f924]) ).
fof(f1526,plain,
! [X0] :
( ~ n1(c,X0,c)
| n1(c,X0,X0) ),
inference(resolution,[status(thm)],[f1048,f936]) ).
fof(f1527,plain,
! [X0] : n1(c,X0,X0),
inference(forward_subsumption_resolution,[status(thm)],[f1526,f1379]) ).
fof(f1528,plain,
! [X0] :
( ~ k2(c,a)
| ~ p0(b,X0)
| p2(b,c,a) ),
inference(backward_subsumption_resolution,[status(thm)],[f1245,f1527]) ).
fof(f1530,plain,
( ~ k2(c,a)
| p2(b,c,a) ),
inference(forward_subsumption_resolution,[status(thm)],[f1528,f382]) ).
fof(f1531,plain,
! [X0] :
( ~ n1(a,X0,a)
| n1(a,X0,X0) ),
inference(resolution,[status(thm)],[f1049,f931]) ).
fof(f1532,plain,
! [X0] : n1(a,X0,X0),
inference(forward_subsumption_resolution,[status(thm)],[f1531,f1380]) ).
fof(f1547,plain,
! [X0,X1] : n1(X0,X0,X1),
inference(resolution,[status(thm)],[f1073,f387]) ).
fof(f1548,plain,
! [X0] :
( ~ q1(e,c,X0)
| ~ p1(X0,b,b)
| p2(b,c,c) ),
inference(backward_subsumption_resolution,[status(thm)],[f662,f1547]) ).
fof(f1549,plain,
! [X0] :
( ~ q1(a,X0,e)
| p2(e,e,X0) ),
inference(resolution,[status(thm)],[f1547,f654]) ).
fof(f1552,plain,
p1(c,c,e),
inference(resolution,[status(thm)],[f1082,f396]) ).
fof(f1554,plain,
p1(b,b,e),
inference(resolution,[status(thm)],[f1083,f396]) ).
fof(f1557,plain,
p1(c,b,c),
inference(resolution,[status(thm)],[f1109,f1106]) ).
fof(f1559,plain,
! [X0] : p1(b,X0,b),
inference(resolution,[status(thm)],[f1109,f1107]) ).
fof(f1562,plain,
! [X0,X1] :
( ~ m0(b,X0,b)
| p1(X0,X1,b) ),
inference(resolution,[status(thm)],[f1559,f538]) ).
fof(f1563,plain,
( ~ q2(b,c,d)
| ~ l1(d,b)
| m3(c,b,d) ),
inference(backward_subsumption_resolution,[status(thm)],[f765,f1241]) ).
fof(f1564,plain,
m2(d),
inference(resolution,[status(thm)],[f1241,f936]) ).
fof(f1570,plain,
! [X0,X1,X2] :
( ~ r3(d,X2,X2)
| ~ m3(X1,b,X0)
| r3(X0,X0,d) ),
inference(resolution,[status(thm)],[f1564,f822]) ).
fof(f1571,plain,
! [X0,X1] :
( ~ m3(X1,X0,X1)
| m3(X0,d,d) ),
inference(resolution,[status(thm)],[f1564,f1369]) ).
fof(f1577,plain,
! [X0] : q1(X0,a,X0),
inference(resolution,[status(thm)],[f1147,f382]) ).
fof(f1579,plain,
! [X0] : q1(X0,d,X0),
inference(resolution,[status(thm)],[f1148,f382]) ).
fof(f1581,plain,
! [X0] : q1(X0,b,X0),
inference(resolution,[status(thm)],[f1149,f382]) ).
fof(f1583,plain,
! [X0] : q1(X0,e,X0),
inference(resolution,[status(thm)],[f1150,f382]) ).
fof(f1585,plain,
! [X0] : q1(X0,c,X0),
inference(resolution,[status(thm)],[f1152,f382]) ).
fof(f1586,plain,
! [X0] : p2(X0,a,X0),
inference(backward_subsumption_resolution,[status(thm)],[f631,f1577]) ).
fof(f1590,plain,
! [X0] :
( ~ q1(X0,X0,b)
| q1(c,X0,X0) ),
inference(resolution,[status(thm)],[f1168,f392]) ).
fof(f1591,plain,
! [X0] :
( ~ q1(X0,X0,b)
| q1(a,X0,X0) ),
inference(resolution,[status(thm)],[f1168,f388]) ).
fof(f1592,plain,
! [X0] :
( ~ q1(X0,X0,e)
| q1(c,X0,X0) ),
inference(resolution,[status(thm)],[f1169,f392]) ).
fof(f1593,plain,
! [X0] :
( ~ q1(X0,X0,e)
| q1(a,X0,X0) ),
inference(resolution,[status(thm)],[f1169,f388]) ).
fof(f1594,plain,
( ~ p1(e,b,b)
| p2(b,c,c) ),
inference(resolution,[status(thm)],[f1585,f1548]) ).
fof(f1595,plain,
! [X0,X1] :
( ~ q0(X0,X0)
| ~ r0(X1)
| q1(c,X0,c) ),
inference(resolution,[status(thm)],[f1185,f382]) ).
fof(f1596,plain,
! [X0,X1] :
( ~ q0(X0,X0)
| ~ r0(X1)
| q1(a,X0,a) ),
inference(resolution,[status(thm)],[f1186,f382]) ).
fof(f1601,plain,
! [X0] : q1(X0,X0,d),
inference(resolution,[status(thm)],[f1209,f1487]) ).
fof(f1611,plain,
! [X0] : l2(X0,X0),
inference(resolution,[status(thm)],[f1235,f387]) ).
fof(f1612,plain,
! [X0,X1] :
( ~ s4(X1)
| p5(X0,X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f903,f1611]) ).
fof(f1614,plain,
! [X0] :
( ~ r2(X0)
| q3(X0,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1399,f1611]) ).
fof(f1615,plain,
! [X0,X1] :
( ~ n0(e,X1)
| l2(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f1231,f1611]) ).
fof(f1616,plain,
! [X0] : l2(X0,b),
inference(backward_subsumption_resolution,[status(thm)],[f1233,f1611]) ).
fof(f1617,plain,
! [X0] : l2(X0,e),
inference(backward_subsumption_resolution,[status(thm)],[f1232,f1611]) ).
fof(f1618,plain,
! [X0] :
( ~ s2(X0)
| r3(c,X0,X0) ),
inference(resolution,[status(thm)],[f1611,f809]) ).
fof(f1624,plain,
( ~ m1(d,a,c)
| ~ l1(e,c)
| p2(a,c,b) ),
inference(backward_subsumption_resolution,[status(thm)],[f1278,f1616]) ).
fof(f1625,plain,
! [X0] :
( ~ s2(X0)
| r3(b,X0,X0) ),
inference(resolution,[status(thm)],[f1616,f809]) ).
fof(f1626,plain,
q3(a,a),
inference(resolution,[status(thm)],[f1614,f1322]) ).
fof(f1627,plain,
q3(c,c),
inference(resolution,[status(thm)],[f1614,f1321]) ).
fof(f1630,plain,
! [X0] :
( ~ s2(X0)
| r3(e,X0,X0) ),
inference(resolution,[status(thm)],[f1617,f809]) ).
fof(f1646,plain,
! [X0] : q2(X0,b,X0),
inference(resolution,[status(thm)],[f1318,f387]) ).
fof(f1654,plain,
! [X0] : q2(X0,e,X0),
inference(resolution,[status(thm)],[f1319,f387]) ).
fof(f1659,plain,
! [X0] : k3(c,X0,c),
inference(resolution,[status(thm)],[f1336,f1281]) ).
fof(f1676,plain,
k3(d,a,d),
inference(resolution,[status(thm)],[f1340,f1586]) ).
fof(f1678,plain,
k3(d,b,d),
inference(resolution,[status(thm)],[f1340,f1280]) ).
fof(f1679,plain,
k3(d,c,d),
inference(resolution,[status(thm)],[f1340,f1267]) ).
fof(f1684,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| r4(X0) ),
inference(resolution,[status(thm)],[f1626,f1434]) ).
fof(f1689,plain,
k3(d,e,d),
inference(resolution,[status(thm)],[f1342,f1267]) ).
fof(f1690,plain,
! [X0,X1] :
( ~ p1(X1,d,X0)
| k3(X0,X0,X1) ),
inference(resolution,[status(thm)],[f1346,f1564]) ).
fof(f1691,plain,
! [X0,X1] :
( ~ p1(X1,b,X0)
| k3(X0,X0,X1) ),
inference(resolution,[status(thm)],[f1346,f1099]) ).
fof(f1694,plain,
l3(e,a),
inference(resolution,[status(thm)],[f1351,f1586]) ).
fof(f1696,plain,
l3(e,b),
inference(resolution,[status(thm)],[f1351,f1280]) ).
fof(f1698,plain,
l3(b,a),
inference(resolution,[status(thm)],[f1352,f1586]) ).
fof(f1699,plain,
l3(b,e),
inference(resolution,[status(thm)],[f1352,f1472]) ).
fof(f1704,plain,
! [X0] :
( ~ n0(X0,b)
| q3(b,X0) ),
inference(resolution,[status(thm)],[f1646,f801]) ).
fof(f1706,plain,
! [X0] : m3(X0,b,b),
inference(resolution,[status(thm)],[f1370,f1163]) ).
fof(f1713,plain,
s2(e),
inference(resolution,[status(thm)],[f1654,f1325]) ).
fof(f1715,plain,
! [X0] :
( ~ n0(X0,e)
| q3(e,X0) ),
inference(resolution,[status(thm)],[f1654,f801]) ).
fof(f1719,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| ~ q2(X1,e,X1)
| s3(e,X0) ),
inference(resolution,[status(thm)],[f1713,f830]) ).
fof(f1720,plain,
! [X0,X1] :
( ~ q3(X0,e)
| ~ n1(X1,e,X0)
| q3(e,X0) ),
inference(resolution,[status(thm)],[f1713,f804]) ).
fof(f1722,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| s3(e,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1719,f1654]) ).
fof(f1723,plain,
! [X0,X1] :
( ~ m3(X1,b,X0)
| r3(X0,X0,b) ),
inference(resolution,[status(thm)],[f1408,f1406]) ).
fof(f1724,plain,
r3(a,a,e),
inference(forward_subsumption_resolution,[status(thm)],[f1411,f1654]) ).
fof(f1728,plain,
! [X0] :
( ~ k3(X0,X0,e)
| q4(e,e) ),
inference(resolution,[status(thm)],[f1431,f1285]) ).
fof(f1729,plain,
! [X0,X1] :
( ~ k3(X1,X1,X0)
| q4(X0,e) ),
inference(resolution,[status(thm)],[f1431,f1654]) ).
fof(f1731,plain,
! [X0,X1] :
( ~ k3(X1,X1,X0)
| q4(X0,b) ),
inference(resolution,[status(thm)],[f1431,f1646]) ).
fof(f1733,plain,
! [X0] :
( ~ q2(X0,d,X0)
| ~ p2(d,b,c)
| p3(X0,d,e) ),
inference(backward_subsumption_resolution,[status(thm)],[f1388,f1699]) ).
fof(f1739,plain,
! [X0] : r4(X0),
inference(resolution,[status(thm)],[f1684,f382]) ).
fof(f1740,plain,
! [X0] : s5(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1455,f1739]) ).
fof(f1741,plain,
! [X0] : n5(X0,X0),
inference(backward_subsumption_resolution,[status(thm)],[f897,f1739]) ).
fof(f1742,plain,
! [X0,X1,X2,X3] :
( ~ p4(X1,X1,X1)
| ~ n4(X0,X3)
| ~ q4(X2,X3)
| n5(X0,X1) ),
inference(resolution,[status(thm)],[f1741,f887]) ).
fof(f1743,plain,
! [X0,X1,X2,X3] :
( ~ n4(X0,X3)
| ~ q4(X2,X3)
| n5(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1742,f1425]) ).
fof(f1749,plain,
! [X0,X1] :
( ~ p2(X0,X1,b)
| p3(X0,X1,X1) ),
inference(resolution,[status(thm)],[f1706,f795]) ).
fof(f1750,plain,
m1(d,a,c),
inference(resolution,[status(thm)],[f990,f401]) ).
fof(f1751,plain,
m1(b,c,c),
inference(resolution,[status(thm)],[f997,f374]) ).
fof(f1752,plain,
m1(d,c,c),
inference(resolution,[status(thm)],[f997,f385]) ).
fof(f1753,plain,
m1(b,e,e),
inference(resolution,[status(thm)],[f998,f374]) ).
fof(f1754,plain,
m1(d,e,e),
inference(resolution,[status(thm)],[f998,f385]) ).
fof(f1756,plain,
m1(d,b,b),
inference(resolution,[status(thm)],[f999,f385]) ).
fof(f1757,plain,
m1(b,a,a),
inference(resolution,[status(thm)],[f1001,f374]) ).
fof(f1758,plain,
m1(d,a,a),
inference(resolution,[status(thm)],[f1001,f385]) ).
fof(f1759,plain,
m1(a,a,b),
inference(resolution,[status(thm)],[f1052,f404]) ).
fof(f1760,plain,
m1(d,a,b),
inference(resolution,[status(thm)],[f1052,f397]) ).
fof(f1766,plain,
! [X0] : p1(d,X0,d),
inference(resolution,[status(thm)],[f1130,f387]) ).
fof(f1776,plain,
! [X0] : q1(d,d,X0),
inference(resolution,[status(thm)],[f1198,f382]) ).
fof(f1777,plain,
! [X0,X1] :
( ~ m1(X1,c,X0)
| k2(X0,c) ),
inference(resolution,[status(thm)],[f1216,f1227]) ).
fof(f1778,plain,
q3(e,e),
inference(resolution,[status(thm)],[f1396,f398]) ).
fof(f1779,plain,
! [X0,X1] :
( ~ m1(X1,e,X0)
| k2(X0,e) ),
inference(resolution,[status(thm)],[f1217,f1227]) ).
fof(f1780,plain,
! [X0,X1] :
( ~ m1(X1,b,X0)
| k2(X0,b) ),
inference(resolution,[status(thm)],[f1218,f1227]) ).
fof(f1782,plain,
! [X0,X1] :
( ~ m1(X1,d,X0)
| k2(X0,d) ),
inference(resolution,[status(thm)],[f1219,f1227]) ).
fof(f1783,plain,
! [X0,X1] :
( ~ m1(X1,a,X0)
| k2(X0,a) ),
inference(resolution,[status(thm)],[f1220,f1227]) ).
fof(f1789,plain,
! [X0] :
( ~ p2(d,X0,d)
| p2(d,X0,X0) ),
inference(resolution,[status(thm)],[f1253,f1766]) ).
fof(f1791,plain,
! [X0] : p2(d,X0,X0),
inference(forward_subsumption_resolution,[status(thm)],[f1789,f1281]) ).
fof(f1794,plain,
! [X0] : p2(X0,a,a),
inference(resolution,[status(thm)],[f1255,f1586]) ).
fof(f1795,plain,
! [X0] : p2(X0,e,e),
inference(resolution,[status(thm)],[f1255,f1472]) ).
fof(f1796,plain,
! [X0] : p2(X0,b,b),
inference(resolution,[status(thm)],[f1255,f1280]) ).
fof(f1807,plain,
! [X0] : p3(d,X0,X0),
inference(resolution,[status(thm)],[f1791,f1392]) ).
fof(f1808,plain,
! [X0] : r3(d,X0,d),
inference(resolution,[status(thm)],[f1791,f820]) ).
fof(f1809,plain,
! [X0] : k3(X0,d,X0),
inference(resolution,[status(thm)],[f1791,f728]) ).
fof(f1819,plain,
! [X0] : p3(X0,a,a),
inference(resolution,[status(thm)],[f1794,f1392]) ).
fof(f1820,plain,
! [X0] : r3(X0,a,X0),
inference(resolution,[status(thm)],[f1794,f820]) ).
fof(f1821,plain,
! [X0] : k3(a,X0,a),
inference(resolution,[status(thm)],[f1794,f728]) ).
fof(f1822,plain,
q2(b,a,b),
inference(resolution,[status(thm)],[f1301,f1532]) ).
fof(f1823,plain,
q2(b,c,b),
inference(resolution,[status(thm)],[f1301,f1527]) ).
fof(f1825,plain,
q2(e,c,c),
inference(resolution,[status(thm)],[f1303,f1617]) ).
fof(f1826,plain,
q2(b,c,c),
inference(resolution,[status(thm)],[f1303,f1616]) ).
fof(f1828,plain,
! [X0] : m3(X0,e,e),
inference(backward_subsumption_resolution,[status(thm)],[f1375,f1795]) ).
fof(f1834,plain,
! [X0] : p3(X0,e,e),
inference(resolution,[status(thm)],[f1795,f1392]) ).
fof(f1835,plain,
! [X0] : r3(X0,e,X0),
inference(resolution,[status(thm)],[f1795,f820]) ).
fof(f1836,plain,
! [X0] : k3(e,X0,e),
inference(resolution,[status(thm)],[f1795,f728]) ).
fof(f1838,plain,
! [X0,X1] :
( ~ p2(X0,X1,e)
| p3(X0,X1,X1) ),
inference(resolution,[status(thm)],[f1828,f795]) ).
fof(f1845,plain,
! [X0] : p4(e,e,X0),
inference(backward_subsumption_resolution,[status(thm)],[f1422,f1835]) ).
fof(f1846,plain,
! [X0] :
( ~ q1(a,a,X0)
| ~ q3(X0,X0)
| k4(e) ),
inference(resolution,[status(thm)],[f1835,f834]) ).
fof(f1847,plain,
! [X0] : m5(e,X0),
inference(resolution,[status(thm)],[f1845,f1446]) ).
fof(f1850,plain,
q2(e,c,e),
inference(resolution,[status(thm)],[f1304,f1617]) ).
fof(f1851,plain,
q2(b,c,e),
inference(resolution,[status(thm)],[f1304,f1616]) ).
fof(f1853,plain,
q2(e,c,b),
inference(resolution,[status(thm)],[f1305,f1617]) ).
fof(f1856,plain,
q2(e,c,d),
inference(resolution,[status(thm)],[f1306,f1617]) ).
fof(f1857,plain,
q2(b,c,d),
inference(resolution,[status(thm)],[f1306,f1616]) ).
fof(f1858,plain,
q2(d,c,d),
inference(resolution,[status(thm)],[f1306,f1611]) ).
fof(f1866,plain,
! [X0] : p3(X0,b,b),
inference(resolution,[status(thm)],[f1796,f1392]) ).
fof(f1867,plain,
! [X0] : r3(X0,b,X0),
inference(resolution,[status(thm)],[f1796,f820]) ).
fof(f1868,plain,
! [X0] : k3(b,X0,b),
inference(resolution,[status(thm)],[f1796,f728]) ).
fof(f1869,plain,
q2(e,c,a),
inference(resolution,[status(thm)],[f1307,f1617]) ).
fof(f1870,plain,
q2(b,c,a),
inference(resolution,[status(thm)],[f1307,f1616]) ).
fof(f1871,plain,
q2(a,c,a),
inference(resolution,[status(thm)],[f1307,f1611]) ).
fof(f1873,plain,
q2(e,a,e),
inference(resolution,[status(thm)],[f1309,f1532]) ).
fof(f1876,plain,
! [X0] : p4(b,b,X0),
inference(backward_subsumption_resolution,[status(thm)],[f1423,f1867]) ).
fof(f1878,plain,
! [X0] : m5(b,X0),
inference(resolution,[status(thm)],[f1876,f1447]) ).
fof(f1881,plain,
! [X0,X1] :
( ~ m0(e,X1,X1)
| m3(e,X0,e) ),
inference(resolution,[status(thm)],[f1366,f1617]) ).
fof(f1882,plain,
! [X0,X1] :
( ~ m0(b,X1,X1)
| m3(b,X0,b) ),
inference(resolution,[status(thm)],[f1366,f1616]) ).
fof(f1883,plain,
! [X0,X1] :
( ~ m0(X0,X0,X0)
| m3(X0,X1,X0) ),
inference(resolution,[status(thm)],[f1366,f1611]) ).
fof(f1886,plain,
m3(c,c,a),
inference(resolution,[status(thm)],[f1377,f1659]) ).
fof(f1892,plain,
! [X0] : p3(c,c,X0),
inference(resolution,[status(thm)],[f1387,f1659]) ).
fof(f1895,plain,
( ~ r0(b)
| l3(d,c) ),
inference(backward_subsumption_resolution,[status(thm)],[f1363,f1821]) ).
fof(f1896,plain,
! [X0] : p3(a,a,X0),
inference(resolution,[status(thm)],[f1821,f1386]) ).
fof(f1897,plain,
m3(a,a,c),
inference(resolution,[status(thm)],[f1821,f1378]) ).
fof(f1900,plain,
l3(d,c),
inference(forward_subsumption_resolution,[status(thm)],[f1895,f377]) ).
fof(f1901,plain,
q3(b,b),
inference(resolution,[status(thm)],[f1395,f383]) ).
fof(f1908,plain,
! [X0] :
( ~ q3(X0,d)
| q3(d,X0) ),
inference(resolution,[status(thm)],[f1397,f1547]) ).
fof(f1910,plain,
! [X0] :
( ~ r3(a,X0,X0)
| r3(X0,a,a) ),
inference(resolution,[status(thm)],[f1414,f1227]) ).
fof(f1911,plain,
! [X0] :
( ~ r3(c,X0,X0)
| r3(X0,c,c) ),
inference(resolution,[status(thm)],[f1415,f1227]) ).
fof(f1912,plain,
! [X0,X1] :
( ~ m0(d,X1,X0)
| s3(d,X0) ),
inference(resolution,[status(thm)],[f1416,f1297]) ).
fof(f1914,plain,
p4(e,a,a),
inference(resolution,[status(thm)],[f1426,f1724]) ).
fof(f1919,plain,
m3(e,e,c),
inference(resolution,[status(thm)],[f1836,f1378]) ).
fof(f1920,plain,
m3(e,e,a),
inference(resolution,[status(thm)],[f1836,f1377]) ).
fof(f1925,plain,
s4(c),
inference(resolution,[status(thm)],[f1435,f1807]) ).
fof(f1927,plain,
s4(e),
inference(resolution,[status(thm)],[f1436,f1807]) ).
fof(f1930,plain,
! [X0] : p5(X0,X0,c),
inference(resolution,[status(thm)],[f1925,f1612]) ).
fof(f1931,plain,
! [X0] :
( ~ n3(X0)
| r5(c,X0) ),
inference(resolution,[status(thm)],[f1925,f1454]) ).
fof(f1932,plain,
! [X0] :
( ~ m2(X0)
| q5(c,X0) ),
inference(resolution,[status(thm)],[f1925,f911]) ).
fof(f1933,plain,
! [X0] :
( ~ r0(X0)
| m5(X0,X0) ),
inference(resolution,[status(thm)],[f1925,f885]) ).
fof(f1934,plain,
! [X0,X1] :
( ~ r3(X1,X0,X0)
| k5(X0) ),
inference(resolution,[status(thm)],[f1925,f875]) ).
fof(f1935,plain,
! [X0] : r5(c,X0),
inference(forward_subsumption_resolution,[status(thm)],[f1931,f1268]) ).
fof(f1936,plain,
s4(b),
inference(resolution,[status(thm)],[f1437,f1807]) ).
fof(f1938,plain,
s4(d),
inference(resolution,[status(thm)],[f1438,f1807]) ).
fof(f1940,plain,
s4(a),
inference(resolution,[status(thm)],[f1439,f1807]) ).
fof(f1944,plain,
! [X0] : p5(X0,X0,e),
inference(resolution,[status(thm)],[f1927,f1612]) ).
fof(f1945,plain,
! [X0] :
( ~ n3(X0)
| r5(e,X0) ),
inference(resolution,[status(thm)],[f1927,f1454]) ).
fof(f1946,plain,
! [X0] :
( ~ m2(X0)
| q5(e,X0) ),
inference(resolution,[status(thm)],[f1927,f911]) ).
fof(f1949,plain,
! [X0] : r5(e,X0),
inference(forward_subsumption_resolution,[status(thm)],[f1945,f1268]) ).
fof(f1954,plain,
! [X0] : p5(X0,X0,b),
inference(resolution,[status(thm)],[f1936,f1612]) ).
fof(f1955,plain,
! [X0] :
( ~ n3(X0)
| r5(b,X0) ),
inference(resolution,[status(thm)],[f1936,f1454]) ).
fof(f1956,plain,
! [X0] :
( ~ m2(X0)
| q5(b,X0) ),
inference(resolution,[status(thm)],[f1936,f911]) ).
fof(f1959,plain,
! [X0] : r5(b,X0),
inference(forward_subsumption_resolution,[status(thm)],[f1955,f1268]) ).
fof(f1961,plain,
! [X0] : p5(X0,X0,d),
inference(resolution,[status(thm)],[f1938,f1612]) ).
fof(f1962,plain,
! [X0] :
( ~ n3(X0)
| r5(d,X0) ),
inference(resolution,[status(thm)],[f1938,f1454]) ).
fof(f1963,plain,
! [X0] :
( ~ m2(X0)
| q5(d,X0) ),
inference(resolution,[status(thm)],[f1938,f911]) ).
fof(f1966,plain,
! [X0] : r5(d,X0),
inference(forward_subsumption_resolution,[status(thm)],[f1962,f1268]) ).
fof(f1967,plain,
! [X0] : l1(d,X0),
inference(resolution,[status(thm)],[f1464,f382]) ).
fof(f1970,plain,
! [X0] :
( ~ m1(b,e,X0)
| m1(X0,e,e) ),
inference(resolution,[status(thm)],[f1483,f434]) ).
fof(f1973,plain,
! [X0] : p5(X0,X0,a),
inference(resolution,[status(thm)],[f1940,f1612]) ).
fof(f1974,plain,
! [X0] :
( ~ n3(X0)
| r5(a,X0) ),
inference(resolution,[status(thm)],[f1940,f1454]) ).
fof(f1975,plain,
! [X0] :
( ~ m2(X0)
| q5(a,X0) ),
inference(resolution,[status(thm)],[f1940,f911]) ).
fof(f1978,plain,
! [X0] : r5(a,X0),
inference(forward_subsumption_resolution,[status(thm)],[f1974,f1268]) ).
fof(f1979,plain,
p1(e,b,b),
inference(resolution,[status(thm)],[f1485,f1135]) ).
fof(f1980,plain,
q1(e,e,b),
inference(resolution,[status(thm)],[f1485,f1209]) ).
fof(f1982,plain,
! [X0] :
( ~ m1(e,b,X0)
| m1(X0,b,b) ),
inference(resolution,[status(thm)],[f1485,f434]) ).
fof(f1985,plain,
p2(b,c,b),
inference(resolution,[status(thm)],[f1497,f684]) ).
fof(f1987,plain,
! [X0] :
( ~ m1(c,X0,b)
| m1(c,b,b) ),
inference(resolution,[status(thm)],[f1497,f434]) ).
fof(f1990,plain,
! [X0] :
( ~ m1(a,X0,b)
| m1(a,b,b) ),
inference(resolution,[status(thm)],[f1498,f434]) ).
fof(f1991,plain,
p2(e,c,e),
inference(resolution,[status(thm)],[f1499,f684]) ).
fof(f1993,plain,
! [X0] :
( ~ m1(c,X0,e)
| m1(c,e,e) ),
inference(resolution,[status(thm)],[f1499,f434]) ).
fof(f1996,plain,
! [X0] :
( ~ m1(a,X0,e)
| m1(a,e,e) ),
inference(resolution,[status(thm)],[f1500,f434]) ).
fof(f1997,plain,
n1(e,a,e),
inference(resolution,[status(thm)],[f1507,f382]) ).
fof(f1998,plain,
n1(b,a,b),
inference(resolution,[status(thm)],[f1508,f386]) ).
fof(f2000,plain,
q2(e,d,e),
inference(resolution,[status(thm)],[f1512,f1309]) ).
fof(f2001,plain,
( ~ q2(b,c,d)
| m3(c,b,d) ),
inference(backward_subsumption_resolution,[status(thm)],[f1563,f1967]) ).
fof(f2004,plain,
! [X0] : q2(X0,X0,d),
inference(resolution,[status(thm)],[f1967,f698]) ).
fof(f2005,plain,
p2(e,c,c),
inference(resolution,[status(thm)],[f1552,f1248]) ).
fof(f2006,plain,
p1(e,c,e),
inference(resolution,[status(thm)],[f1552,f1109]) ).
fof(f2007,plain,
! [X0] :
( ~ m0(c,c,e)
| p1(c,X0,c) ),
inference(resolution,[status(thm)],[f1552,f538]) ).
fof(f2009,plain,
p1(e,b,e),
inference(resolution,[status(thm)],[f1554,f1109]) ).
fof(f2013,plain,
q1(c,d,d),
inference(resolution,[status(thm)],[f1590,f1776]) ).
fof(f2017,plain,
q1(a,d,d),
inference(resolution,[status(thm)],[f1591,f1776]) ).
fof(f2023,plain,
! [X0,X1] :
( ~ k3(X1,X1,d)
| q4(d,X0) ),
inference(resolution,[status(thm)],[f2004,f1431]) ).
fof(f2024,plain,
! [X0] :
( ~ n0(X0,X0)
| q3(X0,d) ),
inference(resolution,[status(thm)],[f2004,f801]) ).
fof(f2025,plain,
! [X0] :
( ~ n1(X0,d,X0)
| ~ p1(d,d,X0)
| q2(d,X0,d) ),
inference(resolution,[status(thm)],[f2004,f692]) ).
fof(f2027,plain,
q1(c,e,e),
inference(resolution,[status(thm)],[f1592,f1189]) ).
fof(f2031,plain,
q1(a,e,e),
inference(resolution,[status(thm)],[f1593,f1189]) ).
fof(f2034,plain,
! [X0] :
( ~ q0(X0,X0)
| q1(c,X0,c) ),
inference(resolution,[status(thm)],[f1595,f381]) ).
fof(f2036,plain,
! [X0] :
( ~ q0(X0,X0)
| q1(a,X0,a) ),
inference(resolution,[status(thm)],[f1596,f381]) ).
fof(f2038,plain,
m3(b,b,c),
inference(resolution,[status(thm)],[f1868,f1378]) ).
fof(f2039,plain,
m3(b,b,a),
inference(resolution,[status(thm)],[f1868,f1377]) ).
fof(f2042,plain,
r3(b,e,e),
inference(resolution,[status(thm)],[f1625,f1713]) ).
fof(f2043,plain,
r3(b,d,d),
inference(resolution,[status(thm)],[f1625,f1329]) ).
fof(f2046,plain,
r3(e,d,d),
inference(resolution,[status(thm)],[f1630,f1329]) ).
fof(f2047,plain,
r3(e,b,b),
inference(resolution,[status(thm)],[f1630,f1326]) ).
fof(f2050,plain,
p3(e,b,e),
inference(backward_subsumption_resolution,[status(thm)],[f1393,f1467]) ).
fof(f2052,plain,
( ~ n0(e,e)
| q3(e,b) ),
inference(resolution,[status(thm)],[f1467,f801]) ).
fof(f2054,plain,
q3(e,b),
inference(forward_subsumption_resolution,[status(thm)],[f2052,f398]) ).
fof(f2055,plain,
( ~ n3(e)
| k4(c) ),
inference(backward_subsumption_resolution,[status(thm)],[f1418,f2054]) ).
fof(f2057,plain,
k4(c),
inference(forward_subsumption_resolution,[status(thm)],[f2055,f1268]) ).
fof(f2058,plain,
! [X0] : n4(X0,X0),
inference(resolution,[status(thm)],[f2057,f1421]) ).
fof(f2060,plain,
m5(c,c),
inference(resolution,[status(thm)],[f2057,f881]) ).
fof(f2061,plain,
! [X0,X1] :
( ~ p3(X0,X1,X1)
| n4(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f844,f2058]) ).
fof(f2065,plain,
! [X0] : n4(d,X0),
inference(resolution,[status(thm)],[f2061,f1807]) ).
fof(f2066,plain,
! [X0] : n4(X0,b),
inference(resolution,[status(thm)],[f2061,f1866]) ).
fof(f2067,plain,
! [X0] : n4(X0,e),
inference(resolution,[status(thm)],[f2061,f1834]) ).
fof(f2068,plain,
! [X0] : n4(X0,a),
inference(resolution,[status(thm)],[f2061,f1819]) ).
fof(f2072,plain,
m3(d,d,a),
inference(resolution,[status(thm)],[f1676,f1377]) ).
fof(f2081,plain,
! [X0] : k3(a,a,X0),
inference(resolution,[status(thm)],[f1691,f1134]) ).
fof(f2084,plain,
q4(e,e),
inference(resolution,[status(thm)],[f1728,f1836]) ).
fof(f2086,plain,
l5(a),
inference(resolution,[status(thm)],[f2084,f1445]) ).
fof(f2087,plain,
l5(d),
inference(resolution,[status(thm)],[f2084,f1444]) ).
fof(f2088,plain,
l5(b),
inference(resolution,[status(thm)],[f2084,f1443]) ).
fof(f2089,plain,
l5(e),
inference(resolution,[status(thm)],[f2084,f1442]) ).
fof(f2090,plain,
l5(c),
inference(resolution,[status(thm)],[f2084,f1441]) ).
fof(f2091,plain,
! [X0] : q4(X0,X0),
inference(resolution,[status(thm)],[f2084,f1433]) ).
fof(f2092,plain,
! [X0,X1] :
( ~ n4(X0,e)
| n5(X0,X1) ),
inference(resolution,[status(thm)],[f2084,f1743]) ).
fof(f2094,plain,
! [X0,X1] : n5(X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[f2092,f2067]) ).
fof(f2098,plain,
! [X0] : p1(a,X0,b),
inference(resolution,[status(thm)],[f1138,f406]) ).
fof(f2099,plain,
! [X0] : p1(b,X0,c),
inference(resolution,[status(thm)],[f1138,f384]) ).
fof(f2101,plain,
! [X0,X1] : p1(d,X0,X1),
inference(resolution,[status(thm)],[f1138,f387]) ).
fof(f2102,plain,
! [X0] :
( ~ k1(X0)
| l5(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f878,f2091]) ).
fof(f2105,plain,
! [X0,X1] : p5(X0,X1,X0),
inference(resolution,[status(thm)],[f2091,f1452]) ).
fof(f2119,plain,
! [X0,X1,X2] :
( ~ m4(X2,X1)
| ~ l2(X0,X2)
| p5(X0,X1,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f905,f2105]) ).
fof(f2125,plain,
! [X0] :
( ~ q3(X0,b)
| q3(b,X0) ),
inference(resolution,[status(thm)],[f1398,f1547]) ).
fof(f2126,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| s3(b,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1417,f1646]) ).
fof(f2134,plain,
! [X0] : s3(b,X0),
inference(resolution,[status(thm)],[f2126,f387]) ).
fof(f2135,plain,
m1(b,a,e),
inference(resolution,[status(thm)],[f1471,f389]) ).
fof(f2136,plain,
! [X0] : k3(X0,X0,d),
inference(resolution,[status(thm)],[f2101,f1691]) ).
fof(f2137,plain,
! [X0] : p2(e,d,X0),
inference(resolution,[status(thm)],[f2101,f1248]) ).
fof(f2138,plain,
! [X0] : p1(X0,d,X0),
inference(resolution,[status(thm)],[f2101,f1109]) ).
fof(f2139,plain,
! [X0,X1,X2] :
( ~ m0(d,X0,X2)
| p1(X0,X1,d) ),
inference(resolution,[status(thm)],[f2101,f538]) ).
fof(f2147,plain,
! [X0,X1] :
( ~ m3(X1,b,X0)
| r3(X0,X0,d) ),
inference(resolution,[status(thm)],[f1570,f1406]) ).
fof(f2150,plain,
! [X0] : m3(X0,d,d),
inference(resolution,[status(thm)],[f1571,f1163]) ).
fof(f2151,plain,
r3(c,e,e),
inference(resolution,[status(thm)],[f1618,f1713]) ).
fof(f2152,plain,
r3(c,d,d),
inference(resolution,[status(thm)],[f1618,f1329]) ).
fof(f2153,plain,
r3(c,b,b),
inference(resolution,[status(thm)],[f1618,f1326]) ).
fof(f2156,plain,
! [X0] : p4(X0,d,X0),
inference(resolution,[status(thm)],[f2136,f852]) ).
fof(f2157,plain,
p2(e,e,d),
inference(resolution,[status(thm)],[f2138,f1248]) ).
fof(f2162,plain,
! [X0] : p4(a,X0,a),
inference(resolution,[status(thm)],[f2081,f852]) ).
fof(f2163,plain,
m3(d,d,c),
inference(resolution,[status(thm)],[f1679,f1378]) ).
fof(f2164,plain,
k3(b,b,a),
inference(resolution,[status(thm)],[f2098,f1691]) ).
fof(f2169,plain,
! [X0,X1] :
( ~ m0(b,X0,c)
| p1(X0,X1,b) ),
inference(resolution,[status(thm)],[f2099,f538]) ).
fof(f2170,plain,
l3(e,d),
inference(resolution,[status(thm)],[f2137,f1351]) ).
fof(f2178,plain,
! [X0] : r3(e,X0,e),
inference(resolution,[status(thm)],[f2137,f820]) ).
fof(f2191,plain,
q3(b,a),
inference(resolution,[status(thm)],[f1704,f383]) ).
fof(f2192,plain,
q3(b,e),
inference(resolution,[status(thm)],[f1704,f379]) ).
fof(f2193,plain,
q3(b,d),
inference(resolution,[status(thm)],[f1704,f375]) ).
fof(f2199,plain,
q3(e,d),
inference(resolution,[status(thm)],[f1715,f371]) ).
fof(f2202,plain,
! [X0] : q4(X0,e),
inference(resolution,[status(thm)],[f1729,f2081]) ).
fof(f2210,plain,
! [X0] : q4(X0,b),
inference(resolution,[status(thm)],[f1731,f2081]) ).
fof(f2223,plain,
( ~ l1(e,c)
| p2(a,c,b) ),
inference(backward_subsumption_resolution,[status(thm)],[f1624,f1750]) ).
fof(f2224,plain,
! [X0] :
( ~ m1(d,c,X0)
| m1(X0,c,c) ),
inference(resolution,[status(thm)],[f1750,f434]) ).
fof(f2225,plain,
! [X0] :
( ~ m1(d,X0,a)
| m1(c,a,a) ),
inference(resolution,[status(thm)],[f1750,f434]) ).
fof(f2227,plain,
q1(b,b,c),
inference(resolution,[status(thm)],[f1751,f1209]) ).
fof(f2229,plain,
! [X0] :
( ~ m1(b,c,X0)
| m1(X0,c,c) ),
inference(resolution,[status(thm)],[f1751,f434]) ).
fof(f2238,plain,
q1(b,b,e),
inference(resolution,[status(thm)],[f1753,f1209]) ).
fof(f2246,plain,
! [X0] :
( ~ m1(d,e,X0)
| m1(X0,e,e) ),
inference(resolution,[status(thm)],[f1754,f434]) ).
fof(f2252,plain,
! [X0] :
( ~ m1(d,b,X0)
| m1(X0,b,b) ),
inference(resolution,[status(thm)],[f1756,f434]) ).
fof(f2257,plain,
q1(b,b,a),
inference(resolution,[status(thm)],[f1757,f1209]) ).
fof(f2259,plain,
! [X0] :
( ~ m1(b,a,X0)
| m1(X0,a,a) ),
inference(resolution,[status(thm)],[f1757,f434]) ).
fof(f2264,plain,
! [X0] :
( ~ m1(d,a,X0)
| m1(X0,a,a) ),
inference(resolution,[status(thm)],[f1758,f434]) ).
fof(f2267,plain,
( ~ p2(e,d,d)
| q3(d,d) ),
inference(resolution,[status(thm)],[f2199,f802]) ).
fof(f2268,plain,
q3(d,d),
inference(forward_subsumption_resolution,[status(thm)],[f2267,f2137]) ).
fof(f2270,plain,
! [X0] :
( ~ m1(a,b,X0)
| m1(X0,b,b) ),
inference(resolution,[status(thm)],[f1759,f434]) ).
fof(f2277,plain,
k2(e,c),
inference(resolution,[status(thm)],[f1777,f1470]) ).
fof(f2279,plain,
k2(b,c),
inference(resolution,[status(thm)],[f1777,f993]) ).
fof(f2282,plain,
k2(a,e),
inference(resolution,[status(thm)],[f1779,f1500]) ).
fof(f2283,plain,
k2(c,e),
inference(resolution,[status(thm)],[f1779,f1499]) ).
fof(f2286,plain,
k2(b,e),
inference(resolution,[status(thm)],[f1779,f993]) ).
fof(f2289,plain,
k2(a,b),
inference(resolution,[status(thm)],[f1780,f1498]) ).
fof(f2290,plain,
k2(c,b),
inference(resolution,[status(thm)],[f1780,f1497]) ).
fof(f2292,plain,
k2(e,b),
inference(resolution,[status(thm)],[f1780,f1470]) ).
fof(f2299,plain,
! [X0] : k2(X0,d),
inference(resolution,[status(thm)],[f1782,f945]) ).
fof(f2306,plain,
! [X0] :
( ~ r2(X0)
| m3(X0,d,X0) ),
inference(resolution,[status(thm)],[f2299,f767]) ).
fof(f2307,plain,
! [X0] : p3(d,X0,d),
inference(resolution,[status(thm)],[f2299,f1384]) ).
fof(f2308,plain,
! [X0,X1,X2,X3] :
( ~ k3(X1,X3,d)
| ~ q0(X2,X1)
| k3(X0,X0,X1) ),
inference(resolution,[status(thm)],[f2299,f723]) ).
fof(f2309,plain,
! [X0] : k3(d,d,X0),
inference(resolution,[status(thm)],[f2299,f710]) ).
fof(f2310,plain,
k2(b,a),
inference(resolution,[status(thm)],[f1783,f1760]) ).
fof(f2312,plain,
k2(c,a),
inference(resolution,[status(thm)],[f1783,f1750]) ).
fof(f2314,plain,
k2(e,a),
inference(resolution,[status(thm)],[f1783,f1470]) ).
fof(f2318,plain,
s2(a),
inference(resolution,[status(thm)],[f1822,f1325]) ).
fof(f2319,plain,
! [X0] :
( ~ k3(X0,X0,b)
| q4(b,a) ),
inference(resolution,[status(thm)],[f1822,f1431]) ).
fof(f2320,plain,
( ~ n0(b,a)
| q3(a,b) ),
inference(resolution,[status(thm)],[f1822,f801]) ).
fof(f2322,plain,
q3(a,b),
inference(forward_subsumption_resolution,[status(thm)],[f2320,f405]) ).
fof(f2323,plain,
s2(c),
inference(resolution,[status(thm)],[f1823,f1325]) ).
fof(f2324,plain,
! [X0] :
( ~ k3(X0,X0,b)
| q4(b,c) ),
inference(resolution,[status(thm)],[f1823,f1431]) ).
fof(f2325,plain,
( ~ n0(b,c)
| q3(c,b) ),
inference(resolution,[status(thm)],[f1823,f801]) ).
fof(f2327,plain,
r3(c,a,a),
inference(resolution,[status(thm)],[f2318,f1618]) ).
fof(f2328,plain,
r3(e,a,a),
inference(resolution,[status(thm)],[f2318,f1630]) ).
fof(f2329,plain,
r3(b,a,a),
inference(resolution,[status(thm)],[f2318,f1625]) ).
fof(f2330,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| ~ q2(X1,a,X1)
| s3(a,X0) ),
inference(resolution,[status(thm)],[f2318,f830]) ).
fof(f2331,plain,
! [X0,X1] :
( ~ q3(X0,a)
| ~ n1(X1,a,X0)
| q3(a,X0) ),
inference(resolution,[status(thm)],[f2318,f804]) ).
fof(f2338,plain,
! [X0] :
( ~ q2(X0,c,c)
| m3(X0,c,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f774,f2323]) ).
fof(f2340,plain,
r3(e,c,c),
inference(resolution,[status(thm)],[f2323,f1630]) ).
fof(f2341,plain,
r3(b,c,c),
inference(resolution,[status(thm)],[f2323,f1625]) ).
fof(f2342,plain,
! [X0,X1,X2] :
( ~ m0(X1,X2,X0)
| ~ q2(X1,c,X1)
| s3(c,X0) ),
inference(resolution,[status(thm)],[f2323,f830]) ).
fof(f2343,plain,
! [X0,X1] :
( ~ q3(X0,c)
| ~ n1(X1,c,X0)
| q3(c,X0) ),
inference(resolution,[status(thm)],[f2323,f804]) ).
fof(f2347,plain,
! [X0] :
( ~ k3(X0,X0,e)
| q4(e,c) ),
inference(resolution,[status(thm)],[f1850,f1431]) ).
fof(f2348,plain,
( ~ n0(e,c)
| q3(c,e) ),
inference(resolution,[status(thm)],[f1850,f801]) ).
fof(f2351,plain,
( ~ n0(b,c)
| q3(c,e) ),
inference(resolution,[status(thm)],[f1851,f801]) ).
fof(f2354,plain,
( ~ n0(e,c)
| q3(c,b) ),
inference(resolution,[status(thm)],[f1853,f801]) ).
fof(f2361,plain,
m3(c,b,d),
inference(backward_subsumption_resolution,[status(thm)],[f2001,f1857]) ).
fof(f2367,plain,
! [X0] :
( ~ r3(c,X0,X0)
| r3(X0,e,c) ),
inference(resolution,[status(thm)],[f2277,f1415]) ).
fof(f2368,plain,
p3(d,e,c),
inference(resolution,[status(thm)],[f2277,f1384]) ).
fof(f2374,plain,
! [X0] :
( ~ r3(c,X0,X0)
| r3(X0,b,c) ),
inference(resolution,[status(thm)],[f2279,f1415]) ).
fof(f2375,plain,
p3(d,b,c),
inference(resolution,[status(thm)],[f2279,f1384]) ).
fof(f2379,plain,
( ~ n0(d,c)
| q3(c,d) ),
inference(resolution,[status(thm)],[f1858,f801]) ).
fof(f2382,plain,
q3(c,d),
inference(forward_subsumption_resolution,[status(thm)],[f2379,f394]) ).
fof(f2383,plain,
! [X0] :
( ~ k3(X0,X0,a)
| q4(a,c) ),
inference(resolution,[status(thm)],[f1869,f1431]) ).
fof(f2384,plain,
( ~ n0(e,c)
| q3(c,a) ),
inference(resolution,[status(thm)],[f1869,f801]) ).
fof(f2387,plain,
p3(d,a,e),
inference(resolution,[status(thm)],[f2282,f1384]) ).
fof(f2389,plain,
k3(e,e,a),
inference(resolution,[status(thm)],[f2282,f710]) ).
fof(f2391,plain,
( ~ n0(b,c)
| q3(c,a) ),
inference(resolution,[status(thm)],[f1870,f801]) ).
fof(f2394,plain,
( ~ n0(a,c)
| q3(c,a) ),
inference(resolution,[status(thm)],[f1871,f801]) ).
fof(f2397,plain,
! [X0] :
( ~ r2(X0)
| m3(X0,e,X0) ),
inference(resolution,[status(thm)],[f2283,f767]) ).
fof(f2398,plain,
p3(d,c,e),
inference(resolution,[status(thm)],[f2283,f1384]) ).
fof(f2401,plain,
! [X0] :
( ~ k3(X0,X0,e)
| q4(e,a) ),
inference(resolution,[status(thm)],[f1873,f1431]) ).
fof(f2402,plain,
( ~ n0(e,a)
| q3(a,e) ),
inference(resolution,[status(thm)],[f1873,f801]) ).
fof(f2405,plain,
p3(d,b,e),
inference(resolution,[status(thm)],[f2286,f1384]) ).
fof(f2408,plain,
! [X0] : m3(e,X0,e),
inference(resolution,[status(thm)],[f1881,f387]) ).
fof(f2409,plain,
! [X0] : m3(b,X0,b),
inference(resolution,[status(thm)],[f1882,f406]) ).
fof(f2412,plain,
p3(d,a,b),
inference(resolution,[status(thm)],[f2289,f1384]) ).
fof(f2415,plain,
! [X0] : m3(a,X0,a),
inference(resolution,[status(thm)],[f1883,f380]) ).
fof(f2416,plain,
! [X0] : m3(d,X0,d),
inference(resolution,[status(thm)],[f1883,f387]) ).
fof(f2417,plain,
p3(b,c,b),
inference(backward_subsumption_resolution,[status(thm)],[f798,f2290]) ).
fof(f2419,plain,
! [X0] :
( ~ r2(X0)
| m3(X0,b,X0) ),
inference(resolution,[status(thm)],[f2290,f767]) ).
fof(f2420,plain,
p3(d,c,b),
inference(resolution,[status(thm)],[f2290,f1384]) ).
fof(f2424,plain,
p3(d,e,b),
inference(resolution,[status(thm)],[f2292,f1384]) ).
fof(f2428,plain,
q3(d,b),
inference(resolution,[status(thm)],[f1908,f2193]) ).
fof(f2429,plain,
q3(d,e),
inference(resolution,[status(thm)],[f1908,f2199]) ).
fof(f2434,plain,
! [X0] : s3(d,X0),
inference(resolution,[status(thm)],[f1912,f387]) ).
fof(f2438,plain,
! [X0] :
( ~ r3(a,X0,X0)
| r3(X0,b,a) ),
inference(resolution,[status(thm)],[f2310,f1414]) ).
fof(f2439,plain,
p3(d,b,a),
inference(resolution,[status(thm)],[f2310,f1384]) ).
fof(f2442,plain,
p2(b,c,c),
inference(backward_subsumption_resolution,[status(thm)],[f1594,f1979]) ).
fof(f2445,plain,
! [X0] :
( ~ m0(e,b,b)
| p1(b,X0,e) ),
inference(resolution,[status(thm)],[f1979,f538]) ).
fof(f2446,plain,
p2(b,c,a),
inference(backward_subsumption_resolution,[status(thm)],[f1530,f2312]) ).
fof(f2448,plain,
! [X0] :
( ~ r2(X0)
| m3(X0,a,X0) ),
inference(resolution,[status(thm)],[f2312,f767]) ).
fof(f2449,plain,
! [X0] :
( ~ r3(a,X0,X0)
| r3(X0,c,a) ),
inference(resolution,[status(thm)],[f2312,f1414]) ).
fof(f2450,plain,
p3(d,c,a),
inference(resolution,[status(thm)],[f2312,f1384]) ).
fof(f2458,plain,
l3(b,c),
inference(resolution,[status(thm)],[f1985,f1352]) ).
fof(f2459,plain,
p3(b,c,c),
inference(resolution,[status(thm)],[f1985,f1749]) ).
fof(f2464,plain,
! [X0] :
( ~ r3(a,X0,X0)
| r3(X0,e,a) ),
inference(resolution,[status(thm)],[f2314,f1414]) ).
fof(f2465,plain,
p3(d,e,a),
inference(resolution,[status(thm)],[f2314,f1384]) ).
fof(f2468,plain,
m1(a,b,b),
inference(resolution,[status(thm)],[f1990,f1759]) ).
fof(f2469,plain,
l3(e,c),
inference(resolution,[status(thm)],[f1991,f1351]) ).
fof(f2476,plain,
! [X0,X1] :
( ~ k2(X0,X1)
| p3(e,X0,X1) ),
inference(resolution,[status(thm)],[f2000,f780]) ).
fof(f2477,plain,
! [X0] :
( ~ k3(X0,X0,e)
| q4(e,d) ),
inference(resolution,[status(thm)],[f2000,f1431]) ).
fof(f2485,plain,
p2(e,e,c),
inference(resolution,[status(thm)],[f2006,f1248]) ).
fof(f2487,plain,
! [X0] :
( ~ m0(e,c,e)
| p1(c,X0,e) ),
inference(resolution,[status(thm)],[f2006,f538]) ).
fof(f2488,plain,
q3(d,c),
inference(resolution,[status(thm)],[f2382,f1908]) ).
fof(f2491,plain,
p2(e,e,b),
inference(resolution,[status(thm)],[f2009,f1248]) ).
fof(f2493,plain,
! [X0] :
( ~ m0(e,b,e)
| p1(b,X0,e) ),
inference(resolution,[status(thm)],[f2009,f538]) ).
fof(f2503,plain,
! [X0,X1] :
( ~ p2(X0,X1,d)
| p3(X0,X1,X1) ),
inference(resolution,[status(thm)],[f2150,f795]) ).
fof(f2504,plain,
! [X0] :
( ~ p2(X0,d,a)
| p3(X0,d,d) ),
inference(resolution,[status(thm)],[f2072,f795]) ).
fof(f2513,plain,
r3(b,c,b),
inference(resolution,[status(thm)],[f2442,f820]) ).
fof(f2517,plain,
! [X0] : p4(d,X0,d),
inference(resolution,[status(thm)],[f2309,f852]) ).
fof(f2527,plain,
! [X0] : s3(e,X0),
inference(resolution,[status(thm)],[f1722,f387]) ).
fof(f2534,plain,
! [X0] :
( ~ q3(X0,e)
| q3(e,X0) ),
inference(resolution,[status(thm)],[f1720,f1547]) ).
fof(f2536,plain,
r3(e,e,b),
inference(resolution,[status(thm)],[f1723,f2408]) ).
fof(f2537,plain,
r3(d,d,b),
inference(resolution,[status(thm)],[f1723,f2361]) ).
fof(f2542,plain,
! [X0] :
( ~ p2(X0,c,a)
| p3(X0,c,c) ),
inference(resolution,[status(thm)],[f1886,f795]) ).
fof(f2548,plain,
r3(a,a,b),
inference(resolution,[status(thm)],[f2415,f1723]) ).
fof(f2549,plain,
p4(c,c,a),
inference(resolution,[status(thm)],[f2415,f1427]) ).
fof(f2571,plain,
r3(a,a,d),
inference(resolution,[status(thm)],[f2147,f2415]) ).
fof(f2572,plain,
r3(b,b,d),
inference(resolution,[status(thm)],[f2147,f2409]) ).
fof(f2573,plain,
r3(e,e,d),
inference(resolution,[status(thm)],[f2147,f2408]) ).
fof(f2580,plain,
r3(d,c,c),
inference(resolution,[status(thm)],[f2152,f1911]) ).
fof(f2582,plain,
! [X0] :
( ~ p2(X0,d,c)
| p3(X0,d,d) ),
inference(resolution,[status(thm)],[f2163,f795]) ).
fof(f2584,plain,
m1(c,a,a),
inference(resolution,[status(thm)],[f2225,f1758]) ).
fof(f2594,plain,
m1(e,a,a),
inference(resolution,[status(thm)],[f2259,f2135]) ).
fof(f2597,plain,
q5(c,d),
inference(resolution,[status(thm)],[f1932,f1564]) ).
fof(f2598,plain,
q5(c,b),
inference(resolution,[status(thm)],[f1932,f1099]) ).
fof(f2603,plain,
q4(b,a),
inference(resolution,[status(thm)],[f2319,f2309]) ).
fof(f2609,plain,
q4(b,c),
inference(resolution,[status(thm)],[f2324,f2309]) ).
fof(f2615,plain,
q4(e,c),
inference(resolution,[status(thm)],[f2347,f2309]) ).
fof(f2619,plain,
q4(a,c),
inference(resolution,[status(thm)],[f2383,f2309]) ).
fof(f2623,plain,
q4(e,a),
inference(resolution,[status(thm)],[f2401,f2309]) ).
fof(f2631,plain,
n4(b,c),
inference(resolution,[status(thm)],[f2459,f2061]) ).
fof(f2635,plain,
q1(a,a,b),
inference(resolution,[status(thm)],[f2468,f1209]) ).
fof(f2641,plain,
p3(e,c,a),
inference(resolution,[status(thm)],[f2476,f2312]) ).
fof(f2642,plain,
p3(e,c,b),
inference(resolution,[status(thm)],[f2476,f2290]) ).
fof(f2643,plain,
p3(e,c,e),
inference(resolution,[status(thm)],[f2476,f2283]) ).
fof(f2644,plain,
p3(e,a,b),
inference(resolution,[status(thm)],[f2476,f2289]) ).
fof(f2645,plain,
p3(e,a,e),
inference(resolution,[status(thm)],[f2476,f2282]) ).
fof(f2646,plain,
p3(e,b,a),
inference(resolution,[status(thm)],[f2476,f2310]) ).
fof(f2648,plain,
p3(e,b,c),
inference(resolution,[status(thm)],[f2476,f2279]) ).
fof(f2649,plain,
p3(e,e,a),
inference(resolution,[status(thm)],[f2476,f2314]) ).
fof(f2650,plain,
p3(e,e,b),
inference(resolution,[status(thm)],[f2476,f2292]) ).
fof(f2651,plain,
p3(e,e,c),
inference(resolution,[status(thm)],[f2476,f2277]) ).
fof(f2652,plain,
! [X0] : p3(e,X0,d),
inference(resolution,[status(thm)],[f2476,f2299]) ).
fof(f2653,plain,
! [X0] : p3(e,X0,X0),
inference(resolution,[status(thm)],[f2476,f1227]) ).
fof(f2654,plain,
q4(e,d),
inference(resolution,[status(thm)],[f2477,f2309]) ).
fof(f2667,plain,
! [X0] : q4(d,X0),
inference(forward_subsumption_resolution,[status(thm)],[f2023,f2136]) ).
fof(f2669,plain,
! [X0] :
( ~ n1(X0,d,X0)
| q2(d,X0,d) ),
inference(forward_subsumption_resolution,[status(thm)],[f2025,f2101]) ).
fof(f2670,plain,
q2(d,a,d),
inference(resolution,[status(thm)],[f2669,f1380]) ).
fof(f2673,plain,
r3(c,c,d),
inference(resolution,[status(thm)],[f2038,f2147]) ).
fof(f2674,plain,
r3(c,c,b),
inference(resolution,[status(thm)],[f2038,f1723]) ).
fof(f2679,plain,
! [X0] : p1(e,X0,d),
inference(resolution,[status(thm)],[f2139,f403]) ).
fof(f2682,plain,
p4(b,a,b),
inference(resolution,[status(thm)],[f2164,f852]) ).
fof(f2683,plain,
! [X0] : n4(e,X0),
inference(resolution,[status(thm)],[f2653,f2061]) ).
fof(f2686,plain,
m3(c,d,c),
inference(resolution,[status(thm)],[f2306,f1321]) ).
fof(f2694,plain,
! [X0,X1,X2] :
( ~ q0(X2,X1)
| k3(X0,X0,X1) ),
inference(resolution,[status(thm)],[f2308,f2136]) ).
fof(f2696,plain,
r3(a,c,c),
inference(resolution,[status(thm)],[f2327,f1911]) ).
fof(f2697,plain,
! [X0,X1] :
( ~ m0(b,X1,X0)
| s3(a,X0) ),
inference(resolution,[status(thm)],[f2330,f1822]) ).
fof(f2706,plain,
! [X0] :
( ~ q3(X0,a)
| q3(a,X0) ),
inference(resolution,[status(thm)],[f2331,f1547]) ).
fof(f2708,plain,
! [X0,X1] :
( ~ m0(a,X1,X0)
| s3(c,X0) ),
inference(resolution,[status(thm)],[f2342,f1871]) ).
fof(f2720,plain,
! [X0] :
( ~ q3(X0,c)
| q3(c,X0) ),
inference(resolution,[status(thm)],[f2343,f1547]) ).
fof(f2724,plain,
! [X0,X1] :
( ~ m0(e,X0,d)
| p1(X0,X1,e) ),
inference(resolution,[status(thm)],[f2679,f538]) ).
fof(f2725,plain,
r3(a,e,c),
inference(resolution,[status(thm)],[f2367,f2327]) ).
fof(f2726,plain,
r3(b,e,c),
inference(resolution,[status(thm)],[f2367,f2153]) ).
fof(f2727,plain,
r3(d,e,c),
inference(resolution,[status(thm)],[f2367,f2152]) ).
fof(f2728,plain,
r3(e,e,c),
inference(resolution,[status(thm)],[f2367,f2151]) ).
fof(f2747,plain,
! [X0] : k5(X0),
inference(resolution,[status(thm)],[f1934,f1406]) ).
fof(f2756,plain,
r3(a,b,c),
inference(resolution,[status(thm)],[f2374,f2327]) ).
fof(f2757,plain,
r3(b,b,c),
inference(resolution,[status(thm)],[f2374,f2153]) ).
fof(f2758,plain,
r3(d,b,c),
inference(resolution,[status(thm)],[f2374,f2152]) ).
fof(f2759,plain,
r3(e,b,c),
inference(resolution,[status(thm)],[f2374,f2151]) ).
fof(f2767,plain,
p4(e,a,e),
inference(resolution,[status(thm)],[f2389,f852]) ).
fof(f2769,plain,
m3(c,e,c),
inference(resolution,[status(thm)],[f2397,f1321]) ).
fof(f2789,plain,
m3(c,b,c),
inference(resolution,[status(thm)],[f2419,f1321]) ).
fof(f2818,plain,
m3(c,a,c),
inference(resolution,[status(thm)],[f2448,f1321]) ).
fof(f2819,plain,
r3(a,c,a),
inference(resolution,[status(thm)],[f2449,f1820]) ).
fof(f2830,plain,
q5(e,d),
inference(resolution,[status(thm)],[f1946,f1564]) ).
fof(f2831,plain,
q5(e,b),
inference(resolution,[status(thm)],[f1946,f1099]) ).
fof(f2850,plain,
p4(b,e,e),
inference(resolution,[status(thm)],[f2536,f1426]) ).
fof(f2852,plain,
p4(b,d,d),
inference(resolution,[status(thm)],[f2537,f1426]) ).
fof(f2853,plain,
q5(b,d),
inference(resolution,[status(thm)],[f1956,f1564]) ).
fof(f2856,plain,
p4(b,a,a),
inference(resolution,[status(thm)],[f2548,f1426]) ).
fof(f2858,plain,
q5(d,b),
inference(resolution,[status(thm)],[f1963,f1099]) ).
fof(f2860,plain,
p4(d,a,a),
inference(resolution,[status(thm)],[f2571,f1426]) ).
fof(f2861,plain,
p4(d,b,b),
inference(resolution,[status(thm)],[f2572,f1426]) ).
fof(f2863,plain,
p4(d,e,e),
inference(resolution,[status(thm)],[f2573,f1426]) ).
fof(f2865,plain,
q5(a,d),
inference(resolution,[status(thm)],[f1975,f1564]) ).
fof(f2866,plain,
q5(a,b),
inference(resolution,[status(thm)],[f1975,f1099]) ).
fof(f2869,plain,
q1(c,c,a),
inference(resolution,[status(thm)],[f2584,f1209]) ).
fof(f2871,plain,
! [X0] :
( ~ m1(c,a,X0)
| m1(X0,a,a) ),
inference(resolution,[status(thm)],[f2584,f434]) ).
fof(f2876,plain,
q1(e,e,a),
inference(resolution,[status(thm)],[f2594,f1209]) ).
fof(f2878,plain,
! [X0] :
( ~ m1(e,a,X0)
| m1(X0,a,a) ),
inference(resolution,[status(thm)],[f2594,f434]) ).
fof(f2882,plain,
q1(c,a,a),
inference(resolution,[status(thm)],[f2635,f1590]) ).
fof(f2886,plain,
( ~ q3(b,b)
| k4(e) ),
inference(resolution,[status(thm)],[f1846,f2635]) ).
fof(f2890,plain,
k4(e),
inference(forward_subsumption_resolution,[status(thm)],[f2886,f1901]) ).
fof(f2898,plain,
( ~ n0(d,a)
| q3(a,d) ),
inference(resolution,[status(thm)],[f2670,f801]) ).
fof(f2900,plain,
p4(d,c,c),
inference(resolution,[status(thm)],[f2673,f1426]) ).
fof(f2901,plain,
p4(b,c,c),
inference(resolution,[status(thm)],[f2674,f1426]) ).
fof(f2903,plain,
r3(c,e,a),
inference(resolution,[status(thm)],[f2696,f2464]) ).
fof(f2904,plain,
r3(c,c,a),
inference(resolution,[status(thm)],[f2696,f2449]) ).
fof(f2905,plain,
r3(c,b,a),
inference(resolution,[status(thm)],[f2696,f2438]) ).
fof(f2907,plain,
! [X0] : k3(X0,X0,b),
inference(resolution,[status(thm)],[f2694,f404]) ).
fof(f2908,plain,
! [X0] : k3(X0,X0,c),
inference(resolution,[status(thm)],[f2694,f401]) ).
fof(f2910,plain,
! [X0] : k3(X0,X0,e),
inference(resolution,[status(thm)],[f2694,f389]) ).
fof(f2915,plain,
! [X0] : s3(a,X0),
inference(resolution,[status(thm)],[f2697,f387]) ).
fof(f2916,plain,
! [X0,X1,X2] :
( ~ l2(X2,X1)
| m4(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f840,f2915]) ).
fof(f2917,plain,
! [X0] : m4(X0,e),
inference(resolution,[status(thm)],[f2916,f1617]) ).
fof(f2919,plain,
! [X0,X1] : m4(X0,X1),
inference(resolution,[status(thm)],[f2916,f1611]) ).
fof(f2920,plain,
! [X0] :
( ~ s4(X0)
| m5(X0,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f883,f2917]) ).
fof(f2922,plain,
! [X0,X1,X2] :
( ~ l2(X0,X2)
| p5(X0,X1,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2119,f2919]) ).
fof(f2923,plain,
m5(a,a),
inference(resolution,[status(thm)],[f2920,f1940]) ).
fof(f2924,plain,
m5(d,d),
inference(resolution,[status(thm)],[f2920,f1938]) ).
fof(f2928,plain,
! [X0,X1] : p5(X0,X1,X1),
inference(resolution,[status(thm)],[f2922,f1617]) ).
fof(f2935,plain,
! [X0] : p4(X0,b,X0),
inference(resolution,[status(thm)],[f2907,f852]) ).
fof(f2940,plain,
! [X0] : p4(X0,c,X0),
inference(resolution,[status(thm)],[f2908,f852]) ).
fof(f2945,plain,
! [X0] : s3(c,X0),
inference(resolution,[status(thm)],[f2708,f387]) ).
fof(f2950,plain,
! [X0] : p4(X0,e,X0),
inference(resolution,[status(thm)],[f2910,f852]) ).
fof(f2953,plain,
p4(c,e,e),
inference(resolution,[status(thm)],[f2728,f1426]) ).
fof(f2954,plain,
p4(c,b,b),
inference(resolution,[status(thm)],[f2757,f1426]) ).
fof(f2964,plain,
p4(a,c,c),
inference(resolution,[status(thm)],[f2904,f1426]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN720-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.73 % Computer : n006.cluster.edu
% 0.08/0.73 % Model : x86_64 x86_64
% 0.08/0.73 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.73 % Memory : 8046.5625MB
% 0.08/0.73 % OS : Linux 6.8.0-71-generic
% 0.08/0.73 % CPULimit : 300
% 0.08/0.73 % WCLimit : 300
% 0.08/0.73 % DateTime : Mon Sep 21 11:13:01 UTC 2026
% 0.08/0.73 % CPUTime :
% 0.08/0.75 % Drodi V4.1.1
% 0.13/0.82 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.13/0.82 % SZS output start Saturation for theBenchmark
% See solution above
% 1.56/2.05 % Elapsed time: 1.098298 seconds
% 1.56/2.05 % CPU time: 0.551754 seconds
% 1.56/2.05 % Total memory used: 25.590 MB
% 1.56/2.05 % Net memory used: 24.634 MB
%------------------------------------------------------------------------------