%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO631-1 : TPTP v8.1.2. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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 : Thu May 9 17:51:01 EDT 2024
% Result : Unsatisfiable 1.95s 2.15s
% Output : Refutation 1.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 26
% Syntax : Number of clauses : 95 ( 7 unt; 76 nHn; 49 RR)
% Number of literals : 286 ( 0 equ; 69 neg)
% Maximal clause size : 5 ( 3 avg)
% Maximal term depth : 13 ( 4 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-1 aty)
% Number of variables : 118 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_19_05,axiom,
~ 'E'(f(X31),f(g(X31))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_19_05) ).
cnf(clause_38_52,axiom,
~ 'LE'(f(X29),'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_38_52) ).
cnf(clause_3_02,axiom,
iLEQ(X13,g(X13)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3_02) ).
cnf(clause_56_31,axiom,
( ~ 'LE'(f(X48),s('0'))
| ~ iLEQ(X48,X47)
| 'E'('0',f(X47))
| 'LE'(f(X47),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_56_31) ).
cnf(clause_23_21,axiom,
( ~ 'LE'(f(X51),s(s('0')))
| ~ iLEQ(X51,X50)
| 'E'(s('0'),f(X50))
| 'LE'(f(X50),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_23_21) ).
cnf(clause_18_06,axiom,
iLEQ(X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_18_06) ).
cnf(clause_51_50,axiom,
( ~ 'LE'(f(X54),s(s(s('0'))))
| ~ iLEQ(X54,X53)
| 'E'(s(s('0')),f(X53))
| 'LE'(f(X53),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_51_50) ).
cnf(clause_8_03,axiom,
( ~ 'LE'(f(X20),s(s(s(s('0')))))
| ~ iLEQ(X20,X19)
| 'E'(s(s(s('0'))),f(X19))
| 'LE'(f(X19),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_8_03) ).
cnf(clause_0_36,axiom,
( ~ 'LE'(f(X61),s(s(s(s(s('0'))))))
| ~ iLEQ(X61,X60)
| 'E'(s(s(s(s('0')))),f(X60))
| 'LE'(f(X60),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_0_36) ).
cnf(clause_5_11,axiom,
( ~ 'LE'(f(X39),s(s(s(s(s(s('0')))))))
| ~ iLEQ(X39,X40)
| 'E'(s(s(s(s(s('0'))))),f(X40))
| 'LE'(f(X40),s(s(s(s(s('0')))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5_11) ).
cnf(clause_54_45,axiom,
( ~ 'LE'(f(X66),s(s(s(s(s(s(s('0'))))))))
| ~ iLEQ(X66,X67)
| 'E'(s(s(s(s(s(s('0')))))),f(X67))
| 'LE'(f(X67),s(s(s(s(s(s('0'))))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_54_45) ).
cnf(clause_26_19,axiom,
( ~ 'LE'(f(X64),s(s(s(s(s(s(s(s('0')))))))))
| ~ iLEQ(X64,X63)
| 'E'(s(s(s(s(s(s(s('0'))))))),f(X63))
| 'LE'(f(X63),s(s(s(s(s(s(s('0')))))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_26_19) ).
cnf(clause_10_13,axiom,
( ~ 'LE'(f(X56),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ iLEQ(X56,X55)
| 'E'(s(s(s(s(s(s(s(s('0')))))))),f(X55))
| 'LE'(f(X55),s(s(s(s(s(s(s(s('0'))))))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_10_13) ).
cnf(clause_48_04,axiom,
( ~ 'LE'(f(X26),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ iLEQ(X26,X27)
| 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X27))
| 'LE'(f(X27),s(s(s(s(s(s(s(s(s('0')))))))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_48_04) ).
cnf(clause_49_39,axiom,
( 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X62))
| 'LE'(f(X62),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_49_39) ).
cnf(c0,plain,
( 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X71))
| ~ iLEQ(X71,X72)
| 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X72))
| 'LE'(f(X72),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(resolution,[status(thm)],[clause_49_39,clause_48_04]) ).
cnf(c6,plain,
( 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X75))
| 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(X75)))
| 'LE'(f(g(X75)),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(resolution,[status(thm)],[c0,clause_3_02]) ).
cnf(clause_42_32,axiom,
( ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X68))
| ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(g(X68)))
| 'E'(f(X68),f(g(X68))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_42_32) ).
cnf(c7,plain,
( 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X74))
| 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X74))
| 'LE'(f(X74),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(resolution,[status(thm)],[c0,clause_18_06]) ).
cnf(c11,plain,
( 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(X93)))
| 'LE'(f(g(X93)),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X93))
| 'E'(f(X93),f(g(X93))) ),
inference(resolution,[status(thm)],[c7,clause_42_32]) ).
cnf(c56,plain,
( 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(X95)))
| 'LE'(f(g(X95)),s(s(s(s(s(s(s(s(s('0'))))))))))
| 'E'(f(X95),f(g(X95))) ),
inference(resolution,[status(thm)],[c11,c6]) ).
cnf(c70,plain,
( 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(X96)))
| 'LE'(f(g(X96)),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(resolution,[status(thm)],[c56,clause_19_05]) ).
cnf(c75,plain,
( 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(X103)))
| ~ iLEQ(g(X103),X104)
| 'E'(s(s(s(s(s(s(s(s('0')))))))),f(X104))
| 'LE'(f(X104),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(resolution,[status(thm)],[c70,clause_10_13]) ).
cnf(c86,plain,
( 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(X112)))
| 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(g(X112))))
| 'LE'(f(g(g(X112))),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(resolution,[status(thm)],[c75,clause_3_02]) ).
cnf(clause_27_01,axiom,
( ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X7))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(X7)))
| 'E'(f(X7),f(g(X7))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_27_01) ).
cnf(c87,plain,
( 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(X105)))
| 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(X105)))
| 'LE'(f(g(X105)),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(resolution,[status(thm)],[c75,clause_18_06]) ).
cnf(c88,plain,
( 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(X115)))
| 'LE'(f(g(X115)),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X115))
| 'E'(f(X115),f(g(X115))) ),
inference(resolution,[status(thm)],[c87,clause_27_01]) ).
cnf(c110,plain,
( 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(g(X117))))
| 'LE'(f(g(g(X117))),s(s(s(s(s(s(s(s('0')))))))))
| 'E'(f(g(X117)),f(g(g(X117)))) ),
inference(resolution,[status(thm)],[c88,c86]) ).
cnf(c116,plain,
( 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(g(X118))))
| 'LE'(f(g(g(X118))),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(resolution,[status(thm)],[c110,clause_19_05]) ).
cnf(c118,plain,
( 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(g(X125))))
| ~ iLEQ(g(g(X125)),X126)
| 'E'(s(s(s(s(s(s(s('0'))))))),f(X126))
| 'LE'(f(X126),s(s(s(s(s(s(s('0')))))))) ),
inference(resolution,[status(thm)],[c116,clause_26_19]) ).
cnf(c127,plain,
( 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(g(X135))))
| 'E'(s(s(s(s(s(s(s('0'))))))),f(g(g(g(X135)))))
| 'LE'(f(g(g(g(X135)))),s(s(s(s(s(s(s('0')))))))) ),
inference(resolution,[status(thm)],[c118,clause_3_02]) ).
cnf(clause_31_54,axiom,
( ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(X65))
| ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(X65)))
| 'E'(f(X65),f(g(X65))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_31_54) ).
cnf(c128,plain,
( 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(g(X127))))
| 'E'(s(s(s(s(s(s(s('0'))))))),f(g(g(X127))))
| 'LE'(f(g(g(X127))),s(s(s(s(s(s(s('0')))))))) ),
inference(resolution,[status(thm)],[c118,clause_18_06]) ).
cnf(c130,plain,
( 'E'(s(s(s(s(s(s(s('0'))))))),f(g(g(X151))))
| 'LE'(f(g(g(X151))),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(X151)))
| 'E'(f(g(X151)),f(g(g(X151)))) ),
inference(resolution,[status(thm)],[c128,clause_31_54]) ).
cnf(c165,plain,
( 'E'(s(s(s(s(s(s(s('0'))))))),f(g(g(g(X152)))))
| 'LE'(f(g(g(g(X152)))),s(s(s(s(s(s(s('0'))))))))
| 'E'(f(g(g(X152))),f(g(g(g(X152))))) ),
inference(resolution,[status(thm)],[c130,c127]) ).
cnf(c172,plain,
( 'E'(s(s(s(s(s(s(s('0'))))))),f(g(g(g(X153)))))
| 'LE'(f(g(g(g(X153)))),s(s(s(s(s(s(s('0')))))))) ),
inference(resolution,[status(thm)],[c165,clause_19_05]) ).
cnf(c174,plain,
( 'E'(s(s(s(s(s(s(s('0'))))))),f(g(g(g(X157)))))
| ~ iLEQ(g(g(g(X157))),X158)
| 'E'(s(s(s(s(s(s('0')))))),f(X158))
| 'LE'(f(X158),s(s(s(s(s(s('0'))))))) ),
inference(resolution,[status(thm)],[c172,clause_54_45]) ).
cnf(c178,plain,
( 'E'(s(s(s(s(s(s(s('0'))))))),f(g(g(g(X169)))))
| 'E'(s(s(s(s(s(s('0')))))),f(g(g(g(g(X169))))))
| 'LE'(f(g(g(g(g(X169))))),s(s(s(s(s(s('0'))))))) ),
inference(resolution,[status(thm)],[c174,clause_3_02]) ).
cnf(clause_44_07,axiom,
( ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(X33))
| ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(g(X33)))
| 'E'(f(X33),f(g(X33))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_44_07) ).
cnf(c179,plain,
( 'E'(s(s(s(s(s(s(s('0'))))))),f(g(g(g(X159)))))
| 'E'(s(s(s(s(s(s('0')))))),f(g(g(g(X159)))))
| 'LE'(f(g(g(g(X159)))),s(s(s(s(s(s('0'))))))) ),
inference(resolution,[status(thm)],[c174,clause_18_06]) ).
cnf(c180,plain,
( 'E'(s(s(s(s(s(s('0')))))),f(g(g(g(X202)))))
| 'LE'(f(g(g(g(X202)))),s(s(s(s(s(s('0')))))))
| ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(g(g(X202))))
| 'E'(f(g(g(X202))),f(g(g(g(X202))))) ),
inference(resolution,[status(thm)],[c179,clause_44_07]) ).
cnf(c246,plain,
( 'E'(s(s(s(s(s(s('0')))))),f(g(g(g(g(X203))))))
| 'LE'(f(g(g(g(g(X203))))),s(s(s(s(s(s('0')))))))
| 'E'(f(g(g(g(X203)))),f(g(g(g(g(X203)))))) ),
inference(resolution,[status(thm)],[c180,c178]) ).
cnf(c251,plain,
( 'E'(s(s(s(s(s(s('0')))))),f(g(g(g(g(X204))))))
| 'LE'(f(g(g(g(g(X204))))),s(s(s(s(s(s('0'))))))) ),
inference(resolution,[status(thm)],[c246,clause_19_05]) ).
cnf(c253,plain,
( 'E'(s(s(s(s(s(s('0')))))),f(g(g(g(g(X206))))))
| ~ iLEQ(g(g(g(g(X206)))),X205)
| 'E'(s(s(s(s(s('0'))))),f(X205))
| 'LE'(f(X205),s(s(s(s(s('0')))))) ),
inference(resolution,[status(thm)],[c251,clause_5_11]) ).
cnf(c254,plain,
( 'E'(s(s(s(s(s(s('0')))))),f(g(g(g(g(X211))))))
| 'E'(s(s(s(s(s('0'))))),f(g(g(g(g(g(X211)))))))
| 'LE'(f(g(g(g(g(g(X211)))))),s(s(s(s(s('0')))))) ),
inference(resolution,[status(thm)],[c253,clause_3_02]) ).
cnf(clause_11_16,axiom,
( ~ 'E'(s(s(s(s(s(s('0')))))),f(X59))
| ~ 'E'(s(s(s(s(s(s('0')))))),f(g(X59)))
| 'E'(f(X59),f(g(X59))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_11_16) ).
cnf(c255,plain,
( 'E'(s(s(s(s(s(s('0')))))),f(g(g(g(g(X210))))))
| 'E'(s(s(s(s(s('0'))))),f(g(g(g(g(X210))))))
| 'LE'(f(g(g(g(g(X210))))),s(s(s(s(s('0')))))) ),
inference(resolution,[status(thm)],[c253,clause_18_06]) ).
cnf(c259,plain,
( 'E'(s(s(s(s(s('0'))))),f(g(g(g(g(X266))))))
| 'LE'(f(g(g(g(g(X266))))),s(s(s(s(s('0'))))))
| ~ 'E'(s(s(s(s(s(s('0')))))),f(g(g(g(X266)))))
| 'E'(f(g(g(g(X266)))),f(g(g(g(g(X266)))))) ),
inference(resolution,[status(thm)],[c255,clause_11_16]) ).
cnf(c334,plain,
( 'E'(s(s(s(s(s('0'))))),f(g(g(g(g(g(X267)))))))
| 'LE'(f(g(g(g(g(g(X267)))))),s(s(s(s(s('0'))))))
| 'E'(f(g(g(g(g(X267))))),f(g(g(g(g(g(X267))))))) ),
inference(resolution,[status(thm)],[c259,c254]) ).
cnf(c338,plain,
( 'E'(s(s(s(s(s('0'))))),f(g(g(g(g(g(X268)))))))
| 'LE'(f(g(g(g(g(g(X268)))))),s(s(s(s(s('0')))))) ),
inference(resolution,[status(thm)],[c334,clause_19_05]) ).
cnf(clause_40_23,axiom,
( ~ 'E'(s(s(s(s(s('0'))))),f(X58))
| ~ 'E'(s(s(s(s(s('0'))))),f(g(X58)))
| 'E'(f(X58),f(g(X58))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_40_23) ).
cnf(c336,plain,
( 'LE'(f(g(g(g(g(g(X273)))))),s(s(s(s(s('0'))))))
| 'E'(f(g(g(g(g(X273))))),f(g(g(g(g(g(X273)))))))
| ~ 'E'(s(s(s(s(s('0'))))),f(g(g(g(g(X273)))))) ),
inference(resolution,[status(thm)],[c334,clause_40_23]) ).
cnf(c347,plain,
( 'LE'(f(g(g(g(g(g(g(X276))))))),s(s(s(s(s('0'))))))
| 'E'(f(g(g(g(g(g(X276)))))),f(g(g(g(g(g(g(X276))))))))
| 'LE'(f(g(g(g(g(g(X276)))))),s(s(s(s(s('0')))))) ),
inference(resolution,[status(thm)],[c336,c338]) ).
cnf(c355,plain,
( 'LE'(f(g(g(g(g(g(g(X277))))))),s(s(s(s(s('0'))))))
| 'LE'(f(g(g(g(g(g(X277)))))),s(s(s(s(s('0')))))) ),
inference(resolution,[status(thm)],[c347,clause_19_05]) ).
cnf(c357,plain,
( 'LE'(f(g(g(g(g(g(X280)))))),s(s(s(s(s('0'))))))
| ~ iLEQ(g(g(g(g(g(g(X280)))))),X279)
| 'E'(s(s(s(s('0')))),f(X279))
| 'LE'(f(X279),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c355,clause_0_36]) ).
cnf(c360,plain,
( 'LE'(f(g(g(g(g(g(X284)))))),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(g(g(g(g(g(g(X284))))))))
| 'LE'(f(g(g(g(g(g(g(X284))))))),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c357,clause_18_06]) ).
cnf(c366,plain,
( 'E'(s(s(s(s('0')))),f(g(g(g(g(g(g(X323))))))))
| 'LE'(f(g(g(g(g(g(g(X323))))))),s(s(s(s('0')))))
| ~ iLEQ(g(g(g(g(g(X323))))),X322)
| 'E'(s(s(s(s('0')))),f(X322))
| 'LE'(f(X322),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c360,clause_0_36]) ).
cnf(c439,plain,
( 'E'(s(s(s(s('0')))),f(g(g(g(g(g(g(X324))))))))
| 'LE'(f(g(g(g(g(g(g(X324))))))),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c366,clause_3_02]) ).
cnf(clause_55_48,axiom,
( ~ 'E'(s(s(s(s('0')))),f(X57))
| ~ 'E'(s(s(s(s('0')))),f(g(X57)))
| 'E'(f(X57),f(g(X57))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_55_48) ).
cnf(c441,plain,
( 'LE'(f(g(g(g(g(g(g(X331))))))),s(s(s(s('0')))))
| ~ 'E'(s(s(s(s('0')))),f(g(g(g(g(g(X331)))))))
| 'E'(f(g(g(g(g(g(X331)))))),f(g(g(g(g(g(g(X331)))))))) ),
inference(resolution,[status(thm)],[c439,clause_55_48]) ).
cnf(c456,plain,
( 'LE'(f(g(g(g(g(g(g(g(X335)))))))),s(s(s(s('0')))))
| 'E'(f(g(g(g(g(g(g(X335))))))),f(g(g(g(g(g(g(g(X335)))))))))
| 'LE'(f(g(g(g(g(g(g(X335))))))),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c441,c439]) ).
cnf(c462,plain,
( 'LE'(f(g(g(g(g(g(g(g(X336)))))))),s(s(s(s('0')))))
| 'LE'(f(g(g(g(g(g(g(X336))))))),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c456,clause_19_05]) ).
cnf(c464,plain,
( 'LE'(f(g(g(g(g(g(g(X337))))))),s(s(s(s('0')))))
| ~ iLEQ(g(g(g(g(g(g(g(X337))))))),X338)
| 'E'(s(s(s('0'))),f(X338))
| 'LE'(f(X338),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c462,clause_8_03]) ).
cnf(c467,plain,
( 'LE'(f(g(g(g(g(g(g(X343))))))),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(g(g(g(g(g(g(g(X343)))))))))
| 'LE'(f(g(g(g(g(g(g(g(X343)))))))),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c464,clause_18_06]) ).
cnf(c473,plain,
( 'E'(s(s(s('0'))),f(g(g(g(g(g(g(g(X356)))))))))
| 'LE'(f(g(g(g(g(g(g(g(X356)))))))),s(s(s('0'))))
| ~ iLEQ(g(g(g(g(g(g(X356)))))),X355)
| 'E'(s(s(s('0'))),f(X355))
| 'LE'(f(X355),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c467,clause_8_03]) ).
cnf(c490,plain,
( 'E'(s(s(s('0'))),f(g(g(g(g(g(g(g(X357)))))))))
| 'LE'(f(g(g(g(g(g(g(g(X357)))))))),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c473,clause_3_02]) ).
cnf(clause_29_12,axiom,
( ~ 'E'(s(s(s('0'))),f(X46))
| ~ 'E'(s(s(s('0'))),f(g(X46)))
| 'E'(f(X46),f(g(X46))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_29_12) ).
cnf(c492,plain,
( 'LE'(f(g(g(g(g(g(g(g(X363)))))))),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(g(g(g(g(g(g(X363))))))))
| 'E'(f(g(g(g(g(g(g(X363))))))),f(g(g(g(g(g(g(g(X363))))))))) ),
inference(resolution,[status(thm)],[c490,clause_29_12]) ).
cnf(c506,plain,
( 'LE'(f(g(g(g(g(g(g(g(g(X369))))))))),s(s(s('0'))))
| 'E'(f(g(g(g(g(g(g(g(X369)))))))),f(g(g(g(g(g(g(g(g(X369))))))))))
| 'LE'(f(g(g(g(g(g(g(g(X369)))))))),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c492,c490]) ).
cnf(c512,plain,
( 'LE'(f(g(g(g(g(g(g(g(g(X370))))))))),s(s(s('0'))))
| 'LE'(f(g(g(g(g(g(g(g(X370)))))))),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c506,clause_19_05]) ).
cnf(c514,plain,
( 'LE'(f(g(g(g(g(g(g(g(X371)))))))),s(s(s('0'))))
| ~ iLEQ(g(g(g(g(g(g(g(g(X371)))))))),X372)
| 'E'(s(s('0')),f(X372))
| 'LE'(f(X372),s(s('0'))) ),
inference(resolution,[status(thm)],[c512,clause_51_50]) ).
cnf(c517,plain,
( 'LE'(f(g(g(g(g(g(g(g(X377)))))))),s(s(s('0'))))
| 'E'(s(s('0')),f(g(g(g(g(g(g(g(g(X377))))))))))
| 'LE'(f(g(g(g(g(g(g(g(g(X377))))))))),s(s('0'))) ),
inference(resolution,[status(thm)],[c514,clause_18_06]) ).
cnf(c523,plain,
( 'E'(s(s('0')),f(g(g(g(g(g(g(g(g(X388))))))))))
| 'LE'(f(g(g(g(g(g(g(g(g(X388))))))))),s(s('0')))
| ~ iLEQ(g(g(g(g(g(g(g(X388))))))),X387)
| 'E'(s(s('0')),f(X387))
| 'LE'(f(X387),s(s('0'))) ),
inference(resolution,[status(thm)],[c517,clause_51_50]) ).
cnf(c538,plain,
( 'E'(s(s('0')),f(g(g(g(g(g(g(g(g(X389))))))))))
| 'LE'(f(g(g(g(g(g(g(g(g(X389))))))))),s(s('0'))) ),
inference(resolution,[status(thm)],[c523,clause_3_02]) ).
cnf(clause_20_22,axiom,
( ~ 'E'(s(s('0')),f(X52))
| ~ 'E'(s(s('0')),f(g(X52)))
| 'E'(f(X52),f(g(X52))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_20_22) ).
cnf(c540,plain,
( 'LE'(f(g(g(g(g(g(g(g(g(X397))))))))),s(s('0')))
| ~ 'E'(s(s('0')),f(g(g(g(g(g(g(g(X397)))))))))
| 'E'(f(g(g(g(g(g(g(g(X397)))))))),f(g(g(g(g(g(g(g(g(X397)))))))))) ),
inference(resolution,[status(thm)],[c538,clause_20_22]) ).
cnf(c554,plain,
( 'LE'(f(g(g(g(g(g(g(g(g(g(X425)))))))))),s(s('0')))
| 'E'(f(g(g(g(g(g(g(g(g(X425))))))))),f(g(g(g(g(g(g(g(g(g(X425)))))))))))
| 'LE'(f(g(g(g(g(g(g(g(g(X425))))))))),s(s('0'))) ),
inference(resolution,[status(thm)],[c540,c538]) ).
cnf(c607,plain,
( 'LE'(f(g(g(g(g(g(g(g(g(g(X426)))))))))),s(s('0')))
| 'LE'(f(g(g(g(g(g(g(g(g(X426))))))))),s(s('0'))) ),
inference(resolution,[status(thm)],[c554,clause_19_05]) ).
cnf(c609,plain,
( 'LE'(f(g(g(g(g(g(g(g(g(X429))))))))),s(s('0')))
| ~ iLEQ(g(g(g(g(g(g(g(g(g(X429))))))))),X428)
| 'E'(s('0'),f(X428))
| 'LE'(f(X428),s('0')) ),
inference(resolution,[status(thm)],[c607,clause_23_21]) ).
cnf(c612,plain,
( 'LE'(f(g(g(g(g(g(g(g(g(X433))))))))),s(s('0')))
| 'E'(s('0'),f(g(g(g(g(g(g(g(g(g(X433)))))))))))
| 'LE'(f(g(g(g(g(g(g(g(g(g(X433)))))))))),s('0')) ),
inference(resolution,[status(thm)],[c609,clause_18_06]) ).
cnf(c618,plain,
( 'E'(s('0'),f(g(g(g(g(g(g(g(g(g(X443)))))))))))
| 'LE'(f(g(g(g(g(g(g(g(g(g(X443)))))))))),s('0'))
| ~ iLEQ(g(g(g(g(g(g(g(g(X443)))))))),X444)
| 'E'(s('0'),f(X444))
| 'LE'(f(X444),s('0')) ),
inference(resolution,[status(thm)],[c612,clause_23_21]) ).
cnf(c633,plain,
( 'E'(s('0'),f(g(g(g(g(g(g(g(g(g(X446)))))))))))
| 'LE'(f(g(g(g(g(g(g(g(g(g(X446)))))))))),s('0')) ),
inference(resolution,[status(thm)],[c618,clause_3_02]) ).
cnf(c649,plain,
( 'E'(s('0'),f(g(g(g(g(g(g(g(g(g(X448)))))))))))
| ~ iLEQ(g(g(g(g(g(g(g(g(g(X448))))))))),X447)
| 'E'('0',f(X447))
| 'LE'(f(X447),'0') ),
inference(resolution,[status(thm)],[c633,clause_56_31]) ).
cnf(c650,plain,
( 'E'(s('0'),f(g(g(g(g(g(g(g(g(g(X451)))))))))))
| 'E'('0',f(g(g(g(g(g(g(g(g(g(g(X451))))))))))))
| 'LE'(f(g(g(g(g(g(g(g(g(g(g(X451))))))))))),'0') ),
inference(resolution,[status(thm)],[c649,clause_3_02]) ).
cnf(c659,plain,
( 'E'(s('0'),f(g(g(g(g(g(g(g(g(g(X454)))))))))))
| 'E'('0',f(g(g(g(g(g(g(g(g(g(g(X454)))))))))))) ),
inference(resolution,[status(thm)],[c650,clause_38_52]) ).
cnf(clause_30_35,axiom,
( ~ 'E'(s('0'),f(X49))
| ~ 'E'(s('0'),f(g(X49)))
| 'E'(f(X49),f(g(X49))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_30_35) ).
cnf(c651,plain,
( 'E'(s('0'),f(g(g(g(g(g(g(g(g(g(X449)))))))))))
| 'E'('0',f(g(g(g(g(g(g(g(g(g(X449)))))))))))
| 'LE'(f(g(g(g(g(g(g(g(g(g(X449)))))))))),'0') ),
inference(resolution,[status(thm)],[c649,clause_18_06]) ).
cnf(c654,plain,
( 'E'(s('0'),f(g(g(g(g(g(g(g(g(g(X450)))))))))))
| 'E'('0',f(g(g(g(g(g(g(g(g(g(X450))))))))))) ),
inference(resolution,[status(thm)],[c651,clause_38_52]) ).
cnf(c655,plain,
( 'E'('0',f(g(g(g(g(g(g(g(g(g(X471)))))))))))
| ~ 'E'(s('0'),f(g(g(g(g(g(g(g(g(X471))))))))))
| 'E'(f(g(g(g(g(g(g(g(g(X471))))))))),f(g(g(g(g(g(g(g(g(g(X471))))))))))) ),
inference(resolution,[status(thm)],[c654,clause_30_35]) ).
cnf(c725,plain,
( 'E'('0',f(g(g(g(g(g(g(g(g(g(g(X472))))))))))))
| 'E'(f(g(g(g(g(g(g(g(g(g(X472)))))))))),f(g(g(g(g(g(g(g(g(g(g(X472)))))))))))) ),
inference(resolution,[status(thm)],[c655,c659]) ).
cnf(c731,plain,
'E'('0',f(g(g(g(g(g(g(g(g(g(g(X473)))))))))))),
inference(resolution,[status(thm)],[c725,clause_19_05]) ).
cnf(clause_2_25,axiom,
( ~ 'E'('0',f(X45))
| ~ 'E'('0',f(g(X45)))
| 'E'(f(X45),f(g(X45))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2_25) ).
cnf(c730,plain,
( 'E'(f(g(g(g(g(g(g(g(g(g(X476)))))))))),f(g(g(g(g(g(g(g(g(g(g(X476))))))))))))
| ~ 'E'('0',f(g(g(g(g(g(g(g(g(g(X476))))))))))) ),
inference(resolution,[status(thm)],[c725,clause_2_25]) ).
cnf(c734,plain,
'E'(f(g(g(g(g(g(g(g(g(g(g(X477))))))))))),f(g(g(g(g(g(g(g(g(g(g(g(X477))))))))))))),
inference(resolution,[status(thm)],[c730,c731]) ).
cnf(c736,plain,
$false,
inference(resolution,[status(thm)],[c734,clause_19_05]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SYO631-1 : TPTP v8.1.2. Released v7.1.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n018.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 18:00:37 EDT 2024
% 0.14/0.35 % CPUTime :
% 1.95/2.15 % Version: 1.5
% 1.95/2.15 % SZS status Unsatisfiable
% 1.95/2.15 % SZS output start CNFRefutation
% See solution above
% 1.95/2.16
% 1.95/2.16 % Initial clauses : 57
% 1.95/2.16 % Processed clauses : 240
% 1.95/2.16 % Factors computed : 0
% 1.95/2.16 % Resolvents computed: 737
% 1.95/2.16 % Tautologies deleted: 0
% 1.95/2.16 % Forward subsumed : 128
% 1.95/2.16 % Backward subsumed : 80
% 1.95/2.16 % -------- CPU Time ---------
% 1.95/2.16 % User time : 1.778 s
% 1.95/2.16 % System time : 0.021 s
% 1.95/2.16 % Total time : 1.799 s
%------------------------------------------------------------------------------