%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : KLE003+1 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n002.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 May 5 04:35:25 PM UTC 2026
% Result : Theorem 0.25s 1.61s
% Output : CNFRefutation 0.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KLE003+1 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n002.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 20:24:16 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 0.25/1.61 % Version : CSE_E---1.7
% 0.25/1.61 % Problem : theBenchmark.p
% 0.25/1.61 % SZS status Theorem for theBenchmark.p
% 0.25/1.61 % SZS output start CNFRefutation
% 0.25/1.61 fof(goals, conjecture, (![X4]:addition(X4,X4)=X4<=>addition(one,one)=one), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 0.25/1.61 fof(left_distributivity, axiom, ![X1, X2, X3]:multiplication(addition(X1,X2),X3)=addition(multiplication(X1,X3),multiplication(X2,X3)), file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', left_distributivity)).
% 0.25/1.61 fof(right_distributivity, axiom, ![X1, X2, X3]:multiplication(X1,addition(X2,X3))=addition(multiplication(X1,X2),multiplication(X1,X3)), file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', right_distributivity)).
% 0.25/1.61 fof(multiplicative_associativity, axiom, ![X1, X2, X3]:multiplication(X1,multiplication(X2,X3))=multiplication(multiplication(X1,X2),X3), file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', multiplicative_associativity)).
% 0.25/1.61 fof(additive_associativity, axiom, ![X3, X2, X1]:addition(X1,addition(X2,X3))=addition(addition(X1,X2),X3), file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', additive_associativity)).
% 0.25/1.61 fof(order, axiom, ![X1, X2]:(leq(X1,X2)<=>addition(X1,X2)=X2), file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', order)).
% 0.25/1.61 fof(additive_commutativity, axiom, ![X1, X2]:addition(X1,X2)=addition(X2,X1), file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', additive_commutativity)).
% 0.25/1.61 fof(additive_idempotence, axiom, ![X1]:addition(X1,X1)=X1, file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', additive_idempotence)).
% 0.25/1.61 fof(multiplicative_left_identity, axiom, ![X1]:multiplication(one,X1)=X1, file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', multiplicative_left_identity)).
% 0.25/1.61 fof(multiplicative_right_identity, axiom, ![X1]:multiplication(X1,one)=X1, file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', multiplicative_right_identity)).
% 0.25/1.61 fof(additive_identity, axiom, ![X1]:addition(X1,zero)=X1, file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', additive_identity)).
% 0.25/1.61 fof(left_annihilation, axiom, ![X1]:multiplication(zero,X1)=zero, file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', left_annihilation)).
% 0.25/1.61 fof(right_annihilation, axiom, ![X1]:multiplication(X1,zero)=zero, file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', right_annihilation)).
% 0.25/1.61 fof(i_0_13, negated_conjecture, ~((![X4]:addition(X4,X4)=X4<=>addition(one,one)=one)), inference(assume_negation,[status(cth)],[goals])).
% 0.25/1.62 fof(i_0_14, plain, ![X43, X44, X45]:multiplication(addition(X43,X44),X45)=addition(multiplication(X43,X45),multiplication(X44,X45)), inference(variable_rename,[status(thm)],[left_distributivity])).
% 0.25/1.62 fof(i_0_15, plain, ![X40, X41, X42]:multiplication(X40,addition(X41,X42))=addition(multiplication(X40,X41),multiplication(X40,X42)), inference(variable_rename,[status(thm)],[right_distributivity])).
% 0.25/1.62 fof(i_0_16, plain, ![X35, X36, X37]:multiplication(X35,multiplication(X36,X37))=multiplication(multiplication(X35,X36),X37), inference(variable_rename,[status(thm)],[multiplicative_associativity])).
% 0.25/1.62 fof(i_0_17, plain, ![X30, X31, X32]:addition(X32,addition(X31,X30))=addition(addition(X32,X31),X30), inference(variable_rename,[status(thm)],[additive_associativity])).
% 0.25/1.62 fof(i_0_18, plain, ![X48, X49]:((~leq(X48,X49)|addition(X48,X49)=X49)&(addition(X48,X49)!=X49|leq(X48,X49))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[order])])).
% 0.25/1.62 fof(i_0_19, negated_conjecture, ![X51]:((addition(esk1_0,esk1_0)!=esk1_0|addition(one,one)!=one)&(addition(X51,X51)=X51|addition(one,one)=one)), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_13])])])])).
% 0.25/1.62 fof(i_0_20, plain, ![X28, X29]:addition(X28,X29)=addition(X29,X28), inference(variable_rename,[status(thm)],[additive_commutativity])).
% 0.25/1.62 fof(i_0_21, plain, ![X34]:addition(X34,X34)=X34, inference(variable_rename,[status(thm)],[additive_idempotence])).
% 0.25/1.62 fof(i_0_22, plain, ![X39]:multiplication(one,X39)=X39, inference(variable_rename,[status(thm)],[multiplicative_left_identity])).
% 0.25/1.62 fof(i_0_23, plain, ![X38]:multiplication(X38,one)=X38, inference(variable_rename,[status(thm)],[multiplicative_right_identity])).
% 0.25/1.62 fof(i_0_24, plain, ![X33]:addition(X33,zero)=X33, inference(variable_rename,[status(thm)],[additive_identity])).
% 0.25/1.62 fof(i_0_25, plain, ![X47]:multiplication(zero,X47)=zero, inference(variable_rename,[status(thm)],[left_annihilation])).
% 0.25/1.62 fof(i_0_26, plain, ![X46]:multiplication(X46,zero)=zero, inference(variable_rename,[status(thm)],[right_annihilation])).
% 0.25/1.62 cnf(i_0_27, plain, (multiplication(addition(X1,X2),X3)=addition(multiplication(X1,X3),multiplication(X2,X3))), inference(split_conjunct,[status(thm)],[i_0_14]), ['final']).
% 0.25/1.62 cnf(i_0_28, plain, (multiplication(X1,addition(X2,X3))=addition(multiplication(X1,X2),multiplication(X1,X3))), inference(split_conjunct,[status(thm)],[i_0_15]), ['final']).
% 0.25/1.62 cnf(i_0_29, plain, (multiplication(X1,multiplication(X2,X3))=multiplication(multiplication(X1,X2),X3)), inference(split_conjunct,[status(thm)],[i_0_16]), ['final']).
% 0.25/1.62 cnf(i_0_30, plain, (addition(X1,addition(X2,X3))=addition(addition(X1,X2),X3)), inference(split_conjunct,[status(thm)],[i_0_17]), ['final']).
% 0.25/1.62 cnf(i_0_31, plain, (leq(X1,X2)|addition(X1,X2)!=X2), inference(split_conjunct,[status(thm)],[i_0_18]), ['final']).
% 0.25/1.62 cnf(i_0_32, plain, (addition(X1,X2)=X2|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_18]), ['final']).
% 0.25/1.62 cnf(i_0_33, negated_conjecture, (addition(esk1_0,esk1_0)!=esk1_0|addition(one,one)!=one), inference(split_conjunct,[status(thm)],[i_0_19]), ['final']).
% 0.25/1.62 cnf(i_0_34, plain, (addition(X1,X2)=addition(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_20]), ['final']).
% 0.25/1.62 cnf(i_0_35, negated_conjecture, (addition(X1,X1)=X1|addition(one,one)=one), inference(split_conjunct,[status(thm)],[i_0_19]), ['final']).
% 0.25/1.62 cnf(i_0_36, plain, (addition(X1,X1)=X1), inference(split_conjunct,[status(thm)],[i_0_21]), ['final']).
% 0.25/1.62 cnf(i_0_37, plain, (multiplication(one,X1)=X1), inference(split_conjunct,[status(thm)],[i_0_22]), ['final']).
% 0.25/1.62 cnf(i_0_38, plain, (multiplication(X1,one)=X1), inference(split_conjunct,[status(thm)],[i_0_23]), ['final']).
% 0.25/1.62 cnf(i_0_39, plain, (addition(X1,zero)=X1), inference(split_conjunct,[status(thm)],[i_0_24]), ['final']).
% 0.25/1.62 cnf(i_0_40, plain, (multiplication(zero,X1)=zero), inference(split_conjunct,[status(thm)],[i_0_25]), ['final']).
% 0.25/1.62 cnf(i_0_41, plain, (multiplication(X1,zero)=zero), inference(split_conjunct,[status(thm)],[i_0_26]), ['final']).
% 0.25/1.62 cnf(i_0_42, axiom, (X1=X1)).
% 0.25/1.62 cnf(i_0_43, axiom, (X1=X2|X2!=X1)).
% 0.25/1.62 cnf(i_0_44, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.25/1.62 cnf(i_0_45, axiom, (X1!=X2|multiplication(X1,X3)=multiplication(X2,X3))).
% 0.25/1.62 cnf(i_0_46, axiom, (X1!=X2|multiplication(X3,X1)=multiplication(X3,X2))).
% 0.25/1.62 cnf(i_0_47, axiom, (X1!=X2|addition(X1,X3)=addition(X2,X3))).
% 0.25/1.62 cnf(i_0_48, axiom, (X1!=X2|addition(X3,X1)=addition(X3,X2))).
% 0.25/1.62 cnf(i_0_49, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.25/1.62 cnf(i_0_50, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.25/1.64 cnf(i_0_42, axiom, (X1=X1)).
% 0.25/1.64 cnf(i_0_43, axiom, (X1=X2|X2!=X1)).
% 0.25/1.64 cnf(i_0_44, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.25/1.64 cnf(i_0_45, axiom, (X1!=X2|multiplication(X1,X3)=multiplication(X2,X3))).
% 0.25/1.64 cnf(i_0_46, axiom, (X1!=X2|multiplication(X3,X1)=multiplication(X3,X2))).
% 0.25/1.64 cnf(i_0_47, axiom, (X1!=X2|addition(X1,X3)=addition(X2,X3))).
% 0.25/1.64 cnf(i_0_48, axiom, (X1!=X2|addition(X3,X1)=addition(X3,X2))).
% 0.25/1.64 cnf(i_0_49, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.25/1.64 cnf(i_0_50, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.25/1.64 cnf(i_0_51, plain, (addition(one,one)!=one), inference(scs_inference,[],[i_0_36,i_0_33])).
% 0.25/1.64 cnf(i_0_52, plain, (addition(multiplication(X1,X2),multiplication(X3,X2))=multiplication(addition(X1,X3),X2)), inference(scs_inference,[],[i_0_27,i_0_43])).
% 0.25/1.64 cnf(i_0_53, plain, (leq(X1,X1)), inference(scs_inference,[],[i_0_27,i_0_36,i_0_43,i_0_31])).
% 0.25/1.64 cnf(i_0_54, plain, (addition(X1,X2)!=X2|leq(X1,X2)), inference(rename_variables,[],[i_0_31])).
% 0.25/1.64 cnf(i_0_55, plain, (multiplication(addition(X1,X1),X2)=multiplication(X1,X2)), inference(scs_inference,[],[i_0_27,i_0_36,i_0_43,i_0_31,i_0_44])).
% 0.25/1.64 cnf(i_0_56, plain, (addition(X1,X1)=X1), inference(rename_variables,[],[i_0_36])).
% 0.25/1.64 cnf(i_0_57, plain, (multiplication(addition(X1,X2),X3)=addition(multiplication(X1,X3),multiplication(X2,X3))), inference(rename_variables,[],[i_0_27])).
% 0.25/1.64 cnf(i_0_58,plain, ($false), inference(scs_inference,[],[i_0+51, i_0_36]), ['proof']).
% 0.25/1.64 % SZS output end CNFRefutation
% 0.25/1.64 % Total time : 1.271s
%------------------------------------------------------------------------------