%------------------------------------------------------------------------------
% File : JavaRes---1.3.0
% Problem : LCL982+1 : TPTP v9.0.0. Released v9.1.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 : n031.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 : Tue Apr 1 01:56:27 AM UTC 2025
% Result : Theorem 0.96s 0.64s
% Output : CNFRefutation 0.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : LCL982+1 : TPTP v9.0.0. Released v9.1.0.
% 0.03/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.13/0.34 % Computer : n031.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Mar 31 10:49:37 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.20/0.47 # Using default include path : /export/starexec/sandbox2/benchmark
% 0.20/0.47 # INFO in ProverFOF.main(): Processing file /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.47 # ProverFOF.processTestFile(): filename: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/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.20/0.47 # ProverFOF.processTestFile(): evals: [Heuristics: PickGiven5 : [SymbolCountEval21, FIFOEval] litSelect: LARGEST indexing: true delTaut: true forSub: true backSub: true]
% 0.20/0.52 # hasConjecture: true isFOF: true
% 0.20/0.52 # ProofState(): heuristics: PickGiven5 : [SymbolCountEval21, FIFOEval]
% 0.20/0.52 # HeuristicsClauseSet using eval functions: PickGiven5 : [SymbolCountEval21, FIFOEval]
% 0.96/0.64 # -----------------
% 0.96/0.64 # SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.96/0.64
% 0.96/0.64 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.96/0.64 fof(prove_cn_1,conjecture,(![A]:(![B]:(![C]:is_a_theorem(implies(implies(A,B),implies(implies(B,C),implies(A,C))))))),input).
% 0.96/0.64 fof(f11,negated_conjecture,(~(![A]:(![B]:(![C]:is_a_theorem(implies(implies(A,B),implies(implies(B,C),implies(A,C)))))))),inference(assume_negation, status(cth), [prove_cn_1])).
% 0.96/0.64 fof(f14,negated_conjecture,(~(![A]:(![B]:(![C]:is_a_theorem(implies(implies(A,B),implies(implies(B,C),implies(A,C)))))))),inference(fof_simplification, status(thm), [f11])).
% 0.96/0.64 fof(f15,negated_conjecture,(?[A]:(?[B]:(?[C]:~is_a_theorem(implies(implies(A,B),implies(implies(B,C),implies(A,C))))))),inference(fof_nnf, status(thm), [f14])).
% 0.96/0.64 fof(f16,negated_conjecture,(?[VAR9]:(?[VAR8]:(?[VAR7]:~is_a_theorem(implies(implies(VAR9,VAR8),implies(implies(VAR8,VAR7),implies(VAR9,VAR7))))))),inference(variable_rename, status(thm), [f15])).
% 0.96/0.64 fof(f17,negated_conjecture,~is_a_theorem(implies(implies(skf10,skf11),implies(implies(skf11,skf12),implies(skf10,skf12)))),inference(skolemize, status(esa), [f16])).
% 0.96/0.64 cnf(cnf2,negated_conjecture,~is_a_theorem(implies(implies(skf10,skf11),implies(implies(skf11,skf12),implies(skf10,skf12)))),inference(split_conjunct, status(thm), [f17])).
% 0.96/0.64 fof(condensed_detachment,axiom,(![X]:(![Y]:(((~is_a_theorem(implies(X,Y)))|(~is_a_theorem(X)))|is_a_theorem(Y)))),input).
% 0.96/0.64 fof(f2,axiom,(![X]:(![Y]:((~is_a_theorem(implies(X,Y))|~is_a_theorem(X))|is_a_theorem(Y)))),inference(fof_simplification, status(thm), [condensed_detachment])).
% 0.96/0.64 fof(f3,axiom,(![VAR1]:(![VAR0]:((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)))),inference(variable_rename, status(thm), [f2])).
% 0.96/0.64 fof(f4,axiom,((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)),inference(shift_quantors, status(thm), [f3])).
% 0.96/0.64 cnf(cnf0,axiom,~is_a_theorem(implies(X1,X2))|~is_a_theorem(X1)|is_a_theorem(X2),inference(split_conjunct, status(thm), [f4])).
% 0.96/0.64 fof(condensed_detachment,axiom,(![X]:(![Y]:(((~is_a_theorem(implies(X,Y)))|(~is_a_theorem(X)))|is_a_theorem(Y)))),input).
% 0.96/0.64 fof(f2,axiom,(![X]:(![Y]:((~is_a_theorem(implies(X,Y))|~is_a_theorem(X))|is_a_theorem(Y)))),inference(fof_simplification, status(thm), [condensed_detachment])).
% 0.96/0.64 fof(f3,axiom,(![VAR1]:(![VAR0]:((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)))),inference(variable_rename, status(thm), [f2])).
% 0.96/0.64 fof(f4,axiom,((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)),inference(shift_quantors, status(thm), [f3])).
% 0.96/0.64 cnf(cnf0,axiom,~is_a_theorem(implies(X1,X2))|~is_a_theorem(X1)|is_a_theorem(X2),inference(split_conjunct, status(thm), [f4])).
% 0.96/0.64 fof(a5,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),input).
% 0.96/0.64 fof(f7,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),inference(fof_simplification, status(thm), [a5])).
% 0.96/0.64 fof(f8,axiom,(![VAR6]:(![VAR5]:(![VAR4]:(![VAR3]:(![VAR2]:is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3))))))))),inference(variable_rename, status(thm), [f7])).
% 0.96/0.64 fof(f9,axiom,is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3)))),inference(shift_quantors, status(thm), [f8])).
% 0.96/0.64 cnf(cnf1,axiom,is_a_theorem(implies(implies(X3,X4),implies(implies(implies(X5,implies(X6,X7)),implies(X4,implies(not(X6),not(X3)))),implies(X3,X6)))),inference(split_conjunct, status(thm), [f9])).
% 0.96/0.64 cnf(c0,plain,~is_a_theorem(implies(X8,X9))|is_a_theorem(implies(implies(implies(X10,implies(X11,X12)),implies(X9,implies(not(X11),not(X8)))),implies(X8,X11))),inference(resolution, status(thm), [cnf1, cnf0])).
% 0.96/0.64 fof(a5,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),input).
% 0.96/0.64 fof(f7,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),inference(fof_simplification, status(thm), [a5])).
% 0.96/0.64 fof(f8,axiom,(![VAR6]:(![VAR5]:(![VAR4]:(![VAR3]:(![VAR2]:is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3))))))))),inference(variable_rename, status(thm), [f7])).
% 0.96/0.64 fof(f9,axiom,is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3)))),inference(shift_quantors, status(thm), [f8])).
% 0.96/0.64 cnf(cnf1,axiom,is_a_theorem(implies(implies(X3,X4),implies(implies(implies(X5,implies(X6,X7)),implies(X4,implies(not(X6),not(X3)))),implies(X3,X6)))),inference(split_conjunct, status(thm), [f9])).
% 0.96/0.64 fof(condensed_detachment,axiom,(![X]:(![Y]:(((~is_a_theorem(implies(X,Y)))|(~is_a_theorem(X)))|is_a_theorem(Y)))),input).
% 0.96/0.64 fof(f2,axiom,(![X]:(![Y]:((~is_a_theorem(implies(X,Y))|~is_a_theorem(X))|is_a_theorem(Y)))),inference(fof_simplification, status(thm), [condensed_detachment])).
% 0.96/0.64 fof(f3,axiom,(![VAR1]:(![VAR0]:((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)))),inference(variable_rename, status(thm), [f2])).
% 0.96/0.64 fof(f4,axiom,((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)),inference(shift_quantors, status(thm), [f3])).
% 0.96/0.64 cnf(cnf0,axiom,~is_a_theorem(implies(X1,X2))|~is_a_theorem(X1)|is_a_theorem(X2),inference(split_conjunct, status(thm), [f4])).
% 0.96/0.64 fof(a5,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),input).
% 0.96/0.64 fof(f7,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),inference(fof_simplification, status(thm), [a5])).
% 0.96/0.64 fof(f8,axiom,(![VAR6]:(![VAR5]:(![VAR4]:(![VAR3]:(![VAR2]:is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3))))))))),inference(variable_rename, status(thm), [f7])).
% 0.96/0.64 fof(f9,axiom,is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3)))),inference(shift_quantors, status(thm), [f8])).
% 0.96/0.64 cnf(cnf1,axiom,is_a_theorem(implies(implies(X3,X4),implies(implies(implies(X5,implies(X6,X7)),implies(X4,implies(not(X6),not(X3)))),implies(X3,X6)))),inference(split_conjunct, status(thm), [f9])).
% 0.96/0.64 cnf(c0,plain,~is_a_theorem(implies(X8,X9))|is_a_theorem(implies(implies(implies(X10,implies(X11,X12)),implies(X9,implies(not(X11),not(X8)))),implies(X8,X11))),inference(resolution, status(thm), [cnf1, cnf0])).
% 0.96/0.65 cnf(c1,plain,is_a_theorem(implies(implies(implies(X13,implies(X14,X15)),implies(implies(implies(implies(X16,implies(X17,X18)),implies(X19,implies(not(X17),not(X20)))),implies(X20,X17)),implies(not(X14),not(implies(X20,X19))))),implies(implies(X20,X19),X14))),inference(resolution, status(thm), [c0, cnf1])).
% 0.96/0.65 fof(condensed_detachment,axiom,(![X]:(![Y]:(((~is_a_theorem(implies(X,Y)))|(~is_a_theorem(X)))|is_a_theorem(Y)))),input).
% 0.96/0.65 fof(f2,axiom,(![X]:(![Y]:((~is_a_theorem(implies(X,Y))|~is_a_theorem(X))|is_a_theorem(Y)))),inference(fof_simplification, status(thm), [condensed_detachment])).
% 0.96/0.65 fof(f3,axiom,(![VAR1]:(![VAR0]:((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)))),inference(variable_rename, status(thm), [f2])).
% 0.96/0.65 fof(f4,axiom,((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)),inference(shift_quantors, status(thm), [f3])).
% 0.96/0.65 cnf(cnf0,axiom,~is_a_theorem(implies(X1,X2))|~is_a_theorem(X1)|is_a_theorem(X2),inference(split_conjunct, status(thm), [f4])).
% 0.96/0.65 fof(a5,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),input).
% 0.96/0.65 fof(f7,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),inference(fof_simplification, status(thm), [a5])).
% 0.96/0.65 fof(f8,axiom,(![VAR6]:(![VAR5]:(![VAR4]:(![VAR3]:(![VAR2]:is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3))))))))),inference(variable_rename, status(thm), [f7])).
% 0.96/0.65 fof(f9,axiom,is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3)))),inference(shift_quantors, status(thm), [f8])).
% 0.96/0.65 cnf(cnf1,axiom,is_a_theorem(implies(implies(X3,X4),implies(implies(implies(X5,implies(X6,X7)),implies(X4,implies(not(X6),not(X3)))),implies(X3,X6)))),inference(split_conjunct, status(thm), [f9])).
% 0.96/0.65 fof(condensed_detachment,axiom,(![X]:(![Y]:(((~is_a_theorem(implies(X,Y)))|(~is_a_theorem(X)))|is_a_theorem(Y)))),input).
% 0.96/0.65 fof(f2,axiom,(![X]:(![Y]:((~is_a_theorem(implies(X,Y))|~is_a_theorem(X))|is_a_theorem(Y)))),inference(fof_simplification, status(thm), [condensed_detachment])).
% 0.96/0.65 fof(f3,axiom,(![VAR1]:(![VAR0]:((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)))),inference(variable_rename, status(thm), [f2])).
% 0.96/0.65 fof(f4,axiom,((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)),inference(shift_quantors, status(thm), [f3])).
% 0.96/0.65 cnf(cnf0,axiom,~is_a_theorem(implies(X1,X2))|~is_a_theorem(X1)|is_a_theorem(X2),inference(split_conjunct, status(thm), [f4])).
% 0.96/0.65 fof(a5,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),input).
% 0.96/0.65 fof(f7,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),inference(fof_simplification, status(thm), [a5])).
% 0.96/0.65 fof(f8,axiom,(![VAR6]:(![VAR5]:(![VAR4]:(![VAR3]:(![VAR2]:is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3))))))))),inference(variable_rename, status(thm), [f7])).
% 0.96/0.65 fof(f9,axiom,is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3)))),inference(shift_quantors, status(thm), [f8])).
% 0.96/0.65 cnf(cnf1,axiom,is_a_theorem(implies(implies(X3,X4),implies(implies(implies(X5,implies(X6,X7)),implies(X4,implies(not(X6),not(X3)))),implies(X3,X6)))),inference(split_conjunct, status(thm), [f9])).
% 0.96/0.65 cnf(c0,plain,~is_a_theorem(implies(X8,X9))|is_a_theorem(implies(implies(implies(X10,implies(X11,X12)),implies(X9,implies(not(X11),not(X8)))),implies(X8,X11))),inference(resolution, status(thm), [cnf1, cnf0])).
% 0.96/0.65 cnf(c1,plain,is_a_theorem(implies(implies(implies(X13,implies(X14,X15)),implies(implies(implies(implies(X16,implies(X17,X18)),implies(X19,implies(not(X17),not(X20)))),implies(X20,X17)),implies(not(X14),not(implies(X20,X19))))),implies(implies(X20,X19),X14))),inference(resolution, status(thm), [c0, cnf1])).
% 0.96/0.65 cnf(c2,plain,~is_a_theorem(implies(implies(X21,implies(X22,X23)),implies(implies(implies(implies(X24,implies(X25,X26)),implies(X27,implies(not(X25),not(X28)))),implies(X28,X25)),implies(not(X22),not(implies(X28,X27))))))|is_a_theorem(implies(implies(X28,X27),X22)),inference(resolution, status(thm), [c1, cnf0])).
% 0.96/0.65 cnf(c4,plain,is_a_theorem(implies(implies(X29,X30),implies(implies(implies(X31,implies(X32,X33)),implies(implies(X29,X34),implies(not(X32),not(implies(implies(X35,implies(X34,X36)),implies(X30,implies(not(X34),not(X29)))))))),implies(implies(implies(X35,implies(X34,X36)),implies(X30,implies(not(X34),not(X29)))),X32)))),inference(resolution, status(thm), [c2, c1])).
% 0.96/0.65 cnf(c6,plain,is_a_theorem(implies(implies(implies(X45,implies(X46,X47)),implies(implies(implies(implies(X48,implies(X49,X50)),implies(implies(X51,X52),implies(not(X49),not(implies(implies(X53,implies(X52,X54)),implies(X55,implies(not(X52),not(X51)))))))),implies(implies(implies(X53,implies(X52,X54)),implies(X55,implies(not(X52),not(X51)))),X49)),implies(not(X46),not(implies(X51,X55))))),implies(implies(X51,X55),X46))),inference(resolution, status(thm), [c4, c0])).
% 0.96/0.65 cnf(c12,plain,~is_a_theorem(implies(implies(X56,implies(X57,X58)),implies(implies(implies(implies(X59,implies(X60,X61)),implies(implies(X62,X63),implies(not(X60),not(implies(implies(X64,implies(X63,X65)),implies(X66,implies(not(X63),not(X62)))))))),implies(implies(implies(X64,implies(X63,X65)),implies(X66,implies(not(X63),not(X62)))),X60)),implies(not(X57),not(implies(X62,X66))))))|is_a_theorem(implies(implies(X62,X66),X57)),inference(resolution, status(thm), [c6, cnf0])).
% 0.96/0.65 fof(condensed_detachment,axiom,(![X]:(![Y]:(((~is_a_theorem(implies(X,Y)))|(~is_a_theorem(X)))|is_a_theorem(Y)))),input).
% 0.96/0.65 fof(f2,axiom,(![X]:(![Y]:((~is_a_theorem(implies(X,Y))|~is_a_theorem(X))|is_a_theorem(Y)))),inference(fof_simplification, status(thm), [condensed_detachment])).
% 0.96/0.65 fof(f3,axiom,(![VAR1]:(![VAR0]:((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)))),inference(variable_rename, status(thm), [f2])).
% 0.96/0.65 fof(f4,axiom,((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)),inference(shift_quantors, status(thm), [f3])).
% 0.96/0.65 cnf(cnf0,axiom,~is_a_theorem(implies(X1,X2))|~is_a_theorem(X1)|is_a_theorem(X2),inference(split_conjunct, status(thm), [f4])).
% 0.96/0.65 fof(a5,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),input).
% 0.96/0.65 fof(f7,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),inference(fof_simplification, status(thm), [a5])).
% 0.96/0.65 fof(f8,axiom,(![VAR6]:(![VAR5]:(![VAR4]:(![VAR3]:(![VAR2]:is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3))))))))),inference(variable_rename, status(thm), [f7])).
% 0.96/0.65 fof(f9,axiom,is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3)))),inference(shift_quantors, status(thm), [f8])).
% 0.96/0.65 cnf(cnf1,axiom,is_a_theorem(implies(implies(X3,X4),implies(implies(implies(X5,implies(X6,X7)),implies(X4,implies(not(X6),not(X3)))),implies(X3,X6)))),inference(split_conjunct, status(thm), [f9])).
% 0.96/0.65 cnf(c0,plain,~is_a_theorem(implies(X8,X9))|is_a_theorem(implies(implies(implies(X10,implies(X11,X12)),implies(X9,implies(not(X11),not(X8)))),implies(X8,X11))),inference(resolution, status(thm), [cnf1, cnf0])).
% 0.96/0.65 fof(a5,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),input).
% 0.96/0.65 fof(f7,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),inference(fof_simplification, status(thm), [a5])).
% 0.96/0.65 fof(f8,axiom,(![VAR6]:(![VAR5]:(![VAR4]:(![VAR3]:(![VAR2]:is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3))))))))),inference(variable_rename, status(thm), [f7])).
% 0.96/0.65 fof(f9,axiom,is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3)))),inference(shift_quantors, status(thm), [f8])).
% 0.96/0.65 cnf(cnf1,axiom,is_a_theorem(implies(implies(X3,X4),implies(implies(implies(X5,implies(X6,X7)),implies(X4,implies(not(X6),not(X3)))),implies(X3,X6)))),inference(split_conjunct, status(thm), [f9])).
% 0.96/0.65 fof(condensed_detachment,axiom,(![X]:(![Y]:(((~is_a_theorem(implies(X,Y)))|(~is_a_theorem(X)))|is_a_theorem(Y)))),input).
% 0.96/0.65 fof(f2,axiom,(![X]:(![Y]:((~is_a_theorem(implies(X,Y))|~is_a_theorem(X))|is_a_theorem(Y)))),inference(fof_simplification, status(thm), [condensed_detachment])).
% 0.96/0.65 fof(f3,axiom,(![VAR1]:(![VAR0]:((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)))),inference(variable_rename, status(thm), [f2])).
% 0.96/0.65 fof(f4,axiom,((~is_a_theorem(implies(VAR1,VAR0))|~is_a_theorem(VAR1))|is_a_theorem(VAR0)),inference(shift_quantors, status(thm), [f3])).
% 0.96/0.65 cnf(cnf0,axiom,~is_a_theorem(implies(X1,X2))|~is_a_theorem(X1)|is_a_theorem(X2),inference(split_conjunct, status(thm), [f4])).
% 0.96/0.65 fof(a5,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),input).
% 0.96/0.65 fof(f7,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))))))),inference(fof_simplification, status(thm), [a5])).
% 0.96/0.65 fof(f8,axiom,(![VAR6]:(![VAR5]:(![VAR4]:(![VAR3]:(![VAR2]:is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3))))))))),inference(variable_rename, status(thm), [f7])).
% 0.96/0.65 fof(f9,axiom,is_a_theorem(implies(implies(VAR6,VAR5),implies(implies(implies(VAR4,implies(VAR3,VAR2)),implies(VAR5,implies(not(VAR3),not(VAR6)))),implies(VAR6,VAR3)))),inference(shift_quantors, status(thm), [f8])).
% 0.96/0.65 cnf(cnf1,axiom,is_a_theorem(implies(implies(X3,X4),implies(implies(implies(X5,implies(X6,X7)),implies(X4,implies(not(X6),not(X3)))),implies(X3,X6)))),inference(split_conjunct, status(thm), [f9])).
% 0.96/0.65 cnf(c0,plain,~is_a_theorem(implies(X8,X9))|is_a_theorem(implies(implies(implies(X10,implies(X11,X12)),implies(X9,implies(not(X11),not(X8)))),implies(X8,X11))),inference(resolution, status(thm), [cnf1, cnf0])).
% 0.96/0.65 cnf(c1,plain,is_a_theorem(implies(implies(implies(X13,implies(X14,X15)),implies(implies(implies(implies(X16,implies(X17,X18)),implies(X19,implies(not(X17),not(X20)))),implies(X20,X17)),implies(not(X14),not(implies(X20,X19))))),implies(implies(X20,X19),X14))),inference(resolution, status(thm), [c0, cnf1])).
% 0.96/0.65 cnf(c3,plain,is_a_theorem(implies(implies(implies(X67,implies(X68,X69)),implies(implies(implies(X70,X71),X72),implies(not(X68),not(implies(implies(X73,implies(X72,X74)),implies(implies(implies(implies(X75,implies(X76,X77)),implies(X71,implies(not(X76),not(X70)))),implies(X70,X76)),implies(not(X72),not(implies(X70,X71))))))))),implies(implies(implies(X73,implies(X72,X74)),implies(implies(implies(implies(X75,implies(X76,X77)),implies(X71,implies(not(X76),not(X70)))),implies(X70,X76)),implies(not(X72),not(implies(X70,X71))))),X68))),inference(resolution, status(thm), [c1, c0])).
% 0.96/0.65 cnf(c18,plain,is_a_theorem(implies(implies(X92,X93),implies(implies(X93,X94),implies(X92,X94)))),inference(resolution, status(thm), [c3, c12])).
% 0.96/0.65 cnf(c28,plain,$false,inference(resolution, status(thm), [c18, cnf2])).
% 0.96/0.65 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.96/0.65 # Filename : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.96/0.65 # Indexed : true
% 0.96/0.65 # Eval function name : PickGiven5
% 0.96/0.65 # Initial clauses : 3
% 0.96/0.65 # Processed clauses : 13
% 0.96/0.65 # Factors computed : 0
% 0.96/0.65 # Resolvents computed: 30
% 0.96/0.65 # Tautologies deleted: 0
% 0.96/0.65 # Forward subsumed : 0
% 0.96/0.65 # Backward subsumed : 0
% 0.96/0.65 # SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.96/0.65 # SZS Expected : Theorem
% 0.96/0.65 # time : 123ms
% 0.96/0.65
%------------------------------------------------------------------------------