%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN067-3 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:18:52 PM UTC 2026
% Result : Unsatisfiable 0.14s 5.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN067-3 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n018.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 10:44:07 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 0.14/5.40 % Refutation found
% 0.14/5.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/5.40 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.40 fof(f1,negated_conjecture,(
% 0.14/5.40 (![A,B]: (( big_p(A)| big_p(B)| big_p(sk1(B))| big_p(sk3(A))| ~ big_p(a) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f2,negated_conjecture,(
% 0.14/5.40 (![C,D]: (( big_p(C)| big_p(D)| big_p(sk1(D))| big_r(C,sk4(C))| ~ big_p(a) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f3,negated_conjecture,(
% 0.14/5.40 (![E,F]: (( big_p(E)| big_p(F)| big_p(sk1(F))| big_r(sk4(E),sk3(E))| ~ big_p(a) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f4,negated_conjecture,(
% 0.14/5.40 (![G,H]: (( big_p(G)| big_p(H)| big_p(sk3(G))| big_r(H,sk2(H))| ~ big_p(a) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f5,negated_conjecture,(
% 0.14/5.40 (![I,J]: (( big_p(I)| big_p(J)| big_r(I,sk4(I))| big_r(J,sk2(J))| ~ big_p(a) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f6,negated_conjecture,(
% 0.14/5.40 (![K,L]: (( big_p(K)| big_p(L)| big_r(L,sk2(L))| big_r(sk4(K),sk3(K))| ~ big_p(a) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f7,negated_conjecture,(
% 0.14/5.40 (![M,N,O]: (( big_p(M)| big_p(sk1(M))| big_p(sk5(N))| ~ big_p(O)| ~ big_p(a)| ~ big_r(N,O) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f9,negated_conjecture,(
% 0.14/5.40 (![S,T,U]: (( big_p(S)| big_p(sk1(S))| big_r(sk6(T),sk5(T))| ~ big_p(U)| ~ big_p(a)| ~ big_r(T,U) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f10,negated_conjecture,(
% 0.14/5.40 (![V,W,X]: (( big_p(V)| big_p(sk5(W))| big_r(V,sk2(V))| ~ big_p(X)| ~ big_p(a)| ~ big_r(W,X) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f12,negated_conjecture,(
% 0.14/5.40 (![B1,C1,D1]: (( big_p(B1)| big_r(B1,sk2(B1))| big_r(sk6(C1),sk5(C1))| ~ big_p(D1)| ~ big_p(a)| ~ big_r(C1,D1) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f13,negated_conjecture,(
% 0.14/5.40 (![E1,F1]: (( big_p(E1)| big_p(F1)| big_p(sk3(E1))| big_r(sk2(F1),sk1(F1))| ~ big_p(a) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f14,negated_conjecture,(
% 0.14/5.40 (![G1,H1]: (( big_p(G1)| big_p(H1)| big_r(G1,sk4(G1))| big_r(sk2(H1),sk1(H1))| ~ big_p(a) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f15,negated_conjecture,(
% 0.14/5.40 (![I1,J1]: (( big_p(I1)| big_p(J1)| big_r(sk2(J1),sk1(J1))| big_r(sk4(I1),sk3(I1))| ~ big_p(a) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f16,negated_conjecture,(
% 0.14/5.40 (![K1,L1,M1]: (( big_p(K1)| big_p(sk1(L1))| big_p(sk3(K1))| ~ big_p(M1)| ~ big_p(a)| ~ big_r(L1,M1) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f17,negated_conjecture,(
% 0.14/5.40 (![N1,O1,P1]: (( big_p(N1)| big_p(sk3(N1))| big_r(O1,sk2(O1))| ~ big_p(P1)| ~ big_p(a)| ~ big_r(O1,P1) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f20,negated_conjecture,(
% 0.14/5.40 (![W1,X1,Y1]: (( big_p(W1)| big_p(sk3(W1))| big_r(sk2(X1),sk1(X1))| ~ big_p(Y1)| ~ big_p(a)| ~ big_r(X1,Y1) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f22,negated_conjecture,(
% 0.14/5.40 (![C2,D2,E2]: (( big_p(C2)| big_p(sk1(D2))| big_r(sk4(C2),sk3(C2))| ~ big_p(E2)| ~ big_p(a)| ~ big_r(D2,E2) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f23,negated_conjecture,(
% 0.14/5.40 (![F2,G2,H2]: (( big_p(F2)| big_r(G2,sk2(G2))| big_r(sk4(F2),sk3(F2))| ~ big_p(H2)| ~ big_p(a)| ~ big_r(G2,H2) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f24,negated_conjecture,(
% 0.14/5.40 (![I2,J2,K2]: (( big_p(I2)| big_r(sk2(J2),sk1(J2))| big_r(sk4(I2),sk3(I2))| ~ big_p(K2)| ~ big_p(a)| ~ big_r(J2,K2) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f25,negated_conjecture,(
% 0.14/5.40 (![L2,M2,N2]: (( big_p(L2)| big_p(sk5(M2))| big_r(sk2(L2),sk1(L2))| ~ big_p(N2)| ~ big_p(a)| ~ big_r(M2,N2) ) ))),
% 0.14/5.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.40 fof(f27,negated_conjecture,(
% 0.14/5.40 (![R2,S2,T2]: (( big_p(R2)| big_r(sk2(R2),sk1(R2))| big_r(sk6(S2),sk5(S2))| ~ big_p(T2)| ~ big_p(a)| ~ big_r(S2,T2) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f28,negated_conjecture,(
% 0.14/5.41 (![U2,V2,W2,X2]: (( big_p(sk1(U2))| big_p(sk5(V2))| ~ big_p(W2)| ~ big_p(X2)| ~ big_p(a)| ~ big_r(V2,W2)| ~ big_r(U2,X2) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f29,negated_conjecture,(
% 0.14/5.41 (![Y2,Z2,A3,B3]: (( big_p(sk5(Y2))| big_r(Z2,sk2(Z2))| ~ big_p(A3)| ~ big_p(B3)| ~ big_p(a)| ~ big_r(Y2,A3)| ~ big_r(Z2,B3) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f30,negated_conjecture,(
% 0.14/5.41 (![C3,D3,E3,F3]: (( big_p(sk1(C3))| big_r(D3,sk6(D3))| ~ big_p(E3)| ~ big_p(F3)| ~ big_p(a)| ~ big_r(D3,E3)| ~ big_r(C3,F3) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f31,negated_conjecture,(
% 0.14/5.41 (![G3,H3,I3,J3]: (( big_r(G3,sk6(G3))| big_r(H3,sk2(H3))| ~ big_p(I3)| ~ big_p(J3)| ~ big_p(a)| ~ big_r(G3,I3)| ~ big_r(H3,J3) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f32,negated_conjecture,(
% 0.14/5.41 (![K3,L3,M3,N3]: (( big_p(sk5(K3))| big_r(sk2(L3),sk1(L3))| ~ big_p(M3)| ~ big_p(N3)| ~ big_p(a)| ~ big_r(K3,M3)| ~ big_r(L3,N3) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f33,negated_conjecture,(
% 0.14/5.41 (![O3,P3,Q3,R3]: (( big_r(O3,sk6(O3))| big_r(sk2(P3),sk1(P3))| ~ big_p(Q3)| ~ big_p(R3)| ~ big_p(a)| ~ big_r(O3,Q3)| ~ big_r(P3,R3) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f34,negated_conjecture,(
% 0.14/5.41 (![S3,T3,U3,V3]: (( big_p(sk1(S3))| big_r(sk6(T3),sk5(T3))| ~ big_p(U3)| ~ big_p(V3)| ~ big_p(a)| ~ big_r(T3,U3)| ~ big_r(S3,V3) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f35,negated_conjecture,(
% 0.14/5.41 (![W3,X3,Y3,Z3]: (( big_r(W3,sk2(W3))| big_r(sk6(X3),sk5(X3))| ~ big_p(Y3)| ~ big_p(Z3)| ~ big_p(a)| ~ big_r(X3,Y3)| ~ big_r(W3,Z3) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f36,negated_conjecture,(
% 0.14/5.41 (![A4,B4,C4,D4]: (( big_r(sk2(A4),sk1(A4))| big_r(sk6(B4),sk5(B4))| ~ big_p(C4)| ~ big_p(D4)| ~ big_p(a)| ~ big_r(B4,C4)| ~ big_r(A4,D4) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f37,negated_conjecture,(
% 0.14/5.41 big_p(a) ),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f38,negated_conjecture,(
% 0.14/5.41 ( big_p(sk10)| big_p(sk8)| ~ big_p(sk7)| ~ big_p(sk9) ) ),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f39,negated_conjecture,(
% 0.14/5.41 ( big_p(sk8)| big_r(sk9,sk10)| ~ big_p(sk7)| ~ big_p(sk9) ) ),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f40,negated_conjecture,(
% 0.14/5.41 ( big_p(sk10)| big_r(sk7,sk8)| ~ big_p(sk7)| ~ big_p(sk9) ) ),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f41,negated_conjecture,(
% 0.14/5.41 ( big_r(sk7,sk8)| big_r(sk9,sk10)| ~ big_p(sk7)| ~ big_p(sk9) ) ),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f42,negated_conjecture,(
% 0.14/5.41 (![E4,F4]: (( big_p(sk8)| ~ big_p(E4)| ~ big_p(sk7)| ~ big_r(F4,E4)| ~ big_r(sk9,F4) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f43,negated_conjecture,(
% 0.14/5.41 (![G4,H4]: (( big_r(sk7,sk8)| ~ big_p(G4)| ~ big_p(sk7)| ~ big_r(H4,G4)| ~ big_r(sk9,H4) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f44,negated_conjecture,(
% 0.14/5.41 (![I4,J4]: (( big_p(sk10)| ~ big_p(I4)| ~ big_p(sk9)| ~ big_r(J4,I4)| ~ big_r(sk7,J4) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f45,negated_conjecture,(
% 0.14/5.41 (![K4,L4]: (( big_r(sk9,sk10)| ~ big_p(K4)| ~ big_p(sk9)| ~ big_r(L4,K4)| ~ big_r(sk7,L4) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f46,negated_conjecture,(
% 0.14/5.41 (![M4,N4,O4,P4]: (( ~ big_p(M4)| ~ big_p(N4)| ~ big_r(O4,M4)| ~ big_r(P4,N4)| ~ big_r(sk7,P4)| ~ big_r(sk9,O4) ) ))),
% 0.14/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f47,plain,(
% 0.14/5.41 (![A]: ((![B]: ((big_p(A)|big_p(B))|big_p(sk1(B))))|big_p(sk3(A))))|~big_p(a)),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f1])).
% 0.14/5.41 fof(f48,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(X0)|big_p(X1)|big_p(sk1(X1))|big_p(sk3(X0))|~big_p(a))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f47])).
% 0.14/5.41 fof(f49,plain,(
% 0.14/5.41 (![C]: ((![D]: ((big_p(C)|big_p(D))|big_p(sk1(D))))|big_r(C,sk4(C))))|~big_p(a)),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f2])).
% 0.14/5.41 fof(f50,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(X0)|big_p(X1)|big_p(sk1(X1))|big_r(X0,sk4(X0))|~big_p(a))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f49])).
% 0.14/5.41 fof(f51,plain,(
% 0.14/5.41 (![E]: ((![F]: ((big_p(E)|big_p(F))|big_p(sk1(F))))|big_r(sk4(E),sk3(E))))|~big_p(a)),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f3])).
% 0.14/5.41 fof(f52,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(X0)|big_p(X1)|big_p(sk1(X1))|big_r(sk4(X0),sk3(X0))|~big_p(a))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f51])).
% 0.14/5.41 fof(f53,plain,(
% 0.14/5.41 (![H]: ((![G]: ((big_p(G)|big_p(H))|big_p(sk3(G))))|big_r(H,sk2(H))))|~big_p(a)),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f4])).
% 0.14/5.41 fof(f54,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(X0)|big_p(X1)|big_p(sk3(X0))|big_r(X1,sk2(X1))|~big_p(a))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f53])).
% 0.14/5.41 fof(f55,plain,(
% 0.14/5.41 (![J]: ((![I]: ((big_p(I)|big_p(J))|big_r(I,sk4(I))))|big_r(J,sk2(J))))|~big_p(a)),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f5])).
% 0.14/5.41 fof(f56,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(X0)|big_p(X1)|big_r(X0,sk4(X0))|big_r(X1,sk2(X1))|~big_p(a))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/5.41 fof(f57,plain,(
% 0.14/5.41 (![K]: ((![L]: ((big_p(K)|big_p(L))|big_r(L,sk2(L))))|big_r(sk4(K),sk3(K))))|~big_p(a)),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f6])).
% 0.14/5.41 fof(f58,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(X0)|big_p(X1)|big_r(X1,sk2(X1))|big_r(sk4(X0),sk3(X0))|~big_p(a))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f57])).
% 0.14/5.41 fof(f59,plain,(
% 0.14/5.41 ![N,O]: (((((![M]: (big_p(M)|big_p(sk1(M))))|big_p(sk5(N)))|~big_p(O))|~big_p(a))|~big_r(N,O))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f7])).
% 0.14/5.41 fof(f60,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_p(sk1(X0))|big_p(sk5(X1))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f59])).
% 0.14/5.41 fof(f63,plain,(
% 0.14/5.41 ![T,U]: (((((![S]: (big_p(S)|big_p(sk1(S))))|big_r(sk6(T),sk5(T)))|~big_p(U))|~big_p(a))|~big_r(T,U))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f9])).
% 0.14/5.41 fof(f64,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_p(sk1(X0))|big_r(sk6(X1),sk5(X1))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f63])).
% 0.14/5.41 fof(f65,plain,(
% 0.14/5.41 ![W,X]: ((((![V]: ((big_p(V)|big_p(sk5(W)))|big_r(V,sk2(V))))|~big_p(X))|~big_p(a))|~big_r(W,X))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f10])).
% 0.14/5.41 fof(f66,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_p(sk5(X1))|big_r(X0,sk2(X0))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f65])).
% 0.14/5.41 fof(f69,plain,(
% 0.14/5.41 ![C1,D1]: (((((![B1]: (big_p(B1)|big_r(B1,sk2(B1))))|big_r(sk6(C1),sk5(C1)))|~big_p(D1))|~big_p(a))|~big_r(C1,D1))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f12])).
% 0.14/5.41 fof(f70,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_r(X0,sk2(X0))|big_r(sk6(X1),sk5(X1))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f69])).
% 0.14/5.41 fof(f71,plain,(
% 0.14/5.41 (![F1]: ((![E1]: ((big_p(E1)|big_p(F1))|big_p(sk3(E1))))|big_r(sk2(F1),sk1(F1))))|~big_p(a)),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f13])).
% 0.14/5.41 fof(f72,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(X0)|big_p(X1)|big_p(sk3(X0))|big_r(sk2(X1),sk1(X1))|~big_p(a))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.14/5.41 fof(f73,plain,(
% 0.14/5.41 (![H1]: ((![G1]: ((big_p(G1)|big_p(H1))|big_r(G1,sk4(G1))))|big_r(sk2(H1),sk1(H1))))|~big_p(a)),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f14])).
% 0.14/5.41 fof(f74,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(X0)|big_p(X1)|big_r(X0,sk4(X0))|big_r(sk2(X1),sk1(X1))|~big_p(a))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/5.41 fof(f75,plain,(
% 0.14/5.41 (![I1]: ((![J1]: ((big_p(I1)|big_p(J1))|big_r(sk2(J1),sk1(J1))))|big_r(sk4(I1),sk3(I1))))|~big_p(a)),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f15])).
% 0.14/5.41 fof(f76,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(X0)|big_p(X1)|big_r(sk2(X1),sk1(X1))|big_r(sk4(X0),sk3(X0))|~big_p(a))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f75])).
% 0.14/5.41 fof(f77,plain,(
% 0.14/5.41 ![L1,M1]: ((((![K1]: ((big_p(K1)|big_p(sk1(L1)))|big_p(sk3(K1))))|~big_p(M1))|~big_p(a))|~big_r(L1,M1))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f16])).
% 0.14/5.41 fof(f78,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_p(sk1(X1))|big_p(sk3(X0))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f77])).
% 0.14/5.41 fof(f79,plain,(
% 0.14/5.41 ![O1,P1]: (((((![N1]: (big_p(N1)|big_p(sk3(N1))))|big_r(O1,sk2(O1)))|~big_p(P1))|~big_p(a))|~big_r(O1,P1))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f17])).
% 0.14/5.41 fof(f80,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_p(sk3(X0))|big_r(X1,sk2(X1))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f79])).
% 0.14/5.41 fof(f85,plain,(
% 0.14/5.41 ![X1,Y1]: (((((![W1]: (big_p(W1)|big_p(sk3(W1))))|big_r(sk2(X1),sk1(X1)))|~big_p(Y1))|~big_p(a))|~big_r(X1,Y1))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f20])).
% 0.14/5.41 fof(f86,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_p(sk3(X0))|big_r(sk2(X1),sk1(X1))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f85])).
% 0.14/5.41 fof(f89,plain,(
% 0.14/5.41 ![D2,E2]: ((((![C2]: ((big_p(C2)|big_p(sk1(D2)))|big_r(sk4(C2),sk3(C2))))|~big_p(E2))|~big_p(a))|~big_r(D2,E2))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f22])).
% 0.14/5.41 fof(f90,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_p(sk1(X1))|big_r(sk4(X0),sk3(X0))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f89])).
% 0.14/5.41 fof(f91,plain,(
% 0.14/5.41 ![G2,H2]: ((((![F2]: ((big_p(F2)|big_r(G2,sk2(G2)))|big_r(sk4(F2),sk3(F2))))|~big_p(H2))|~big_p(a))|~big_r(G2,H2))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f23])).
% 0.14/5.41 fof(f92,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_r(X1,sk2(X1))|big_r(sk4(X0),sk3(X0))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f91])).
% 0.14/5.41 fof(f93,plain,(
% 0.14/5.41 ![J2,K2]: ((((![I2]: ((big_p(I2)|big_r(sk2(J2),sk1(J2)))|big_r(sk4(I2),sk3(I2))))|~big_p(K2))|~big_p(a))|~big_r(J2,K2))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f24])).
% 0.14/5.41 fof(f94,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_r(sk2(X1),sk1(X1))|big_r(sk4(X0),sk3(X0))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f93])).
% 0.14/5.41 fof(f95,plain,(
% 0.14/5.41 ![M2,N2]: ((((![L2]: ((big_p(L2)|big_p(sk5(M2)))|big_r(sk2(L2),sk1(L2))))|~big_p(N2))|~big_p(a))|~big_r(M2,N2))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f25])).
% 0.14/5.41 fof(f96,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_p(sk5(X1))|big_r(sk2(X0),sk1(X0))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f95])).
% 0.14/5.41 fof(f99,plain,(
% 0.14/5.41 ![S2,T2]: (((((![R2]: (big_p(R2)|big_r(sk2(R2),sk1(R2))))|big_r(sk6(S2),sk5(S2)))|~big_p(T2))|~big_p(a))|~big_r(S2,T2))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f27])).
% 0.14/5.41 fof(f100,plain,(
% 0.14/5.41 ![X0,X1,X2]: (big_p(X0)|big_r(sk2(X0),sk1(X0))|big_r(sk6(X1),sk5(X1))|~big_p(X2)|~big_p(a)|~big_r(X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f99])).
% 0.14/5.41 fof(f101,plain,(
% 0.14/5.41 ![U2,X2]: ((![V2,W2]: (((((big_p(sk1(U2))|big_p(sk5(V2)))|~big_p(W2))|~big_p(X2))|~big_p(a))|~big_r(V2,W2)))|~big_r(U2,X2))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f28])).
% 0.14/5.41 fof(f102,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (big_p(sk1(X0))|big_p(sk5(X1))|~big_p(X2)|~big_p(X3)|~big_p(a)|~big_r(X1,X2)|~big_r(X0,X3))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f101])).
% 0.14/5.41 fof(f103,plain,(
% 0.14/5.41 ![Z2,B3]: ((![Y2,A3]: (((((big_p(sk5(Y2))|big_r(Z2,sk2(Z2)))|~big_p(A3))|~big_p(B3))|~big_p(a))|~big_r(Y2,A3)))|~big_r(Z2,B3))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f29])).
% 0.14/5.41 fof(f104,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (big_p(sk5(X0))|big_r(X1,sk2(X1))|~big_p(X2)|~big_p(X3)|~big_p(a)|~big_r(X0,X2)|~big_r(X1,X3))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f103])).
% 0.14/5.41 fof(f105,plain,(
% 0.14/5.41 ![C3,F3]: ((![D3,E3]: (((((big_p(sk1(C3))|big_r(D3,sk6(D3)))|~big_p(E3))|~big_p(F3))|~big_p(a))|~big_r(D3,E3)))|~big_r(C3,F3))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f30])).
% 0.14/5.41 fof(f106,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (big_p(sk1(X0))|big_r(X1,sk6(X1))|~big_p(X2)|~big_p(X3)|~big_p(a)|~big_r(X1,X2)|~big_r(X0,X3))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f105])).
% 0.14/5.41 fof(f107,plain,(
% 0.14/5.41 ![H3,J3]: ((![G3,I3]: (((((big_r(G3,sk6(G3))|big_r(H3,sk2(H3)))|~big_p(I3))|~big_p(J3))|~big_p(a))|~big_r(G3,I3)))|~big_r(H3,J3))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f31])).
% 0.14/5.41 fof(f108,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (big_r(X0,sk6(X0))|big_r(X1,sk2(X1))|~big_p(X2)|~big_p(X3)|~big_p(a)|~big_r(X0,X2)|~big_r(X1,X3))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f107])).
% 0.14/5.41 fof(f109,plain,(
% 0.14/5.41 ![L3,N3]: ((![K3,M3]: (((((big_p(sk5(K3))|big_r(sk2(L3),sk1(L3)))|~big_p(M3))|~big_p(N3))|~big_p(a))|~big_r(K3,M3)))|~big_r(L3,N3))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f32])).
% 0.14/5.41 fof(f110,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (big_p(sk5(X0))|big_r(sk2(X1),sk1(X1))|~big_p(X2)|~big_p(X3)|~big_p(a)|~big_r(X0,X2)|~big_r(X1,X3))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f109])).
% 0.14/5.41 fof(f111,plain,(
% 0.14/5.41 ![P3,R3]: ((![O3,Q3]: (((((big_r(O3,sk6(O3))|big_r(sk2(P3),sk1(P3)))|~big_p(Q3))|~big_p(R3))|~big_p(a))|~big_r(O3,Q3)))|~big_r(P3,R3))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f33])).
% 0.14/5.41 fof(f112,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (big_r(X0,sk6(X0))|big_r(sk2(X1),sk1(X1))|~big_p(X2)|~big_p(X3)|~big_p(a)|~big_r(X0,X2)|~big_r(X1,X3))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f111])).
% 0.14/5.41 fof(f113,plain,(
% 0.14/5.41 ![S3,V3]: ((![T3,U3]: (((((big_p(sk1(S3))|big_r(sk6(T3),sk5(T3)))|~big_p(U3))|~big_p(V3))|~big_p(a))|~big_r(T3,U3)))|~big_r(S3,V3))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f34])).
% 0.14/5.41 fof(f114,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (big_p(sk1(X0))|big_r(sk6(X1),sk5(X1))|~big_p(X2)|~big_p(X3)|~big_p(a)|~big_r(X1,X2)|~big_r(X0,X3))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f113])).
% 0.14/5.41 fof(f115,plain,(
% 0.14/5.41 ![W3,Z3]: ((![X3,Y3]: (((((big_r(W3,sk2(W3))|big_r(sk6(X3),sk5(X3)))|~big_p(Y3))|~big_p(Z3))|~big_p(a))|~big_r(X3,Y3)))|~big_r(W3,Z3))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f35])).
% 0.14/5.41 fof(f116,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (big_r(X0,sk2(X0))|big_r(sk6(X1),sk5(X1))|~big_p(X2)|~big_p(X3)|~big_p(a)|~big_r(X1,X2)|~big_r(X0,X3))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f115])).
% 0.14/5.41 fof(f117,plain,(
% 0.14/5.41 ![A4,D4]: ((![B4,C4]: (((((big_r(sk2(A4),sk1(A4))|big_r(sk6(B4),sk5(B4)))|~big_p(C4))|~big_p(D4))|~big_p(a))|~big_r(B4,C4)))|~big_r(A4,D4))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f36])).
% 0.14/5.41 fof(f118,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (big_r(sk2(X0),sk1(X0))|big_r(sk6(X1),sk5(X1))|~big_p(X2)|~big_p(X3)|~big_p(a)|~big_r(X1,X2)|~big_r(X0,X3))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f117])).
% 0.14/5.41 fof(f119,plain,(
% 0.14/5.41 big_p(a)),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f37])).
% 0.14/5.41 fof(f120,plain,(
% 0.14/5.41 big_p(sk10)|big_p(sk8)|~big_p(sk7)|~big_p(sk9)),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f38])).
% 0.14/5.41 fof(f121,plain,(
% 0.14/5.41 big_p(sk8)|big_r(sk9,sk10)|~big_p(sk7)|~big_p(sk9)),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f39])).
% 0.14/5.41 fof(f122,plain,(
% 0.14/5.41 big_p(sk10)|big_r(sk7,sk8)|~big_p(sk7)|~big_p(sk9)),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f40])).
% 0.14/5.41 fof(f123,plain,(
% 0.14/5.41 big_r(sk7,sk8)|big_r(sk9,sk10)|~big_p(sk7)|~big_p(sk9)),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f41])).
% 0.14/5.41 fof(f124,plain,(
% 0.14/5.41 ![F4]: ((![E4]: (((big_p(sk8)|~big_p(E4))|~big_p(sk7))|~big_r(F4,E4)))|~big_r(sk9,F4))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f42])).
% 0.14/5.41 fof(f125,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(sk8)|~big_p(X0)|~big_p(sk7)|~big_r(X1,X0)|~big_r(sk9,X1))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f124])).
% 0.14/5.41 fof(f126,plain,(
% 0.14/5.41 ![H4]: ((![G4]: (((big_r(sk7,sk8)|~big_p(G4))|~big_p(sk7))|~big_r(H4,G4)))|~big_r(sk9,H4))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f43])).
% 0.14/5.41 fof(f127,plain,(
% 0.14/5.41 ![X0,X1]: (big_r(sk7,sk8)|~big_p(X0)|~big_p(sk7)|~big_r(X1,X0)|~big_r(sk9,X1))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f126])).
% 0.14/5.41 fof(f128,plain,(
% 0.14/5.41 ![J4]: ((![I4]: (((big_p(sk10)|~big_p(I4))|~big_p(sk9))|~big_r(J4,I4)))|~big_r(sk7,J4))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f44])).
% 0.14/5.41 fof(f129,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(sk10)|~big_p(X0)|~big_p(sk9)|~big_r(X1,X0)|~big_r(sk7,X1))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f128])).
% 0.14/5.41 fof(f130,plain,(
% 0.14/5.41 ![L4]: ((![K4]: (((big_r(sk9,sk10)|~big_p(K4))|~big_p(sk9))|~big_r(L4,K4)))|~big_r(sk7,L4))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f45])).
% 0.14/5.41 fof(f131,plain,(
% 0.14/5.41 ![X0,X1]: (big_r(sk9,sk10)|~big_p(X0)|~big_p(sk9)|~big_r(X1,X0)|~big_r(sk7,X1))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f130])).
% 0.14/5.41 fof(f132,plain,(
% 0.14/5.41 ![O4]: ((![P4]: ((![N4]: ((![M4]: ((~big_p(M4)|~big_p(N4))|~big_r(O4,M4)))|~big_r(P4,N4)))|~big_r(sk7,P4)))|~big_r(sk9,O4))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f46])).
% 0.14/5.41 fof(f133,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (~big_p(X0)|~big_p(X1)|~big_r(X2,X0)|~big_r(X3,X1)|~big_r(sk7,X3)|~big_r(sk9,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f132])).
% 0.14/5.41 fof(f134,definition,(
% 0.14/5.41 ![X0]: (sQ0_spl <=> (big_p(X0)|big_p(sk3(X0))))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f135,plain,(
% 0.14/5.41 ![X0]: (big_p(X0)|big_p(sk3(X0))|~sQ0_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f134])).
% 0.14/5.41 fof(f137,definition,(
% 0.14/5.41 ![X1]: (sQ1_spl <=> (big_p(X1)|big_p(sk1(X1))))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f138,plain,(
% 0.14/5.41 ![X0]: (big_p(X0)|big_p(sk1(X0))|~sQ1_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f137])).
% 0.14/5.41 fof(f140,definition,(
% 0.14/5.41 sQ2_spl <=> (big_p(a))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f142,plain,(
% 0.14/5.41 ~big_p(a)|sQ2_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f140])).
% 0.14/5.41 fof(f143,plain,(
% 0.14/5.41 sQ0_spl|sQ1_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f48,f134,f137,f140])).
% 0.14/5.41 fof(f144,definition,(
% 0.14/5.41 ![X0]: (sQ3_spl <=> (big_p(X0)|big_r(X0,sk4(X0))))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f145,plain,(
% 0.14/5.41 ![X0]: (big_p(X0)|big_r(X0,sk4(X0))|~sQ3_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f144])).
% 0.14/5.41 fof(f147,plain,(
% 0.14/5.41 sQ3_spl|sQ1_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f50,f144,f137,f140])).
% 0.14/5.41 fof(f148,definition,(
% 0.14/5.41 ![X0]: (sQ4_spl <=> (big_p(X0)|big_r(sk4(X0),sk3(X0))))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f149,plain,(
% 0.14/5.41 ![X0]: (big_p(X0)|big_r(sk4(X0),sk3(X0))|~sQ4_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f148])).
% 0.14/5.41 fof(f151,plain,(
% 0.14/5.41 sQ4_spl|sQ1_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f52,f148,f137,f140])).
% 0.14/5.41 fof(f152,definition,(
% 0.14/5.41 ![X1]: (sQ5_spl <=> (big_p(X1)|big_r(X1,sk2(X1))))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f153,plain,(
% 0.14/5.41 ![X0]: (big_p(X0)|big_r(X0,sk2(X0))|~sQ5_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f152])).
% 0.14/5.41 fof(f155,plain,(
% 0.14/5.41 sQ0_spl|sQ5_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f54,f134,f152,f140])).
% 0.14/5.41 fof(f156,plain,(
% 0.14/5.41 sQ3_spl|sQ5_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f56,f144,f152,f140])).
% 0.14/5.41 fof(f157,plain,(
% 0.14/5.41 sQ4_spl|sQ5_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f58,f148,f152,f140])).
% 0.14/5.41 fof(f158,definition,(
% 0.14/5.41 ![X1,X2]: (sQ6_spl <=> (big_p(sk5(X1))|~big_p(X2)|~big_r(X1,X2)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f159,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(sk5(X0))|~big_p(X1)|~big_r(X0,X1)|~sQ6_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f158])).
% 0.14/5.41 fof(f161,plain,(
% 0.14/5.41 sQ1_spl|sQ6_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f60,f137,f158,f140])).
% 0.14/5.41 fof(f162,definition,(
% 0.14/5.41 ![X1,X2]: (sQ7_spl <=> (big_r(X1,sk6(X1))|~big_p(X2)|~big_r(X1,X2)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f163,plain,(
% 0.14/5.41 ![X0,X1]: (big_r(X0,sk6(X0))|~big_p(X1)|~big_r(X0,X1)|~sQ7_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f162])).
% 0.14/5.41 fof(f166,definition,(
% 0.14/5.41 ![X1,X2]: (sQ8_spl <=> (big_r(sk6(X1),sk5(X1))|~big_p(X2)|~big_r(X1,X2)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f167,plain,(
% 0.14/5.41 ![X0,X1]: (big_r(sk6(X0),sk5(X0))|~big_p(X1)|~big_r(X0,X1)|~sQ8_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f166])).
% 0.14/5.41 fof(f169,plain,(
% 0.14/5.41 sQ1_spl|sQ8_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f64,f137,f166,f140])).
% 0.14/5.41 fof(f170,plain,(
% 0.14/5.41 sQ5_spl|sQ6_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f66,f152,f158,f140])).
% 0.14/5.41 fof(f172,plain,(
% 0.14/5.41 sQ5_spl|sQ8_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f70,f152,f166,f140])).
% 0.14/5.41 fof(f173,definition,(
% 0.14/5.41 ![X1]: (sQ9_spl <=> (big_p(X1)|big_r(sk2(X1),sk1(X1))))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f174,plain,(
% 0.14/5.41 ![X0]: (big_p(X0)|big_r(sk2(X0),sk1(X0))|~sQ9_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f173])).
% 0.14/5.41 fof(f176,plain,(
% 0.14/5.41 sQ0_spl|sQ9_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f72,f134,f173,f140])).
% 0.14/5.41 fof(f177,plain,(
% 0.14/5.41 sQ3_spl|sQ9_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f74,f144,f173,f140])).
% 0.14/5.41 fof(f178,plain,(
% 0.14/5.41 sQ4_spl|sQ9_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f76,f148,f173,f140])).
% 0.14/5.41 fof(f179,definition,(
% 0.14/5.41 ![X1,X2]: (sQ10_spl <=> (big_p(sk1(X1))|~big_p(X2)|~big_r(X1,X2)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f180,plain,(
% 0.14/5.41 ![X0,X1]: (big_p(sk1(X0))|~big_p(X1)|~big_r(X0,X1)|~sQ10_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f179])).
% 0.14/5.41 fof(f182,plain,(
% 0.14/5.41 sQ0_spl|sQ10_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f78,f134,f179,f140])).
% 0.14/5.41 fof(f183,definition,(
% 0.14/5.41 ![X1,X2]: (sQ11_spl <=> (big_r(X1,sk2(X1))|~big_p(X2)|~big_r(X1,X2)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f184,plain,(
% 0.14/5.41 ![X0,X1]: (big_r(X0,sk2(X0))|~big_p(X1)|~big_r(X0,X1)|~sQ11_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f183])).
% 0.14/5.41 fof(f186,plain,(
% 0.14/5.41 sQ0_spl|sQ11_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f80,f134,f183,f140])).
% 0.14/5.41 fof(f189,definition,(
% 0.14/5.41 ![X1,X2]: (sQ12_spl <=> (big_r(sk2(X1),sk1(X1))|~big_p(X2)|~big_r(X1,X2)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f190,plain,(
% 0.14/5.41 ![X0,X1]: (big_r(sk2(X0),sk1(X0))|~big_p(X1)|~big_r(X0,X1)|~sQ12_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f189])).
% 0.14/5.41 fof(f192,plain,(
% 0.14/5.41 sQ0_spl|sQ12_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f86,f134,f189,f140])).
% 0.14/5.41 fof(f194,plain,(
% 0.14/5.41 sQ4_spl|sQ10_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f90,f148,f179,f140])).
% 0.14/5.41 fof(f195,plain,(
% 0.14/5.41 sQ4_spl|sQ11_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f92,f148,f183,f140])).
% 0.14/5.41 fof(f196,plain,(
% 0.14/5.41 sQ4_spl|sQ12_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f94,f148,f189,f140])).
% 0.14/5.41 fof(f197,plain,(
% 0.14/5.41 sQ9_spl|sQ6_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f96,f173,f158,f140])).
% 0.14/5.41 fof(f199,plain,(
% 0.14/5.41 sQ9_spl|sQ8_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f100,f173,f166,f140])).
% 0.14/5.41 fof(f200,plain,(
% 0.14/5.41 sQ10_spl|sQ6_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f102,f179,f158,f140])).
% 0.14/5.41 fof(f201,plain,(
% 0.14/5.41 sQ6_spl|sQ11_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f104,f158,f183,f140])).
% 0.14/5.41 fof(f202,plain,(
% 0.14/5.41 sQ10_spl|sQ7_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f106,f179,f162,f140])).
% 0.14/5.41 fof(f203,plain,(
% 0.14/5.41 sQ7_spl|sQ11_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f108,f162,f183,f140])).
% 0.14/5.41 fof(f204,plain,(
% 0.14/5.41 sQ6_spl|sQ12_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f110,f158,f189,f140])).
% 0.14/5.41 fof(f205,plain,(
% 0.14/5.41 sQ7_spl|sQ12_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f112,f162,f189,f140])).
% 0.14/5.41 fof(f206,plain,(
% 0.14/5.41 sQ10_spl|sQ8_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f114,f179,f166,f140])).
% 0.14/5.41 fof(f207,plain,(
% 0.14/5.41 sQ11_spl|sQ8_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f116,f183,f166,f140])).
% 0.14/5.41 fof(f208,plain,(
% 0.14/5.41 sQ12_spl|sQ8_spl|~sQ2_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f118,f189,f166,f140])).
% 0.14/5.41 fof(f209,definition,(
% 0.14/5.41 sQ13_spl <=> (big_p(sk10))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f210,plain,(
% 0.14/5.41 big_p(sk10)|~sQ13_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f209])).
% 0.14/5.41 fof(f212,definition,(
% 0.14/5.41 sQ14_spl <=> (big_p(sk8))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f213,plain,(
% 0.14/5.41 big_p(sk8)|~sQ14_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f212])).
% 0.14/5.41 fof(f215,definition,(
% 0.14/5.41 sQ15_spl <=> (big_p(sk7))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f217,plain,(
% 0.14/5.41 ~big_p(sk7)|sQ15_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f215])).
% 0.14/5.41 fof(f218,definition,(
% 0.14/5.41 sQ16_spl <=> (big_p(sk9))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f220,plain,(
% 0.14/5.41 ~big_p(sk9)|sQ16_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f218])).
% 0.14/5.41 fof(f221,plain,(
% 0.14/5.41 sQ13_spl|sQ14_spl|~sQ15_spl|~sQ16_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f120,f209,f212,f215,f218])).
% 0.14/5.41 fof(f222,definition,(
% 0.14/5.41 sQ17_spl <=> (big_r(sk9,sk10))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f223,plain,(
% 0.14/5.41 big_r(sk9,sk10)|~sQ17_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f222])).
% 0.14/5.41 fof(f225,plain,(
% 0.14/5.41 sQ14_spl|sQ17_spl|~sQ15_spl|~sQ16_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f121,f212,f222,f215,f218])).
% 0.14/5.41 fof(f226,definition,(
% 0.14/5.41 sQ18_spl <=> (big_r(sk7,sk8))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f227,plain,(
% 0.14/5.41 big_r(sk7,sk8)|~sQ18_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f226])).
% 0.14/5.41 fof(f229,plain,(
% 0.14/5.41 sQ13_spl|sQ18_spl|~sQ15_spl|~sQ16_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f122,f209,f226,f215,f218])).
% 0.14/5.41 fof(f230,plain,(
% 0.14/5.41 sQ18_spl|sQ17_spl|~sQ15_spl|~sQ16_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f123,f226,f222,f215,f218])).
% 0.14/5.41 fof(f231,definition,(
% 0.14/5.41 ![X0,X1]: (sQ19_spl <=> (~big_p(X0)|~big_r(X1,X0)|~big_r(sk9,X1)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f232,plain,(
% 0.14/5.41 ![X0,X1]: (~big_p(X0)|~big_r(X1,X0)|~big_r(sk9,X1)|~sQ19_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f231])).
% 0.14/5.41 fof(f234,plain,(
% 0.14/5.41 sQ14_spl|sQ19_spl|~sQ15_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f125,f212,f231,f215])).
% 0.14/5.41 fof(f235,plain,(
% 0.14/5.41 sQ18_spl|sQ19_spl|~sQ15_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f127,f226,f231,f215])).
% 0.14/5.41 fof(f236,definition,(
% 0.14/5.41 ![X0,X1]: (sQ20_spl <=> (~big_p(X0)|~big_r(X1,X0)|~big_r(sk7,X1)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f237,plain,(
% 0.14/5.41 ![X0,X1]: (~big_p(X0)|~big_r(X1,X0)|~big_r(sk7,X1)|~sQ20_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f236])).
% 0.14/5.41 fof(f239,plain,(
% 0.14/5.41 sQ13_spl|sQ20_spl|~sQ16_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f129,f209,f236,f218])).
% 0.14/5.41 fof(f240,plain,(
% 0.14/5.41 sQ17_spl|sQ20_spl|~sQ16_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f131,f222,f236,f218])).
% 0.14/5.41 fof(f241,plain,(
% 0.14/5.41 sQ19_spl|sQ20_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f133,f231,f236])).
% 0.14/5.41 fof(f242,plain,(
% 0.14/5.41 $false|sQ2_spl),
% 0.14/5.41 inference(forward_subsumption_resolution,[status(thm)],[f142,f119])).
% 0.14/5.41 fof(f243,plain,(
% 0.14/5.41 sQ2_spl),
% 0.14/5.41 inference(contradiction_clause,[status(thm)],[f242])).
% 0.14/5.41 fof(f244,plain,(
% 0.14/5.41 ![X0]: (big_p(sk9)|~big_p(X0)|~big_r(sk4(sk9),X0)|~sQ3_spl|~sQ19_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f145,f232])).
% 0.14/5.41 fof(f245,definition,(
% 0.14/5.41 ![X0]: (sQ21_spl <=> (~big_p(X0)|~big_r(sk4(sk9),X0)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f246,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk4(sk9),X0)|~sQ21_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f245])).
% 0.14/5.41 fof(f248,plain,(
% 0.14/5.41 sQ16_spl|sQ21_spl|~sQ3_spl|~sQ19_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f244,f218,f245,f144,f231])).
% 0.14/5.41 fof(f249,plain,(
% 0.14/5.41 ~big_p(sk3(sk9))|big_p(sk9)|~sQ21_spl|~sQ4_spl),
% 0.14/5.41 inference(resolution,[status(thm)],[f246,f149])).
% 0.14/5.41 fof(f251,definition,(
% 0.14/5.41 sQ22_spl <=> (big_p(sk3(sk9)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f253,plain,(
% 0.14/5.41 ~big_p(sk3(sk9))|sQ22_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f251])).
% 0.14/5.41 fof(f254,plain,(
% 0.14/5.41 ~sQ22_spl|sQ16_spl|~sQ21_spl|~sQ4_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f249,f251,f218,f245,f148])).
% 0.14/5.41 fof(f262,plain,(
% 0.14/5.41 big_p(sk9)|sQ22_spl|~sQ0_spl),
% 0.14/5.41 inference(resolution,[status(thm)],[f253,f135])).
% 0.14/5.41 fof(f263,plain,(
% 0.14/5.41 $false|sQ16_spl|sQ22_spl|~sQ0_spl),
% 0.14/5.41 inference(forward_subsumption_resolution,[status(thm)],[f262,f220])).
% 0.14/5.41 fof(f264,plain,(
% 0.14/5.41 sQ16_spl|sQ22_spl|~sQ0_spl),
% 0.14/5.41 inference(contradiction_clause,[status(thm)],[f263])).
% 0.14/5.41 fof(f266,plain,(
% 0.14/5.41 ![X0,X1]: (~big_p(X0)|~big_r(sk2(sk7),X0)|~big_p(X1)|~big_r(sk7,X1)|~sQ20_spl|~sQ11_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f237,f184])).
% 0.14/5.41 fof(f267,plain,(
% 0.14/5.41 ![X0,X1]: (~big_p(X0)|~big_r(sk6(sk7),X0)|~big_p(X1)|~big_r(sk7,X1)|~sQ20_spl|~sQ7_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f237,f163])).
% 0.14/5.41 fof(f268,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk4(sk7),X0)|big_p(sk7)|~sQ20_spl|~sQ3_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f237,f145])).
% 0.14/5.41 fof(f269,definition,(
% 0.14/5.41 ![X0]: (sQ25_spl <=> (~big_p(X0)|~big_r(sk2(sk7),X0)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f270,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk2(sk7),X0)|~sQ25_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f269])).
% 0.14/5.41 fof(f272,definition,(
% 0.14/5.41 ![X1]: (sQ26_spl <=> (~big_p(X1)|~big_r(sk7,X1)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f273,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk7,X0)|~sQ26_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f272])).
% 0.14/5.41 fof(f275,plain,(
% 0.14/5.41 sQ25_spl|sQ26_spl|~sQ20_spl|~sQ11_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f266,f269,f272,f236,f183])).
% 0.14/5.41 fof(f276,definition,(
% 0.14/5.41 ![X0]: (sQ27_spl <=> (~big_p(X0)|~big_r(sk6(sk7),X0)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f277,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk6(sk7),X0)|~sQ27_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f276])).
% 0.14/5.41 fof(f279,plain,(
% 0.14/5.41 sQ27_spl|sQ26_spl|~sQ20_spl|~sQ7_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f267,f276,f272,f236,f162])).
% 0.14/5.41 fof(f280,definition,(
% 0.14/5.41 ![X0]: (sQ28_spl <=> (~big_p(X0)|~big_r(sk4(sk7),X0)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f281,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk4(sk7),X0)|~sQ28_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f280])).
% 0.14/5.41 fof(f283,plain,(
% 0.14/5.41 sQ28_spl|sQ15_spl|~sQ20_spl|~sQ3_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f268,f280,f215,f236,f144])).
% 0.14/5.41 fof(f284,plain,(
% 0.14/5.41 ~big_p(sk8)|~sQ26_spl|~sQ18_spl),
% 0.14/5.41 inference(resolution,[status(thm)],[f273,f227])).
% 0.14/5.41 fof(f286,plain,(
% 0.14/5.41 $false|~sQ14_spl|~sQ26_spl|~sQ18_spl),
% 0.14/5.41 inference(forward_subsumption_resolution,[status(thm)],[f284,f213])).
% 0.14/5.41 fof(f287,plain,(
% 0.14/5.41 ~sQ14_spl|~sQ26_spl|~sQ18_spl),
% 0.14/5.41 inference(contradiction_clause,[status(thm)],[f286])).
% 0.14/5.41 fof(f305,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk2(sk9),X0)|big_p(sk9)|~sQ19_spl|~sQ5_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f232,f153])).
% 0.14/5.41 fof(f306,plain,(
% 0.14/5.41 ![X0,X1]: (~big_p(X0)|~big_r(sk2(sk9),X0)|~big_p(X1)|~big_r(sk9,X1)|~sQ19_spl|~sQ11_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f232,f184])).
% 0.14/5.41 fof(f308,definition,(
% 0.14/5.41 ![X0]: (sQ32_spl <=> (~big_p(X0)|~big_r(sk2(sk9),X0)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f309,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk2(sk9),X0)|~sQ32_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f308])).
% 0.14/5.41 fof(f311,plain,(
% 0.14/5.41 sQ32_spl|sQ16_spl|~sQ19_spl|~sQ5_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f305,f308,f218,f231,f152])).
% 0.14/5.41 fof(f312,definition,(
% 0.14/5.41 ![X1]: (sQ33_spl <=> (~big_p(X1)|~big_r(sk9,X1)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f313,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk9,X0)|~sQ33_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f312])).
% 0.14/5.41 fof(f315,plain,(
% 0.14/5.41 sQ32_spl|sQ33_spl|~sQ19_spl|~sQ11_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f306,f308,f312,f231,f183])).
% 0.14/5.41 fof(f331,plain,(
% 0.14/5.41 ~big_p(sk10)|~sQ33_spl|~sQ17_spl),
% 0.14/5.41 inference(resolution,[status(thm)],[f313,f223])).
% 0.14/5.41 fof(f335,plain,(
% 0.14/5.41 $false|~sQ13_spl|~sQ33_spl|~sQ17_spl),
% 0.14/5.41 inference(forward_subsumption_resolution,[status(thm)],[f331,f210])).
% 0.14/5.41 fof(f336,plain,(
% 0.14/5.41 ~sQ13_spl|~sQ33_spl|~sQ17_spl),
% 0.14/5.41 inference(contradiction_clause,[status(thm)],[f335])).
% 0.14/5.41 fof(f352,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk2(sk7),X0)|big_p(sk7)|~sQ20_spl|~sQ5_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f237,f153])).
% 0.14/5.41 fof(f355,plain,(
% 0.14/5.41 sQ25_spl|sQ15_spl|~sQ20_spl|~sQ5_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f352,f269,f215,f236,f152])).
% 0.14/5.41 fof(f366,plain,(
% 0.14/5.41 ![X0]: (~big_p(sk5(sk7))|~big_p(X0)|~big_r(sk7,X0)|~sQ27_spl|~sQ8_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f277,f167])).
% 0.14/5.41 fof(f369,definition,(
% 0.14/5.41 sQ40_spl <=> (big_p(sk5(sk7)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f371,plain,(
% 0.14/5.41 ~big_p(sk5(sk7))|sQ40_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f369])).
% 0.14/5.41 fof(f372,plain,(
% 0.14/5.41 ~sQ40_spl|sQ26_spl|~sQ27_spl|~sQ8_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f366,f369,f272,f276,f166])).
% 0.14/5.41 fof(f381,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk7,X0)|sQ40_spl|~sQ6_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f371,f159])).
% 0.14/5.41 fof(f382,plain,(
% 0.14/5.41 sQ26_spl|sQ40_spl|~sQ6_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f381,f272,f369,f158])).
% 0.14/5.41 fof(f383,plain,(
% 0.14/5.41 ![X0]: (~big_p(sk1(sk7))|~big_p(X0)|~big_r(sk7,X0)|~sQ25_spl|~sQ12_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f270,f190])).
% 0.14/5.41 fof(f384,plain,(
% 0.14/5.41 ~big_p(sk1(sk7))|big_p(sk7)|~sQ25_spl|~sQ9_spl),
% 0.14/5.41 inference(resolution,[status(thm)],[f270,f174])).
% 0.14/5.41 fof(f387,definition,(
% 0.14/5.41 sQ43_spl <=> (big_p(sk1(sk7)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f389,plain,(
% 0.14/5.41 ~big_p(sk1(sk7))|sQ43_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f387])).
% 0.14/5.41 fof(f390,plain,(
% 0.14/5.41 ~sQ43_spl|sQ26_spl|~sQ25_spl|~sQ12_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f383,f387,f272,f269,f189])).
% 0.14/5.41 fof(f391,plain,(
% 0.14/5.41 ~sQ43_spl|sQ15_spl|~sQ25_spl|~sQ9_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f384,f387,f215,f269,f173])).
% 0.14/5.41 fof(f400,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk7,X0)|sQ43_spl|~sQ10_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f389,f180])).
% 0.14/5.41 fof(f401,plain,(
% 0.14/5.41 big_p(sk7)|sQ43_spl|~sQ1_spl),
% 0.14/5.41 inference(resolution,[status(thm)],[f389,f138])).
% 0.14/5.41 fof(f402,plain,(
% 0.14/5.41 sQ26_spl|sQ43_spl|~sQ10_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f400,f272,f387,f179])).
% 0.14/5.41 fof(f403,plain,(
% 0.14/5.41 $false|sQ15_spl|sQ43_spl|~sQ1_spl),
% 0.14/5.41 inference(forward_subsumption_resolution,[status(thm)],[f401,f217])).
% 0.14/5.41 fof(f404,plain,(
% 0.14/5.41 sQ15_spl|sQ43_spl|~sQ1_spl),
% 0.14/5.41 inference(contradiction_clause,[status(thm)],[f403])).
% 0.14/5.41 fof(f413,plain,(
% 0.14/5.41 ![X0]: (~big_p(sk1(sk9))|~big_p(X0)|~big_r(sk9,X0)|~sQ32_spl|~sQ12_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f309,f190])).
% 0.14/5.41 fof(f416,definition,(
% 0.14/5.41 sQ46_spl <=> (big_p(sk1(sk9)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f418,plain,(
% 0.14/5.41 ~big_p(sk1(sk9))|sQ46_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f416])).
% 0.14/5.41 fof(f419,plain,(
% 0.14/5.41 ~sQ46_spl|sQ33_spl|~sQ32_spl|~sQ12_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f413,f416,f312,f308,f189])).
% 0.14/5.41 fof(f431,plain,(
% 0.14/5.41 big_p(sk9)|~sQ1_spl|sQ46_spl),
% 0.14/5.41 inference(resolution,[status(thm)],[f138,f418])).
% 0.14/5.41 fof(f432,plain,(
% 0.14/5.41 ![X0,X1]: (~big_p(X0)|~big_r(sk6(sk9),X0)|~big_p(X1)|~big_r(sk9,X1)|~sQ19_spl|~sQ7_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f232,f163])).
% 0.14/5.41 fof(f434,definition,(
% 0.14/5.41 ![X0]: (sQ50_spl <=> (~big_p(X0)|~big_r(sk6(sk9),X0)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f435,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk6(sk9),X0)|~sQ50_spl)),
% 0.14/5.41 inference(component_clause,[status(thm)],[f434])).
% 0.14/5.41 fof(f437,plain,(
% 0.14/5.41 sQ50_spl|sQ33_spl|~sQ19_spl|~sQ7_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f432,f434,f312,f231,f162])).
% 0.14/5.41 fof(f447,plain,(
% 0.14/5.41 ![X0]: (~big_p(sk5(sk9))|~big_p(X0)|~big_r(sk9,X0)|~sQ50_spl|~sQ8_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f435,f167])).
% 0.14/5.41 fof(f450,definition,(
% 0.14/5.41 sQ52_spl <=> (big_p(sk5(sk9)))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f452,plain,(
% 0.14/5.41 ~big_p(sk5(sk9))|sQ52_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f450])).
% 0.14/5.41 fof(f453,plain,(
% 0.14/5.41 ~sQ52_spl|sQ33_spl|~sQ50_spl|~sQ8_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f447,f450,f312,f434,f166])).
% 0.14/5.41 fof(f465,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk9,X0)|sQ52_spl|~sQ6_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f452,f159])).
% 0.14/5.41 fof(f466,plain,(
% 0.14/5.41 sQ33_spl|sQ52_spl|~sQ6_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f465,f312,f450,f158])).
% 0.14/5.41 fof(f468,plain,(
% 0.14/5.41 ![X0]: (~big_p(X0)|~big_r(sk9,X0)|~sQ10_spl|sQ46_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f180,f418])).
% 0.14/5.41 fof(f469,plain,(
% 0.14/5.41 sQ33_spl|~sQ10_spl|sQ46_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f468,f312,f179,f416])).
% 0.14/5.42 fof(f474,plain,(
% 0.14/5.42 ~big_p(sk3(sk7))|big_p(sk7)|~sQ28_spl|~sQ4_spl),
% 0.14/5.42 inference(resolution,[status(thm)],[f281,f149])).
% 0.14/5.42 fof(f476,definition,(
% 0.14/5.42 sQ56_spl <=> (big_p(sk3(sk7)))),
% 0.14/5.42 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.14/5.42 fof(f478,plain,(
% 0.14/5.42 ~big_p(sk3(sk7))|sQ56_spl),
% 0.14/5.42 inference(component_clause,[status(thm)],[f476])).
% 0.14/5.42 fof(f479,plain,(
% 0.14/5.42 ~sQ56_spl|sQ15_spl|~sQ28_spl|~sQ4_spl),
% 0.14/5.42 inference(split_clause,[status(thm)],[f474,f476,f215,f280,f148])).
% 0.14/5.42 fof(f481,plain,(
% 0.14/5.42 big_p(sk7)|sQ56_spl|~sQ0_spl),
% 0.14/5.42 inference(resolution,[status(thm)],[f478,f135])).
% 0.14/5.42 fof(f482,plain,(
% 0.14/5.42 sQ15_spl|sQ56_spl|~sQ0_spl),
% 0.14/5.42 inference(split_clause,[status(thm)],[f481,f215,f476,f134])).
% 0.14/5.42 fof(f500,plain,(
% 0.14/5.42 big_p(sk9)|~big_p(sk1(sk9))|~sQ9_spl|~sQ32_spl),
% 0.14/5.42 inference(resolution,[status(thm)],[f174,f309])).
% 0.14/5.42 fof(f501,plain,(
% 0.14/5.42 sQ16_spl|~sQ46_spl|~sQ9_spl|~sQ32_spl),
% 0.14/5.42 inference(split_clause,[status(thm)],[f500,f218,f416,f173,f308])).
% 0.14/5.42 fof(f502,plain,(
% 0.14/5.42 sQ16_spl|~sQ1_spl|sQ46_spl),
% 0.14/5.42 inference(split_clause,[status(thm)],[f431,f218,f137,f416])).
% 0.14/5.42 fof(f503,plain,(
% 0.14/5.42 $false),
% 0.14/5.42 inference(sat_refutation,[status(thm)],[f143,f147,f151,f155,f156,f157,f161,f169,f170,f172,f176,f177,f178,f182,f186,f192,f194,f195,f196,f197,f199,f200,f201,f202,f203,f204,f205,f206,f207,f208,f221,f225,f229,f230,f234,f235,f239,f240,f241,f243,f248,f254,f264,f275,f279,f283,f287,f311,f315,f336,f355,f372,f382,f390,f391,f402,f404,f419,f437,f453,f466,f469,f479,f482,f501,f502])).
% 0.14/5.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.43 % Elapsed time: 0.053457 seconds
% 0.14/5.43 % CPU time: 0.161667 seconds
% 0.14/5.43 % Total memory used: 19.303 MB
% 0.14/5.43 % Net memory used: 19.115 MB
%------------------------------------------------------------------------------