%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL416-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:58:27 PM UTC 2026
% Result : Unsatisfiable 209.54s 209.85s
% Output : CNFRefutation 209.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 3
% Syntax : Number of clauses : 23 ( 14 unt; 0 nHn; 9 RR)
% Number of literals : 33 ( 0 equ; 11 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-2 aty)
% Number of variables : 124 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_reflexivity,negated_conjecture,
~ is_a_theorem(equivalent(a,a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_reflexivity) ).
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(xcb,axiom,
is_a_theorem(equivalent(X4,equivalent(equivalent(equivalent(X4,X6),equivalent(X5,X6)),X5))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xcb) ).
cnf(c0,plain,
( ~ is_a_theorem(X7)
| is_a_theorem(equivalent(equivalent(equivalent(X7,X8),equivalent(X9,X8)),X9)) ),
inference(resolution,[status(thm)],[xcb,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X14,equivalent(equivalent(equivalent(X14,X11),equivalent(X12,X11)),X12)),X13),equivalent(X10,X13)),X10)),
inference(resolution,[status(thm)],[c0,xcb]) ).
cnf(c2,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X19,equivalent(equivalent(equivalent(X19,X17),equivalent(X15,X17)),X15)),X16),equivalent(X18,X16)))
| is_a_theorem(X18) ),
inference(resolution,[status(thm)],[c1,condensed_detachment]) ).
cnf(c4,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X23,equivalent(equivalent(equivalent(X23,X24),equivalent(X20,X24)),X20)),X22),X21),equivalent(X22,X21))),
inference(resolution,[status(thm)],[c2,xcb]) ).
cnf(c5,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X28,equivalent(equivalent(equivalent(X28,X26),equivalent(X27,X26)),X27)),X29),X25))
| is_a_theorem(equivalent(X29,X25)) ),
inference(resolution,[status(thm)],[c4,condensed_detachment]) ).
cnf(c8,plain,
is_a_theorem(equivalent(equivalent(X35,equivalent(equivalent(equivalent(equivalent(X40,equivalent(equivalent(equivalent(X40,X39),equivalent(X37,X39)),X37)),X38),equivalent(X36,X38)),X36)),X35)),
inference(resolution,[status(thm)],[c5,c1]) ).
cnf(c11,plain,
( ~ is_a_theorem(equivalent(X68,equivalent(equivalent(equivalent(equivalent(X66,equivalent(equivalent(equivalent(X66,X63),equivalent(X67,X63)),X67)),X65),equivalent(X64,X65)),X64)))
| is_a_theorem(X68) ),
inference(resolution,[status(thm)],[c8,condensed_detachment]) ).
cnf(c30,plain,
is_a_theorem(equivalent(equivalent(equivalent(X467,equivalent(equivalent(equivalent(X467,X463),equivalent(X464,X463)),X464)),equivalent(equivalent(equivalent(X468,equivalent(equivalent(equivalent(X468,X465),equivalent(X466,X465)),X466)),X461),equivalent(X462,X461))),X462)),
inference(resolution,[status(thm)],[c11,c4]) ).
cnf(c454,plain,
( ~ is_a_theorem(equivalent(equivalent(X9074,equivalent(equivalent(equivalent(X9074,X9068),equivalent(X9070,X9068)),X9070)),equivalent(equivalent(equivalent(X9069,equivalent(equivalent(equivalent(X9069,X9071),equivalent(X9072,X9071)),X9072)),X9067),equivalent(X9073,X9067))))
| is_a_theorem(X9073) ),
inference(resolution,[status(thm)],[c30,condensed_detachment]) ).
cnf(c3,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X50,equivalent(equivalent(equivalent(X50,X49),equivalent(X46,X49)),X46)),X48),equivalent(X45,X48)),X45),X47),equivalent(X44,X47)),X44)),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c15,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X101,equivalent(equivalent(equivalent(X101,X102),equivalent(X96,X102)),X96)),X100),equivalent(X97,X100)),X97),X98),equivalent(X99,X98)))
| is_a_theorem(X99) ),
inference(resolution,[status(thm)],[c3,condensed_detachment]) ).
cnf(c51,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X132,equivalent(equivalent(equivalent(X132,X134),equivalent(X135,X134)),X135)),X133),equivalent(X129,X133)),X129),X130),X131),equivalent(X130,X131))),
inference(resolution,[status(thm)],[c15,xcb]) ).
cnf(c65,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X172,equivalent(equivalent(equivalent(X172,X176),equivalent(X175,X176)),X175)),X174),equivalent(X173,X174)),X173),X177),X171))
| is_a_theorem(equivalent(X177,X171)) ),
inference(resolution,[status(thm)],[c51,condensed_detachment]) ).
cnf(c9,plain,
is_a_theorem(equivalent(X55,equivalent(equivalent(equivalent(equivalent(equivalent(X54,equivalent(equivalent(equivalent(X54,X56),equivalent(X53,X56)),X53)),X55),X51),equivalent(X52,X51)),X52))),
inference(resolution,[status(thm)],[c5,xcb]) ).
cnf(c18,plain,
( ~ is_a_theorem(X88)
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X87,equivalent(equivalent(equivalent(X87,X84),equivalent(X85,X84)),X85)),X88),X86),equivalent(X89,X86)),X89)) ),
inference(resolution,[status(thm)],[c9,condensed_detachment]) ).
cnf(c70,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1458,equivalent(equivalent(equivalent(X1458,X1461),equivalent(X1465,X1461)),X1465)),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X1460,equivalent(equivalent(equivalent(X1460,X1466),equivalent(X1463,X1466)),X1463)),X1464),equivalent(X1462,X1464)),X1462),X1469),X1459),equivalent(X1469,X1459))),X1468),equivalent(X1467,X1468)),X1467)),
inference(resolution,[status(thm)],[c51,c18]) ).
cnf(c1620,plain,
is_a_theorem(equivalent(equivalent(X37719,equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X37713,equivalent(equivalent(equivalent(X37713,X37712),equivalent(X37709,X37712)),X37709)),X37714),equivalent(X37715,X37714)),X37715),equivalent(equivalent(equivalent(X37718,equivalent(equivalent(equivalent(X37718,X37710),equivalent(X37711,X37710)),X37711)),X37717),equivalent(X37716,X37717))),X37716)),X37719)),
inference(resolution,[status(thm)],[c70,c65]) ).
cnf(c84152,plain,
is_a_theorem(equivalent(equivalent(equivalent(X37748,equivalent(equivalent(equivalent(X37748,X37746),equivalent(X37747,X37746)),X37747)),X37745),X37745)),
inference(resolution,[status(thm)],[c1620,c454]) ).
cnf(c84243,plain,
is_a_theorem(equivalent(X37749,X37749)),
inference(resolution,[status(thm)],[c84152,c5]) ).
cnf(c84326,plain,
$false,
inference(resolution,[status(thm)],[c84243,prove_reflexivity]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL416-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.36 % Computer : n019.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 : Sat Sep 5 12:12:08 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.42 (re.compile("\."), Token.FullStop),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.42 (re.compile("\("), Token.OpenPar),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.42 (re.compile("\)"), Token.ClosePar),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.42 (re.compile("\["), Token.OpenSquare),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("~\|"), Token.Nor),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("\|"), Token.Or),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.42 (re.compile("\?"), Token.Existential),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.50 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.32/0.59 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.59 """
% 209.54/209.85 % Version: 1.5
% 209.54/209.85 % SZS status Unsatisfiable
% 209.54/209.85 % SZS output start CNFRefutation
% See solution above
% 209.54/209.85
% 209.54/209.85 % Initial clauses : 3
% 209.54/209.85 % Processed clauses : 1212
% 209.54/209.85 % Factors computed : 0
% 209.54/209.85 % Resolvents computed: 84452
% 209.54/209.85 % Tautologies deleted: 1
% 209.54/209.85 % Forward subsumed : 6037
% 209.54/209.85 % Backward subsumed : 2
% 209.54/209.85 % -------- CPU Time ---------
% 209.54/209.85 % User time : 209.143 s
% 209.54/209.85 % System time : 0.330 s
% 209.54/209.85 % Total time : 209.473 s
%------------------------------------------------------------------------------