%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO664-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:06 EDT 2024
% Result : Unsatisfiable 10.96s 11.16s
% Output : Refutation 10.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 10
% Syntax : Number of clauses : 33 ( 8 unt; 10 nHn; 26 RR)
% Number of literals : 131 ( 0 equ; 100 neg)
% Maximal clause size : 14 ( 3 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 44 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_70,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_70) ).
cnf(clause_94,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_94) ).
cnf(clause_58,axiom,
'LE'(f(X2),s(s('0'))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_58) ).
cnf(clause_20,axiom,
( ~ 'LE'(f(X12),s(s('0')))
| 'E'(s('0'),f(X12))
| 'LE'(f(X12),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_20) ).
cnf(c8,plain,
( 'E'(s('0'),f(X13))
| 'LE'(f(X13),s('0')) ),
inference(resolution,[status(thm)],[clause_20,clause_58]) ).
cnf(clause_50,axiom,
( ~ 'E'(s('0'),f(X11))
| ~ 'E'(s('0'),f(suc(X11)))
| iLEQ(suc(X11),suc(X11)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_50) ).
cnf(clause_83,axiom,
( ~ 'LE'(f(suc(X23)),s(s('0')))
| 'E'(s('0'),f(suc(X23)))
| 'LE'(f(X23),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_83) ).
cnf(c47,plain,
( 'E'(s('0'),f(suc(X24)))
| 'LE'(f(X24),s('0')) ),
inference(resolution,[status(thm)],[clause_83,clause_58]) ).
cnf(c48,plain,
( 'LE'(f(X26),s('0'))
| ~ 'E'(s('0'),f(X26))
| iLEQ(suc(X26),suc(X26)) ),
inference(resolution,[status(thm)],[c47,clause_50]) ).
cnf(c62,plain,
( 'LE'(f(X27),s('0'))
| iLEQ(suc(X27),suc(X27)) ),
inference(resolution,[status(thm)],[c48,c8]) ).
cnf(clause_37,axiom,
( ~ 'E'(s('0'),f(suc(X7)))
| ~ 'E'(s('0'),f(X7))
| ~ 'E'(s('0'),f(suc(X9)))
| ~ 'E'(s('0'),f(suc(X6)))
| ~ 'E'(s('0'),f(X10))
| ~ 'E'(s('0'),f(suc(X10)))
| ~ iLEQ(suc(X10),suc(X6))
| ~ 'E'(s('0'),f(X6))
| ~ iLEQ(suc(X8),suc(X7))
| ~ 'E'(s('0'),f(X9))
| ~ 'E'(s('0'),f(X8))
| ~ iLEQ(suc(X7),suc(X9))
| ~ iLEQ(suc(X6),suc(X8))
| ~ 'E'(s('0'),f(suc(X8))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_37) ).
cnf(c0,plain,
( ~ 'E'(s('0'),f(suc(X30)))
| ~ 'E'(s('0'),f(X30))
| ~ 'E'(s('0'),f(suc(X29)))
| ~ 'E'(s('0'),f(suc(X28)))
| ~ 'E'(s('0'),f(X31))
| ~ 'E'(s('0'),f(suc(X31)))
| ~ iLEQ(suc(X31),suc(X28))
| ~ 'E'(s('0'),f(X28))
| ~ iLEQ(suc(X30),suc(X30))
| ~ 'E'(s('0'),f(X29))
| ~ iLEQ(suc(X30),suc(X29))
| ~ iLEQ(suc(X28),suc(X30)) ),
inference(factor,[status(thm)],[clause_37]) ).
cnf(c72,plain,
( ~ 'E'(s('0'),f(suc(X209)))
| ~ 'E'(s('0'),f(X209))
| ~ 'E'(s('0'),f(suc(X207)))
| ~ 'E'(s('0'),f(suc(X208)))
| ~ iLEQ(suc(X209),suc(X208))
| ~ 'E'(s('0'),f(X208))
| ~ iLEQ(suc(X209),suc(X209))
| ~ 'E'(s('0'),f(X207))
| ~ iLEQ(suc(X209),suc(X207))
| ~ iLEQ(suc(X208),suc(X209)) ),
inference(factor,[status(thm)],[c0]) ).
cnf(c871,plain,
( ~ 'E'(s('0'),f(suc(X372)))
| ~ 'E'(s('0'),f(X372))
| ~ 'E'(s('0'),f(suc(X371)))
| ~ iLEQ(suc(X372),suc(X372))
| ~ 'E'(s('0'),f(X371))
| ~ iLEQ(suc(X372),suc(X371)) ),
inference(factor,[status(thm)],[c72]) ).
cnf(c1930,plain,
( ~ 'E'(s('0'),f(suc(X373)))
| ~ 'E'(s('0'),f(X373))
| ~ iLEQ(suc(X373),suc(X373)) ),
inference(factor,[status(thm)],[c871]) ).
cnf(c1950,plain,
( ~ 'E'(s('0'),f(X374))
| ~ iLEQ(suc(X374),suc(X374))
| 'LE'(f(X374),s('0')) ),
inference(resolution,[status(thm)],[c1930,c47]) ).
cnf(c1983,plain,
( ~ 'E'(s('0'),f(X375))
| 'LE'(f(X375),s('0')) ),
inference(resolution,[status(thm)],[c1950,c62]) ).
cnf(c2032,plain,
'LE'(f(X376),s('0')),
inference(resolution,[status(thm)],[c1983,c8]) ).
cnf(c2035,plain,
( 'E'('0',f(X381))
| 'LE'(f(X381),'0') ),
inference(resolution,[status(thm)],[c2032,clause_94]) ).
cnf(c2090,plain,
'E'('0',f(z)),
inference(resolution,[status(thm)],[c2035,clause_70]) ).
cnf(clause_117,axiom,
( ~ 'LE'(f(suc(X5)),s('0'))
| 'E'('0',f(suc(X5)))
| 'LE'(f(X5),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_117) ).
cnf(c2036,plain,
( 'E'('0',f(suc(X382)))
| 'LE'(f(X382),'0') ),
inference(resolution,[status(thm)],[c2032,clause_117]) ).
cnf(c2117,plain,
'E'('0',f(suc(z))),
inference(resolution,[status(thm)],[c2036,clause_70]) ).
cnf(clause_6,axiom,
( ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(X4)))
| iLEQ(suc(X4),suc(X4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6) ).
cnf(c2131,plain,
( ~ 'E'('0',f(z))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c2117,clause_6]) ).
cnf(c2137,plain,
iLEQ(suc(z),suc(z)),
inference(resolution,[status(thm)],[c2131,c2090]) ).
cnf(clause_66,axiom,
( ~ 'E'('0',f(X18))
| ~ 'E'('0',f(suc(X17)))
| ~ 'E'('0',f(suc(X16)))
| ~ iLEQ(suc(X16),suc(X17))
| ~ iLEQ(suc(X17),suc(X19))
| ~ 'E'('0',f(suc(X18)))
| ~ 'E'('0',f(X16))
| ~ iLEQ(suc(X19),suc(X18))
| ~ 'E'('0',f(X15))
| ~ iLEQ(suc(X18),suc(X15))
| ~ 'E'('0',f(suc(X19)))
| ~ 'E'('0',f(X17))
| ~ 'E'('0',f(suc(X15)))
| ~ 'E'('0',f(X19)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_66) ).
cnf(c20,plain,
( ~ 'E'('0',f(X115))
| ~ 'E'('0',f(suc(X116)))
| ~ 'E'('0',f(suc(X117)))
| ~ iLEQ(suc(X117),suc(X116))
| ~ iLEQ(suc(X116),suc(X118))
| ~ 'E'('0',f(suc(X115)))
| ~ 'E'('0',f(X117))
| ~ iLEQ(suc(X118),suc(X115))
| ~ iLEQ(suc(X115),suc(X115))
| ~ 'E'('0',f(suc(X118)))
| ~ 'E'('0',f(X116))
| ~ 'E'('0',f(X118)) ),
inference(factor,[status(thm)],[clause_66]) ).
cnf(c449,plain,
( ~ 'E'('0',f(X698))
| ~ 'E'('0',f(suc(X700)))
| ~ 'E'('0',f(suc(X699)))
| ~ iLEQ(suc(X699),suc(X700))
| ~ iLEQ(suc(X700),suc(X698))
| ~ 'E'('0',f(suc(X698)))
| ~ 'E'('0',f(X699))
| ~ iLEQ(suc(X698),suc(X698))
| ~ 'E'('0',f(X700)) ),
inference(factor,[status(thm)],[c20]) ).
cnf(c2220,plain,
( ~ 'E'('0',f(X701))
| ~ 'E'('0',f(suc(X701)))
| ~ iLEQ(suc(X701),suc(X701)) ),
inference(factor,[status(thm)],[c449]) ).
cnf(c2228,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[c2220,c2137]) ).
cnf(c2230,plain,
~ 'E'('0',f(z)),
inference(resolution,[status(thm)],[c2228,c2117]) ).
cnf(c2234,plain,
$false,
inference(resolution,[status(thm)],[c2230,c2090]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYO664-1 : TPTP v8.1.2. Released v7.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n016.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 17:48:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 10.96/11.16 % Version: 1.5
% 10.96/11.16 % SZS status Unsatisfiable
% 10.96/11.16 % SZS output start CNFRefutation
% See solution above
% 10.96/11.16
% 10.96/11.16 % Initial clauses : 10
% 10.96/11.16 % Processed clauses : 183
% 10.96/11.16 % Factors computed : 337
% 10.96/11.16 % Resolvents computed: 1898
% 10.96/11.16 % Tautologies deleted: 4
% 10.96/11.16 % Forward subsumed : 473
% 10.96/11.16 % Backward subsumed : 134
% 10.96/11.16 % -------- CPU Time ---------
% 10.96/11.16 % User time : 10.779 s
% 10.96/11.16 % System time : 0.021 s
% 10.96/11.16 % Total time : 10.800 s
%------------------------------------------------------------------------------