%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL540+1 : TPTP v9.3.1. Bugfixed v9.2.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:40 PM UTC 2026
% Result : Theorem 2.36s 2.63s
% Output : CNFRefutation 2.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL540+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.06/0.33 % Computer : n003.cluster.edu
% 0.06/0.33 % Model : x86_64 x86_64
% 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.33 % Memory : 8046.5625MB
% 0.06/0.33 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Fri Sep 4 16:04:19 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.15/0.40 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.15/0.40 (re.compile("\."), Token.FullStop),
% 0.15/0.40 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.15/0.40 (re.compile("\("), Token.OpenPar),
% 0.15/0.40 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.15/0.40 (re.compile("\)"), Token.ClosePar),
% 0.15/0.40 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.15/0.40 (re.compile("\["), Token.OpenSquare),
% 0.15/0.40 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.15/0.40 (re.compile("\]"), Token.CloseSquare),
% 0.15/0.40 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.40 (re.compile("~\|"), Token.Nor),
% 0.15/0.40 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.40 (re.compile("\|"), Token.Or),
% 0.15/0.40 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.15/0.40 (re.compile("\?"), Token.Existential),
% 0.15/0.40 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.15/0.40 (re.compile("\s+"), Token.WhiteSpace),
% 0.15/0.40 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.15/0.40 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.47 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.47 """
% 0.22/0.47 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.47 """
% 0.31/0.56 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.56 """
% 2.36/2.63 % Version: 1.5
% 2.36/2.63 % SZS status Theorem
% 2.36/2.63 % SZS output start CNFRefutation
% 2.36/2.63 fof(s1_0_adjunction,conjecture,adjunction,file('/export/starexec/sandbox/benchmark/theBenchmark.p', s1_0_adjunction)).
% 2.36/2.63 fof(c10,negated_conjecture,(~adjunction),inference(assume_negation,[status(cth)],[s1_0_adjunction])).
% 2.36/2.63 fof(c11,negated_conjecture,~adjunction,inference(fof_simplification,[status(thm)],[c10])).
% 2.36/2.63 cnf(c12,negated_conjecture,~adjunction,inference(split_conjunct,[status(thm)],[c11])).
% 2.36/2.63 fof(adjunction,axiom,(adjunction<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(Y))=>is_a_theorem(and(X,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL007+0.ax', adjunction)).
% 2.36/2.63 fof(c163,plain,((~adjunction|(![X]:(![Y]:((~is_a_theorem(X)|~is_a_theorem(Y))|is_a_theorem(and(X,Y))))))&((?[X]:(?[Y]:((is_a_theorem(X)&is_a_theorem(Y))&~is_a_theorem(and(X,Y)))))|adjunction)),inference(fof_nnf,[status(thm)],[adjunction])).
% 2.36/2.63 fof(c164,plain,((~adjunction|(![X76]:(![X77]:((~is_a_theorem(X76)|~is_a_theorem(X77))|is_a_theorem(and(X76,X77))))))&((?[X78]:(?[X79]:((is_a_theorem(X78)&is_a_theorem(X79))&~is_a_theorem(and(X78,X79)))))|adjunction)),inference(variable_rename,[status(thm)],[c163])).
% 2.36/2.63 fof(c166,plain,(![X76]:(![X77]:((~adjunction|((~is_a_theorem(X76)|~is_a_theorem(X77))|is_a_theorem(and(X76,X77))))&(((is_a_theorem(skolem0035)&is_a_theorem(skolem0036))&~is_a_theorem(and(skolem0035,skolem0036)))|adjunction)))),inference(shift_quantors,[status(thm)],[fof(c165,plain,((~adjunction|(![X76]:(![X77]:((~is_a_theorem(X76)|~is_a_theorem(X77))|is_a_theorem(and(X76,X77))))))&(((is_a_theorem(skolem0035)&is_a_theorem(skolem0036))&~is_a_theorem(and(skolem0035,skolem0036)))|adjunction)),inference(skolemize,[status(esa)],[c164])).])).
% 2.36/2.63 fof(c167,plain,(![X76]:(![X77]:((~adjunction|((~is_a_theorem(X76)|~is_a_theorem(X77))|is_a_theorem(and(X76,X77))))&(((is_a_theorem(skolem0035)|adjunction)&(is_a_theorem(skolem0036)|adjunction))&(~is_a_theorem(and(skolem0035,skolem0036))|adjunction))))),inference(distribute,[status(thm)],[c166])).
% 2.36/2.63 cnf(c171,plain,~is_a_theorem(and(skolem0035,skolem0036))|adjunction,inference(split_conjunct,[status(thm)],[c167])).
% 2.36/2.63 fof(hilbert_modus_ponens,axiom,modus_ponens,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+2.ax', hilbert_modus_ponens)).
% 2.36/2.63 cnf(c203,plain,modus_ponens,inference(split_conjunct,[status(thm)],[hilbert_modus_ponens])).
% 2.36/2.63 cnf(c170,plain,is_a_theorem(skolem0036)|adjunction,inference(split_conjunct,[status(thm)],[c167])).
% 2.36/2.63 cnf(c397,plain,is_a_theorem(skolem0036),inference(resolution,[status(thm)],[c170, c12])).
% 2.36/2.63 fof(modus_ponens,axiom,(modus_ponens<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))=>is_a_theorem(Y))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', modus_ponens)).
% 2.36/2.63 fof(c379,plain,((~modus_ponens|(![X]:(![Y]:((~is_a_theorem(X)|~is_a_theorem(implies(X,Y)))|is_a_theorem(Y)))))&((?[X]:(?[Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))&~is_a_theorem(Y))))|modus_ponens)),inference(fof_nnf,[status(thm)],[modus_ponens])).
% 2.36/2.63 fof(c380,plain,((~modus_ponens|(![X202]:(![X203]:((~is_a_theorem(X202)|~is_a_theorem(implies(X202,X203)))|is_a_theorem(X203)))))&((?[X204]:(?[X205]:((is_a_theorem(X204)&is_a_theorem(implies(X204,X205)))&~is_a_theorem(X205))))|modus_ponens)),inference(variable_rename,[status(thm)],[c379])).
% 2.36/2.63 fof(c382,plain,(![X202]:(![X203]:((~modus_ponens|((~is_a_theorem(X202)|~is_a_theorem(implies(X202,X203)))|is_a_theorem(X203)))&(((is_a_theorem(skolem0093)&is_a_theorem(implies(skolem0093,skolem0094)))&~is_a_theorem(skolem0094))|modus_ponens)))),inference(shift_quantors,[status(thm)],[fof(c381,plain,((~modus_ponens|(![X202]:(![X203]:((~is_a_theorem(X202)|~is_a_theorem(implies(X202,X203)))|is_a_theorem(X203)))))&(((is_a_theorem(skolem0093)&is_a_theorem(implies(skolem0093,skolem0094)))&~is_a_theorem(skolem0094))|modus_ponens)),inference(skolemize,[status(esa)],[c380])).])).
% 2.36/2.63 fof(c383,plain,(![X202]:(![X203]:((~modus_ponens|((~is_a_theorem(X202)|~is_a_theorem(implies(X202,X203)))|is_a_theorem(X203)))&(((is_a_theorem(skolem0093)|modus_ponens)&(is_a_theorem(implies(skolem0093,skolem0094))|modus_ponens))&(~is_a_theorem(skolem0094)|modus_ponens))))),inference(distribute,[status(thm)],[c382])).
% 2.36/2.63 cnf(c384,plain,~modus_ponens|~is_a_theorem(X371)|~is_a_theorem(implies(X371,X372))|is_a_theorem(X372),inference(split_conjunct,[status(thm)],[c383])).
% 2.36/2.63 cnf(c169,plain,is_a_theorem(skolem0035)|adjunction,inference(split_conjunct,[status(thm)],[c167])).
% 2.36/2.63 cnf(c396,plain,is_a_theorem(skolem0035),inference(resolution,[status(thm)],[c169, c12])).
% 2.36/2.63 fof(hilbert_and_3,axiom,and_3,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+2.ax', hilbert_and_3)).
% 2.36/2.63 cnf(c196,plain,and_3,inference(split_conjunct,[status(thm)],[hilbert_and_3])).
% 2.36/2.63 fof(and_3,axiom,(and_3<=>(![X]:(![Y]:is_a_theorem(implies(X,implies(Y,and(X,Y))))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', and_3)).
% 2.36/2.63 fof(c329,plain,((~and_3|(![X]:(![Y]:is_a_theorem(implies(X,implies(Y,and(X,Y)))))))&((?[X]:(?[Y]:~is_a_theorem(implies(X,implies(Y,and(X,Y))))))|and_3)),inference(fof_nnf,[status(thm)],[and_3])).
% 2.36/2.63 fof(c330,plain,((~and_3|(![X168]:(![X169]:is_a_theorem(implies(X168,implies(X169,and(X168,X169)))))))&((?[X170]:(?[X171]:~is_a_theorem(implies(X170,implies(X171,and(X170,X171))))))|and_3)),inference(variable_rename,[status(thm)],[c329])).
% 2.36/2.63 fof(c332,plain,(![X168]:(![X169]:((~and_3|is_a_theorem(implies(X168,implies(X169,and(X168,X169)))))&(~is_a_theorem(implies(skolem0076,implies(skolem0077,and(skolem0076,skolem0077))))|and_3)))),inference(shift_quantors,[status(thm)],[fof(c331,plain,((~and_3|(![X168]:(![X169]:is_a_theorem(implies(X168,implies(X169,and(X168,X169)))))))&(~is_a_theorem(implies(skolem0076,implies(skolem0077,and(skolem0076,skolem0077))))|and_3)),inference(skolemize,[status(esa)],[c330])).])).
% 2.36/2.63 cnf(c333,plain,~and_3|is_a_theorem(implies(X365,implies(X366,and(X365,X366)))),inference(split_conjunct,[status(thm)],[c332])).
% 2.36/2.63 cnf(c517,plain,is_a_theorem(implies(X367,implies(X368,and(X367,X368)))),inference(resolution,[status(thm)],[c333, c196])).
% 2.36/2.63 cnf(c529,plain,~modus_ponens|~is_a_theorem(X1165)|is_a_theorem(implies(X1166,and(X1165,X1166))),inference(resolution,[status(thm)],[c384, c517])).
% 2.36/2.63 cnf(c3504,plain,~modus_ponens|is_a_theorem(implies(X1193,and(skolem0035,X1193))),inference(resolution,[status(thm)],[c529, c396])).
% 2.36/2.63 cnf(c3647,plain,is_a_theorem(implies(X1196,and(skolem0035,X1196))),inference(resolution,[status(thm)],[c3504, c203])).
% 2.36/2.63 cnf(c3649,plain,~modus_ponens|~is_a_theorem(X1202)|is_a_theorem(and(skolem0035,X1202)),inference(resolution,[status(thm)],[c3647, c384])).
% 2.36/2.63 cnf(c3915,plain,~modus_ponens|is_a_theorem(and(skolem0035,skolem0036)),inference(resolution,[status(thm)],[c3649, c397])).
% 2.36/2.63 cnf(c4056,plain,is_a_theorem(and(skolem0035,skolem0036)),inference(resolution,[status(thm)],[c3915, c203])).
% 2.36/2.63 cnf(c4058,plain,adjunction,inference(resolution,[status(thm)],[c4056, c171])).
% 2.36/2.63 cnf(c4074,plain,$false,inference(resolution,[status(thm)],[c4058, c12])).
% 2.36/2.63 % SZS output end CNFRefutation
% 2.36/2.63
% 2.36/2.63 % Initial clauses : 160
% 2.36/2.63 % Processed clauses : 595
% 2.36/2.63 % Factors computed : 7
% 2.36/2.63 % Resolvents computed: 3680
% 2.36/2.63 % Tautologies deleted: 5
% 2.36/2.63 % Forward subsumed : 303
% 2.36/2.63 % Backward subsumed : 206
% 2.36/2.63 % -------- CPU Time ---------
% 2.36/2.63 % User time : 2.248 s
% 2.36/2.63 % System time : 0.041 s
% 2.36/2.63 % Total time : 2.289 s
%------------------------------------------------------------------------------