%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL067-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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 : Mon Sep 7 12:57:47 PM UTC 2026
% Result : Unsatisfiable 229.15s 229.41s
% Output : CNFRefutation 229.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 5
% Syntax : Number of clauses : 28 ( 19 unt; 0 nHn; 9 RR)
% Number of literals : 38 ( 0 equ; 11 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 82 ( 22 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_1,negated_conjecture,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_cn_1) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X2,X3))
| ~ is_a_theorem(X2)
| is_a_theorem(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(cn_19,axiom,
is_a_theorem(implies(implies(implies(X5,X6),X4),implies(X6,X4))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_19) ).
cnf(c0,plain,
( ~ is_a_theorem(implies(implies(X8,X9),X7))
| is_a_theorem(implies(X9,X7)) ),
inference(resolution,[status(thm)],[cn_19,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(implies(X10,implies(X11,X10))),
inference(resolution,[status(thm)],[c0,cn_19]) ).
cnf(cn_37,axiom,
is_a_theorem(implies(implies(implies(X15,X16),X14),implies(not(X15),X14))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_37) ).
cnf(c6,plain,
( ~ is_a_theorem(implies(implies(X77,X79),X78))
| is_a_theorem(implies(not(X77),X78)) ),
inference(resolution,[status(thm)],[cn_37,condensed_detachment]) ).
cnf(c51,plain,
is_a_theorem(implies(not(X80),implies(X81,implies(X80,X82)))),
inference(resolution,[status(thm)],[c6,c1]) ).
cnf(cn_59,axiom,
is_a_theorem(implies(implies(not(X32),X31),implies(implies(X33,X31),implies(implies(X32,X33),X31)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_59) ).
cnf(c20,plain,
( ~ is_a_theorem(implies(not(X195),X193))
| is_a_theorem(implies(implies(X194,X193),implies(implies(X195,X194),X193))) ),
inference(resolution,[status(thm)],[cn_59,condensed_detachment]) ).
cnf(c147,plain,
is_a_theorem(implies(implies(X1553,implies(X1550,implies(X1551,X1552))),implies(implies(X1551,X1553),implies(X1550,implies(X1551,X1552))))),
inference(resolution,[status(thm)],[c20,c51]) ).
cnf(c1132,plain,
( ~ is_a_theorem(implies(X18869,implies(X18866,implies(X18868,X18867))))
| is_a_theorem(implies(implies(X18868,X18869),implies(X18866,implies(X18868,X18867)))) ),
inference(resolution,[status(thm)],[c147,condensed_detachment]) ).
cnf(c3,plain,
is_a_theorem(implies(X19,implies(X20,implies(X21,X19)))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c54,plain,
is_a_theorem(implies(not(implies(X84,X85)),implies(X85,X83))),
inference(resolution,[status(thm)],[c6,cn_19]) ).
cnf(c140,plain,
is_a_theorem(implies(implies(X831,implies(X830,X832)),implies(implies(implies(X829,X830),X831),implies(X830,X832)))),
inference(resolution,[status(thm)],[c20,c54]) ).
cnf(c474,plain,
( ~ is_a_theorem(implies(X1033,implies(X1034,X1036)))
| is_a_theorem(implies(implies(implies(X1035,X1034),X1033),implies(X1034,X1036))) ),
inference(resolution,[status(thm)],[c140,condensed_detachment]) ).
cnf(c601,plain,
is_a_theorem(implies(implies(implies(X1140,X1137),not(X1138)),implies(X1137,implies(X1138,X1139)))),
inference(resolution,[status(thm)],[c474,c51]) ).
cnf(c577,plain,
is_a_theorem(implies(implies(implies(X1231,X1232),implies(implies(X1230,X1232),X1229)),implies(X1232,X1229))),
inference(resolution,[status(thm)],[c474,cn_19]) ).
cnf(c776,plain,
( ~ is_a_theorem(implies(implies(X1464,X1462),implies(implies(X1463,X1462),X1465)))
| is_a_theorem(implies(X1462,X1465)) ),
inference(resolution,[status(thm)],[c577,condensed_detachment]) ).
cnf(c1018,plain,
is_a_theorem(implies(not(X1503),implies(X1503,X1502))),
inference(resolution,[status(thm)],[c776,c601]) ).
cnf(c1086,plain,
is_a_theorem(implies(implies(X3065,implies(X3063,X3064)),implies(implies(X3063,X3065),implies(X3063,X3064)))),
inference(resolution,[status(thm)],[c1018,c20]) ).
cnf(c2012,plain,
( ~ is_a_theorem(implies(X3431,implies(X3432,X3433)))
| is_a_theorem(implies(implies(X3432,X3431),implies(X3432,X3433))) ),
inference(resolution,[status(thm)],[c1086,condensed_detachment]) ).
cnf(c2290,plain,
is_a_theorem(implies(implies(X3451,X3450),implies(X3451,implies(X3452,X3450)))),
inference(resolution,[status(thm)],[c2012,c3]) ).
cnf(c31442,plain,
is_a_theorem(implies(implies(X25798,implies(X25800,X25799)),implies(X25800,implies(X25798,X25799)))),
inference(resolution,[status(thm)],[c1132,c2290]) ).
cnf(c56413,plain,
( ~ is_a_theorem(implies(X35327,implies(X35325,X35326)))
| is_a_theorem(implies(X35325,implies(X35327,X35326))) ),
inference(resolution,[status(thm)],[c31442,condensed_detachment]) ).
cnf(c86955,plain,
is_a_theorem(implies(X35418,implies(implies(X35418,X35417),implies(X35416,X35417)))),
inference(resolution,[status(thm)],[c56413,c2290]) ).
cnf(c88090,plain,
is_a_theorem(implies(implies(X41929,X41928),implies(implies(X41928,X41930),implies(X41929,X41930)))),
inference(resolution,[status(thm)],[c86955,c1132]) ).
cnf(c115070,plain,
$false,
inference(resolution,[status(thm)],[c88090,prove_cn_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL067-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.37 % Computer : n028.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 5 16:28:29 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.43 (re.compile("\."), Token.FullStop),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.43 (re.compile("\("), Token.OpenPar),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.43 (re.compile("\)"), Token.ClosePar),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.43 (re.compile("\["), Token.OpenSquare),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("~\|"), Token.Nor),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("\|"), Token.Or),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.43 (re.compile("\?"), Token.Existential),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.50 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.22/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.32/0.59 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.59 """
% 229.15/229.41 % Version: 1.5
% 229.15/229.41 % SZS status Unsatisfiable
% 229.15/229.41 % SZS output start CNFRefutation
% See solution above
% 229.15/229.41
% 229.15/229.41 % Initial clauses : 5
% 229.15/229.41 % Processed clauses : 1258
% 229.15/229.41 % Factors computed : 0
% 229.15/229.41 % Resolvents computed: 115093
% 229.15/229.41 % Tautologies deleted: 1
% 229.15/229.41 % Forward subsumed : 10139
% 229.15/229.41 % Backward subsumed : 4
% 229.15/229.41 % -------- CPU Time ---------
% 229.15/229.41 % User time : 228.751 s
% 229.15/229.41 % System time : 0.280 s
% 229.15/229.41 % Total time : 229.031 s
%------------------------------------------------------------------------------