%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SYO689-1 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 21 19:45:11 EDT 2022
% Result : Unsatisfiable 1.47s 1.64s
% Output : Refutation 1.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 22
% Syntax : Number of clauses : 178 ( 6 unt; 162 nHn; 115 RR)
% Number of literals : 840 ( 0 equ; 106 neg)
% Maximal clause size : 17 ( 4 avg)
% Maximal term depth : 7 ( 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 : 108 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_1581,axiom,
( ~ 'E'(s(s(s(s('0')))),f(X))
| ~ 'E'(s(s(s(s('0')))),f(suc(X)))
| iLEQ(suc(X),suc(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1581) ).
cnf(clause_1218,axiom,
( ~ 'E'(s(s('0')),f(X))
| ~ 'E'(s(s('0')),f(suc(X)))
| iLEQ(suc(X),suc(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1218) ).
cnf(clause_327,axiom,
( ~ 'E'(s('0'),f(suc(X)))
| ~ 'E'(s('0'),f(Y))
| ~ 'E'(s('0'),f(suc(Z)))
| ~ iLEQ(suc(U),suc(Z))
| ~ 'E'(s('0'),f(V))
| ~ 'E'(s('0'),f(X))
| ~ 'E'(s('0'),f(suc(U)))
| ~ iLEQ(suc(X),suc(U))
| ~ iLEQ(suc(W),suc(X))
| ~ iLEQ(suc(Z),suc(Y))
| ~ 'E'(s('0'),f(suc(Y)))
| ~ iLEQ(suc(Y),suc(V))
| ~ 'E'(s('0'),f(suc(W)))
| ~ 'E'(s('0'),f(suc(V)))
| ~ 'E'(s('0'),f(Z))
| ~ 'E'(s('0'),f(W))
| ~ 'E'(s('0'),f(U)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_327) ).
cnf(clause_583,axiom,
'LE'(f(X),s(s(s(s(s('0')))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_583) ).
cnf(clause_740,axiom,
( ~ 'LE'(f(X),s(s('0')))
| 'E'(s('0'),f(X))
| 'LE'(f(X),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_740) ).
cnf(clause_388,axiom,
( ~ 'LE'(f(suc(X)),s(s(s('0'))))
| 'E'(s(s('0')),f(suc(X)))
| 'LE'(f(X),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_388) ).
cnf(clause_657,axiom,
( ~ 'E'(s(s(s('0'))),f(X))
| ~ 'E'(s(s(s('0'))),f(suc(Y)))
| ~ 'E'(s(s(s('0'))),f(Z))
| ~ 'E'(s(s(s('0'))),f(U))
| ~ iLEQ(suc(V),suc(U))
| ~ 'E'(s(s(s('0'))),f(Y))
| ~ 'E'(s(s(s('0'))),f(suc(U)))
| ~ 'E'(s(s(s('0'))),f(W))
| ~ iLEQ(suc(Y),suc(X))
| ~ iLEQ(suc(W),suc(V))
| ~ 'E'(s(s(s('0'))),f(suc(W)))
| ~ 'E'(s(s(s('0'))),f(V))
| ~ 'E'(s(s(s('0'))),f(suc(Z)))
| ~ 'E'(s(s(s('0'))),f(suc(X)))
| ~ iLEQ(suc(U),suc(Z))
| ~ iLEQ(suc(X),suc(W))
| ~ 'E'(s(s(s('0'))),f(suc(V))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_657) ).
cnf(clause_328,axiom,
( ~ 'LE'(f(X),s('0'))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_328) ).
cnf(clause_1314,axiom,
( ~ 'LE'(f(X),s(s(s('0'))))
| 'E'(s(s('0')),f(X))
| 'LE'(f(X),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1314) ).
cnf(clause_2293,axiom,
( ~ 'E'('0',f(X))
| ~ 'E'('0',f(suc(X)))
| iLEQ(suc(X),suc(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2293) ).
cnf(clause_1092,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1092) ).
cnf(clause_1230,axiom,
( ~ 'LE'(f(X),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(X))
| 'LE'(f(X),s(s(s('0')))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1230) ).
cnf(clause_421,axiom,
( ~ 'E'('0',f(X))
| ~ iLEQ(suc(Y),suc(Z))
| ~ 'E'('0',f(suc(Z)))
| ~ iLEQ(suc(U),suc(Y))
| ~ 'E'('0',f(U))
| ~ 'E'('0',f(Y))
| ~ 'E'('0',f(V))
| ~ 'E'('0',f(suc(U)))
| ~ 'E'('0',f(suc(W)))
| ~ 'E'('0',f(W))
| ~ iLEQ(suc(X),suc(W))
| ~ iLEQ(suc(Z),suc(V))
| ~ 'E'('0',f(suc(X)))
| ~ 'E'('0',f(suc(V)))
| ~ 'E'('0',f(suc(Y)))
| ~ iLEQ(suc(V),suc(X))
| ~ 'E'('0',f(Z)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_421) ).
cnf(clause_1514,axiom,
( ~ 'E'(s(s(s(s('0')))),f(X))
| ~ 'E'(s(s(s(s('0')))),f(suc(X)))
| ~ iLEQ(suc(Y),suc(Z))
| ~ iLEQ(suc(X),suc(U))
| ~ 'E'(s(s(s(s('0')))),f(suc(Z)))
| ~ 'E'(s(s(s(s('0')))),f(U))
| ~ 'E'(s(s(s(s('0')))),f(V))
| ~ iLEQ(suc(Z),suc(X))
| ~ 'E'(s(s(s(s('0')))),f(Y))
| ~ iLEQ(suc(U),suc(V))
| ~ 'E'(s(s(s(s('0')))),f(suc(V)))
| ~ 'E'(s(s(s(s('0')))),f(suc(W)))
| ~ iLEQ(suc(W),suc(Y))
| ~ 'E'(s(s(s(s('0')))),f(suc(Y)))
| ~ 'E'(s(s(s(s('0')))),f(W))
| ~ 'E'(s(s(s(s('0')))),f(suc(U)))
| ~ 'E'(s(s(s(s('0')))),f(Z)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1514) ).
cnf(clause_1329,axiom,
( ~ 'E'(s('0'),f(X))
| ~ 'E'(s('0'),f(suc(X)))
| iLEQ(suc(X),suc(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1329) ).
cnf(clause_1935,axiom,
( ~ 'LE'(f(suc(X)),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'LE'(f(X),s(s(s('0')))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1935) ).
cnf(clause_2115,axiom,
( ~ 'LE'(f(X),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(X))
| 'LE'(f(X),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2115) ).
cnf(18,plain,
( 'E'(s(s(s(s('0')))),f(X))
| 'LE'(f(X),s(s(s(s('0'))))) ),
inference('REWRITE',[status(thm)],[clause_2115,clause_583]) ).
cnf(clause_2227,axiom,
( ~ 'E'(s(s(s('0'))),f(X))
| ~ 'E'(s(s(s('0'))),f(suc(X)))
| iLEQ(suc(X),suc(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2227) ).
cnf(clause_1440,axiom,
( ~ 'LE'(f(suc(X)),s(s('0')))
| 'E'(s('0'),f(suc(X)))
| 'LE'(f(X),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1440) ).
cnf(clause_2050,axiom,
( ~ 'LE'(f(suc(X)),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(suc(X)))
| 'LE'(f(X),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2050) ).
cnf(22,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'LE'(f(X),s(s(s(s('0'))))) ),
inference('REWRITE',[status(thm)],[clause_2050,clause_583]) ).
cnf(clause_1712,axiom,
( ~ 'E'(s(s('0')),f(X))
| ~ 'E'(s(s('0')),f(suc(Y)))
| ~ 'E'(s(s('0')),f(Z))
| ~ 'E'(s(s('0')),f(U))
| ~ 'E'(s(s('0')),f(suc(U)))
| ~ iLEQ(suc(Y),suc(U))
| ~ 'E'(s(s('0')),f(suc(V)))
| ~ 'E'(s(s('0')),f(Y))
| ~ iLEQ(suc(U),suc(X))
| ~ 'E'(s(s('0')),f(W))
| ~ iLEQ(suc(V),suc(Y))
| ~ 'E'(s(s('0')),f(suc(X)))
| ~ iLEQ(suc(X),suc(Z))
| ~ 'E'(s(s('0')),f(suc(W)))
| ~ 'E'(s(s('0')),f(suc(Z)))
| ~ 'E'(s(s('0')),f(V))
| ~ iLEQ(suc(Z),suc(W)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1712) ).
cnf(clause_113,axiom,
( ~ 'LE'(f(suc(X)),s('0'))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_113) ).
cnf(25,plain,
( 'E'(s(s(s(s('0')))),f(X))
| 'E'(s(s(s('0'))),f(X))
| 'LE'(f(X),s(s(s('0')))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1230,18]) ).
cnf(26,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(X))
| 'LE'(f(X),s(s(s('0')))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1230,22]) ).
cnf(27,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'LE'(f(X),s(s(s('0')))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1935,18]) ).
cnf(28,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'LE'(f(X),s(s(s('0')))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1935,22]) ).
cnf(29,plain,
( 'E'(s(s(s(s('0')))),f(X))
| 'E'(s(s(s('0'))),f(X))
| 'E'(s(s('0')),f(X))
| 'LE'(f(X),s(s('0'))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1314,25]) ).
cnf(30,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'LE'(f(X),s(s('0'))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_388,25]) ).
cnf(31,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(X))
| 'E'(s(s('0')),f(X))
| 'LE'(f(X),s(s('0'))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1314,26]) ).
cnf(32,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'LE'(f(X),s(s('0'))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_388,26]) ).
cnf(33,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(X))
| 'LE'(f(X),s(s('0'))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1314,27]) ).
cnf(34,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'LE'(f(X),s(s('0'))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_388,27]) ).
cnf(35,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(X))
| 'LE'(f(X),s(s('0'))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1314,28]) ).
cnf(36,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'LE'(f(X),s(s('0'))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_388,28]) ).
cnf(37,plain,
( 'E'(s(s(s(s('0')))),f(X))
| 'E'(s(s(s('0'))),f(X))
| 'E'(s(s('0')),f(X))
| 'E'(s('0'),f(X))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_740,29]) ).
cnf(38,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1440,29]) ).
cnf(39,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(X))
| 'E'(s(s('0')),f(X))
| 'E'(s('0'),f(X))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_740,31]) ).
cnf(40,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1440,31]) ).
cnf(41,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(X))
| 'E'(s('0'),f(X))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_740,33]) ).
cnf(42,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1440,33]) ).
cnf(43,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(X))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_740,30]) ).
cnf(44,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1440,30]) ).
cnf(45,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(X))
| 'E'(s('0'),f(X))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_740,35]) ).
cnf(46,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1440,35]) ).
cnf(47,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(X))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_740,32]) ).
cnf(48,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1440,32]) ).
cnf(49,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(X))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_740,34]) ).
cnf(50,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X)))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1440,34]) ).
cnf(51,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(X))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_740,36]) ).
cnf(52,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(X))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X)))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'LE'(f(X),s('0')) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1440,36]) ).
cnf(53,plain,
( 'E'(s(s(s(s('0')))),f(X))
| 'E'(s(s(s('0'))),f(X))
| 'E'(s(s('0')),f(X))
| 'E'(s('0'),f(X))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,37]) ).
cnf(54,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,37]) ).
cnf(55,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(X))
| 'E'(s(s('0')),f(X))
| 'E'(s('0'),f(X))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,39]) ).
cnf(56,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,39]) ).
cnf(57,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(X))
| 'E'(s('0'),f(X))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,41]) ).
cnf(58,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,41]) ).
cnf(59,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(X))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,43]) ).
cnf(60,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,43]) ).
cnf(61,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(X))
| 'E'(s('0'),f(X))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,45]) ).
cnf(62,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,45]) ).
cnf(63,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(X))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,47]) ).
cnf(64,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,47]) ).
cnf(65,plain,
( 'E'(s(s(s(s('0')))),f(suc(X)))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,38]) ).
cnf(66,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(suc(X))))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,38]) ).
cnf(67,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(X))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,49]) ).
cnf(68,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X)))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,49]) ).
cnf(69,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(X)))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,40]) ).
cnf(70,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(suc(X))))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,40]) ).
cnf(71,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(X))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,51]) ).
cnf(72,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(X))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X)))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,51]) ).
cnf(73,plain,
( 'E'(s(s(s(s('0')))),f(z))
| 'E'(s(s(s('0'))),f(z))
| 'E'(s(s('0')),f(z))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,53]) ).
cnf(74,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,42]) ).
cnf(75,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X)))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(suc(X))))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,42]) ).
cnf(76,plain,
( 'E'(s(s(s(s('0')))),f(suc(z)))
| 'E'(s(s(s('0'))),f(z))
| 'E'(s(s('0')),f(z))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,55]) ).
cnf(77,plain,
( 'E'(s(s(s('0'))),f(z))
| 'E'(s(s('0')),f(z))
| 'E'(s('0'),f(z))
| 'E'('0',f(z))
| iLEQ(suc(z),suc(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,76,73]) ).
cnf(78,plain,
( 'E'(s(s(s('0'))),f(z))
| 'E'(s(s('0')),f(z))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,77,73,76,77,76,73,73,77,73,77,76,76,77,76,73,76,73]) ).
cnf(79,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(X)))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,46]) ).
cnf(80,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(X))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X)))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(suc(X))))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,46]) ).
cnf(81,plain,
( 'E'(s(s(s(s('0')))),f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(z))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,57]) ).
cnf(82,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,44]) ).
cnf(83,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X)))))
| 'E'(s(s('0')),f(suc(suc(suc(X)))))
| 'E'(s('0'),f(suc(suc(X))))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,44]) ).
cnf(84,plain,
( 'E'(s(s(s(s('0')))),f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,59]) ).
cnf(85,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(z))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,61]) ).
cnf(86,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(z))
| 'E'(s('0'),f(z))
| 'E'('0',f(z))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,85,81]) ).
cnf(87,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(z))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,86,81,85,86,85,81,81,86,81,86,85,85,86,85,81,85,81]) ).
cnf(88,plain,
( 'E'(s(s('0')),f(z))
| 'E'(s('0'),f(z))
| 'E'('0',f(z))
| iLEQ(suc(z),suc(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_2227,87,78]) ).
cnf(89,plain,
( 'E'(s(s('0')),f(z))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_657,88,78,87,78,78,88,78,87,78,88,88,87,78,87,87,88,87]) ).
cnf(90,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(X))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,48]) ).
cnf(91,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(X))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X)))))
| 'E'(s(s('0')),f(suc(suc(suc(X)))))
| 'E'(s('0'),f(suc(suc(X))))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,48]) ).
cnf(92,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,63]) ).
cnf(93,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(z))
| 'E'('0',f(z))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,92,84]) ).
cnf(94,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,93,84,92,93,92,84,84,93,84,93,92,92,93,92,84,92,84]) ).
cnf(95,plain,
( 'E'(s(s(s(s('0')))),f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,65]) ).
cnf(96,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,67]) ).
cnf(97,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(X)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X)))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,50]) ).
cnf(98,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(X))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X))))))
| 'E'(s(s('0')),f(suc(suc(suc(X)))))
| 'E'(s('0'),f(suc(suc(X))))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,50]) ).
cnf(99,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,69]) ).
cnf(100,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,99,95]) ).
cnf(101,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,100,95,99,100,99,95,95,100,95,100,99,99,100,99,95,99,95]) ).
cnf(102,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,71]) ).
cnf(103,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(z))
| 'E'('0',f(z))
| iLEQ(suc(suc(suc(z))),suc(suc(suc(z)))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,102,96]) ).
cnf(104,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,103,96,102,103,102,96,96,103,96,103,102,102,103,102,96,102,96]) ).
cnf(105,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(z))
| 'E'('0',f(z))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_2227,104,94]) ).
cnf(106,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_657,105,94,104,94,94,105,94,104,94,105,105,104,94,104,104,105,104]) ).
cnf(107,plain,
( 'E'(s('0'),f(z))
| 'E'('0',f(z))
| iLEQ(suc(z),suc(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1218,106,89]) ).
cnf(108,plain,
( 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1712,107,89,106,89,89,106,106,89,107,89,107,106,107,106,106,89,107]) ).
cnf(109,plain,
( 'E'(s(s(s(s('0')))),f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,54]) ).
cnf(110,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,74]) ).
cnf(111,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(X))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X)))))
| 'E'(s(s('0')),f(suc(suc(X))))
| 'E'(s('0'),f(suc(X)))
| 'E'('0',f(X))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_328,52]) ).
cnf(112,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(suc(X)))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X))))))
| 'E'(s(s('0')),f(suc(suc(suc(X)))))
| 'E'(s('0'),f(suc(suc(X))))
| 'E'('0',f(suc(X)))
| 'LE'(f(X),'0') ),
inference('HYPERRESOLVE',[status(thm)],[clause_113,52]) ).
cnf(113,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,56]) ).
cnf(114,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,113,109]) ).
cnf(115,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,114,109,113,114,113,109,109,114,109,114,113,113,114,113,109,113,109]) ).
cnf(116,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,79]) ).
cnf(117,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z))
| iLEQ(suc(suc(suc(z))),suc(suc(suc(z)))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,116,110]) ).
cnf(118,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,117,110,116,117,116,110,110,117,110,117,116,116,117,116,110,116,110]) ).
cnf(119,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_2227,118,101]) ).
cnf(120,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_657,119,101,118,101,101,119,101,118,101,119,119,118,101,118,118,119,118]) ).
cnf(121,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,58]) ).
cnf(122,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,82]) ).
cnf(123,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,62]) ).
cnf(124,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(suc(z))),suc(suc(suc(z)))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,123,121]) ).
cnf(125,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,124,121,123,124,123,121,121,124,121,124,123,123,124,123,121,123,121]) ).
cnf(126,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_2227,125,115]) ).
cnf(127,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_657,126,115,125,115,115,126,115,125,115,126,126,125,115,125,125,126,125]) ).
cnf(128,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,90]) ).
cnf(129,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z))
| iLEQ(suc(suc(suc(z))),suc(suc(suc(z)))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,128,122]) ).
cnf(130,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,129,122,128,129,128,122,122,129,122,129,128,128,129,128,122,128,122]) ).
cnf(131,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,60]) ).
cnf(132,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,64]) ).
cnf(133,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(suc(z))),suc(suc(suc(z)))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,132,131]) ).
cnf(134,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,133,131,132,133,132,131,131,133,131,133,132,132,133,132,131,132,131]) ).
cnf(135,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,97]) ).
cnf(136,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,66]) ).
cnf(137,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,68]) ).
cnf(138,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,70]) ).
cnf(139,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(suc(z))),suc(suc(suc(z)))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,138,136]) ).
cnf(140,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,139,136,138,139,138,136,136,139,136,139,138,138,139,138,136,138,136]) ).
cnf(141,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,111]) ).
cnf(142,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z))
| iLEQ(suc(suc(suc(suc(z)))),suc(suc(suc(suc(z))))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,141,135]) ).
cnf(143,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,142,135,141,142,141,135,135,142,135,142,141,141,142,141,135,141,135]) ).
cnf(144,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z))
| iLEQ(suc(suc(suc(z))),suc(suc(suc(z)))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_2227,143,130]) ).
cnf(145,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_657,144,130,143,130,130,144,130,143,130,144,144,143,130,143,143,144,143]) ).
cnf(146,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1218,145,120]) ).
cnf(147,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1712,146,120,145,120,120,145,145,120,146,120,146,145,146,145,145,120,146]) ).
cnf(148,plain,
( 'E'('0',f(z))
| iLEQ(suc(z),suc(z)) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1329,147,108]) ).
cnf(149,plain,
'E'('0',f(z)),
inference('HYPERRESOLVE',[status(thm)],[clause_327,148,147,108,147,108,108,147,148,148,148,147,148,147,147,108,108,108]) ).
cnf(150,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,72]) ).
cnf(151,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(suc(suc(z)))),suc(suc(suc(suc(z))))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,150,137]) ).
cnf(152,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,151,137,150,151,150,137,137,151,137,151,150,150,151,150,137,150,137]) ).
cnf(153,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(suc(z))),suc(suc(suc(z)))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_2227,152,134]) ).
cnf(154,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_657,153,134,152,134,134,153,134,152,134,153,153,152,134,152,152,153,152]) ).
cnf(155,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1218,154,127]) ).
cnf(156,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1712,155,127,154,127,127,154,154,127,155,127,155,154,155,154,154,127,155]) ).
cnf(157,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,75]) ).
cnf(158,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,80]) ).
cnf(159,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(suc(suc(z)))),suc(suc(suc(suc(z))))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,158,157]) ).
cnf(160,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,159,157,158,159,158,157,157,159,157,159,158,158,159,158,157,158,157]) ).
cnf(161,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(suc(z))),suc(suc(suc(z)))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_2227,160,140]) ).
cnf(162,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_657,161,140,160,140,140,161,140,160,140,161,161,160,140,160,160,161,160]) ).
cnf(163,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,83]) ).
cnf(164,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,91]) ).
cnf(165,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(suc(suc(z)))),suc(suc(suc(suc(z))))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,164,163]) ).
cnf(166,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,165,163,164,165,164,163,163,165,163,165,164,164,165,164,163,164,163]) ).
cnf(167,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,98]) ).
cnf(168,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(suc(z)))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1092,112]) ).
cnf(169,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(suc(suc(suc(z))))),suc(suc(suc(suc(suc(z)))))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1581,168,167]) ).
cnf(170,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1514,169,167,168,169,168,167,167,169,167,169,168,168,169,168,167,168,167]) ).
cnf(171,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(suc(suc(z)))),suc(suc(suc(suc(z))))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_2227,170,166]) ).
cnf(172,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_657,171,166,170,166,166,171,166,170,166,171,171,170,166,170,170,171,170]) ).
cnf(173,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| iLEQ(suc(suc(suc(z))),suc(suc(suc(z)))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1218,172,162]) ).
cnf(174,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1712,173,162,172,162,162,172,172,162,173,162,173,172,173,172,172,162,173]) ).
cnf(175,plain,
( 'E'('0',f(suc(z)))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference('HYPERRESOLVE',[status(thm)],[clause_1329,174,156]) ).
cnf(176,plain,
'E'('0',f(suc(z))),
inference('HYPERRESOLVE',[status(thm)],[clause_327,175,174,156,174,156,156,174,175,175,175,174,175,174,174,156,156,156]) ).
cnf(177,plain,
iLEQ(suc(z),suc(z)),
inference('HYPERRESOLVE',[status(thm)],[clause_2293,176,149]) ).
cnf(178,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[clause_421,176,149,176,149,149,149,176,176,149,176,176,149]),177]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SYO689-1 : TPTP v8.1.0. Released v7.3.0.
% 0.11/0.12 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n027.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Fri Jul 8 21:31:31 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.44 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 *
% 0.19/0.45 *
% 0.19/0.46 #<PACKAGE "SNARK-USER">
% 0.19/0.46 *
% 0.19/0.46 SNARK-TPTP-OPTIONS
% 0.19/0.46 *
% 0.19/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.46 (USE-FACTORING :POS)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.46 *
% 0.19/0.46 "."
% 0.19/0.46 *
% 0.19/0.46 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-07-08T21:31:31
% 0.19/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n027.cluster.edu at 2022-07-08T21:31:31
% 1.47/1.64
% 1.47/1.64
% 1.47/1.64 #||
% 1.47/1.64 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.47/1.64 % SZS output start Refutation
% See solution above
% 1.47/1.68 ||#
% 1.47/1.68
% 1.47/1.68 ; Summary of computation:
% 1.47/1.68 ; 10432 formulas have been input or derived (from 175 formulas).
% 1.47/1.68 ; 178 ( 2%) were retained. Of these,
% 1.47/1.68 ; 92 (52%) were simplified or subsumed later,
% 1.47/1.68 ; 86 (48%) are still being kept.
% 1.47/1.68 ;
% 1.47/1.68 ; Run time in seconds excluding printing time:
% 1.47/1.68 ; 0.011 1% Read assertion file (1 call)
% 1.47/1.68 ; 0.004 0% Assert (22 calls)
% 1.47/1.68 ; 0.033 3% Process new row (202 calls)
% 1.47/1.68 ; 1.056 89% Resolution (348 calls)
% 1.47/1.68 ; 0.002 0% Paramodulation (174 calls)
% 1.47/1.68 ; 0.001 0% Factoring (152 calls)
% 1.47/1.68 ; 0.011 1% Condensing (183 calls)
% 1.47/1.68 ; 0.015 1% Forward subsumption (183 calls)
% 1.47/1.68 ; 0.021 2% Backward subsumption (170 calls)
% 1.47/1.68 ; 0.003 0% Clause clause subsumption (1,342 calls)
% 1.47/1.68 ; 0.004 0% Forward simplification (189 calls)
% 1.47/1.68 ; 0.000 0% Backward simplification (176 calls)
% 1.47/1.68 ; 0.003 0% Ordering (644 calls)
% 1.47/1.68 ; 0.000 0% Sortal reasoning (32 calls)
% 1.47/1.68 ; 0.000 0% Purity testing (1 call)
% 1.47/1.68 ; 0.020 2% Other
% 1.47/1.68 ; 1.184 Total
% 1.47/1.68 ; 1.221 Real time
% 1.47/1.68 ;
% 1.47/1.68 ; Term-hash-array has 170 terms in all.
% 1.47/1.68 ; Feature-vector-row-index has 80 entries (90 at peak, 170 added, 90 deleted).
% 1.47/1.68 ; Feature-vector-row-index has 342 nodes (469 at peak, 1,549 added, 1,207 deleted).
% 1.47/1.68 ; Retrieved 1,153 possibly forward subsuming rows in 183 calls.
% 1.47/1.68 ; Retrieved 216 possibly backward subsumed rows in 170 calls.
% 1.47/1.68 ; Path-index has 142 entries (158 at peak, 302 added, 160 deleted).
% 1.47/1.68 ; Path-index has 100 nodes (112 at peak, 254 added, 154 deleted).
% 1.47/1.68 ; Trie-index has 142 entries (158 at peak, 302 added, 160 deleted).
% 1.47/1.68 ; Trie-index has 124 nodes (148 at peak, 442 added, 318 deleted).
% 1.47/1.68 ; Retrieved 3 generalization terms in 181 calls.
% 1.47/1.68 ; Retrieved 5 instance terms in 5 calls.
% 1.47/1.68 ; Retrieved 257,033 unifiable terms in 71,161 calls.
% 1.47/1.68 ;
% 1.47/1.68 ; The agenda of rows to process has 2 entries:
% 1.47/1.68 ; 2 with value 21
% 1.47/1.68 ; The agenda of rows to give has 1 entry:
% 1.47/1.68 ; 1 with value (4 21)
% 1.47/1.68 Evaluation took:
% 1.47/1.68 1.221 seconds of real time
% 1.47/1.68 1.199564 seconds of user run time
% 1.47/1.68 0.021863 seconds of system run time
% 1.47/1.68 [Run times include 0.03 seconds GC run time.]
% 1.47/1.68 0 calls to %EVAL
% 1.47/1.68 0 page faults and
% 1.47/1.68 140,029,128 bytes consed.
% 1.47/1.68 :PROOF-FOUND
% 1.47/1.68 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-07-08T21:31:32
% 1.47/1.68 :PROOF-FOUND
% 1.47/1.68 *
%------------------------------------------------------------------------------