%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYO686-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 : Sun Sep 27 09:51:13 AM UTC 2026
% Result : Unsatisfiable 61.65s 9.32s
% Output : CNFRefutation 61.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 91
% Number of leaves : 52
% Syntax : Number of formulae : 385 ( 16 unt; 0 def)
% Number of atoms : 2588 ( 0 equ)
% Maximal formula atoms : 18 ( 6 avg)
% Number of connectives : 4066 (1863 ~;2203 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 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 : 395 ( 5 sgn 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clause_322,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| ~ 'E'(s('0'),f(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(s('0'),f(suc(VAR_0)))
| ~ 'E'(s('0'),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(s('0'),f(suc(suc(VAR_0))))
| ~ 'E'(f(VAR_0),f(suc(VAR_0))) ),
file('theBenchmark.p',clause_322) ).
cnf(c_1,plain,
( iLEQ(suc(A),suc(A))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(clausify,[status(thm)],[clause_322]) ).
fof(clause_380,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(VAR_0)))
| ~ 'E'(s(s(s(s('0')))),f(VAR_0)) ),
file('theBenchmark.p',clause_380) ).
cnf(c_4,plain,
( iLEQ(suc(A),suc(A))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(clausify,[status(thm)],[clause_380]) ).
fof(clause_59,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'('0',f(suc(VAR_0)))
| ~ 'E'('0',f(VAR_0)) ),
file('theBenchmark.p',clause_59) ).
cnf(c_5,plain,
( iLEQ(suc(A),suc(A))
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A)) ),
inference(clausify,[status(thm)],[clause_59]) ).
fof(clause_340,axiom,
! [VAR_0,VAR_1] :
( ~ 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| ~ 'E'(s('0'),f(VAR_0))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(s('0'),f(suc(VAR_0)))
| ~ 'E'(s('0'),f(suc(suc(suc(VAR_1)))))
| ~ 'E'(s('0'),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(s('0'),f(suc(suc(VAR_0))))
| ~ 'E'(s('0'),f(VAR_1))
| ~ 'E'(s('0'),f(suc(suc(VAR_1))))
| ~ 'E'(s('0'),f(suc(VAR_1)))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ iLEQ(suc(VAR_0),suc(VAR_1)) ),
file('theBenchmark.p',clause_340) ).
cnf(c_6,plain,
( ~ 'E'(f(B),f(suc(suc(B))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(B)))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(B))
| ~ 'E'(s('0'),f(suc(suc(B))))
| ~ 'E'(s('0'),f(suc(B)))
| ~ 'E'(f(A),f(suc(A)))
| ~ iLEQ(suc(A),suc(B)) ),
inference(clausify,[status(thm)],[clause_340]) ).
fof(clause_226,axiom,
! [VAR_0,VAR_1] :
( ~ 'E'(s(s('0')),f(suc(suc(VAR_0))))
| ~ 'E'(s(s('0')),f(VAR_1))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(VAR_1)))))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ iLEQ(suc(VAR_1),suc(VAR_0))
| ~ 'E'(s(s('0')),f(suc(suc(VAR_1))))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| ~ 'E'(s(s('0')),f(suc(VAR_1)))
| ~ 'E'(s(s('0')),f(VAR_0))
| ~ 'E'(s(s('0')),f(suc(VAR_0))) ),
file('theBenchmark.p',clause_226) ).
cnf(c_11,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(B))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(B)))))
| ~ 'E'(f(B),f(suc(B)))
| ~ iLEQ(suc(B),suc(A))
| ~ 'E'(s(s('0')),f(suc(suc(B))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(B),f(suc(suc(B))))
| ~ 'E'(s(s('0')),f(suc(B)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(clausify,[status(thm)],[clause_226]) ).
fof(clause_575,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| ~ 'E'(s(s('0')),f(VAR_0))
| ~ 'E'(s(s('0')),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(suc(suc(VAR_0))))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(s(s('0')),f(suc(VAR_0))) ),
file('theBenchmark.p',clause_575) ).
cnf(c_12,plain,
( iLEQ(suc(A),suc(A))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(clausify,[status(thm)],[clause_575]) ).
fof(clause_432,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(VAR_0)) ),
file('theBenchmark.p',clause_432) ).
cnf(c_13,plain,
( iLEQ(suc(A),suc(A))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(clausify,[status(thm)],[clause_432]) ).
fof(clause_614,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| ~ 'E'(s(s(s(s('0')))),f(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(VAR_0)))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(VAR_0))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(VAR_0))))) ),
file('theBenchmark.p',clause_614) ).
cnf(c_14,plain,
( iLEQ(suc(A),suc(A))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A))))) ),
inference(clausify,[status(thm)],[clause_614]) ).
fof(clause_638,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(s(s('0')),f(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(suc(suc(VAR_0)))) ),
file('theBenchmark.p',clause_638) ).
cnf(c_16,plain,
( iLEQ(suc(A),suc(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A)))) ),
inference(clausify,[status(thm)],[clause_638]) ).
fof(clause_308,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(VAR_0))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(VAR_1))))
| ~ 'E'(s(s(s('0'))),f(suc(VAR_1)))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(s(s(s('0'))),f(VAR_0))
| ~ 'E'(s(s(s('0'))),f(VAR_1))
| ~ 'E'(s(s(s('0'))),f(suc(VAR_0)))
| ~ iLEQ(suc(VAR_0),suc(VAR_1)) ),
file('theBenchmark.p',clause_308) ).
cnf(c_17,plain,
( 'E'(f(B),f(suc(suc(B))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(B))))
| ~ 'E'(s(s(s('0'))),f(suc(B)))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(B))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ iLEQ(suc(A),suc(B)) ),
inference(clausify,[status(thm)],[clause_308]) ).
fof(clause_494,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_1),f(suc(VAR_1)))
| 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'('0',f(VAR_1))
| ~ 'E'('0',f(suc(VAR_1)))
| ~ 'E'('0',f(suc(VAR_0)))
| ~ 'E'('0',f(VAR_0))
| ~ iLEQ(suc(VAR_0),suc(VAR_1)) ),
file('theBenchmark.p',clause_494) ).
cnf(c_19,plain,
( 'E'(f(B),f(suc(B)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(B))
| ~ 'E'('0',f(suc(B)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A))
| ~ iLEQ(suc(A),suc(B)) ),
inference(clausify,[status(thm)],[clause_494]) ).
fof(clause_354,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(s('0'),f(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s('0'),f(suc(VAR_0)))
| ~ 'E'(s('0'),f(suc(suc(VAR_0)))) ),
file('theBenchmark.p',clause_354) ).
cnf(c_20,plain,
( iLEQ(suc(A),suc(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A)))) ),
inference(clausify,[status(thm)],[clause_354]) ).
fof(clause_86,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s(s('0'))),f(suc(VAR_0)))
| ~ 'E'(s(s(s('0'))),f(VAR_0)) ),
file('theBenchmark.p',clause_86) ).
cnf(c_22,plain,
( iLEQ(suc(A),suc(A))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A)) ),
inference(clausify,[status(thm)],[clause_86]) ).
fof(clause_643,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'('0',f(suc(suc(VAR_0))))
| ~ 'E'('0',f(suc(VAR_0)))
| ~ 'E'('0',f(suc(suc(suc(VAR_0)))))
| ~ 'E'('0',f(VAR_0)) ),
file('theBenchmark.p',clause_643) ).
cnf(c_23,plain,
( iLEQ(suc(A),suc(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A)) ),
inference(clausify,[status(thm)],[clause_643]) ).
fof(clause_355,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_0),f(suc(VAR_0)))
| 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(s(s('0')),f(VAR_1))
| ~ iLEQ(suc(VAR_1),suc(VAR_0))
| ~ 'E'(s(s('0')),f(suc(VAR_1)))
| ~ 'E'(s(s('0')),f(VAR_0))
| ~ 'E'(s(s('0')),f(suc(VAR_0))) ),
file('theBenchmark.p',clause_355) ).
cnf(c_26,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(B),f(suc(B)))
| ~ 'E'(s(s('0')),f(B))
| ~ iLEQ(suc(B),suc(A))
| ~ 'E'(s(s('0')),f(suc(B)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(clausify,[status(thm)],[clause_355]) ).
fof(clause_558,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(s('0'),f(VAR_0))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(s('0'),f(suc(VAR_0)))
| ~ 'E'(s('0'),f(suc(suc(VAR_0))))
| ~ 'E'(s('0'),f(VAR_1))
| ~ 'E'(s('0'),f(suc(suc(VAR_1))))
| ~ 'E'(s('0'),f(suc(VAR_1)))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ iLEQ(suc(VAR_0),suc(VAR_1)) ),
file('theBenchmark.p',clause_558) ).
cnf(c_28,plain,
( 'E'(f(B),f(suc(suc(B))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(B))
| ~ 'E'(s('0'),f(suc(suc(B))))
| ~ 'E'(s('0'),f(suc(B)))
| ~ 'E'(f(A),f(suc(A)))
| ~ iLEQ(suc(A),suc(B)) ),
inference(clausify,[status(thm)],[clause_558]) ).
fof(clause_139,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_1),f(suc(VAR_1)))
| 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s(s('0'))),f(suc(VAR_1)))
| ~ 'E'(s(s(s('0'))),f(VAR_0))
| ~ 'E'(s(s(s('0'))),f(VAR_1))
| ~ 'E'(s(s(s('0'))),f(suc(VAR_0)))
| ~ iLEQ(suc(VAR_0),suc(VAR_1)) ),
file('theBenchmark.p',clause_139) ).
cnf(c_31,plain,
( 'E'(f(B),f(suc(B)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(B)))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(B))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ iLEQ(suc(A),suc(B)) ),
inference(clausify,[status(thm)],[clause_139]) ).
fof(clause_431,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'('0',f(VAR_0))
| ~ 'E'('0',f(suc(VAR_0)))
| ~ 'E'('0',f(suc(suc(VAR_1))))
| ~ 'E'('0',f(suc(VAR_1)))
| ~ 'E'('0',f(VAR_1))
| ~ iLEQ(suc(VAR_1),suc(VAR_0))
| ~ 'E'('0',f(suc(suc(VAR_0))))
| ~ 'E'(f(VAR_0),f(suc(VAR_0))) ),
file('theBenchmark.p',clause_431) ).
cnf(c_32,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(B),f(suc(suc(B))))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(B))))
| ~ 'E'('0',f(suc(B)))
| ~ 'E'('0',f(B))
| ~ iLEQ(suc(B),suc(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(clausify,[status(thm)],[clause_431]) ).
fof(clause_93,axiom,
! [VAR_0,VAR_1] :
( ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(s(s(s(s('0')))),f(VAR_1))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(VAR_1)))
| ~ 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(VAR_1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(VAR_1)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(VAR_0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(VAR_0))))
| ~ iLEQ(suc(VAR_1),suc(VAR_0))
| ~ 'E'(s(s(s(s('0')))),f(VAR_0)) ),
file('theBenchmark.p',clause_93) ).
cnf(c_34,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(B))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'(s(s(s(s('0')))),f(suc(B)))
| ~ 'E'(f(B),f(suc(suc(B))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(B)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ iLEQ(suc(B),suc(A))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(clausify,[status(thm)],[clause_93]) ).
fof(clause_267,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(s(s(s(s('0')))),f(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(VAR_0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(VAR_0)))) ),
file('theBenchmark.p',clause_267) ).
cnf(c_35,plain,
( iLEQ(suc(A),suc(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A)))) ),
inference(clausify,[status(thm)],[clause_267]) ).
fof(clause_57,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(s(s(s('0'))),f(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s(s('0'))),f(suc(VAR_0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(VAR_0)))) ),
file('theBenchmark.p',clause_57) ).
cnf(c_38,plain,
( iLEQ(suc(A),suc(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(clausify,[status(thm)],[clause_57]) ).
fof(clause_250,axiom,
! [VAR_0,VAR_1] :
( ~ 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'('0',f(VAR_0))
| ~ 'E'('0',f(suc(VAR_0)))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'('0',f(suc(suc(suc(VAR_0)))))
| ~ 'E'('0',f(suc(suc(VAR_1))))
| ~ 'E'('0',f(suc(VAR_1)))
| ~ 'E'('0',f(suc(suc(suc(VAR_1)))))
| ~ 'E'('0',f(VAR_1))
| ~ iLEQ(suc(VAR_1),suc(VAR_0))
| ~ 'E'('0',f(suc(suc(VAR_0))))
| ~ 'E'(f(VAR_0),f(suc(VAR_0))) ),
file('theBenchmark.p',clause_250) ).
cnf(c_40,plain,
( ~ 'E'(f(B),f(suc(suc(B))))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(suc(B))))
| ~ 'E'('0',f(suc(B)))
| ~ 'E'('0',f(suc(suc(suc(B)))))
| ~ 'E'('0',f(B))
| ~ iLEQ(suc(B),suc(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(clausify,[status(thm)],[clause_250]) ).
fof(clause_425,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s(s(s('0')))),f(VAR_1))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(VAR_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(VAR_1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(VAR_0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(VAR_0))))
| ~ iLEQ(suc(VAR_1),suc(VAR_0))
| ~ 'E'(s(s(s(s('0')))),f(VAR_0)) ),
file('theBenchmark.p',clause_425) ).
cnf(c_41,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(B),f(suc(suc(B))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(B))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'(s(s(s(s('0')))),f(suc(B)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ iLEQ(suc(B),suc(A))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(clausify,[status(thm)],[clause_425]) ).
fof(clause_149,axiom,
! [VAR_0,VAR_1] :
( ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(VAR_0))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(VAR_1))))
| ~ 'E'(s(s(s('0'))),f(suc(VAR_1)))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| ~ 'E'(s(s(s('0'))),f(VAR_0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(VAR_1)))))
| ~ 'E'(s(s(s('0'))),f(VAR_1))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(s(s(s('0'))),f(suc(VAR_0)))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ iLEQ(suc(VAR_0),suc(VAR_1)) ),
file('theBenchmark.p',clause_149) ).
cnf(c_44,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(B))))
| ~ 'E'(s(s(s('0'))),f(suc(B)))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'(f(B),f(suc(suc(B))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(B)))))
| ~ 'E'(s(s(s('0'))),f(B))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ iLEQ(suc(A),suc(B)) ),
inference(clausify,[status(thm)],[clause_149]) ).
fof(clause_323,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(VAR_0))))
| ~ 'E'(s(s(s('0'))),f(VAR_0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(s(s(s('0'))),f(suc(VAR_0)))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0)))) ),
file('theBenchmark.p',clause_323) ).
cnf(c_50,plain,
( iLEQ(suc(A),suc(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(clausify,[status(thm)],[clause_323]) ).
fof(clause_264,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_1),f(suc(VAR_1)))
| 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s('0'),f(VAR_0))
| ~ 'E'(s('0'),f(suc(VAR_0)))
| ~ 'E'(s('0'),f(VAR_1))
| ~ 'E'(s('0'),f(suc(VAR_1)))
| ~ iLEQ(suc(VAR_0),suc(VAR_1)) ),
file('theBenchmark.p',clause_264) ).
cnf(c_52,plain,
( 'E'(f(B),f(suc(B)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(B))
| ~ 'E'(s('0'),f(suc(B)))
| ~ iLEQ(suc(A),suc(B)) ),
inference(clausify,[status(thm)],[clause_264]) ).
fof(clause_550,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| ~ 'E'(s(s('0')),f(suc(suc(VAR_0))))
| ~ 'E'(s(s('0')),f(VAR_1))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ iLEQ(suc(VAR_1),suc(VAR_0))
| ~ 'E'(s(s('0')),f(suc(suc(VAR_1))))
| ~ 'E'(s(s('0')),f(suc(VAR_1)))
| ~ 'E'(s(s('0')),f(VAR_0))
| ~ 'E'(s(s('0')),f(suc(VAR_0))) ),
file('theBenchmark.p',clause_550) ).
cnf(c_53,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(B),f(suc(suc(B))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(B))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(B),f(suc(B)))
| ~ iLEQ(suc(B),suc(A))
| ~ 'E'(s(s('0')),f(suc(suc(B))))
| ~ 'E'(s(s('0')),f(suc(B)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(clausify,[status(thm)],[clause_550]) ).
fof(clause_573,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'('0',f(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'('0',f(suc(VAR_0)))
| ~ 'E'('0',f(suc(suc(VAR_0)))) ),
file('theBenchmark.p',clause_573) ).
cnf(c_54,plain,
( iLEQ(suc(A),suc(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(clausify,[status(thm)],[clause_573]) ).
fof(clause_105,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_0),f(suc(VAR_0)))
| 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(s(s(s(s('0')))),f(VAR_1))
| ~ 'E'(s(s(s(s('0')))),f(suc(VAR_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(VAR_0)))
| ~ iLEQ(suc(VAR_1),suc(VAR_0))
| ~ 'E'(s(s(s(s('0')))),f(VAR_0)) ),
file('theBenchmark.p',clause_105) ).
cnf(c_55,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(B),f(suc(B)))
| ~ 'E'(s(s(s(s('0')))),f(B))
| ~ 'E'(s(s(s(s('0')))),f(suc(B)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ iLEQ(suc(B),suc(A))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(clausify,[status(thm)],[clause_105]) ).
fof(clause_601,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s('0'),f(suc(VAR_0)))
| ~ 'E'(s('0'),f(VAR_0)) ),
file('theBenchmark.p',clause_601) ).
cnf(c_58,plain,
( iLEQ(suc(A),suc(A))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A)) ),
inference(clausify,[status(thm)],[clause_601]) ).
cnf(c_61,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A)) ),
inference(resolve,[status(thm)],[c_58,c_52]) ).
cnf(c_839,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A)) ),
inference(copy,[status(thm)],[c_61]) ).
cnf(c_840,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A)) ),
inference(copy,[status(thm)],[c_839]) ).
cnf(c_841,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(A))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A)) ),
inference(copy,[status(thm)],[c_840]) ).
cnf(c_842,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A)) ),
inference(copy,[status(thm)],[c_841]) ).
cnf(c_843,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A)) ),
inference(copy,[status(thm)],[c_842]) ).
cnf(c_62,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A)) ),
inference(copy,[status(thm)],[c_843]) ).
cnf(c_63,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(resolve,[status(thm)],[c_55,c_4]) ).
cnf(c_844,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_63]) ).
cnf(c_845,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_844]) ).
cnf(c_846,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_845]) ).
cnf(c_847,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_846]) ).
cnf(c_848,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_847]) ).
cnf(c_64,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_848]) ).
cnf(c_65,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_54,c_32]) ).
cnf(c_849,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_65]) ).
cnf(c_850,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_849]) ).
cnf(c_851,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_850]) ).
cnf(c_852,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_851]) ).
cnf(c_853,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_852]) ).
cnf(c_854,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_853]) ).
cnf(c_855,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_854]) ).
cnf(c_856,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_855]) ).
cnf(c_857,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_856]) ).
cnf(c_66,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_857]) ).
cnf(c_67,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(resolve,[status(thm)],[c_53,c_16]) ).
cnf(c_858,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_67]) ).
cnf(c_859,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_858]) ).
cnf(c_860,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_859]) ).
cnf(c_861,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_860]) ).
cnf(c_862,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_861]) ).
cnf(c_863,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_862]) ).
cnf(c_864,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_863]) ).
cnf(c_865,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_864]) ).
cnf(c_866,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_865]) ).
cnf(c_68,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_866]) ).
cnf(c_70,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_50,c_44]) ).
cnf(c_867,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_70]) ).
cnf(c_868,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_867]) ).
cnf(c_869,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_868]) ).
cnf(c_870,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_869]) ).
cnf(c_871,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_870]) ).
cnf(c_872,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_871]) ).
cnf(c_873,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_872]) ).
cnf(c_874,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_873]) ).
cnf(c_875,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_874]) ).
cnf(c_876,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_875]) ).
cnf(c_877,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_876]) ).
cnf(c_71,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_877]) ).
cnf(c_72,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(resolve,[status(thm)],[c_41,c_35]) ).
cnf(c_878,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_72]) ).
cnf(c_879,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_878]) ).
cnf(c_880,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_879]) ).
cnf(c_881,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_880]) ).
cnf(c_882,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_881]) ).
cnf(c_883,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_882]) ).
cnf(c_884,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_883]) ).
cnf(c_885,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_884]) ).
cnf(c_886,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_885]) ).
cnf(c_73,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_886]) ).
cnf(c_74,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_40,c_23]) ).
cnf(c_887,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_74]) ).
cnf(c_888,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_887]) ).
cnf(c_889,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_888]) ).
cnf(c_890,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_889]) ).
cnf(c_891,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_890]) ).
cnf(c_892,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_891]) ).
cnf(c_893,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_892]) ).
cnf(c_894,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_893]) ).
cnf(c_895,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_894]) ).
cnf(c_896,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_895]) ).
cnf(c_897,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_896]) ).
cnf(c_75,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_897]) ).
cnf(c_76,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_38,c_17]) ).
cnf(c_898,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_76]) ).
cnf(c_899,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_898]) ).
cnf(c_900,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_899]) ).
cnf(c_901,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_900]) ).
cnf(c_902,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_901]) ).
cnf(c_903,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_902]) ).
cnf(c_904,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_903]) ).
cnf(c_905,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_904]) ).
cnf(c_906,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_905]) ).
cnf(c_77,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_906]) ).
cnf(c_81,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(resolve,[status(thm)],[c_34,c_14]) ).
cnf(c_907,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_81]) ).
cnf(c_908,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_907]) ).
cnf(c_909,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_908]) ).
cnf(c_910,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_909]) ).
cnf(c_911,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_910]) ).
cnf(c_912,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_911]) ).
cnf(c_913,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_912]) ).
cnf(c_914,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_913]) ).
cnf(c_915,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_914]) ).
cnf(c_916,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_915]) ).
cnf(c_917,plain,
( ~ 'E'(s(s(s(s('0')))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_916]) ).
cnf(c_82,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(A)) ),
inference(copy,[status(thm)],[c_917]) ).
cnf(c_85,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(A))) ),
inference(resolve,[status(thm)],[c_31,c_22]) ).
cnf(c_918,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(A))) ),
inference(copy,[status(thm)],[c_85]) ).
cnf(c_919,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(A))) ),
inference(copy,[status(thm)],[c_918]) ).
cnf(c_920,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(A))) ),
inference(copy,[status(thm)],[c_919]) ).
cnf(c_921,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(A))) ),
inference(copy,[status(thm)],[c_920]) ).
cnf(c_922,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(A))) ),
inference(copy,[status(thm)],[c_921]) ).
cnf(c_86,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(A))) ),
inference(copy,[status(thm)],[c_922]) ).
cnf(c_87,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_28,c_20]) ).
cnf(c_923,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_87]) ).
cnf(c_924,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_923]) ).
cnf(c_925,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_924]) ).
cnf(c_926,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_925]) ).
cnf(c_927,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_926]) ).
cnf(c_928,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_927]) ).
cnf(c_929,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_928]) ).
cnf(c_930,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_929]) ).
cnf(c_931,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_930]) ).
cnf(c_88,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_931]) ).
cnf(c_89,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(resolve,[status(thm)],[c_26,c_13]) ).
cnf(c_932,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_89]) ).
cnf(c_933,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_932]) ).
cnf(c_934,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_933]) ).
cnf(c_935,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_934]) ).
cnf(c_936,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_935]) ).
cnf(c_90,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_936]) ).
cnf(c_93,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A)) ),
inference(resolve,[status(thm)],[c_19,c_5]) ).
cnf(c_937,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A)) ),
inference(copy,[status(thm)],[c_93]) ).
cnf(c_938,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A))
| 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A)) ),
inference(copy,[status(thm)],[c_937]) ).
cnf(c_939,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A))
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A)) ),
inference(copy,[status(thm)],[c_938]) ).
cnf(c_940,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A)) ),
inference(copy,[status(thm)],[c_939]) ).
cnf(c_941,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A)) ),
inference(copy,[status(thm)],[c_940]) ).
cnf(c_94,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A)) ),
inference(copy,[status(thm)],[c_941]) ).
cnf(c_97,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(resolve,[status(thm)],[c_12,c_11]) ).
cnf(c_942,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_97]) ).
cnf(c_943,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_942]) ).
cnf(c_944,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_943]) ).
cnf(c_945,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_944]) ).
cnf(c_946,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_945]) ).
cnf(c_947,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_946]) ).
cnf(c_948,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_947]) ).
cnf(c_949,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_948]) ).
cnf(c_950,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_949]) ).
cnf(c_951,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_950]) ).
cnf(c_952,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_951]) ).
cnf(c_98,plain,
( ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(copy,[status(thm)],[c_952]) ).
cnf(c_99,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_6,c_1]) ).
cnf(c_953,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_99]) ).
cnf(c_954,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_953]) ).
cnf(c_955,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_954]) ).
cnf(c_956,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_955]) ).
cnf(c_957,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_956]) ).
cnf(c_958,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_957]) ).
cnf(c_959,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_958]) ).
cnf(c_960,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_959]) ).
cnf(c_961,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_960]) ).
cnf(c_962,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_961]) ).
cnf(c_963,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_962]) ).
cnf(c_100,plain,
( ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_963]) ).
fof(clause_486,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),'0')
| 'E'('0',f(suc(VAR_0)))
| ~ 'LE'(f(suc(VAR_0)),s('0')) ),
file('theBenchmark.p',clause_486) ).
cnf(c_101,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(A)))
| ~ 'LE'(f(suc(A)),s('0')) ),
inference(clausify,[status(thm)],[clause_486]) ).
fof(clause_534,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s('0'))
| 'E'(s('0'),f(VAR_0))
| ~ 'LE'(f(VAR_0),s(s('0'))) ),
file('theBenchmark.p',clause_534) ).
cnf(c_102,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(A))
| ~ 'LE'(f(A),s(s('0'))) ),
inference(clausify,[status(thm)],[clause_534]) ).
fof(clause_345,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(VAR_0))
| ~ 'LE'(f(VAR_0),s(s(s(s(s('0')))))) ),
file('theBenchmark.p',clause_345) ).
cnf(c_103,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(A))
| ~ 'LE'(f(A),s(s(s(s(s('0')))))) ),
inference(clausify,[status(thm)],[clause_345]) ).
fof(clause_295,axiom,
~ 'LE'(f(z),'0'),
file('theBenchmark.p',clause_295) ).
cnf(c_104,plain,
~ 'LE'(f(z),'0'),
inference(clausify,[status(thm)],[clause_295]) ).
fof(clause_158,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(VAR_0))))
| ~ 'LE'(f(suc(suc(VAR_0))),s(s(s(s('0'))))) ),
file('theBenchmark.p',clause_158) ).
cnf(c_105,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'LE'(f(suc(suc(A))),s(s(s(s('0'))))) ),
inference(clausify,[status(thm)],[clause_158]) ).
fof(clause_603,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(suc(VAR_0)))))
| ~ 'LE'(f(suc(suc(suc(VAR_0)))),s(s(s(s(s('0')))))) ),
file('theBenchmark.p',clause_603) ).
cnf(c_106,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'LE'(f(suc(suc(suc(A)))),s(s(s(s(s('0')))))) ),
inference(clausify,[status(thm)],[clause_603]) ).
fof(clause_356,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s('0'))
| 'E'(s('0'),f(suc(suc(VAR_0))))
| ~ 'LE'(f(suc(suc(VAR_0))),s(s('0'))) ),
file('theBenchmark.p',clause_356) ).
cnf(c_107,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(suc(A))))
| ~ 'LE'(f(suc(suc(A))),s(s('0'))) ),
inference(clausify,[status(thm)],[clause_356]) ).
fof(clause_368,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s('0')))
| 'E'(s(s('0')),f(VAR_0))
| ~ 'LE'(f(VAR_0),s(s(s('0')))) ),
file('theBenchmark.p',clause_368) ).
cnf(c_108,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(A))
| ~ 'LE'(f(A),s(s(s('0')))) ),
inference(clausify,[status(thm)],[clause_368]) ).
fof(clause_335,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(VAR_0)))
| ~ 'LE'(f(suc(VAR_0)),s(s(s(s('0'))))) ),
file('theBenchmark.p',clause_335) ).
cnf(c_109,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'LE'(f(suc(A)),s(s(s(s('0'))))) ),
inference(clausify,[status(thm)],[clause_335]) ).
fof(clause_503,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),'0')
| 'E'('0',f(VAR_0))
| ~ 'LE'(f(VAR_0),s('0')) ),
file('theBenchmark.p',clause_503) ).
cnf(c_110,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(A))
| ~ 'LE'(f(A),s('0')) ),
inference(clausify,[status(thm)],[clause_503]) ).
fof(clause_41,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),'0')
| 'E'('0',f(suc(suc(VAR_0))))
| ~ 'LE'(f(suc(suc(VAR_0))),s('0')) ),
file('theBenchmark.p',clause_41) ).
cnf(c_111,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(suc(A))))
| ~ 'LE'(f(suc(suc(A))),s('0')) ),
inference(clausify,[status(thm)],[clause_41]) ).
fof(clause_282,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(VAR_0))))
| ~ 'LE'(f(suc(suc(VAR_0))),s(s(s(s(s('0')))))) ),
file('theBenchmark.p',clause_282) ).
cnf(c_112,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(A))))
| ~ 'LE'(f(suc(suc(A))),s(s(s(s(s('0')))))) ),
inference(clausify,[status(thm)],[clause_282]) ).
fof(clause_294,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(VAR_0))
| ~ 'LE'(f(VAR_0),s(s(s(s('0'))))) ),
file('theBenchmark.p',clause_294) ).
cnf(c_113,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(A))
| ~ 'LE'(f(A),s(s(s(s('0'))))) ),
inference(clausify,[status(thm)],[clause_294]) ).
fof(clause_263,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s('0')))
| 'E'(s(s('0')),f(suc(VAR_0)))
| ~ 'LE'(f(suc(VAR_0)),s(s(s('0')))) ),
file('theBenchmark.p',clause_263) ).
cnf(c_114,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(A)))
| ~ 'LE'(f(suc(A)),s(s(s('0')))) ),
inference(clausify,[status(thm)],[clause_263]) ).
fof(clause_232,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(VAR_0)))))
| ~ 'LE'(f(suc(suc(suc(VAR_0)))),s(s(s('0')))) ),
file('theBenchmark.p',clause_232) ).
cnf(c_115,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'LE'(f(suc(suc(suc(A)))),s(s(s('0')))) ),
inference(clausify,[status(thm)],[clause_232]) ).
fof(clause_300,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(VAR_0))))
| ~ 'LE'(f(suc(suc(VAR_0))),s(s(s('0')))) ),
file('theBenchmark.p',clause_300) ).
cnf(c_116,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'LE'(f(suc(suc(A))),s(s(s('0')))) ),
inference(clausify,[status(thm)],[clause_300]) ).
fof(clause_478,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),'0')
| 'E'('0',f(suc(suc(suc(VAR_0)))))
| ~ 'LE'(f(suc(suc(suc(VAR_0)))),s('0')) ),
file('theBenchmark.p',clause_478) ).
cnf(c_117,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(suc(suc(A)))))
| ~ 'LE'(f(suc(suc(suc(A)))),s('0')) ),
inference(clausify,[status(thm)],[clause_478]) ).
fof(clause_569,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(VAR_0)))
| ~ 'LE'(f(suc(VAR_0)),s(s(s(s(s('0')))))) ),
file('theBenchmark.p',clause_569) ).
cnf(c_118,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'LE'(f(suc(A)),s(s(s(s(s('0')))))) ),
inference(clausify,[status(thm)],[clause_569]) ).
fof(clause_159,axiom,
! [VAR_0] : 'LE'(f(VAR_0),s(s(s(s(s('0')))))),
file('theBenchmark.p',clause_159) ).
cnf(c_119,plain,
'LE'(f(A),s(s(s(s(s('0')))))),
inference(clausify,[status(thm)],[clause_159]) ).
fof(clause_327,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(VAR_0)))))
| ~ 'LE'(f(suc(suc(suc(VAR_0)))),s(s(s(s('0'))))) ),
file('theBenchmark.p',clause_327) ).
cnf(c_120,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'LE'(f(suc(suc(suc(A)))),s(s(s(s('0'))))) ),
inference(clausify,[status(thm)],[clause_327]) ).
fof(clause_313,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s('0'))
| 'E'(s('0'),f(suc(suc(suc(VAR_0)))))
| ~ 'LE'(f(suc(suc(suc(VAR_0)))),s(s('0'))) ),
file('theBenchmark.p',clause_313) ).
cnf(c_121,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'LE'(f(suc(suc(suc(A)))),s(s('0'))) ),
inference(clausify,[status(thm)],[clause_313]) ).
fof(clause_92,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),s('0'))
| 'E'(s('0'),f(suc(VAR_0)))
| ~ 'LE'(f(suc(VAR_0)),s(s('0'))) ),
file('theBenchmark.p',clause_92) ).
cnf(c_122,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(A)))
| ~ 'LE'(f(suc(A)),s(s('0'))) ),
inference(clausify,[status(thm)],[clause_92]) ).
cnf(c_123,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(A))) ),
inference(resolve,[status(thm)],[c_119,c_118]) ).
cnf(c_124,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_119,c_112]) ).
cnf(c_125,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_119,c_106]) ).
cnf(c_126,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(A)) ),
inference(resolve,[status(thm)],[c_119,c_103]) ).
cnf(c_964,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A))) ),
inference(resolve,[status(thm)],[c_64,c_126]) ).
cnf(c_965,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_964,c_123]) ).
cnf(c_164,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_965]) ).
cnf(c_966,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_73,c_126]) ).
cnf(c_967,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A))) ),
inference(resolve,[status(thm)],[c_966,c_124]) ).
cnf(c_968,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_967,c_123]) ).
cnf(c_969,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_968,c_164]) ).
cnf(c_970,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_969]) ).
cnf(c_971,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_970]) ).
cnf(c_184,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_971]) ).
cnf(c_972,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_82,c_126]) ).
cnf(c_973,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s(s('0')))),f(suc(A))) ),
inference(resolve,[status(thm)],[c_972,c_124]) ).
cnf(c_974,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_973,c_123]) ).
cnf(c_975,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_974,c_125]) ).
cnf(c_976,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_975,c_184]) ).
cnf(c_977,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0'))))) ),
inference(resolve,[status(thm)],[c_976,c_164]) ).
cnf(c_978,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0'))))) ),
inference(copy,[status(thm)],[c_977]) ).
cnf(c_979,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0'))))) ),
inference(copy,[status(thm)],[c_978]) ).
cnf(c_980,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0'))))) ),
inference(copy,[status(thm)],[c_979]) ).
cnf(c_981,plain,
( 'LE'(f(A),s(s(s(s('0')))))
| 'LE'(f(A),s(s(s(s('0'))))) ),
inference(copy,[status(thm)],[c_980]) ).
cnf(c_205,plain,
'LE'(f(A),s(s(s(s('0'))))),
inference(copy,[status(thm)],[c_981]) ).
cnf(c_206,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_205,c_120]) ).
cnf(c_207,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(A)) ),
inference(resolve,[status(thm)],[c_205,c_113]) ).
cnf(c_208,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(A))) ),
inference(resolve,[status(thm)],[c_205,c_109]) ).
cnf(c_209,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_205,c_105]) ).
cnf(c_982,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(A)) ),
inference(resolve,[status(thm)],[c_86,c_208]) ).
cnf(c_983,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_982,c_207]) ).
cnf(c_227,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_983]) ).
cnf(c_984,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A))) ),
inference(resolve,[status(thm)],[c_77,c_209]) ).
cnf(c_985,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_984,c_208]) ).
cnf(c_986,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A)) ),
inference(resolve,[status(thm)],[c_985,c_227]) ).
cnf(c_987,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_986,c_207]) ).
cnf(c_988,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_987]) ).
cnf(c_989,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_988]) ).
cnf(c_312,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_989]) ).
cnf(c_990,plain,
( 'LE'(f(A),s(s(s('0'))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A)))))
| ~ 'E'(s(s(s('0'))),f(suc(A))) ),
inference(resolve,[status(thm)],[c_71,c_312]) ).
cnf(c_991,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_990,c_208]) ).
cnf(c_992,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A)) ),
inference(resolve,[status(thm)],[c_991,c_206]) ).
cnf(c_993,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_992,c_207]) ).
cnf(c_994,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_993,c_209]) ).
cnf(c_995,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0')))) ),
inference(resolve,[status(thm)],[c_994,c_227]) ).
cnf(c_996,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0')))) ),
inference(copy,[status(thm)],[c_995]) ).
cnf(c_997,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0')))) ),
inference(copy,[status(thm)],[c_996]) ).
cnf(c_998,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0')))) ),
inference(copy,[status(thm)],[c_997]) ).
cnf(c_999,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0')))) ),
inference(copy,[status(thm)],[c_998]) ).
cnf(c_348,plain,
'LE'(f(A),s(s(s('0')))),
inference(copy,[status(thm)],[c_999]) ).
cnf(c_349,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_348,c_116]) ).
cnf(c_350,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_348,c_115]) ).
cnf(c_351,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(A))) ),
inference(resolve,[status(thm)],[c_348,c_114]) ).
cnf(c_352,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(A)) ),
inference(resolve,[status(thm)],[c_348,c_108]) ).
cnf(c_1000,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(resolve,[status(thm)],[c_90,c_351]) ).
cnf(c_1001,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_1000,c_352]) ).
cnf(c_372,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_1001]) ).
cnf(c_1002,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A)) ),
inference(resolve,[status(thm)],[c_68,c_351]) ).
cnf(c_1003,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_1002,c_352]) ).
cnf(c_1004,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_1003,c_349]) ).
cnf(c_1005,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_1004,c_372]) ).
cnf(c_1006,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_1005]) ).
cnf(c_1007,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_1006]) ).
cnf(c_410,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_1007]) ).
cnf(c_1008,plain,
( 'LE'(f(A),s(s('0')))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_98,c_351]) ).
cnf(c_1009,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_1008,c_410]) ).
cnf(c_1010,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_1009,c_349]) ).
cnf(c_1011,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| ~ 'E'(s(s('0')),f(A))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_1010,c_372]) ).
cnf(c_1012,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| ~ 'E'(s(s('0')),f(A)) ),
inference(resolve,[status(thm)],[c_1011,c_350]) ).
cnf(c_1013,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0'))) ),
inference(resolve,[status(thm)],[c_1012,c_352]) ).
cnf(c_1014,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0'))) ),
inference(copy,[status(thm)],[c_1013]) ).
cnf(c_1015,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0'))) ),
inference(copy,[status(thm)],[c_1014]) ).
cnf(c_1016,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0'))) ),
inference(copy,[status(thm)],[c_1015]) ).
cnf(c_1017,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0'))) ),
inference(copy,[status(thm)],[c_1016]) ).
cnf(c_488,plain,
'LE'(f(A),s(s('0'))),
inference(copy,[status(thm)],[c_1017]) ).
cnf(c_489,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(A))) ),
inference(resolve,[status(thm)],[c_488,c_122]) ).
cnf(c_490,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_488,c_121]) ).
cnf(c_491,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_488,c_107]) ).
cnf(c_492,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(A)) ),
inference(resolve,[status(thm)],[c_488,c_102]) ).
cnf(c_1018,plain,
( 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A))) ),
inference(resolve,[status(thm)],[c_62,c_492]) ).
cnf(c_1019,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_1018,c_489]) ).
cnf(c_508,plain,
( 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_1019]) ).
cnf(c_1020,plain,
( 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A))) ),
inference(resolve,[status(thm)],[c_88,c_508]) ).
cnf(c_1021,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_1020,c_489]) ).
cnf(c_1022,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A)) ),
inference(resolve,[status(thm)],[c_1021,c_491]) ).
cnf(c_1023,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_1022,c_492]) ).
cnf(c_1024,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_1023]) ).
cnf(c_1025,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_1024]) ).
cnf(c_572,plain,
( 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_1025]) ).
cnf(c_1026,plain,
( 'LE'(f(A),s('0'))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A))) ),
inference(resolve,[status(thm)],[c_100,c_508]) ).
cnf(c_1027,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_1026,c_489]) ).
cnf(c_1028,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(A)) ),
inference(resolve,[status(thm)],[c_1027,c_491]) ).
cnf(c_1029,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_1028,c_492]) ).
cnf(c_1030,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_1029,c_490]) ).
cnf(c_1031,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0')) ),
inference(resolve,[status(thm)],[c_1030,c_572]) ).
cnf(c_1032,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0')) ),
inference(copy,[status(thm)],[c_1031]) ).
cnf(c_1033,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0')) ),
inference(copy,[status(thm)],[c_1032]) ).
cnf(c_1034,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0')) ),
inference(copy,[status(thm)],[c_1033]) ).
cnf(c_1035,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0')) ),
inference(copy,[status(thm)],[c_1034]) ).
cnf(c_768,plain,
'LE'(f(A),s('0')),
inference(copy,[status(thm)],[c_1035]) ).
cnf(c_769,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_768,c_117]) ).
cnf(c_770,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_768,c_111]) ).
cnf(c_771,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(A)) ),
inference(resolve,[status(thm)],[c_768,c_110]) ).
cnf(c_772,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(A))) ),
inference(resolve,[status(thm)],[c_768,c_101]) ).
cnf(c_776,plain,
'E'('0',f(z)),
inference(resolve,[status(thm)],[c_771,c_104]) ).
cnf(c_782,plain,
'E'('0',f(suc(suc(suc(z))))),
inference(resolve,[status(thm)],[c_769,c_104]) ).
cnf(c_789,plain,
'E'('0',f(suc(z))),
inference(resolve,[status(thm)],[c_772,c_104]) ).
cnf(c_1036,plain,
( 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(suc(z))) ),
inference(resolve,[status(thm)],[c_94,c_776]) ).
cnf(c_1037,plain,
( 'LE'(f(z),'0')
| 'E'(f(z),f(suc(z))) ),
inference(resolve,[status(thm)],[c_1036,c_772]) ).
cnf(c_790,plain,
'E'(f(z),f(suc(z))),
inference(resolve,[status(thm)],[c_104,c_1037]) ).
cnf(c_1038,plain,
( 'LE'(f(A),'0')
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A))) ),
inference(resolve,[status(thm)],[c_94,c_771]) ).
cnf(c_1039,plain,
( 'LE'(f(A),'0')
| 'LE'(f(A),'0')
| 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_1038,c_772]) ).
cnf(c_792,plain,
( 'LE'(f(A),'0')
| 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_1039]) ).
cnf(c_1040,plain,
( ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z))) ),
inference(resolve,[status(thm)],[c_782,c_75]) ).
cnf(c_1041,plain,
( ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z)))) ),
inference(resolve,[status(thm)],[c_790,c_1040]) ).
cnf(c_1042,plain,
( ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z)))) ),
inference(resolve,[status(thm)],[c_776,c_1041]) ).
cnf(c_817,plain,
( ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z)))) ),
inference(resolve,[status(thm)],[c_789,c_1042]) ).
cnf(c_825,plain,
'E'('0',f(suc(suc(z)))),
inference(resolve,[status(thm)],[c_770,c_104]) ).
cnf(c_1043,plain,
( 'LE'(f(A),'0')
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A))) ),
inference(resolve,[status(thm)],[c_66,c_770]) ).
cnf(c_1044,plain,
( 'LE'(f(z),'0')
| 'E'(f(z),f(suc(suc(z))))
| ~ 'E'('0',f(z))
| ~ 'E'(f(z),f(suc(z))) ),
inference(resolve,[status(thm)],[c_1043,c_789]) ).
cnf(c_1045,plain,
( 'LE'(f(z),'0')
| 'LE'(f(z),'0')
| 'E'(f(z),f(suc(suc(z))))
| ~ 'E'('0',f(z)) ),
inference(resolve,[status(thm)],[c_1044,c_792]) ).
cnf(c_1046,plain,
( 'LE'(f(z),'0')
| 'LE'(f(z),'0')
| 'E'(f(z),f(suc(suc(z)))) ),
inference(resolve,[status(thm)],[c_1045,c_776]) ).
cnf(c_1047,plain,
( 'LE'(f(z),'0')
| 'E'(f(z),f(suc(suc(z)))) ),
inference(copy,[status(thm)],[c_1046]) ).
cnf(c_834,plain,
'E'(f(z),f(suc(suc(z)))),
inference(resolve,[status(thm)],[c_104,c_1047]) ).
cnf(c_1048,plain,
~ 'E'(f(z),f(suc(suc(z)))),
inference(resolve,[status(thm)],[c_825,c_817]) ).
cnf(c_838,plain,
$false,
inference(resolve,[status(thm)],[c_834,c_1048]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO686-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n007.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 : Sat Sep 26 19:43:39 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 336554 was started by sandbox on n007,
% 0.11/0.37 % Sat Sep 26 19:43:39 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/0.38
% 0.14/0.38 % From the command line: assign(max_seconds, 300).
% 61.65/9.32
% 61.65/9.32 % SZS status Unsatisfiable for theBenchmark
% 61.65/9.32
% 61.65/9.32 % Proof 1 at 2.29 (+ 0.26) seconds.
% 61.65/9.32 % Length of proof is 123.
% 61.65/9.32 % Level of proof is 22.
% 61.65/9.32 % Maximum clause weight is 83.000.
% 61.65/9.32 % Given clauses 86.
% 61.65/9.32
% 61.65/9.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------