%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL107-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:52 PM UTC 2026
% Result : Unsatisfiable 0.95s 1.28s
% Output : CNFRefutation 0.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 3
% Syntax : Number of clauses : 20 ( 13 unt; 0 nHn; 8 RR)
% Number of literals : 28 ( 0 equ; 9 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 8 ( 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 : 98 ( 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/sandbox2/benchmark/theBenchmark.p',prove_p_1) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(X3)
| is_a_theorem(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(lg_27_1690,axiom,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X5,X4),X6),equivalent(equivalent(X7,X9),equivalent(equivalent(equivalent(X10,X9),equivalent(X10,X7)),X8))),equivalent(X6,equivalent(equivalent(X4,X5),X8)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lg_27_1690) ).
cnf(c0,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X17,X12),X11),equivalent(equivalent(X16,X14),equivalent(equivalent(equivalent(X13,X14),equivalent(X13,X16)),X15))))
| is_a_theorem(equivalent(X11,equivalent(equivalent(X12,X17),X15))) ),
inference(resolution,[status(thm)],[lg_27_1690,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(equivalent(equivalent(equivalent(X23,X20),equivalent(equivalent(equivalent(X19,X20),equivalent(X19,X23)),X22)),equivalent(equivalent(equivalent(X18,X21),equivalent(equivalent(X24,X18),equivalent(X24,X21))),X22))),
inference(resolution,[status(thm)],[c0,lg_27_1690]) ).
cnf(c3,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X36,X35),equivalent(X36,X38)),equivalent(equivalent(equivalent(X39,equivalent(equivalent(X32,X34),equivalent(X32,X33))),equivalent(X39,equivalent(X34,X33))),X37)),equivalent(equivalent(X35,X38),X37))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c4,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X47,X41),equivalent(X47,X45)),equivalent(equivalent(equivalent(X43,equivalent(equivalent(X42,X40),equivalent(X42,X44))),equivalent(X43,equivalent(X40,X44))),X46)))
| is_a_theorem(equivalent(equivalent(X41,X45),X46)) ),
inference(resolution,[status(thm)],[c3,condensed_detachment]) ).
cnf(c6,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X49,equivalent(equivalent(X48,equivalent(X53,X51)),equivalent(X48,equivalent(X53,X50)))),equivalent(X49,equivalent(X51,X50))),X52),X52)),
inference(resolution,[status(thm)],[c4,c3]) ).
cnf(c8,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X54,equivalent(equivalent(X59,equivalent(X55,X57)),equivalent(X59,equivalent(X55,X58)))),equivalent(X54,equivalent(X57,X58))),X56))
| is_a_theorem(X56) ),
inference(resolution,[status(thm)],[c6,condensed_detachment]) ).
cnf(c5,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X69,equivalent(equivalent(X66,X65),equivalent(X66,X68))),equivalent(X69,equivalent(X65,X68))),equivalent(equivalent(equivalent(X73,X70),equivalent(X73,X67)),X71)),equivalent(equivalent(equivalent(X72,X70),equivalent(X72,X67)),X71))),
inference(resolution,[status(thm)],[c3,c0]) ).
cnf(c17,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X178,equivalent(equivalent(X182,X181),equivalent(X182,X176))),equivalent(X178,equivalent(X181,X176))),equivalent(equivalent(equivalent(X184,X177),equivalent(X184,X183)),X180)))
| is_a_theorem(equivalent(equivalent(equivalent(X179,X177),equivalent(X179,X183)),X180)) ),
inference(resolution,[status(thm)],[c5,condensed_detachment]) ).
cnf(c68,plain,
is_a_theorem(equivalent(equivalent(equivalent(X186,equivalent(equivalent(X189,X187),equivalent(X189,X185))),equivalent(X186,X188)),equivalent(equivalent(X187,X185),X188))),
inference(resolution,[status(thm)],[c17,lg_27_1690]) ).
cnf(c72,plain,
is_a_theorem(equivalent(equivalent(equivalent(X192,X190),equivalent(X192,X191)),equivalent(X190,X191))),
inference(resolution,[status(thm)],[c68,c8]) ).
cnf(c75,plain,
( ~ is_a_theorem(equivalent(equivalent(X195,X193),equivalent(X195,X194)))
| is_a_theorem(equivalent(X193,X194)) ),
inference(resolution,[status(thm)],[c72,condensed_detachment]) ).
cnf(c71,plain,
is_a_theorem(equivalent(equivalent(equivalent(X202,X201),equivalent(X202,X199)),equivalent(equivalent(X200,X201),equivalent(X200,X199)))),
inference(resolution,[status(thm)],[c68,c17]) ).
cnf(c94,plain,
is_a_theorem(equivalent(equivalent(X214,X213),equivalent(X214,X213))),
inference(resolution,[status(thm)],[c71,c75]) ).
cnf(c107,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X257,X258),equivalent(X257,X259)),X256),equivalent(equivalent(X258,X259),X256))),
inference(resolution,[status(thm)],[c94,c0]) ).
cnf(c150,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X302,X301),equivalent(X302,X303)),X300))
| is_a_theorem(equivalent(equivalent(X301,X303),X300)) ),
inference(resolution,[status(thm)],[c107,condensed_detachment]) ).
cnf(c219,plain,
is_a_theorem(equivalent(equivalent(equivalent(X814,X815),X813),equivalent(equivalent(X812,X815),equivalent(equivalent(X814,X812),X813)))),
inference(resolution,[status(thm)],[c150,c107]) ).
cnf(c861,plain,
$false,
inference(resolution,[status(thm)],[c219,prove_p_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL107-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.36 % Computer : n013.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 6 00:57:05 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.08/0.42 (re.compile("\."), Token.FullStop),
% 0.08/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.08/0.42 (re.compile("\("), Token.OpenPar),
% 0.08/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.08/0.42 (re.compile("\)"), Token.ClosePar),
% 0.08/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.08/0.42 (re.compile("\["), Token.OpenSquare),
% 0.08/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.08/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.08/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.08/0.42 (re.compile("~\|"), Token.Nor),
% 0.08/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.08/0.42 (re.compile("\|"), Token.Or),
% 0.08/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.08/0.42 (re.compile("\?"), Token.Existential),
% 0.08/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.08/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.08/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.08/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.49 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.49 """
% 0.21/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.49 """
% 0.31/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.58 """
% 0.95/1.28 % Version: 1.5
% 0.95/1.28 % SZS status Unsatisfiable
% 0.95/1.28 % SZS output start CNFRefutation
% See solution above
% 0.95/1.28
% 0.95/1.28 % Initial clauses : 3
% 0.95/1.28 % Processed clauses : 96
% 0.95/1.28 % Factors computed : 0
% 0.95/1.28 % Resolvents computed: 882
% 0.95/1.28 % Tautologies deleted: 2
% 0.95/1.28 % Forward subsumed : 127
% 0.95/1.28 % Backward subsumed : 1
% 0.95/1.28 % -------- CPU Time ---------
% 0.95/1.28 % User time : 0.895 s
% 0.95/1.28 % System time : 0.024 s
% 0.95/1.28 % Total time : 0.919 s
%------------------------------------------------------------------------------