%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN067-3 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:15:07 PM UTC 2026
% Result : Unsatisfiable 0.09s 5.98s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 80
% Syntax : Number of formulae : 298 ( 4 unt; 43 def)
% Number of atoms : 1245 ( 0 equ)
% Maximal formula atoms : 7 ( 4 avg)
% Number of connectives : 1647 ( 700 ~; 904 |; 0 &)
% ( 43 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 46 ( 45 usr; 44 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-1 aty)
% Number of variables : 356 ( 356 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [A,B] :
( ~ big_p(a)
| big_p(sk3(A))
| big_p(sk1(B))
| big_p(B)
| big_p(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
! [C,D] :
( ~ big_p(a)
| big_r(C,sk4(C))
| big_p(sk1(D))
| big_p(D)
| big_p(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
! [E,F] :
( ~ big_p(a)
| big_r(sk4(E),sk3(E))
| big_p(sk1(F))
| big_p(F)
| big_p(E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
! [G,H] :
( ~ big_p(a)
| big_r(H,sk2(H))
| big_p(sk3(G))
| big_p(H)
| big_p(G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
! [I,J] :
( ~ big_p(a)
| big_r(J,sk2(J))
| big_r(I,sk4(I))
| big_p(J)
| big_p(I) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
! [K,L] :
( ~ big_p(a)
| big_r(sk4(K),sk3(K))
| big_r(L,sk2(L))
| big_p(L)
| big_p(K) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
! [E1,F1] :
( ~ big_p(a)
| big_r(sk2(F1),sk1(F1))
| big_p(sk3(E1))
| big_p(F1)
| big_p(E1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
! [G1,H1] :
( ~ big_p(a)
| big_r(sk2(H1),sk1(H1))
| big_r(G1,sk4(G1))
| big_p(H1)
| big_p(G1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
! [I1,J1] :
( ~ big_p(a)
| big_r(sk4(I1),sk3(I1))
| big_r(sk2(J1),sk1(J1))
| big_p(J1)
| big_p(I1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
! [K1,L1,M1] :
( ~ big_r(L1,M1)
| ~ big_p(a)
| ~ big_p(M1)
| big_p(sk3(K1))
| big_p(sk1(L1))
| big_p(K1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
! [N1,O1,P1] :
( ~ big_r(O1,P1)
| ~ big_p(a)
| ~ big_p(P1)
| big_r(O1,sk2(O1))
| big_p(sk3(N1))
| big_p(N1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
! [Q1,R1,S1] :
( ~ big_r(R1,S1)
| ~ big_p(a)
| ~ big_p(S1)
| big_r(Q1,sk4(Q1))
| big_p(sk1(R1))
| big_p(Q1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
! [T1,U1,V1] :
( ~ big_r(U1,V1)
| ~ big_p(a)
| ~ big_p(V1)
| big_r(U1,sk2(U1))
| big_r(T1,sk4(T1))
| big_p(T1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
! [W1,X1,Y1] :
( ~ big_r(X1,Y1)
| ~ big_p(a)
| ~ big_p(Y1)
| big_r(sk2(X1),sk1(X1))
| big_p(sk3(W1))
| big_p(W1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
! [Z1,A2,B2] :
( ~ big_r(A2,B2)
| ~ big_p(a)
| ~ big_p(B2)
| big_r(sk2(A2),sk1(A2))
| big_r(Z1,sk4(Z1))
| big_p(Z1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
! [C2,D2,E2] :
( ~ big_r(D2,E2)
| ~ big_p(a)
| ~ big_p(E2)
| big_r(sk4(C2),sk3(C2))
| big_p(sk1(D2))
| big_p(C2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
! [F2,G2,H2] :
( ~ big_r(G2,H2)
| ~ big_p(a)
| ~ big_p(H2)
| big_r(sk4(F2),sk3(F2))
| big_r(G2,sk2(G2))
| big_p(F2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
! [I2,J2,K2] :
( ~ big_r(J2,K2)
| ~ big_p(a)
| ~ big_p(K2)
| big_r(sk4(I2),sk3(I2))
| big_r(sk2(J2),sk1(J2))
| big_p(I2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,negated_conjecture,
! [U2,V2,W2,X2] :
( ~ big_r(U2,X2)
| ~ big_r(V2,W2)
| ~ big_p(a)
| ~ big_p(X2)
| ~ big_p(W2)
| big_p(sk5(V2))
| big_p(sk1(U2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
! [Y2,Z2,A3,B3] :
( ~ big_r(Z2,B3)
| ~ big_r(Y2,A3)
| ~ big_p(a)
| ~ big_p(B3)
| ~ big_p(A3)
| big_r(Z2,sk2(Z2))
| big_p(sk5(Y2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
! [C3,D3,E3,F3] :
( ~ big_r(C3,F3)
| ~ big_r(D3,E3)
| ~ big_p(a)
| ~ big_p(F3)
| ~ big_p(E3)
| big_r(D3,sk6(D3))
| big_p(sk1(C3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
! [G3,H3,I3,J3] :
( ~ big_r(H3,J3)
| ~ big_r(G3,I3)
| ~ big_p(a)
| ~ big_p(J3)
| ~ big_p(I3)
| big_r(H3,sk2(H3))
| big_r(G3,sk6(G3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
! [K3,L3,M3,N3] :
( ~ big_r(L3,N3)
| ~ big_r(K3,M3)
| ~ big_p(a)
| ~ big_p(N3)
| ~ big_p(M3)
| big_r(sk2(L3),sk1(L3))
| big_p(sk5(K3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,negated_conjecture,
! [O3,P3,Q3,R3] :
( ~ big_r(P3,R3)
| ~ big_r(O3,Q3)
| ~ big_p(a)
| ~ big_p(R3)
| ~ big_p(Q3)
| big_r(sk2(P3),sk1(P3))
| big_r(O3,sk6(O3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
! [S3,T3,U3,V3] :
( ~ big_r(S3,V3)
| ~ big_r(T3,U3)
| ~ big_p(a)
| ~ big_p(V3)
| ~ big_p(U3)
| big_r(sk6(T3),sk5(T3))
| big_p(sk1(S3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,negated_conjecture,
! [W3,X3,Y3,Z3] :
( ~ big_r(W3,Z3)
| ~ big_r(X3,Y3)
| ~ big_p(a)
| ~ big_p(Z3)
| ~ big_p(Y3)
| big_r(sk6(X3),sk5(X3))
| big_r(W3,sk2(W3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
! [A4,B4,C4,D4] :
( ~ big_r(A4,D4)
| ~ big_r(B4,C4)
| ~ big_p(a)
| ~ big_p(D4)
| ~ big_p(C4)
| big_r(sk6(B4),sk5(B4))
| big_r(sk2(A4),sk1(A4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,negated_conjecture,
big_p(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_p(sk8)
| big_p(sk10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk9,sk10)
| big_p(sk8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk7,sk8)
| big_p(sk10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk9,sk10)
| big_r(sk7,sk8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
! [E4,F4] :
( ~ big_r(sk9,F4)
| ~ big_r(F4,E4)
| ~ big_p(sk7)
| ~ big_p(E4)
| big_p(sk8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
! [G4,H4] :
( ~ big_r(sk9,H4)
| ~ big_r(H4,G4)
| ~ big_p(sk7)
| ~ big_p(G4)
| big_r(sk7,sk8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,negated_conjecture,
! [I4,J4] :
( ~ big_r(sk7,J4)
| ~ big_r(J4,I4)
| ~ big_p(sk9)
| ~ big_p(I4)
| big_p(sk10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
! [K4,L4] :
( ~ big_r(sk7,L4)
| ~ big_r(L4,K4)
| ~ big_p(sk9)
| ~ big_p(K4)
| big_r(sk9,sk10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
! [M4,N4,O4,P4] :
( ~ big_r(sk9,O4)
| ~ big_r(sk7,P4)
| ~ big_r(P4,N4)
| ~ big_r(O4,M4)
| ~ big_p(N4)
| ~ big_p(M4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,plain,
( ~ big_p(a)
| ! [A] :
( big_p(sk3(A))
| ! [B] :
( big_p(sk1(B))
| big_p(B)
| big_p(A) ) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f48,plain,
! [X0,X1] :
( ~ big_p(a)
| big_p(sk3(X0))
| big_p(sk1(X1))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
( ~ big_p(a)
| ! [C] :
( big_r(C,sk4(C))
| ! [D] :
( big_p(sk1(D))
| big_p(D)
| big_p(C) ) ) ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f50,plain,
! [X0,X1] :
( ~ big_p(a)
| big_r(X0,sk4(X0))
| big_p(sk1(X1))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
( ~ big_p(a)
| ! [E] :
( big_r(sk4(E),sk3(E))
| ! [F] :
( big_p(sk1(F))
| big_p(F)
| big_p(E) ) ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f52,plain,
! [X0,X1] :
( ~ big_p(a)
| big_r(sk4(X0),sk3(X0))
| big_p(sk1(X1))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f53,plain,
( ~ big_p(a)
| ! [H] :
( big_r(H,sk2(H))
| ! [G] :
( big_p(sk3(G))
| big_p(H)
| big_p(G) ) ) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f54,plain,
! [X0,X1] :
( ~ big_p(a)
| big_r(X1,sk2(X1))
| big_p(sk3(X0))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f55,plain,
( ~ big_p(a)
| ! [J] :
( big_r(J,sk2(J))
| ! [I] :
( big_r(I,sk4(I))
| big_p(J)
| big_p(I) ) ) ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f56,plain,
! [X0,X1] :
( ~ big_p(a)
| big_r(X1,sk2(X1))
| big_r(X0,sk4(X0))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
( ~ big_p(a)
| ! [K] :
( big_r(sk4(K),sk3(K))
| ! [L] :
( big_r(L,sk2(L))
| big_p(L)
| big_p(K) ) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f58,plain,
! [X0,X1] :
( ~ big_p(a)
| big_r(sk4(X0),sk3(X0))
| big_r(X1,sk2(X1))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f71,plain,
( ~ big_p(a)
| ! [F1] :
( big_r(sk2(F1),sk1(F1))
| ! [E1] :
( big_p(sk3(E1))
| big_p(F1)
| big_p(E1) ) ) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f72,plain,
! [X0,X1] :
( ~ big_p(a)
| big_r(sk2(X1),sk1(X1))
| big_p(sk3(X0))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
( ~ big_p(a)
| ! [H1] :
( big_r(sk2(H1),sk1(H1))
| ! [G1] :
( big_r(G1,sk4(G1))
| big_p(H1)
| big_p(G1) ) ) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f74,plain,
! [X0,X1] :
( ~ big_p(a)
| big_r(sk2(X1),sk1(X1))
| big_r(X0,sk4(X0))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f75,plain,
( ~ big_p(a)
| ! [I1] :
( big_r(sk4(I1),sk3(I1))
| ! [J1] :
( big_r(sk2(J1),sk1(J1))
| big_p(J1)
| big_p(I1) ) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f76,plain,
! [X0,X1] :
( ~ big_p(a)
| big_r(sk4(X0),sk3(X0))
| big_r(sk2(X1),sk1(X1))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f77,plain,
! [L1,M1] :
( ~ big_r(L1,M1)
| ~ big_p(a)
| ~ big_p(M1)
| ! [K1] :
( big_p(sk3(K1))
| big_p(sk1(L1))
| big_p(K1) ) ),
inference(miniscoping,[status(thm)],[f16]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X2)
| big_p(sk3(X0))
| big_p(sk1(X1))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f79,plain,
! [O1,P1] :
( ~ big_r(O1,P1)
| ~ big_p(a)
| ~ big_p(P1)
| big_r(O1,sk2(O1))
| ! [N1] :
( big_p(sk3(N1))
| big_p(N1) ) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X2)
| big_r(X1,sk2(X1))
| big_p(sk3(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f81,plain,
! [R1,S1] :
( ~ big_r(R1,S1)
| ~ big_p(a)
| ~ big_p(S1)
| ! [Q1] :
( big_r(Q1,sk4(Q1))
| big_p(sk1(R1))
| big_p(Q1) ) ),
inference(miniscoping,[status(thm)],[f18]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X2)
| big_r(X0,sk4(X0))
| big_p(sk1(X1))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
! [U1,V1] :
( ~ big_r(U1,V1)
| ~ big_p(a)
| ~ big_p(V1)
| big_r(U1,sk2(U1))
| ! [T1] :
( big_r(T1,sk4(T1))
| big_p(T1) ) ),
inference(miniscoping,[status(thm)],[f19]) ).
fof(f84,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X2)
| big_r(X1,sk2(X1))
| big_r(X0,sk4(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f85,plain,
! [X1,Y1] :
( ~ big_r(X1,Y1)
| ~ big_p(a)
| ~ big_p(Y1)
| big_r(sk2(X1),sk1(X1))
| ! [W1] :
( big_p(sk3(W1))
| big_p(W1) ) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f86,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1))
| big_p(sk3(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f87,plain,
! [A2,B2] :
( ~ big_r(A2,B2)
| ~ big_p(a)
| ~ big_p(B2)
| big_r(sk2(A2),sk1(A2))
| ! [Z1] :
( big_r(Z1,sk4(Z1))
| big_p(Z1) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f88,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1))
| big_r(X0,sk4(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f89,plain,
! [D2,E2] :
( ~ big_r(D2,E2)
| ~ big_p(a)
| ~ big_p(E2)
| ! [C2] :
( big_r(sk4(C2),sk3(C2))
| big_p(sk1(D2))
| big_p(C2) ) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f90,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X2)
| big_r(sk4(X0),sk3(X0))
| big_p(sk1(X1))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f91,plain,
! [G2,H2] :
( ~ big_r(G2,H2)
| ~ big_p(a)
| ~ big_p(H2)
| ! [F2] :
( big_r(sk4(F2),sk3(F2))
| big_r(G2,sk2(G2))
| big_p(F2) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f92,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X2)
| big_r(sk4(X0),sk3(X0))
| big_r(X1,sk2(X1))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
! [J2,K2] :
( ~ big_r(J2,K2)
| ~ big_p(a)
| ~ big_p(K2)
| ! [I2] :
( big_r(sk4(I2),sk3(I2))
| big_r(sk2(J2),sk1(J2))
| big_p(I2) ) ),
inference(miniscoping,[status(thm)],[f24]) ).
fof(f94,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X2)
| big_r(sk4(X0),sk3(X0))
| big_r(sk2(X1),sk1(X1))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f101,plain,
! [U2,X2] :
( ~ big_r(U2,X2)
| ! [V2,W2] :
( ~ big_r(V2,W2)
| ~ big_p(a)
| ~ big_p(X2)
| ~ big_p(W2)
| big_p(sk5(V2))
| big_p(sk1(U2)) ) ),
inference(miniscoping,[status(thm)],[f28]) ).
fof(f102,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X2)
| big_p(sk5(X1))
| big_p(sk1(X0)) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
! [Z2,B3] :
( ~ big_r(Z2,B3)
| ! [Y2,A3] :
( ~ big_r(Y2,A3)
| ~ big_p(a)
| ~ big_p(B3)
| ~ big_p(A3)
| big_r(Z2,sk2(Z2))
| big_p(sk5(Y2)) ) ),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f104,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(X1,sk2(X1))
| big_p(sk5(X0)) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [C3,F3] :
( ~ big_r(C3,F3)
| ! [D3,E3] :
( ~ big_r(D3,E3)
| ~ big_p(a)
| ~ big_p(F3)
| ~ big_p(E3)
| big_r(D3,sk6(D3))
| big_p(sk1(C3)) ) ),
inference(miniscoping,[status(thm)],[f30]) ).
fof(f106,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(X1,sk6(X1))
| big_p(sk1(X0)) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f107,plain,
! [H3,J3] :
( ~ big_r(H3,J3)
| ! [G3,I3] :
( ~ big_r(G3,I3)
| ~ big_p(a)
| ~ big_p(J3)
| ~ big_p(I3)
| big_r(H3,sk2(H3))
| big_r(G3,sk6(G3)) ) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f108,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(X1,sk2(X1))
| big_r(X0,sk6(X0)) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
! [L3,N3] :
( ~ big_r(L3,N3)
| ! [K3,M3] :
( ~ big_r(K3,M3)
| ~ big_p(a)
| ~ big_p(N3)
| ~ big_p(M3)
| big_r(sk2(L3),sk1(L3))
| big_p(sk5(K3)) ) ),
inference(miniscoping,[status(thm)],[f32]) ).
fof(f110,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1))
| big_p(sk5(X0)) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
! [P3,R3] :
( ~ big_r(P3,R3)
| ! [O3,Q3] :
( ~ big_r(O3,Q3)
| ~ big_p(a)
| ~ big_p(R3)
| ~ big_p(Q3)
| big_r(sk2(P3),sk1(P3))
| big_r(O3,sk6(O3)) ) ),
inference(miniscoping,[status(thm)],[f33]) ).
fof(f112,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1))
| big_r(X0,sk6(X0)) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f113,plain,
! [S3,V3] :
( ~ big_r(S3,V3)
| ! [T3,U3] :
( ~ big_r(T3,U3)
| ~ big_p(a)
| ~ big_p(V3)
| ~ big_p(U3)
| big_r(sk6(T3),sk5(T3))
| big_p(sk1(S3)) ) ),
inference(miniscoping,[status(thm)],[f34]) ).
fof(f114,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_p(sk1(X0)) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [W3,Z3] :
( ~ big_r(W3,Z3)
| ! [X3,Y3] :
( ~ big_r(X3,Y3)
| ~ big_p(a)
| ~ big_p(Z3)
| ~ big_p(Y3)
| big_r(sk6(X3),sk5(X3))
| big_r(W3,sk2(W3)) ) ),
inference(miniscoping,[status(thm)],[f35]) ).
fof(f116,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_r(X0,sk2(X0)) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f117,plain,
! [A4,D4] :
( ~ big_r(A4,D4)
| ! [B4,C4] :
( ~ big_r(B4,C4)
| ~ big_p(a)
| ~ big_p(D4)
| ~ big_p(C4)
| big_r(sk6(B4),sk5(B4))
| big_r(sk2(A4),sk1(A4)) ) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f118,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_r(sk2(X0),sk1(X0)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f119,plain,
big_p(a),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f120,plain,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_p(sk8)
| big_p(sk10) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f121,plain,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk9,sk10)
| big_p(sk8) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f122,plain,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk7,sk8)
| big_p(sk10) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f123,plain,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk9,sk10)
| big_r(sk7,sk8) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f124,plain,
! [F4] :
( ~ big_r(sk9,F4)
| ! [E4] :
( ~ big_r(F4,E4)
| ~ big_p(sk7)
| ~ big_p(E4)
| big_p(sk8) ) ),
inference(miniscoping,[status(thm)],[f42]) ).
fof(f125,plain,
! [X0,X1] :
( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_p(sk8) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f126,plain,
! [H4] :
( ~ big_r(sk9,H4)
| ! [G4] :
( ~ big_r(H4,G4)
| ~ big_p(sk7)
| ~ big_p(G4)
| big_r(sk7,sk8) ) ),
inference(miniscoping,[status(thm)],[f43]) ).
fof(f127,plain,
! [X0,X1] :
( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_r(sk7,sk8) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f128,plain,
! [J4] :
( ~ big_r(sk7,J4)
| ! [I4] :
( ~ big_r(J4,I4)
| ~ big_p(sk9)
| ~ big_p(I4)
| big_p(sk10) ) ),
inference(miniscoping,[status(thm)],[f44]) ).
fof(f129,plain,
! [X0,X1] :
( ~ big_r(sk7,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk9)
| ~ big_p(X0)
| big_p(sk10) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [L4] :
( ~ big_r(sk7,L4)
| ! [K4] :
( ~ big_r(L4,K4)
| ~ big_p(sk9)
| ~ big_p(K4)
| big_r(sk9,sk10) ) ),
inference(miniscoping,[status(thm)],[f45]) ).
fof(f131,plain,
! [X0,X1] :
( ~ big_r(sk7,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk9)
| ~ big_p(X0)
| big_r(sk9,sk10) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f132,plain,
! [O4] :
( ~ big_r(sk9,O4)
| ! [P4] :
( ~ big_r(sk7,P4)
| ! [N4] :
( ~ big_r(P4,N4)
| ! [M4] :
( ~ big_r(O4,M4)
| ~ big_p(N4)
| ~ big_p(M4) ) ) ) ),
inference(miniscoping,[status(thm)],[f46]) ).
fof(f133,plain,
! [X0,X1,X2,X3] :
( ~ big_r(sk9,X2)
| ~ big_r(sk7,X3)
| ~ big_r(X3,X1)
| ~ big_r(X2,X0)
| ~ big_p(X1)
| ~ big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f134,definition,
! [X0] :
( sQ0_spl
<=> ( big_p(sk3(X0))
| big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f135,plain,
! [X0] :
( ~ sQ0_spl
| big_p(sk3(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f134]) ).
fof(f137,definition,
! [X1] :
( sQ1_spl
<=> ( big_p(sk1(X1))
| big_p(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f138,plain,
! [X0] :
( ~ sQ1_spl
| big_p(sk1(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f137]) ).
fof(f140,definition,
( sQ2_spl
<=> big_p(a) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f142,plain,
( sQ2_spl
| ~ big_p(a) ),
inference(component_clause,[status(thm)],[f140]) ).
fof(f143,plain,
( ~ sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f48,f134,f137,f140]) ).
fof(f144,definition,
! [X0] :
( sQ3_spl
<=> ( big_r(X0,sk4(X0))
| big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f145,plain,
! [X0] :
( ~ sQ3_spl
| big_r(X0,sk4(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f144]) ).
fof(f147,plain,
( ~ sQ2_spl
| sQ1_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f50,f144,f137,f140]) ).
fof(f148,definition,
! [X0] :
( sQ4_spl
<=> ( big_r(sk4(X0),sk3(X0))
| big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f149,plain,
! [X0] :
( ~ sQ4_spl
| big_r(sk4(X0),sk3(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f148]) ).
fof(f151,plain,
( ~ sQ2_spl
| sQ1_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f52,f148,f137,f140]) ).
fof(f152,definition,
! [X1] :
( sQ5_spl
<=> ( big_r(X1,sk2(X1))
| big_p(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f153,plain,
! [X0] :
( ~ sQ5_spl
| big_r(X0,sk2(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f152]) ).
fof(f155,plain,
( ~ sQ2_spl
| sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f54,f134,f152,f140]) ).
fof(f156,plain,
( ~ sQ2_spl
| sQ5_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f56,f144,f152,f140]) ).
fof(f157,plain,
( ~ sQ2_spl
| sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f58,f148,f152,f140]) ).
fof(f158,definition,
! [X1,X2] :
( sQ6_spl
<=> ( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_p(sk5(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f159,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_p(sk5(X0)) ),
inference(component_clause,[status(thm)],[f158]) ).
fof(f162,definition,
! [X1,X2] :
( sQ7_spl
<=> ( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(X1,sk6(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f163,plain,
! [X0,X1] :
( ~ sQ7_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_r(X0,sk6(X0)) ),
inference(component_clause,[status(thm)],[f162]) ).
fof(f166,definition,
! [X1,X2] :
( sQ8_spl
<=> ( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f167,plain,
! [X0,X1] :
( ~ sQ8_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_r(sk6(X0),sk5(X0)) ),
inference(component_clause,[status(thm)],[f166]) ).
fof(f173,definition,
! [X1] :
( sQ9_spl
<=> ( big_r(sk2(X1),sk1(X1))
| big_p(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f174,plain,
! [X0] :
( ~ sQ9_spl
| big_r(sk2(X0),sk1(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f173]) ).
fof(f176,plain,
( ~ sQ2_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f72,f134,f173,f140]) ).
fof(f177,plain,
( ~ sQ2_spl
| sQ9_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f74,f144,f173,f140]) ).
fof(f178,plain,
( ~ sQ2_spl
| sQ9_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f76,f148,f173,f140]) ).
fof(f179,definition,
! [X1,X2] :
( sQ10_spl
<=> ( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_p(sk1(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f180,plain,
! [X0,X1] :
( ~ sQ10_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_p(sk1(X0)) ),
inference(component_clause,[status(thm)],[f179]) ).
fof(f182,plain,
( ~ sQ2_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f78,f134,f179,f140]) ).
fof(f183,definition,
! [X1,X2] :
( sQ11_spl
<=> ( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(X1,sk2(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f184,plain,
! [X0,X1] :
( ~ sQ11_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_r(X0,sk2(X0)) ),
inference(component_clause,[status(thm)],[f183]) ).
fof(f186,plain,
( ~ sQ2_spl
| sQ11_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f80,f134,f183,f140]) ).
fof(f187,plain,
( ~ sQ2_spl
| sQ10_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f82,f144,f179,f140]) ).
fof(f188,plain,
( ~ sQ2_spl
| sQ11_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f84,f144,f183,f140]) ).
fof(f189,definition,
! [X1,X2] :
( sQ12_spl
<=> ( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f190,plain,
! [X0,X1] :
( ~ sQ12_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_r(sk2(X0),sk1(X0)) ),
inference(component_clause,[status(thm)],[f189]) ).
fof(f192,plain,
( ~ sQ2_spl
| sQ12_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f86,f134,f189,f140]) ).
fof(f193,plain,
( ~ sQ2_spl
| sQ12_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f88,f144,f189,f140]) ).
fof(f194,plain,
( ~ sQ2_spl
| sQ10_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f90,f148,f179,f140]) ).
fof(f195,plain,
( ~ sQ2_spl
| sQ11_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f92,f148,f183,f140]) ).
fof(f196,plain,
( ~ sQ2_spl
| sQ12_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f94,f148,f189,f140]) ).
fof(f200,plain,
( ~ sQ2_spl
| sQ6_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f102,f179,f158,f140]) ).
fof(f201,plain,
( ~ sQ2_spl
| sQ11_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f104,f158,f183,f140]) ).
fof(f202,plain,
( ~ sQ2_spl
| sQ7_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f106,f179,f162,f140]) ).
fof(f203,plain,
( ~ sQ2_spl
| sQ11_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f108,f162,f183,f140]) ).
fof(f204,plain,
( ~ sQ2_spl
| sQ12_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f110,f158,f189,f140]) ).
fof(f205,plain,
( ~ sQ2_spl
| sQ12_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f112,f162,f189,f140]) ).
fof(f206,plain,
( ~ sQ2_spl
| sQ8_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f114,f179,f166,f140]) ).
fof(f207,plain,
( ~ sQ2_spl
| sQ8_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f116,f183,f166,f140]) ).
fof(f208,plain,
( ~ sQ2_spl
| sQ8_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f118,f189,f166,f140]) ).
fof(f209,definition,
( sQ13_spl
<=> big_p(sk10) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f210,plain,
( ~ sQ13_spl
| big_p(sk10) ),
inference(component_clause,[status(thm)],[f209]) ).
fof(f212,definition,
( sQ14_spl
<=> big_p(sk8) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f215,definition,
( sQ15_spl
<=> big_p(sk7) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f217,plain,
( sQ15_spl
| ~ big_p(sk7) ),
inference(component_clause,[status(thm)],[f215]) ).
fof(f218,definition,
( sQ16_spl
<=> big_p(sk9) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f221,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| sQ14_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f120,f209,f212,f215,f218]) ).
fof(f222,definition,
( sQ17_spl
<=> big_r(sk9,sk10) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f223,plain,
( ~ sQ17_spl
| big_r(sk9,sk10) ),
inference(component_clause,[status(thm)],[f222]) ).
fof(f225,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| sQ17_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f121,f212,f222,f215,f218]) ).
fof(f226,definition,
( sQ18_spl
<=> big_r(sk7,sk8) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f227,plain,
( ~ sQ18_spl
| big_r(sk7,sk8) ),
inference(component_clause,[status(thm)],[f226]) ).
fof(f229,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| sQ18_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f122,f209,f226,f215,f218]) ).
fof(f230,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| sQ17_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f123,f226,f222,f215,f218]) ).
fof(f231,definition,
! [X0,X1] :
( sQ19_spl
<=> ( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f232,plain,
! [X0,X1] :
( ~ sQ19_spl
| ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f231]) ).
fof(f234,plain,
( ~ sQ15_spl
| sQ19_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f125,f212,f231,f215]) ).
fof(f235,plain,
( ~ sQ15_spl
| sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f127,f226,f231,f215]) ).
fof(f236,definition,
! [X0,X1] :
( sQ20_spl
<=> ( ~ big_r(sk7,X1)
| ~ big_r(X1,X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f237,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ big_r(sk7,X1)
| ~ big_r(X1,X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f236]) ).
fof(f239,plain,
( ~ sQ16_spl
| sQ20_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f129,f209,f236,f218]) ).
fof(f240,plain,
( ~ sQ16_spl
| sQ20_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f131,f222,f236,f218]) ).
fof(f241,plain,
( sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f133,f231,f236]) ).
fof(f242,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f142,f119]) ).
fof(f243,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f242]) ).
fof(f256,definition,
( sQ23_spl
<=> big_r(sk9,sk2(sk9)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f260,definition,
( sQ24_spl
<=> big_r(sk9,sk6(sk9)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f261,plain,
( ~ sQ24_spl
| big_r(sk9,sk6(sk9)) ),
inference(component_clause,[status(thm)],[f260]) ).
fof(f265,plain,
( sQ15_spl
| ~ sQ5_spl
| big_r(sk7,sk2(sk7)) ),
inference(resolution,[status(thm)],[f153,f217]) ).
fof(f267,plain,
( ~ sQ8_spl
| sQ15_spl
| ~ sQ5_spl
| ~ big_p(sk2(sk7))
| big_r(sk6(sk7),sk5(sk7)) ),
inference(resolution,[status(thm)],[f265,f167]) ).
fof(f268,plain,
( ~ sQ12_spl
| sQ15_spl
| ~ sQ5_spl
| ~ big_p(sk2(sk7))
| big_r(sk2(sk7),sk1(sk7)) ),
inference(resolution,[status(thm)],[f265,f190]) ).
fof(f269,plain,
( ~ sQ11_spl
| sQ15_spl
| ~ sQ5_spl
| ~ big_p(sk2(sk7))
| big_r(sk7,sk2(sk7)) ),
inference(resolution,[status(thm)],[f265,f184]) ).
fof(f270,definition,
( sQ25_spl
<=> big_r(sk6(sk7),sk5(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f271,plain,
( ~ sQ25_spl
| big_r(sk6(sk7),sk5(sk7)) ),
inference(component_clause,[status(thm)],[f270]) ).
fof(f273,definition,
( sQ26_spl
<=> big_p(sk2(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f276,plain,
( ~ sQ8_spl
| sQ15_spl
| ~ sQ5_spl
| ~ sQ26_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f267,f270,f273,f152,f215,f166]) ).
fof(f277,definition,
( sQ27_spl
<=> big_r(sk2(sk7),sk1(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f278,plain,
( ~ sQ27_spl
| big_r(sk2(sk7),sk1(sk7)) ),
inference(component_clause,[status(thm)],[f277]) ).
fof(f280,plain,
( ~ sQ12_spl
| sQ15_spl
| ~ sQ5_spl
| ~ sQ26_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f268,f277,f273,f152,f215,f189]) ).
fof(f281,definition,
( sQ28_spl
<=> big_r(sk7,sk2(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f282,plain,
( ~ sQ28_spl
| big_r(sk7,sk2(sk7)) ),
inference(component_clause,[status(thm)],[f281]) ).
fof(f284,plain,
( ~ sQ11_spl
| sQ15_spl
| ~ sQ5_spl
| ~ sQ26_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f269,f281,f273,f152,f215,f183]) ).
fof(f286,plain,
( ~ sQ8_spl
| ~ sQ17_spl
| ~ big_p(sk10)
| big_r(sk6(sk9),sk5(sk9)) ),
inference(resolution,[status(thm)],[f223,f167]) ).
fof(f287,definition,
( sQ29_spl
<=> big_r(sk6(sk9),sk5(sk9)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f288,plain,
( ~ sQ29_spl
| big_r(sk6(sk9),sk5(sk9)) ),
inference(component_clause,[status(thm)],[f287]) ).
fof(f290,plain,
( ~ sQ8_spl
| ~ sQ17_spl
| ~ sQ13_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f286,f287,f209,f222,f166]) ).
fof(f293,plain,
( ~ sQ8_spl
| ~ sQ18_spl
| ~ big_p(sk8)
| big_r(sk6(sk7),sk5(sk7)) ),
inference(resolution,[status(thm)],[f227,f167]) ).
fof(f294,definition,
( sQ30_spl
<=> big_r(sk7,sk6(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f298,plain,
( ~ sQ8_spl
| ~ sQ18_spl
| ~ sQ14_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f293,f270,f212,f226,f166]) ).
fof(f308,plain,
( ~ sQ7_spl
| ~ sQ17_spl
| ~ big_p(sk10)
| big_r(sk9,sk6(sk9)) ),
inference(resolution,[status(thm)],[f223,f163]) ).
fof(f310,plain,
( ~ sQ7_spl
| ~ sQ17_spl
| ~ sQ13_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f308,f260,f209,f222,f162]) ).
fof(f318,plain,
( ~ sQ7_spl
| ~ sQ28_spl
| ~ big_p(sk2(sk7))
| big_r(sk7,sk6(sk7)) ),
inference(resolution,[status(thm)],[f282,f163]) ).
fof(f320,plain,
( ~ sQ7_spl
| ~ sQ28_spl
| ~ sQ26_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f318,f294,f273,f281,f162]) ).
fof(f322,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ24_spl
| ~ big_r(sk6(sk9),X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f261,f232]) ).
fof(f340,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ sQ11_spl
| ~ big_r(sk2(sk7),X1)
| ~ big_p(X1)
| ~ big_r(sk7,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f184,f237]) ).
fof(f341,plain,
! [X0,X1] :
( ~ sQ19_spl
| ~ sQ11_spl
| ~ big_r(sk2(sk9),X1)
| ~ big_p(X1)
| ~ big_r(sk9,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f184,f232]) ).
fof(f342,definition,
! [X0] :
( sQ34_spl
<=> ( ~ big_r(sk7,X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f343,plain,
! [X0] :
( ~ sQ34_spl
| ~ big_r(sk7,X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f342]) ).
fof(f345,definition,
! [X1] :
( sQ35_spl
<=> ( ~ big_r(sk2(sk7),X1)
| ~ big_p(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f346,plain,
! [X0] :
( ~ sQ35_spl
| ~ big_r(sk2(sk7),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f345]) ).
fof(f348,plain,
( ~ sQ20_spl
| ~ sQ11_spl
| sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f340,f342,f345,f183,f236]) ).
fof(f349,definition,
! [X0] :
( sQ36_spl
<=> ( ~ big_r(sk9,X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f350,plain,
! [X0] :
( ~ sQ36_spl
| ~ big_r(sk9,X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f349]) ).
fof(f352,definition,
! [X1] :
( sQ37_spl
<=> ( ~ big_r(sk2(sk9),X1)
| ~ big_p(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f353,plain,
! [X0] :
( ~ sQ37_spl
| ~ big_r(sk2(sk9),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f352]) ).
fof(f355,plain,
( ~ sQ19_spl
| ~ sQ11_spl
| sQ37_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f341,f349,f352,f183,f231]) ).
fof(f356,plain,
! [X0] :
( ~ sQ20_spl
| ~ sQ3_spl
| ~ big_r(sk4(sk7),X0)
| ~ big_p(X0)
| big_p(sk7) ),
inference(resolution,[status(thm)],[f145,f237]) ).
fof(f357,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ3_spl
| ~ big_r(sk4(sk9),X0)
| ~ big_p(X0)
| big_p(sk9) ),
inference(resolution,[status(thm)],[f145,f232]) ).
fof(f358,definition,
! [X0] :
( sQ38_spl
<=> ( ~ big_r(sk4(sk7),X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f359,plain,
! [X0] :
( ~ sQ38_spl
| ~ big_r(sk4(sk7),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f358]) ).
fof(f361,plain,
( ~ sQ20_spl
| ~ sQ3_spl
| sQ38_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f356,f215,f358,f144,f236]) ).
fof(f362,definition,
! [X0] :
( sQ39_spl
<=> ( ~ big_r(sk4(sk9),X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f363,plain,
! [X0] :
( ~ sQ39_spl
| ~ big_r(sk4(sk9),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f362]) ).
fof(f365,plain,
( ~ sQ19_spl
| ~ sQ3_spl
| sQ39_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f357,f218,f362,f144,f231]) ).
fof(f366,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ5_spl
| ~ big_r(sk2(sk9),X0)
| ~ big_p(X0)
| big_p(sk9) ),
inference(resolution,[status(thm)],[f153,f232]) ).
fof(f367,plain,
( ~ sQ19_spl
| ~ sQ5_spl
| sQ37_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f366,f218,f352,f152,f231]) ).
fof(f376,plain,
( ~ sQ18_spl
| ~ sQ34_spl
| ~ big_p(sk8) ),
inference(resolution,[status(thm)],[f343,f227]) ).
fof(f378,plain,
( ~ sQ5_spl
| ~ sQ34_spl
| big_p(sk7)
| ~ big_p(sk2(sk7)) ),
inference(resolution,[status(thm)],[f343,f153]) ).
fof(f380,plain,
( ~ sQ18_spl
| ~ sQ34_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f376,f212,f342,f226]) ).
fof(f385,plain,
( ~ sQ5_spl
| ~ sQ34_spl
| sQ15_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f378,f273,f215,f342,f152]) ).
fof(f390,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ37_spl
| big_p(X0)
| ~ big_r(sk2(sk9),sk1(X0)) ),
inference(resolution,[status(thm)],[f353,f138]) ).
fof(f395,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ35_spl
| big_p(X0)
| ~ big_r(sk2(sk7),sk1(X0)) ),
inference(resolution,[status(thm)],[f346,f138]) ).
fof(f398,plain,
( ~ sQ4_spl
| ~ sQ39_spl
| big_p(sk9)
| ~ big_p(sk3(sk9)) ),
inference(resolution,[status(thm)],[f363,f149]) ).
fof(f402,definition,
( sQ41_spl
<=> big_p(sk3(sk9)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f404,plain,
( sQ41_spl
| ~ big_p(sk3(sk9)) ),
inference(component_clause,[status(thm)],[f402]) ).
fof(f405,plain,
( ~ sQ4_spl
| ~ sQ39_spl
| sQ16_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f398,f402,f218,f362,f148]) ).
fof(f420,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ20_spl
| big_p(sk7)
| ~ big_r(sk2(sk7),X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f237,f153]) ).
fof(f423,plain,
( ~ sQ5_spl
| ~ sQ20_spl
| sQ15_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f420,f345,f215,f236,f152]) ).
fof(f445,plain,
( ~ sQ4_spl
| ~ sQ38_spl
| big_p(sk7)
| ~ big_p(sk3(sk7)) ),
inference(resolution,[status(thm)],[f359,f149]) ).
fof(f449,definition,
( sQ47_spl
<=> big_p(sk3(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f451,plain,
( sQ47_spl
| ~ big_p(sk3(sk7)) ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,plain,
( ~ sQ4_spl
| ~ sQ38_spl
| sQ15_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f445,f449,f215,f358,f148]) ).
fof(f462,plain,
( ~ sQ0_spl
| sQ47_spl
| big_p(sk7) ),
inference(resolution,[status(thm)],[f451,f135]) ).
fof(f463,plain,
( ~ sQ29_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ big_p(sk5(sk9)) ),
inference(resolution,[status(thm)],[f322,f288]) ).
fof(f479,plain,
( ~ sQ0_spl
| sQ47_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f462,f215,f449,f134]) ).
fof(f483,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ29_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ big_r(sk9,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f463,f159]) ).
fof(f497,plain,
( ~ sQ17_spl
| ~ sQ6_spl
| ~ sQ29_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ big_p(sk10) ),
inference(resolution,[status(thm)],[f483,f223]) ).
fof(f501,plain,
( ~ sQ17_spl
| ~ sQ6_spl
| ~ sQ29_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f497,f210]) ).
fof(f502,plain,
( ~ sQ17_spl
| ~ sQ6_spl
| ~ sQ29_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f501]) ).
fof(f516,plain,
( ~ sQ9_spl
| ~ sQ1_spl
| ~ sQ37_spl
| big_p(sk9)
| big_p(sk9) ),
inference(resolution,[status(thm)],[f390,f174]) ).
fof(f518,plain,
( ~ sQ9_spl
| ~ sQ1_spl
| ~ sQ37_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f516,f218,f352,f137,f173]) ).
fof(f523,plain,
( ~ sQ17_spl
| ~ sQ36_spl
| ~ big_p(sk10) ),
inference(resolution,[status(thm)],[f350,f223]) ).
fof(f527,plain,
( ~ sQ17_spl
| ~ sQ36_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f523,f210]) ).
fof(f528,plain,
( ~ sQ17_spl
| ~ sQ36_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f527]) ).
fof(f547,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ sQ7_spl
| ~ big_r(sk6(sk7),X1)
| ~ big_p(X1)
| ~ big_r(sk7,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f163,f237]) ).
fof(f550,definition,
! [X1] :
( sQ53_spl
<=> ( ~ big_r(sk6(sk7),X1)
| ~ big_p(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f551,plain,
! [X0] :
( ~ sQ53_spl
| ~ big_r(sk6(sk7),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f550]) ).
fof(f553,plain,
( ~ sQ20_spl
| ~ sQ7_spl
| sQ53_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f547,f342,f550,f162,f236]) ).
fof(f571,plain,
( ~ sQ25_spl
| ~ sQ53_spl
| ~ big_p(sk5(sk7)) ),
inference(resolution,[status(thm)],[f551,f271]) ).
fof(f584,plain,
( ~ sQ9_spl
| ~ sQ1_spl
| ~ sQ35_spl
| big_p(sk7)
| big_p(sk7) ),
inference(resolution,[status(thm)],[f395,f174]) ).
fof(f586,plain,
( ~ sQ9_spl
| ~ sQ1_spl
| ~ sQ35_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f584,f215,f345,f137,f173]) ).
fof(f592,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ53_spl
| ~ sQ6_spl
| ~ big_r(sk7,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f159,f571]) ).
fof(f593,plain,
( ~ sQ25_spl
| ~ sQ53_spl
| ~ sQ6_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f592,f342,f158,f550,f270]) ).
fof(f605,definition,
( sQ59_spl
<=> big_p(sk1(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f607,plain,
( sQ59_spl
| ~ big_p(sk1(sk7)) ),
inference(component_clause,[status(thm)],[f605]) ).
fof(f618,plain,
! [X0] :
( ~ sQ10_spl
| sQ59_spl
| ~ big_r(sk7,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f607,f180]) ).
fof(f619,plain,
( ~ sQ10_spl
| sQ59_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f618,f342,f605,f179]) ).
fof(f627,plain,
( ~ sQ25_spl
| ~ sQ11_spl
| ~ big_p(sk5(sk7))
| big_r(sk6(sk7),sk2(sk6(sk7))) ),
inference(resolution,[status(thm)],[f184,f271]) ).
fof(f629,plain,
( ~ sQ18_spl
| ~ sQ11_spl
| ~ big_p(sk8)
| big_r(sk7,sk2(sk7)) ),
inference(resolution,[status(thm)],[f184,f227]) ).
fof(f632,definition,
( sQ62_spl
<=> big_r(sk6(sk7),sk2(sk6(sk7))) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f635,definition,
( sQ63_spl
<=> big_p(sk5(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f638,plain,
( ~ sQ25_spl
| ~ sQ11_spl
| ~ sQ63_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f627,f632,f635,f183,f270]) ).
fof(f640,plain,
( ~ sQ18_spl
| ~ sQ11_spl
| ~ sQ14_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f629,f281,f212,f183,f226]) ).
fof(f651,plain,
! [X0] :
( ~ sQ35_spl
| ~ sQ12_spl
| ~ big_p(sk1(sk7))
| ~ big_r(sk7,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f190,f346]) ).
fof(f654,plain,
( ~ sQ35_spl
| ~ sQ12_spl
| ~ sQ59_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f651,f342,f605,f189,f345]) ).
fof(f659,plain,
( ~ sQ0_spl
| sQ41_spl
| big_p(sk9) ),
inference(resolution,[status(thm)],[f404,f135]) ).
fof(f661,plain,
( ~ sQ11_spl
| ~ sQ17_spl
| ~ big_p(sk10)
| big_r(sk9,sk2(sk9)) ),
inference(resolution,[status(thm)],[f223,f184]) ).
fof(f662,plain,
( ~ sQ11_spl
| ~ sQ17_spl
| ~ sQ13_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f661,f256,f209,f222,f183]) ).
fof(f678,plain,
( ~ sQ11_spl
| ~ sQ27_spl
| ~ big_p(sk1(sk7))
| big_r(sk2(sk7),sk2(sk2(sk7))) ),
inference(resolution,[status(thm)],[f278,f184]) ).
fof(f679,definition,
( sQ64_spl
<=> big_r(sk2(sk7),sk2(sk2(sk7))) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f682,plain,
( ~ sQ11_spl
| ~ sQ27_spl
| ~ sQ59_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f678,f679,f605,f277,f183]) ).
fof(f689,definition,
( sQ66_spl
<=> big_p(sk1(sk9)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f691,plain,
( sQ66_spl
| ~ big_p(sk1(sk9)) ),
inference(component_clause,[status(thm)],[f689]) ).
fof(f694,plain,
! [X0] :
( ~ sQ10_spl
| sQ66_spl
| ~ big_r(sk9,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f691,f180]) ).
fof(f695,plain,
( ~ sQ10_spl
| sQ66_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f694,f349,f689,f179]) ).
fof(f705,plain,
! [X0] :
( ~ sQ12_spl
| ~ sQ37_spl
| ~ big_r(sk9,X0)
| ~ big_p(X0)
| ~ big_p(sk1(sk9)) ),
inference(resolution,[status(thm)],[f353,f190]) ).
fof(f713,plain,
( ~ sQ12_spl
| ~ sQ37_spl
| sQ36_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f705,f689,f349,f352,f189]) ).
fof(f720,plain,
( ~ sQ0_spl
| sQ41_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f659,f218,f402,f134]) ).
fof(f723,plain,
$false,
inference(sat_refutation,[status(thm)],[f143,f147,f151,f155,f156,f157,f176,f177,f178,f182,f186,f187,f188,f192,f193,f194,f195,f196,f200,f201,f202,f203,f204,f205,f206,f207,f208,f221,f225,f229,f230,f234,f235,f239,f240,f241,f243,f276,f280,f284,f290,f298,f310,f320,f348,f355,f361,f365,f367,f380,f385,f405,f423,f452,f479,f502,f518,f528,f553,f586,f593,f619,f638,f640,f654,f662,f682,f695,f713,f720]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN067-3 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.95 % Computer : n015.cluster.edu
% 0.09/5.95 % Model : x86_64 x86_64
% 0.09/5.95 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.95 % Memory : 8046.5625MB
% 0.09/5.95 % OS : Linux 6.8.0-71-generic
% 0.09/5.95 % CPULimit : 300
% 0.09/5.95 % WCLimit : 300
% 0.09/5.95 % DateTime : Mon Sep 21 10:45:12 UTC 2026
% 0.09/5.95 % CPUTime :
% 0.09/5.97 % Drodi V4.1.1
% 0.09/5.98 % Refutation found
% 0.09/5.98 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/5.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/6.01 % Elapsed time: 0.043212 seconds
% 0.09/6.01 % CPU time: 0.135268 seconds
% 0.09/6.01 % Total memory used: 14.194 MB
% 0.09/6.01 % Net memory used: 14.088 MB
%------------------------------------------------------------------------------