%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYO656-1 : TPTP v9.0.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n024.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 09:59:09 PM UTC 2025
% Result : Unsatisfiable 30.39s 4.15s
% Output : CNFRefutation 30.39s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause_1153)
% Comments :
%------------------------------------------------------------------------------
cnf(64,plain,
'LE'(f(X0),s('0')),
inference(cnf,[status(esa)],[clause_1153]) ).
cnf(l0,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(62,plain,
( ~ 'LE'(f(X0),s('0'))
| 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_1005]) ).
cnf(l1,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[62]) ).
cnf(9,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(cnf,[status(esa)],[clause_181]) ).
cnf(l2,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(12,plain,
~ 'LE'(f(z),'0'),
inference(cnf,[status(esa)],[clause_613]) ).
cnf(l11,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(45,plain,
( ~ 'LE'(f(suc(X0)),s('0'))
| 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_968]) ).
cnf(l123,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l422,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l431,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(35,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X4),suc(X1))
| ~ iLEQ(suc(X5),suc(X4)) ),
inference(cnf,[status(esa)],[clause_1201]) ).
cnf(l9,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2554,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(14,plain,
( ~ 'LE'(f(suc(suc(X0))),s('0'))
| 'E'('0',f(suc(suc(X0))))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_73]) ).
cnf(l2419,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2425,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2479,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2482,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2344,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2475,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(69,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(cnf,[status(esa)],[clause_854]) ).
cnf(l2376,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[69]) ).
cnf(l2346,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2476,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2705,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[69]) ).
cnf(l2545,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2403,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2558,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2731,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2495,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2431,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2527,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2859,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2341,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2887,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2810,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2736,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2540,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2730,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2480,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2829,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2402,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2494,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2347,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2483,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[69]) ).
cnf(l2473,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2365,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[69]) ).
cnf(l2379,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2917,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2745,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2834,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2935,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2433,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2512,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2809,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2411,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2729,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2531,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2746,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2434,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2477,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2932,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2533,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3009,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2423,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2496,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2567,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2534,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2855,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2871,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3000,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3013,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2349,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[69]) ).
cnf(l2414,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2800,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2765,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2806,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3041,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2775,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2936,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3040,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3042,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2599,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2977,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2999,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(5,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X5),f(suc(X5))) ),
inference(cnf,[status(esa)],[clause_1185]) ).
cnf(l23,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2448,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2615,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2375,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2702,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2315,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2352,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2633,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2143,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2614,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2353,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2680,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2670,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2355,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3061,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2301,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2562,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2561,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2413,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2302,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3024,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3252,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2938,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3342,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2571,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3091,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3033,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3269,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2575,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3351,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3096,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3268,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3353,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3237,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3255,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3256,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3140,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3831,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2574,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3026,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3911,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2568,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3177,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3325,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3728,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3209,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3248,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3730,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3215,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2354,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3595,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2611,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2925,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2610,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2929,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2608,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3323,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4030,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3247,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3571,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3015,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2927,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2316,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2924,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l4066,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2926,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3239,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3141,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3863,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4075,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2437,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3098,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3427,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3121,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3187,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3030,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3708,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3825,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2934,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3479,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3731,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3150,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3119,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3127,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3219,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2939,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3131,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3004,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3083,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2504,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4267,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3423,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3493,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2393,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3378,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3729,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3705,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4143,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2453,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2928,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3032,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3221,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2940,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3036,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3122,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3354,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3053,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3419,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3511,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2418,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3054,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3025,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3023,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3129,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2412,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3371,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2394,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2447,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3884,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3055,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3118,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3699,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3143,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2152,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3175,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l4085,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3182,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3356,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2981,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3103,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3045,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4060,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2313,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3606,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3401,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3052,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3149,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3403,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2466,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3599,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4383,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2464,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3464,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3489,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3317,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3512,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2678,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2388,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3048,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3799,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2390,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3223,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2373,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2987,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3949,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4325,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l4401,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l4345,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l4257,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2468,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3201,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3120,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2455,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4069,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3582,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3147,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3794,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l4041,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3631,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3132,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2465,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l4061,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2712,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2956,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3183,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3908,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3783,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2937,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4036,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3514,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3313,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3583,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3346,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3567,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3597,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3320,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4382,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3321,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l4028,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3244,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2980,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3227,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3399,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2303,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3653,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2363,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2389,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l4346,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2356,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3598,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2671,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2306,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3038,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2371,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3600,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3341,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3265,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3163,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2361,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3347,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l4436,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2374,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3043,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2636,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3508,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2359,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3094,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2988,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3249,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2625,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2676,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l4427,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3117,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2391,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3517,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3596,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3445,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2672,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3468,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3093,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2673,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3105,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3158,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3301,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3782,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3162,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2631,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2360,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2384,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3719,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2998,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[64]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l11,l123,l422,l431,l9,l2554,l2419,l2425,l2479,l2482,l2344,l2475,l2376,l2346,l2476,l2705,l2545,l2403,l2558,l2731,l2495,l2431,l2527,l2859,l2341,l2887,l2810,l2736,l2540,l2730,l2480,l2829,l2402,l2494,l2347,l2483,l2473,l2365,l2379,l2917,l2745,l2834,l2935,l2433,l2512,l2809,l2411,l2729,l2531,l2746,l2434,l2477,l2932,l2533,l3009,l2423,l2496,l2567,l2534,l2855,l2871,l3000,l3013,l2349,l2414,l2800,l2765,l2806,l3041,l2775,l2936,l3040,l3042,l2599,l2977,l2999,l23,l2448,l2615,l2375,l2702,l2315,l2352,l2633,l2143,l2614,l2353,l2680,l2670,l2355,l3061,l2301,l2562,l2561,l2413,l2302,l3024,l3252,l2938,l3342,l2571,l3091,l3033,l3269,l2575,l3351,l3096,l3268,l3353,l3237,l3255,l3256,l3140,l3831,l2574,l3026,l3911,l2568,l3177,l3325,l3728,l3209,l3248,l3730,l3215,l2354,l3595,l2611,l2925,l2610,l2929,l2608,l3323,l4030,l3247,l3571,l3015,l2927,l2316,l2924,l4066,l2926,l3239,l3141,l3863,l4075,l2437,l3098,l3427,l3121,l3187,l3030,l3708,l3825,l2934,l3479,l3731,l3150,l3119,l3127,l3219,l2939,l3131,l3004,l3083,l2504,l4267,l3423,l3493,l2393,l3378,l3729,l3705,l4143,l2453,l2928,l3032,l3221,l2940,l3036,l3122,l3354,l3053,l3419,l3511,l2418,l3054,l3025,l3023,l3129,l2412,l3371,l2394,l2447,l3884,l3055,l3118,l3699,l3143,l2152,l3175,l4085,l3182,l3356,l2981,l3103,l3045,l4060,l2313,l3606,l3401,l3052,l3149,l3403,l2466,l3599,l4383,l2464,l3464,l3489,l3317,l3512,l2678,l2388,l3048,l3799,l2390,l3223,l2373,l2987,l3949,l4325,l4401,l4345,l4257,l2468,l3201,l3120,l2455,l4069,l3582,l3147,l3794,l4041,l3631,l3132,l2465,l4061,l2712,l2956,l3183,l3908,l3783,l2937,l4036,l3514,l3313,l3583,l3346,l3567,l3597,l3320,l4382,l3321,l4028,l3244,l2980,l3227,l3399,l2303,l3653,l2363,l2389,l4346,l2356,l3598,l2671,l2306,l3038,l2371,l3600,l3341,l3265,l3163,l2361,l3347,l4436,l2374,l3043,l2636,l3508,l2359,l3094,l2988,l3249,l2625,l2676,l4427,l3117,l2391,l3517,l3596,l3445,l2672,l3468,l3093,l2673,l3105,l3158,l3301,l3782,l3162,l2631,l2360,l2384,l3719,l2998]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.09 % Problem : SYO656-1 : TPTP v9.0.0. Released v7.3.0.
% 0.01/0.09 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.29 % Computer : n024.cluster.edu
% 0.08/0.29 % Model : x86_64 x86_64
% 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.29 % Memory : 8042.1875MB
% 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.29 % CPULimit : 300
% 0.08/0.29 % WCLimit : 300
% 0.08/0.29 % DateTime : Tue Jul 22 20:08:04 EDT 2025
% 0.08/0.29 % CPUTime :
% 0.14/0.31 % launching worker at depth: 2
% 0.14/0.31 % launching worker at depth: 4
% 0.14/0.31 % launching worker at depth: 3
% 0.14/0.31 % launching worker at depth: 1
% 0.14/0.31 % launching worker at depth: 7
% 0.14/0.31 % launching worker at depth: 8
% 0.14/0.31 % launching worker at depth: 5
% 0.14/0.31 % launching worker at depth: 6
% 0.14/0.32 % launching worker at depth: 9
% 0.14/0.44 % launching worker at depth: 10
% 0.14/0.46 % launching worker at depth: 11
% 5.09/0.96 % launching worker at depth: 12
% 30.39/4.15 % SZS status Theorem for theBenchmark
% 30.39/4.15 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------