%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL203-3 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:03 PM UTC 2026
% Result : Unsatisfiable 243.28s 243.61s
% Output : CNFRefutation 243.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of clauses : 42 ( 27 unt; 0 nHn; 14 RR)
% Number of literals : 60 ( 11 equ; 19 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 91 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_this,negated_conjecture,
~ theorem(implies(not(or(p,q)),or(not(p),not(q)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
cnf(c4,axiom,
( X16 != X17
| ~ theorem(X16)
| theorem(X17) ),
theory(equality) ).
cnf(symmetry,axiom,
( X5 != X4
| X4 = X5 ),
theory(equality) ).
cnf(implies_definition,axiom,
implies(X22,X21) = or(not(X22),X21),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',implies_definition) ).
cnf(c12,plain,
or(not(X46),X45) = implies(X46,X45),
inference(resolution,[status(thm)],[implies_definition,symmetry]) ).
cnf(c29,plain,
( ~ theorem(or(not(X107),X108))
| theorem(implies(X107,X108)) ),
inference(resolution,[status(thm)],[c12,c4]) ).
cnf(rule_2,axiom,
( theorem(X24)
| ~ theorem(implies(X23,X24))
| ~ theorem(X23) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',rule_2) ).
cnf(rule_1,axiom,
( theorem(X3)
| ~ axiom(X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',rule_1) ).
cnf(axiom_1_4,axiom,
axiom(implies(or(X19,X18),or(X18,X19))),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',axiom_1_4) ).
cnf(c10,plain,
theorem(implies(or(X43,X44),or(X44,X43))),
inference(resolution,[status(thm)],[axiom_1_4,rule_1]) ).
cnf(c26,plain,
( theorem(or(X56,X55))
| ~ theorem(or(X55,X56)) ),
inference(resolution,[status(thm)],[c10,rule_2]) ).
cnf(axiom_1_3,axiom,
axiom(implies(X9,or(X8,X9))),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',axiom_1_3) ).
cnf(c7,plain,
theorem(implies(X11,or(X12,X11))),
inference(resolution,[status(thm)],[axiom_1_3,rule_1]) ).
cnf(c11,plain,
( ~ theorem(implies(X77,X76))
| theorem(or(not(X77),X76)) ),
inference(resolution,[status(thm)],[implies_definition,c4]) ).
cnf(c48,plain,
theorem(or(not(X82),or(X83,X82))),
inference(resolution,[status(thm)],[c11,c7]) ).
cnf(axiom_1_2,axiom,
axiom(implies(or(X7,X7),X7)),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',axiom_1_2) ).
cnf(c6,plain,
theorem(implies(or(X10,X10),X10)),
inference(resolution,[status(thm)],[axiom_1_2,rule_1]) ).
cnf(c15,plain,
( theorem(X27)
| ~ theorem(or(X27,X27)) ),
inference(resolution,[status(thm)],[rule_2,c6]) ).
cnf(axiom_1_5,axiom,
axiom(implies(or(X30,or(X29,X28)),or(X29,or(X30,X28)))),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',axiom_1_5) ).
cnf(c18,plain,
theorem(implies(or(X99,or(X100,X101)),or(X100,or(X99,X101)))),
inference(resolution,[status(thm)],[axiom_1_5,rule_1]) ).
cnf(c70,plain,
( theorem(or(X352,or(X353,X351)))
| ~ theorem(or(X353,or(X352,X351))) ),
inference(resolution,[status(thm)],[c18,rule_2]) ).
cnf(c327,plain,
theorem(or(X354,or(not(X355),X355))),
inference(resolution,[status(thm)],[c70,c48]) ).
cnf(c331,plain,
theorem(or(not(X356),X356)),
inference(resolution,[status(thm)],[c327,c15]) ).
cnf(c335,plain,
theorem(or(X359,not(X359))),
inference(resolution,[status(thm)],[c331,c26]) ).
cnf(c344,plain,
theorem(implies(X381,not(not(X381)))),
inference(resolution,[status(thm)],[c335,c29]) ).
cnf(axiom_1_6,axiom,
axiom(implies(implies(X42,X41),implies(or(X40,X42),or(X40,X41)))),
file('/export/starexec/sandbox/benchmark/Axioms/LCL004-0.ax',axiom_1_6) ).
cnf(c24,plain,
theorem(implies(implies(X139,X138),implies(or(X137,X139),or(X137,X138)))),
inference(resolution,[status(thm)],[axiom_1_6,rule_1]) ).
cnf(c103,plain,
( theorem(implies(or(X552,X551),or(X552,X553)))
| ~ theorem(implies(X551,X553)) ),
inference(resolution,[status(thm)],[c24,rule_2]) ).
cnf(c747,plain,
theorem(implies(or(X2548,X2547),or(X2548,not(not(X2547))))),
inference(resolution,[status(thm)],[c103,c344]) ).
cnf(c3403,plain,
( theorem(or(X2840,not(not(X2841))))
| ~ theorem(or(X2840,X2841)) ),
inference(resolution,[status(thm)],[c747,rule_2]) ).
cnf(c3855,plain,
theorem(or(not(X3011),not(not(or(X3010,X3011))))),
inference(resolution,[status(thm)],[c3403,c48]) ).
cnf(c4505,plain,
theorem(or(not(not(or(X3233,X3232))),not(X3232))),
inference(resolution,[status(thm)],[c3855,c26]) ).
cnf(c5407,plain,
theorem(implies(not(or(X3234,X3235)),not(X3235))),
inference(resolution,[status(thm)],[c4505,c29]) ).
cnf(c742,plain,
theorem(implies(or(X1373,X1374),or(X1373,or(X1375,X1374)))),
inference(resolution,[status(thm)],[c103,c7]) ).
cnf(c0,axiom,
( X65 != X67
| X66 != X64
| implies(X65,X66) = implies(X67,X64) ),
theory(equality) ).
cnf(c43,plain,
( X250 != X251
| implies(X250,or(not(X248),X249)) = implies(X251,implies(X248,X249)) ),
inference(resolution,[status(thm)],[c0,c12]) ).
cnf(c198,plain,
implies(or(not(X1381),X1383),or(not(X1382),X1380)) = implies(implies(X1381,X1383),implies(X1382,X1380)),
inference(resolution,[status(thm)],[c43,c12]) ).
cnf(c2169,plain,
( ~ theorem(implies(or(not(X25083),X25084),or(not(X25081),X25082)))
| theorem(implies(implies(X25083,X25084),implies(X25081,X25082))) ),
inference(resolution,[status(thm)],[c198,c4]) ).
cnf(c93351,plain,
theorem(implies(implies(X26245,X26244),implies(X26245,or(X26246,X26244)))),
inference(resolution,[status(thm)],[c2169,c742]) ).
cnf(c99146,plain,
( theorem(implies(X27452,or(X27451,X27453)))
| ~ theorem(implies(X27452,X27453)) ),
inference(resolution,[status(thm)],[c93351,rule_2]) ).
cnf(c107077,plain,
theorem(implies(not(or(X40292,X40290)),or(X40291,not(X40290)))),
inference(resolution,[status(thm)],[c99146,c5407]) ).
cnf(c175224,plain,
$false,
inference(resolution,[status(thm)],[c107077,prove_this]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL203-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.02 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sat Sep 5 13:13:27 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.08/0.34 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.08/0.34 (re.compile("\."), Token.FullStop),
% 0.08/0.34 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.08/0.34 (re.compile("\("), Token.OpenPar),
% 0.08/0.34 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.08/0.34 (re.compile("\)"), Token.ClosePar),
% 0.08/0.34 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.08/0.34 (re.compile("\["), Token.OpenSquare),
% 0.08/0.34 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.08/0.34 (re.compile("\]"), Token.CloseSquare),
% 0.08/0.34 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.08/0.34 (re.compile("~\|"), Token.Nor),
% 0.08/0.34 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.08/0.34 (re.compile("\|"), Token.Or),
% 0.08/0.34 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.08/0.34 (re.compile("\?"), Token.Existential),
% 0.08/0.34 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.08/0.34 (re.compile("\s+"), Token.WhiteSpace),
% 0.08/0.34 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.08/0.34 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.08/0.37 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.08/0.37 """
% 0.08/0.37 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.08/0.37 """
% 0.08/0.41 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.08/0.41 """
% 243.28/243.61 % Version: 1.5
% 243.28/243.61 % SZS status Unsatisfiable
% 243.28/243.61 % SZS output start CNFRefutation
% See solution above
% 243.28/243.61
% 243.28/243.61 % Initial clauses : 17
% 243.28/243.61 % Processed clauses : 2947
% 243.28/243.61 % Factors computed : 3
% 243.28/243.61 % Resolvents computed: 175248
% 243.28/243.61 % Tautologies deleted: 5
% 243.28/243.61 % Forward subsumed : 11754
% 243.28/243.61 % Backward subsumed : 93
% 243.28/243.61 % -------- CPU Time ---------
% 243.28/243.61 % User time : 242.946 s
% 243.28/243.61 % System time : 0.285 s
% 243.28/243.61 % Total time : 243.231 s
%------------------------------------------------------------------------------