%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYO669-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:11 AM UTC 2026
% Result : Unsatisfiable 79.16s 10.47s
% Output : CNFRefutation 79.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 32
% Syntax : Number of formulae : 233 ( 14 unt; 0 def)
% Number of atoms : 1541 ( 0 equ)
% Maximal formula atoms : 18 ( 6 avg)
% Number of connectives : 2423 (1115 ~;1308 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 7 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 232 ( 3 sgn 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clause_246,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_246) ).
cnf(c_2,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_246]) ).
fof(clause_257,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| ~ 'E'(s('0'),f(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s('0'),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(s('0'),f(suc(suc(VAR_0))))
| ~ 'E'(s('0'),f(suc(VAR_0)))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0)))) ),
file('theBenchmark.p',clause_257) ).
cnf(c_3,plain,
( iLEQ(suc(A),suc(A))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(clausify,[status(thm)],[clause_257]) ).
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_4,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_106,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)))
| ~ iLEQ(suc(VAR_1),suc(VAR_0))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'('0',f(suc(VAR_1)))
| ~ 'E'('0',f(suc(suc(VAR_1))))
| ~ 'E'('0',f(VAR_1))
| ~ 'E'('0',f(VAR_0))
| ~ 'E'('0',f(suc(suc(VAR_0))))
| ~ 'E'('0',f(suc(VAR_0))) ),
file('theBenchmark.p',clause_106) ).
cnf(c_6,plain,
( 'E'(f(A),f(suc(suc(A))))
| 'E'(f(B),f(suc(suc(B))))
| ~ 'E'(f(A),f(suc(A)))
| ~ iLEQ(suc(B),suc(A))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'('0',f(suc(B)))
| ~ 'E'('0',f(suc(suc(B))))
| ~ 'E'('0',f(B))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(A))) ),
inference(clausify,[status(thm)],[clause_106]) ).
fof(clause_267,axiom,
! [VAR_0] :
( iLEQ(suc(VAR_0),suc(VAR_0))
| ~ 'E'(s(s('0')),f(suc(suc(VAR_0))))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(s(s('0')),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(VAR_0)) ),
file('theBenchmark.p',clause_267) ).
cnf(c_7,plain,
( iLEQ(suc(A),suc(A))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(clausify,[status(thm)],[clause_267]) ).
fof(clause_25,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_25) ).
cnf(c_9,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_25]) ).
fof(clause_295,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(suc(suc(VAR_0))))
| ~ 'E'('0',f(VAR_0))
| ~ 'E'('0',f(suc(suc(suc(VAR_0)))))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0)))) ),
file('theBenchmark.p',clause_295) ).
cnf(c_11,plain,
( iLEQ(suc(A),suc(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(clausify,[status(thm)],[clause_295]) ).
fof(clause_144,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ iLEQ(suc(VAR_0),suc(VAR_1))
| ~ 'E'(s('0'),f(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(s('0'),f(suc(suc(VAR_0))))
| ~ 'E'(s('0'),f(suc(VAR_1)))
| ~ 'E'(s('0'),f(suc(suc(VAR_1))))
| ~ 'E'(s('0'),f(VAR_1))
| ~ 'E'(s('0'),f(suc(VAR_0))) ),
file('theBenchmark.p',clause_144) ).
cnf(c_13,plain,
( 'E'(f(B),f(suc(suc(B))))
| 'E'(f(A),f(suc(suc(A))))
| ~ iLEQ(suc(A),suc(B))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(B)))
| ~ 'E'(s('0'),f(suc(suc(B))))
| ~ 'E'(s('0'),f(B))
| ~ 'E'(s('0'),f(suc(A))) ),
inference(clausify,[status(thm)],[clause_144]) ).
fof(clause_292,axiom,
! [VAR_0,VAR_1] :
( ~ iLEQ(suc(VAR_0),suc(VAR_1))
| ~ 'E'(s('0'),f(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s('0'),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(s('0'),f(suc(suc(suc(VAR_1)))))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(s('0'),f(suc(suc(VAR_0))))
| ~ 'E'(s('0'),f(suc(VAR_1)))
| ~ 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| ~ 'E'(s('0'),f(suc(suc(VAR_1))))
| ~ 'E'(s('0'),f(VAR_1))
| ~ 'E'(s('0'),f(suc(VAR_0)))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0)))) ),
file('theBenchmark.p',clause_292) ).
cnf(c_14,plain,
( ~ iLEQ(suc(A),suc(B))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(suc(B)))))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(B)))
| ~ 'E'(f(B),f(suc(suc(B))))
| ~ 'E'(s('0'),f(suc(suc(B))))
| ~ 'E'(s('0'),f(B))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(clausify,[status(thm)],[clause_292]) ).
fof(clause_7,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_1),f(suc(VAR_1)))
| 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ iLEQ(suc(VAR_0),suc(VAR_1))
| ~ 'E'(s('0'),f(VAR_0))
| ~ 'E'(s('0'),f(suc(VAR_1)))
| ~ 'E'(s('0'),f(VAR_1))
| ~ 'E'(s('0'),f(suc(VAR_0))) ),
file('theBenchmark.p',clause_7) ).
cnf(c_16,plain,
( 'E'(f(B),f(suc(B)))
| 'E'(f(A),f(suc(A)))
| ~ iLEQ(suc(A),suc(B))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(B)))
| ~ 'E'(s('0'),f(B))
| ~ 'E'(s('0'),f(suc(A))) ),
inference(clausify,[status(thm)],[clause_7]) ).
fof(clause_100,axiom,
! [VAR_0,VAR_1] :
( ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ iLEQ(suc(VAR_1),suc(VAR_0))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'('0',f(suc(VAR_1)))
| ~ 'E'('0',f(suc(suc(VAR_1))))
| ~ 'E'('0',f(VAR_1))
| ~ 'E'('0',f(suc(suc(suc(VAR_1)))))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| ~ 'E'('0',f(VAR_0))
| ~ 'E'('0',f(suc(suc(VAR_0))))
| ~ 'E'('0',f(suc(suc(suc(VAR_0)))))
| ~ 'E'('0',f(suc(VAR_0))) ),
file('theBenchmark.p',clause_100) ).
cnf(c_17,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ iLEQ(suc(B),suc(A))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'('0',f(suc(B)))
| ~ 'E'('0',f(suc(suc(B))))
| ~ 'E'('0',f(B))
| ~ 'E'('0',f(suc(suc(suc(B)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(B),f(suc(suc(B))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(clausify,[status(thm)],[clause_100]) ).
fof(clause_44,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_44) ).
cnf(c_20,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_44]) ).
fof(clause_248,axiom,
! [VAR_0,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'('0',f(suc(VAR_1)))
| ~ 'E'('0',f(VAR_1))
| ~ 'E'('0',f(VAR_0))
| ~ 'E'('0',f(suc(VAR_0))) ),
file('theBenchmark.p',clause_248) ).
cnf(c_22,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(B),f(suc(B)))
| ~ iLEQ(suc(B),suc(A))
| ~ 'E'('0',f(suc(B)))
| ~ 'E'('0',f(B))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A))) ),
inference(clausify,[status(thm)],[clause_248]) ).
fof(clause_122,axiom,
! [VAR_0,VAR_1] :
( ~ 'E'(s(s('0')),f(VAR_1))
| ~ 'E'(s(s('0')),f(suc(suc(VAR_0))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(VAR_1)))))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(suc(VAR_1)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'(s(s('0')),f(suc(suc(VAR_1))))
| ~ iLEQ(suc(VAR_0),suc(VAR_1))
| ~ 'E'(f(VAR_1),f(suc(suc(VAR_1))))
| ~ 'E'(s(s('0')),f(suc(VAR_0)))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(s(s('0')),f(VAR_0)) ),
file('theBenchmark.p',clause_122) ).
cnf(c_23,plain,
( ~ 'E'(s(s('0')),f(B))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(B)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(B)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(B))))
| ~ iLEQ(suc(A),suc(B))
| ~ 'E'(f(B),f(suc(suc(B))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(clausify,[status(thm)],[clause_122]) ).
fof(clause_76,axiom,
! [VAR_0,VAR_1] :
( 'E'(f(VAR_1),f(suc(VAR_1)))
| 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(VAR_1))
| ~ 'E'(s(s('0')),f(suc(VAR_1)))
| ~ iLEQ(suc(VAR_0),suc(VAR_1))
| ~ 'E'(s(s('0')),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(VAR_0)) ),
file('theBenchmark.p',clause_76) ).
cnf(c_24,plain,
( 'E'(f(B),f(suc(B)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(B))
| ~ 'E'(s(s('0')),f(suc(B)))
| ~ iLEQ(suc(A),suc(B))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(clausify,[status(thm)],[clause_76]) ).
fof(clause_143,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_143) ).
cnf(c_26,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_143]) ).
fof(clause_72,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_72) ).
cnf(c_28,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_72]) ).
fof(clause_74,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(s('0')),f(VAR_1))
| ~ 'E'(s(s('0')),f(suc(suc(VAR_0))))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(suc(VAR_1)))
| ~ 'E'(s(s('0')),f(suc(suc(VAR_1))))
| ~ iLEQ(suc(VAR_0),suc(VAR_1))
| ~ 'E'(s(s('0')),f(suc(VAR_0)))
| ~ 'E'(f(VAR_1),f(suc(VAR_1)))
| ~ 'E'(s(s('0')),f(VAR_0)) ),
file('theBenchmark.p',clause_74) ).
cnf(c_32,plain,
( 'E'(f(B),f(suc(suc(B))))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(B))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(B)))
| ~ 'E'(s(s('0')),f(suc(suc(B))))
| ~ iLEQ(suc(A),suc(B))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(B),f(suc(B)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(clausify,[status(thm)],[clause_74]) ).
cnf(c_37,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(A))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(resolve,[status(thm)],[c_32,c_2]) ).
cnf(c_447,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(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(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_37]) ).
cnf(c_448,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(A))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_447]) ).
cnf(c_449,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(A))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_448]) ).
cnf(c_450,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(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_449]) ).
cnf(c_451,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'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_450]) ).
cnf(c_452,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'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_451]) ).
cnf(c_453,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'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_452]) ).
cnf(c_454,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(A))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_453]) ).
cnf(c_455,plain,
( '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(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_454]) ).
cnf(c_38,plain,
( 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_455]) ).
cnf(c_39,plain,
( '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'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(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(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(resolve,[status(thm)],[c_28,c_13]) ).
cnf(c_456,plain,
( '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'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(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(copy,[status(thm)],[c_39]) ).
cnf(c_457,plain,
( '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'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(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'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_456]) ).
cnf(c_458,plain,
( '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'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(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(copy,[status(thm)],[c_457]) ).
cnf(c_459,plain,
( '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'(f(A),f(suc(A)))
| ~ 'E'(s('0'),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)))) ),
inference(copy,[status(thm)],[c_458]) ).
cnf(c_460,plain,
( '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'(f(A),f(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(copy,[status(thm)],[c_459]) ).
cnf(c_461,plain,
( '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'(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(copy,[status(thm)],[c_460]) ).
cnf(c_462,plain,
( 'E'(f(A),f(suc(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(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_461]) ).
cnf(c_463,plain,
( 'E'(f(A),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)))) ),
inference(copy,[status(thm)],[c_462]) ).
cnf(c_464,plain,
( '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)))) ),
inference(copy,[status(thm)],[c_463]) ).
cnf(c_40,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)))) ),
inference(copy,[status(thm)],[c_464]) ).
cnf(c_41,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(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(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(resolve,[status(thm)],[c_26,c_6]) ).
cnf(c_465,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(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(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_41]) ).
cnf(c_466,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(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(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_465]) ).
cnf(c_467,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(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(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_466]) ).
cnf(c_468,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(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_467]) ).
cnf(c_469,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(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_468]) ).
cnf(c_470,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(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_469]) ).
cnf(c_471,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_470]) ).
cnf(c_472,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_471]) ).
cnf(c_473,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_472]) ).
cnf(c_42,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_473]) ).
cnf(c_44,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(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(resolve,[status(thm)],[c_24,c_9]) ).
cnf(c_474,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)) ),
inference(copy,[status(thm)],[c_44]) ).
cnf(c_475,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(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_474]) ).
cnf(c_476,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(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_475]) ).
cnf(c_477,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(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_476]) ).
cnf(c_478,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_477]) ).
cnf(c_45,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_478]) ).
cnf(c_46,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(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(A))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(resolve,[status(thm)],[c_23,c_7]) ).
cnf(c_479,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(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(A))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_46]) ).
cnf(c_480,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(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(A))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_479]) ).
cnf(c_481,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(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(A))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_480]) ).
cnf(c_482,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(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(A))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_481]) ).
cnf(c_483,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(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'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_482]) ).
cnf(c_484,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(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'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_483]) ).
cnf(c_485,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_484]) ).
cnf(c_486,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_485]) ).
cnf(c_487,plain,
( ~ 'E'(s(s('0')),f(suc(suc(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(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_486]) ).
cnf(c_488,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_487]) ).
cnf(c_489,plain,
( ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_488]) ).
cnf(c_47,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(copy,[status(thm)],[c_489]) ).
cnf(c_48,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))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A))) ),
inference(resolve,[status(thm)],[c_22,c_4]) ).
cnf(c_490,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))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_48]) ).
cnf(c_491,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))) ),
inference(copy,[status(thm)],[c_490]) ).
cnf(c_492,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(A))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_491]) ).
cnf(c_493,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_492]) ).
cnf(c_494,plain,
( 'E'(f(A),f(suc(A)))
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_493]) ).
cnf(c_49,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_494]) ).
cnf(c_51,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_20,c_16]) ).
cnf(c_495,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_51]) ).
cnf(c_496,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_495]) ).
cnf(c_497,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_496]) ).
cnf(c_498,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_497]) ).
cnf(c_499,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_498]) ).
cnf(c_52,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A)) ),
inference(copy,[status(thm)],[c_499]) ).
cnf(c_53,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(resolve,[status(thm)],[c_17,c_11]) ).
cnf(c_500,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_53]) ).
cnf(c_501,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_500]) ).
cnf(c_502,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_501]) ).
cnf(c_503,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_502]) ).
cnf(c_504,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_503]) ).
cnf(c_505,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(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'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_504]) ).
cnf(c_506,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_505]) ).
cnf(c_507,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_506]) ).
cnf(c_508,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(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'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_507]) ).
cnf(c_509,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_508]) ).
cnf(c_510,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_509]) ).
cnf(c_54,plain,
( ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(A))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'('0',f(suc(A))) ),
inference(copy,[status(thm)],[c_510]) ).
cnf(c_57,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(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(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_14,c_3]) ).
cnf(c_511,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(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(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(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(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_57]) ).
cnf(c_512,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(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(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_511]) ).
cnf(c_513,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(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(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_512]) ).
cnf(c_514,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(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(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_513]) ).
cnf(c_515,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(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(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_514]) ).
cnf(c_516,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),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'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_515]) ).
cnf(c_517,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_516]) ).
cnf(c_518,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_517]) ).
cnf(c_519,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_518]) ).
cnf(c_520,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_519]) ).
cnf(c_521,plain,
( ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_520]) ).
cnf(c_58,plain,
( ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_521]) ).
fof(clause_263,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_263) ).
cnf(c_63,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_263]) ).
fof(clause_151,axiom,
~ 'LE'(f(z),'0'),
file('theBenchmark.p',clause_151) ).
cnf(c_64,plain,
~ 'LE'(f(z),'0'),
inference(clausify,[status(thm)],[clause_151]) ).
fof(clause_222,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_222) ).
cnf(c_65,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_222]) ).
fof(clause_196,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_196) ).
cnf(c_66,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_196]) ).
fof(clause_272,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_272) ).
cnf(c_67,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(A))
| ~ 'LE'(f(A),s(s('0'))) ),
inference(clausify,[status(thm)],[clause_272]) ).
fof(clause_153,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_153) ).
cnf(c_68,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_153]) ).
fof(clause_4,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_4) ).
cnf(c_69,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(suc(A))))
| ~ 'LE'(f(suc(suc(A))),s('0')) ),
inference(clausify,[status(thm)],[clause_4]) ).
fof(clause_260,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_260) ).
cnf(c_70,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(A)))
| ~ 'LE'(f(suc(A)),s('0')) ),
inference(clausify,[status(thm)],[clause_260]) ).
fof(clause_299,axiom,
! [VAR_0] : 'LE'(f(VAR_0),s(s(s('0')))),
file('theBenchmark.p',clause_299) ).
cnf(c_71,plain,
'LE'(f(A),s(s(s('0')))),
inference(clausify,[status(thm)],[clause_299]) ).
fof(clause_12,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_12) ).
cnf(c_72,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(A)))
| ~ 'LE'(f(suc(A)),s(s('0'))) ),
inference(clausify,[status(thm)],[clause_12]) ).
fof(clause_18,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),'0')
| 'E'('0',f(VAR_0))
| ~ 'LE'(f(VAR_0),s('0')) ),
file('theBenchmark.p',clause_18) ).
cnf(c_73,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(A))
| ~ 'LE'(f(A),s('0')) ),
inference(clausify,[status(thm)],[clause_18]) ).
fof(clause_207,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_207) ).
cnf(c_74,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_207]) ).
fof(clause_301,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_301) ).
cnf(c_75,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_301]) ).
cnf(c_76,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_71,c_75]) ).
fof(clause_88,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_88) ).
cnf(c_77,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_88]) ).
cnf(c_78,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_71,c_77]) ).
cnf(c_79,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(A))) ),
inference(resolve,[status(thm)],[c_71,c_68]) ).
cnf(c_80,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(A)) ),
inference(resolve,[status(thm)],[c_71,c_65]) ).
cnf(c_522,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(resolve,[status(thm)],[c_45,c_80]) ).
cnf(c_523,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_522,c_79]) ).
cnf(c_118,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_523]) ).
cnf(c_524,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_38,c_80]) ).
cnf(c_525,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(resolve,[status(thm)],[c_524,c_118]) ).
cnf(c_526,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'(s(s('0')),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_525,c_79]) ).
cnf(c_527,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_526,c_76]) ).
cnf(c_528,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_527]) ).
cnf(c_529,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_528]) ).
cnf(c_132,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_529]) ).
cnf(c_530,plain,
( 'LE'(f(A),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_47,c_80]) ).
cnf(c_531,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(suc(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_530,c_118]) ).
cnf(c_532,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A))))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_531,c_79]) ).
cnf(c_533,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(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_532,c_132]) ).
cnf(c_534,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(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_533,c_76]) ).
cnf(c_535,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_534,c_78]) ).
cnf(c_536,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_535]) ).
cnf(c_537,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_536]) ).
cnf(c_538,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0'))) ),
inference(copy,[status(thm)],[c_537]) ).
cnf(c_539,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0'))) ),
inference(copy,[status(thm)],[c_538]) ).
cnf(c_178,plain,
'LE'(f(A),s(s('0'))),
inference(copy,[status(thm)],[c_539]) ).
cnf(c_179,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(A))) ),
inference(resolve,[status(thm)],[c_178,c_72]) ).
cnf(c_180,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(A)) ),
inference(resolve,[status(thm)],[c_178,c_67]) ).
cnf(c_181,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_178,c_66]) ).
cnf(c_182,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_178,c_63]) ).
cnf(c_540,plain,
( 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A))) ),
inference(resolve,[status(thm)],[c_52,c_180]) ).
cnf(c_541,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_540,c_179]) ).
cnf(c_198,plain,
( 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_541]) ).
cnf(c_542,plain,
( 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A))) ),
inference(resolve,[status(thm)],[c_40,c_181]) ).
cnf(c_543,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_542,c_179]) ).
cnf(c_544,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_543,c_198]) ).
cnf(c_545,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_544,c_180]) ).
cnf(c_546,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_545]) ).
cnf(c_547,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_546]) ).
cnf(c_247,plain,
( 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_547]) ).
cnf(c_548,plain,
( 'LE'(f(A),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(s('0'),f(suc(A))) ),
inference(resolve,[status(thm)],[c_58,c_247]) ).
cnf(c_549,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A)) ),
inference(resolve,[status(thm)],[c_548,c_179]) ).
cnf(c_550,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_549,c_180]) ).
cnf(c_551,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_550,c_181]) ).
cnf(c_552,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'(s('0'),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_551,c_198]) ).
cnf(c_553,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_552,c_182]) ).
cnf(c_554,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_553]) ).
cnf(c_555,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_554]) ).
cnf(c_556,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0')) ),
inference(copy,[status(thm)],[c_555]) ).
cnf(c_557,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0')) ),
inference(copy,[status(thm)],[c_556]) ).
cnf(c_381,plain,
'LE'(f(A),s('0')),
inference(copy,[status(thm)],[c_557]) ).
cnf(c_382,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_381,c_74]) ).
cnf(c_383,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(A)) ),
inference(resolve,[status(thm)],[c_381,c_73]) ).
cnf(c_384,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(A))) ),
inference(resolve,[status(thm)],[c_381,c_70]) ).
cnf(c_385,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_381,c_69]) ).
cnf(c_389,plain,
'E'('0',f(z)),
inference(resolve,[status(thm)],[c_383,c_64]) ).
cnf(c_395,plain,
'E'('0',f(suc(z))),
inference(resolve,[status(thm)],[c_384,c_64]) ).
cnf(c_558,plain,
( 'LE'(f(A),'0')
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A)) ),
inference(resolve,[status(thm)],[c_49,c_384]) ).
cnf(c_559,plain,
( 'LE'(f(z),'0')
| 'E'(f(z),f(suc(z))) ),
inference(resolve,[status(thm)],[c_558,c_389]) ).
cnf(c_398,plain,
'E'(f(z),f(suc(z))),
inference(resolve,[status(thm)],[c_64,c_559]) ).
cnf(c_560,plain,
( 'LE'(f(A),'0')
| 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(A)) ),
inference(resolve,[status(thm)],[c_49,c_384]) ).
cnf(c_561,plain,
( 'LE'(f(A),'0')
| 'LE'(f(A),'0')
| 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_560,c_383]) ).
cnf(c_399,plain,
( 'LE'(f(A),'0')
| 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_561]) ).
cnf(c_409,plain,
'E'('0',f(suc(suc(suc(z))))),
inference(resolve,[status(thm)],[c_382,c_64]) ).
cnf(c_562,plain,
( ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(resolve,[status(thm)],[c_409,c_54]) ).
cnf(c_563,plain,
( ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z)))) ),
inference(resolve,[status(thm)],[c_395,c_562]) ).
cnf(c_564,plain,
( ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z)))) ),
inference(resolve,[status(thm)],[c_389,c_563]) ).
cnf(c_424,plain,
( ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z)))) ),
inference(resolve,[status(thm)],[c_398,c_564]) ).
cnf(c_433,plain,
'E'('0',f(suc(suc(z)))),
inference(resolve,[status(thm)],[c_385,c_64]) ).
cnf(c_565,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_42,c_385]) ).
cnf(c_566,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_565,c_395]) ).
cnf(c_567,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_566,c_399]) ).
cnf(c_568,plain,
( 'LE'(f(z),'0')
| 'LE'(f(z),'0')
| 'E'(f(z),f(suc(suc(z)))) ),
inference(resolve,[status(thm)],[c_567,c_389]) ).
cnf(c_569,plain,
( 'LE'(f(z),'0')
| 'E'(f(z),f(suc(suc(z)))) ),
inference(copy,[status(thm)],[c_568]) ).
cnf(c_442,plain,
'E'(f(z),f(suc(suc(z)))),
inference(resolve,[status(thm)],[c_64,c_569]) ).
cnf(c_570,plain,
~ 'E'(f(z),f(suc(suc(z)))),
inference(resolve,[status(thm)],[c_433,c_424]) ).
cnf(c_446,plain,
$false,
inference(resolve,[status(thm)],[c_442,c_570]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO669-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n013.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sat Sep 26 19:43:51 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.38 % Process 3465380 was started by sandbox2 on n013,
% 0.11/0.38 % Sat Sep 26 19:43:51 2026
% 0.11/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.39
% 0.11/0.39 % From the command line: assign(max_seconds, 300).
% 79.16/10.47
% 79.16/10.47 % SZS status Unsatisfiable for theBenchmark
% 79.16/10.47
% 79.16/10.47 % Proof 1 at 1.87 (+ 0.05) seconds.
% 79.16/10.47 % Length of proof is 77.
% 79.16/10.47 % Level of proof is 14.
% 79.16/10.47 % Maximum clause weight is 59.000.
% 79.16/10.47 % Given clauses 51.
% 79.16/10.47
% 79.16/10.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------