%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYO648-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 : n001.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:35 PM UTC 2026
% Result : Unsatisfiable 172.14s 34.94s
% Output : Proof 172.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 15
% Syntax : Number of formulae : 168 ( 11 unt; 0 def)
% Number of atoms : 1021 ( 0 equ)
% Maximal formula atoms : 17 ( 6 avg)
% Number of connectives : 1548 ( 695 ~; 853 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 7 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 : 117 ( 2 sgn 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f23,axiom,
( ~ qtd0(qtd1,f(suc(suc(suc(suc(A_1))))))
| ~ qtd0(qtd1,f(suc(suc(B_2))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_2),f(suc(suc(suc(B_2)))))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(f(B_2),f(suc(B_2)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(B_2))))))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(f(B_2),f(suc(suc(B_2))))
| ~ qtd0(qtd1,f(suc(suc(suc(B_2)))))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_145) ).
fof(f23_nnf,plain,
! [A_1,B_2] :
( ~ qtd0(qtd1,f(suc(suc(suc(suc(A_1))))))
| ~ qtd0(qtd1,f(suc(suc(B_2))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_2),f(suc(suc(suc(B_2)))))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(f(B_2),f(suc(B_2)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(B_2))))))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(f(B_2),f(suc(suc(B_2))))
| ~ qtd0(qtd1,f(suc(suc(suc(B_2)))))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [A_1,B_2] :
( ~ qtd0(qtd1,f(suc(suc(suc(suc(A_1))))))
| ~ qtd0(qtd1,f(suc(suc(B_2))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_2),f(suc(suc(suc(B_2)))))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(f(B_2),f(suc(B_2)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(B_2))))))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(f(B_2),f(suc(suc(B_2))))
| ~ qtd0(qtd1,f(suc(suc(suc(B_2)))))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(suc(suc(X1))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X1),f(suc(suc(suc(X1)))))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X1))))))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X1),f(suc(suc(X1))))
| ~ qtd0(qtd1,f(suc(suc(suc(X1)))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p313,plain,
( ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[c23]) ).
cnf(p1575,plain,
( ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p313]) ).
cnf(p4475,plain,
( ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p1575]) ).
cnf(p6246,plain,
( ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p4475]) ).
cnf(p6249,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p6246]) ).
cnf(p6254,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p6249]) ).
cnf(p6255,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p6254]) ).
cnf(p6258,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p6255]) ).
cnf(f1,axiom,
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(suc(suc(B_1)))))
| ~ qtd2(f(suc(suc(suc(B_1)))),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_260) ).
fof(f1_nnf,plain,
! [B_1] :
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(suc(suc(B_1)))))
| ~ qtd2(f(suc(suc(suc(B_1)))),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [B_1] :
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(suc(suc(B_1)))))
| ~ qtd2(f(suc(suc(suc(B_1)))),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(f7,axiom,
qtd2(f(A),s(qtd1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_299) ).
fof(f7_nnf,plain,
! [A] : qtd2(f(A),s(qtd1)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A] : qtd2(f(A),s(qtd1)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
qtd2(f(X0),s(qtd1)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p36,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[c1,c7]) ).
cnf(p6261,plain,
( qtd2(f(X0),qtd1)
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p6258,p36]) ).
cnf(f8,axiom,
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(A_1))))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_157) ).
fof(f8_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(A_1))))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(A_1))))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p136,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[c8,p36]) ).
cnf(f9,axiom,
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(B_1)))
| ~ qtd2(f(suc(B_1)),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_328) ).
fof(f9_nnf,plain,
! [B_1] :
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(B_1)))
| ~ qtd2(f(suc(B_1)),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [B_1] :
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(B_1)))
| ~ qtd2(f(suc(B_1)),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p33,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[c9,c7]) ).
cnf(p836,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p136,p33]) ).
cnf(p925,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p836]) ).
cnf(f5,axiom,
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_326) ).
fof(f5_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p96,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[c5,p36]) ).
cnf(p479,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p96,p33]) ).
cnf(p487,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p479]) ).
cnf(f18,axiom,
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(suc(B_1))))
| ~ qtd2(f(suc(suc(B_1))),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_114) ).
fof(f18_nnf,plain,
! [B_1] :
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(suc(B_1))))
| ~ qtd2(f(suc(suc(B_1))),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [B_1] :
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(suc(B_1))))
| ~ qtd2(f(suc(suc(B_1))),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p35,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c18,c7]) ).
cnf(p489,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p487,p35]) ).
cnf(p492,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p489]) ).
cnf(f25,axiom,
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(B_1))
| ~ qtd2(f(B_1),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_62) ).
fof(f25_nnf,plain,
! [B_1] :
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(B_1))
| ~ qtd2(f(B_1),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [B_1] :
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(B_1))
| ~ qtd2(f(B_1),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd2(f(X0),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p27,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[c25,c7]) ).
cnf(f20,axiom,
~ qtd2(f(z),qtd1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_160) ).
fof(f20_nnf,plain,
~ qtd2(f(z),qtd1),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
~ qtd2(f(z),qtd1),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
~ qtd2(f(z),qtd1),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p28,plain,
qtd0(qtd1,f(z)),
inference(resolution,[status(thm)],[p27,c20]) ).
cnf(p493,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(f(z),f(suc(suc(z)))) ),
inference(resolution,[status(thm)],[p492,p28]) ).
cnf(f17,axiom,
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_254) ).
fof(f17_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(suc(A_1)))) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(suc(A_1)))) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(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)],[f17_sk]) ).
cnf(p99,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[c17,p35]) ).
cnf(p102,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p99,p33]) ).
cnf(p106,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p102]) ).
cnf(f2,axiom,
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_48) ).
fof(f2_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(A_1)) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(qtd1,f(A_1)) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,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)],[f2_sk]) ).
cnf(p39,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[c2,p28]) ).
cnf(p43,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z))) ),
inference(resolution,[status(thm)],[p39,p33]) ).
cnf(p127,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(qtd1,f(z)) ),
inference(resolution,[status(thm)],[p106,p43]) ).
cnf(p130,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(qtd1,f(z)) ),
inference(factoring,[status(thm)],[p127]) ).
cnf(p132,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(qtd1,f(z)) ),
inference(factoring,[status(thm)],[p130]) ).
cnf(p133,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(z)))) ),
inference(resolution,[status(thm)],[p132,p28]) ).
cnf(p502,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ qtd0(f(z),f(suc(z))) ),
inference(resolution,[status(thm)],[p493,p133]) ).
cnf(p503,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ qtd0(f(z),f(suc(z))) ),
inference(factoring,[status(thm)],[p502]) ).
cnf(p505,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ qtd0(f(z),f(suc(z))) ),
inference(factoring,[status(thm)],[p503]) ).
cnf(p506,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(suc(z))))) ),
inference(resolution,[status(thm)],[p505,p43]) ).
cnf(p510,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(suc(z))))) ),
inference(factoring,[status(thm)],[p506]) ).
cnf(p512,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(suc(z))))) ),
inference(factoring,[status(thm)],[p510]) ).
cnf(p926,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z)))) ),
inference(resolution,[status(thm)],[p925,p512]) ).
cnf(p929,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z)))) ),
inference(factoring,[status(thm)],[p926]) ).
cnf(p931,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z)))) ),
inference(factoring,[status(thm)],[p929]) ).
cnf(p937,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(qtd1,f(z)) ),
inference(resolution,[status(thm)],[p931,p35]) ).
cnf(p938,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(qtd1,f(z)) ),
inference(factoring,[status(thm)],[p937]) ).
cnf(p939,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(f(z),f(suc(suc(z)))) ),
inference(resolution,[status(thm)],[p938,p28]) ).
cnf(p940,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(f(z),f(suc(z))) ),
inference(resolution,[status(thm)],[p939,p133]) ).
cnf(p942,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(f(z),f(suc(z))) ),
inference(factoring,[status(thm)],[p940]) ).
cnf(p944,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(f(z),f(suc(z))) ),
inference(factoring,[status(thm)],[p942]) ).
cnf(p945,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[status(thm)],[p944,p43]) ).
cnf(p946,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z)))))) ),
inference(factoring,[status(thm)],[p945]) ).
cnf(p949,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z)))))) ),
inference(factoring,[status(thm)],[p946]) ).
cnf(f14,axiom,
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(suc(suc(suc(B_1))))))
| ~ qtd2(f(suc(suc(suc(suc(B_1))))),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_231) ).
fof(f14_nnf,plain,
! [B_1] :
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(suc(suc(suc(B_1))))))
| ~ qtd2(f(suc(suc(suc(suc(B_1))))),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [B_1] :
( qtd2(f(B_1),qtd1)
| qtd0(qtd1,f(suc(suc(suc(suc(B_1))))))
| ~ qtd2(f(suc(suc(suc(suc(B_1))))),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(suc(X0))))))
| ~ qtd2(f(suc(suc(suc(suc(X0))))),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p58,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[status(thm)],[c14,c7]) ).
cnf(p953,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[p949,p58]) ).
cnf(p954,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z)) ),
inference(factoring,[status(thm)],[p953]) ).
cnf(f13,axiom,
( qtd0(f(B_2),f(suc(B_2)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(A_1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_168) ).
fof(f13_nnf,plain,
! [A_1,B_2] :
( qtd0(f(B_2),f(suc(B_2)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(A_1))) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [A_1,B_2] :
( qtd0(f(B_2),f(suc(B_2)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(A_1))) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p159,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c13]) ).
cnf(p164,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p159]) ).
cnf(p166,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p164]) ).
cnf(p179,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p166,p33]) ).
cnf(p183,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[p179,p28]) ).
cnf(p955,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p954,p183]) ).
cnf(p957,plain,
( qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p955]) ).
cnf(f3,axiom,
( qtd0(f(B_2),f(suc(suc(B_2))))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(suc(B_2))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(f(B_2),f(suc(B_2)))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(A_1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_79) ).
fof(f3_nnf,plain,
! [A_1,B_2] :
( qtd0(f(B_2),f(suc(suc(B_2))))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(suc(B_2))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(f(B_2),f(suc(B_2)))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(A_1))) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A_1,B_2] :
( qtd0(f(B_2),f(suc(suc(B_2))))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(suc(B_2))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(f(B_2),f(suc(B_2)))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(A_1))) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( qtd0(f(X1),f(suc(suc(X1))))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X1))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p44,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c3]) ).
cnf(p452,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p44]) ).
cnf(p705,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p452]) ).
cnf(p709,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p705]) ).
cnf(p710,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p709]) ).
cnf(p711,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(X0),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p710,p33]) ).
cnf(p717,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(f(X0),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p711,p35]) ).
cnf(p720,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(X0),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p717]) ).
cnf(p721,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(z))))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z))) ),
inference(resolution,[status(thm)],[p720,p28]) ).
cnf(p959,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(z))))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p957,p721]) ).
cnf(p962,plain,
( qtd0(f(z),f(suc(suc(z))))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p959]) ).
cnf(p963,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(z))))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p962,p954]) ).
cnf(p968,plain,
( qtd0(f(z),f(suc(suc(z))))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p963]) ).
cnf(p6263,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| ~ qtd0(f(z),f(suc(suc(suc(z)))))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p6261,p968]) ).
cnf(p6271,plain,
( qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| ~ qtd0(f(z),f(suc(suc(suc(z)))))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(factoring,[status(thm)],[p6263]) ).
cnf(p6273,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| ~ qtd0(f(z),f(suc(suc(suc(z))))) ),
inference(resolution,[status(thm)],[p6271,p33]) ).
cnf(p6274,plain,
( qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| ~ qtd0(f(z),f(suc(suc(suc(z))))) ),
inference(factoring,[status(thm)],[p6273]) ).
cnf(f4,axiom,
( qtd0(f(B_2),f(suc(suc(suc(B_2)))))
| qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(qtd1,f(suc(suc(B_2))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(f(B_2),f(suc(B_2)))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(f(B_2),f(suc(suc(B_2))))
| ~ qtd0(qtd1,f(suc(suc(suc(B_2)))))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_90) ).
fof(f4_nnf,plain,
! [A_1,B_2] :
( qtd0(f(B_2),f(suc(suc(suc(B_2)))))
| qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(qtd1,f(suc(suc(B_2))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(f(B_2),f(suc(B_2)))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(f(B_2),f(suc(suc(B_2))))
| ~ qtd0(qtd1,f(suc(suc(suc(B_2)))))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A_1,B_2] :
( qtd0(f(B_2),f(suc(suc(suc(B_2)))))
| qtd0(f(A_1),f(suc(suc(suc(A_1)))))
| ~ qtd0(qtd1,f(suc(suc(B_2))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(B_2))
| ~ iLEQ(suc(A_1),suc(B_2))
| ~ qtd0(f(B_2),f(suc(B_2)))
| ~ qtd0(qtd1,f(suc(B_2)))
| ~ qtd0(qtd1,f(A_1))
| ~ qtd0(qtd1,f(suc(suc(A_1))))
| ~ qtd0(qtd1,f(suc(A_1)))
| ~ qtd0(f(B_2),f(suc(suc(B_2))))
| ~ qtd0(qtd1,f(suc(suc(suc(B_2)))))
| ~ qtd0(qtd1,f(suc(suc(suc(A_1))))) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( qtd0(f(X1),f(suc(suc(suc(X1)))))
| qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(suc(X1))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X1),f(suc(suc(X1))))
| ~ qtd0(qtd1,f(suc(suc(suc(X1)))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p66,plain,
( qtd0(f(X0),f(suc(suc(suc(X0)))))
| qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[c4]) ).
cnf(p546,plain,
( qtd0(f(X0),f(suc(suc(suc(X0)))))
| qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p66]) ).
cnf(p2154,plain,
( qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p546]) ).
cnf(p2884,plain,
( qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p2154]) ).
cnf(p2889,plain,
( qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p2884]) ).
cnf(p2900,plain,
( qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p2889]) ).
cnf(p2902,plain,
( qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p2900]) ).
cnf(p2905,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(X0),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p2902,p36]) ).
cnf(p2907,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p2905,p968]) ).
cnf(p2921,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(factoring,[status(thm)],[p2907]) ).
cnf(p2922,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z)))) ),
inference(resolution,[status(thm)],[p2921,p33]) ).
cnf(p2923,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z)))) ),
inference(factoring,[status(thm)],[p2922]) ).
cnf(p2925,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(z)) ),
inference(resolution,[status(thm)],[p2923,p35]) ).
cnf(p2931,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(z)) ),
inference(factoring,[status(thm)],[p2925]) ).
cnf(p2932,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z))) ),
inference(resolution,[status(thm)],[p2931,p28]) ).
cnf(p2933,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[p2932,p957]) ).
cnf(p2934,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z)) ),
inference(factoring,[status(thm)],[p2933]) ).
cnf(p2943,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(suc(z))))) ),
inference(resolution,[status(thm)],[p2934,p954]) ).
cnf(p2944,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(suc(z))))) ),
inference(factoring,[status(thm)],[p2943]) ).
cnf(p6275,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z)))) ),
inference(resolution,[status(thm)],[p6274,p2944]) ).
cnf(p6276,plain,
( qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z)))) ),
inference(factoring,[status(thm)],[p6275]) ).
cnf(p6279,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(qtd1,f(z)) ),
inference(resolution,[status(thm)],[p6276,p35]) ).
cnf(p6280,plain,
( qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z))))))
| ~ qtd0(qtd1,f(z)) ),
inference(factoring,[status(thm)],[p6279]) ).
cnf(p6281,plain,
( qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[status(thm)],[p6280,p28]) ).
cnf(p6285,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z))) ),
inference(resolution,[status(thm)],[p6281,p58]) ).
cnf(p6287,plain,
( qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z))) ),
inference(factoring,[status(thm)],[p6285]) ).
cnf(p6288,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[p6287,p957]) ).
cnf(p6289,plain,
( qtd2(f(z),qtd1)
| ~ iLEQ(suc(z),suc(z)) ),
inference(factoring,[status(thm)],[p6288]) ).
cnf(p6290,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p6289,p954]) ).
cnf(p6293,plain,
qtd2(f(z),qtd1),
inference(factoring,[status(thm)],[p6290]) ).
cnf(p6294,plain,
$false,
inference(resolution,[status(thm)],[p6293,c20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO648-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n001.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 03:25:39 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 172.14/34.94 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 172.14/34.94 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------