%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYO681-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 : n020.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:39 PM UTC 2026
% Result : Unsatisfiable 22.14s 22.71s
% Output : Proof 22.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 80
% Number of leaves : 30
% Syntax : Number of formulae : 299 ( 13 unt; 0 def)
% Number of atoms : 1597 ( 0 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 2391 (1093 ~;1298 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 366 ( 6 sgn 90 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f37,axiom,
( ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_25)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(B_25))))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_24)))
| ~ qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(f(B_25),f(suc(B_25)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(A_1))))
| ~ qtd2(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_24))
| ~ qtd2(s(s(s(qtd1))),f(B_24))
| ~ qtd2(f(B_24),f(suc(B_24)))
| ~ qtd2(s(s(s(qtd1))),f(B_25))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(B_24))))
| ~ iLEQ(suc(B_24),suc(B_25)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_131) ).
fof(f37_nnf,plain,
! [B_24,B_25,A_1] :
( ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_25)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(B_25))))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_24)))
| ~ qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(f(B_25),f(suc(B_25)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(A_1))))
| ~ qtd2(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_24))
| ~ qtd2(s(s(s(qtd1))),f(B_24))
| ~ qtd2(f(B_24),f(suc(B_24)))
| ~ qtd2(s(s(s(qtd1))),f(B_25))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(B_24))))
| ~ iLEQ(suc(B_24),suc(B_25)) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [B_24,B_25,A_1] :
( ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_25)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(B_25))))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_24)))
| ~ qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(f(B_25),f(suc(B_25)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(A_1))))
| ~ qtd2(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_24))
| ~ qtd2(s(s(s(qtd1))),f(B_24))
| ~ qtd2(f(B_24),f(suc(B_24)))
| ~ qtd2(s(s(s(qtd1))),f(B_25))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(B_24))))
| ~ iLEQ(suc(B_24),suc(B_25)) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
( ~ qtd2(s(s(s(qtd1))),f(suc(X2)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X1))))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X2),f(suc(X2)))
| ~ qtd2(f(X1),f(suc(X1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X2))))
| ~ qtd2(s(s(s(qtd1))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X1))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p614,plain,
( ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X1))))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(f(X1),f(suc(X1)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X1))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(factoring,[status(thm)],[c37]) ).
cnf(p3682,plain,
( ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p614]) ).
cnf(p5871,plain,
( ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p3682]) ).
cnf(p5875,plain,
( ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p5871]) ).
cnf(p5877,plain,
( ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p5875]) ).
cnf(p5880,plain,
( ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p5877]) ).
cnf(p5893,plain,
( ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p5880]) ).
cnf(p5895,plain,
( ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p5893]) ).
cnf(p5896,plain,
( ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p5895]) ).
cnf(f35,axiom,
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd2(s(s(s(qtd1))),f(A_1))
| ~ qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_663) ).
fof(f35_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd2(s(s(s(qtd1))),f(A_1))
| ~ qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(A_1)))) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd2(s(s(s(qtd1))),f(A_1))
| ~ qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(A_1)))) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(f27,axiom,
( qtd0(f(B_23),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(suc(suc(B_23))))
| ~ qtd0(f(suc(suc(B_23))),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_103) ).
fof(f27_nnf,plain,
! [B_23] :
( qtd0(f(B_23),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(suc(suc(B_23))))
| ~ qtd0(f(suc(suc(B_23))),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [B_23] :
( qtd0(f(B_23),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(suc(suc(B_23))))
| ~ qtd0(f(suc(suc(B_23))),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(f2,axiom,
qtd0(f(A),s(s(s(s(qtd1))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_556) ).
fof(f2_nnf,plain,
! [A] : qtd0(f(A),s(s(s(s(qtd1))))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A] : qtd0(f(A),s(s(s(s(qtd1))))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
qtd0(f(X0),s(s(s(s(qtd1))))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p95,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c27,c2]) ).
cnf(p142,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c35,p95]) ).
cnf(f42,axiom,
( qtd0(f(B_23),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(suc(B_23)))
| ~ qtd0(f(suc(B_23)),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_550) ).
fof(f42_nnf,plain,
! [B_23] :
( qtd0(f(B_23),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(suc(B_23)))
| ~ qtd0(f(suc(B_23)),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [B_23] :
( qtd0(f(B_23),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(suc(B_23)))
| ~ qtd0(f(suc(B_23)),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(f(suc(X0)),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p81,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c42,c2]) ).
cnf(p162,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p142,p81]) ).
cnf(p164,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p162]) ).
cnf(f31,axiom,
( iLEQ(suc(A_1),suc(A_1))
| qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_283) ).
fof(f31_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(A_1)) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(A_1)) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(f0,axiom,
( qtd0(f(B_23),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(B_23))
| ~ qtd0(f(B_23),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_658) ).
fof(f0_nnf,plain,
! [B_23] :
( qtd0(f(B_23),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(B_23))
| ~ qtd0(f(B_23),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [B_23] :
( qtd0(f(B_23),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(B_23))
| ~ qtd0(f(B_23),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p54,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd2(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[c0,c2]) ).
cnf(p96,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c31,p54]) ).
cnf(p113,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p96,p81]) ).
cnf(p115,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p113]) ).
cnf(p165,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p164,p115]) ).
cnf(p171,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p165]) ).
cnf(p186,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p171]) ).
cnf(p187,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p186,p54]) ).
cnf(p190,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p187]) ).
cnf(p5897,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p5896,p190]) ).
cnf(p5922,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),s(s(s(qtd1))))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p5897,p95]) ).
cnf(p5923,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p5922]) ).
cnf(p5924,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),s(s(s(qtd1))))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p5923,p54]) ).
cnf(p5927,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p5924]) ).
cnf(f13,axiom,
( qtd2(f(B_25),f(suc(B_25)))
| qtd2(f(B_24),f(suc(B_24)))
| qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_25)))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_24)))
| ~ qtd2(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_24))
| ~ qtd2(s(s(s(qtd1))),f(B_24))
| ~ qtd2(s(s(s(qtd1))),f(B_25))
| ~ iLEQ(suc(B_24),suc(B_25)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_486) ).
fof(f13_nnf,plain,
! [B_24,B_25,A_1] :
( qtd2(f(B_25),f(suc(B_25)))
| qtd2(f(B_24),f(suc(B_24)))
| qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_25)))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_24)))
| ~ qtd2(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_24))
| ~ qtd2(s(s(s(qtd1))),f(B_24))
| ~ qtd2(s(s(s(qtd1))),f(B_25))
| ~ iLEQ(suc(B_24),suc(B_25)) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [B_24,B_25,A_1] :
( qtd2(f(B_25),f(suc(B_25)))
| qtd2(f(B_24),f(suc(B_24)))
| qtd2(f(A_1),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_25)))
| ~ qtd2(s(s(s(qtd1))),f(suc(B_24)))
| ~ qtd2(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_24))
| ~ qtd2(s(s(s(qtd1))),f(B_24))
| ~ qtd2(s(s(s(qtd1))),f(B_25))
| ~ iLEQ(suc(B_24),suc(B_25)) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( qtd2(f(X1),f(suc(X1)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X2),f(suc(X2)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X2)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(X1))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p230,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X1),f(suc(X1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X1)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c13]) ).
cnf(p1421,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p230]) ).
cnf(p1425,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p1421]) ).
cnf(p1428,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p1425]) ).
cnf(p1436,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p1428]) ).
cnf(p1438,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p1436]) ).
cnf(p1439,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p1438]) ).
cnf(p1440,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p1439,p190]) ).
cnf(p1458,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1440,p54]) ).
cnf(p1461,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1458]) ).
cnf(p1463,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1461,p81]) ).
cnf(p1465,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1463]) ).
cnf(p5939,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),s(s(s(qtd1))))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p5927,p1465]) ).
cnf(p5954,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| ~ qtd2(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p5939]) ).
cnf(p5956,plain,
( qtd0(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p5954,p81]) ).
cnf(p5957,plain,
qtd0(f(X0),s(s(s(qtd1)))),
inference(factoring,[status(thm)],[p5956]) ).
cnf(f33,axiom,
( qtd0(f(B_41),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(suc(B_41)))
| ~ qtd0(f(suc(B_41)),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_457) ).
fof(f33_nnf,plain,
! [B_41] :
( qtd0(f(B_41),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(suc(B_41)))
| ~ qtd0(f(suc(B_41)),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [B_41] :
( qtd0(f(B_41),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(suc(B_41)))
| ~ qtd0(f(suc(B_41)),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( qtd0(f(X0),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(f(suc(X0)),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p5959,plain,
( qtd0(f(X0),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p5957,c33]) ).
cnf(f15,axiom,
( ~ qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(A_2))
| ~ qtd2(f(B_42),f(suc(B_42)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(A_2))))
| ~ qtd2(s(s(qtd1)),f(B_43))
| ~ iLEQ(suc(A_2),suc(B_42))
| ~ qtd2(s(s(qtd1)),f(suc(B_43)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(B_43))))
| ~ qtd2(s(s(qtd1)),f(suc(suc(B_42))))
| ~ iLEQ(suc(B_42),suc(B_43))
| ~ qtd2(s(s(qtd1)),f(B_42))
| ~ qtd2(f(B_43),f(suc(B_43)))
| ~ qtd2(s(s(qtd1)),f(suc(B_42))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_528) ).
fof(f15_nnf,plain,
! [B_42,B_43,A_2] :
( ~ qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(A_2))
| ~ qtd2(f(B_42),f(suc(B_42)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(A_2))))
| ~ qtd2(s(s(qtd1)),f(B_43))
| ~ iLEQ(suc(A_2),suc(B_42))
| ~ qtd2(s(s(qtd1)),f(suc(B_43)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(B_43))))
| ~ qtd2(s(s(qtd1)),f(suc(suc(B_42))))
| ~ iLEQ(suc(B_42),suc(B_43))
| ~ qtd2(s(s(qtd1)),f(B_42))
| ~ qtd2(f(B_43),f(suc(B_43)))
| ~ qtd2(s(s(qtd1)),f(suc(B_42))) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [B_42,B_43,A_2] :
( ~ qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(A_2))
| ~ qtd2(f(B_42),f(suc(B_42)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(A_2))))
| ~ qtd2(s(s(qtd1)),f(B_43))
| ~ iLEQ(suc(A_2),suc(B_42))
| ~ qtd2(s(s(qtd1)),f(suc(B_43)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(B_43))))
| ~ qtd2(s(s(qtd1)),f(suc(suc(B_42))))
| ~ iLEQ(suc(B_42),suc(B_43))
| ~ qtd2(s(s(qtd1)),f(B_42))
| ~ qtd2(f(B_43),f(suc(B_43)))
| ~ qtd2(s(s(qtd1)),f(suc(B_42))) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( ~ qtd2(f(X2),f(suc(X2)))
| ~ qtd2(s(s(qtd1)),f(X2))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X2))))
| ~ qtd2(s(s(qtd1)),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X1)))
| ~ qtd2(s(s(qtd1)),f(suc(X2)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X1))))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X1),f(suc(X1)))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p272,plain,
( ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd2(s(s(qtd1)),f(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X1)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X1))))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X1),f(suc(X1)))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[c15]) ).
cnf(p1874,plain,
( ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X1)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X1))))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X1),f(suc(X1)))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p272]) ).
cnf(p4503,plain,
( ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1874]) ).
cnf(p4515,plain,
( ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p4503]) ).
cnf(p4519,plain,
( ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p4515]) ).
cnf(p4522,plain,
( ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p4519]) ).
cnf(p4525,plain,
( ~ qtd2(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p4522]) ).
cnf(p4537,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p4525]) ).
cnf(p4539,plain,
( ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p4537]) ).
cnf(p6220,plain,
( ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p5959,p4539]) ).
cnf(f9,axiom,
( qtd0(f(B_41),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(suc(suc(B_41))))
| ~ qtd0(f(suc(suc(B_41))),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_607) ).
fof(f9_nnf,plain,
! [B_41] :
( qtd0(f(B_41),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(suc(suc(B_41))))
| ~ qtd0(f(suc(suc(B_41))),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [B_41] :
( qtd0(f(B_41),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(suc(suc(B_41))))
| ~ qtd0(f(suc(suc(B_41))),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( qtd0(f(X0),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p5960,plain,
( qtd0(f(X0),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p5957,c9]) ).
cnf(f7,axiom,
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd2(s(s(qtd1)),f(A_2))
| ~ qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(A_2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_415) ).
fof(f7_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd2(s(s(qtd1)),f(A_2))
| ~ qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(A_2)))) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd2(s(s(qtd1)),f(A_2))
| ~ qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(A_2)))) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p6267,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0)))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p5960,c7]) ).
cnf(p6483,plain,
( qtd0(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p6267,p5959]) ).
cnf(p6485,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p6483]) ).
cnf(f6,axiom,
( qtd0(f(B_41),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(B_41))
| ~ qtd0(f(B_41),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_300) ).
fof(f6_nnf,plain,
! [B_41] :
( qtd0(f(B_41),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(B_41))
| ~ qtd0(f(B_41),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [B_41] :
( qtd0(f(B_41),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(B_41))
| ~ qtd0(f(B_41),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( qtd0(f(X0),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p191,plain,
( qtd0(f(X0),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p190,c6]) ).
cnf(f45,axiom,
( iLEQ(suc(A_2),suc(A_2))
| qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(A_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_383) ).
fof(f45_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(A_2)) ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(A_2)) ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p213,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0)))
| qtd0(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p191,c45]) ).
cnf(p219,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(suc(X0)))
| qtd0(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p213]) ).
cnf(p6097,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p5959,p219]) ).
cnf(p6438,plain,
( qtd2(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p6097]) ).
cnf(p6486,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p6485,p6438]) ).
cnf(p6488,plain,
( iLEQ(suc(X0),suc(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p6486]) ).
cnf(p6497,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p6488]) ).
cnf(p5958,plain,
( qtd0(f(X0),s(s(qtd1)))
| qtd2(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p5957,c6]) ).
cnf(p6498,plain,
( qtd0(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p6497,p5958]) ).
cnf(p6501,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p6498]) ).
cnf(f18,axiom,
( qtd2(f(B_43),f(suc(B_43)))
| qtd2(f(B_42),f(suc(B_42)))
| qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(A_2))
| ~ qtd2(s(s(qtd1)),f(B_43))
| ~ iLEQ(suc(A_2),suc(B_42))
| ~ qtd2(s(s(qtd1)),f(suc(B_43)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ iLEQ(suc(B_42),suc(B_43))
| ~ qtd2(s(s(qtd1)),f(B_42))
| ~ qtd2(s(s(qtd1)),f(suc(B_42))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_463) ).
fof(f18_nnf,plain,
! [B_42,B_43,A_2] :
( qtd2(f(B_43),f(suc(B_43)))
| qtd2(f(B_42),f(suc(B_42)))
| qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(A_2))
| ~ qtd2(s(s(qtd1)),f(B_43))
| ~ iLEQ(suc(A_2),suc(B_42))
| ~ qtd2(s(s(qtd1)),f(suc(B_43)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ iLEQ(suc(B_42),suc(B_43))
| ~ qtd2(s(s(qtd1)),f(B_42))
| ~ qtd2(s(s(qtd1)),f(suc(B_42))) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [B_42,B_43,A_2] :
( qtd2(f(B_43),f(suc(B_43)))
| qtd2(f(B_42),f(suc(B_42)))
| qtd2(f(A_2),f(suc(A_2)))
| ~ qtd2(s(s(qtd1)),f(A_2))
| ~ qtd2(s(s(qtd1)),f(B_43))
| ~ iLEQ(suc(A_2),suc(B_42))
| ~ qtd2(s(s(qtd1)),f(suc(B_43)))
| ~ qtd2(s(s(qtd1)),f(suc(A_2)))
| ~ iLEQ(suc(B_42),suc(B_43))
| ~ qtd2(s(s(qtd1)),f(B_42))
| ~ qtd2(s(s(qtd1)),f(suc(B_42))) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( qtd2(f(X1),f(suc(X1)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X2),f(suc(X2)))
| ~ qtd2(s(s(qtd1)),f(X2))
| ~ qtd2(s(s(qtd1)),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X1)))
| ~ qtd2(s(s(qtd1)),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p313,plain,
( qtd2(f(X1),f(suc(X1)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[c18]) ).
cnf(p1147,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p313]) ).
cnf(p1154,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1147]) ).
cnf(p1157,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1154]) ).
cnf(p1161,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1157]) ).
cnf(p1163,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1161]) ).
cnf(p1164,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| ~ qtd2(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1163]) ).
cnf(p6105,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p5959,p1164]) ).
cnf(p6451,plain,
( qtd0(f(X0),s(s(qtd1)))
| qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p6105,p5958]) ).
cnf(p6454,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p6451]) ).
cnf(p6528,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(s(qtd1)))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p6501,p6454]) ).
cnf(p6563,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p6528]) ).
cnf(p6586,plain,
( qtd0(f(X0),s(s(qtd1)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p6220,p6563]) ).
cnf(p6595,plain,
( ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(s(qtd1)),f(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p6586]) ).
cnf(p6596,plain,
( qtd0(f(X0),s(s(qtd1)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p6595,p5958]) ).
cnf(p6602,plain,
( ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p6596]) ).
cnf(p6603,plain,
( qtd0(f(X0),s(s(qtd1)))
| ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p6602,p6501]) ).
cnf(p6607,plain,
( ~ qtd2(s(s(qtd1)),f(suc(suc(X0))))
| qtd0(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p6603]) ).
cnf(p6610,plain,
( qtd0(f(X0),s(s(qtd1)))
| qtd0(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p6607,p5960]) ).
cnf(p6612,plain,
qtd0(f(X0),s(s(qtd1))),
inference(factoring,[status(thm)],[p6610]) ).
cnf(f51,axiom,
( qtd0(f(B_53),s(qtd1))
| qtd2(s(qtd1),f(suc(suc(B_53))))
| ~ qtd0(f(suc(suc(B_53))),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_508) ).
fof(f51_nnf,plain,
! [B_53] :
( qtd0(f(B_53),s(qtd1))
| qtd2(s(qtd1),f(suc(suc(B_53))))
| ~ qtd0(f(suc(suc(B_53))),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
! [B_53] :
( qtd0(f(B_53),s(qtd1))
| qtd2(s(qtd1),f(suc(suc(B_53))))
| ~ qtd0(f(suc(suc(B_53))),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
( qtd0(f(X0),s(qtd1))
| qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p6615,plain,
( qtd0(f(X0),s(qtd1))
| qtd2(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p6612,c51]) ).
cnf(f23,axiom,
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd2(s(qtd1),f(A_3))
| ~ qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(suc(suc(A_3)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_125) ).
fof(f23_nnf,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd2(s(qtd1),f(A_3))
| ~ qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(suc(suc(A_3)))) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd2(s(qtd1),f(A_3))
| ~ qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(suc(suc(A_3)))) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p6621,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6615,c23]) ).
cnf(f21,axiom,
( qtd0(f(B_53),s(qtd1))
| qtd2(s(qtd1),f(suc(B_53)))
| ~ qtd0(f(suc(B_53)),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_95) ).
fof(f21_nnf,plain,
! [B_53] :
( qtd0(f(B_53),s(qtd1))
| qtd2(s(qtd1),f(suc(B_53)))
| ~ qtd0(f(suc(B_53)),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [B_53] :
( qtd0(f(B_53),s(qtd1))
| qtd2(s(qtd1),f(suc(B_53)))
| ~ qtd0(f(suc(B_53)),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( qtd0(f(X0),s(qtd1))
| qtd2(s(qtd1),f(suc(X0)))
| ~ qtd0(f(suc(X0)),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p6614,plain,
( qtd0(f(X0),s(qtd1))
| qtd2(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p6612,c21]) ).
cnf(p6630,plain,
( qtd0(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6621,p6614]) ).
cnf(p6632,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p6630]) ).
cnf(f41,axiom,
( qtd0(f(B_53),s(qtd1))
| qtd2(s(qtd1),f(B_53))
| ~ qtd0(f(B_53),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_44) ).
fof(f41_nnf,plain,
! [B_53] :
( qtd0(f(B_53),s(qtd1))
| qtd2(s(qtd1),f(B_53))
| ~ qtd0(f(B_53),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [B_53] :
( qtd0(f(B_53),s(qtd1))
| qtd2(s(qtd1),f(B_53))
| ~ qtd0(f(B_53),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
( qtd0(f(X0),s(qtd1))
| qtd2(s(qtd1),f(X0))
| ~ qtd0(f(X0),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p6613,plain,
( qtd0(f(X0),s(qtd1))
| qtd2(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p6612,c41]) ).
cnf(f28,axiom,
( iLEQ(suc(A_3),suc(A_3))
| qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(A_3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_563) ).
fof(f28_nnf,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(A_3)) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(A_3)) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p6616,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6613,c28]) ).
cnf(p6623,plain,
( qtd0(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6616,p6614]) ).
cnf(p6625,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p6623]) ).
cnf(p6633,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(qtd1),f(X0))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6632,p6625]) ).
cnf(p6635,plain,
( iLEQ(suc(X0),suc(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(qtd1),f(X0))
| qtd0(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p6633]) ).
cnf(p6637,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(qtd1),f(X0))
| qtd0(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p6635]) ).
cnf(p6638,plain,
( qtd0(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6637,p6613]) ).
cnf(p6641,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p6638]) ).
cnf(f39,axiom,
( ~ qtd2(s(qtd1),f(B_54))
| ~ qtd2(s(qtd1),f(suc(suc(A_3))))
| ~ qtd2(s(qtd1),f(suc(B_54)))
| ~ qtd2(s(qtd1),f(suc(suc(B_55))))
| ~ qtd2(s(qtd1),f(B_55))
| ~ qtd2(s(qtd1),f(A_3))
| ~ qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(f(B_54),f(suc(B_54)))
| ~ qtd2(s(qtd1),f(suc(suc(B_54))))
| ~ qtd2(s(qtd1),f(suc(B_55)))
| ~ iLEQ(suc(A_3),suc(B_54))
| ~ qtd2(f(B_55),f(suc(B_55)))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ iLEQ(suc(B_54),suc(B_55)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_41) ).
fof(f39_nnf,plain,
! [B_54,B_55,A_3] :
( ~ qtd2(s(qtd1),f(B_54))
| ~ qtd2(s(qtd1),f(suc(suc(A_3))))
| ~ qtd2(s(qtd1),f(suc(B_54)))
| ~ qtd2(s(qtd1),f(suc(suc(B_55))))
| ~ qtd2(s(qtd1),f(B_55))
| ~ qtd2(s(qtd1),f(A_3))
| ~ qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(f(B_54),f(suc(B_54)))
| ~ qtd2(s(qtd1),f(suc(suc(B_54))))
| ~ qtd2(s(qtd1),f(suc(B_55)))
| ~ iLEQ(suc(A_3),suc(B_54))
| ~ qtd2(f(B_55),f(suc(B_55)))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ iLEQ(suc(B_54),suc(B_55)) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [B_54,B_55,A_3] :
( ~ qtd2(s(qtd1),f(B_54))
| ~ qtd2(s(qtd1),f(suc(suc(A_3))))
| ~ qtd2(s(qtd1),f(suc(B_54)))
| ~ qtd2(s(qtd1),f(suc(suc(B_55))))
| ~ qtd2(s(qtd1),f(B_55))
| ~ qtd2(s(qtd1),f(A_3))
| ~ qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(f(B_54),f(suc(B_54)))
| ~ qtd2(s(qtd1),f(suc(suc(B_54))))
| ~ qtd2(s(qtd1),f(suc(B_55)))
| ~ iLEQ(suc(A_3),suc(B_54))
| ~ qtd2(f(B_55),f(suc(B_55)))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ iLEQ(suc(B_54),suc(B_55)) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(suc(X2))))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(suc(X1))))
| ~ qtd2(s(qtd1),f(X1))
| ~ qtd2(s(qtd1),f(X2))
| ~ qtd2(f(X2),f(suc(X2)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(s(qtd1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd2(f(X1),f(suc(X1)))
| ~ qtd2(s(qtd1),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p699,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c39]) ).
cnf(p4187,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p699]) ).
cnf(p4191,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p4187]) ).
cnf(p4193,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p4191]) ).
cnf(p4196,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p4193]) ).
cnf(p4199,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p4196]) ).
cnf(p4208,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p4199]) ).
cnf(p4210,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p4208]) ).
cnf(p4211,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p4210]) ).
cnf(p6659,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6641,p4211]) ).
cnf(p6676,plain,
( qtd0(f(X0),s(qtd1))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6659,p6614]) ).
cnf(p6678,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p6676]) ).
cnf(f14,axiom,
( qtd2(f(B_55),f(suc(B_55)))
| qtd2(f(B_54),f(suc(B_54)))
| qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(B_54))
| ~ qtd2(s(qtd1),f(suc(B_54)))
| ~ qtd2(s(qtd1),f(B_55))
| ~ qtd2(s(qtd1),f(A_3))
| ~ qtd2(s(qtd1),f(suc(B_55)))
| ~ iLEQ(suc(A_3),suc(B_54))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ iLEQ(suc(B_54),suc(B_55)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_687) ).
fof(f14_nnf,plain,
! [B_54,B_55,A_3] :
( qtd2(f(B_55),f(suc(B_55)))
| qtd2(f(B_54),f(suc(B_54)))
| qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(B_54))
| ~ qtd2(s(qtd1),f(suc(B_54)))
| ~ qtd2(s(qtd1),f(B_55))
| ~ qtd2(s(qtd1),f(A_3))
| ~ qtd2(s(qtd1),f(suc(B_55)))
| ~ iLEQ(suc(A_3),suc(B_54))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ iLEQ(suc(B_54),suc(B_55)) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [B_54,B_55,A_3] :
( qtd2(f(B_55),f(suc(B_55)))
| qtd2(f(B_54),f(suc(B_54)))
| qtd2(f(A_3),f(suc(A_3)))
| ~ qtd2(s(qtd1),f(B_54))
| ~ qtd2(s(qtd1),f(suc(B_54)))
| ~ qtd2(s(qtd1),f(B_55))
| ~ qtd2(s(qtd1),f(A_3))
| ~ qtd2(s(qtd1),f(suc(B_55)))
| ~ iLEQ(suc(A_3),suc(B_54))
| ~ qtd2(s(qtd1),f(suc(A_3)))
| ~ iLEQ(suc(B_54),suc(B_55)) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( qtd2(f(X1),f(suc(X1)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X2),f(suc(X2)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X1))
| ~ qtd2(s(qtd1),f(X2))
| ~ qtd2(s(qtd1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd2(s(qtd1),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p247,plain,
( qtd2(f(X1),f(suc(X1)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X1),f(suc(X1)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X1))
| ~ qtd2(s(qtd1),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd2(s(qtd1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(factoring,[status(thm)],[c14]) ).
cnf(p875,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p247]) ).
cnf(p913,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p875]) ).
cnf(p916,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p913]) ).
cnf(p917,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p916]) ).
cnf(p919,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p917]) ).
cnf(p938,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p919]) ).
cnf(p6649,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6641,p938]) ).
cnf(p6663,plain,
( qtd0(f(X0),s(qtd1))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6649,p6614]) ).
cnf(p6665,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(s(qtd1),f(X0))
| qtd0(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p6663]) ).
cnf(p6666,plain,
( qtd0(f(X0),s(qtd1))
| qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6665,p6613]) ).
cnf(p6669,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p6666]) ).
cnf(p6679,plain,
( qtd0(f(X0),s(qtd1))
| ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6678,p6669]) ).
cnf(p6680,plain,
( ~ qtd2(s(qtd1),f(X0))
| ~ qtd2(s(qtd1),f(suc(suc(X0))))
| qtd0(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p6679]) ).
cnf(p6683,plain,
( qtd0(f(X0),s(qtd1))
| ~ qtd2(s(qtd1),f(X0))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6680,p6615]) ).
cnf(p6684,plain,
( ~ qtd2(s(qtd1),f(X0))
| qtd0(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p6683]) ).
cnf(p6685,plain,
( qtd0(f(X0),s(qtd1))
| qtd0(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p6684,p6613]) ).
cnf(p6688,plain,
qtd0(f(X0),s(qtd1)),
inference(factoring,[status(thm)],[p6685]) ).
cnf(f50,axiom,
( qtd0(f(B_60),qtd1)
| qtd2(qtd1,f(suc(B_60)))
| ~ qtd0(f(suc(B_60)),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_595) ).
fof(f50_nnf,plain,
! [B_60] :
( qtd0(f(B_60),qtd1)
| qtd2(qtd1,f(suc(B_60)))
| ~ qtd0(f(suc(B_60)),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [B_60] :
( qtd0(f(B_60),qtd1)
| qtd2(qtd1,f(suc(B_60)))
| ~ qtd0(f(suc(B_60)),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
( qtd0(f(X0),qtd1)
| qtd2(qtd1,f(suc(X0)))
| ~ qtd0(f(suc(X0)),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(p6690,plain,
( qtd0(f(X0),qtd1)
| qtd2(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p6688,c50]) ).
cnf(f48,axiom,
( ~ qtd2(qtd1,f(A_4))
| ~ qtd2(f(B_61),f(suc(B_61)))
| ~ qtd2(qtd1,f(suc(suc(B_61))))
| ~ qtd2(qtd1,f(B_62))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(suc(B_62))))
| ~ qtd2(qtd1,f(B_61))
| ~ qtd2(f(B_62),f(suc(B_62)))
| ~ qtd2(qtd1,f(suc(suc(A_4))))
| ~ qtd2(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(A_4),suc(B_61))
| ~ qtd2(f(A_4),f(suc(A_4)))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ qtd2(qtd1,f(suc(B_61))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_363) ).
fof(f48_nnf,plain,
! [B_61,B_62,A_4] :
( ~ qtd2(qtd1,f(A_4))
| ~ qtd2(f(B_61),f(suc(B_61)))
| ~ qtd2(qtd1,f(suc(suc(B_61))))
| ~ qtd2(qtd1,f(B_62))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(suc(B_62))))
| ~ qtd2(qtd1,f(B_61))
| ~ qtd2(f(B_62),f(suc(B_62)))
| ~ qtd2(qtd1,f(suc(suc(A_4))))
| ~ qtd2(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(A_4),suc(B_61))
| ~ qtd2(f(A_4),f(suc(A_4)))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ qtd2(qtd1,f(suc(B_61))) ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [B_61,B_62,A_4] :
( ~ qtd2(qtd1,f(A_4))
| ~ qtd2(f(B_61),f(suc(B_61)))
| ~ qtd2(qtd1,f(suc(suc(B_61))))
| ~ qtd2(qtd1,f(B_62))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(suc(B_62))))
| ~ qtd2(qtd1,f(B_61))
| ~ qtd2(f(B_62),f(suc(B_62)))
| ~ qtd2(qtd1,f(suc(suc(A_4))))
| ~ qtd2(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(A_4),suc(B_61))
| ~ qtd2(f(A_4),f(suc(A_4)))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ qtd2(qtd1,f(suc(B_61))) ),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c48,plain,
( ~ qtd2(qtd1,f(X2))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(qtd1,f(X1))
| ~ qtd2(qtd1,f(suc(X2)))
| ~ qtd2(qtd1,f(suc(suc(X1))))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(f(X1),f(suc(X1)))
| ~ qtd2(qtd1,f(suc(suc(X2))))
| ~ qtd2(qtd1,f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd2(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p887,plain,
( ~ qtd2(qtd1,f(X1))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(qtd1,f(X1))
| ~ qtd2(qtd1,f(suc(X1)))
| ~ qtd2(qtd1,f(suc(suc(X1))))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X1))))
| ~ qtd2(qtd1,f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd2(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c48]) ).
cnf(p2288,plain,
( ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p887]) ).
cnf(p2298,plain,
( ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p2288]) ).
cnf(p2302,plain,
( ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p2298]) ).
cnf(p2306,plain,
( ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p2302]) ).
cnf(p2309,plain,
( ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p2306]) ).
cnf(p2312,plain,
( ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p2309]) ).
cnf(p2314,plain,
( ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p2312]) ).
cnf(p2316,plain,
( ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p2314]) ).
cnf(p6996,plain,
( ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p6690,p2316]) ).
cnf(f24,axiom,
( qtd0(f(B_60),qtd1)
| qtd2(qtd1,f(suc(suc(B_60))))
| ~ qtd0(f(suc(suc(B_60))),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_61) ).
fof(f24_nnf,plain,
! [B_60] :
( qtd0(f(B_60),qtd1)
| qtd2(qtd1,f(suc(suc(B_60))))
| ~ qtd0(f(suc(suc(B_60))),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [B_60] :
( qtd0(f(B_60),qtd1)
| qtd2(qtd1,f(suc(suc(B_60))))
| ~ qtd0(f(suc(suc(B_60))),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( qtd0(f(X0),qtd1)
| qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p6691,plain,
( qtd0(f(X0),qtd1)
| qtd2(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p6688,c24]) ).
cnf(f26,axiom,
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd2(qtd1,f(A_4))
| ~ qtd2(f(A_4),f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(suc(A_4)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_560) ).
fof(f26_nnf,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd2(qtd1,f(A_4))
| ~ qtd2(f(A_4),f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(suc(A_4)))) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd2(qtd1,f(A_4))
| ~ qtd2(f(A_4),f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(suc(A_4)))) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ qtd2(qtd1,f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p7071,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(suc(X0)))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p6691,c26]) ).
cnf(p7267,plain,
( qtd0(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p7071,p6690]) ).
cnf(p7269,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p7267]) ).
cnf(f17,axiom,
( qtd0(f(B_60),qtd1)
| qtd2(qtd1,f(B_60))
| ~ qtd0(f(B_60),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_497) ).
fof(f17_nnf,plain,
! [B_60] :
( qtd0(f(B_60),qtd1)
| qtd2(qtd1,f(B_60))
| ~ qtd0(f(B_60),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [B_60] :
( qtd0(f(B_60),qtd1)
| qtd2(qtd1,f(B_60))
| ~ qtd0(f(B_60),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( qtd0(f(X0),qtd1)
| qtd2(qtd1,f(X0))
| ~ qtd0(f(X0),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p6689,plain,
( qtd0(f(X0),qtd1)
| qtd2(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p6688,c17]) ).
cnf(f25,axiom,
( iLEQ(suc(A_4),suc(A_4))
| qtd2(f(A_4),f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(A_4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_713) ).
fof(f25_nnf,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| qtd2(f(A_4),f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(A_4)) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| qtd2(f(A_4),f(suc(A_4)))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(A_4)) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ qtd2(qtd1,f(X0)) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p6692,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(suc(X0)))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p6689,c25]) ).
cnf(p7260,plain,
( qtd0(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p6692,p6690]) ).
cnf(p7262,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p7260]) ).
cnf(p7270,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(X0))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p7269,p7262]) ).
cnf(p7273,plain,
( qtd0(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(X0))
| qtd0(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p7270]) ).
cnf(p7274,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(X0))
| qtd0(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p7273]) ).
cnf(p7275,plain,
( qtd0(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p7274,p6689]) ).
cnf(p7278,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p7275]) ).
cnf(p7309,plain,
( qtd0(f(X0),qtd1)
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p6996,p7278]) ).
cnf(p7310,plain,
( ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p7309]) ).
cnf(f8,axiom,
( qtd2(f(B_62),f(suc(B_62)))
| qtd2(f(B_61),f(suc(B_61)))
| qtd2(f(A_4),f(suc(A_4)))
| ~ qtd2(qtd1,f(A_4))
| ~ qtd2(qtd1,f(B_62))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(B_61))
| ~ qtd2(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(A_4),suc(B_61))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ qtd2(qtd1,f(suc(B_61))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_614) ).
fof(f8_nnf,plain,
! [B_61,B_62,A_4] :
( qtd2(f(B_62),f(suc(B_62)))
| qtd2(f(B_61),f(suc(B_61)))
| qtd2(f(A_4),f(suc(A_4)))
| ~ qtd2(qtd1,f(A_4))
| ~ qtd2(qtd1,f(B_62))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(B_61))
| ~ qtd2(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(A_4),suc(B_61))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ qtd2(qtd1,f(suc(B_61))) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [B_61,B_62,A_4] :
( qtd2(f(B_62),f(suc(B_62)))
| qtd2(f(B_61),f(suc(B_61)))
| qtd2(f(A_4),f(suc(A_4)))
| ~ qtd2(qtd1,f(A_4))
| ~ qtd2(qtd1,f(B_62))
| ~ qtd2(qtd1,f(suc(A_4)))
| ~ qtd2(qtd1,f(B_61))
| ~ qtd2(qtd1,f(suc(B_62)))
| ~ iLEQ(suc(A_4),suc(B_61))
| ~ iLEQ(suc(B_61),suc(B_62))
| ~ qtd2(qtd1,f(suc(B_61))) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( qtd2(f(X1),f(suc(X1)))
| qtd2(f(X0),f(suc(X0)))
| qtd2(f(X2),f(suc(X2)))
| ~ qtd2(qtd1,f(X2))
| ~ qtd2(qtd1,f(X1))
| ~ qtd2(qtd1,f(suc(X2)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p136,plain,
( qtd2(f(X1),f(suc(X1)))
| qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X1))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c8]) ).
cnf(p514,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p136]) ).
cnf(p515,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p514]) ).
cnf(p518,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p515]) ).
cnf(p552,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p518]) ).
cnf(p554,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p552]) ).
cnf(p555,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd2(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p554]) ).
cnf(p6887,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p6690,p555]) ).
cnf(p7299,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| qtd0(f(X0),qtd1)
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p7278,p6887]) ).
cnf(p7302,plain,
( qtd2(f(X0),f(suc(X0)))
| ~ qtd2(qtd1,f(X0))
| qtd0(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p7299]) ).
cnf(p7303,plain,
( qtd0(f(X0),qtd1)
| qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p7302,p6689]) ).
cnf(p7306,plain,
( qtd2(f(X0),f(suc(X0)))
| qtd0(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p7303]) ).
cnf(p7311,plain,
( qtd0(f(X0),qtd1)
| ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p7310,p7306]) ).
cnf(p7312,plain,
( ~ qtd2(qtd1,f(X0))
| ~ qtd2(qtd1,f(suc(suc(X0))))
| qtd0(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p7311]) ).
cnf(p7315,plain,
( qtd0(f(X0),qtd1)
| ~ qtd2(qtd1,f(X0))
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p7312,p6691]) ).
cnf(p7316,plain,
( ~ qtd2(qtd1,f(X0))
| qtd0(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p7315]) ).
cnf(p7317,plain,
( qtd0(f(X0),qtd1)
| qtd0(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p7316,p6689]) ).
cnf(p7320,plain,
qtd0(f(X0),qtd1),
inference(factoring,[status(thm)],[p7317]) ).
cnf(f16,axiom,
~ qtd0(f(z),qtd1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_359) ).
fof(f16_nnf,plain,
~ qtd0(f(z),qtd1),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
~ qtd0(f(z),qtd1),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
~ qtd0(f(z),qtd1),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p7321,plain,
$false,
inference(resolution,[status(thm)],[p7320,c16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO681-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 03:24:04 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 22.14/22.71 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.14/22.71 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------