%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL009-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.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:41 PM UTC 2026
% Result : Unsatisfiable 37.65s 37.96s
% Output : CNFRefutation 37.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 3
% Syntax : Number of clauses : 25 ( 17 unt; 0 nHn; 7 RR)
% Number of literals : 34 ( 0 equ; 10 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 : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 60 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_ec_5,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(equivalent(a,b),c),equivalent(a,equivalent(b,c)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_ec_5) ).
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(yql,axiom,
is_a_theorem(equivalent(equivalent(X4,X5),equivalent(equivalent(X6,X5),equivalent(X4,X6)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',yql) ).
cnf(c0,plain,
( ~ is_a_theorem(equivalent(X9,X8))
| is_a_theorem(equivalent(equivalent(X7,X8),equivalent(X9,X7))) ),
inference(resolution,[status(thm)],[yql,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(equivalent(equivalent(X10,equivalent(equivalent(X13,X11),equivalent(X12,X13))),equivalent(equivalent(X12,X11),X10))),
inference(resolution,[status(thm)],[c0,yql]) ).
cnf(c3,plain,
( ~ is_a_theorem(equivalent(X22,equivalent(equivalent(X21,X20),equivalent(X19,X21))))
| is_a_theorem(equivalent(equivalent(X19,X20),X22)) ),
inference(resolution,[status(thm)],[c1,condensed_detachment]) ).
cnf(c7,plain,
is_a_theorem(equivalent(equivalent(X24,X23),equivalent(X24,X23))),
inference(resolution,[status(thm)],[c3,yql]) ).
cnf(c9,plain,
is_a_theorem(equivalent(equivalent(X27,equivalent(X29,X28)),equivalent(equivalent(X29,X28),X27))),
inference(resolution,[status(thm)],[c7,c0]) ).
cnf(c14,plain,
is_a_theorem(equivalent(equivalent(X44,X45),equivalent(equivalent(X44,X46),equivalent(X46,X45)))),
inference(resolution,[status(thm)],[c9,c3]) ).
cnf(c25,plain,
( ~ is_a_theorem(equivalent(X97,X98))
| is_a_theorem(equivalent(equivalent(X97,X96),equivalent(X96,X98))) ),
inference(resolution,[status(thm)],[c14,condensed_detachment]) ).
cnf(c13,plain,
( ~ is_a_theorem(equivalent(X41,equivalent(X40,X39)))
| is_a_theorem(equivalent(equivalent(X40,X39),X41)) ),
inference(resolution,[status(thm)],[c9,condensed_detachment]) ).
cnf(c18,plain,
is_a_theorem(equivalent(equivalent(equivalent(X86,X87),equivalent(X88,X86)),equivalent(X88,X87))),
inference(resolution,[status(thm)],[c13,yql]) ).
cnf(c73,plain,
( ~ is_a_theorem(equivalent(equivalent(X139,X138),equivalent(X140,X139)))
| is_a_theorem(equivalent(X140,X138)) ),
inference(resolution,[status(thm)],[c18,condensed_detachment]) ).
cnf(c27,plain,
is_a_theorem(equivalent(equivalent(X47,X47),equivalent(X48,X48))),
inference(resolution,[status(thm)],[c14,c3]) ).
cnf(c29,plain,
( ~ is_a_theorem(equivalent(X50,X50))
| is_a_theorem(equivalent(X49,X49)) ),
inference(resolution,[status(thm)],[c27,condensed_detachment]) ).
cnf(c32,plain,
is_a_theorem(equivalent(X56,X56)),
inference(resolution,[status(thm)],[c29,c27]) ).
cnf(c43,plain,
is_a_theorem(equivalent(equivalent(X68,X69),equivalent(X69,X68))),
inference(resolution,[status(thm)],[c32,c0]) ).
cnf(c54,plain,
( ~ is_a_theorem(equivalent(X73,X72))
| is_a_theorem(equivalent(X72,X73)) ),
inference(resolution,[status(thm)],[c43,condensed_detachment]) ).
cnf(c26,plain,
is_a_theorem(equivalent(equivalent(equivalent(X102,X101),equivalent(X101,X103)),equivalent(X102,X103))),
inference(resolution,[status(thm)],[c14,c13]) ).
cnf(c143,plain,
is_a_theorem(equivalent(X145,equivalent(X144,equivalent(X145,X144)))),
inference(resolution,[status(thm)],[c73,c26]) ).
cnf(c156,plain,
is_a_theorem(equivalent(equivalent(X161,equivalent(X160,X161)),X160)),
inference(resolution,[status(thm)],[c143,c54]) ).
cnf(c196,plain,
is_a_theorem(equivalent(X201,equivalent(equivalent(X201,X202),X202))),
inference(resolution,[status(thm)],[c156,c73]) ).
cnf(c268,plain,
is_a_theorem(equivalent(equivalent(X1107,X1109),equivalent(X1109,equivalent(equivalent(X1107,X1108),X1108)))),
inference(resolution,[status(thm)],[c196,c25]) ).
cnf(c2529,plain,
is_a_theorem(equivalent(equivalent(equivalent(X8747,X8748),X8746),equivalent(X8747,equivalent(X8748,X8746)))),
inference(resolution,[status(thm)],[c268,c3]) ).
cnf(c43044,plain,
$false,
inference(resolution,[status(thm)],[c2529,prove_ec_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL009-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 : n002.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 : Sat Sep 5 03:02:50 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.42 (re.compile("\."), Token.FullStop),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.42 (re.compile("\("), Token.OpenPar),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.42 (re.compile("\)"), Token.ClosePar),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.42 (re.compile("\["), Token.OpenSquare),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.42 (re.compile("~\|"), Token.Nor),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.42 (re.compile("\|"), Token.Or),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.42 (re.compile("\?"), Token.Existential),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.49 """
% 0.21/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.49 """
% 0.32/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 37.65/37.96 % Version: 1.5
% 37.65/37.96 % SZS status Unsatisfiable
% 37.65/37.96 % SZS output start CNFRefutation
% See solution above
% 37.65/37.97
% 37.65/37.97 % Initial clauses : 3
% 37.65/37.97 % Processed clauses : 771
% 37.65/37.97 % Factors computed : 0
% 37.65/37.97 % Resolvents computed: 43146
% 37.65/37.97 % Tautologies deleted: 2
% 37.65/37.97 % Forward subsumed : 2635
% 37.65/37.97 % Backward subsumed : 10
% 37.65/37.97 % -------- CPU Time ---------
% 37.65/37.97 % User time : 37.443 s
% 37.65/37.97 % System time : 0.155 s
% 37.65/37.97 % Total time : 37.598 s
%------------------------------------------------------------------------------