%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN036-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n012.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 : Fri Sep 25 03:33:21 PM UTC 2026
% Result : Unsatisfiable 8.94s 1.79s
% Output : Proof 8.94s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(f100,negated_conjecture,
( big_q(X17)
| big_p(c19)
| big_q(X16)
| big_q(f4(X16))
| big_p(X11)
| big_q(c14)
| big_p(f3(X10))
| big_p(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_101) ).
fof(f100_nnf,plain,
! [X10,X11,X16,X17] :
( big_q(X17)
| big_p(c19)
| big_q(X16)
| big_q(f4(X16))
| big_p(X11)
| big_q(c14)
| big_p(f3(X10))
| big_p(X10) ),
inference(nnf_transformation,[status(thm)],[f100]) ).
fof(f100_sk,plain,
! [X10,X11,X16,X17] :
( big_q(X17)
| big_p(c19)
| big_q(X16)
| big_q(f4(X16))
| big_p(X11)
| big_q(c14)
| big_p(f3(X10))
| big_p(X10) ),
inference(skolemisation,[status(esa)],[f100_nnf]) ).
cnf(c100,plain,
( big_q(X3)
| big_p(c19)
| big_q(X2)
| big_q(f4(X2))
| big_p(X1)
| big_q(c14)
| big_p(f3(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(esa)],[f100_sk]) ).
cnf(p519,plain,
( big_q(X2)
| big_p(c19)
| big_q(X1)
| big_q(f4(X1))
| big_q(c14)
| big_p(f3(X0))
| big_p(X0) ),
inference(factoring,[status(thm)],[c100]) ).
cnf(p523,plain,
( big_q(X1)
| big_q(X0)
| big_q(f4(X0))
| big_q(c14)
| big_p(f3(c19))
| big_p(c19) ),
inference(factoring,[status(thm)],[p519]) ).
cnf(p526,plain,
( big_q(X0)
| big_q(f4(c14))
| big_q(c14)
| big_p(f3(c19))
| big_p(c19) ),
inference(factoring,[status(thm)],[p523]) ).
cnf(p528,plain,
( big_q(f4(c14))
| big_q(c14)
| big_p(f3(c19))
| big_p(c19) ),
inference(factoring,[status(thm)],[p526]) ).
cnf(f4,negated_conjecture,
( big_q(X5)
| big_p(c9)
| big_q(c8)
| ~ big_q(Z)
| big_p(V)
| ~ big_q(U)
| big_p(f1(X))
| big_p(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5) ).
fof(f4_nnf,plain,
! [X,U,V,Z,X5] :
( big_q(X5)
| big_p(c9)
| big_q(c8)
| ~ big_q(Z)
| big_p(V)
| ~ big_q(U)
| big_p(f1(X))
| big_p(X) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,U,V,Z,X5] :
( big_q(X5)
| big_p(c9)
| big_q(c8)
| ~ big_q(Z)
| big_p(V)
| ~ big_q(U)
| big_p(f1(X))
| big_p(X) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( big_q(X4)
| big_p(c9)
| big_q(c8)
| ~ big_q(X3)
| big_p(X2)
| ~ big_q(X1)
| big_p(f1(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p161,plain,
( big_q(X3)
| big_p(c9)
| big_q(c8)
| ~ big_q(X2)
| ~ big_q(X1)
| big_p(f1(X0))
| big_p(X0) ),
inference(factoring,[status(thm)],[c4]) ).
cnf(p166,plain,
( big_q(X2)
| big_q(c8)
| ~ big_q(X1)
| ~ big_q(X0)
| big_p(f1(c9))
| big_p(c9) ),
inference(factoring,[status(thm)],[p161]) ).
cnf(p169,plain,
( big_q(X1)
| big_q(c8)
| ~ big_q(X0)
| big_p(f1(c9))
| big_p(c9) ),
inference(factoring,[status(thm)],[p166]) ).
cnf(p173,plain,
( big_q(c8)
| ~ big_q(X0)
| big_p(f1(c9))
| big_p(c9) ),
inference(factoring,[status(thm)],[p169]) ).
cnf(p532,plain,
( big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_q(c14)
| big_p(f3(c19))
| big_p(c19) ),
inference(resolution,[status(thm)],[p528,p173]) ).
cnf(f48,negated_conjecture,
( big_q(X2)
| ~ big_p(X1)
| big_q(W)
| big_q(f2(W))
| big_p(X3)
| big_q(c4)
| ~ big_p(Y)
| big_p(c3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_49) ).
fof(f48_nnf,plain,
! [Y,X3,W,X1,X2] :
( big_q(X2)
| ~ big_p(X1)
| big_q(W)
| big_q(f2(W))
| big_p(X3)
| big_q(c4)
| ~ big_p(Y)
| big_p(c3) ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [Y,X3,W,X1,X2] :
( big_q(X2)
| ~ big_p(X1)
| big_q(W)
| big_q(f2(W))
| big_p(X3)
| big_q(c4)
| ~ big_p(Y)
| big_p(c3) ),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c48,plain,
( big_q(X4)
| ~ big_p(X3)
| big_q(X2)
| big_q(f2(X2))
| big_p(X1)
| big_q(c4)
| ~ big_p(X0)
| big_p(c3) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p323,plain,
( big_q(X3)
| ~ big_p(X2)
| big_q(X1)
| big_q(f2(X1))
| big_q(c4)
| ~ big_p(X0)
| big_p(c3) ),
inference(factoring,[status(thm)],[c48]) ).
cnf(p327,plain,
( big_q(X2)
| big_q(X1)
| big_q(f2(X1))
| big_q(c4)
| ~ big_p(X0)
| big_p(c3) ),
inference(factoring,[status(thm)],[p323]) ).
cnf(p330,plain,
( big_q(X1)
| big_q(f2(c4))
| big_q(c4)
| ~ big_p(X0)
| big_p(c3) ),
inference(factoring,[status(thm)],[p327]) ).
cnf(p332,plain,
( big_q(f2(c4))
| big_q(c4)
| ~ big_p(X0)
| big_p(c3) ),
inference(factoring,[status(thm)],[p330]) ).
cnf(p597,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(resolution,[status(thm)],[p532,p332]) ).
cnf(p1022,plain,
( big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(resolution,[status(thm)],[p597,p173]) ).
cnf(p1629,plain,
( big_q(c8)
| big_p(c9)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1022]) ).
cnf(p1631,plain,
( big_q(c8)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1629]) ).
cnf(p1633,plain,
( big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1631]) ).
cnf(f52,negated_conjecture,
( big_q(X5)
| big_p(c9)
| big_q(c8)
| ~ big_q(Z)
| big_p(X3)
| big_q(c4)
| ~ big_p(Y)
| big_p(c3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_53) ).
fof(f52_nnf,plain,
! [Y,X3,Z,X5] :
( big_q(X5)
| big_p(c9)
| big_q(c8)
| ~ big_q(Z)
| big_p(X3)
| big_q(c4)
| ~ big_p(Y)
| big_p(c3) ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [Y,X3,Z,X5] :
( big_q(X5)
| big_p(c9)
| big_q(c8)
| ~ big_q(Z)
| big_p(X3)
| big_q(c4)
| ~ big_p(Y)
| big_p(c3) ),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c52,plain,
( big_q(X3)
| big_p(c9)
| big_q(c8)
| ~ big_q(X2)
| big_p(X1)
| big_q(c4)
| ~ big_p(X0)
| big_p(c3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p339,plain,
( big_q(X2)
| big_p(c9)
| big_q(c8)
| ~ big_q(X1)
| big_q(c4)
| ~ big_p(X0)
| big_p(c3) ),
inference(factoring,[status(thm)],[c52]) ).
cnf(p341,plain,
( big_p(c9)
| big_q(c8)
| ~ big_q(X1)
| big_q(c4)
| ~ big_p(X0)
| big_p(c3) ),
inference(factoring,[status(thm)],[p339]) ).
cnf(p1637,plain,
( big_p(c9)
| big_q(c8)
| ~ big_q(X0)
| big_q(c4)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(resolution,[status(thm)],[p1633,p341]) ).
cnf(p1879,plain,
( big_q(c8)
| ~ big_q(X0)
| big_q(c4)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1637]) ).
cnf(p1883,plain,
( ~ big_q(X0)
| big_q(c4)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1879]) ).
cnf(p1886,plain,
( ~ big_q(X0)
| big_q(c4)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1883]) ).
cnf(p1888,plain,
( ~ big_q(X0)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1886]) ).
cnf(p1634,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(resolution,[status(thm)],[p1633,p332]) ).
cnf(p1650,plain,
( big_q(f2(c4))
| big_q(c4)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1634]) ).
cnf(p1652,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1650]) ).
cnf(p1895,plain,
( big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(resolution,[status(thm)],[p1888,p1652]) ).
cnf(p2111,plain,
( big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1895]) ).
cnf(p2117,plain,
( big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2111]) ).
cnf(p2122,plain,
( big_q(c4)
| big_p(c3)
| big_q(c8)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2117]) ).
cnf(p2126,plain,
( big_q(c4)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2122]) ).
cnf(p2129,plain,
( big_q(c4)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2126]) ).
cnf(p2131,plain,
( big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2129]) ).
cnf(p2132,plain,
( big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2131,p173]) ).
cnf(p2138,plain,
( big_q(c8)
| big_p(f1(c9))
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2132]) ).
cnf(p2140,plain,
( big_p(f1(c9))
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2138]) ).
cnf(p2144,plain,
( big_p(c9)
| big_q(c8)
| ~ big_q(X0)
| big_q(c4)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2140,p341]) ).
cnf(p2193,plain,
( big_q(c8)
| ~ big_q(X0)
| big_q(c4)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2144]) ).
cnf(p2197,plain,
( ~ big_q(X0)
| big_q(c4)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2193]) ).
cnf(p2200,plain,
( ~ big_q(X0)
| big_q(c4)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2197]) ).
cnf(p2206,plain,
( ~ big_q(X0)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2200]) ).
cnf(p2207,plain,
( big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2206,p2131]) ).
cnf(p2259,plain,
( big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2207]) ).
cnf(p2264,plain,
( big_q(c4)
| big_p(c3)
| big_q(c8)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2259]) ).
cnf(p2268,plain,
( big_q(c4)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2264]) ).
cnf(p2271,plain,
( big_q(c4)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2268]) ).
cnf(p2279,plain,
( big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2271]) ).
cnf(p524,plain,
( big_q(X1)
| big_p(c19)
| big_q(f4(c14))
| big_q(c14)
| big_p(f3(X0))
| big_p(X0) ),
inference(factoring,[status(thm)],[p519]) ).
cnf(p535,plain,
( big_p(c19)
| big_q(f4(c14))
| big_q(c14)
| big_p(f3(X0))
| big_p(X0) ),
inference(factoring,[status(thm)],[p524]) ).
cnf(f84,negated_conjecture,
( big_q(X17)
| big_p(c19)
| big_q(X16)
| big_q(f4(X16))
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_85) ).
fof(f84_nnf,plain,
! [X7,X8,X9,X16,X17] :
( big_q(X17)
| big_p(c19)
| big_q(X16)
| big_q(f4(X16))
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
inference(nnf_transformation,[status(thm)],[f84]) ).
fof(f84_sk,plain,
! [X7,X8,X9,X16,X17] :
( big_q(X17)
| big_p(c19)
| big_q(X16)
| big_q(f4(X16))
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
inference(skolemisation,[status(esa)],[f84_nnf]) ).
cnf(c84,plain,
( big_q(X4)
| big_p(c19)
| big_q(X3)
| big_q(f4(X3))
| big_p(X2)
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(p472,plain,
( big_q(X3)
| big_p(c19)
| big_q(X2)
| big_q(f4(X2))
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[c84]) ).
cnf(p477,plain,
( big_p(c19)
| big_q(X2)
| big_q(f4(X2))
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[p472]) ).
cnf(p561,plain,
( big_p(c19)
| big_q(X2)
| big_q(f4(X2))
| ~ big_q(X1)
| big_p(c11)
| big_p(c19)
| big_q(f4(c14))
| big_q(c14)
| big_p(X0) ),
inference(resolution,[status(thm)],[p535,p477]) ).
cnf(p988,plain,
( big_p(c19)
| big_q(c14)
| ~ big_q(X1)
| big_p(c11)
| big_p(c19)
| big_q(f4(c14))
| big_q(c14)
| big_p(X0) ),
inference(factoring,[status(thm)],[p561]) ).
cnf(p994,plain,
( big_p(c19)
| ~ big_q(X1)
| big_p(c11)
| big_p(c19)
| big_q(f4(c14))
| big_q(c14)
| big_p(X0) ),
inference(factoring,[status(thm)],[p988]) ).
cnf(p1001,plain,
( ~ big_q(X1)
| big_p(c11)
| big_p(c19)
| big_q(f4(c14))
| big_q(c14)
| big_p(X0) ),
inference(factoring,[status(thm)],[p994]) ).
cnf(p1002,plain,
( ~ big_q(X0)
| big_p(c11)
| big_q(f4(c14))
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1001]) ).
cnf(p331,plain,
( big_q(X1)
| big_q(f2(X1))
| big_q(c4)
| ~ big_p(X0)
| big_p(c3) ),
inference(factoring,[status(thm)],[p327]) ).
cnf(p552,plain,
( big_q(X1)
| big_q(f2(X1))
| big_q(c4)
| big_p(c3)
| big_p(c19)
| big_q(f4(c14))
| big_q(c14)
| big_p(X0) ),
inference(resolution,[status(thm)],[p535,p331]) ).
cnf(p955,plain,
( big_q(X0)
| big_q(f2(X0))
| big_q(c4)
| big_p(c3)
| big_q(f4(c14))
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p552]) ).
cnf(p959,plain,
( big_q(f2(f4(c14)))
| big_q(c4)
| big_p(c3)
| big_q(f4(c14))
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p955]) ).
cnf(p1004,plain,
( big_q(c4)
| big_p(c3)
| big_q(f4(c14))
| big_q(c14)
| big_p(c19)
| big_p(c11)
| big_q(f4(c14))
| big_q(c14)
| big_p(c19) ),
inference(resolution,[status(thm)],[p1002,p959]) ).
cnf(p1367,plain,
( big_q(c4)
| big_p(c3)
| big_q(c14)
| big_p(c19)
| big_p(c11)
| big_q(f4(c14))
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1004]) ).
cnf(p1368,plain,
( big_q(c4)
| big_p(c3)
| big_q(c14)
| big_p(c11)
| big_q(f4(c14))
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1367]) ).
cnf(p1373,plain,
( big_q(c4)
| big_p(c3)
| big_p(c11)
| big_q(f4(c14))
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1368]) ).
cnf(p1894,plain,
( big_q(c4)
| big_p(c3)
| big_p(c11)
| big_q(c14)
| big_p(c19)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(resolution,[status(thm)],[p1888,p1373]) ).
cnf(p1918,plain,
( big_q(c4)
| big_p(c3)
| big_p(c11)
| big_q(c14)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1894]) ).
cnf(p1922,plain,
( big_q(c4)
| big_p(c3)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1918]) ).
cnf(p1926,plain,
( big_q(c4)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1922]) ).
cnf(p1928,plain,
( big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c14)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1926]) ).
cnf(p1929,plain,
( big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p1928,p173]) ).
cnf(p1935,plain,
( big_q(c8)
| big_p(f1(c9))
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1929]) ).
cnf(p1938,plain,
( big_p(f1(c9))
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1935]) ).
cnf(p1942,plain,
( big_p(c9)
| big_q(c8)
| ~ big_q(X0)
| big_q(c4)
| big_p(c3)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p1938,p341]) ).
cnf(p2035,plain,
( big_q(c8)
| ~ big_q(X0)
| big_q(c4)
| big_p(c3)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p1942]) ).
cnf(p2042,plain,
( ~ big_q(X0)
| big_q(c4)
| big_p(c3)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2035]) ).
cnf(p2045,plain,
( ~ big_q(X0)
| big_q(c4)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2042]) ).
cnf(p2047,plain,
( ~ big_q(X0)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2045]) ).
cnf(p2137,plain,
( big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2131,p2047]) ).
cnf(p2183,plain,
( big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2137]) ).
cnf(p2210,plain,
( big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2183]) ).
cnf(p2214,plain,
( big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2210]) ).
cnf(p2217,plain,
( big_p(c11)
| big_q(c4)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2214]) ).
cnf(p2219,plain,
( big_p(c11)
| big_q(c4)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2217]) ).
cnf(p2222,plain,
( big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2219,p173]) ).
cnf(p2230,plain,
( big_q(c8)
| big_p(f1(c9))
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2222]) ).
cnf(p2232,plain,
( big_p(f1(c9))
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2230]) ).
cnf(f80,negated_conjecture,
( big_q(X15)
| ~ big_p(X14)
| big_q(c16)
| ~ big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_81) ).
fof(f80_nnf,plain,
! [X7,X8,X9,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| big_q(c16)
| ~ big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
inference(nnf_transformation,[status(thm)],[f80]) ).
fof(f80_sk,plain,
! [X7,X8,X9,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| big_q(c16)
| ~ big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
inference(skolemisation,[status(esa)],[f80_nnf]) ).
cnf(c80,plain,
( big_q(X5)
| ~ big_p(X4)
| big_q(c16)
| ~ big_q(X3)
| big_p(X2)
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(cnf_transformation,[status(esa)],[f80_sk]) ).
cnf(p429,plain,
( big_q(X4)
| ~ big_p(X3)
| big_q(c16)
| ~ big_q(X2)
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[c80]) ).
cnf(p435,plain,
( big_q(X3)
| big_q(c16)
| ~ big_q(X2)
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[p429]) ).
cnf(p438,plain,
( big_q(X2)
| big_q(c16)
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[p435]) ).
cnf(p440,plain,
( big_q(c16)
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[p438]) ).
cnf(p2243,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2232,p440]) ).
cnf(p2253,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2243]) ).
cnf(p2289,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2279,p2253]) ).
cnf(p2440,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2289]) ).
cnf(p2473,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2440]) ).
cnf(p2478,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2473]) ).
cnf(p2480,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2478]) ).
cnf(f82,negated_conjecture,
( big_q(X15)
| ~ big_p(X14)
| ~ big_q(c16)
| big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_83) ).
fof(f82_nnf,plain,
! [X7,X8,X9,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| ~ big_q(c16)
| big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [X7,X8,X9,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| ~ big_q(c16)
| big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c82,plain,
( big_q(X5)
| ~ big_p(X4)
| ~ big_q(c16)
| big_q(X3)
| big_p(X2)
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
cnf(p459,plain,
( big_q(X4)
| ~ big_p(X3)
| ~ big_q(c16)
| big_q(X2)
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[c82]) ).
cnf(p464,plain,
( big_q(X3)
| ~ big_q(c16)
| big_q(X2)
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[p459]) ).
cnf(p469,plain,
( big_q(X2)
| big_q(X1)
| ~ big_q(c16)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[p464]) ).
cnf(p471,plain,
( big_q(X1)
| ~ big_q(c16)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[p469]) ).
cnf(p2244,plain,
( big_q(X0)
| ~ big_q(c16)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2232,p471]) ).
cnf(p2255,plain,
( ~ big_q(c16)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2244]) ).
cnf(p2257,plain,
( ~ big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2255]) ).
cnf(p2489,plain,
( big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2480,p2257]) ).
cnf(p2572,plain,
( big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2489]) ).
cnf(p2577,plain,
( big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2572]) ).
cnf(p2581,plain,
( big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2577]) ).
cnf(p2584,plain,
( big_p(c11)
| big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2581]) ).
cnf(p2586,plain,
( big_p(c11)
| big_p(c3)
| big_q(c8)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2584]) ).
cnf(f6,negated_conjecture,
( big_q(X5)
| big_p(c9)
| ~ big_q(c8)
| big_q(Z)
| big_p(V)
| ~ big_q(U)
| big_p(f1(X))
| big_p(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7) ).
fof(f6_nnf,plain,
! [X,U,V,Z,X5] :
( big_q(X5)
| big_p(c9)
| ~ big_q(c8)
| big_q(Z)
| big_p(V)
| ~ big_q(U)
| big_p(f1(X))
| big_p(X) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,U,V,Z,X5] :
( big_q(X5)
| big_p(c9)
| ~ big_q(c8)
| big_q(Z)
| big_p(V)
| ~ big_q(U)
| big_p(f1(X))
| big_p(X) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( big_q(X4)
| big_p(c9)
| ~ big_q(c8)
| big_q(X3)
| big_p(X2)
| ~ big_q(X1)
| big_p(f1(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p175,plain,
( big_q(X3)
| big_p(c9)
| ~ big_q(c8)
| big_q(X2)
| ~ big_q(X1)
| big_p(f1(X0))
| big_p(X0) ),
inference(factoring,[status(thm)],[c6]) ).
cnf(p181,plain,
( big_q(X2)
| ~ big_q(c8)
| big_q(X1)
| ~ big_q(X0)
| big_p(f1(c9))
| big_p(c9) ),
inference(factoring,[status(thm)],[p175]) ).
cnf(p186,plain,
( big_q(X1)
| big_q(X0)
| ~ big_q(c8)
| big_p(f1(c9))
| big_p(c9) ),
inference(factoring,[status(thm)],[p181]) ).
cnf(p188,plain,
( big_q(X0)
| ~ big_q(c8)
| big_p(f1(c9))
| big_p(c9) ),
inference(factoring,[status(thm)],[p186]) ).
cnf(p2588,plain,
( big_q(X0)
| big_p(f1(c9))
| big_p(c9)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2586,p188]) ).
cnf(p2596,plain,
( big_q(X0)
| big_p(f1(c9))
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2588]) ).
cnf(p2616,plain,
( big_q(c16)
| ~ big_q(X1)
| big_p(c11)
| big_q(X0)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2596,p440]) ).
cnf(p2649,plain,
( big_q(c16)
| ~ big_q(X1)
| big_q(X0)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2616]) ).
cnf(p2651,plain,
( ~ big_q(X0)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2649]) ).
cnf(p2655,plain,
( big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2651,p2586]) ).
cnf(p2780,plain,
( big_p(c11)
| big_p(c3)
| big_p(c9)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2655]) ).
cnf(p2785,plain,
( big_p(c11)
| big_p(c3)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2780]) ).
cnf(p2788,plain,
( big_p(c11)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2785]) ).
cnf(p2790,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2788]) ).
cnf(p2617,plain,
( big_q(X1)
| ~ big_q(c16)
| big_p(c11)
| big_q(X0)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2596,p471]) ).
cnf(p2656,plain,
( big_q(X1)
| ~ big_q(c16)
| big_q(X0)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2617]) ).
cnf(p2660,plain,
( ~ big_q(c16)
| big_q(X0)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2656]) ).
cnf(p2795,plain,
( big_q(X0)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2790,p2660]) ).
cnf(p2832,plain,
( big_q(X0)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2795]) ).
cnf(p2836,plain,
( big_q(X0)
| big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2832]) ).
cnf(p2839,plain,
( big_q(X0)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2836]) ).
cnf(p2841,plain,
( big_q(X0)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2839]) ).
cnf(f3,negated_conjecture,
( ~ big_q(c7)
| big_p(c6)
| ~ big_q(W)
| ~ big_q(f2(W))
| big_p(V)
| ~ big_q(U)
| big_p(f1(X))
| big_p(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4) ).
fof(f3_nnf,plain,
! [X,U,V,W] :
( ~ big_q(c7)
| big_p(c6)
| ~ big_q(W)
| ~ big_q(f2(W))
| big_p(V)
| ~ big_q(U)
| big_p(f1(X))
| big_p(X) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,U,V,W] :
( ~ big_q(c7)
| big_p(c6)
| ~ big_q(W)
| ~ big_q(f2(W))
| big_p(V)
| ~ big_q(U)
| big_p(f1(X))
| big_p(X) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( ~ big_q(c7)
| big_p(c6)
| ~ big_q(X3)
| ~ big_q(f2(X3))
| big_p(X2)
| ~ big_q(X1)
| big_p(f1(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p151,plain,
( ~ big_q(c7)
| big_p(c6)
| ~ big_q(X2)
| ~ big_q(f2(X2))
| ~ big_q(X1)
| big_p(f1(X0))
| big_p(X0) ),
inference(factoring,[status(thm)],[c3]) ).
cnf(p156,plain,
( ~ big_q(c7)
| big_p(c6)
| ~ big_q(X1)
| ~ big_q(f2(X1))
| big_p(f1(X0))
| big_p(X0) ),
inference(factoring,[status(thm)],[p151]) ).
cnf(p165,plain,
( big_p(c6)
| ~ big_q(c7)
| ~ big_q(f2(c7))
| big_p(f1(X0))
| big_p(X0) ),
inference(factoring,[status(thm)],[p156]) ).
cnf(p2600,plain,
( big_p(c6)
| ~ big_q(c7)
| big_p(f1(X0))
| big_p(X0)
| big_p(f1(c9))
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2596,p165]) ).
cnf(p2807,plain,
( big_p(c6)
| ~ big_q(c7)
| big_p(c9)
| big_p(f1(c9))
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2600]) ).
cnf(p2822,plain,
( big_p(c6)
| ~ big_q(c7)
| big_p(f1(c9))
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2807]) ).
cnf(p2853,plain,
( big_p(c6)
| big_p(f1(c9))
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2841,p2822]) ).
cnf(p2868,plain,
( big_p(c6)
| big_p(f1(c9))
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2853]) ).
cnf(p2872,plain,
( big_p(c6)
| big_p(f1(c9))
| big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2868]) ).
cnf(p2879,plain,
( big_p(c6)
| big_p(f1(c9))
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2872]) ).
cnf(p2881,plain,
( big_p(c6)
| big_p(f1(c9))
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2879]) ).
cnf(f87,negated_conjecture,
( ~ big_q(c20)
| ~ big_p(X18)
| ~ big_q(X16)
| ~ big_q(f4(X16))
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_88) ).
fof(f87_nnf,plain,
! [X7,X8,X9,X16,X18] :
( ~ big_q(c20)
| ~ big_p(X18)
| ~ big_q(X16)
| ~ big_q(f4(X16))
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
inference(nnf_transformation,[status(thm)],[f87]) ).
fof(f87_sk,plain,
! [X7,X8,X9,X16,X18] :
( ~ big_q(c20)
| ~ big_p(X18)
| ~ big_q(X16)
| ~ big_q(f4(X16))
| big_p(X9)
| ~ big_q(X8)
| ~ big_p(X7)
| big_p(c11) ),
inference(skolemisation,[status(esa)],[f87_nnf]) ).
cnf(c87,plain,
( ~ big_q(c20)
| ~ big_p(X4)
| ~ big_q(X3)
| ~ big_q(f4(X3))
| big_p(X2)
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(cnf_transformation,[status(esa)],[f87_sk]) ).
cnf(p484,plain,
( ~ big_q(c20)
| ~ big_p(X3)
| ~ big_q(X2)
| ~ big_q(f4(X2))
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[c87]) ).
cnf(p491,plain,
( ~ big_q(c20)
| ~ big_q(X2)
| ~ big_q(f4(X2))
| ~ big_q(X1)
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[p484]) ).
cnf(p494,plain,
( ~ big_q(c20)
| ~ big_q(X1)
| ~ big_q(f4(X1))
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[p491]) ).
cnf(p496,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| ~ big_p(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[p494]) ).
cnf(p2885,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2881,p496]) ).
cnf(p2886,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2885]) ).
cnf(p2891,plain,
( big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19)
| ~ big_q(c20)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2886,p2841]) ).
cnf(p2915,plain,
( big_p(c11)
| big_p(c3)
| big_p(c9)
| ~ big_q(c20)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2891]) ).
cnf(p2921,plain,
( big_p(c11)
| big_p(c3)
| ~ big_q(c20)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2915]) ).
cnf(p2924,plain,
( big_p(c11)
| ~ big_q(c20)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2921]) ).
cnf(p2926,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2924]) ).
cnf(p2927,plain,
( big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(resolution,[status(thm)],[p2926,p2841]) ).
cnf(p2928,plain,
( big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2927]) ).
cnf(p2932,plain,
( big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2928]) ).
cnf(p2935,plain,
( big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2932]) ).
cnf(p2938,plain,
( big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c19) ),
inference(factoring,[status(thm)],[p2935]) ).
cnf(p2951,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p2938,p332]) ).
cnf(p2969,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p2951]) ).
cnf(p2959,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p2938,p440]) ).
cnf(p2966,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p2959]) ).
cnf(p2974,plain,
( big_q(c16)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p2969,p2966]) ).
cnf(p3009,plain,
( big_q(c16)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p2974]) ).
cnf(p3018,plain,
( big_q(c16)
| big_p(c6)
| big_p(c11)
| big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3009]) ).
cnf(p3021,plain,
( big_q(c16)
| big_p(c6)
| big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3018]) ).
cnf(p3023,plain,
( big_q(c16)
| big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3021]) ).
cnf(p2960,plain,
( big_q(X0)
| ~ big_q(c16)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p2938,p471]) ).
cnf(p2968,plain,
( big_q(X0)
| ~ big_q(c16)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p2960]) ).
cnf(p3028,plain,
( big_q(X0)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3023,p2968]) ).
cnf(p3073,plain,
( big_q(X0)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3028]) ).
cnf(p3085,plain,
( big_q(X0)
| big_p(c6)
| big_p(c11)
| big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3073]) ).
cnf(p3089,plain,
( big_q(X0)
| big_p(c6)
| big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3085]) ).
cnf(p3092,plain,
( big_q(X0)
| big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3089]) ).
cnf(p3099,plain,
( big_q(c4)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3092]) ).
cnf(p3103,plain,
( big_q(c16)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3099,p2966]) ).
cnf(p3162,plain,
( big_q(c16)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3103]) ).
cnf(p3166,plain,
( big_q(c16)
| big_p(c6)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3162]) ).
cnf(p3169,plain,
( big_q(c16)
| big_p(c6)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3166]) ).
cnf(p3172,plain,
( big_q(c16)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3169]) ).
cnf(p3177,plain,
( big_q(X0)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3172,p2968]) ).
cnf(p3197,plain,
( big_q(X0)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3177]) ).
cnf(p3201,plain,
( big_q(X0)
| big_p(c6)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3197]) ).
cnf(p3204,plain,
( big_q(X0)
| big_p(c6)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3201]) ).
cnf(p3206,plain,
( big_q(X0)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3204]) ).
cnf(p2963,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p2938,p496]) ).
cnf(p2976,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p2963]) ).
cnf(p3213,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3206,p2976]) ).
cnf(p3230,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3213]) ).
cnf(p3239,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3230]) ).
cnf(p3242,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3239]) ).
cnf(p3244,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3242]) ).
cnf(p3249,plain,
( big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3244,p3206]) ).
cnf(p3250,plain,
( big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3249]) ).
cnf(p3254,plain,
( big_p(c6)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3250]) ).
cnf(p3257,plain,
( big_p(c6)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3254]) ).
cnf(p3259,plain,
( big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3257]) ).
cnf(p3272,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3259,p332]) ).
cnf(p3326,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3272]) ).
cnf(f64,negated_conjecture,
( big_q(X15)
| ~ big_p(X14)
| big_q(c16)
| ~ big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| big_p(X7)
| ~ big_p(c11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_65) ).
fof(f64_nnf,plain,
! [X7,X8,X9,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| big_q(c16)
| ~ big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| big_p(X7)
| ~ big_p(c11) ),
inference(nnf_transformation,[status(thm)],[f64]) ).
fof(f64_sk,plain,
! [X7,X8,X9,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| big_q(c16)
| ~ big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| big_p(X7)
| ~ big_p(c11) ),
inference(skolemisation,[status(esa)],[f64_nnf]) ).
cnf(c64,plain,
( big_q(X5)
| ~ big_p(X4)
| big_q(c16)
| ~ big_q(X3)
| big_p(X2)
| ~ big_q(X1)
| big_p(X0)
| ~ big_p(c11) ),
inference(cnf_transformation,[status(esa)],[f64_sk]) ).
cnf(p398,plain,
( big_q(X4)
| big_q(c16)
| ~ big_q(X3)
| big_p(X2)
| ~ big_q(X1)
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[c64]) ).
cnf(p402,plain,
( big_q(X3)
| big_q(c16)
| ~ big_q(X2)
| ~ big_q(X1)
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[p398]) ).
cnf(p405,plain,
( big_q(X2)
| big_q(c16)
| ~ big_q(X1)
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[p402]) ).
cnf(p407,plain,
( big_q(c16)
| ~ big_q(X1)
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[p405]) ).
cnf(p3280,plain,
( big_q(c16)
| ~ big_q(X1)
| big_p(X0)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3259,p407]) ).
cnf(p3316,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3280]) ).
cnf(p3333,plain,
( big_q(c16)
| big_p(c6)
| big_p(c3)
| big_p(c9)
| big_q(c4)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3326,p3316]) ).
cnf(p3384,plain,
( big_q(c16)
| big_p(c6)
| big_p(c3)
| big_q(c4)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3333]) ).
cnf(p3387,plain,
( big_q(c16)
| big_p(c6)
| big_q(c4)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3384]) ).
cnf(p3405,plain,
( big_q(c16)
| big_q(c4)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3387]) ).
cnf(f66,negated_conjecture,
( big_q(X15)
| ~ big_p(X14)
| ~ big_q(c16)
| big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| big_p(X7)
| ~ big_p(c11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_67) ).
fof(f66_nnf,plain,
! [X7,X8,X9,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| ~ big_q(c16)
| big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| big_p(X7)
| ~ big_p(c11) ),
inference(nnf_transformation,[status(thm)],[f66]) ).
fof(f66_sk,plain,
! [X7,X8,X9,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| ~ big_q(c16)
| big_q(X13)
| big_p(X9)
| ~ big_q(X8)
| big_p(X7)
| ~ big_p(c11) ),
inference(skolemisation,[status(esa)],[f66_nnf]) ).
cnf(c66,plain,
( big_q(X5)
| ~ big_p(X4)
| ~ big_q(c16)
| big_q(X3)
| big_p(X2)
| ~ big_q(X1)
| big_p(X0)
| ~ big_p(c11) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p408,plain,
( big_q(X4)
| ~ big_q(c16)
| big_q(X3)
| big_p(X2)
| ~ big_q(X1)
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[c66]) ).
cnf(p412,plain,
( big_q(X3)
| ~ big_q(c16)
| big_q(X2)
| ~ big_q(X1)
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[p408]) ).
cnf(p415,plain,
( big_q(X2)
| big_q(X1)
| ~ big_q(c16)
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[p412]) ).
cnf(p417,plain,
( big_q(X1)
| ~ big_q(c16)
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[p415]) ).
cnf(p3281,plain,
( big_q(X1)
| ~ big_q(c16)
| big_p(X0)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3259,p417]) ).
cnf(p3324,plain,
( big_q(X0)
| ~ big_q(c16)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3281]) ).
cnf(p3410,plain,
( big_q(X0)
| big_p(c6)
| big_p(c3)
| big_p(c9)
| big_q(c4)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3405,p3324]) ).
cnf(p3411,plain,
( big_q(X0)
| big_p(c6)
| big_p(c3)
| big_q(c4)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3410]) ).
cnf(p3415,plain,
( big_q(X0)
| big_p(c6)
| big_q(c4)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3411]) ).
cnf(p3418,plain,
( big_q(X0)
| big_q(c4)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3415]) ).
cnf(p3420,plain,
( big_q(c4)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3418]) ).
cnf(p3428,plain,
( big_q(c16)
| big_p(c6)
| big_p(c3)
| big_p(c9)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3420,p3316]) ).
cnf(p3441,plain,
( big_q(c16)
| big_p(c6)
| big_p(c3)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3428]) ).
cnf(p3444,plain,
( big_q(c16)
| big_p(c6)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3441]) ).
cnf(p3446,plain,
( big_q(c16)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3444]) ).
cnf(p3464,plain,
( big_q(X0)
| big_p(c6)
| big_p(c3)
| big_p(c9)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3446,p3324]) ).
cnf(p3465,plain,
( big_q(X0)
| big_p(c6)
| big_p(c3)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3464]) ).
cnf(p3468,plain,
( big_q(X0)
| big_p(c6)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3465]) ).
cnf(p3470,plain,
( big_q(X0)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3468]) ).
cnf(f71,negated_conjecture,
( ~ big_q(c20)
| ~ big_p(X18)
| ~ big_q(X16)
| ~ big_q(f4(X16))
| big_p(X9)
| ~ big_q(X8)
| big_p(X7)
| ~ big_p(c11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_72) ).
fof(f71_nnf,plain,
! [X7,X8,X9,X16,X18] :
( ~ big_q(c20)
| ~ big_p(X18)
| ~ big_q(X16)
| ~ big_q(f4(X16))
| big_p(X9)
| ~ big_q(X8)
| big_p(X7)
| ~ big_p(c11) ),
inference(nnf_transformation,[status(thm)],[f71]) ).
fof(f71_sk,plain,
! [X7,X8,X9,X16,X18] :
( ~ big_q(c20)
| ~ big_p(X18)
| ~ big_q(X16)
| ~ big_q(f4(X16))
| big_p(X9)
| ~ big_q(X8)
| big_p(X7)
| ~ big_p(c11) ),
inference(skolemisation,[status(esa)],[f71_nnf]) ).
cnf(c71,plain,
( ~ big_q(c20)
| ~ big_p(X4)
| ~ big_q(X3)
| ~ big_q(f4(X3))
| big_p(X2)
| ~ big_q(X1)
| big_p(X0)
| ~ big_p(c11) ),
inference(cnf_transformation,[status(esa)],[f71_sk]) ).
cnf(p441,plain,
( ~ big_q(c20)
| ~ big_q(X3)
| ~ big_q(f4(X3))
| big_p(X2)
| ~ big_q(X1)
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[c71]) ).
cnf(p448,plain,
( ~ big_q(c20)
| ~ big_q(X2)
| ~ big_q(f4(X2))
| ~ big_q(X1)
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[p441]) ).
cnf(p454,plain,
( ~ big_q(c20)
| ~ big_q(X1)
| ~ big_q(f4(X1))
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[p448]) ).
cnf(p456,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(X0)
| ~ big_p(c11) ),
inference(factoring,[status(thm)],[p454]) ).
cnf(p3286,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(X0)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3259,p456]) ).
cnf(p3334,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3286]) ).
cnf(p3477,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c3)
| big_p(c9)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3470,p3334]) ).
cnf(p3480,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c3)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3477]) ).
cnf(p3483,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3480]) ).
cnf(p3488,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3483]) ).
cnf(p3489,plain,
( big_p(c6)
| big_p(c3)
| big_p(c9)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3488,p3470]) ).
cnf(p3490,plain,
( big_p(c6)
| big_p(c3)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3489]) ).
cnf(p3493,plain,
( big_p(c6)
| big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3490]) ).
cnf(p3497,plain,
( big_p(c6)
| big_p(c3)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3493]) ).
cnf(f32,negated_conjecture,
( big_q(X2)
| ~ big_p(X1)
| big_q(W)
| big_q(f2(W))
| big_p(X3)
| big_q(c4)
| big_p(Y)
| ~ big_p(c3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_33) ).
fof(f32_nnf,plain,
! [Y,X3,W,X1,X2] :
( big_q(X2)
| ~ big_p(X1)
| big_q(W)
| big_q(f2(W))
| big_p(X3)
| big_q(c4)
| big_p(Y)
| ~ big_p(c3) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [Y,X3,W,X1,X2] :
( big_q(X2)
| ~ big_p(X1)
| big_q(W)
| big_q(f2(W))
| big_p(X3)
| big_q(c4)
| big_p(Y)
| ~ big_p(c3) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
( big_q(X4)
| ~ big_p(X3)
| big_q(X2)
| big_q(f2(X2))
| big_p(X1)
| big_q(c4)
| big_p(X0)
| ~ big_p(c3) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p275,plain,
( big_q(X3)
| big_q(X2)
| big_q(f2(X2))
| big_p(X1)
| big_q(c4)
| big_p(X0)
| ~ big_p(c3) ),
inference(factoring,[status(thm)],[c32]) ).
cnf(p280,plain,
( big_q(X2)
| big_q(X1)
| big_q(f2(X1))
| big_q(c4)
| big_p(X0)
| ~ big_p(c3) ),
inference(factoring,[status(thm)],[p275]) ).
cnf(p283,plain,
( big_q(X1)
| big_q(f2(c4))
| big_q(c4)
| big_p(X0)
| ~ big_p(c3) ),
inference(factoring,[status(thm)],[p280]) ).
cnf(p288,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(X0)
| ~ big_p(c3) ),
inference(factoring,[status(thm)],[p283]) ).
cnf(p3513,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(X0)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3497,p288]) ).
cnf(p3575,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3513]) ).
cnf(p3526,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3497,p440]) ).
cnf(p3586,plain,
( big_q(c16)
| big_p(c11)
| big_p(c6)
| big_p(c9)
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3575,p3526]) ).
cnf(p3628,plain,
( big_q(c16)
| big_p(c11)
| big_p(c6)
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3586]) ).
cnf(p3630,plain,
( big_q(c16)
| big_p(c11)
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3628]) ).
cnf(p3527,plain,
( big_q(X0)
| ~ big_q(c16)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3497,p471]) ).
cnf(p3636,plain,
( big_q(X0)
| big_p(c11)
| big_p(c6)
| big_p(c9)
| big_p(c11)
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3630,p3527]) ).
cnf(p3879,plain,
( big_q(X0)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3636]) ).
cnf(p3883,plain,
( big_q(X0)
| big_p(c11)
| big_p(c11)
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3879]) ).
cnf(p3886,plain,
( big_p(c11)
| big_p(c11)
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3883]) ).
cnf(p3888,plain,
( big_p(c11)
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3886]) ).
cnf(p3906,plain,
( big_q(c16)
| big_p(c11)
| big_p(c6)
| big_p(c9)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3888,p3526]) ).
cnf(p3909,plain,
( big_q(c16)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3906]) ).
cnf(p3912,plain,
( big_q(c16)
| big_p(c11)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3909]) ).
cnf(p3914,plain,
( big_q(c16)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3912]) ).
cnf(p3933,plain,
( big_q(X0)
| big_p(c11)
| big_p(c6)
| big_p(c9)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3914,p3527]) ).
cnf(p3934,plain,
( big_q(X0)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3933]) ).
cnf(p3937,plain,
( big_q(X0)
| big_p(c11)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3934]) ).
cnf(p3939,plain,
( big_q(X0)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3937]) ).
cnf(p3532,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3497,p496]) ).
cnf(p3948,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c6)
| big_p(c9)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3939,p3532]) ).
cnf(p3952,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3948]) ).
cnf(p3957,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3952]) ).
cnf(p3959,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3957]) ).
cnf(p3960,plain,
( big_p(c11)
| big_p(c6)
| big_p(c9)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3959,p3939]) ).
cnf(p3961,plain,
( big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3960]) ).
cnf(p3978,plain,
( big_p(c11)
| big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3961]) ).
cnf(p3980,plain,
( big_p(c11)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3978]) ).
cnf(p3994,plain,
( big_q(c16)
| ~ big_q(X1)
| big_p(X0)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3980,p407]) ).
cnf(p4010,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3994]) ).
cnf(p4013,plain,
( big_q(c4)
| big_p(c6)
| big_p(c9)
| big_q(c16)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p4010,p3575]) ).
cnf(p4017,plain,
( big_q(c4)
| big_p(c6)
| big_q(c16)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4013]) ).
cnf(p4019,plain,
( big_q(c4)
| big_q(c16)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4017]) ).
cnf(p3995,plain,
( big_q(X1)
| ~ big_q(c16)
| big_p(X0)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3980,p417]) ).
cnf(p4015,plain,
( big_q(X0)
| ~ big_q(c16)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p3995]) ).
cnf(p4024,plain,
( big_q(X0)
| big_p(c6)
| big_p(c9)
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p4019,p4015]) ).
cnf(p4035,plain,
( big_q(X0)
| big_p(c6)
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4024]) ).
cnf(p4050,plain,
( big_q(X0)
| big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4035]) ).
cnf(p4052,plain,
( big_q(c4)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4050]) ).
cnf(p4059,plain,
( big_q(c16)
| big_p(c6)
| big_p(c9)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p4052,p4010]) ).
cnf(p4060,plain,
( big_q(c16)
| big_p(c6)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4059]) ).
cnf(p4064,plain,
( big_q(c16)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4060]) ).
cnf(p4069,plain,
( big_q(X0)
| big_p(c6)
| big_p(c9)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p4064,p4015]) ).
cnf(p4070,plain,
( big_q(X0)
| big_p(c6)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4069]) ).
cnf(p4072,plain,
( big_q(X0)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4070]) ).
cnf(p4000,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(X0)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p3980,p456]) ).
cnf(p4016,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4000]) ).
cnf(p4081,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c9)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p4072,p4016]) ).
cnf(p4082,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4081]) ).
cnf(p4084,plain,
( ~ big_q(c20)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4082]) ).
cnf(p4085,plain,
( big_p(c6)
| big_p(c9)
| big_p(c6)
| big_p(c9) ),
inference(resolution,[status(thm)],[p4084,p4072]) ).
cnf(p4087,plain,
( big_p(c6)
| big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4085]) ).
cnf(p4089,plain,
( big_p(c6)
| big_p(c9) ),
inference(factoring,[status(thm)],[p4087]) ).
cnf(p4100,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4089,p332]) ).
cnf(p4106,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c11)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4089,p440]) ).
cnf(p4157,plain,
( big_q(c16)
| big_p(c11)
| big_p(c6)
| big_q(c4)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4100,p4106]) ).
cnf(p4184,plain,
( big_q(c16)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4157]) ).
cnf(p4107,plain,
( big_q(X0)
| ~ big_q(c16)
| big_p(c11)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4089,p471]) ).
cnf(p4189,plain,
( big_q(X0)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4184,p4107]) ).
cnf(p4236,plain,
( big_q(X0)
| big_p(c11)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4189]) ).
cnf(p4239,plain,
( big_p(c11)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4236]) ).
cnf(p4241,plain,
( big_p(c11)
| big_q(c4)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4239]) ).
cnf(p4249,plain,
( big_q(c16)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4241,p4106]) ).
cnf(p4251,plain,
( big_q(c16)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4249]) ).
cnf(p4253,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4251]) ).
cnf(p4258,plain,
( big_q(X0)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4253,p4107]) ).
cnf(p4259,plain,
( big_q(X0)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4258]) ).
cnf(p4273,plain,
( big_q(X0)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4259]) ).
cnf(p4112,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4089,p496]) ).
cnf(p4280,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4273,p4112]) ).
cnf(p4281,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4280]) ).
cnf(p4283,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4281]) ).
cnf(p4297,plain,
( big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4283,p4273]) ).
cnf(p4298,plain,
( big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4297]) ).
cnf(p4301,plain,
( big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4298]) ).
cnf(p4303,plain,
( big_p(c11)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4301]) ).
cnf(p4315,plain,
( big_q(c16)
| ~ big_q(X1)
| big_p(X0)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4303,p407]) ).
cnf(p4331,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4315]) ).
cnf(p4338,plain,
( big_q(c4)
| big_p(c3)
| big_p(c6)
| big_q(c16)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4331,p4100]) ).
cnf(p4353,plain,
( big_q(c4)
| big_p(c3)
| big_q(c16)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4338]) ).
cnf(p4366,plain,
( big_q(c4)
| big_q(c16)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4353]) ).
cnf(p4316,plain,
( big_q(X1)
| ~ big_q(c16)
| big_p(X0)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4303,p417]) ).
cnf(p4339,plain,
( big_q(X0)
| ~ big_q(c16)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4316]) ).
cnf(p4371,plain,
( big_q(X0)
| big_p(c3)
| big_p(c6)
| big_q(c4)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4366,p4339]) ).
cnf(p4372,plain,
( big_q(X0)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4371]) ).
cnf(p4375,plain,
( big_q(X0)
| big_q(c4)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4372]) ).
cnf(p4388,plain,
( big_q(c4)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4375]) ).
cnf(p4394,plain,
( big_q(c16)
| big_p(c3)
| big_p(c6)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4388,p4331]) ).
cnf(p4395,plain,
( big_q(c16)
| big_p(c3)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4394]) ).
cnf(p4397,plain,
( big_q(c16)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4395]) ).
cnf(p4403,plain,
( big_q(X0)
| big_p(c3)
| big_p(c6)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4397,p4339]) ).
cnf(p4404,plain,
( big_q(X0)
| big_p(c3)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4403]) ).
cnf(p4406,plain,
( big_q(X0)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4404]) ).
cnf(p4321,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(X0)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4303,p456]) ).
cnf(p4352,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4321]) ).
cnf(p4413,plain,
( ~ big_q(c20)
| big_p(c3)
| big_p(c6)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4406,p4352]) ).
cnf(p4415,plain,
( ~ big_q(c20)
| big_p(c3)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4413]) ).
cnf(p4417,plain,
( ~ big_q(c20)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4415]) ).
cnf(p4418,plain,
( big_p(c3)
| big_p(c6)
| big_p(c3)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4417,p4406]) ).
cnf(p4419,plain,
( big_p(c3)
| big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4418]) ).
cnf(p4434,plain,
( big_p(c3)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4419]) ).
cnf(p4445,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(X0)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4434,p288]) ).
cnf(p4473,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4445]) ).
cnf(p4480,plain,
( big_q(c16)
| big_p(c11)
| big_p(c6)
| big_q(c4)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4473,p4106]) ).
cnf(p4486,plain,
( big_q(c16)
| big_p(c11)
| big_q(c4)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4480]) ).
cnf(p4491,plain,
( big_q(X0)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_q(c4)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4486,p4107]) ).
cnf(p4514,plain,
( big_q(X0)
| big_p(c11)
| big_p(c11)
| big_q(c4)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4491]) ).
cnf(p4529,plain,
( big_p(c11)
| big_p(c11)
| big_q(c4)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4514]) ).
cnf(p4531,plain,
( big_p(c11)
| big_q(c4)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4529]) ).
cnf(p4539,plain,
( big_q(c16)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4531,p4106]) ).
cnf(p4541,plain,
( big_q(c16)
| big_p(c11)
| big_p(c11)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4539]) ).
cnf(p4546,plain,
( big_q(c16)
| big_p(c11)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4541]) ).
cnf(p4551,plain,
( big_q(X0)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4546,p4107]) ).
cnf(p4552,plain,
( big_q(X0)
| big_p(c11)
| big_p(c11)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4551]) ).
cnf(p4554,plain,
( big_q(X0)
| big_p(c11)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4552]) ).
cnf(p4563,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4554,p4112]) ).
cnf(p4565,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c11)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4563]) ).
cnf(p4567,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4565]) ).
cnf(p4568,plain,
( big_p(c11)
| big_p(c6)
| big_p(c11)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4567,p4554]) ).
cnf(p4570,plain,
( big_p(c11)
| big_p(c11)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4568]) ).
cnf(p4572,plain,
( big_p(c11)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4570]) ).
cnf(p4590,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(X0)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4572,p456]) ).
cnf(p4636,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c6) ),
inference(factoring,[status(thm)],[p4590]) ).
cnf(p4584,plain,
( big_q(c16)
| ~ big_q(X1)
| big_p(X0)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4572,p407]) ).
cnf(p4600,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4584]) ).
cnf(p4601,plain,
( big_q(c4)
| big_p(c6)
| big_q(c16)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4600,p4473]) ).
cnf(p4603,plain,
( big_q(c4)
| big_q(c16)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4601]) ).
cnf(p4585,plain,
( big_q(X1)
| ~ big_q(c16)
| big_p(X0)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4572,p417]) ).
cnf(p4602,plain,
( big_q(X0)
| ~ big_q(c16)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4585]) ).
cnf(p4610,plain,
( big_q(X0)
| big_p(c6)
| big_q(c4)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4603,p4602]) ).
cnf(p4611,plain,
( big_q(X0)
| big_q(c4)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4610]) ).
cnf(p4613,plain,
( big_q(c4)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4611]) ).
cnf(p4619,plain,
( big_q(c16)
| big_p(c6)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4613,p4600]) ).
cnf(p4620,plain,
( big_q(c16)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4619]) ).
cnf(p4625,plain,
( big_q(X0)
| big_p(c6)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4620,p4602]) ).
cnf(p4626,plain,
( big_q(X0)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4625]) ).
cnf(p4637,plain,
( big_p(c6)
| ~ big_q(c20)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4636,p4626]) ).
cnf(p4638,plain,
( ~ big_q(c20)
| big_p(c6) ),
inference(factoring,[status(thm)],[p4637]) ).
cnf(p4639,plain,
( big_p(c6)
| big_p(c6) ),
inference(resolution,[status(thm)],[p4638,p4626]) ).
cnf(p4640,plain,
big_p(c6),
inference(factoring,[status(thm)],[p4639]) ).
cnf(p4651,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4640,p332]) ).
cnf(p4659,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c11) ),
inference(resolution,[status(thm)],[p4640,p440]) ).
cnf(p4711,plain,
( big_q(c16)
| big_p(c11)
| big_q(c4)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4651,p4659]) ).
cnf(p4660,plain,
( big_q(X0)
| ~ big_q(c16)
| big_p(c11) ),
inference(resolution,[status(thm)],[p4640,p471]) ).
cnf(p4717,plain,
( big_q(X0)
| big_p(c11)
| big_p(c11)
| big_q(c4)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4711,p4660]) ).
cnf(p4737,plain,
( big_p(c11)
| big_p(c11)
| big_q(c4)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4717]) ).
cnf(p4739,plain,
( big_p(c11)
| big_q(c4)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4737]) ).
cnf(p4747,plain,
( big_q(c16)
| big_p(c11)
| big_p(c11)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4739,p4659]) ).
cnf(p4748,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4747]) ).
cnf(p4753,plain,
( big_q(X0)
| big_p(c11)
| big_p(c11)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4748,p4660]) ).
cnf(p4754,plain,
( big_q(X0)
| big_p(c11)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4753]) ).
cnf(p4665,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11) ),
inference(resolution,[status(thm)],[p4640,p496]) ).
cnf(p4757,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c11)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4754,p4665]) ).
cnf(p4758,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4757]) ).
cnf(p4759,plain,
( big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4758,p4754]) ).
cnf(p4760,plain,
( big_p(c11)
| big_p(c11)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4759]) ).
cnf(p4762,plain,
( big_p(c11)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4760]) ).
cnf(p4780,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(X0)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4762,p456]) ).
cnf(p4820,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c3) ),
inference(factoring,[status(thm)],[p4780]) ).
cnf(p4774,plain,
( big_q(c16)
| ~ big_q(X1)
| big_p(X0)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4762,p407]) ).
cnf(p4790,plain,
( big_q(c16)
| ~ big_q(X0)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4774]) ).
cnf(p4792,plain,
( big_q(c4)
| big_p(c3)
| big_q(c16)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4790,p4651]) ).
cnf(p4794,plain,
( big_q(c4)
| big_q(c16)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4792]) ).
cnf(p4775,plain,
( big_q(X1)
| ~ big_q(c16)
| big_p(X0)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4762,p417]) ).
cnf(p4793,plain,
( big_q(X0)
| ~ big_q(c16)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4775]) ).
cnf(p4799,plain,
( big_q(X0)
| big_p(c3)
| big_q(c4)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4794,p4793]) ).
cnf(p4800,plain,
( big_q(X0)
| big_q(c4)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4799]) ).
cnf(p4802,plain,
( big_q(c4)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4800]) ).
cnf(p4810,plain,
( big_q(c16)
| big_p(c3)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4802,p4790]) ).
cnf(p4811,plain,
( big_q(c16)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4810]) ).
cnf(p4816,plain,
( big_q(X0)
| big_p(c3)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4811,p4793]) ).
cnf(p4817,plain,
( big_q(X0)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4816]) ).
cnf(p4821,plain,
( big_p(c3)
| ~ big_q(c20)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4820,p4817]) ).
cnf(p4822,plain,
( ~ big_q(c20)
| big_p(c3) ),
inference(factoring,[status(thm)],[p4821]) ).
cnf(p4823,plain,
( big_p(c3)
| big_p(c3) ),
inference(resolution,[status(thm)],[p4822,p4817]) ).
cnf(p4824,plain,
big_p(c3),
inference(factoring,[status(thm)],[p4823]) ).
cnf(p4838,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(X0) ),
inference(resolution,[status(thm)],[p4824,p288]) ).
cnf(p4891,plain,
( big_q(c16)
| big_p(c11)
| big_q(c4)
| big_p(X0) ),
inference(resolution,[status(thm)],[p4838,p4659]) ).
cnf(p4907,plain,
( big_q(c16)
| big_q(c4)
| big_p(c11) ),
inference(factoring,[status(thm)],[p4891]) ).
cnf(p4912,plain,
( big_q(X0)
| big_p(c11)
| big_q(c4)
| big_p(c11) ),
inference(resolution,[status(thm)],[p4907,p4660]) ).
cnf(p4913,plain,
( big_q(X0)
| big_q(c4)
| big_p(c11) ),
inference(factoring,[status(thm)],[p4912]) ).
cnf(p4915,plain,
( big_q(c4)
| big_p(c11) ),
inference(factoring,[status(thm)],[p4913]) ).
cnf(p4923,plain,
( big_q(c16)
| big_p(c11)
| big_p(c11) ),
inference(resolution,[status(thm)],[p4915,p4659]) ).
cnf(p4926,plain,
( big_q(c16)
| big_p(c11) ),
inference(factoring,[status(thm)],[p4923]) ).
cnf(p4931,plain,
( big_q(X0)
| big_p(c11)
| big_p(c11) ),
inference(resolution,[status(thm)],[p4926,p4660]) ).
cnf(p4932,plain,
( big_q(X0)
| big_p(c11) ),
inference(factoring,[status(thm)],[p4931]) ).
cnf(p4935,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c11) ),
inference(resolution,[status(thm)],[p4932,p4665]) ).
cnf(p4936,plain,
( ~ big_q(c20)
| big_p(c11) ),
inference(factoring,[status(thm)],[p4935]) ).
cnf(p4937,plain,
( big_p(c11)
| big_p(c11) ),
inference(resolution,[status(thm)],[p4936,p4932]) ).
cnf(p4938,plain,
big_p(c11),
inference(factoring,[status(thm)],[p4937]) ).
cnf(p4950,plain,
( big_q(c16)
| ~ big_q(X1)
| big_p(X0) ),
inference(resolution,[status(thm)],[p4938,p407]) ).
cnf(p4966,plain,
( big_q(c4)
| big_p(X1)
| big_q(c16)
| big_p(X0) ),
inference(resolution,[status(thm)],[p4950,p4838]) ).
cnf(p4968,plain,
( big_q(c4)
| big_q(c16)
| big_p(X0) ),
inference(factoring,[status(thm)],[p4966]) ).
cnf(p4951,plain,
( big_q(X1)
| ~ big_q(c16)
| big_p(X0) ),
inference(resolution,[status(thm)],[p4938,p417]) ).
cnf(p4994,plain,
( big_q(X2)
| big_p(X1)
| big_q(c4)
| big_p(X0) ),
inference(resolution,[status(thm)],[p4968,p4951]) ).
cnf(p4996,plain,
( big_q(X1)
| big_q(c4)
| big_p(X0) ),
inference(factoring,[status(thm)],[p4994]) ).
cnf(p5008,plain,
( big_q(c4)
| big_p(X0) ),
inference(factoring,[status(thm)],[p4996]) ).
cnf(p5041,plain,
( big_q(c16)
| big_p(X1)
| big_p(X0) ),
inference(resolution,[status(thm)],[p5008,p4950]) ).
cnf(p5043,plain,
( big_q(c16)
| big_p(X0) ),
inference(factoring,[status(thm)],[p5041]) ).
cnf(p5069,plain,
( big_q(X2)
| big_p(X1)
| big_p(X0) ),
inference(resolution,[status(thm)],[p5043,p4951]) ).
cnf(p5073,plain,
( big_q(X1)
| big_p(X0) ),
inference(factoring,[status(thm)],[p5069]) ).
cnf(p4956,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(X0) ),
inference(resolution,[status(thm)],[p4938,p456]) ).
cnf(p5103,plain,
( ~ big_q(c20)
| big_p(X1)
| big_p(X0) ),
inference(resolution,[status(thm)],[p5073,p4956]) ).
cnf(p5105,plain,
( ~ big_q(c20)
| big_p(X0) ),
inference(factoring,[status(thm)],[p5103]) ).
cnf(p5106,plain,
( big_p(X1)
| big_p(X0) ),
inference(resolution,[status(thm)],[p5105,p5073]) ).
cnf(p5107,plain,
big_p(X0),
inference(factoring,[status(thm)],[p5106]) ).
cnf(f127,negated_conjecture,
( ~ big_q(c20)
| ~ big_p(X18)
| ~ big_q(X16)
| ~ big_q(f4(X16))
| ~ big_p(c15)
| ~ big_q(X12)
| ~ big_p(f3(X10))
| ~ big_p(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_128) ).
fof(f127_nnf,plain,
! [X10,X12,X16,X18] :
( ~ big_q(c20)
| ~ big_p(X18)
| ~ big_q(X16)
| ~ big_q(f4(X16))
| ~ big_p(c15)
| ~ big_q(X12)
| ~ big_p(f3(X10))
| ~ big_p(X10) ),
inference(nnf_transformation,[status(thm)],[f127]) ).
fof(f127_sk,plain,
! [X10,X12,X16,X18] :
( ~ big_q(c20)
| ~ big_p(X18)
| ~ big_q(X16)
| ~ big_q(f4(X16))
| ~ big_p(c15)
| ~ big_q(X12)
| ~ big_p(f3(X10))
| ~ big_p(X10) ),
inference(skolemisation,[status(esa)],[f127_nnf]) ).
cnf(c127,plain,
( ~ big_q(c20)
| ~ big_p(X3)
| ~ big_q(X2)
| ~ big_q(f4(X2))
| ~ big_p(c15)
| ~ big_q(X1)
| ~ big_p(f3(X0))
| ~ big_p(X0) ),
inference(cnf_transformation,[status(esa)],[f127_sk]) ).
cnf(p787,plain,
( ~ big_q(c20)
| ~ big_p(X2)
| ~ big_q(X1)
| ~ big_q(f4(X1))
| ~ big_q(X0)
| ~ big_p(f3(c15))
| ~ big_p(c15) ),
inference(factoring,[status(thm)],[c127]) ).
cnf(p793,plain,
( ~ big_q(c20)
| ~ big_q(X1)
| ~ big_q(f4(X1))
| ~ big_q(X0)
| ~ big_p(f3(c15))
| ~ big_p(c15) ),
inference(factoring,[status(thm)],[p787]) ).
cnf(p796,plain,
( ~ big_q(c20)
| ~ big_q(X0)
| ~ big_q(f4(X0))
| ~ big_p(f3(c15))
| ~ big_p(c15) ),
inference(factoring,[status(thm)],[p793]) ).
cnf(p5124,plain,
( ~ big_q(c20)
| ~ big_q(X0)
| ~ big_q(f4(X0))
| ~ big_p(f3(c15)) ),
inference(resolution,[status(thm)],[p5107,p796]) ).
cnf(p5138,plain,
( ~ big_q(c20)
| ~ big_q(X0)
| ~ big_q(f4(X0)) ),
inference(resolution,[status(thm)],[p5124,p5107]) ).
cnf(f24,negated_conjecture,
( big_q(X2)
| ~ big_p(X1)
| big_q(W)
| big_q(f2(W))
| ~ big_p(c2)
| big_q(c1)
| ~ big_p(f1(X))
| ~ big_p(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_25) ).
fof(f24_nnf,plain,
! [X,W,X1,X2] :
( big_q(X2)
| ~ big_p(X1)
| big_q(W)
| big_q(f2(W))
| ~ big_p(c2)
| big_q(c1)
| ~ big_p(f1(X))
| ~ big_p(X) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [X,W,X1,X2] :
( big_q(X2)
| ~ big_p(X1)
| big_q(W)
| big_q(f2(W))
| ~ big_p(c2)
| big_q(c1)
| ~ big_p(f1(X))
| ~ big_p(X) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( big_q(X3)
| ~ big_p(X2)
| big_q(X1)
| big_q(f2(X1))
| ~ big_p(c2)
| big_q(c1)
| ~ big_p(f1(X0))
| ~ big_p(X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p246,plain,
( big_q(X2)
| ~ big_p(X1)
| big_q(X0)
| big_q(f2(X0))
| big_q(c1)
| ~ big_p(f1(c2))
| ~ big_p(c2) ),
inference(factoring,[status(thm)],[c24]) ).
cnf(p253,plain,
( big_q(X1)
| big_q(X0)
| big_q(f2(X0))
| big_q(c1)
| ~ big_p(f1(c2))
| ~ big_p(c2) ),
inference(factoring,[status(thm)],[p246]) ).
cnf(p259,plain,
( big_q(X0)
| big_q(f2(c1))
| big_q(c1)
| ~ big_p(f1(c2))
| ~ big_p(c2) ),
inference(factoring,[status(thm)],[p253]) ).
cnf(p261,plain,
( big_q(f2(c1))
| big_q(c1)
| ~ big_p(f1(c2))
| ~ big_p(c2) ),
inference(factoring,[status(thm)],[p259]) ).
cnf(p5108,plain,
( big_q(f2(c1))
| big_q(c1)
| ~ big_p(f1(c2)) ),
inference(resolution,[status(thm)],[p5107,p261]) ).
cnf(p5131,plain,
( big_q(f2(c1))
| big_q(c1) ),
inference(resolution,[status(thm)],[p5108,p5107]) ).
cnf(f120,negated_conjecture,
( big_q(X15)
| ~ big_p(X14)
| big_q(c16)
| ~ big_q(X13)
| ~ big_p(c15)
| ~ big_q(X12)
| ~ big_p(f3(X10))
| ~ big_p(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_121) ).
fof(f120_nnf,plain,
! [X10,X12,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| big_q(c16)
| ~ big_q(X13)
| ~ big_p(c15)
| ~ big_q(X12)
| ~ big_p(f3(X10))
| ~ big_p(X10) ),
inference(nnf_transformation,[status(thm)],[f120]) ).
fof(f120_sk,plain,
! [X10,X12,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| big_q(c16)
| ~ big_q(X13)
| ~ big_p(c15)
| ~ big_q(X12)
| ~ big_p(f3(X10))
| ~ big_p(X10) ),
inference(skolemisation,[status(esa)],[f120_nnf]) ).
cnf(c120,plain,
( big_q(X4)
| ~ big_p(X3)
| big_q(c16)
| ~ big_q(X2)
| ~ big_p(c15)
| ~ big_q(X1)
| ~ big_p(f3(X0))
| ~ big_p(X0) ),
inference(cnf_transformation,[status(esa)],[f120_sk]) ).
cnf(p729,plain,
( big_q(X3)
| ~ big_p(X2)
| big_q(c16)
| ~ big_q(X1)
| ~ big_q(X0)
| ~ big_p(f3(c15))
| ~ big_p(c15) ),
inference(factoring,[status(thm)],[c120]) ).
cnf(p734,plain,
( big_q(X2)
| big_q(c16)
| ~ big_q(X1)
| ~ big_q(X0)
| ~ big_p(f3(c15))
| ~ big_p(c15) ),
inference(factoring,[status(thm)],[p729]) ).
cnf(p737,plain,
( big_q(X1)
| big_q(c16)
| ~ big_q(X0)
| ~ big_p(f3(c15))
| ~ big_p(c15) ),
inference(factoring,[status(thm)],[p734]) ).
cnf(p739,plain,
( big_q(c16)
| ~ big_q(X0)
| ~ big_p(f3(c15))
| ~ big_p(c15) ),
inference(factoring,[status(thm)],[p737]) ).
cnf(p5118,plain,
( big_q(c16)
| ~ big_q(X0)
| ~ big_p(f3(c15)) ),
inference(resolution,[status(thm)],[p5107,p739]) ).
cnf(p5128,plain,
( big_q(c16)
| ~ big_q(X0) ),
inference(resolution,[status(thm)],[p5118,p5107]) ).
cnf(p5132,plain,
( big_q(c16)
| big_q(c1) ),
inference(resolution,[status(thm)],[p5131,p5128]) ).
cnf(f122,negated_conjecture,
( big_q(X15)
| ~ big_p(X14)
| ~ big_q(c16)
| big_q(X13)
| ~ big_p(c15)
| ~ big_q(X12)
| ~ big_p(f3(X10))
| ~ big_p(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_123) ).
fof(f122_nnf,plain,
! [X10,X12,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| ~ big_q(c16)
| big_q(X13)
| ~ big_p(c15)
| ~ big_q(X12)
| ~ big_p(f3(X10))
| ~ big_p(X10) ),
inference(nnf_transformation,[status(thm)],[f122]) ).
fof(f122_sk,plain,
! [X10,X12,X13,X14,X15] :
( big_q(X15)
| ~ big_p(X14)
| ~ big_q(c16)
| big_q(X13)
| ~ big_p(c15)
| ~ big_q(X12)
| ~ big_p(f3(X10))
| ~ big_p(X10) ),
inference(skolemisation,[status(esa)],[f122_nnf]) ).
cnf(c122,plain,
( big_q(X4)
| ~ big_p(X3)
| ~ big_q(c16)
| big_q(X2)
| ~ big_p(c15)
| ~ big_q(X1)
| ~ big_p(f3(X0))
| ~ big_p(X0) ),
inference(cnf_transformation,[status(esa)],[f122_sk]) ).
cnf(p746,plain,
( big_q(X3)
| ~ big_p(X2)
| ~ big_q(c16)
| big_q(X1)
| ~ big_q(X0)
| ~ big_p(f3(c15))
| ~ big_p(c15) ),
inference(factoring,[status(thm)],[c122]) ).
cnf(p750,plain,
( big_q(X2)
| ~ big_q(c16)
| big_q(X1)
| ~ big_q(X0)
| ~ big_p(f3(c15))
| ~ big_p(c15) ),
inference(factoring,[status(thm)],[p746]) ).
cnf(p753,plain,
( big_q(X1)
| big_q(X0)
| ~ big_q(c16)
| ~ big_p(f3(c15))
| ~ big_p(c15) ),
inference(factoring,[status(thm)],[p750]) ).
cnf(p755,plain,
( big_q(X0)
| ~ big_q(c16)
| ~ big_p(f3(c15))
| ~ big_p(c15) ),
inference(factoring,[status(thm)],[p753]) ).
cnf(p5120,plain,
( big_q(X0)
| ~ big_q(c16)
| ~ big_p(f3(c15)) ),
inference(resolution,[status(thm)],[p5107,p755]) ).
cnf(p5130,plain,
( big_q(X0)
| ~ big_q(c16) ),
inference(resolution,[status(thm)],[p5120,p5107]) ).
cnf(p5134,plain,
( big_q(X0)
| big_q(c1) ),
inference(resolution,[status(thm)],[p5132,p5130]) ).
cnf(p5135,plain,
big_q(c1),
inference(factoring,[status(thm)],[p5134]) ).
cnf(p5136,plain,
big_q(c16),
inference(resolution,[status(thm)],[p5135,p5128]) ).
cnf(p5137,plain,
big_q(X0),
inference(resolution,[status(thm)],[p5136,p5130]) ).
cnf(p5140,plain,
( ~ big_q(c20)
| ~ big_q(X0) ),
inference(resolution,[status(thm)],[p5138,p5137]) ).
cnf(p5141,plain,
~ big_q(c20),
inference(factoring,[status(thm)],[p5140]) ).
cnf(p5142,plain,
$false,
inference(resolution,[status(thm)],[p5141,p5137]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN036-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.03/0.33 % Computer : n012.cluster.edu
% 0.03/0.33 % Model : x86_64 x86_64
% 0.03/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.33 % Memory : 8046.5625MB
% 0.03/0.33 % OS : Linux 6.8.0-71-generic
% 0.03/0.33 % CPULimit : 300
% 0.03/0.33 % WCLimit : 300
% 0.03/0.33 % DateTime : Thu Sep 24 23:52:35 UTC 2026
% 0.03/0.33 % CPUTime :
% 0.03/0.33 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.94/1.79 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.94/1.79 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------