%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYO664-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n006.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:37 PM UTC 2026
% Result : Unsatisfiable 29.91s 13.43s
% Output : Proof 29.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 10
% Syntax : Number of formulae : 97 ( 11 unt; 0 def)
% Number of atoms : 478 ( 0 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 715 ( 334 ~; 381 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 4 ( 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 : 129 ( 2 sgn 34 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f0,axiom,
( ~ qtd0(s(qtd1),f(suc(B_44)))
| ~ iLEQ(suc(B_43),suc(B_44))
| ~ iLEQ(suc(B_45),suc(B_46))
| ~ qtd0(s(qtd1),f(B_44))
| ~ qtd0(s(qtd1),f(B_46))
| ~ iLEQ(suc(B_44),suc(B_45))
| ~ qtd0(s(qtd1),f(B_43))
| ~ iLEQ(suc(A_1),suc(B_43))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(B_43)))
| ~ qtd0(s(qtd1),f(suc(B_46)))
| ~ qtd0(s(qtd1),f(B_45))
| ~ qtd0(s(qtd1),f(suc(B_45))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_37) ).
fof(f0_nnf,plain,
! [B_45,B_46,B_43,A_1,B_44] :
( ~ qtd0(s(qtd1),f(suc(B_44)))
| ~ iLEQ(suc(B_43),suc(B_44))
| ~ iLEQ(suc(B_45),suc(B_46))
| ~ qtd0(s(qtd1),f(B_44))
| ~ qtd0(s(qtd1),f(B_46))
| ~ iLEQ(suc(B_44),suc(B_45))
| ~ qtd0(s(qtd1),f(B_43))
| ~ iLEQ(suc(A_1),suc(B_43))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(B_43)))
| ~ qtd0(s(qtd1),f(suc(B_46)))
| ~ qtd0(s(qtd1),f(B_45))
| ~ qtd0(s(qtd1),f(suc(B_45))) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [B_45,B_46,B_43,A_1,B_44] :
( ~ qtd0(s(qtd1),f(suc(B_44)))
| ~ iLEQ(suc(B_43),suc(B_44))
| ~ iLEQ(suc(B_45),suc(B_46))
| ~ qtd0(s(qtd1),f(B_44))
| ~ qtd0(s(qtd1),f(B_46))
| ~ iLEQ(suc(B_44),suc(B_45))
| ~ qtd0(s(qtd1),f(B_43))
| ~ iLEQ(suc(A_1),suc(B_43))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(B_43)))
| ~ qtd0(s(qtd1),f(suc(B_46)))
| ~ qtd0(s(qtd1),f(B_45))
| ~ qtd0(s(qtd1),f(suc(B_45))) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ qtd0(s(qtd1),f(suc(X4)))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(qtd1),f(X4))
| ~ qtd0(s(qtd1),f(X1))
| ~ iLEQ(suc(X4),suc(X0))
| ~ qtd0(s(qtd1),f(X2))
| ~ iLEQ(suc(X3),suc(X2))
| ~ qtd0(s(qtd1),f(suc(X3)))
| ~ qtd0(s(qtd1),f(X3))
| ~ qtd0(s(qtd1),f(suc(X2)))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p10,plain,
( ~ qtd0(s(qtd1),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X3))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X3),suc(X0))
| ~ qtd0(s(qtd1),f(X1))
| ~ iLEQ(suc(X2),suc(X1))
| ~ qtd0(s(qtd1),f(suc(X2)))
| ~ qtd0(s(qtd1),f(X2))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[c0]) ).
cnf(p112,plain,
( ~ qtd0(s(qtd1),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X2))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p10]) ).
cnf(p661,plain,
( ~ qtd0(s(qtd1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p112]) ).
cnf(p675,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p661]) ).
cnf(p692,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p675]) ).
cnf(p694,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p692]) ).
cnf(p696,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p694]) ).
cnf(p698,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p696]) ).
cnf(p709,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p698]) ).
cnf(p710,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p709]) ).
cnf(p711,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p710]) ).
cnf(f9,axiom,
( qtd2(f(B_42),s(qtd1))
| qtd0(s(qtd1),f(suc(B_42)))
| ~ qtd2(f(suc(B_42)),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_83) ).
fof(f9_nnf,plain,
! [B_42] :
( qtd2(f(B_42),s(qtd1))
| qtd0(s(qtd1),f(suc(B_42)))
| ~ qtd2(f(suc(B_42)),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [B_42] :
( qtd2(f(B_42),s(qtd1))
| qtd0(s(qtd1),f(suc(B_42)))
| ~ qtd2(f(suc(B_42)),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(f4,axiom,
qtd2(f(A),s(s(qtd1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_58) ).
fof(f4_nnf,plain,
! [A] : qtd2(f(A),s(s(qtd1))),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A] : qtd2(f(A),s(s(qtd1))),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
qtd2(f(X0),s(s(qtd1))),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p109,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[c9,c4]) ).
cnf(p714,plain,
( qtd2(f(X0),s(qtd1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p711,p109]) ).
cnf(f2,axiom,
( qtd2(f(B_42),s(qtd1))
| qtd0(s(qtd1),f(B_42))
| ~ qtd2(f(B_42),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_20) ).
fof(f2_nnf,plain,
! [B_42] :
( qtd2(f(B_42),s(qtd1))
| qtd0(s(qtd1),f(B_42))
| ~ qtd2(f(B_42),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [B_42] :
( qtd2(f(B_42),s(qtd1))
| qtd0(s(qtd1),f(B_42))
| ~ qtd2(f(B_42),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd2(f(X0),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p56,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[c2,c4]) ).
cnf(f6,axiom,
( qtd2(f(B_60),qtd1)
| qtd0(qtd1,f(suc(B_60)))
| ~ qtd2(f(suc(B_60)),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_117) ).
fof(f6_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)],[f6]) ).
fof(f6_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)],[f6_nnf]) ).
cnf(c6,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p58,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p56,c6]) ).
cnf(p727,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p714,p58]) ).
cnf(f8,axiom,
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_50) ).
fof(f8_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1)) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1)) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p108,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c8,p58]) ).
cnf(p175,plain,
( 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)],[p108,p109]) ).
cnf(p758,plain,
( qtd2(f(suc(X0)),s(qtd1))
| 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)],[p727,p175]) ).
cnf(p837,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(factoring,[status(thm)],[p758]) ).
cnf(p840,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p837]) ).
cnf(p842,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p840]) ).
cnf(p843,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p842,c6]) ).
cnf(p850,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p843]) ).
cnf(p852,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p850]) ).
cnf(f7,axiom,
( qtd2(f(B_60),qtd1)
| qtd0(qtd1,f(B_60))
| ~ qtd2(f(B_60),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_94) ).
fof(f7_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)],[f7]) ).
fof(f7_sk,plain,
! [B_60] :
( qtd2(f(B_60),qtd1)
| qtd0(qtd1,f(B_60))
| ~ qtd2(f(B_60),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(p57,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p56,c7]) ).
cnf(p726,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p714,p57]) ).
cnf(p107,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[c8,p57]) ).
cnf(p144,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p107,p109]) ).
cnf(p145,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)],[p144,c7]) ).
cnf(p171,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p145]) ).
cnf(p173,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p171]) ).
cnf(p735,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p726,p173]) ).
cnf(p799,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p735]) ).
cnf(p801,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p799]) ).
cnf(p802,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p801,c7]) ).
cnf(p804,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p802]) ).
cnf(p813,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p804]) ).
cnf(f1,axiom,
~ qtd2(f(z),qtd1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_70) ).
fof(f1_nnf,plain,
~ qtd2(f(z),qtd1),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
~ qtd2(f(z),qtd1),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
~ qtd2(f(z),qtd1),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p814,plain,
qtd0(qtd1,f(z)),
inference(resolution,[status(thm)],[p813,c1]) ).
cnf(f3,axiom,
( ~ qtd0(qtd1,f(B_62))
| ~ qtd0(qtd1,f(suc(B_64)))
| ~ qtd0(qtd1,f(B_61))
| ~ qtd0(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(B_63),suc(B_64))
| ~ qtd0(qtd1,f(B_64))
| ~ iLEQ(suc(B_62),suc(B_63))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(B_63)))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ iLEQ(suc(A_2),suc(B_61))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(B_61)))
| ~ qtd0(qtd1,f(B_63)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_66) ).
fof(f3_nnf,plain,
! [B_63,B_61,A_2,B_62,B_64] :
( ~ qtd0(qtd1,f(B_62))
| ~ qtd0(qtd1,f(suc(B_64)))
| ~ qtd0(qtd1,f(B_61))
| ~ qtd0(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(B_63),suc(B_64))
| ~ qtd0(qtd1,f(B_64))
| ~ iLEQ(suc(B_62),suc(B_63))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(B_63)))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ iLEQ(suc(A_2),suc(B_61))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(B_61)))
| ~ qtd0(qtd1,f(B_63)) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [B_63,B_61,A_2,B_62,B_64] :
( ~ qtd0(qtd1,f(B_62))
| ~ qtd0(qtd1,f(suc(B_64)))
| ~ qtd0(qtd1,f(B_61))
| ~ qtd0(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(B_63),suc(B_64))
| ~ qtd0(qtd1,f(B_64))
| ~ iLEQ(suc(B_62),suc(B_63))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(B_63)))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ iLEQ(suc(A_2),suc(B_61))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(B_61)))
| ~ qtd0(qtd1,f(B_63)) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( ~ qtd0(qtd1,f(X3))
| ~ qtd0(qtd1,f(suc(X4)))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X3)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ qtd0(qtd1,f(X4))
| ~ iLEQ(suc(X3),suc(X0))
| ~ qtd0(qtd1,f(X2))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| ~ qtd0(qtd1,f(suc(X2)))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X0)) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p68,plain,
( ~ qtd0(qtd1,f(X2))
| ~ qtd0(qtd1,f(suc(X3)))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X3))
| ~ qtd0(qtd1,f(X3))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X1),suc(X1))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[c3]) ).
cnf(p231,plain,
( ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X2)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ qtd0(qtd1,f(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p68]) ).
cnf(p253,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(qtd1,f(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p231]) ).
cnf(p265,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p253]) ).
cnf(p268,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p265]) ).
cnf(p297,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p268]) ).
cnf(p299,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p297]) ).
cnf(p300,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p299]) ).
cnf(p301,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p300]) ).
cnf(p328,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p301]) ).
cnf(p329,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p328]) ).
cnf(p817,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p814,p329]) ).
cnf(p884,plain,
( ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p852,p817]) ).
cnf(f5,axiom,
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(A_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6) ).
fof(f5_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(A_2)) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(A_2)) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p815,plain,
( iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p814,c5]) ).
cnf(p883,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p852,p815]) ).
cnf(p890,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p884,p883]) ).
cnf(p891,plain,
qtd2(f(z),qtd1),
inference(factoring,[status(thm)],[p890]) ).
cnf(p892,plain,
$false,
inference(resolution,[status(thm)],[p891,c1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO664-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/5.53 % Computer : n006.cluster.edu
% 0.11/5.53 % Model : x86_64 x86_64
% 0.11/5.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.53 % Memory : 8046.5625MB
% 0.11/5.53 % OS : Linux 6.8.0-71-generic
% 0.11/5.53 % CPULimit : 300
% 0.11/5.53 % WCLimit : 300
% 0.11/5.53 % DateTime : Fri Sep 25 03:21:16 UTC 2026
% 0.11/5.53 % CPUTime :
% 0.11/5.53 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 29.91/13.43 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.91/13.43 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------