%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL102-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:51 PM UTC 2026
% Result : Unsatisfiable 184.59s 184.98s
% Output : CNFRefutation 184.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 5
% Syntax : Number of clauses : 24 ( 16 unt; 0 nHn; 7 RR)
% Number of literals : 33 ( 0 equ; 10 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 82 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_p_1,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(equivalent(a,b),c),equivalent(equivalent(e,b),equivalent(equivalent(a,e),c)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_p_1) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(equivalent(X2,X3))
| ~ is_a_theorem(X2)
| is_a_theorem(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(q_1,axiom,
is_a_theorem(equivalent(X5,equivalent(equivalent(X6,X4),equivalent(equivalent(X4,X6),X5)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',q_1) ).
cnf(q_2,axiom,
is_a_theorem(equivalent(equivalent(X8,X9),equivalent(equivalent(X7,X8),equivalent(X7,X9)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',q_2) ).
cnf(c1,plain,
( ~ is_a_theorem(equivalent(X13,X15))
| is_a_theorem(equivalent(equivalent(X14,X13),equivalent(X14,X15))) ),
inference(resolution,[status(thm)],[q_2,condensed_detachment]) ).
cnf(c4,plain,
is_a_theorem(equivalent(equivalent(X23,X22),equivalent(X23,equivalent(equivalent(X20,X21),equivalent(equivalent(X21,X20),X22))))),
inference(resolution,[status(thm)],[c1,q_1]) ).
cnf(lg_2,axiom,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X17,X19),equivalent(X17,X16)),equivalent(X19,X16)),X18),X18)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lg_2) ).
cnf(c6,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X29,X31),equivalent(X29,X30)),equivalent(X31,X30)),X28))
| is_a_theorem(X28) ),
inference(resolution,[status(thm)],[lg_2,condensed_detachment]) ).
cnf(c17,plain,
is_a_theorem(equivalent(equivalent(X46,equivalent(equivalent(X47,X44),equivalent(X47,X45))),equivalent(X46,equivalent(X44,X45)))),
inference(resolution,[status(thm)],[c6,q_2]) ).
cnf(c34,plain,
( ~ is_a_theorem(equivalent(X248,equivalent(equivalent(X249,X247),equivalent(X249,X246))))
| is_a_theorem(equivalent(X248,equivalent(X247,X246))) ),
inference(resolution,[status(thm)],[c17,condensed_detachment]) ).
cnf(c263,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X739,X740),X741),X738),equivalent(X741,equivalent(equivalent(X740,X739),X738)))),
inference(resolution,[status(thm)],[c34,c4]) ).
cnf(c832,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X4776,X4775),X4774),X4773))
| is_a_theorem(equivalent(X4774,equivalent(equivalent(X4775,X4776),X4773))) ),
inference(resolution,[status(thm)],[c263,condensed_detachment]) ).
cnf(c5,plain,
is_a_theorem(equivalent(equivalent(X27,equivalent(X24,X26)),equivalent(X27,equivalent(equivalent(X25,X24),equivalent(X25,X26))))),
inference(resolution,[status(thm)],[c1,q_2]) ).
cnf(c16,plain,
is_a_theorem(equivalent(equivalent(equivalent(X43,X40),equivalent(X43,X42)),equivalent(equivalent(X41,X40),equivalent(X41,X42)))),
inference(resolution,[status(thm)],[c6,c5]) ).
cnf(c29,plain,
( ~ is_a_theorem(equivalent(equivalent(X57,X59),equivalent(X57,X56)))
| is_a_theorem(equivalent(equivalent(X58,X59),equivalent(X58,X56))) ),
inference(resolution,[status(thm)],[c16,condensed_detachment]) ).
cnf(c55,plain,
is_a_theorem(equivalent(equivalent(X67,equivalent(X65,X66)),equivalent(X67,equivalent(X65,X66)))),
inference(resolution,[status(thm)],[c29,c16]) ).
cnf(c70,plain,
is_a_theorem(equivalent(equivalent(equivalent(X76,X74),equivalent(X76,X75)),equivalent(X74,X75))),
inference(resolution,[status(thm)],[c55,c6]) ).
cnf(c72,plain,
( ~ is_a_theorem(equivalent(equivalent(X79,X78),equivalent(X79,X77)))
| is_a_theorem(equivalent(X78,X77)) ),
inference(resolution,[status(thm)],[c70,condensed_detachment]) ).
cnf(c12,plain,
( ~ is_a_theorem(equivalent(X39,equivalent(X36,X38)))
| is_a_theorem(equivalent(X39,equivalent(equivalent(X37,X36),equivalent(X37,X38)))) ),
inference(resolution,[status(thm)],[c5,condensed_detachment]) ).
cnf(c28,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X364,X368),equivalent(X364,X365)),equivalent(X368,X365)),equivalent(X367,X369)),equivalent(equivalent(X366,X367),equivalent(X366,X369)))),
inference(resolution,[status(thm)],[c12,lg_2]) ).
cnf(c402,plain,
is_a_theorem(equivalent(equivalent(equivalent(X979,X980),X978),equivalent(equivalent(equivalent(X977,X979),equivalent(X977,X980)),X978))),
inference(resolution,[status(thm)],[c28,c72]) ).
cnf(c1151,plain,
is_a_theorem(equivalent(equivalent(equivalent(X5937,X5939),equivalent(equivalent(X5938,X5937),X5936)),equivalent(equivalent(X5938,X5939),X5936))),
inference(resolution,[status(thm)],[c402,c34]) ).
cnf(c19052,plain,
is_a_theorem(equivalent(equivalent(equivalent(X33739,X33737),X33738),equivalent(equivalent(X33736,X33737),equivalent(equivalent(X33739,X33736),X33738)))),
inference(resolution,[status(thm)],[c1151,c832]) ).
cnf(c156722,plain,
$false,
inference(resolution,[status(thm)],[c19052,prove_p_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL102-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 4 17:54:25 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.39 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.39 (re.compile("\."), Token.FullStop),
% 0.09/0.39 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.39 (re.compile("\("), Token.OpenPar),
% 0.09/0.39 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.39 (re.compile("\)"), Token.ClosePar),
% 0.09/0.39 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.39 (re.compile("\["), Token.OpenSquare),
% 0.09/0.39 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.39 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.39 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.39 (re.compile("~\|"), Token.Nor),
% 0.09/0.39 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.39 (re.compile("\|"), Token.Or),
% 0.09/0.39 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.39 (re.compile("\?"), Token.Existential),
% 0.09/0.39 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.39 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.39 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.39 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.09/0.43 """
% 0.09/0.43 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.09/0.43 """
% 0.23/0.47 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.47 """
% 184.59/184.98 % Version: 1.5
% 184.59/184.98 % SZS status Unsatisfiable
% 184.59/184.98 % SZS output start CNFRefutation
% See solution above
% 184.59/184.98
% 184.59/184.98 % Initial clauses : 5
% 184.59/184.98 % Processed clauses : 1770
% 184.59/184.98 % Factors computed : 0
% 184.59/184.98 % Resolvents computed: 156745
% 184.59/184.98 % Tautologies deleted: 3
% 184.59/184.98 % Forward subsumed : 8381
% 184.59/184.98 % Backward subsumed : 2
% 184.59/184.98 % -------- CPU Time ---------
% 184.59/184.98 % User time : 184.211 s
% 184.59/184.98 % System time : 0.335 s
% 184.59/184.98 % Total time : 184.546 s
%------------------------------------------------------------------------------