%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL132-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:55 PM UTC 2026
% Result : Unsatisfiable 0.67s 0.99s
% Output : CNFRefutation 0.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 7
% Syntax : Number of clauses : 23 ( 14 unt; 0 nHn; 9 RR)
% Number of literals : 34 ( 33 equ; 12 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 42 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_wajsberg_lemma,negated_conjecture,
implies(x,x) != truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_wajsberg_lemma) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(wajsberg_1,axiom,
implies(truth,X3) = X3,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL001-0.ax',wajsberg_1) ).
cnf(symmetry,axiom,
( X5 != X4
| X4 = X5 ),
theory(equality) ).
cnf(c3,plain,
X7 = implies(truth,X7),
inference(resolution,[status(thm)],[symmetry,wajsberg_1]) ).
cnf(c0,axiom,
( X38 != X36
| X37 != X35
| implies(X38,X37) = implies(X36,X35) ),
theory(equality) ).
cnf(c51,plain,
( X198 != X199
| implies(X198,X197) = implies(X199,implies(truth,X197)) ),
inference(resolution,[status(thm)],[c0,c3]) ).
cnf(c807,plain,
implies(X201,X200) = implies(X201,implies(truth,X200)),
inference(resolution,[status(thm)],[c51,reflexivity]) ).
cnf(transitivity,axiom,
( X13 != X12
| X12 != X14
| X13 = X14 ),
theory(equality) ).
cnf(wajsberg_2,axiom,
implies(implies(X9,X8),implies(implies(X8,X10),implies(X9,X10))) = truth,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL001-0.ax',wajsberg_2) ).
cnf(c5,plain,
truth = implies(implies(X44,X45),implies(implies(X45,X46),implies(X44,X46))),
inference(resolution,[status(thm)],[wajsberg_2,symmetry]) ).
cnf(c10,plain,
( X27 != implies(truth,X26)
| X27 = X26 ),
inference(resolution,[status(thm)],[transitivity,wajsberg_1]) ).
cnf(c50,plain,
( X53 != X54
| implies(X53,X52) = implies(X54,X52) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c85,plain,
implies(implies(truth,X64),X63) = implies(X64,X63),
inference(resolution,[status(thm)],[c50,wajsberg_1]) ).
cnf(c104,plain,
implies(implies(truth,truth),X65) = X65,
inference(resolution,[status(thm)],[c85,c10]) ).
cnf(c111,plain,
( X126 != implies(implies(truth,truth),X125)
| X126 = X125 ),
inference(resolution,[status(thm)],[c104,transitivity]) ).
cnf(c323,plain,
truth = implies(implies(truth,X187),implies(truth,X187)),
inference(resolution,[status(thm)],[c111,c5]) ).
cnf(c102,plain,
( X287 != implies(implies(truth,X286),X285)
| X287 = implies(X286,X285) ),
inference(resolution,[status(thm)],[c85,transitivity]) ).
cnf(c1370,plain,
truth = implies(X294,implies(truth,X294)),
inference(resolution,[status(thm)],[c102,c323]) ).
cnf(c1419,plain,
implies(X298,implies(truth,X298)) = truth,
inference(resolution,[status(thm)],[c1370,symmetry]) ).
cnf(c1464,plain,
( X321 != implies(X320,implies(truth,X320))
| X321 = truth ),
inference(resolution,[status(thm)],[c1419,transitivity]) ).
cnf(c1643,plain,
implies(X322,X322) = truth,
inference(resolution,[status(thm)],[c1464,c807]) ).
cnf(c1675,plain,
$false,
inference(resolution,[status(thm)],[c1643,prove_wajsberg_lemma]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL132-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.34 % Computer : n005.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Fri Sep 4 20:17:50 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.41 (re.compile("\."), Token.FullStop),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.41 (re.compile("\("), Token.OpenPar),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.41 (re.compile("\)"), Token.ClosePar),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.41 (re.compile("\["), Token.OpenSquare),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("~\|"), Token.Nor),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("\|"), Token.Or),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.41 (re.compile("\?"), Token.Existential),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.48 """
% 0.23/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.48 """
% 0.33/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.57 """
% 0.67/0.99 % Version: 1.5
% 0.67/0.99 % SZS status Unsatisfiable
% 0.67/0.99 % SZS output start CNFRefutation
% See solution above
% 0.67/0.99
% 0.67/0.99 % Initial clauses : 10
% 0.67/0.99 % Processed clauses : 107
% 0.67/0.99 % Factors computed : 2
% 0.67/0.99 % Resolvents computed: 1703
% 0.67/0.99 % Tautologies deleted: 2
% 0.67/0.99 % Forward subsumed : 119
% 0.67/0.99 % Backward subsumed : 1
% 0.67/0.99 % -------- CPU Time ---------
% 0.67/0.99 % User time : 0.612 s
% 0.67/0.99 % System time : 0.034 s
% 0.67/0.99 % Total time : 0.646 s
%------------------------------------------------------------------------------