%------------------------------------------------------------------------------
% File : JavaRes---1.3.0
% Problem : LCL469+1 : TPTP v9.2.0. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xmx15G -cp /export/starexec/sandbox2/solver/bin atp.ProverFOF -i /export/starexec/sandbox2/benchmark --eqax --proof --forward-subsumption --backward_subsumption --delete-tautologies --timeout 0 %s
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 1 12:40:26 PM UTC 2025
% Result : Theorem 203.21s 193.05s
% Output : CNFRefutation 203.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL469+1 : TPTP v9.2.0. Bugfixed v9.2.0.
% 0.11/0.12 % Command : java -Xmx15G -cp /export/starexec/sandbox2/solver/bin atp.ProverFOF -i /export/starexec/sandbox2/benchmark --eqax --proof --forward-subsumption --backward_subsumption --delete-tautologies --timeout 0 %s
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Sep 30 13:10:23 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.18/0.46 # Using default include path : /export/starexec/sandbox2/benchmark
% 0.18/0.47 # INFO in ProverFOF.main(): Processing file /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.47 # ProverFOF.processTestFile(): filename: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.47 # ProverFOF.processTestFile(): opts: {backward_subsumption=true, delete-tautologies=true, filename=/export/starexec/sandbox2/benchmark/theBenchmark.p, forward-subsumption=true, proof=true, eqax=true, timeout=0}
% 0.18/0.47 # ProverFOF.processTestFile(): evals: [Heuristics: PickGiven5 : [SymbolCountEval21, FIFOEval] litSelect: LARGEST indexing: true delTaut: true forSub: true backSub: true]
% 0.18/0.49 # INFO in Formula.command2clauses(): include file: /export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax
% 0.77/0.60 # INFO in Formula.command2clauses(): include file: /export/starexec/sandbox2/benchmark/Axioms/LCL006+1.ax
% 0.77/0.61 # INFO in Formula.command2clauses(): include file: /export/starexec/sandbox2/benchmark/Axioms/LCL006+3.ax
% 0.77/0.62 # hasConjecture: true isFOF: true
% 0.77/0.62 # ProverFOF() problem is equational
% 0.77/0.62 # INFO in ClauseSet.addEqAxioms(): adding axioms
% 0.77/0.62 # ProofState(): heuristics: PickGiven5 : [SymbolCountEval21, FIFOEval]
% 0.77/0.62 # HeuristicsClauseSet using eval functions: PickGiven5 : [SymbolCountEval21, FIFOEval]
% 203.21/193.05 # -----------------
% 203.21/193.05 # SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 203.21/193.05
% 203.21/193.05 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 203.21/193.05 fof(hilbert_or_1,conjecture,or_1,input).
% 203.21/193.05 fof(f277,negated_conjecture,(~or_1),inference(assume_negation, status(cth), [hilbert_or_1])).
% 203.21/193.05 fof(f280,negated_conjecture,~or_1,inference(fof_simplification, status(thm), [f277])).
% 203.21/193.05 cnf(cnf71,negated_conjecture,~or_1,inference(split_conjunct, status(thm), [f280])).
% 203.21/193.05 fof(or_1,axiom,(or_1<=>(![X]:(![Y]:is_a_theorem(implies(X,or(X,Y)))))),input).
% 203.21/193.05 fof(f74,axiom,(or_1<=>(![X]:(![Y]:is_a_theorem(implies(X,or(X,Y)))))),inference(fof_simplification, status(thm), [or_1])).
% 203.21/193.05 fof(f75,axiom,((~or_1|(![X]:(![Y]:is_a_theorem(implies(X,or(X,Y))))))&((?[X]:(?[Y]:~is_a_theorem(implies(X,or(X,Y)))))|or_1)),inference(fof_nnf, status(thm), [f74])).
% 203.21/193.05 fof(f76,axiom,((~or_1|(![VAR58]:(![VAR57]:is_a_theorem(implies(VAR58,or(VAR58,VAR57))))))&((?[VAR60]:(?[VAR59]:~is_a_theorem(implies(VAR60,or(VAR60,VAR59)))))|or_1)),inference(variable_rename, status(thm), [f75])).
% 203.21/193.05 fof(f77,axiom,((~or_1|(![VAR58]:(![VAR57]:is_a_theorem(implies(VAR58,or(VAR58,VAR57))))))&(~is_a_theorem(implies(skf61,or(skf61,skf62)))|or_1)),inference(skolemize, status(esa), [f76])).
% 203.21/193.05 fof(f78,axiom,((~or_1|is_a_theorem(implies(VAR58,or(VAR58,VAR57))))&(~is_a_theorem(implies(skf61,or(skf61,skf62)))|or_1)),inference(shift_quantors, status(thm), [f77])).
% 203.21/193.05 fof(f79,axiom,((~or_1|is_a_theorem(implies(VAR58,or(VAR58,VAR57))))&(~is_a_theorem(implies(skf61,or(skf61,skf62)))|or_1)),inference(distribute, status(thm), [f78])).
% 203.21/193.05 cnf(cnf22,axiom,~is_a_theorem(implies(skf61,or(skf61,skf62)))|or_1,inference(split_conjunct, status(thm), [f79])).
% 203.21/193.05 fof(luka_modus_ponens,axiom,modus_ponens,input).
% 203.21/193.05 fof(f254,axiom,modus_ponens,inference(fof_simplification, status(thm), [luka_modus_ponens])).
% 203.21/193.05 cnf(cnf63,axiom,modus_ponens,inference(split_conjunct, status(thm), [f254])).
% 203.21/193.05 fof(modus_ponens,axiom,(modus_ponens<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))=>is_a_theorem(Y))))),input).
% 203.21/193.05 fof(f2,axiom,(modus_ponens<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))=>is_a_theorem(Y))))),inference(fof_simplification, status(thm), [modus_ponens])).
% 203.21/193.05 fof(f3,axiom,((~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), [f2])).
% 203.21/193.05 fof(f4,axiom,((~modus_ponens|(![VAR1]:(![VAR0]:((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))))&((?[VAR3]:(?[VAR2]:((is_a_theorem(VAR3)&is_a_theorem(implies(VAR3,VAR2)))&~is_a_theorem(VAR2))))|modus_ponens)),inference(variable_rename, status(thm), [f3])).
% 203.21/193.05 fof(f5,axiom,((~modus_ponens|(![VAR1]:(![VAR0]:((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))))&(((is_a_theorem(skf4)&is_a_theorem(implies(skf4,skf5)))&~is_a_theorem(skf5))|modus_ponens)),inference(skolemize, status(esa), [f4])).
% 203.21/193.05 fof(f6,axiom,((~modus_ponens|((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))&(((is_a_theorem(skf4)&is_a_theorem(implies(skf4,skf5)))&~is_a_theorem(skf5))|modus_ponens)),inference(shift_quantors, status(thm), [f5])).
% 203.21/193.05 fof(f7,axiom,((~modus_ponens|((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))&(((is_a_theorem(skf4)|modus_ponens)&(is_a_theorem(implies(skf4,skf5))|modus_ponens))&(~is_a_theorem(skf5)|modus_ponens))),inference(distribute, status(thm), [f6])).
% 203.21/193.05 cnf(cnf0,axiom,~modus_ponens|~is_a_theorem(X1)|~is_a_theorem(implies(X1,X2))|is_a_theorem(X2),inference(split_conjunct, status(thm), [f7])).
% 203.21/193.05 fof(luka_modus_ponens,axiom,modus_ponens,input).
% 203.21/193.05 fof(f254,axiom,modus_ponens,inference(fof_simplification, status(thm), [luka_modus_ponens])).
% 203.21/193.05 cnf(cnf63,axiom,modus_ponens,inference(split_conjunct, status(thm), [f254])).
% 203.21/193.05 fof(luka_cn2,axiom,cn2,input).
% 203.21/193.05 fof(f260,axiom,cn2,inference(fof_simplification, status(thm), [luka_cn2])).
% 203.21/193.05 cnf(cnf65,axiom,cn2,inference(split_conjunct, status(thm), [f260])).
% 203.21/193.05 fof(cn2,axiom,(cn2<=>(![P]:(![Q]:is_a_theorem(implies(P,implies(not(P),Q)))))),input).
% 203.21/193.05 fof(f154,axiom,(cn2<=>(![P]:(![Q]:is_a_theorem(implies(P,implies(not(P),Q)))))),inference(fof_simplification, status(thm), [cn2])).
% 203.21/193.05 fof(f155,axiom,((~cn2|(![P]:(![Q]:is_a_theorem(implies(P,implies(not(P),Q))))))&((?[P]:(?[Q]:~is_a_theorem(implies(P,implies(not(P),Q)))))|cn2)),inference(fof_nnf, status(thm), [f154])).
% 203.21/193.05 fof(f156,axiom,((~cn2|(![VAR124]:(![VAR123]:is_a_theorem(implies(VAR124,implies(not(VAR124),VAR123))))))&((?[VAR126]:(?[VAR125]:~is_a_theorem(implies(VAR126,implies(not(VAR126),VAR125)))))|cn2)),inference(variable_rename, status(thm), [f155])).
% 203.21/193.05 fof(f157,axiom,((~cn2|(![VAR124]:(![VAR123]:is_a_theorem(implies(VAR124,implies(not(VAR124),VAR123))))))&(~is_a_theorem(implies(skf127,implies(not(skf127),skf128)))|cn2)),inference(skolemize, status(esa), [f156])).
% 203.21/193.05 fof(f158,axiom,((~cn2|is_a_theorem(implies(VAR124,implies(not(VAR124),VAR123))))&(~is_a_theorem(implies(skf127,implies(not(skf127),skf128)))|cn2)),inference(shift_quantors, status(thm), [f157])).
% 203.21/193.05 fof(f159,axiom,((~cn2|is_a_theorem(implies(VAR124,implies(not(VAR124),VAR123))))&(~is_a_theorem(implies(skf127,implies(not(skf127),skf128)))|cn2)),inference(distribute, status(thm), [f158])).
% 203.21/193.05 cnf(cnf41,axiom,~cn2|is_a_theorem(implies(X39,implies(not(X39),X40))),inference(split_conjunct, status(thm), [f159])).
% 203.21/193.05 cnf(c5,plain,is_a_theorem(implies(X41,implies(not(X41),X42))),inference(resolution, status(thm), [cnf41, cnf65])).
% 203.21/193.05 fof(modus_ponens,axiom,(modus_ponens<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))=>is_a_theorem(Y))))),input).
% 203.21/193.05 fof(f2,axiom,(modus_ponens<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))=>is_a_theorem(Y))))),inference(fof_simplification, status(thm), [modus_ponens])).
% 203.21/193.05 fof(f3,axiom,((~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), [f2])).
% 203.21/193.05 fof(f4,axiom,((~modus_ponens|(![VAR1]:(![VAR0]:((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))))&((?[VAR3]:(?[VAR2]:((is_a_theorem(VAR3)&is_a_theorem(implies(VAR3,VAR2)))&~is_a_theorem(VAR2))))|modus_ponens)),inference(variable_rename, status(thm), [f3])).
% 203.21/193.05 fof(f5,axiom,((~modus_ponens|(![VAR1]:(![VAR0]:((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))))&(((is_a_theorem(skf4)&is_a_theorem(implies(skf4,skf5)))&~is_a_theorem(skf5))|modus_ponens)),inference(skolemize, status(esa), [f4])).
% 203.21/193.05 fof(f6,axiom,((~modus_ponens|((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))&(((is_a_theorem(skf4)&is_a_theorem(implies(skf4,skf5)))&~is_a_theorem(skf5))|modus_ponens)),inference(shift_quantors, status(thm), [f5])).
% 203.21/193.05 fof(f7,axiom,((~modus_ponens|((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))&(((is_a_theorem(skf4)|modus_ponens)&(is_a_theorem(implies(skf4,skf5))|modus_ponens))&(~is_a_theorem(skf5)|modus_ponens))),inference(distribute, status(thm), [f6])).
% 203.21/193.05 cnf(cnf0,axiom,~modus_ponens|~is_a_theorem(X1)|~is_a_theorem(implies(X1,X2))|is_a_theorem(X2),inference(split_conjunct, status(thm), [f7])).
% 203.21/193.05 fof(luka_cn1,axiom,cn1,input).
% 203.21/193.05 fof(f257,axiom,cn1,inference(fof_simplification, status(thm), [luka_cn1])).
% 203.21/193.05 cnf(cnf64,axiom,cn1,inference(split_conjunct, status(thm), [f257])).
% 203.21/193.05 fof(cn1,axiom,(cn1<=>(![P]:(![Q]:(![R]:is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))))))),input).
% 203.21/193.05 fof(f146,axiom,(cn1<=>(![P]:(![Q]:(![R]:is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))))))),inference(fof_simplification, status(thm), [cn1])).
% 203.21/193.05 fof(f147,axiom,((~cn1|(![P]:(![Q]:(![R]:is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R))))))))&((?[P]:(?[Q]:(?[R]:~is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))))))|cn1)),inference(fof_nnf, status(thm), [f146])).
% 203.21/193.05 fof(f148,axiom,((~cn1|(![VAR116]:(![VAR115]:(![VAR114]:is_a_theorem(implies(implies(VAR116,VAR115),implies(implies(VAR115,VAR114),implies(VAR116,VAR114))))))))&((?[VAR119]:(?[VAR118]:(?[VAR117]:~is_a_theorem(implies(implies(VAR119,VAR118),implies(implies(VAR118,VAR117),implies(VAR119,VAR117)))))))|cn1)),inference(variable_rename, status(thm), [f147])).
% 203.21/193.05 fof(f149,axiom,((~cn1|(![VAR116]:(![VAR115]:(![VAR114]:is_a_theorem(implies(implies(VAR116,VAR115),implies(implies(VAR115,VAR114),implies(VAR116,VAR114))))))))&(~is_a_theorem(implies(implies(skf120,skf121),implies(implies(skf121,skf122),implies(skf120,skf122))))|cn1)),inference(skolemize, status(esa), [f148])).
% 203.21/193.05 fof(f150,axiom,((~cn1|is_a_theorem(implies(implies(VAR116,VAR115),implies(implies(VAR115,VAR114),implies(VAR116,VAR114)))))&(~is_a_theorem(implies(implies(skf120,skf121),implies(implies(skf121,skf122),implies(skf120,skf122))))|cn1)),inference(shift_quantors, status(thm), [f149])).
% 203.21/193.05 fof(f151,axiom,((~cn1|is_a_theorem(implies(implies(VAR116,VAR115),implies(implies(VAR115,VAR114),implies(VAR116,VAR114)))))&(~is_a_theorem(implies(implies(skf120,skf121),implies(implies(skf121,skf122),implies(skf120,skf122))))|cn1)),inference(distribute, status(thm), [f150])).
% 203.21/193.05 cnf(cnf39,axiom,~cn1|is_a_theorem(implies(implies(X150,X151),implies(implies(X151,X152),implies(X150,X152)))),inference(split_conjunct, status(thm), [f151])).
% 203.21/193.05 cnf(c125,plain,is_a_theorem(implies(implies(X258,X259),implies(implies(X259,X260),implies(X258,X260)))),inference(resolution, status(thm), [cnf39, cnf64])).
% 203.21/193.05 cnf(c268,plain,~modus_ponens|~is_a_theorem(implies(X494,X495))|is_a_theorem(implies(implies(X495,X496),implies(X494,X496))),inference(resolution, status(thm), [c125, cnf0])).
% 203.21/193.05 cnf(c996,plain,~modus_ponens|is_a_theorem(implies(implies(implies(not(X503),X504),X505),implies(X503,X505))),inference(resolution, status(thm), [c268, c5])).
% 203.21/193.05 cnf(c1028,plain,is_a_theorem(implies(implies(implies(not(X506),X507),X508),implies(X506,X508))),inference(resolution, status(thm), [c996, cnf63])).
% 203.21/193.05 cnf(c1032,plain,~modus_ponens|~is_a_theorem(implies(implies(not(X524),X525),X526))|is_a_theorem(implies(X524,X526)),inference(resolution, status(thm), [c1028, cnf0])).
% 203.21/193.05 fof(luka_modus_ponens,axiom,modus_ponens,input).
% 203.21/193.05 fof(f254,axiom,modus_ponens,inference(fof_simplification, status(thm), [luka_modus_ponens])).
% 203.21/193.05 cnf(cnf63,axiom,modus_ponens,inference(split_conjunct, status(thm), [f254])).
% 203.21/193.05 fof(luka_cn3,axiom,cn3,input).
% 203.21/193.05 fof(f263,axiom,cn3,inference(fof_simplification, status(thm), [luka_cn3])).
% 203.21/193.05 cnf(cnf66,axiom,cn3,inference(split_conjunct, status(thm), [f263])).
% 203.21/193.05 fof(cn3,axiom,(cn3<=>(![P]:is_a_theorem(implies(implies(not(P),P),P)))),input).
% 203.21/193.05 fof(f162,axiom,(cn3<=>(![P]:is_a_theorem(implies(implies(not(P),P),P)))),inference(fof_simplification, status(thm), [cn3])).
% 203.21/193.05 fof(f163,axiom,((~cn3|(![P]:is_a_theorem(implies(implies(not(P),P),P))))&((?[P]:~is_a_theorem(implies(implies(not(P),P),P)))|cn3)),inference(fof_nnf, status(thm), [f162])).
% 203.21/193.05 fof(f164,axiom,((~cn3|(![VAR129]:is_a_theorem(implies(implies(not(VAR129),VAR129),VAR129))))&((?[VAR130]:~is_a_theorem(implies(implies(not(VAR130),VAR130),VAR130)))|cn3)),inference(variable_rename, status(thm), [f163])).
% 203.21/193.05 fof(f165,axiom,((~cn3|(![VAR129]:is_a_theorem(implies(implies(not(VAR129),VAR129),VAR129))))&(~is_a_theorem(implies(implies(not(skf131),skf131),skf131))|cn3)),inference(skolemize, status(esa), [f164])).
% 203.21/193.05 fof(f166,axiom,((~cn3|is_a_theorem(implies(implies(not(VAR129),VAR129),VAR129)))&(~is_a_theorem(implies(implies(not(skf131),skf131),skf131))|cn3)),inference(shift_quantors, status(thm), [f165])).
% 203.21/193.05 fof(f167,axiom,((~cn3|is_a_theorem(implies(implies(not(VAR129),VAR129),VAR129)))&(~is_a_theorem(implies(implies(not(skf131),skf131),skf131))|cn3)),inference(distribute, status(thm), [f166])).
% 203.21/193.05 cnf(cnf43,axiom,~cn3|is_a_theorem(implies(implies(not(X43),X43),X43)),inference(split_conjunct, status(thm), [f167])).
% 203.21/193.05 cnf(c7,plain,is_a_theorem(implies(implies(not(X44),X44),X44)),inference(resolution, status(thm), [cnf43, cnf66])).
% 203.21/193.05 fof(modus_ponens,axiom,(modus_ponens<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))=>is_a_theorem(Y))))),input).
% 203.21/193.05 fof(f2,axiom,(modus_ponens<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))=>is_a_theorem(Y))))),inference(fof_simplification, status(thm), [modus_ponens])).
% 203.21/193.05 fof(f3,axiom,((~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), [f2])).
% 203.21/193.05 fof(f4,axiom,((~modus_ponens|(![VAR1]:(![VAR0]:((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))))&((?[VAR3]:(?[VAR2]:((is_a_theorem(VAR3)&is_a_theorem(implies(VAR3,VAR2)))&~is_a_theorem(VAR2))))|modus_ponens)),inference(variable_rename, status(thm), [f3])).
% 203.21/193.05 fof(f5,axiom,((~modus_ponens|(![VAR1]:(![VAR0]:((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))))&(((is_a_theorem(skf4)&is_a_theorem(implies(skf4,skf5)))&~is_a_theorem(skf5))|modus_ponens)),inference(skolemize, status(esa), [f4])).
% 203.21/193.05 fof(f6,axiom,((~modus_ponens|((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))&(((is_a_theorem(skf4)&is_a_theorem(implies(skf4,skf5)))&~is_a_theorem(skf5))|modus_ponens)),inference(shift_quantors, status(thm), [f5])).
% 203.21/193.05 fof(f7,axiom,((~modus_ponens|((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))&(((is_a_theorem(skf4)|modus_ponens)&(is_a_theorem(implies(skf4,skf5))|modus_ponens))&(~is_a_theorem(skf5)|modus_ponens))),inference(distribute, status(thm), [f6])).
% 203.21/193.05 cnf(cnf0,axiom,~modus_ponens|~is_a_theorem(X1)|~is_a_theorem(implies(X1,X2))|is_a_theorem(X2),inference(split_conjunct, status(thm), [f7])).
% 203.21/193.06 fof(luka_modus_ponens,axiom,modus_ponens,input).
% 203.21/193.06 fof(f254,axiom,modus_ponens,inference(fof_simplification, status(thm), [luka_modus_ponens])).
% 203.21/193.06 cnf(cnf63,axiom,modus_ponens,inference(split_conjunct, status(thm), [f254])).
% 203.21/193.06 fof(luka_cn2,axiom,cn2,input).
% 203.21/193.06 fof(f260,axiom,cn2,inference(fof_simplification, status(thm), [luka_cn2])).
% 203.21/193.06 cnf(cnf65,axiom,cn2,inference(split_conjunct, status(thm), [f260])).
% 203.21/193.06 fof(cn2,axiom,(cn2<=>(![P]:(![Q]:is_a_theorem(implies(P,implies(not(P),Q)))))),input).
% 203.21/193.06 fof(f154,axiom,(cn2<=>(![P]:(![Q]:is_a_theorem(implies(P,implies(not(P),Q)))))),inference(fof_simplification, status(thm), [cn2])).
% 203.21/193.06 fof(f155,axiom,((~cn2|(![P]:(![Q]:is_a_theorem(implies(P,implies(not(P),Q))))))&((?[P]:(?[Q]:~is_a_theorem(implies(P,implies(not(P),Q)))))|cn2)),inference(fof_nnf, status(thm), [f154])).
% 203.21/193.06 fof(f156,axiom,((~cn2|(![VAR124]:(![VAR123]:is_a_theorem(implies(VAR124,implies(not(VAR124),VAR123))))))&((?[VAR126]:(?[VAR125]:~is_a_theorem(implies(VAR126,implies(not(VAR126),VAR125)))))|cn2)),inference(variable_rename, status(thm), [f155])).
% 203.21/193.06 fof(f157,axiom,((~cn2|(![VAR124]:(![VAR123]:is_a_theorem(implies(VAR124,implies(not(VAR124),VAR123))))))&(~is_a_theorem(implies(skf127,implies(not(skf127),skf128)))|cn2)),inference(skolemize, status(esa), [f156])).
% 203.21/193.06 fof(f158,axiom,((~cn2|is_a_theorem(implies(VAR124,implies(not(VAR124),VAR123))))&(~is_a_theorem(implies(skf127,implies(not(skf127),skf128)))|cn2)),inference(shift_quantors, status(thm), [f157])).
% 203.21/193.06 fof(f159,axiom,((~cn2|is_a_theorem(implies(VAR124,implies(not(VAR124),VAR123))))&(~is_a_theorem(implies(skf127,implies(not(skf127),skf128)))|cn2)),inference(distribute, status(thm), [f158])).
% 203.21/193.06 cnf(cnf41,axiom,~cn2|is_a_theorem(implies(X39,implies(not(X39),X40))),inference(split_conjunct, status(thm), [f159])).
% 203.21/193.06 cnf(c5,plain,is_a_theorem(implies(X41,implies(not(X41),X42))),inference(resolution, status(thm), [cnf41, cnf65])).
% 203.21/193.06 fof(modus_ponens,axiom,(modus_ponens<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))=>is_a_theorem(Y))))),input).
% 203.21/193.06 fof(f2,axiom,(modus_ponens<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))=>is_a_theorem(Y))))),inference(fof_simplification, status(thm), [modus_ponens])).
% 203.21/193.06 fof(f3,axiom,((~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), [f2])).
% 203.21/193.06 fof(f4,axiom,((~modus_ponens|(![VAR1]:(![VAR0]:((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))))&((?[VAR3]:(?[VAR2]:((is_a_theorem(VAR3)&is_a_theorem(implies(VAR3,VAR2)))&~is_a_theorem(VAR2))))|modus_ponens)),inference(variable_rename, status(thm), [f3])).
% 203.21/193.06 fof(f5,axiom,((~modus_ponens|(![VAR1]:(![VAR0]:((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))))&(((is_a_theorem(skf4)&is_a_theorem(implies(skf4,skf5)))&~is_a_theorem(skf5))|modus_ponens)),inference(skolemize, status(esa), [f4])).
% 203.21/193.06 fof(f6,axiom,((~modus_ponens|((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))&(((is_a_theorem(skf4)&is_a_theorem(implies(skf4,skf5)))&~is_a_theorem(skf5))|modus_ponens)),inference(shift_quantors, status(thm), [f5])).
% 203.21/193.06 fof(f7,axiom,((~modus_ponens|((~is_a_theorem(VAR1)|~is_a_theorem(implies(VAR1,VAR0)))|is_a_theorem(VAR0)))&(((is_a_theorem(skf4)|modus_ponens)&(is_a_theorem(implies(skf4,skf5))|modus_ponens))&(~is_a_theorem(skf5)|modus_ponens))),inference(distribute, status(thm), [f6])).
% 203.21/193.06 cnf(cnf0,axiom,~modus_ponens|~is_a_theorem(X1)|~is_a_theorem(implies(X1,X2))|is_a_theorem(X2),inference(split_conjunct, status(thm), [f7])).
% 203.21/193.06 fof(luka_cn1,axiom,cn1,input).
% 203.21/193.06 fof(f257,axiom,cn1,inference(fof_simplification, status(thm), [luka_cn1])).
% 203.21/193.06 cnf(cnf64,axiom,cn1,inference(split_conjunct, status(thm), [f257])).
% 203.21/193.06 fof(cn1,axiom,(cn1<=>(![P]:(![Q]:(![R]:is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))))))),input).
% 203.21/193.06 fof(f146,axiom,(cn1<=>(![P]:(![Q]:(![R]:is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))))))),inference(fof_simplification, status(thm), [cn1])).
% 203.21/193.06 fof(f147,axiom,((~cn1|(![P]:(![Q]:(![R]:is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R))))))))&((?[P]:(?[Q]:(?[R]:~is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))))))|cn1)),inference(fof_nnf, status(thm), [f146])).
% 203.21/193.06 fof(f148,axiom,((~cn1|(![VAR116]:(![VAR115]:(![VAR114]:is_a_theorem(implies(implies(VAR116,VAR115),implies(implies(VAR115,VAR114),implies(VAR116,VAR114))))))))&((?[VAR119]:(?[VAR118]:(?[VAR117]:~is_a_theorem(implies(implies(VAR119,VAR118),implies(implies(VAR118,VAR117),implies(VAR119,VAR117)))))))|cn1)),inference(variable_rename, status(thm), [f147])).
% 203.21/193.06 fof(f149,axiom,((~cn1|(![VAR116]:(![VAR115]:(![VAR114]:is_a_theorem(implies(implies(VAR116,VAR115),implies(implies(VAR115,VAR114),implies(VAR116,VAR114))))))))&(~is_a_theorem(implies(implies(skf120,skf121),implies(implies(skf121,skf122),implies(skf120,skf122))))|cn1)),inference(skolemize, status(esa), [f148])).
% 203.21/193.06 fof(f150,axiom,((~cn1|is_a_theorem(implies(implies(VAR116,VAR115),implies(implies(VAR115,VAR114),implies(VAR116,VAR114)))))&(~is_a_theorem(implies(implies(skf120,skf121),implies(implies(skf121,skf122),implies(skf120,skf122))))|cn1)),inference(shift_quantors, status(thm), [f149])).
% 203.21/193.06 fof(f151,axiom,((~cn1|is_a_theorem(implies(implies(VAR116,VAR115),implies(implies(VAR115,VAR114),implies(VAR116,VAR114)))))&(~is_a_theorem(implies(implies(skf120,skf121),implies(implies(skf121,skf122),implies(skf120,skf122))))|cn1)),inference(distribute, status(thm), [f150])).
% 203.21/193.06 cnf(cnf39,axiom,~cn1|is_a_theorem(implies(implies(X150,X151),implies(implies(X151,X152),implies(X150,X152)))),inference(split_conjunct, status(thm), [f151])).
% 203.21/193.06 cnf(c125,plain,is_a_theorem(implies(implies(X258,X259),implies(implies(X259,X260),implies(X258,X260)))),inference(resolution, status(thm), [cnf39, cnf64])).
% 203.21/193.06 cnf(c268,plain,~modus_ponens|~is_a_theorem(implies(X494,X495))|is_a_theorem(implies(implies(X495,X496),implies(X494,X496))),inference(resolution, status(thm), [c125, cnf0])).
% 203.21/193.06 cnf(c996,plain,~modus_ponens|is_a_theorem(implies(implies(implies(not(X503),X504),X505),implies(X503,X505))),inference(resolution, status(thm), [c268, c5])).
% 203.21/193.06 cnf(c1028,plain,is_a_theorem(implies(implies(implies(not(X506),X507),X508),implies(X506,X508))),inference(resolution, status(thm), [c996, cnf63])).
% 203.21/193.06 cnf(c1032,plain,~modus_ponens|~is_a_theorem(implies(implies(not(X524),X525),X526))|is_a_theorem(implies(X524,X526)),inference(resolution, status(thm), [c1028, cnf0])).
% 203.21/193.06 cnf(c1077,plain,~modus_ponens|is_a_theorem(implies(X529,X529)),inference(resolution, status(thm), [c1032, c7])).
% 203.21/193.06 cnf(c1106,plain,is_a_theorem(implies(X530,X530)),inference(resolution, status(thm), [c1077, cnf63])).
% 203.21/193.06 cnf(predcompat5,plain,~X7=X8|~is_a_theorem(X7)|is_a_theorem(X8),eq_axiom).
% 203.21/193.06 cnf(reflexivity,axiom,X3=X3,inference(eq_axioms, , [])).
% 203.21/193.06 cnf(funcompat0,plain,~X104=X105|~X106=X107|implies(X104,X106)=implies(X105,X107),eq_axiom).
% 203.21/193.06 cnf(c51,plain,~X111=X112|implies(X111,X113)=implies(X112,X113),inference(resolution, status(thm), [funcompat0, reflexivity])).
% 203.21/193.06 fof(luka_op_or,axiom,op_or,input).
% 203.21/193.06 fof(f245,axiom,op_or,inference(fof_simplification, status(thm), [luka_op_or])).
% 203.21/193.06 cnf(cnf60,axiom,op_or,inference(split_conjunct, status(thm), [f245])).
% 203.21/193.06 fof(op_or,axiom,(op_or=>(![X]:(![Y]:or(X,Y)=not(and(not(X),not(Y)))))),input).
% 203.21/193.06 fof(f210,axiom,(op_or=>(![X]:(![Y]:or(X,Y)=not(and(not(X),not(Y)))))),inference(fof_simplification, status(thm), [op_or])).
% 203.21/193.06 fof(f211,axiom,(~op_or|(![X]:(![Y]:or(X,Y)=not(and(not(X),not(Y)))))),inference(fof_nnf, status(thm), [f210])).
% 203.21/193.06 fof(f212,axiom,(~op_or|(![VAR166]:(![VAR165]:or(VAR166,VAR165)=not(and(not(VAR166),not(VAR165)))))),inference(variable_rename, status(thm), [f211])).
% 203.21/193.06 fof(f213,axiom,(~op_or|or(VAR166,VAR165)=not(and(not(VAR166),not(VAR165)))),inference(shift_quantors, status(thm), [f212])).
% 203.21/193.06 fof(f214,axiom,(~op_or|or(VAR166,VAR165)=not(and(not(VAR166),not(VAR165)))),inference(distribute, status(thm), [f213])).
% 203.21/193.06 cnf(cnf55,axiom,~op_or|or(X84,X85)=not(and(not(X84),not(X85))),inference(split_conjunct, status(thm), [f214])).
% 203.21/193.06 cnf(c26,plain,or(X86,X87)=not(and(not(X86),not(X87))),inference(resolution, status(thm), [cnf55, cnf60])).
% 203.21/193.06 cnf(transitivity,axiom,~X30=X31|~X31=X32|X30=X32,inference(eq_axioms, , [])).
% 203.21/193.06 cnf(symmetry,axiom,~X4=X5|X5=X4,inference(eq_axioms, , [])).
% 203.21/193.06 fof(hilbert_op_implies_and,axiom,op_implies_and,input).
% 203.21/193.06 fof(f272,axiom,op_implies_and,inference(fof_simplification, status(thm), [hilbert_op_implies_and])).
% 203.21/193.06 cnf(cnf69,axiom,op_implies_and,inference(split_conjunct, status(thm), [f272])).
% 203.21/193.06 fof(op_implies_and,axiom,(op_implies_and=>(![X]:(![Y]:implies(X,Y)=not(and(X,not(Y)))))),input).
% 203.21/193.06 fof(f224,axiom,(op_implies_and=>(![X]:(![Y]:implies(X,Y)=not(and(X,not(Y)))))),inference(fof_simplification, status(thm), [op_implies_and])).
% 203.21/193.06 fof(f225,axiom,(~op_implies_and|(![X]:(![Y]:implies(X,Y)=not(and(X,not(Y)))))),inference(fof_nnf, status(thm), [f224])).
% 203.21/193.06 fof(f226,axiom,(~op_implies_and|(![VAR170]:(![VAR169]:implies(VAR170,VAR169)=not(and(VAR170,not(VAR169)))))),inference(variable_rename, status(thm), [f225])).
% 203.21/193.06 fof(f227,axiom,(~op_implies_and|implies(VAR170,VAR169)=not(and(VAR170,not(VAR169)))),inference(shift_quantors, status(thm), [f226])).
% 203.21/193.06 fof(f228,axiom,(~op_implies_and|implies(VAR170,VAR169)=not(and(VAR170,not(VAR169)))),inference(distribute, status(thm), [f227])).
% 203.21/193.06 cnf(cnf57,axiom,~op_implies_and|implies(X63,X64)=not(and(X63,not(X64))),inference(split_conjunct, status(thm), [f228])).
% 203.21/193.06 cnf(c11,plain,implies(X65,X66)=not(and(X65,not(X66))),inference(resolution, status(thm), [cnf57, cnf69])).
% 203.21/193.06 cnf(c14,plain,not(and(X67,not(X68)))=implies(X67,X68),inference(resolution, status(thm), [c11, symmetry])).
% 203.21/193.06 cnf(c16,plain,~X181=not(and(X182,not(X183)))|X181=implies(X182,X183),inference(resolution, status(thm), [c14, transitivity])).
% 203.21/193.06 cnf(c162,plain,or(X186,X187)=implies(not(X186),X187),inference(resolution, status(thm), [c16, c26])).
% 203.21/193.06 cnf(c175,plain,implies(or(X286,X287),X288)=implies(implies(not(X286),X287),X288),inference(resolution, status(thm), [c162, c51])).
% 203.21/193.06 cnf(c346,plain,~is_a_theorem(implies(or(X913,X914),X915))|is_a_theorem(implies(implies(not(X913),X914),X915)),inference(resolution, status(thm), [c175, predcompat5])).
% 203.21/193.06 cnf(c2309,plain,is_a_theorem(implies(implies(not(X916),X917),or(X916,X917))),inference(resolution, status(thm), [c346, c1106])).
% 203.21/193.06 cnf(c2317,plain,~modus_ponens|is_a_theorem(implies(X922,or(X922,X923))),inference(resolution, status(thm), [c2309, c1032])).
% 203.21/193.06 cnf(c2377,plain,is_a_theorem(implies(X924,or(X924,X925))),inference(resolution, status(thm), [c2317, cnf63])).
% 203.21/193.06 cnf(c2378,plain,or_1,inference(resolution, status(thm), [c2377, cnf22])).
% 203.21/193.06 cnf(c2389,plain,$false,inference(resolution, status(thm), [c2378, cnf71])).
% 203.21/193.06 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 203.21/193.06 # Filename : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 203.21/193.06 # Indexed : true
% 203.21/193.06 # Eval function name : PickGiven5
% 203.21/193.06 # Initial clauses : 81
% 203.21/193.06 # Processed clauses : 275
% 203.21/193.06 # Factors computed : 5
% 203.21/193.06 # Resolvents computed: 2385
% 203.21/193.06 # Tautologies deleted: 4
% 203.21/193.06 # Forward subsumed : 144
% 203.21/193.06 # Backward subsumed : 33
% 203.21/193.06 # SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 203.21/193.06 # SZS Expected : Theorem
% 203.21/193.06 # time : 192425ms
% 203.21/193.06
%------------------------------------------------------------------------------