%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYO671-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 : n009.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 23.76s 63.30s
% Output : Proof 23.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 23
% Syntax : Number of formulae : 359 ( 11 unt; 0 def)
% Number of atoms : 1937 ( 0 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 2488 ( 910 ~;1578 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 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 : 392 ( 2 sgn 68 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f7,axiom,
( ~ qtd0(s(s(qtd1)),f(suc(suc(B_17))))
| ~ qtd0(s(s(qtd1)),f(suc(B_18)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_17))
| ~ qtd0(f(B_17),f(suc(B_17)))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_18),f(suc(B_18)))
| ~ qtd0(s(s(qtd1)),f(B_18))
| ~ iLEQ(suc(B_17),suc(B_18))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(B_18))))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17)))
| ~ qtd0(s(s(qtd1)),f(A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_20) ).
fof(f7_nnf,plain,
! [A_1,B_17,B_18] :
( ~ qtd0(s(s(qtd1)),f(suc(suc(B_17))))
| ~ qtd0(s(s(qtd1)),f(suc(B_18)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_17))
| ~ qtd0(f(B_17),f(suc(B_17)))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_18),f(suc(B_18)))
| ~ qtd0(s(s(qtd1)),f(B_18))
| ~ iLEQ(suc(B_17),suc(B_18))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(B_18))))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17)))
| ~ qtd0(s(s(qtd1)),f(A_1)) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A_1,B_17,B_18] :
( ~ qtd0(s(s(qtd1)),f(suc(suc(B_17))))
| ~ qtd0(s(s(qtd1)),f(suc(B_18)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_17))
| ~ qtd0(f(B_17),f(suc(B_17)))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_18),f(suc(B_18)))
| ~ qtd0(s(s(qtd1)),f(B_18))
| ~ iLEQ(suc(B_17),suc(B_18))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(B_18))))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17)))
| ~ qtd0(s(s(qtd1)),f(A_1)) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X1))))
| ~ qtd0(s(s(qtd1)),f(suc(X2)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X2),f(suc(X2)))
| ~ qtd0(s(s(qtd1)),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X2))))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p148,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X1))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(suc(X1),suc(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X1))))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[c7]) ).
cnf(p1591,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(suc(X1),suc(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X1))))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p148]) ).
cnf(p7014,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p1591]) ).
cnf(p7024,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p7014]) ).
cnf(p7027,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p7024]) ).
cnf(p7030,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p7027]) ).
cnf(p7034,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p7030]) ).
cnf(p7041,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p7034]) ).
cnf(p7042,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p7041]) ).
cnf(f40,axiom,
( qtd2(f(B_28),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_28))))
| ~ qtd2(f(suc(suc(B_28))),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18) ).
fof(f40_nnf,plain,
! [B_28] :
( qtd2(f(B_28),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_28))))
| ~ qtd2(f(suc(suc(B_28))),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [B_28] :
( qtd2(f(B_28),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_28))))
| ~ qtd2(f(suc(suc(B_28))),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,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)],[f40_sk]) ).
cnf(f26,axiom,
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_16))
| ~ qtd2(f(B_16),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_261) ).
fof(f26_nnf,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_16))
| ~ qtd2(f(B_16),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_16))
| ~ qtd2(f(B_16),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,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)],[f26_sk]) ).
cnf(f10,axiom,
qtd2(f(A),s(s(s(qtd1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_421) ).
fof(f10_nnf,plain,
! [A] : qtd2(f(A),s(s(s(qtd1)))),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A] : qtd2(f(A),s(s(s(qtd1)))),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
qtd2(f(X0),s(s(s(qtd1)))),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p54,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[c26,c10]) ).
cnf(p72,plain,
( qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c40,p54]) ).
cnf(p7045,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p7042,p72]) ).
cnf(f3,axiom,
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_16)))
| ~ qtd2(f(suc(B_16)),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_183) ).
fof(f3_nnf,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_16)))
| ~ qtd2(f(suc(B_16)),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_16)))
| ~ qtd2(f(suc(B_16)),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,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)],[f3_sk]) ).
cnf(p90,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[c3,c10]) ).
cnf(p11072,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[status(thm)],[p7045,p90]) ).
cnf(f5,axiom,
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(B_16))))
| ~ qtd2(f(suc(suc(B_16))),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_217) ).
fof(f5_nnf,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(B_16))))
| ~ qtd2(f(suc(suc(B_16))),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(B_16))))
| ~ qtd2(f(suc(suc(B_16))),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p97,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c5,c10]) ).
cnf(p11075,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p11072,p97]) ).
cnf(p11076,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p11075]) ).
cnf(f4,axiom,
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_26) ).
fof(f4_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(A_1)) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(A_1)) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p95,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(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(s(qtd1)),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[c4,p72]) ).
cnf(p452,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(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)],[p95,p90]) ).
cnf(f23,axiom,
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(qtd1)),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_91) ).
fof(f23_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(qtd1)),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_1)))) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(qtd1)),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_1)))) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p178,plain,
( qtd2(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[c23,p97]) ).
cnf(p182,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p178,p90]) ).
cnf(p200,plain,
( qtd2(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p182]) ).
cnf(p453,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p452,p200]) ).
cnf(p812,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p453]) ).
cnf(p820,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p812]) ).
cnf(p821,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p820,p72]) ).
cnf(p822,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p821]) ).
cnf(p824,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p822]) ).
cnf(p11077,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p11076,p824]) ).
cnf(p11210,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p11077]) ).
cnf(p11211,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p11210]) ).
cnf(p11216,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p11211]) ).
cnf(f12,axiom,
( qtd0(f(B_18),f(suc(B_18)))
| qtd0(f(B_17),f(suc(B_17)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(B_18)))
| ~ iLEQ(suc(A_1),suc(B_17))
| ~ qtd0(s(s(qtd1)),f(B_18))
| ~ iLEQ(suc(B_17),suc(B_18))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17)))
| ~ qtd0(s(s(qtd1)),f(A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_311) ).
fof(f12_nnf,plain,
! [A_1,B_17,B_18] :
( qtd0(f(B_18),f(suc(B_18)))
| qtd0(f(B_17),f(suc(B_17)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(B_18)))
| ~ iLEQ(suc(A_1),suc(B_17))
| ~ qtd0(s(s(qtd1)),f(B_18))
| ~ iLEQ(suc(B_17),suc(B_18))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17)))
| ~ qtd0(s(s(qtd1)),f(A_1)) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A_1,B_17,B_18] :
( qtd0(f(B_18),f(suc(B_18)))
| qtd0(f(B_17),f(suc(B_17)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(suc(B_18)))
| ~ iLEQ(suc(A_1),suc(B_17))
| ~ qtd0(s(s(qtd1)),f(B_18))
| ~ iLEQ(suc(B_17),suc(B_18))
| ~ qtd0(s(s(qtd1)),f(suc(A_1)))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17)))
| ~ qtd0(s(s(qtd1)),f(A_1)) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( qtd0(f(X2),f(suc(X2)))
| qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(s(qtd1)),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p251,plain,
( qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[c12]) ).
cnf(p962,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p251]) ).
cnf(p965,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p962]) ).
cnf(p973,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p965]) ).
cnf(p977,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p973]) ).
cnf(p979,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p977]) ).
cnf(p980,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p979]) ).
cnf(p990,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p980,p72]) ).
cnf(p1200,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p990,p90]) ).
cnf(p1204,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p1200,p824]) ).
cnf(p1251,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p1204]) ).
cnf(p1252,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p1251]) ).
cnf(p1254,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p1252]) ).
cnf(p11217,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p11216,p1254]) ).
cnf(p11220,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p11217]) ).
cnf(p11221,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p11220]) ).
cnf(p11223,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p11221]) ).
cnf(p11224,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p11223,c40]) ).
cnf(p11225,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p11224]) ).
cnf(p11227,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p11225]) ).
cnf(f14,axiom,
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(qtd1),f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(suc(A_2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_37) ).
fof(f14_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(qtd1),f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(suc(A_2)))) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(qtd1),f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(suc(A_2)))) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,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)],[f14_sk]) ).
cnf(p11233,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p11227,c14]) ).
cnf(f35,axiom,
( qtd2(f(B_28),s(qtd1))
| qtd0(s(qtd1),f(suc(B_28)))
| ~ qtd2(f(suc(B_28)),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_138) ).
fof(f35_nnf,plain,
! [B_28] :
( qtd2(f(B_28),s(qtd1))
| qtd0(s(qtd1),f(suc(B_28)))
| ~ qtd2(f(suc(B_28)),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [B_28] :
( qtd2(f(B_28),s(qtd1))
| qtd0(s(qtd1),f(suc(B_28)))
| ~ qtd2(f(suc(B_28)),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p69,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p54,c35]) ).
cnf(p7044,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p7042,p69]) ).
cnf(p8426,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p7044,p90]) ).
cnf(p8427,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p8426,p97]) ).
cnf(p8428,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p8427]) ).
cnf(p94,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c4,p69]) ).
cnf(p342,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p94,p90]) ).
cnf(p356,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p342,p200]) ).
cnf(p569,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p356]) ).
cnf(p589,plain,
( ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p569]) ).
cnf(p590,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)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p589,p69]) ).
cnf(p593,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p590]) ).
cnf(p613,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p593]) ).
cnf(p614,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p613,c35]) ).
cnf(p616,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p614]) ).
cnf(p618,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p616]) ).
cnf(p8432,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)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p8428,p618]) ).
cnf(p8434,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8432]) ).
cnf(p8436,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8434]) ).
cnf(p989,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p980,p69]) ).
cnf(p1112,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p989,p90]) ).
cnf(p1123,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)))
| qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1112,p618]) ).
cnf(p1164,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1123]) ).
cnf(p1173,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1164]) ).
cnf(p8437,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| 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)],[p8436,p1173]) ).
cnf(p8444,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(factoring,[status(thm)],[p8437]) ).
cnf(p8445,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)],[p8444]) ).
cnf(p8447,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p8445]) ).
cnf(p8448,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)],[p8447,c35]) ).
cnf(p8453,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p8448]) ).
cnf(p8455,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p8453]) ).
cnf(p11430,plain,
( qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p11233,p8455]) ).
cnf(p11432,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p11430]) ).
cnf(f9,axiom,
( qtd2(f(B_28),s(qtd1))
| qtd0(s(qtd1),f(B_28))
| ~ qtd2(f(B_28),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_326) ).
fof(f9_nnf,plain,
! [B_28] :
( qtd2(f(B_28),s(qtd1))
| qtd0(s(qtd1),f(B_28))
| ~ qtd2(f(B_28),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [B_28] :
( qtd2(f(B_28),s(qtd1))
| qtd0(s(qtd1),f(B_28))
| ~ qtd2(f(B_28),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd2(f(X0),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p68,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p54,c9]) ).
cnf(p7043,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p7042,p68]) ).
cnf(p7051,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p7043,p90]) ).
cnf(p7062,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p7051,p97]) ).
cnf(p7063,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p7062]) ).
cnf(p93,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[c4,p68]) ).
cnf(p127,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p93,p90]) ).
cnf(p129,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))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p127,c9]) ).
cnf(p207,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p129]) ).
cnf(p240,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p207]) ).
cnf(p241,plain,
( qtd2(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p240,p200]) ).
cnf(p268,plain,
( qtd2(f(X0),s(s(qtd1)))
| ~ qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p241]) ).
cnf(p269,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))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p268,p68]) ).
cnf(p274,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p269]) ).
cnf(p276,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p274]) ).
cnf(p308,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)],[p276,c9]) ).
cnf(p311,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)],[p308]) ).
cnf(p313,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p311]) ).
cnf(p7064,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))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p7063,p313]) ).
cnf(p7090,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p7064]) ).
cnf(p7097,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p7090]) ).
cnf(p988,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p980,p68]) ).
cnf(p996,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p988,p90]) ).
cnf(p998,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))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p996,p313]) ).
cnf(p1095,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p998]) ).
cnf(p1097,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1095]) ).
cnf(p1098,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1097,c9]) ).
cnf(p1107,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1098]) ).
cnf(p1109,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1107]) ).
cnf(p7106,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)],[p7097,p1109]) ).
cnf(p7126,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)],[p7106]) ).
cnf(p7128,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p7126]) ).
cnf(p7134,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)],[p7128,c9]) ).
cnf(p7137,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p7134]) ).
cnf(p7139,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p7137]) ).
cnf(f22,axiom,
( qtd2(f(B_35),qtd1)
| qtd0(qtd1,f(suc(suc(B_35))))
| ~ qtd2(f(suc(suc(B_35))),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_72) ).
fof(f22_nnf,plain,
! [B_35] :
( qtd2(f(B_35),qtd1)
| qtd0(qtd1,f(suc(suc(B_35))))
| ~ qtd2(f(suc(suc(B_35))),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [B_35] :
( qtd2(f(B_35),qtd1)
| qtd0(qtd1,f(suc(suc(B_35))))
| ~ qtd2(f(suc(suc(B_35))),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p7142,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p7139,c22]) ).
cnf(f20,axiom,
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(A_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_60) ).
fof(f20_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(A_2)) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(A_2)) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,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)],[f20_sk]) ).
cnf(p7577,plain,
( 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)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p7142,c20]) ).
cnf(p8630,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8455,p7577]) ).
cnf(p11435,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| 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)) ),
inference(resolution,[status(thm)],[p11432,p8630]) ).
cnf(p13250,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| 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)) ),
inference(factoring,[status(thm)],[p11435]) ).
cnf(p13251,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13250]) ).
cnf(p13252,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p13251,p7142]) ).
cnf(p13256,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13252]) ).
cnf(p13258,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13256]) ).
cnf(f11,axiom,
( ~ qtd0(s(qtd1),f(suc(suc(B_30))))
| ~ qtd0(s(qtd1),f(A_2))
| ~ qtd0(f(B_30),f(suc(B_30)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(suc(A_2))))
| ~ qtd0(s(qtd1),f(suc(B_29)))
| ~ qtd0(s(qtd1),f(suc(suc(B_29))))
| ~ qtd0(f(B_29),f(suc(B_29)))
| ~ iLEQ(suc(B_29),suc(B_30))
| ~ qtd0(s(qtd1),f(B_29))
| ~ iLEQ(suc(A_2),suc(B_29))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(B_30)))
| ~ qtd0(s(qtd1),f(B_30)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_219) ).
fof(f11_nnf,plain,
! [B_30,A_2,B_29] :
( ~ qtd0(s(qtd1),f(suc(suc(B_30))))
| ~ qtd0(s(qtd1),f(A_2))
| ~ qtd0(f(B_30),f(suc(B_30)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(suc(A_2))))
| ~ qtd0(s(qtd1),f(suc(B_29)))
| ~ qtd0(s(qtd1),f(suc(suc(B_29))))
| ~ qtd0(f(B_29),f(suc(B_29)))
| ~ iLEQ(suc(B_29),suc(B_30))
| ~ qtd0(s(qtd1),f(B_29))
| ~ iLEQ(suc(A_2),suc(B_29))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(B_30)))
| ~ qtd0(s(qtd1),f(B_30)) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [B_30,A_2,B_29] :
( ~ qtd0(s(qtd1),f(suc(suc(B_30))))
| ~ qtd0(s(qtd1),f(A_2))
| ~ qtd0(f(B_30),f(suc(B_30)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(suc(A_2))))
| ~ qtd0(s(qtd1),f(suc(B_29)))
| ~ qtd0(s(qtd1),f(suc(suc(B_29))))
| ~ qtd0(f(B_29),f(suc(B_29)))
| ~ iLEQ(suc(B_29),suc(B_30))
| ~ qtd0(s(qtd1),f(B_29))
| ~ iLEQ(suc(A_2),suc(B_29))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(B_30)))
| ~ qtd0(s(qtd1),f(B_30)) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(suc(X1))))
| ~ qtd0(s(qtd1),f(suc(X2)))
| ~ qtd0(s(qtd1),f(suc(suc(X2))))
| ~ qtd0(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(s(qtd1),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p223,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(suc(X1))))
| ~ qtd0(s(qtd1),f(suc(suc(X1))))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(qtd1),f(X1))
| ~ iLEQ(suc(X1),suc(X1))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[c11]) ).
cnf(p2025,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(suc(X1))))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(qtd1),f(X1))
| ~ iLEQ(suc(X1),suc(X1))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p223]) ).
cnf(p5309,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p2025]) ).
cnf(p5311,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p5309]) ).
cnf(p5316,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p5311]) ).
cnf(p5319,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p5316]) ).
cnf(p5320,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p5319]) ).
cnf(p5322,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p5320]) ).
cnf(p5333,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p5322]) ).
cnf(p7715,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p7142,p5333]) ).
cnf(p9916,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p7715,p8455]) ).
cnf(p13260,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p13258,p9916]) ).
cnf(p13451,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13260]) ).
cnf(p13454,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13451]) ).
cnf(p13458,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13454]) ).
cnf(f28,axiom,
( qtd0(f(B_30),f(suc(B_30)))
| qtd0(f(B_29),f(suc(B_29)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(A_2))
| ~ qtd0(s(qtd1),f(suc(B_29)))
| ~ iLEQ(suc(B_29),suc(B_30))
| ~ qtd0(s(qtd1),f(B_29))
| ~ iLEQ(suc(A_2),suc(B_29))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(B_30)))
| ~ qtd0(s(qtd1),f(B_30)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_340) ).
fof(f28_nnf,plain,
! [B_30,A_2,B_29] :
( qtd0(f(B_30),f(suc(B_30)))
| qtd0(f(B_29),f(suc(B_29)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(A_2))
| ~ qtd0(s(qtd1),f(suc(B_29)))
| ~ iLEQ(suc(B_29),suc(B_30))
| ~ qtd0(s(qtd1),f(B_29))
| ~ iLEQ(suc(A_2),suc(B_29))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(B_30)))
| ~ qtd0(s(qtd1),f(B_30)) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [B_30,A_2,B_29] :
( qtd0(f(B_30),f(suc(B_30)))
| qtd0(f(B_29),f(suc(B_29)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(A_2))
| ~ qtd0(s(qtd1),f(suc(B_29)))
| ~ iLEQ(suc(B_29),suc(B_30))
| ~ qtd0(s(qtd1),f(B_29))
| ~ iLEQ(suc(A_2),suc(B_29))
| ~ qtd0(s(qtd1),f(suc(A_2)))
| ~ qtd0(s(qtd1),f(suc(B_30)))
| ~ qtd0(s(qtd1),f(B_30)) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X2),f(suc(X2)))
| qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(s(qtd1),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p488,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(qtd1),f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[c28]) ).
cnf(p860,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(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(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p488]) ).
cnf(p866,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(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(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p860]) ).
cnf(p869,plain,
( qtd0(f(X0),f(suc(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(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p866]) ).
cnf(p870,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p869]) ).
cnf(p881,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p870]) ).
cnf(p883,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p881]) ).
cnf(p7596,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p7142,p883]) ).
cnf(p8631,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8455,p7596]) ).
cnf(p13259,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| 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))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p13258,p8631]) ).
cnf(p13261,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13259]) ).
cnf(p13265,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13261]) ).
cnf(p13267,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13265]) ).
cnf(p13459,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p13458,p13267]) ).
cnf(p13460,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13459]) ).
cnf(p13463,plain,
( qtd2(f(X0),qtd1)
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13460]) ).
cnf(p13466,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13463]) ).
cnf(p13467,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)) ),
inference(resolution,[status(thm)],[p13466,p11227]) ).
cnf(p13468,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p13467]) ).
cnf(p13469,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)],[p13468,c22]) ).
cnf(p13473,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p13469]) ).
cnf(p13475,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p13473]) ).
cnf(f27,axiom,
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(qtd1,f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(suc(A_3)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_116) ).
fof(f27_nnf,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(qtd1,f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(suc(A_3)))) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(qtd1,f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(suc(A_3)))) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,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)],[f27_sk]) ).
cnf(p13477,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)],[p13475,c27]) ).
cnf(f29,axiom,
( qtd2(f(B_35),qtd1)
| qtd0(qtd1,f(suc(B_35)))
| ~ qtd2(f(suc(B_35)),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_353) ).
fof(f29_nnf,plain,
! [B_35] :
( qtd2(f(B_35),qtd1)
| qtd0(qtd1,f(suc(B_35)))
| ~ qtd2(f(suc(B_35)),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [B_35] :
( qtd2(f(B_35),qtd1)
| qtd0(qtd1,f(suc(B_35)))
| ~ qtd2(f(suc(B_35)),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p7141,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p7139,c29]) ).
cnf(p7372,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p7141,c20]) ).
cnf(p8624,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p8455,p7372]) ).
cnf(p11434,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| 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)) ),
inference(resolution,[status(thm)],[p11432,p8624]) ).
cnf(p12194,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| 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)) ),
inference(factoring,[status(thm)],[p11434]) ).
cnf(p12195,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p12194]) ).
cnf(p12196,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p12195,p7141]) ).
cnf(p12198,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p12196]) ).
cnf(p12202,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p12198]) ).
cnf(p7524,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ 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)],[p7141,p5333]) ).
cnf(p8636,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ 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)],[p8455,p7524]) ).
cnf(p12205,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p12202,p8636]) ).
cnf(p12694,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| 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)],[p12205]) ).
cnf(p12701,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p12694]) ).
cnf(p12703,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p12701]) ).
cnf(p7393,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ 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)],[p7141,p883]) ).
cnf(p8625,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ 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)],[p8455,p7393]) ).
cnf(p12203,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p12202,p8625]) ).
cnf(p12207,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| 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)],[p12203]) ).
cnf(p12210,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p12207]) ).
cnf(p12216,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p12210]) ).
cnf(p12705,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p12703,p12216]) ).
cnf(p12706,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p12705]) ).
cnf(p12710,plain,
( qtd2(f(X0),qtd1)
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p12706]) ).
cnf(p12712,plain,
( ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p12710]) ).
cnf(p12713,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p12712,p11227]) ).
cnf(p12714,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p12713]) ).
cnf(p12717,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p12714,c29]) ).
cnf(p12719,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p12717]) ).
cnf(p12721,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p12719]) ).
cnf(p13726,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)],[p13477,p12721]) ).
cnf(p13728,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p13726]) ).
cnf(f39,axiom,
( qtd2(f(B_35),qtd1)
| qtd0(qtd1,f(B_35))
| ~ qtd2(f(B_35),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_307) ).
fof(f39_nnf,plain,
! [B_35] :
( qtd2(f(B_35),qtd1)
| qtd0(qtd1,f(B_35))
| ~ qtd2(f(B_35),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [B_35] :
( qtd2(f(B_35),qtd1)
| qtd0(qtd1,f(B_35))
| ~ qtd2(f(B_35),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd2(f(X0),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p7140,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p7139,c39]) ).
cnf(p7148,plain,
( iLEQ(suc(X0),suc(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)],[p7140,c20]) ).
cnf(p8622,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p8455,p7148]) ).
cnf(p11433,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p11432,p8622]) ).
cnf(p11611,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p11433]) ).
cnf(p11613,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p11611]) ).
cnf(p11614,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p11613,p7140]) ).
cnf(p11618,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p11614]) ).
cnf(p11620,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p11618]) ).
cnf(p11621,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)],[p11620,c39]) ).
cnf(p11631,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p11621]) ).
cnf(p11633,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p11631]) ).
cnf(p7314,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p7140,p5333]) ).
cnf(p8626,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p8455,p7314]) ).
cnf(p11637,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| 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)],[p11633,p8626]) ).
cnf(p11655,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p11637]) ).
cnf(p11659,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p11655]) ).
cnf(p7170,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p7140,p883]) ).
cnf(p8623,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p8455,p7170]) ).
cnf(p11635,plain,
( qtd0(f(X0),f(suc(X0)))
| 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)],[p11633,p8623]) ).
cnf(p11642,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p11635]) ).
cnf(p11644,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p11642]) ).
cnf(p11663,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p11659,p11644]) ).
cnf(p11667,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p11663]) ).
cnf(p11668,plain,
( qtd2(f(X0),qtd1)
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p11667]) ).
cnf(p11670,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p11668]) ).
cnf(p11671,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p11670,p11227]) ).
cnf(p11672,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p11671]) ).
cnf(p11673,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p11672,c39]) ).
cnf(p11676,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p11673]) ).
cnf(p11678,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p11676]) ).
cnf(f33,axiom,
~ qtd2(f(z),qtd1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_211) ).
fof(f33_nnf,plain,
~ qtd2(f(z),qtd1),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
~ qtd2(f(z),qtd1),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
~ qtd2(f(z),qtd1),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p11679,plain,
qtd0(qtd1,f(z)),
inference(resolution,[status(thm)],[p11678,c33]) ).
cnf(f15,axiom,
( iLEQ(suc(A_3),suc(A_3))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(qtd1,f(A_3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_86) ).
fof(f15_nnf,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(qtd1,f(A_3)) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(qtd1,f(A_3)) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,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)],[f15_sk]) ).
cnf(p11680,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p11679,c15]) ).
cnf(p12893,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p12721,p11680]) ).
cnf(p13732,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)],[p13728,p12893]) ).
cnf(p13735,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p13732]) ).
cnf(p13736,plain,
( iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p13735]) ).
cnf(p13737,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p13736,p11679]) ).
cnf(f8,axiom,
( qtd0(f(B_37),f(suc(B_37)))
| qtd0(f(B_36),f(suc(B_36)))
| qtd0(f(A_3),f(suc(A_3)))
| ~ iLEQ(suc(B_36),suc(B_37))
| ~ iLEQ(suc(A_3),suc(B_36))
| ~ qtd0(qtd1,f(B_37))
| ~ qtd0(qtd1,f(suc(B_37)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(qtd1,f(A_3))
| ~ qtd0(qtd1,f(suc(B_36)))
| ~ qtd0(qtd1,f(B_36)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16) ).
fof(f8_nnf,plain,
! [B_36,A_3,B_37] :
( qtd0(f(B_37),f(suc(B_37)))
| qtd0(f(B_36),f(suc(B_36)))
| qtd0(f(A_3),f(suc(A_3)))
| ~ iLEQ(suc(B_36),suc(B_37))
| ~ iLEQ(suc(A_3),suc(B_36))
| ~ qtd0(qtd1,f(B_37))
| ~ qtd0(qtd1,f(suc(B_37)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(qtd1,f(A_3))
| ~ qtd0(qtd1,f(suc(B_36)))
| ~ qtd0(qtd1,f(B_36)) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [B_36,A_3,B_37] :
( qtd0(f(B_37),f(suc(B_37)))
| qtd0(f(B_36),f(suc(B_36)))
| qtd0(f(A_3),f(suc(A_3)))
| ~ iLEQ(suc(B_36),suc(B_37))
| ~ iLEQ(suc(A_3),suc(B_36))
| ~ qtd0(qtd1,f(B_37))
| ~ qtd0(qtd1,f(suc(B_37)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(qtd1,f(A_3))
| ~ qtd0(qtd1,f(suc(B_36)))
| ~ qtd0(qtd1,f(B_36)) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( qtd0(f(X2),f(suc(X2)))
| qtd0(f(X0),f(suc(X0)))
| qtd0(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(qtd1,f(X2))
| ~ qtd0(qtd1,f(suc(X2)))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p197,plain,
( qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[c8]) ).
cnf(p782,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p197]) ).
cnf(p784,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p782]) ).
cnf(p787,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p784]) ).
cnf(p790,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p787]) ).
cnf(p796,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p790]) ).
cnf(p797,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p796]) ).
cnf(p11689,plain,
( qtd0(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p11679,p797]) ).
cnf(p12894,plain,
( qtd0(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p12721,p11689]) ).
cnf(p13741,plain,
( qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p13737,p12894]) ).
cnf(p13742,plain,
( qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p13741]) ).
cnf(f13,axiom,
( ~ iLEQ(suc(B_36),suc(B_37))
| ~ iLEQ(suc(A_3),suc(B_36))
| ~ qtd0(f(B_37),f(suc(B_37)))
| ~ qtd0(qtd1,f(B_37))
| ~ qtd0(qtd1,f(suc(B_37)))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(f(B_36),f(suc(B_36)))
| ~ qtd0(qtd1,f(suc(suc(A_3))))
| ~ qtd0(qtd1,f(A_3))
| ~ qtd0(qtd1,f(suc(B_36)))
| ~ qtd0(qtd1,f(suc(suc(B_37))))
| ~ qtd0(qtd1,f(suc(suc(B_36))))
| ~ qtd0(qtd1,f(B_36)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_83) ).
fof(f13_nnf,plain,
! [B_36,B_37,A_3] :
( ~ iLEQ(suc(B_36),suc(B_37))
| ~ iLEQ(suc(A_3),suc(B_36))
| ~ qtd0(f(B_37),f(suc(B_37)))
| ~ qtd0(qtd1,f(B_37))
| ~ qtd0(qtd1,f(suc(B_37)))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(f(B_36),f(suc(B_36)))
| ~ qtd0(qtd1,f(suc(suc(A_3))))
| ~ qtd0(qtd1,f(A_3))
| ~ qtd0(qtd1,f(suc(B_36)))
| ~ qtd0(qtd1,f(suc(suc(B_37))))
| ~ qtd0(qtd1,f(suc(suc(B_36))))
| ~ qtd0(qtd1,f(B_36)) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [B_36,B_37,A_3] :
( ~ iLEQ(suc(B_36),suc(B_37))
| ~ iLEQ(suc(A_3),suc(B_36))
| ~ qtd0(f(B_37),f(suc(B_37)))
| ~ qtd0(qtd1,f(B_37))
| ~ qtd0(qtd1,f(suc(B_37)))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(qtd1,f(suc(A_3)))
| ~ qtd0(f(B_36),f(suc(B_36)))
| ~ qtd0(qtd1,f(suc(suc(A_3))))
| ~ qtd0(qtd1,f(A_3))
| ~ qtd0(qtd1,f(suc(B_36)))
| ~ qtd0(qtd1,f(suc(suc(B_37))))
| ~ qtd0(qtd1,f(suc(suc(B_36))))
| ~ qtd0(qtd1,f(B_36)) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(f(X2),f(suc(X2)))
| ~ qtd0(qtd1,f(suc(X2)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X2))))
| ~ qtd0(qtd1,f(X2))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X1))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0)) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p278,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X1))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[c13]) ).
cnf(p2261,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X1))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p278]) ).
cnf(p2269,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2261]) ).
cnf(p2278,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2269]) ).
cnf(p2282,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2278]) ).
cnf(p2285,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2282]) ).
cnf(p2301,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ 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))))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2285]) ).
cnf(p2304,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))))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2301]) ).
cnf(p2305,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2304]) ).
cnf(p11719,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(z)))) ),
inference(resolution,[status(thm)],[p11679,p2305]) ).
cnf(p13647,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p13475,p11719]) ).
cnf(p13716,plain,
( qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p13647,p12721]) ).
cnf(p13719,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p13716]) ).
cnf(p13751,plain,
( ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p13742,p13719]) ).
cnf(p13752,plain,
( ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p13751]) ).
cnf(p13756,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p13752,p13737]) ).
cnf(p13757,plain,
qtd2(f(z),qtd1),
inference(factoring,[status(thm)],[p13756]) ).
cnf(p13758,plain,
$false,
inference(resolution,[status(thm)],[p13757,c33]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO671-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 03:21:45 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 23.76/63.30 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.76/63.30 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------