%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN036-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:45 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN036-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n007.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 10:37:20 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.38 % Refutation found
% 0.13/0.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.38 fof(f1,negated_conjecture,(
% 0.13/0.38 (![X,U,V,W,X1,X2]: (( big_p(X)| big_p(f1(X))| ~ big_q(U)| big_p(V)| big_q(f2(W))| big_q(W)| ~ big_p(X1)| big_q(X2) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f3,negated_conjecture,(
% 0.13/0.38 (![X,U,V,W,X1,X2]: (( big_p(X)| big_p(f1(X))| ~ big_q(U)| big_p(V)| ~ big_q(f2(W))| ~ big_q(W)| ~ big_p(X1)| big_q(X2) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f4,negated_conjecture,(
% 0.13/0.38 (![X,U,V,W]: (( big_p(X)| big_p(f1(X))| ~ big_q(U)| big_p(V)| ~ big_q(f2(W))| ~ big_q(W)| big_p(c6)| ~ big_q(c7) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f5,negated_conjecture,(
% 0.13/0.38 (![X,U,V,Z,X5]: (( big_p(X)| big_p(f1(X))| ~ big_q(U)| big_p(V)| ~ big_q(Z)| big_q(c8)| big_p(c9)| big_q(X5) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f6,negated_conjecture,(
% 0.13/0.38 (![X,U,V,Z,X6]: (( big_p(X)| big_p(f1(X))| ~ big_q(U)| big_p(V)| ~ big_q(Z)| big_q(c8)| ~ big_p(X6)| ~ big_q(c10) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f7,negated_conjecture,(
% 0.13/0.38 (![X,U,V,Z,X5]: (( big_p(X)| big_p(f1(X))| ~ big_q(U)| big_p(V)| big_q(Z)| ~ big_q(c8)| big_p(c9)| big_q(X5) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f8,negated_conjecture,(
% 0.13/0.38 (![X,U,V,Z,X6]: (( big_p(X)| big_p(f1(X))| ~ big_q(U)| big_p(V)| big_q(Z)| ~ big_q(c8)| ~ big_p(X6)| ~ big_q(c10) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f9,negated_conjecture,(
% 0.13/0.38 (![X,W,X1,X2]: (( big_p(X)| big_p(f1(X))| big_q(c1)| ~ big_p(c2)| big_q(f2(W))| big_q(W)| ~ big_p(X1)| big_q(X2) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f17,negated_conjecture,(
% 0.13/0.38 (![X,U,V,W,X1,X2]: (( ~ big_p(X)| ~ big_p(f1(X))| ~ big_q(U)| big_p(V)| big_q(f2(W))| big_q(W)| ~ big_p(X1)| big_q(X2) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f19,negated_conjecture,(
% 0.13/0.38 (![X,U,V,W,X1,X2]: (( ~ big_p(X)| ~ big_p(f1(X))| ~ big_q(U)| big_p(V)| ~ big_q(f2(W))| ~ big_q(W)| ~ big_p(X1)| big_q(X2) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f21,negated_conjecture,(
% 0.13/0.38 (![X,U,V,Z,X5]: (( ~ big_p(X)| ~ big_p(f1(X))| ~ big_q(U)| big_p(V)| ~ big_q(Z)| big_q(c8)| big_p(c9)| big_q(X5) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f22,negated_conjecture,(
% 0.13/0.38 (![X,U,V,Z,X6]: (( ~ big_p(X)| ~ big_p(f1(X))| ~ big_q(U)| big_p(V)| ~ big_q(Z)| big_q(c8)| ~ big_p(X6)| ~ big_q(c10) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f23,negated_conjecture,(
% 0.13/0.38 (![X,U,V,Z,X5]: (( ~ big_p(X)| ~ big_p(f1(X))| ~ big_q(U)| big_p(V)| big_q(Z)| ~ big_q(c8)| big_p(c9)| big_q(X5) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f24,negated_conjecture,(
% 0.13/0.38 (![X,U,V,Z,X6]: (( ~ big_p(X)| ~ big_p(f1(X))| ~ big_q(U)| big_p(V)| big_q(Z)| ~ big_q(c8)| ~ big_p(X6)| ~ big_q(c10) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f25,negated_conjecture,(
% 0.13/0.38 (![X,W,X1,X2]: (( ~ big_p(X)| ~ big_p(f1(X))| big_q(c1)| ~ big_p(c2)| big_q(f2(W))| big_q(W)| ~ big_p(X1)| big_q(X2) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f33,negated_conjecture,(
% 0.13/0.38 (![Y,X3,W,X1,X2]: (( ~ big_p(c3)| big_p(Y)| big_q(c4)| big_p(X3)| big_q(f2(W))| big_q(W)| ~ big_p(X1)| big_q(X2) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f49,negated_conjecture,(
% 0.13/0.38 (![Y,X3,W,X1,X2]: (( big_p(c3)| ~ big_p(Y)| big_q(c4)| big_p(X3)| big_q(f2(W))| big_q(W)| ~ big_p(X1)| big_q(X2) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f65,negated_conjecture,(
% 0.13/0.38 (![X7,X8,X9,X13,X14,X15]: (( ~ big_p(c11)| big_p(X7)| ~ big_q(X8)| big_p(X9)| ~ big_q(X13)| big_q(c16)| ~ big_p(X14)| big_q(X15) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f67,negated_conjecture,(
% 0.13/0.38 (![X7,X8,X9,X13,X14,X15]: (( ~ big_p(c11)| big_p(X7)| ~ big_q(X8)| big_p(X9)| big_q(X13)| ~ big_q(c16)| ~ big_p(X14)| big_q(X15) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f72,negated_conjecture,(
% 0.13/0.38 (![X7,X8,X9,X16,X18]: (( ~ big_p(c11)| big_p(X7)| ~ big_q(X8)| big_p(X9)| ~ big_q(f4(X16))| ~ big_q(X16)| ~ big_p(X18)| ~ big_q(c20) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f81,negated_conjecture,(
% 0.13/0.38 (![X7,X8,X9,X13,X14,X15]: (( big_p(c11)| ~ big_p(X7)| ~ big_q(X8)| big_p(X9)| ~ big_q(X13)| big_q(c16)| ~ big_p(X14)| big_q(X15) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f83,negated_conjecture,(
% 0.13/0.38 (![X7,X8,X9,X13,X14,X15]: (( big_p(c11)| ~ big_p(X7)| ~ big_q(X8)| big_p(X9)| big_q(X13)| ~ big_q(c16)| ~ big_p(X14)| big_q(X15) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f88,negated_conjecture,(
% 0.13/0.38 (![X7,X8,X9,X16,X18]: (( big_p(c11)| ~ big_p(X7)| ~ big_q(X8)| big_p(X9)| ~ big_q(f4(X16))| ~ big_q(X16)| ~ big_p(X18)| ~ big_q(c20) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f101,negated_conjecture,(
% 0.13/0.38 (![X10,X11,X16,X17]: (( big_p(X10)| big_p(f3(X10))| big_q(c14)| big_p(X11)| big_q(f4(X16))| big_q(X16)| big_p(c19)| big_q(X17) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f121,negated_conjecture,(
% 0.13/0.38 (![X10,X12,X13,X14,X15]: (( ~ big_p(X10)| ~ big_p(f3(X10))| ~ big_q(X12)| ~ big_p(c15)| ~ big_q(X13)| big_q(c16)| ~ big_p(X14)| big_q(X15) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f123,negated_conjecture,(
% 0.13/0.38 (![X10,X12,X13,X14,X15]: (( ~ big_p(X10)| ~ big_p(f3(X10))| ~ big_q(X12)| ~ big_p(c15)| big_q(X13)| ~ big_q(c16)| ~ big_p(X14)| big_q(X15) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f128,negated_conjecture,(
% 0.13/0.38 (![X10,X12,X16,X18]: (( ~ big_p(X10)| ~ big_p(f3(X10))| ~ big_q(X12)| ~ big_p(c15)| ~ big_q(f4(X16))| ~ big_q(X16)| ~ big_p(X18)| ~ big_q(c20) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f129,plain,(
% 0.13/0.38 ((![W]: (((((![X]: (big_p(X)|big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|big_q(f2(W)))|big_q(W)))|(![X1]: ~big_p(X1)))|(![X2]: big_q(X2))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f1])).
% 0.13/0.38 fof(f130,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4,X5]: (big_p(X0)|big_p(f1(X0))|~big_q(X1)|big_p(X2)|big_q(f2(X3))|big_q(X3)|~big_p(X4)|big_q(X5))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f129])).
% 0.13/0.38 fof(f133,plain,(
% 0.13/0.38 ((![W]: (((((![X]: (big_p(X)|big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|~big_q(f2(W)))|~big_q(W)))|(![X1]: ~big_p(X1)))|(![X2]: big_q(X2))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f3])).
% 0.13/0.38 fof(f134,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4,X5]: (big_p(X0)|big_p(f1(X0))|~big_q(X1)|big_p(X2)|~big_q(f2(X3))|~big_q(X3)|~big_p(X4)|big_q(X5))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f133])).
% 0.13/0.38 fof(f135,plain,(
% 0.13/0.38 ((![W]: (((((![X]: (big_p(X)|big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|~big_q(f2(W)))|~big_q(W)))|big_p(c6))|~big_q(c7)),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f4])).
% 0.13/0.38 fof(f136,plain,(
% 0.13/0.38 ![X0,X1,X2,X3]: (big_p(X0)|big_p(f1(X0))|~big_q(X1)|big_p(X2)|~big_q(f2(X3))|~big_q(X3)|big_p(c6)|~big_q(c7))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f135])).
% 0.13/0.38 fof(f137,plain,(
% 0.13/0.38 ((((((![X]: (big_p(X)|big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|(![Z]: ~big_q(Z)))|big_q(c8))|big_p(c9))|(![X5]: big_q(X5))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f5])).
% 0.13/0.38 fof(f138,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (big_p(X0)|big_p(f1(X0))|~big_q(X1)|big_p(X2)|~big_q(X3)|big_q(c8)|big_p(c9)|big_q(X4))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f137])).
% 0.13/0.38 fof(f139,plain,(
% 0.13/0.38 ((((((![X]: (big_p(X)|big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|(![Z]: ~big_q(Z)))|big_q(c8))|(![X6]: ~big_p(X6)))|~big_q(c10)),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f6])).
% 0.13/0.38 fof(f140,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (big_p(X0)|big_p(f1(X0))|~big_q(X1)|big_p(X2)|~big_q(X3)|big_q(c8)|~big_p(X4)|~big_q(c10))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f139])).
% 0.13/0.38 fof(f141,plain,(
% 0.13/0.38 ((((((![X]: (big_p(X)|big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|(![Z]: big_q(Z)))|~big_q(c8))|big_p(c9))|(![X5]: big_q(X5))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f7])).
% 0.13/0.38 fof(f142,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (big_p(X0)|big_p(f1(X0))|~big_q(X1)|big_p(X2)|big_q(X3)|~big_q(c8)|big_p(c9)|big_q(X4))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f141])).
% 0.13/0.38 fof(f143,plain,(
% 0.13/0.38 ((((((![X]: (big_p(X)|big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|(![Z]: big_q(Z)))|~big_q(c8))|(![X6]: ~big_p(X6)))|~big_q(c10)),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f8])).
% 0.13/0.38 fof(f144,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (big_p(X0)|big_p(f1(X0))|~big_q(X1)|big_p(X2)|big_q(X3)|~big_q(c8)|~big_p(X4)|~big_q(c10))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f143])).
% 0.13/0.38 fof(f145,plain,(
% 0.13/0.38 ((![W]: (((((![X]: (big_p(X)|big_p(f1(X))))|big_q(c1))|~big_p(c2))|big_q(f2(W)))|big_q(W)))|(![X1]: ~big_p(X1)))|(![X2]: big_q(X2))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f9])).
% 0.13/0.38 fof(f146,plain,(
% 0.13/0.38 ![X0,X1,X2,X3]: (big_p(X0)|big_p(f1(X0))|big_q(c1)|~big_p(c2)|big_q(f2(X1))|big_q(X1)|~big_p(X2)|big_q(X3))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f145])).
% 0.13/0.38 fof(f161,plain,(
% 0.13/0.38 ((![W]: (((((![X]: (~big_p(X)|~big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|big_q(f2(W)))|big_q(W)))|(![X1]: ~big_p(X1)))|(![X2]: big_q(X2))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f17])).
% 0.13/0.38 fof(f162,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4,X5]: (~big_p(X0)|~big_p(f1(X0))|~big_q(X1)|big_p(X2)|big_q(f2(X3))|big_q(X3)|~big_p(X4)|big_q(X5))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f161])).
% 0.13/0.38 fof(f165,plain,(
% 0.13/0.38 ((![W]: (((((![X]: (~big_p(X)|~big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|~big_q(f2(W)))|~big_q(W)))|(![X1]: ~big_p(X1)))|(![X2]: big_q(X2))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f19])).
% 0.13/0.38 fof(f166,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4,X5]: (~big_p(X0)|~big_p(f1(X0))|~big_q(X1)|big_p(X2)|~big_q(f2(X3))|~big_q(X3)|~big_p(X4)|big_q(X5))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f165])).
% 0.13/0.38 fof(f169,plain,(
% 0.13/0.38 ((((((![X]: (~big_p(X)|~big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|(![Z]: ~big_q(Z)))|big_q(c8))|big_p(c9))|(![X5]: big_q(X5))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f21])).
% 0.13/0.38 fof(f170,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (~big_p(X0)|~big_p(f1(X0))|~big_q(X1)|big_p(X2)|~big_q(X3)|big_q(c8)|big_p(c9)|big_q(X4))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f169])).
% 0.13/0.38 fof(f171,plain,(
% 0.13/0.38 ((((((![X]: (~big_p(X)|~big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|(![Z]: ~big_q(Z)))|big_q(c8))|(![X6]: ~big_p(X6)))|~big_q(c10)),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f22])).
% 0.13/0.38 fof(f172,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (~big_p(X0)|~big_p(f1(X0))|~big_q(X1)|big_p(X2)|~big_q(X3)|big_q(c8)|~big_p(X4)|~big_q(c10))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f171])).
% 0.13/0.38 fof(f173,plain,(
% 0.13/0.38 ((((((![X]: (~big_p(X)|~big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|(![Z]: big_q(Z)))|~big_q(c8))|big_p(c9))|(![X5]: big_q(X5))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f23])).
% 0.13/0.38 fof(f174,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (~big_p(X0)|~big_p(f1(X0))|~big_q(X1)|big_p(X2)|big_q(X3)|~big_q(c8)|big_p(c9)|big_q(X4))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f173])).
% 0.13/0.38 fof(f175,plain,(
% 0.13/0.38 ((((((![X]: (~big_p(X)|~big_p(f1(X))))|(![U]: ~big_q(U)))|(![V]: big_p(V)))|(![Z]: big_q(Z)))|~big_q(c8))|(![X6]: ~big_p(X6)))|~big_q(c10)),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f24])).
% 0.13/0.38 fof(f176,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (~big_p(X0)|~big_p(f1(X0))|~big_q(X1)|big_p(X2)|big_q(X3)|~big_q(c8)|~big_p(X4)|~big_q(c10))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f175])).
% 0.13/0.38 fof(f177,plain,(
% 0.13/0.38 ((![W]: (((((![X]: (~big_p(X)|~big_p(f1(X))))|big_q(c1))|~big_p(c2))|big_q(f2(W)))|big_q(W)))|(![X1]: ~big_p(X1)))|(![X2]: big_q(X2))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f25])).
% 0.13/0.38 fof(f178,plain,(
% 0.13/0.38 ![X0,X1,X2,X3]: (~big_p(X0)|~big_p(f1(X0))|big_q(c1)|~big_p(c2)|big_q(f2(X1))|big_q(X1)|~big_p(X2)|big_q(X3))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f177])).
% 0.13/0.38 fof(f193,plain,(
% 0.13/0.38 ((![W]: (((((~big_p(c3)|(![Y]: big_p(Y)))|big_q(c4))|(![X3]: big_p(X3)))|big_q(f2(W)))|big_q(W)))|(![X1]: ~big_p(X1)))|(![X2]: big_q(X2))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f33])).
% 0.13/0.38 fof(f194,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (~big_p(c3)|big_p(X0)|big_q(c4)|big_p(X1)|big_q(f2(X2))|big_q(X2)|~big_p(X3)|big_q(X4))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f193])).
% 0.13/0.38 fof(f225,plain,(
% 0.13/0.38 ((![W]: (((((big_p(c3)|(![Y]: ~big_p(Y)))|big_q(c4))|(![X3]: big_p(X3)))|big_q(f2(W)))|big_q(W)))|(![X1]: ~big_p(X1)))|(![X2]: big_q(X2))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f49])).
% 0.13/0.38 fof(f226,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (big_p(c3)|~big_p(X0)|big_q(c4)|big_p(X1)|big_q(f2(X2))|big_q(X2)|~big_p(X3)|big_q(X4))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f225])).
% 0.13/0.38 fof(f257,plain,(
% 0.13/0.38 ((((((~big_p(c11)|(![X7]: big_p(X7)))|(![X8]: ~big_q(X8)))|(![X9]: big_p(X9)))|(![X13]: ~big_q(X13)))|big_q(c16))|(![X14]: ~big_p(X14)))|(![X15]: big_q(X15))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f65])).
% 0.13/0.38 fof(f258,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4,X5]: (~big_p(c11)|big_p(X0)|~big_q(X1)|big_p(X2)|~big_q(X3)|big_q(c16)|~big_p(X4)|big_q(X5))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f257])).
% 0.13/0.38 fof(f261,plain,(
% 0.13/0.38 ((((((~big_p(c11)|(![X7]: big_p(X7)))|(![X8]: ~big_q(X8)))|(![X9]: big_p(X9)))|(![X13]: big_q(X13)))|~big_q(c16))|(![X14]: ~big_p(X14)))|(![X15]: big_q(X15))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f67])).
% 0.13/0.38 fof(f262,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4,X5]: (~big_p(c11)|big_p(X0)|~big_q(X1)|big_p(X2)|big_q(X3)|~big_q(c16)|~big_p(X4)|big_q(X5))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f261])).
% 0.13/0.38 fof(f271,plain,(
% 0.13/0.38 ((![X16]: (((((~big_p(c11)|(![X7]: big_p(X7)))|(![X8]: ~big_q(X8)))|(![X9]: big_p(X9)))|~big_q(f4(X16)))|~big_q(X16)))|(![X18]: ~big_p(X18)))|~big_q(c20)),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f72])).
% 0.13/0.38 fof(f272,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (~big_p(c11)|big_p(X0)|~big_q(X1)|big_p(X2)|~big_q(f4(X3))|~big_q(X3)|~big_p(X4)|~big_q(c20))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f271])).
% 0.13/0.38 fof(f289,plain,(
% 0.13/0.38 ((((((big_p(c11)|(![X7]: ~big_p(X7)))|(![X8]: ~big_q(X8)))|(![X9]: big_p(X9)))|(![X13]: ~big_q(X13)))|big_q(c16))|(![X14]: ~big_p(X14)))|(![X15]: big_q(X15))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f81])).
% 0.13/0.38 fof(f290,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4,X5]: (big_p(c11)|~big_p(X0)|~big_q(X1)|big_p(X2)|~big_q(X3)|big_q(c16)|~big_p(X4)|big_q(X5))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f289])).
% 0.13/0.38 fof(f293,plain,(
% 0.13/0.38 ((((((big_p(c11)|(![X7]: ~big_p(X7)))|(![X8]: ~big_q(X8)))|(![X9]: big_p(X9)))|(![X13]: big_q(X13)))|~big_q(c16))|(![X14]: ~big_p(X14)))|(![X15]: big_q(X15))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f83])).
% 0.13/0.38 fof(f294,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4,X5]: (big_p(c11)|~big_p(X0)|~big_q(X1)|big_p(X2)|big_q(X3)|~big_q(c16)|~big_p(X4)|big_q(X5))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f293])).
% 0.13/0.38 fof(f303,plain,(
% 0.13/0.38 ((![X16]: (((((big_p(c11)|(![X7]: ~big_p(X7)))|(![X8]: ~big_q(X8)))|(![X9]: big_p(X9)))|~big_q(f4(X16)))|~big_q(X16)))|(![X18]: ~big_p(X18)))|~big_q(c20)),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f88])).
% 0.13/0.38 fof(f304,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (big_p(c11)|~big_p(X0)|~big_q(X1)|big_p(X2)|~big_q(f4(X3))|~big_q(X3)|~big_p(X4)|~big_q(c20))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f303])).
% 0.13/0.38 fof(f329,plain,(
% 0.13/0.38 ((![X16]: (((((![X10]: (big_p(X10)|big_p(f3(X10))))|big_q(c14))|(![X11]: big_p(X11)))|big_q(f4(X16)))|big_q(X16)))|big_p(c19))|(![X17]: big_q(X17))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f101])).
% 0.13/0.38 fof(f330,plain,(
% 0.13/0.38 ![X0,X1,X2,X3]: (big_p(X0)|big_p(f3(X0))|big_q(c14)|big_p(X1)|big_q(f4(X2))|big_q(X2)|big_p(c19)|big_q(X3))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f329])).
% 0.13/0.38 fof(f369,plain,(
% 0.13/0.38 ((((((![X10]: (~big_p(X10)|~big_p(f3(X10))))|(![X12]: ~big_q(X12)))|~big_p(c15))|(![X13]: ~big_q(X13)))|big_q(c16))|(![X14]: ~big_p(X14)))|(![X15]: big_q(X15))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f121])).
% 0.13/0.38 fof(f370,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (~big_p(X0)|~big_p(f3(X0))|~big_q(X1)|~big_p(c15)|~big_q(X2)|big_q(c16)|~big_p(X3)|big_q(X4))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f369])).
% 0.13/0.38 fof(f373,plain,(
% 0.13/0.38 ((((((![X10]: (~big_p(X10)|~big_p(f3(X10))))|(![X12]: ~big_q(X12)))|~big_p(c15))|(![X13]: big_q(X13)))|~big_q(c16))|(![X14]: ~big_p(X14)))|(![X15]: big_q(X15))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f123])).
% 0.13/0.38 fof(f374,plain,(
% 0.13/0.38 ![X0,X1,X2,X3,X4]: (~big_p(X0)|~big_p(f3(X0))|~big_q(X1)|~big_p(c15)|big_q(X2)|~big_q(c16)|~big_p(X3)|big_q(X4))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f373])).
% 0.13/0.38 fof(f383,plain,(
% 0.13/0.38 ((![X16]: (((((![X10]: (~big_p(X10)|~big_p(f3(X10))))|(![X12]: ~big_q(X12)))|~big_p(c15))|~big_q(f4(X16)))|~big_q(X16)))|(![X18]: ~big_p(X18)))|~big_q(c20)),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f128])).
% 0.13/0.38 fof(f384,plain,(
% 0.13/0.38 ![X0,X1,X2,X3]: (~big_p(X0)|~big_p(f3(X0))|~big_q(X1)|~big_p(c15)|~big_q(f4(X2))|~big_q(X2)|~big_p(X3)|~big_q(c20))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f383])).
% 0.13/0.38 fof(f385,definition,(
% 0.13/0.38 ![X0]: (sQ0_spl <=> (big_p(X0)|big_p(f1(X0))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f386,plain,(
% 0.13/0.38 ![X0]: (big_p(X0)|big_p(f1(X0))|~sQ0_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f385])).
% 0.13/0.38 fof(f388,definition,(
% 0.13/0.38 ![X1]: (sQ1_spl <=> (~big_q(X1)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f389,plain,(
% 0.13/0.38 ![X0]: (~big_q(X0)|~sQ1_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f388])).
% 0.13/0.38 fof(f391,definition,(
% 0.13/0.38 ![X2]: (sQ2_spl <=> (big_p(X2)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f392,plain,(
% 0.13/0.38 ![X0]: (big_p(X0)|~sQ2_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f391])).
% 0.13/0.38 fof(f394,definition,(
% 0.13/0.38 ![X3]: (sQ3_spl <=> (big_q(f2(X3))|big_q(X3)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f395,plain,(
% 0.13/0.38 ![X0]: (big_q(f2(X0))|big_q(X0)|~sQ3_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f394])).
% 0.13/0.38 fof(f397,definition,(
% 0.13/0.38 ![X4]: (sQ4_spl <=> (~big_p(X4)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f398,plain,(
% 0.13/0.38 ![X0]: (~big_p(X0)|~sQ4_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f397])).
% 0.13/0.38 fof(f400,definition,(
% 0.13/0.38 ![X5]: (sQ5_spl <=> (big_q(X5)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f401,plain,(
% 0.13/0.38 ![X0]: (big_q(X0)|~sQ5_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f400])).
% 0.13/0.38 fof(f403,plain,(
% 0.13/0.38 sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl|sQ4_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f130,f385,f388,f391,f394,f397,f400])).
% 0.13/0.38 fof(f404,definition,(
% 0.13/0.38 sQ6_spl <=> (big_p(c6))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f405,plain,(
% 0.13/0.38 big_p(c6)|~sQ6_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f404])).
% 0.13/0.38 fof(f407,definition,(
% 0.13/0.38 sQ7_spl <=> (big_q(c7))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f409,plain,(
% 0.13/0.38 ~big_q(c7)|sQ7_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f407])).
% 0.13/0.38 fof(f411,definition,(
% 0.13/0.38 ![X3]: (sQ8_spl <=> (~big_q(f2(X3))|~big_q(X3)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f412,plain,(
% 0.13/0.38 ![X0]: (~big_q(f2(X0))|~big_q(X0)|~sQ8_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f411])).
% 0.13/0.38 fof(f414,plain,(
% 0.13/0.38 sQ0_spl|sQ1_spl|sQ2_spl|sQ8_spl|sQ4_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f134,f385,f388,f391,f411,f397,f400])).
% 0.13/0.38 fof(f415,plain,(
% 0.13/0.38 sQ0_spl|sQ1_spl|sQ2_spl|sQ8_spl|sQ6_spl|~sQ7_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f136,f385,f388,f391,f411,f404,f407])).
% 0.13/0.38 fof(f416,definition,(
% 0.13/0.38 sQ9_spl <=> (big_q(c8))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f419,definition,(
% 0.13/0.38 sQ10_spl <=> (big_p(c9))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f420,plain,(
% 0.13/0.38 big_p(c9)|~sQ10_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f419])).
% 0.13/0.38 fof(f422,plain,(
% 0.13/0.38 sQ0_spl|sQ1_spl|sQ2_spl|sQ9_spl|sQ10_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f138,f385,f388,f391,f416,f419,f400])).
% 0.13/0.38 fof(f423,definition,(
% 0.13/0.38 sQ11_spl <=> (big_q(c10))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f425,plain,(
% 0.13/0.38 ~big_q(c10)|sQ11_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f423])).
% 0.13/0.38 fof(f426,plain,(
% 0.13/0.38 sQ0_spl|sQ1_spl|sQ2_spl|sQ9_spl|sQ4_spl|~sQ11_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f140,f385,f388,f391,f416,f397,f423])).
% 0.13/0.38 fof(f427,plain,(
% 0.13/0.38 sQ0_spl|sQ1_spl|sQ2_spl|sQ5_spl|~sQ9_spl|sQ10_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f142,f385,f388,f391,f400,f416,f419])).
% 0.13/0.38 fof(f428,plain,(
% 0.13/0.38 sQ0_spl|sQ1_spl|sQ2_spl|sQ5_spl|~sQ9_spl|sQ4_spl|~sQ11_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f144,f385,f388,f391,f400,f416,f397,f423])).
% 0.13/0.38 fof(f429,definition,(
% 0.13/0.38 sQ12_spl <=> (big_q(c1))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f430,plain,(
% 0.13/0.38 big_q(c1)|~sQ12_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f429])).
% 0.13/0.38 fof(f432,definition,(
% 0.13/0.38 sQ13_spl <=> (big_p(c2))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f434,plain,(
% 0.13/0.38 ~big_p(c2)|sQ13_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f432])).
% 0.13/0.38 fof(f435,plain,(
% 0.13/0.38 sQ0_spl|sQ12_spl|~sQ13_spl|sQ3_spl|sQ4_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f146,f385,f429,f432,f394,f397,f400])).
% 0.13/0.38 fof(f443,definition,(
% 0.13/0.38 ![X0]: (sQ14_spl <=> (~big_p(X0)|~big_p(f1(X0))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f444,plain,(
% 0.13/0.38 ![X0]: (~big_p(X0)|~big_p(f1(X0))|~sQ14_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f443])).
% 0.13/0.38 fof(f446,plain,(
% 0.13/0.38 sQ14_spl|sQ1_spl|sQ2_spl|sQ3_spl|sQ4_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f162,f443,f388,f391,f394,f397,f400])).
% 0.13/0.38 fof(f448,plain,(
% 0.13/0.38 sQ14_spl|sQ1_spl|sQ2_spl|sQ8_spl|sQ4_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f166,f443,f388,f391,f411,f397,f400])).
% 0.13/0.38 fof(f450,plain,(
% 0.13/0.38 sQ14_spl|sQ1_spl|sQ2_spl|sQ9_spl|sQ10_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f170,f443,f388,f391,f416,f419,f400])).
% 0.13/0.38 fof(f451,plain,(
% 0.13/0.38 sQ14_spl|sQ1_spl|sQ2_spl|sQ9_spl|sQ4_spl|~sQ11_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f172,f443,f388,f391,f416,f397,f423])).
% 0.13/0.38 fof(f452,plain,(
% 0.13/0.38 sQ14_spl|sQ1_spl|sQ2_spl|sQ5_spl|~sQ9_spl|sQ10_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f174,f443,f388,f391,f400,f416,f419])).
% 0.13/0.38 fof(f453,plain,(
% 0.13/0.38 sQ14_spl|sQ1_spl|sQ2_spl|sQ5_spl|~sQ9_spl|sQ4_spl|~sQ11_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f176,f443,f388,f391,f400,f416,f397,f423])).
% 0.13/0.38 fof(f454,plain,(
% 0.13/0.38 sQ14_spl|sQ12_spl|~sQ13_spl|sQ3_spl|sQ4_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f178,f443,f429,f432,f394,f397,f400])).
% 0.13/0.38 fof(f462,definition,(
% 0.13/0.38 sQ15_spl <=> (big_p(c3))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f465,definition,(
% 0.13/0.38 sQ16_spl <=> (big_q(c4))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f466,plain,(
% 0.13/0.38 big_q(c4)|~sQ16_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f465])).
% 0.13/0.38 fof(f468,plain,(
% 0.13/0.38 ~sQ15_spl|sQ2_spl|sQ16_spl|sQ3_spl|sQ4_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f194,f462,f391,f465,f394,f397,f400])).
% 0.13/0.38 fof(f487,plain,(
% 0.13/0.38 sQ15_spl|sQ4_spl|sQ16_spl|sQ2_spl|sQ3_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f226,f462,f397,f465,f391,f394,f400])).
% 0.13/0.38 fof(f503,definition,(
% 0.13/0.38 sQ18_spl <=> (big_p(c11))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f506,definition,(
% 0.13/0.38 sQ19_spl <=> (big_q(c16))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f509,plain,(
% 0.13/0.38 ~sQ18_spl|sQ2_spl|sQ1_spl|sQ19_spl|sQ4_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f258,f503,f391,f388,f506,f397,f400])).
% 0.13/0.38 fof(f513,definition,(
% 0.13/0.38 sQ21_spl <=> (big_q(c18))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f515,plain,(
% 0.13/0.38 ~big_q(c18)|sQ21_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f513])).
% 0.13/0.38 fof(f517,plain,(
% 0.13/0.38 ~sQ18_spl|sQ2_spl|sQ1_spl|sQ5_spl|~sQ19_spl|sQ4_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f262,f503,f391,f388,f400,f506,f397])).
% 0.13/0.38 fof(f519,definition,(
% 0.13/0.38 ![X3]: (sQ22_spl <=> (big_q(f4(X3))|big_q(X3)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f520,plain,(
% 0.13/0.38 ![X0]: (big_q(f4(X0))|big_q(X0)|~sQ22_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f519])).
% 0.13/0.38 fof(f522,definition,(
% 0.13/0.38 sQ23_spl <=> (big_p(c19))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f523,plain,(
% 0.13/0.38 big_p(c19)|~sQ23_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f522])).
% 0.13/0.38 fof(f526,definition,(
% 0.13/0.38 sQ24_spl <=> (big_q(c20))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f528,plain,(
% 0.13/0.38 ~big_q(c20)|sQ24_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f526])).
% 0.13/0.38 fof(f530,definition,(
% 0.13/0.38 ![X3]: (sQ25_spl <=> (~big_q(f4(X3))|~big_q(X3)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f531,plain,(
% 0.13/0.38 ![X0]: (~big_q(f4(X0))|~big_q(X0)|~sQ25_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f530])).
% 0.13/0.38 fof(f534,plain,(
% 0.13/0.38 ~sQ18_spl|sQ2_spl|sQ1_spl|sQ25_spl|sQ4_spl|~sQ24_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f272,f503,f391,f388,f530,f397,f526])).
% 0.13/0.38 fof(f535,definition,(
% 0.13/0.38 sQ26_spl <=> (big_q(c12))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f536,plain,(
% 0.13/0.38 big_q(c12)|~sQ26_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f535])).
% 0.13/0.38 fof(f549,plain,(
% 0.13/0.38 sQ18_spl|sQ4_spl|sQ1_spl|sQ2_spl|sQ19_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f290,f503,f397,f388,f391,f506,f400])).
% 0.13/0.38 fof(f551,plain,(
% 0.13/0.38 sQ18_spl|sQ4_spl|sQ1_spl|sQ2_spl|sQ5_spl|~sQ19_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f294,f503,f397,f388,f391,f400,f506])).
% 0.13/0.38 fof(f556,plain,(
% 0.13/0.38 sQ18_spl|sQ4_spl|sQ1_spl|sQ2_spl|sQ25_spl|~sQ24_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f304,f503,f397,f388,f391,f530,f526])).
% 0.13/0.38 fof(f565,definition,(
% 0.13/0.38 ![X0]: (sQ28_spl <=> (big_p(X0)|big_p(f3(X0))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f566,plain,(
% 0.13/0.38 ![X0]: (big_p(X0)|big_p(f3(X0))|~sQ28_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f565])).
% 0.13/0.38 fof(f568,definition,(
% 0.13/0.38 sQ29_spl <=> (big_q(c14))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f569,plain,(
% 0.13/0.38 big_q(c14)|~sQ29_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f568])).
% 0.13/0.38 fof(f575,plain,(
% 0.13/0.38 sQ28_spl|sQ29_spl|sQ2_spl|sQ22_spl|sQ23_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f330,f565,f568,f391,f519,f522,f400])).
% 0.13/0.38 fof(f579,definition,(
% 0.13/0.38 sQ30_spl <=> (big_p(c15))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f581,plain,(
% 0.13/0.38 ~big_p(c15)|sQ30_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f579])).
% 0.13/0.38 fof(f590,definition,(
% 0.13/0.38 ![X0]: (sQ31_spl <=> (~big_p(X0)|~big_p(f3(X0))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f591,plain,(
% 0.13/0.38 ![X0]: (~big_p(X0)|~big_p(f3(X0))|~sQ31_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f590])).
% 0.13/0.38 fof(f601,plain,(
% 0.13/0.38 sQ31_spl|sQ1_spl|~sQ30_spl|sQ19_spl|sQ4_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f370,f590,f388,f579,f506,f397,f400])).
% 0.13/0.38 fof(f603,plain,(
% 0.13/0.38 sQ31_spl|sQ1_spl|~sQ30_spl|sQ5_spl|~sQ19_spl|sQ4_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f374,f590,f388,f579,f400,f506,f397])).
% 0.13/0.38 fof(f608,plain,(
% 0.13/0.38 sQ31_spl|sQ1_spl|~sQ30_spl|sQ25_spl|sQ4_spl|~sQ24_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f384,f590,f388,f579,f530,f397,f526])).
% 0.13/0.38 fof(f609,plain,(
% 0.13/0.38 $false|~sQ1_spl|~sQ5_spl),
% 0.13/0.38 inference(forward_subsumption_resolution,[status(thm)],[f401,f389])).
% 0.13/0.38 fof(f610,plain,(
% 0.13/0.38 ~sQ1_spl|~sQ5_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f609])).
% 0.13/0.38 fof(f611,plain,(
% 0.13/0.38 $false|~sQ4_spl|~sQ2_spl),
% 0.13/0.38 inference(forward_subsumption_resolution,[status(thm)],[f392,f398])).
% 0.13/0.38 fof(f612,plain,(
% 0.13/0.38 ~sQ4_spl|~sQ2_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f611])).
% 0.13/0.38 fof(f614,plain,(
% 0.13/0.38 ![X0]: (~big_p(X0)|~sQ2_spl|~sQ14_spl)),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f444,f392])).
% 0.13/0.38 fof(f615,plain,(
% 0.13/0.38 $false|~sQ2_spl|sQ13_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f434,f392])).
% 0.13/0.38 fof(f617,plain,(
% 0.13/0.38 ![X0]: (~big_p(X0)|~sQ2_spl|~sQ31_spl)),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f591,f392])).
% 0.13/0.38 fof(f618,plain,(
% 0.13/0.38 $false|~sQ2_spl|sQ30_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f581,f392])).
% 0.13/0.38 fof(f622,plain,(
% 0.13/0.38 $false|~sQ5_spl|sQ21_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f515,f401])).
% 0.13/0.38 fof(f623,plain,(
% 0.13/0.38 ![X0]: (~big_q(X0)|~sQ5_spl|~sQ8_spl)),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f412,f401])).
% 0.13/0.38 fof(f624,plain,(
% 0.13/0.38 $false|~sQ5_spl|sQ7_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f409,f401])).
% 0.13/0.38 fof(f625,plain,(
% 0.13/0.38 $false|~sQ5_spl|sQ11_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f425,f401])).
% 0.13/0.38 fof(f626,plain,(
% 0.13/0.38 ![X0]: (~big_q(X0)|~sQ5_spl|~sQ25_spl)),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f531,f401])).
% 0.13/0.38 fof(f627,plain,(
% 0.13/0.38 $false|~sQ5_spl|sQ24_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f528,f401])).
% 0.13/0.38 fof(f628,plain,(
% 0.13/0.38 ~sQ5_spl|sQ21_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f622])).
% 0.13/0.38 fof(f629,plain,(
% 0.13/0.38 $false|~sQ1_spl|~sQ26_spl),
% 0.13/0.38 inference(forward_subsumption_resolution,[status(thm)],[f536,f389])).
% 0.13/0.38 fof(f630,plain,(
% 0.13/0.38 ~sQ1_spl|~sQ26_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f629])).
% 0.13/0.38 fof(f631,plain,(
% 0.13/0.38 sQ4_spl|~sQ2_spl|~sQ14_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f614,f397,f391,f443])).
% 0.13/0.38 fof(f632,plain,(
% 0.13/0.38 ~sQ2_spl|sQ13_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f615])).
% 0.13/0.38 fof(f633,plain,(
% 0.13/0.38 $false|~sQ4_spl|~sQ23_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f523,f398])).
% 0.13/0.38 fof(f634,plain,(
% 0.13/0.38 ![X0]: (big_p(X0)|~sQ4_spl|~sQ28_spl)),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f566,f398])).
% 0.13/0.38 fof(f635,plain,(
% 0.13/0.38 $false|~sQ4_spl|~sQ10_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f420,f398])).
% 0.13/0.38 fof(f636,plain,(
% 0.13/0.38 $false|~sQ4_spl|~sQ6_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f405,f398])).
% 0.13/0.38 fof(f637,plain,(
% 0.13/0.38 ![X0]: (big_p(X0)|~sQ4_spl|~sQ0_spl)),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f386,f398])).
% 0.13/0.38 fof(f638,plain,(
% 0.13/0.38 ~sQ4_spl|~sQ23_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f633])).
% 0.13/0.38 fof(f639,plain,(
% 0.13/0.38 sQ1_spl|~sQ5_spl|~sQ8_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f623,f388,f400,f411])).
% 0.13/0.38 fof(f640,plain,(
% 0.13/0.38 ~sQ5_spl|sQ7_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f624])).
% 0.13/0.38 fof(f641,plain,(
% 0.13/0.38 ![X0]: (big_q(X0)|~sQ1_spl|~sQ22_spl)),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f520,f389])).
% 0.13/0.38 fof(f642,plain,(
% 0.13/0.38 $false|~sQ1_spl|~sQ29_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f569,f389])).
% 0.13/0.38 fof(f643,plain,(
% 0.13/0.38 ![X0]: (big_q(X0)|~sQ1_spl|~sQ3_spl)),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f395,f389])).
% 0.13/0.38 fof(f644,plain,(
% 0.13/0.38 $false|~sQ1_spl|~sQ16_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f466,f389])).
% 0.13/0.38 fof(f645,plain,(
% 0.13/0.38 $false|~sQ1_spl|~sQ12_spl),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f430,f389])).
% 0.13/0.38 fof(f646,plain,(
% 0.13/0.38 sQ5_spl|~sQ1_spl|~sQ22_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f641,f400,f388,f519])).
% 0.13/0.38 fof(f647,plain,(
% 0.13/0.38 ~sQ1_spl|~sQ29_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f642])).
% 0.13/0.38 fof(f649,plain,(
% 0.13/0.38 sQ2_spl|~sQ4_spl|~sQ28_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f634,f391,f397,f565])).
% 0.13/0.38 fof(f650,plain,(
% 0.13/0.38 ~sQ4_spl|~sQ10_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f635])).
% 0.13/0.38 fof(f651,plain,(
% 0.13/0.38 ~sQ5_spl|sQ11_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f625])).
% 0.13/0.38 fof(f652,plain,(
% 0.13/0.38 sQ4_spl|~sQ2_spl|~sQ31_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f617,f397,f391,f590])).
% 0.13/0.38 fof(f653,plain,(
% 0.13/0.38 ~sQ2_spl|sQ30_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f618])).
% 0.13/0.38 fof(f654,plain,(
% 0.13/0.38 sQ1_spl|~sQ5_spl|~sQ25_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f626,f388,f400,f530])).
% 0.13/0.38 fof(f655,plain,(
% 0.13/0.38 ~sQ5_spl|sQ24_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f627])).
% 0.13/0.38 fof(f656,plain,(
% 0.13/0.38 ~sQ4_spl|~sQ6_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f636])).
% 0.13/0.38 fof(f657,plain,(
% 0.13/0.38 sQ5_spl|~sQ1_spl|~sQ3_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f643,f400,f388,f394])).
% 0.13/0.38 fof(f658,plain,(
% 0.13/0.38 ~sQ1_spl|~sQ16_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f644])).
% 0.13/0.38 fof(f659,plain,(
% 0.13/0.38 sQ2_spl|~sQ4_spl|~sQ0_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f637,f391,f397,f385])).
% 0.13/0.38 fof(f662,plain,(
% 0.13/0.38 ~sQ1_spl|~sQ12_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f645])).
% 0.13/0.38 fof(f663,plain,(
% 0.13/0.38 $false),
% 0.13/0.38 inference(sat_refutation,[status(thm)],[f403,f414,f415,f422,f426,f427,f428,f435,f446,f448,f450,f451,f452,f453,f454,f468,f487,f509,f517,f534,f549,f551,f556,f575,f601,f603,f608,f610,f612,f628,f630,f631,f632,f638,f639,f640,f646,f647,f649,f650,f651,f652,f653,f654,f655,f656,f657,f658,f659,f662])).
% 0.13/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.42 % Elapsed time: 0.059679 seconds
% 0.13/0.42 % CPU time: 0.167214 seconds
% 0.13/0.42 % Total memory used: 23.369 MB
% 0.13/0.42 % Net memory used: 22.943 MB
%------------------------------------------------------------------------------