%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO630-1 : TPTP v8.1.2. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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 0.80s 1.02s
% Output : Refutation 0.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 16
% Syntax : Number of clauses : 52 ( 7 unt; 38 nHn; 26 RR)
% Number of literals : 147 ( 0 equ; 36 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 8 ( 3 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 : 62 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_31_05,axiom,
~ 'E'(f(X13),f(g(X13))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_31_05) ).
cnf(clause_6_07,axiom,
~ 'LE'(f(X16),'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6_07) ).
cnf(clause_13_02,axiom,
iLEQ(X9,g(X9)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_13_02) ).
cnf(clause_1_06,axiom,
( ~ 'LE'(f(X19),s('0'))
| ~ iLEQ(X19,X20)
| 'E'('0',f(X20))
| 'LE'(f(X20),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1_06) ).
cnf(clause_17_32,axiom,
( ~ 'LE'(f(X29),s(s('0')))
| ~ iLEQ(X29,X28)
| 'E'(s('0'),f(X28))
| 'LE'(f(X28),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_17_32) ).
cnf(clause_18_04,axiom,
iLEQ(X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_18_04) ).
cnf(clause_16_15,axiom,
( ~ 'LE'(f(X33),s(s(s('0'))))
| ~ iLEQ(X33,X32)
| 'E'(s(s('0')),f(X32))
| 'LE'(f(X32),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_16_15) ).
cnf(clause_26_17,axiom,
( ~ 'LE'(f(X37),s(s(s(s('0')))))
| ~ iLEQ(X37,X38)
| 'E'(s(s(s('0'))),f(X38))
| 'LE'(f(X38),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_26_17) ).
cnf(clause_8_01,axiom,
( 'E'(s(s(s(s(s('0'))))),f(X7))
| 'LE'(f(X7),s(s(s(s(s('0')))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_8_01) ).
cnf(clause_7_16,axiom,
( ~ 'LE'(f(X34),s(s(s(s(s('0'))))))
| ~ iLEQ(X34,X35)
| 'E'(s(s(s(s('0')))),f(X35))
| 'LE'(f(X35),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7_16) ).
cnf(c1,plain,
( ~ iLEQ(X42,X43)
| 'E'(s(s(s(s('0')))),f(X43))
| 'LE'(f(X43),s(s(s(s('0')))))
| 'E'(s(s(s(s(s('0'))))),f(X42)) ),
inference(resolution,[status(thm)],[clause_7_16,clause_8_01]) ).
cnf(c9,plain,
( 'E'(s(s(s(s('0')))),f(g(X45)))
| 'LE'(f(g(X45)),s(s(s(s('0')))))
| 'E'(s(s(s(s(s('0'))))),f(X45)) ),
inference(resolution,[status(thm)],[c1,clause_13_02]) ).
cnf(clause_3_10,axiom,
( ~ 'E'(s(s(s(s(s('0'))))),f(X26))
| ~ 'E'(s(s(s(s(s('0'))))),f(g(X26)))
| 'E'(f(X26),f(g(X26))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3_10) ).
cnf(c8,plain,
( 'E'(s(s(s(s('0')))),f(X44))
| 'LE'(f(X44),s(s(s(s('0')))))
| 'E'(s(s(s(s(s('0'))))),f(X44)) ),
inference(resolution,[status(thm)],[c1,clause_18_04]) ).
cnf(c13,plain,
( 'E'(s(s(s(s('0')))),f(g(X64)))
| 'LE'(f(g(X64)),s(s(s(s('0')))))
| ~ 'E'(s(s(s(s(s('0'))))),f(X64))
| 'E'(f(X64),f(g(X64))) ),
inference(resolution,[status(thm)],[c8,clause_3_10]) ).
cnf(c64,plain,
( 'E'(s(s(s(s('0')))),f(g(X67)))
| 'LE'(f(g(X67)),s(s(s(s('0')))))
| 'E'(f(X67),f(g(X67))) ),
inference(resolution,[status(thm)],[c13,c9]) ).
cnf(c72,plain,
( 'E'(s(s(s(s('0')))),f(g(X68)))
| 'LE'(f(g(X68)),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c64,clause_31_05]) ).
cnf(c77,plain,
( 'E'(s(s(s(s('0')))),f(g(X72)))
| ~ iLEQ(g(X72),X71)
| 'E'(s(s(s('0'))),f(X71))
| 'LE'(f(X71),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c72,clause_26_17]) ).
cnf(c82,plain,
( 'E'(s(s(s(s('0')))),f(g(X78)))
| 'E'(s(s(s('0'))),f(g(g(X78))))
| 'LE'(f(g(g(X78))),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c77,clause_13_02]) ).
cnf(clause_12_30,axiom,
( ~ 'E'(s(s(s(s('0')))),f(X36))
| ~ 'E'(s(s(s(s('0')))),f(g(X36)))
| 'E'(f(X36),f(g(X36))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_12_30) ).
cnf(c81,plain,
( 'E'(s(s(s(s('0')))),f(g(X75)))
| 'E'(s(s(s('0'))),f(g(X75)))
| 'LE'(f(g(X75)),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c77,clause_18_04]) ).
cnf(c83,plain,
( 'E'(s(s(s('0'))),f(g(X87)))
| 'LE'(f(g(X87)),s(s(s('0'))))
| ~ 'E'(s(s(s(s('0')))),f(X87))
| 'E'(f(X87),f(g(X87))) ),
inference(resolution,[status(thm)],[c81,clause_12_30]) ).
cnf(c110,plain,
( 'E'(s(s(s('0'))),f(g(g(X89))))
| 'LE'(f(g(g(X89))),s(s(s('0'))))
| 'E'(f(g(X89)),f(g(g(X89)))) ),
inference(resolution,[status(thm)],[c83,c82]) ).
cnf(c116,plain,
( 'E'(s(s(s('0'))),f(g(g(X90))))
| 'LE'(f(g(g(X90))),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c110,clause_31_05]) ).
cnf(c118,plain,
( 'E'(s(s(s('0'))),f(g(g(X93))))
| ~ iLEQ(g(g(X93)),X94)
| 'E'(s(s('0')),f(X94))
| 'LE'(f(X94),s(s('0'))) ),
inference(resolution,[status(thm)],[c116,clause_16_15]) ).
cnf(c123,plain,
( 'E'(s(s(s('0'))),f(g(g(X98))))
| 'E'(s(s('0')),f(g(g(g(X98)))))
| 'LE'(f(g(g(g(X98)))),s(s('0'))) ),
inference(resolution,[status(thm)],[c118,clause_13_02]) ).
cnf(clause_21_11,axiom,
( ~ 'E'(s(s(s('0'))),f(X31))
| ~ 'E'(s(s(s('0'))),f(g(X31)))
| 'E'(f(X31),f(g(X31))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_21_11) ).
cnf(c122,plain,
( 'E'(s(s(s('0'))),f(g(g(X97))))
| 'E'(s(s('0')),f(g(g(X97))))
| 'LE'(f(g(g(X97))),s(s('0'))) ),
inference(resolution,[status(thm)],[c118,clause_18_04]) ).
cnf(c124,plain,
( 'E'(s(s('0')),f(g(g(X128))))
| 'LE'(f(g(g(X128))),s(s('0')))
| ~ 'E'(s(s(s('0'))),f(g(X128)))
| 'E'(f(g(X128)),f(g(g(X128)))) ),
inference(resolution,[status(thm)],[c122,clause_21_11]) ).
cnf(c192,plain,
( 'E'(s(s('0')),f(g(g(g(X129)))))
| 'LE'(f(g(g(g(X129)))),s(s('0')))
| 'E'(f(g(g(X129))),f(g(g(g(X129))))) ),
inference(resolution,[status(thm)],[c124,c123]) ).
cnf(c195,plain,
( 'E'(s(s('0')),f(g(g(g(X130)))))
| 'LE'(f(g(g(g(X130)))),s(s('0'))) ),
inference(resolution,[status(thm)],[c192,clause_31_05]) ).
cnf(clause_27_12,axiom,
( ~ 'E'(s(s('0')),f(X30))
| ~ 'E'(s(s('0')),f(g(X30)))
| 'E'(f(X30),f(g(X30))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_27_12) ).
cnf(c193,plain,
( 'LE'(f(g(g(g(X136)))),s(s('0')))
| 'E'(f(g(g(X136))),f(g(g(g(X136)))))
| ~ 'E'(s(s('0')),f(g(g(X136)))) ),
inference(resolution,[status(thm)],[c192,clause_27_12]) ).
cnf(c204,plain,
( 'LE'(f(g(g(g(g(X141))))),s(s('0')))
| 'E'(f(g(g(g(X141)))),f(g(g(g(g(X141))))))
| 'LE'(f(g(g(g(X141)))),s(s('0'))) ),
inference(resolution,[status(thm)],[c193,c195]) ).
cnf(c215,plain,
( 'LE'(f(g(g(g(g(X143))))),s(s('0')))
| 'LE'(f(g(g(g(X143)))),s(s('0'))) ),
inference(resolution,[status(thm)],[c204,clause_31_05]) ).
cnf(c217,plain,
( 'LE'(f(g(g(g(X145)))),s(s('0')))
| ~ iLEQ(g(g(g(g(X145)))),X144)
| 'E'(s('0'),f(X144))
| 'LE'(f(X144),s('0')) ),
inference(resolution,[status(thm)],[c215,clause_17_32]) ).
cnf(c219,plain,
( 'LE'(f(g(g(g(X149)))),s(s('0')))
| 'E'(s('0'),f(g(g(g(g(X149))))))
| 'LE'(f(g(g(g(g(X149))))),s('0')) ),
inference(resolution,[status(thm)],[c217,clause_18_04]) ).
cnf(c226,plain,
( 'E'(s('0'),f(g(g(g(g(X225))))))
| 'LE'(f(g(g(g(g(X225))))),s('0'))
| ~ iLEQ(g(g(g(X225))),X224)
| 'E'(s('0'),f(X224))
| 'LE'(f(X224),s('0')) ),
inference(resolution,[status(thm)],[c219,clause_17_32]) ).
cnf(c471,plain,
( 'E'(s('0'),f(g(g(g(g(X226))))))
| 'LE'(f(g(g(g(g(X226))))),s('0')) ),
inference(resolution,[status(thm)],[c226,clause_13_02]) ).
cnf(c474,plain,
( 'E'(s('0'),f(g(g(g(g(X229))))))
| ~ iLEQ(g(g(g(g(X229)))),X228)
| 'E'('0',f(X228))
| 'LE'(f(X228),'0') ),
inference(resolution,[status(thm)],[c471,clause_1_06]) ).
cnf(c476,plain,
( 'E'(s('0'),f(g(g(g(g(X232))))))
| 'E'('0',f(g(g(g(g(g(X232)))))))
| 'LE'(f(g(g(g(g(g(X232)))))),'0') ),
inference(resolution,[status(thm)],[c474,clause_13_02]) ).
cnf(c490,plain,
( 'E'(s('0'),f(g(g(g(g(X233))))))
| 'E'('0',f(g(g(g(g(g(X233))))))) ),
inference(resolution,[status(thm)],[c476,clause_6_07]) ).
cnf(clause_30_13,axiom,
( ~ 'E'(s('0'),f(X27))
| ~ 'E'(s('0'),f(g(X27)))
| 'E'(f(X27),f(g(X27))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_30_13) ).
cnf(c475,plain,
( 'E'(s('0'),f(g(g(g(g(X230))))))
| 'E'('0',f(g(g(g(g(X230))))))
| 'LE'(f(g(g(g(g(X230))))),'0') ),
inference(resolution,[status(thm)],[c474,clause_18_04]) ).
cnf(c481,plain,
( 'E'(s('0'),f(g(g(g(g(X231))))))
| 'E'('0',f(g(g(g(g(X231)))))) ),
inference(resolution,[status(thm)],[c475,clause_6_07]) ).
cnf(c482,plain,
( 'E'('0',f(g(g(g(g(X235))))))
| ~ 'E'(s('0'),f(g(g(g(X235)))))
| 'E'(f(g(g(g(X235)))),f(g(g(g(g(X235)))))) ),
inference(resolution,[status(thm)],[c481,clause_30_13]) ).
cnf(c495,plain,
( 'E'('0',f(g(g(g(g(g(X236)))))))
| 'E'(f(g(g(g(g(X236))))),f(g(g(g(g(g(X236))))))) ),
inference(resolution,[status(thm)],[c482,c490]) ).
cnf(c508,plain,
'E'('0',f(g(g(g(g(g(X237))))))),
inference(resolution,[status(thm)],[c495,clause_31_05]) ).
cnf(clause_29_24,axiom,
( ~ 'E'('0',f(X25))
| ~ 'E'('0',f(g(X25)))
| 'E'(f(X25),f(g(X25))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_29_24) ).
cnf(c507,plain,
( 'E'(f(g(g(g(g(X238))))),f(g(g(g(g(g(X238)))))))
| ~ 'E'('0',f(g(g(g(g(X238)))))) ),
inference(resolution,[status(thm)],[c495,clause_29_24]) ).
cnf(c512,plain,
'E'(f(g(g(g(g(g(X239)))))),f(g(g(g(g(g(g(X239)))))))),
inference(resolution,[status(thm)],[c507,c508]) ).
cnf(c516,plain,
$false,
inference(resolution,[status(thm)],[c512,clause_31_05]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.13 % Problem : SYO630-1 : TPTP v8.1.2. Released v7.1.0.
% 0.05/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n012.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 17:51:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.80/1.02 % Version: 1.5
% 0.80/1.02 % SZS status Unsatisfiable
% 0.80/1.02 % SZS output start CNFRefutation
% See solution above
% 0.80/1.02
% 0.80/1.02 % Initial clauses : 32
% 0.80/1.02 % Processed clauses : 134
% 0.80/1.02 % Factors computed : 0
% 0.80/1.02 % Resolvents computed: 517
% 0.80/1.02 % Tautologies deleted: 0
% 0.80/1.02 % Forward subsumed : 58
% 0.80/1.02 % Backward subsumed : 41
% 0.80/1.02 % -------- CPU Time ---------
% 0.80/1.02 % User time : 0.648 s
% 0.80/1.02 % System time : 0.017 s
% 0.80/1.02 % Total time : 0.665 s
%------------------------------------------------------------------------------