%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYO680-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 : n013.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:38 PM UTC 2026
% Result : Unsatisfiable 5.32s 1.21s
% Output : Proof 5.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 18
% Syntax : Number of formulae : 185 ( 11 unt; 0 def)
% Number of atoms : 707 ( 0 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 851 ( 329 ~; 522 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 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 : 211 ( 2 sgn 50 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f6,axiom,
( ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_25)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_24)))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_24))
| ~ qtd0(s(s(s(qtd1))),f(B_24))
| ~ qtd0(s(s(s(qtd1))),f(B_25))
| ~ iLEQ(suc(B_24),suc(B_25)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_71) ).
fof(f6_nnf,plain,
! [B_24,B_25,A_1] :
( ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_25)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_24)))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_24))
| ~ qtd0(s(s(s(qtd1))),f(B_24))
| ~ qtd0(s(s(s(qtd1))),f(B_25))
| ~ iLEQ(suc(B_24),suc(B_25)) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [B_24,B_25,A_1] :
( ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_25)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_24)))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_24))
| ~ qtd0(s(s(s(qtd1))),f(B_24))
| ~ qtd0(s(s(s(qtd1))),f(B_25))
| ~ iLEQ(suc(B_24),suc(B_25)) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(X2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X1))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p33,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(X1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c6]) ).
cnf(p228,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(X1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p33]) ).
cnf(p308,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p228]) ).
cnf(p323,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p308]) ).
cnf(p324,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p323]) ).
cnf(f11,axiom,
( qtd2(f(B_23),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_23))
| ~ qtd2(f(B_23),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_127) ).
fof(f11_nnf,plain,
! [B_23] :
( qtd2(f(B_23),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_23))
| ~ qtd2(f(B_23),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [B_23] :
( qtd2(f(B_23),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_23))
| ~ qtd2(f(B_23),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(f1,axiom,
qtd2(f(A),s(s(s(s(qtd1))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_104) ).
fof(f1_nnf,plain,
! [A] : qtd2(f(A),s(s(s(s(qtd1))))),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A] : qtd2(f(A),s(s(s(s(qtd1))))),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
qtd2(f(X0),s(s(s(s(qtd1))))),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p31,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[c11,c1]) ).
cnf(f9,axiom,
( qtd2(f(B_41),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_41)))
| ~ qtd2(f(suc(B_41)),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_84) ).
fof(f9_nnf,plain,
! [B_41] :
( qtd2(f(B_41),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_41)))
| ~ qtd2(f(suc(B_41)),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [B_41] :
( qtd2(f(B_41),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_41)))
| ~ qtd2(f(suc(B_41)),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p46,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p31,c9]) ).
cnf(f15,axiom,
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(A_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_14) ).
fof(f15_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(A_1)) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(A_1)) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p48,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p46,c15]) ).
cnf(f14,axiom,
( qtd2(f(B_23),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_23)))
| ~ qtd2(f(suc(B_23)),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_102) ).
fof(f14_nnf,plain,
! [B_23] :
( qtd2(f(B_23),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_23)))
| ~ qtd2(f(suc(B_23)),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [B_23] :
( qtd2(f(B_23),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_23)))
| ~ qtd2(f(suc(B_23)),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p49,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c14,c1]) ).
cnf(p101,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p48,p49]) ).
cnf(p108,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p101,c9]) ).
cnf(p148,plain,
( qtd2(f(X0),s(s(qtd1)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p108]) ).
cnf(p150,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p148]) ).
cnf(p331,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p324,p150]) ).
cnf(p341,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p331,p46]) ).
cnf(p465,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p341]) ).
cnf(p467,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p465]) ).
cnf(p468,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p467,p49]) ).
cnf(p469,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p468,c9]) ).
cnf(p473,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p469]) ).
cnf(p475,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p473]) ).
cnf(f12,axiom,
( qtd2(f(B_41),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_41))
| ~ qtd2(f(B_41),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_51) ).
fof(f12_nnf,plain,
! [B_41] :
( qtd2(f(B_41),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_41))
| ~ qtd2(f(B_41),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [B_41] :
( qtd2(f(B_41),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_41))
| ~ qtd2(f(B_41),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p45,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p31,c12]) ).
cnf(p47,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p45,c15]) ).
cnf(p72,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p47,p49]) ).
cnf(p87,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p72,c12]) ).
cnf(p119,plain,
( qtd2(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p87]) ).
cnf(p124,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p119]) ).
cnf(p328,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p324,p124]) ).
cnf(p338,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p328,p45]) ).
cnf(p381,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p338]) ).
cnf(p383,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p381]) ).
cnf(p384,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p383,p49]) ).
cnf(p385,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p384,c12]) ).
cnf(p387,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p385]) ).
cnf(p389,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p387]) ).
cnf(f17,axiom,
( qtd2(f(B_53),s(qtd1))
| qtd0(s(qtd1),f(suc(B_53)))
| ~ qtd2(f(suc(B_53)),s(s(qtd1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_15) ).
fof(f17_nnf,plain,
! [B_53] :
( qtd2(f(B_53),s(qtd1))
| qtd0(s(qtd1),f(suc(B_53)))
| ~ qtd2(f(suc(B_53)),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [B_53] :
( qtd2(f(B_53),s(qtd1))
| qtd0(s(qtd1),f(suc(B_53)))
| ~ qtd2(f(suc(B_53)),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p391,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p389,c17]) ).
cnf(f4,axiom,
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
fof(f4_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2)) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2)) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p404,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p391,c4]) ).
cnf(p490,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p475,p404]) ).
cnf(p534,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p490,c17]) ).
cnf(p641,plain,
( qtd2(f(X0),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p534]) ).
cnf(p643,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p641]) ).
cnf(f5,axiom,
( ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(B_43))
| ~ iLEQ(suc(A_2),suc(B_42))
| ~ qtd0(s(s(qtd1)),f(suc(B_43)))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ iLEQ(suc(B_42),suc(B_43))
| ~ qtd0(s(s(qtd1)),f(B_42))
| ~ qtd0(s(s(qtd1)),f(suc(B_42))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_20) ).
fof(f5_nnf,plain,
! [B_42,B_43,A_2] :
( ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(B_43))
| ~ iLEQ(suc(A_2),suc(B_42))
| ~ qtd0(s(s(qtd1)),f(suc(B_43)))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ iLEQ(suc(B_42),suc(B_43))
| ~ qtd0(s(s(qtd1)),f(B_42))
| ~ qtd0(s(s(qtd1)),f(suc(B_42))) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [B_42,B_43,A_2] :
( ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(B_43))
| ~ iLEQ(suc(A_2),suc(B_42))
| ~ qtd0(s(s(qtd1)),f(suc(B_43)))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ iLEQ(suc(B_42),suc(B_43))
| ~ qtd0(s(s(qtd1)),f(B_42))
| ~ qtd0(s(s(qtd1)),f(suc(B_42))) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ~ qtd0(s(s(qtd1)),f(X2))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p18,plain,
( ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[c5]) ).
cnf(p102,plain,
( ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p18]) ).
cnf(p185,plain,
( ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p102]) ).
cnf(p187,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p185]) ).
cnf(p189,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p187]) ).
cnf(p484,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p475,p189]) ).
cnf(p496,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p484,p391]) ).
cnf(p648,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p643,p496]) ).
cnf(p650,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p648]) ).
cnf(p652,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p650]) ).
cnf(p653,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p652,c17]) ).
cnf(p654,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p653]) ).
cnf(p656,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p654]) ).
cnf(f7,axiom,
( qtd2(f(B_53),s(qtd1))
| qtd0(s(qtd1),f(B_53))
| ~ qtd2(f(B_53),s(s(qtd1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6) ).
fof(f7_nnf,plain,
! [B_53] :
( qtd2(f(B_53),s(qtd1))
| qtd0(s(qtd1),f(B_53))
| ~ qtd2(f(B_53),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [B_53] :
( qtd2(f(B_53),s(qtd1))
| qtd0(s(qtd1),f(B_53))
| ~ qtd2(f(B_53),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd2(f(X0),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p125,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p124,c7]) ).
cnf(p129,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p125,c4]) ).
cnf(p139,plain,
( ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p129]) ).
cnf(p479,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p475,p139]) ).
cnf(p515,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p479,c7]) ).
cnf(p567,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p515]) ).
cnf(p569,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p567]) ).
cnf(p390,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p389,c7]) ).
cnf(p495,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p484,p390]) ).
cnf(p576,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p569,p495]) ).
cnf(p600,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p576]) ).
cnf(p602,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p600]) ).
cnf(p603,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p602,c7]) ).
cnf(p605,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p603]) ).
cnf(p607,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p605]) ).
cnf(f3,axiom,
( qtd2(f(B_60),qtd1)
| qtd0(qtd1,f(suc(B_60)))
| ~ qtd2(f(suc(B_60)),s(qtd1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_114) ).
fof(f3_nnf,plain,
! [B_60] :
( qtd2(f(B_60),qtd1)
| qtd0(qtd1,f(suc(B_60)))
| ~ qtd2(f(suc(B_60)),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [B_60] :
( qtd2(f(B_60),qtd1)
| qtd0(qtd1,f(suc(B_60)))
| ~ qtd2(f(suc(B_60)),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p609,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p607,c3]) ).
cnf(f2,axiom,
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(A_3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_91) ).
fof(f2_nnf,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(A_3)) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(A_3)) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p611,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p609,c2]) ).
cnf(p659,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p656,p611]) ).
cnf(f13,axiom,
( ~ qtd0(s(qtd1),f(B_54))
| ~ qtd0(s(qtd1),f(suc(B_54)))
| ~ qtd0(s(qtd1),f(B_55))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(s(qtd1),f(suc(B_55)))
| ~ iLEQ(suc(A_3),suc(B_54))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ iLEQ(suc(B_54),suc(B_55)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_21) ).
fof(f13_nnf,plain,
! [B_54,B_55,A_3] :
( ~ qtd0(s(qtd1),f(B_54))
| ~ qtd0(s(qtd1),f(suc(B_54)))
| ~ qtd0(s(qtd1),f(B_55))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(s(qtd1),f(suc(B_55)))
| ~ iLEQ(suc(A_3),suc(B_54))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ iLEQ(suc(B_54),suc(B_55)) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [B_54,B_55,A_3] :
( ~ qtd0(s(qtd1),f(B_54))
| ~ qtd0(s(qtd1),f(suc(B_54)))
| ~ qtd0(s(qtd1),f(B_55))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(s(qtd1),f(suc(B_55)))
| ~ iLEQ(suc(A_3),suc(B_54))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ iLEQ(suc(B_54),suc(B_55)) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(X2))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p74,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(factoring,[status(thm)],[c13]) ).
cnf(p233,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p74]) ).
cnf(p236,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p233]) ).
cnf(p238,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p236]) ).
cnf(p243,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p238]) ).
cnf(p679,plain,
( ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p659,p243]) ).
cnf(p722,plain,
( qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p679,p656]) ).
cnf(p723,plain,
( ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p722]) ).
cnf(p724,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p723,p609]) ).
cnf(p725,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p724]) ).
cnf(p727,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p725]) ).
cnf(p728,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p727,c3]) ).
cnf(p729,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p728]) ).
cnf(p732,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p729]) ).
cnf(f10,axiom,
( ~ qtd0(qtd1,f(A_4))
| ~ qtd0(qtd1,f(B_62))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(B_61))
| ~ qtd0(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(A_4),suc(B_61))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ qtd0(qtd1,f(suc(B_61))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_144) ).
fof(f10_nnf,plain,
! [B_61,B_62,A_4] :
( ~ qtd0(qtd1,f(A_4))
| ~ qtd0(qtd1,f(B_62))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(B_61))
| ~ qtd0(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(A_4),suc(B_61))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ qtd0(qtd1,f(suc(B_61))) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [B_61,B_62,A_4] :
( ~ qtd0(qtd1,f(A_4))
| ~ qtd0(qtd1,f(B_62))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(B_61))
| ~ qtd0(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(A_4),suc(B_61))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ qtd0(qtd1,f(suc(B_61))) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( ~ qtd0(qtd1,f(X2))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X2)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p50,plain,
( ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c10]) ).
cnf(p153,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p50]) ).
cnf(p163,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p153]) ).
cnf(p165,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p163]) ).
cnf(p166,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p165]) ).
cnf(p735,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p732,p166]) ).
cnf(f16,axiom,
( qtd2(f(B_60),qtd1)
| qtd0(qtd1,f(B_60))
| ~ qtd2(f(B_60),s(qtd1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_96) ).
fof(f16_nnf,plain,
! [B_60] :
( qtd2(f(B_60),qtd1)
| qtd0(qtd1,f(B_60))
| ~ qtd2(f(B_60),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [B_60] :
( qtd2(f(B_60),qtd1)
| qtd0(qtd1,f(B_60))
| ~ qtd2(f(B_60),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd2(f(X0),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p608,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p607,c16]) ).
cnf(p610,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p608,c2]) ).
cnf(p658,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p656,p610]) ).
cnf(p669,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p658,c16]) ).
cnf(p683,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p669]) ).
cnf(p685,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p683]) ).
cnf(p688,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p685,p243]) ).
cnf(p692,plain,
( qtd2(f(X0),s(qtd1))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p688,p656]) ).
cnf(p693,plain,
( 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)],[p692,p608]) ).
cnf(p698,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p693]) ).
cnf(p700,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p698]) ).
cnf(p701,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p700,c16]) ).
cnf(p703,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p701]) ).
cnf(p705,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p703]) ).
cnf(f8,axiom,
~ qtd2(f(z),qtd1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_66) ).
fof(f8_nnf,plain,
~ qtd2(f(z),qtd1),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
~ qtd2(f(z),qtd1),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
~ qtd2(f(z),qtd1),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p706,plain,
qtd0(qtd1,f(z)),
inference(resolution,[status(thm)],[p705,c8]) ).
cnf(f0,axiom,
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_109) ).
fof(f0_nnf,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4)) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4)) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p708,plain,
( iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p706,c0]) ).
cnf(p750,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p732,p708]) ).
cnf(p756,plain,
( qtd2(f(z),qtd1)
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p735,p750]) ).
cnf(p757,plain,
( ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p756]) ).
cnf(p758,plain,
qtd2(f(z),qtd1),
inference(resolution,[status(thm)],[p757,p706]) ).
cnf(p759,plain,
$false,
inference(resolution,[status(thm)],[p758,c8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO680-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n013.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 03:22:36 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.32/1.21 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.32/1.21 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------