%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYO675-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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:51:12 AM UTC 2026
% Result : Unsatisfiable 14.89s 2.35s
% Output : CNFRefutation 14.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 30
% Syntax : Number of formulae : 156 ( 15 unt; 0 def)
% Number of atoms : 543 ( 0 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 605 ( 218 ~; 387 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 137 ( 4 sgn 29 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clause_11,axiom,
! [VAR_0] :
( ~ 'E'('0',f(VAR_0))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0))))
| ~ 'E'('0',f(suc(VAR_0)))
| ~ 'E'('0',f(suc(suc(VAR_0))))
| ~ 'E'('0',f(suc(suc(suc(VAR_0)))))
| ~ 'E'(f(VAR_0),f(suc(VAR_0))) ),
file('theBenchmark.p',clause_11) ).
cnf(c_1,plain,
( ~ 'E'('0',f(A))
| ~ 'E'(f(A),f(suc(suc(A))))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(suc(suc(A))))
| ~ 'E'('0',f(suc(suc(suc(A)))))
| ~ 'E'(f(A),f(suc(A))) ),
inference(clausify,[status(thm)],[clause_11]) ).
fof(clause_27,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_27) ).
cnf(c_2,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_27]) ).
fof(clause_20,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_20) ).
cnf(c_3,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_20]) ).
fof(clause_31,axiom,
! [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_31) ).
cnf(c_4,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(clausify,[status(thm)],[clause_31]) ).
fof(clause_10,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_10) ).
cnf(c_5,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_10]) ).
fof(clause_23,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_23) ).
cnf(c_6,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(A)))
| ~ 'LE'(f(suc(A)),s('0')) ),
inference(clausify,[status(thm)],[clause_23]) ).
fof(clause_26,axiom,
! [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_26) ).
cnf(c_7,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(s(s('0')),f(A)) ),
inference(clausify,[status(thm)],[clause_26]) ).
fof(clause_29,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_29) ).
cnf(c_8,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_29]) ).
fof(clause_14,axiom,
! [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_14) ).
cnf(c_9,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'('0',f(suc(A)))
| ~ 'E'('0',f(A)) ),
inference(clausify,[status(thm)],[clause_14]) ).
fof(clause_25,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_25) ).
cnf(c_10,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(A)))
| ~ 'LE'(f(suc(A)),s(s('0'))) ),
inference(clausify,[status(thm)],[clause_25]) ).
fof(clause_18,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_18) ).
cnf(c_11,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_18]) ).
fof(clause_19,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_19) ).
cnf(c_12,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_19]) ).
fof(clause_24,axiom,
! [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_24) ).
cnf(c_13,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)))) ),
inference(clausify,[status(thm)],[clause_24]) ).
fof(clause_2,axiom,
! [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_2) ).
cnf(c_14,plain,
( '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_2]) ).
fof(clause_37,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_37) ).
cnf(c_15,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(suc(A))))
| ~ 'LE'(f(suc(suc(A))),s('0')) ),
inference(clausify,[status(thm)],[clause_37]) ).
fof(clause_13,axiom,
! [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_13) ).
cnf(c_16,plain,
( 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A)))
| ~ 'E'(s('0'),f(A)) ),
inference(clausify,[status(thm)],[clause_13]) ).
fof(clause_17,axiom,
! [VAR_0] :
( ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(VAR_0)))))
| ~ 'E'(s(s('0')),f(VAR_0))
| ~ 'E'(s(s('0')),f(suc(suc(VAR_0))))
| ~ 'E'(s(s('0')),f(suc(VAR_0)))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0)))) ),
file('theBenchmark.p',clause_17) ).
cnf(c_17,plain,
( ~ '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(A))))
| ~ 'E'(s(s('0')),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(clausify,[status(thm)],[clause_17]) ).
fof(clause_21,axiom,
~ 'LE'(f(z),'0'),
file('theBenchmark.p',clause_21) ).
cnf(c_18,plain,
~ 'LE'(f(z),'0'),
inference(clausify,[status(thm)],[clause_21]) ).
fof(clause_1,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_1) ).
cnf(c_19,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_1]) ).
fof(clause_36,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_36) ).
cnf(c_20,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_36]) ).
fof(clause_15,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_15) ).
cnf(c_21,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_15]) ).
fof(clause_5,axiom,
! [VAR_0] :
( ~ 'E'(s('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(suc(VAR_0)))))
| ~ 'E'(f(VAR_0),f(suc(suc(VAR_0)))) ),
file('theBenchmark.p',clause_5) ).
cnf(c_22,plain,
( ~ 'E'(s('0'),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(suc(A)))))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(clausify,[status(thm)],[clause_5]) ).
fof(clause_4,axiom,
! [VAR_0] :
( 'LE'(f(VAR_0),'0')
| 'E'('0',f(VAR_0))
| ~ 'LE'(f(VAR_0),s('0')) ),
file('theBenchmark.p',clause_4) ).
cnf(c_23,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(A))
| ~ 'LE'(f(A),s('0')) ),
inference(clausify,[status(thm)],[clause_4]) ).
fof(clause_8,axiom,
! [VAR_0] :
( ~ 'E'(s(s(s('0'))),f(suc(VAR_0)))
| ~ 'E'(f(VAR_0),f(suc(VAR_0)))
| ~ 'E'(f(VAR_0),f(suc(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))))) ),
file('theBenchmark.p',clause_8) ).
cnf(c_24,plain,
( ~ '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(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(A))))) ),
inference(clausify,[status(thm)],[clause_8]) ).
fof(clause_32,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_32) ).
cnf(c_25,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_32]) ).
fof(clause_16,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_16) ).
cnf(c_26,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(A))
| ~ 'LE'(f(A),s(s('0'))) ),
inference(clausify,[status(thm)],[clause_16]) ).
fof(clause_7,axiom,
! [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_7) ).
cnf(c_27,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(clausify,[status(thm)],[clause_7]) ).
fof(clause_6,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_6) ).
cnf(c_28,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_6]) ).
fof(clause_34,axiom,
! [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_34) ).
cnf(c_29,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(clausify,[status(thm)],[clause_34]) ).
fof(clause_30,axiom,
! [VAR_0] : 'LE'(f(VAR_0),s(s(s(s('0'))))),
file('theBenchmark.p',clause_30) ).
cnf(c_30,plain,
'LE'(f(A),s(s(s(s('0'))))),
inference(clausify,[status(thm)],[clause_30]) ).
cnf(c_31,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_30,c_28]) ).
cnf(c_32,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(A))) ),
inference(resolve,[status(thm)],[c_30,c_25]) ).
cnf(c_33,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(A)) ),
inference(resolve,[status(thm)],[c_30,c_20]) ).
cnf(c_34,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_30,c_19]) ).
cnf(c_517,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s(s('0'))),f(suc(A))) ),
inference(resolve,[status(thm)],[c_14,c_33]) ).
cnf(c_518,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_517,c_32]) ).
cnf(c_63,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_518]) ).
cnf(c_519,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_4,c_34]) ).
cnf(c_520,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_519,c_32]) ).
cnf(c_521,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_520,c_63]) ).
cnf(c_522,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_521,c_33]) ).
cnf(c_523,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_522]) ).
cnf(c_524,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_523]) ).
cnf(c_88,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_524]) ).
cnf(c_525,plain,
( 'LE'(f(A),s(s(s('0'))))
| ~ '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(suc(suc(A))))
| ~ 'E'(s(s(s('0'))),f(A)) ),
inference(resolve,[status(thm)],[c_24,c_31]) ).
cnf(c_526,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| ~ '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(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_525,c_33]) ).
cnf(c_527,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(f(A),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_526,c_34]) ).
cnf(c_528,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'(s(s(s('0'))),f(suc(A)))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_527,c_88]) ).
cnf(c_529,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'(s(s(s('0'))),f(suc(A))) ),
inference(resolve,[status(thm)],[c_528,c_63]) ).
cnf(c_530,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_529,c_32]) ).
cnf(c_531,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_530]) ).
cnf(c_532,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_531]) ).
cnf(c_533,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_532]) ).
cnf(c_534,plain,
( 'LE'(f(A),s(s(s('0'))))
| 'LE'(f(A),s(s(s('0')))) ),
inference(copy,[status(thm)],[c_533]) ).
cnf(c_105,plain,
'LE'(f(A),s(s(s('0')))),
inference(copy,[status(thm)],[c_534]) ).
cnf(c_106,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(A))) ),
inference(resolve,[status(thm)],[c_105,c_12]) ).
cnf(c_107,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_105,c_11]) ).
cnf(c_108,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(A)) ),
inference(resolve,[status(thm)],[c_105,c_8]) ).
cnf(c_109,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_105,c_5]) ).
cnf(c_535,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_7,c_108]) ).
cnf(c_536,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_535,c_106]) ).
cnf(c_125,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_536]) ).
cnf(c_537,plain,
( 'LE'(f(A),s(s('0')))
| '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))) ),
inference(resolve,[status(thm)],[c_13,c_107]) ).
cnf(c_538,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(A))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_537,c_106]) ).
cnf(c_539,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(A)) ),
inference(resolve,[status(thm)],[c_538,c_125]) ).
cnf(c_540,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_539,c_108]) ).
cnf(c_541,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_540]) ).
cnf(c_542,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_541]) ).
cnf(c_150,plain,
( 'LE'(f(A),s(s('0')))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_542]) ).
cnf(c_543,plain,
( 'LE'(f(A),s(s('0')))
| ~ '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(A))))
| ~ 'E'(s(s('0')),f(suc(A))) ),
inference(resolve,[status(thm)],[c_17,c_150]) ).
cnf(c_544,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| ~ '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(A)))) ),
inference(resolve,[status(thm)],[c_543,c_106]) ).
cnf(c_545,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| ~ 'E'(f(A),f(suc(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A)))))
| ~ 'E'(s(s('0')),f(A)) ),
inference(resolve,[status(thm)],[c_544,c_107]) ).
cnf(c_546,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(A)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_545,c_108]) ).
cnf(c_547,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'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_546,c_109]) ).
cnf(c_548,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_547,c_125]) ).
cnf(c_549,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_548]) ).
cnf(c_550,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_549]) ).
cnf(c_551,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0'))) ),
inference(copy,[status(thm)],[c_550]) ).
cnf(c_552,plain,
( 'LE'(f(A),s(s('0')))
| 'LE'(f(A),s(s('0'))) ),
inference(copy,[status(thm)],[c_551]) ).
cnf(c_221,plain,
'LE'(f(A),s(s('0'))),
inference(copy,[status(thm)],[c_552]) ).
cnf(c_222,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(A)) ),
inference(resolve,[status(thm)],[c_221,c_26]) ).
cnf(c_223,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_221,c_21]) ).
cnf(c_224,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(A))) ),
inference(resolve,[status(thm)],[c_221,c_10]) ).
cnf(c_225,plain,
( 'LE'(f(A),s('0'))
| 'E'(s('0'),f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_221,c_2]) ).
cnf(c_553,plain,
( 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(A)))
| ~ 'E'(s('0'),f(suc(A))) ),
inference(resolve,[status(thm)],[c_16,c_222]) ).
cnf(c_554,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_553,c_224]) ).
cnf(c_242,plain,
( 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(A))) ),
inference(copy,[status(thm)],[c_554]) ).
cnf(c_555,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_29,c_225]) ).
cnf(c_556,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_555,c_224]) ).
cnf(c_557,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_556,c_242]) ).
cnf(c_558,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_557,c_222]) ).
cnf(c_559,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_558]) ).
cnf(c_560,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_559]) ).
cnf(c_309,plain,
( 'LE'(f(A),s('0'))
| 'E'(f(A),f(suc(suc(A)))) ),
inference(copy,[status(thm)],[c_560]) ).
cnf(c_561,plain,
( 'LE'(f(A),s('0'))
| ~ 'E'(s('0'),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(suc(A))))) ),
inference(resolve,[status(thm)],[c_22,c_309]) ).
cnf(c_562,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| ~ 'E'(s('0'),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_561,c_223]) ).
cnf(c_563,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| ~ 'E'(s('0'),f(suc(suc(A))))
| ~ 'E'(s('0'),f(A))
| ~ 'E'(f(A),f(suc(A))) ),
inference(resolve,[status(thm)],[c_562,c_224]) ).
cnf(c_564,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(A))))
| ~ 'E'(s('0'),f(A)) ),
inference(resolve,[status(thm)],[c_563,c_242]) ).
cnf(c_565,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(A)))) ),
inference(resolve,[status(thm)],[c_564,c_222]) ).
cnf(c_566,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_565,c_225]) ).
cnf(c_567,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_566]) ).
cnf(c_568,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_567]) ).
cnf(c_569,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0')) ),
inference(copy,[status(thm)],[c_568]) ).
cnf(c_570,plain,
( 'LE'(f(A),s('0'))
| 'LE'(f(A),s('0')) ),
inference(copy,[status(thm)],[c_569]) ).
cnf(c_472,plain,
'LE'(f(A),s('0')),
inference(copy,[status(thm)],[c_570]) ).
cnf(c_473,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(A)) ),
inference(resolve,[status(thm)],[c_472,c_23]) ).
cnf(c_474,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(suc(A)))) ),
inference(resolve,[status(thm)],[c_472,c_15]) ).
cnf(c_475,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(A))) ),
inference(resolve,[status(thm)],[c_472,c_6]) ).
cnf(c_476,plain,
( 'LE'(f(A),'0')
| 'E'('0',f(suc(suc(suc(A))))) ),
inference(resolve,[status(thm)],[c_472,c_3]) ).
cnf(c_480,plain,
'E'('0',f(z)),
inference(resolve,[status(thm)],[c_473,c_18]) ).
cnf(c_486,plain,
'E'('0',f(suc(suc(z)))),
inference(resolve,[status(thm)],[c_474,c_18]) ).
cnf(c_571,plain,
( 'E'(f(z),f(suc(suc(z))))
| ~ 'E'('0',f(z))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(suc(z))) ),
inference(resolve,[status(thm)],[c_486,c_27]) ).
cnf(c_490,plain,
( 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(suc(z))) ),
inference(resolve,[status(thm)],[c_480,c_571]) ).
cnf(c_498,plain,
'E'('0',f(suc(z))),
inference(resolve,[status(thm)],[c_475,c_18]) ).
cnf(c_572,plain,
( 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(suc(z))) ),
inference(resolve,[status(thm)],[c_9,c_480]) ).
cnf(c_573,plain,
( 'LE'(f(z),'0')
| 'E'(f(z),f(suc(z))) ),
inference(resolve,[status(thm)],[c_572,c_475]) ).
cnf(c_500,plain,
'E'(f(z),f(suc(z))),
inference(resolve,[status(thm)],[c_18,c_573]) ).
cnf(c_574,plain,
( 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z))) ),
inference(resolve,[status(thm)],[c_498,c_490]) ).
cnf(c_505,plain,
'E'(f(z),f(suc(suc(z)))),
inference(resolve,[status(thm)],[c_500,c_574]) ).
cnf(c_575,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z))) ),
inference(resolve,[status(thm)],[c_505,c_1]) ).
cnf(c_576,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z))))) ),
inference(resolve,[status(thm)],[c_500,c_575]) ).
cnf(c_577,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(suc(z))))) ),
inference(resolve,[status(thm)],[c_486,c_576]) ).
cnf(c_578,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(suc(z))))) ),
inference(resolve,[status(thm)],[c_498,c_577]) ).
cnf(c_509,plain,
~ 'E'('0',f(suc(suc(suc(z))))),
inference(resolve,[status(thm)],[c_480,c_578]) ).
cnf(c_579,plain,
'E'('0',f(suc(suc(suc(z))))),
inference(resolve,[status(thm)],[c_476,c_18]) ).
cnf(c_516,plain,
$false,
inference(resolve,[status(thm)],[c_509,c_579]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO675-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.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 19:50:43 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 2543358 was started by sandbox2 on n001,
% 0.10/0.37 % Sat Sep 26 19:50:43 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 14.89/2.35
% 14.89/2.35 % SZS status Unsatisfiable for theBenchmark
% 14.89/2.35
% 14.89/2.35 % Proof 1 at 0.44 (+ 0.15) seconds.
% 14.89/2.35 % Length of proof is 63.
% 14.89/2.35 % Level of proof is 18.
% 14.89/2.35 % Maximum clause weight is 71.000.
% 14.89/2.35 % Given clauses 67.
% 14.89/2.35
% 14.89/2.35 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------