%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYO657-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n019.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:48:36 PM UTC 2026
% Result : Unsatisfiable 6.48s 1.75s
% Output : Proof 6.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 16
% Syntax : Number of formulae : 198 ( 11 unt; 0 def)
% Number of atoms : 909 ( 0 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 1087 ( 376 ~; 711 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 194 ( 2 sgn 38 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f3,axiom,
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_23) ).
fof(f3_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1)) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1)) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(f13,axiom,
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(suc(B_5))))
| ~ qtd2(f(suc(suc(B_5))),s(qtd1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_51) ).
fof(f13_nnf,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(suc(B_5))))
| ~ qtd2(f(suc(suc(B_5))),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(suc(B_5))))
| ~ qtd2(f(suc(suc(B_5))),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(f6,axiom,
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(B_2))
| ~ qtd2(f(B_2),s(s(qtd1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_9) ).
fof(f6_nnf,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(B_2))
| ~ qtd2(f(B_2),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(B_2))
| ~ qtd2(f(B_2),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd2(f(X0),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(f2,axiom,
qtd2(f(A),s(s(qtd1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_17) ).
fof(f2_nnf,plain,
! [A] : qtd2(f(A),s(s(qtd1))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A] : qtd2(f(A),s(s(qtd1))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
qtd2(f(X0),s(s(qtd1))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p25,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[c6,c2]) ).
cnf(p29,plain,
( qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c13,p25]) ).
cnf(p34,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[c3,p29]) ).
cnf(f15,axiom,
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(B_2)))
| ~ qtd2(f(suc(B_2)),s(s(qtd1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_32) ).
fof(f15_nnf,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(B_2)))
| ~ qtd2(f(suc(B_2)),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(B_2)))
| ~ qtd2(f(suc(B_2)),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p30,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[c15,c2]) ).
cnf(p165,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p34,p30]) ).
cnf(f17,axiom,
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
fof(f17_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(A_1)))) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(A_1)))) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(f1,axiom,
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_2))))
| ~ qtd2(f(suc(suc(B_2))),s(s(qtd1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_45) ).
fof(f1_nnf,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_2))))
| ~ qtd2(f(suc(suc(B_2))),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_2))))
| ~ qtd2(f(suc(suc(B_2))),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p28,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c1,c2]) ).
cnf(p57,plain,
( qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[c17,p28]) ).
cnf(p64,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p57,p30]) ).
cnf(p65,plain,
( qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p64]) ).
cnf(p212,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p165,p65]) ).
cnf(p422,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p212]) ).
cnf(p457,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p422]) ).
cnf(p458,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p457,p29]) ).
cnf(p459,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p458]) ).
cnf(p461,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p459]) ).
cnf(f19,axiom,
( ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_3),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_33) ).
fof(f19_nnf,plain,
! [A_1,B_3] :
( ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_3),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [A_1,B_3] :
( ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_3),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X1))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p124,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c19]) ).
cnf(p337,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p124]) ).
cnf(p344,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p337]) ).
cnf(p346,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p344]) ).
cnf(p465,plain,
( ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p461,p346]) ).
cnf(p556,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p465,p28]) ).
cnf(p691,plain,
( ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p556]) ).
cnf(p822,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p691,p29]) ).
cnf(p831,plain,
( qtd2(f(X0),qtd1)
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p822]) ).
cnf(p833,plain,
( ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p831]) ).
cnf(p834,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p833,p30]) ).
cnf(p835,plain,
( ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p834]) ).
cnf(f16,axiom,
( qtd0(f(B_3),f(suc(B_3)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_52) ).
fof(f16_nnf,plain,
! [A_1,B_3] :
( qtd0(f(B_3),f(suc(B_3)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A_1,B_3] :
( qtd0(f(B_3),f(suc(B_3)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p97,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c16]) ).
cnf(p144,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p97]) ).
cnf(p145,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p144]) ).
cnf(p464,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p461,p145]) ).
cnf(p554,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p464,p29]) ).
cnf(p687,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p554]) ).
cnf(p698,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p687]) ).
cnf(p699,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p698,p30]) ).
cnf(p702,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p699]) ).
cnf(p836,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p835,p702]) ).
cnf(p839,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p836]) ).
cnf(p840,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p839]) ).
cnf(p842,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p840]) ).
cnf(p843,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p842,c13]) ).
cnf(p844,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p843]) ).
cnf(p846,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p844]) ).
cnf(f8,axiom,
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(suc(A_2)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_41) ).
fof(f8_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(suc(A_2)))) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(suc(A_2)))) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p850,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p846,c8]) ).
cnf(f12,axiom,
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(B_5)))
| ~ qtd2(f(suc(B_5)),s(qtd1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_40) ).
fof(f12_nnf,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(B_5)))
| ~ qtd2(f(suc(B_5)),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(B_5)))
| ~ qtd2(f(suc(B_5)),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p27,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p25,c12]) ).
cnf(p32,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c3,p27]) ).
cnf(p93,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p32,p30]) ).
cnf(p94,plain,
( qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p93,p65]) ).
cnf(p298,plain,
( qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p94]) ).
cnf(p300,plain,
( ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p298]) ).
cnf(p301,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p300,p27]) ).
cnf(p304,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p301]) ).
cnf(p306,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p304]) ).
cnf(p353,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p346,p306]) ).
cnf(p528,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p353,p28]) ).
cnf(p557,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p528]) ).
cnf(p558,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p557,p27]) ).
cnf(p560,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p558]) ).
cnf(p562,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p560]) ).
cnf(p563,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p562,p30]) ).
cnf(p564,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p563]) ).
cnf(p311,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p306,p145]) ).
cnf(p319,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p311,p27]) ).
cnf(p333,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p319]) ).
cnf(p335,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p333]) ).
cnf(p341,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p335,p30]) ).
cnf(p342,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p341]) ).
cnf(p565,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p564,p342]) ).
cnf(p570,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p565]) ).
cnf(p571,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p570]) ).
cnf(p573,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p571]) ).
cnf(p574,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p573,c12]) ).
cnf(p576,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p574]) ).
cnf(p578,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p576]) ).
cnf(p919,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p850,p578]) ).
cnf(p921,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p919]) ).
cnf(f7,axiom,
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(B_5))
| ~ qtd2(f(B_5),s(qtd1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_34) ).
fof(f7_nnf,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(B_5))
| ~ qtd2(f(B_5),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(B_5))
| ~ qtd2(f(B_5),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd2(f(X0),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p26,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p25,c7]) ).
cnf(p31,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[c3,p26]) ).
cnf(p40,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p31,p30]) ).
cnf(p66,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p65,p40]) ).
cnf(p166,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p66]) ).
cnf(p168,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p166]) ).
cnf(p169,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p168,p26]) ).
cnf(p173,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p169]) ).
cnf(p176,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p173]) ).
cnf(p177,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p176,c7]) ).
cnf(p183,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p177]) ).
cnf(p185,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p183]) ).
cnf(p348,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p346,p185]) ).
cnf(p357,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p348,p28]) ).
cnf(p360,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p357,p26]) ).
cnf(p370,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p360]) ).
cnf(p372,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p370]) ).
cnf(p377,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p372,p30]) ).
cnf(p378,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p377]) ).
cnf(p188,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p185,p145]) ).
cnf(p189,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p188,p26]) ).
cnf(p194,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p189]) ).
cnf(p196,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p194]) ).
cnf(p201,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p196,p30]) ).
cnf(p380,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p378,p201]) ).
cnf(p402,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p380]) ).
cnf(p403,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p402]) ).
cnf(p405,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p403]) ).
cnf(p407,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p405,c7]) ).
cnf(p410,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p407]) ).
cnf(p412,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p410]) ).
cnf(f14,axiom,
~ qtd2(f(z),qtd1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_24) ).
fof(f14_nnf,plain,
~ qtd2(f(z),qtd1),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
~ qtd2(f(z),qtd1),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
~ qtd2(f(z),qtd1),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p413,plain,
qtd0(qtd1,f(z)),
inference(resolution,[status(thm)],[p412,c14]) ).
cnf(f10,axiom,
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(A_2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_26) ).
fof(f10_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(A_2)) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(A_2)) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p416,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p413,c10]) ).
cnf(p597,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p578,p416]) ).
cnf(p925,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p921,p597]) ).
cnf(p928,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p925]) ).
cnf(p929,plain,
( iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p928]) ).
cnf(p930,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p929,p413]) ).
cnf(f11,axiom,
( ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_43) ).
fof(f11_nnf,plain,
! [A_2,B_6] :
( ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A_2,B_6] :
( ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X1))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p82,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c11]) ).
cnf(p279,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p82]) ).
cnf(p283,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p279]) ).
cnf(p284,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p283]) ).
cnf(p594,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p578,p284]) ).
cnf(p871,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p846,p594]) ).
cnf(p914,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p871]) ).
cnf(p915,plain,
( ~ qtd0(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p914,p413]) ).
cnf(p937,plain,
( ~ qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p930,p915]) ).
cnf(p939,plain,
( ~ qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p937]) ).
cnf(f0,axiom,
( qtd0(f(B_6),f(suc(B_6)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(A_2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_10) ).
fof(f0_nnf,plain,
! [A_2,B_6] :
( qtd0(f(B_6),f(suc(B_6)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A_2,B_6] :
( qtd0(f(B_6),f(suc(B_6)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p24,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c0]) ).
cnf(p78,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p24]) ).
cnf(p90,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p78]) ).
cnf(p585,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p578,p90]) ).
cnf(p612,plain,
( qtd0(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p585,p413]) ).
cnf(p936,plain,
( qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p930,p612]) ).
cnf(p938,plain,
( qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p936]) ).
cnf(p940,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p939,p938]) ).
cnf(p941,plain,
qtd2(f(z),qtd1),
inference(factoring,[status(thm)],[p940]) ).
cnf(p942,plain,
$false,
inference(resolution,[status(thm)],[p941,c14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO657-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n019.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 03:21:03 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.48/1.75 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.48/1.75 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------