%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL379-1 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:22 PM UTC 2026
% Result : Unsatisfiable 50.15s 50.42s
% Output : CNFRefutation 50.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 5
% Syntax : Number of clauses : 57 ( 42 unt; 0 nHn; 11 RR)
% Number of literals : 73 ( 0 equ; 17 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 : 3 ( 3 usr; 1 con; 0-2 aty)
% Number of variables : 144 ( 43 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_38,negated_conjecture,
~ is_a_theorem(implies(implies(x,not(x)),not(x))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_cn_38) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X5,X6))
| ~ is_a_theorem(X5)
| is_a_theorem(X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(cn_1,axiom,
is_a_theorem(implies(implies(X11,X12),implies(implies(X12,X10),implies(X11,X10)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_1) ).
cnf(c5,plain,
( ~ is_a_theorem(implies(X31,X30))
| is_a_theorem(implies(implies(X30,X32),implies(X31,X32))) ),
inference(resolution,[status(thm)],[cn_1,condensed_detachment]) ).
cnf(c16,plain,
is_a_theorem(implies(implies(implies(implies(X131,X133),implies(X132,X133)),X130),implies(implies(X132,X131),X130))),
inference(resolution,[status(thm)],[c5,cn_1]) ).
cnf(c130,plain,
( ~ is_a_theorem(implies(implies(implies(X1600,X1602),implies(X1601,X1602)),X1603))
| is_a_theorem(implies(implies(X1601,X1600),X1603)) ),
inference(resolution,[status(thm)],[c16,condensed_detachment]) ).
cnf(cn_2,axiom,
is_a_theorem(implies(implies(not(X2),X2),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_2) ).
cnf(c1,plain,
( ~ is_a_theorem(implies(not(X9),X9))
| is_a_theorem(X9) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_2]) ).
cnf(cn_3,axiom,
is_a_theorem(implies(X3,implies(not(X3),X4))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_3) ).
cnf(c17,plain,
is_a_theorem(implies(implies(implies(not(X34),X35),X33),implies(X34,X33))),
inference(resolution,[status(thm)],[c5,cn_3]) ).
cnf(c22,plain,
( ~ is_a_theorem(implies(implies(not(X47),X45),X46))
| is_a_theorem(implies(X47,X46)) ),
inference(resolution,[status(thm)],[c17,condensed_detachment]) ).
cnf(c0,plain,
( ~ is_a_theorem(X7)
| is_a_theorem(implies(not(X7),X8)) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_3]) ).
cnf(c34,plain,
is_a_theorem(implies(X48,X48)),
inference(resolution,[status(thm)],[c22,cn_2]) ).
cnf(c35,plain,
is_a_theorem(implies(not(implies(X51,X51)),X50)),
inference(resolution,[status(thm)],[c34,c0]) ).
cnf(c42,plain,
is_a_theorem(implies(implies(X121,X119),implies(not(implies(X120,X120)),X119))),
inference(resolution,[status(thm)],[c35,c5]) ).
cnf(c119,plain,
is_a_theorem(implies(X123,implies(not(implies(X122,X122)),X124))),
inference(resolution,[status(thm)],[c42,c22]) ).
cnf(c127,plain,
is_a_theorem(implies(implies(implies(not(implies(X217,X217)),X216),X219),implies(X218,X219))),
inference(resolution,[status(thm)],[c119,c5]) ).
cnf(c244,plain,
( ~ is_a_theorem(implies(implies(not(implies(X222,X222)),X223),X220))
| is_a_theorem(implies(X221,X220)) ),
inference(resolution,[status(thm)],[c127,condensed_detachment]) ).
cnf(c257,plain,
is_a_theorem(implies(X224,implies(X225,X225))),
inference(resolution,[status(thm)],[c244,cn_2]) ).
cnf(c272,plain,
is_a_theorem(implies(implies(implies(X270,X270),X268),implies(X269,X268))),
inference(resolution,[status(thm)],[c257,c5]) ).
cnf(c309,plain,
( ~ is_a_theorem(implies(implies(X273,X273),X272))
| is_a_theorem(implies(X271,X272)) ),
inference(resolution,[status(thm)],[c272,condensed_detachment]) ).
cnf(c324,plain,
is_a_theorem(implies(X284,implies(X282,implies(X283,X283)))),
inference(resolution,[status(thm)],[c309,c272]) ).
cnf(c338,plain,
is_a_theorem(implies(implies(implies(X421,implies(X420,X420)),X418),implies(X419,X418))),
inference(resolution,[status(thm)],[c324,c5]) ).
cnf(c20,plain,
is_a_theorem(implies(implies(X37,X36),implies(implies(not(X37),X37),X36))),
inference(resolution,[status(thm)],[c5,cn_2]) ).
cnf(c329,plain,
is_a_theorem(implies(X311,implies(implies(not(X310),X310),X310))),
inference(resolution,[status(thm)],[c309,c20]) ).
cnf(c360,plain,
is_a_theorem(implies(implies(implies(implies(not(X845),X845),X845),X843),implies(X844,X843))),
inference(resolution,[status(thm)],[c329,c5]) ).
cnf(c1306,plain,
is_a_theorem(implies(implies(X3030,implies(not(X3031),X3031)),implies(X3032,implies(X3030,X3031)))),
inference(resolution,[status(thm)],[c130,c360]) ).
cnf(c3426,plain,
( ~ is_a_theorem(implies(X4266,implies(not(X4267),X4267)))
| is_a_theorem(implies(X4265,implies(X4266,X4267))) ),
inference(resolution,[status(thm)],[c1306,condensed_detachment]) ).
cnf(c5505,plain,
is_a_theorem(implies(X4517,implies(implies(implies(X4519,implies(X4518,X4518)),X4520),X4520))),
inference(resolution,[status(thm)],[c3426,c338]) ).
cnf(c6160,plain,
is_a_theorem(implies(implies(implies(X4524,implies(X4525,X4525)),X4523),X4523)),
inference(resolution,[status(thm)],[c5505,c1]) ).
cnf(c6178,plain,
( ~ is_a_theorem(implies(implies(X4569,implies(X4571,X4571)),X4570))
| is_a_theorem(X4570) ),
inference(resolution,[status(thm)],[c6160,condensed_detachment]) ).
cnf(c3425,plain,
is_a_theorem(implies(implies(not(X4147),X4148),implies(X4146,implies(implies(X4148,X4147),X4147)))),
inference(resolution,[status(thm)],[c1306,c130]) ).
cnf(c5010,plain,
is_a_theorem(implies(X4158,implies(X4159,implies(implies(X4160,X4158),X4158)))),
inference(resolution,[status(thm)],[c3425,c22]) ).
cnf(c5397,plain,
is_a_theorem(implies(X4308,implies(X4310,implies(implies(X4309,X4310),X4310)))),
inference(resolution,[status(thm)],[c3426,c5010]) ).
cnf(c5578,plain,
is_a_theorem(implies(X4312,implies(implies(X4311,X4312),X4312))),
inference(resolution,[status(thm)],[c5397,c1]) ).
cnf(c5600,plain,
is_a_theorem(implies(implies(implies(implies(X4950,X4948),X4948),X4949),implies(X4948,X4949))),
inference(resolution,[status(thm)],[c5578,c5]) ).
cnf(c6744,plain,
is_a_theorem(implies(implies(X5098,implies(X5099,X5100)),implies(X5100,implies(X5098,X5100)))),
inference(resolution,[status(thm)],[c5600,c130]) ).
cnf(c6882,plain,
is_a_theorem(implies(X5101,implies(X5102,X5101))),
inference(resolution,[status(thm)],[c6744,c6178]) ).
cnf(c6909,plain,
is_a_theorem(implies(implies(implies(X5355,X5353),X5354),implies(X5353,X5354))),
inference(resolution,[status(thm)],[c6882,c5]) ).
cnf(c7553,plain,
( ~ is_a_theorem(implies(implies(X5463,X5464),X5465))
| is_a_theorem(implies(X5464,X5465)) ),
inference(resolution,[status(thm)],[c6909,condensed_detachment]) ).
cnf(c8119,plain,
is_a_theorem(implies(X5793,implies(X5791,implies(implies(X5793,X5792),X5792)))),
inference(resolution,[status(thm)],[c7553,c3425]) ).
cnf(c9262,plain,
is_a_theorem(implies(X5900,implies(X5901,implies(implies(X5901,X5902),X5902)))),
inference(resolution,[status(thm)],[c8119,c3426]) ).
cnf(c9790,plain,
is_a_theorem(implies(X5903,implies(implies(X5903,X5904),X5904))),
inference(resolution,[status(thm)],[c9262,c6178]) ).
cnf(c9810,plain,
( ~ is_a_theorem(X5927)
| is_a_theorem(implies(implies(X5927,X5928),X5928)) ),
inference(resolution,[status(thm)],[c9790,condensed_detachment]) ).
cnf(c10114,plain,
is_a_theorem(implies(implies(implies(implies(not(X7434),X7434),X7434),X7433),X7433)),
inference(resolution,[status(thm)],[c9810,cn_2]) ).
cnf(c13550,plain,
is_a_theorem(implies(implies(X8422,implies(not(X8423),X8423)),implies(X8422,X8423))),
inference(resolution,[status(thm)],[c10114,c130]) ).
cnf(c16357,plain,
is_a_theorem(implies(implies(not(X8947),X8948),implies(implies(X8948,X8947),X8947))),
inference(resolution,[status(thm)],[c13550,c130]) ).
cnf(c17443,plain,
( ~ is_a_theorem(implies(not(X9658),X9659))
| is_a_theorem(implies(implies(X9659,X9658),X9658)) ),
inference(resolution,[status(thm)],[c16357,condensed_detachment]) ).
cnf(c16359,plain,
( ~ is_a_theorem(implies(X8981,implies(not(X8980),X8980)))
| is_a_theorem(implies(X8981,X8980)) ),
inference(resolution,[status(thm)],[c13550,condensed_detachment]) ).
cnf(c10092,plain,
is_a_theorem(implies(implies(implies(X7403,implies(not(X7403),X7404)),X7402),X7402)),
inference(resolution,[status(thm)],[c9810,cn_3]) ).
cnf(c13517,plain,
( ~ is_a_theorem(implies(implies(X8225,implies(not(X8225),X8223)),X8224))
| is_a_theorem(X8224) ),
inference(resolution,[status(thm)],[c10092,condensed_detachment]) ).
cnf(c9822,plain,
is_a_theorem(implies(implies(implies(implies(X13054,X13056),X13056),X13055),implies(X13054,X13055))),
inference(resolution,[status(thm)],[c9790,c5]) ).
cnf(c28287,plain,
is_a_theorem(implies(implies(X16898,implies(X16900,X16899)),implies(X16900,implies(X16898,X16899)))),
inference(resolution,[status(thm)],[c9822,c130]) ).
cnf(c38312,plain,
is_a_theorem(implies(not(X16905),implies(X16905,X16906))),
inference(resolution,[status(thm)],[c28287,c13517]) ).
cnf(c38367,plain,
is_a_theorem(implies(not(not(X16913)),X16913)),
inference(resolution,[status(thm)],[c38312,c16359]) ).
cnf(c38397,plain,
is_a_theorem(implies(implies(X17148,not(X17148)),not(X17148))),
inference(resolution,[status(thm)],[c38367,c17443]) ).
cnf(c39854,plain,
$false,
inference(resolution,[status(thm)],[c38397,prove_cn_38]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL379-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.35 % Computer : n003.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 5 01:11:35 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.41 (re.compile("\."), Token.FullStop),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.41 (re.compile("\("), Token.OpenPar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.41 (re.compile("\)"), Token.ClosePar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.41 (re.compile("\["), Token.OpenSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("~\|"), Token.Nor),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("\|"), Token.Or),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.41 (re.compile("\?"), Token.Existential),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.49 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.32/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 50.15/50.42 % Version: 1.5
% 50.15/50.42 % SZS status Unsatisfiable
% 50.15/50.42 % SZS output start CNFRefutation
% See solution above
% 50.15/50.42
% 50.15/50.42 % Initial clauses : 5
% 50.15/50.42 % Processed clauses : 903
% 50.15/50.42 % Factors computed : 0
% 50.15/50.42 % Resolvents computed: 39865
% 50.15/50.42 % Tautologies deleted: 1
% 50.15/50.42 % Forward subsumed : 4384
% 50.15/50.42 % Backward subsumed : 69
% 50.15/50.42 % -------- CPU Time ---------
% 50.15/50.42 % User time : 49.951 s
% 50.15/50.42 % System time : 0.119 s
% 50.15/50.42 % Total time : 50.070 s
%------------------------------------------------------------------------------