%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GRP541-1 : TPTP v9.2.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n020.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:26:21 PM UTC 2026
% Result : Unsatisfiable 0.25s 1.62s
% Output : CNFRefutation 0.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP541-1 : TPTP v9.2.1. Released v2.6.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n020.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 18:43:34 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 0.25/1.62 % Version : CSE_E---1.7
% 0.25/1.62 % Problem : theBenchmark.p
% 0.25/1.62 % SZS status Unsatisfiable for theBenchmark.p
% 0.25/1.62 % SZS output start CNFRefutation
% 0.25/1.62 cnf(prove_these_axioms_1, negated_conjecture, (multiply(inverse(a1),a1)!=multiply(inverse(b1),b1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_these_axioms_1)).
% 0.25/1.62 cnf(inverse, axiom, (inverse(X1)=divide(identity,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', inverse)).
% 0.25/1.62 cnf(multiply, axiom, (multiply(X1,X2)=divide(X1,divide(identity,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', multiply)).
% 0.25/1.62 cnf(single_axiom, axiom, (divide(divide(identity,divide(divide(divide(X1,X2),X3),X1)),X3)=X2), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', single_axiom)).
% 0.25/1.62 cnf(identity, axiom, (identity=divide(X1,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', identity)).
% 0.25/1.62 cnf(i_0_5, negated_conjecture, (multiply(inverse(a1),a1)!=multiply(inverse(b1),b1)), prove_these_axioms_1).
% 0.25/1.62 cnf(i_0_6, axiom, (inverse(X1)=divide(identity,X1)), inverse).
% 0.25/1.62 cnf(i_0_7, axiom, (multiply(X1,X2)=divide(X1,divide(identity,X2))), multiply).
% 0.25/1.62 cnf(i_0_8, axiom, (divide(divide(identity,divide(divide(divide(X1,X2),X3),X1)),X3)=X2), single_axiom, ['final']).
% 0.25/1.62 cnf(i_0_9, negated_conjecture, (divide(divide(identity,b1),divide(identity,b1))!=divide(divide(identity,a1),divide(identity,a1))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_5, c_0_6]), c_0_6]), c_0_7]), c_0_7]), ['final']).
% 0.25/1.62 cnf(i_0_10, axiom, (identity=divide(X1,X1)), identity, ['final']).
% 0.25/1.62 cnf(i_0_11, axiom, (X1=X1)).
% 0.25/1.62 cnf(i_0_12, axiom, (X1=X2|X2!=X1)).
% 0.25/1.62 cnf(i_0_13, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.25/1.62 cnf(i_0_14, axiom, (X1!=X2|divide(X1,X3)=divide(X2,X3))).
% 0.25/1.62 cnf(i_0_15, axiom, (X1!=X2|divide(X3,X1)=divide(X3,X2))).
% 0.25/1.64 cnf(i_0_11, axiom, (X1=X1)).
% 0.25/1.64 cnf(i_0_12, axiom, (X1=X2|X2!=X1)).
% 0.25/1.64 cnf(i_0_13, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.25/1.64 cnf(i_0_14, axiom, (X1!=X2|divide(X1,X3)=divide(X2,X3))).
% 0.25/1.64 cnf(i_0_15, axiom, (X1!=X2|divide(X3,X1)=divide(X3,X2))).
% 0.25/1.64 cnf(i_0_16, plain, (divide(X1,X1)=identity), inference(scs_inference,[],[i_0_10,i_0_12])).
% 0.25/1.64 cnf(i_0_17, plain, (divide(divide(identity,b1),divide(identity,b1))!=identity), inference(scs_inference,[],[i_0_9,i_0_10,i_0_12,i_0_13])).
% 0.25/1.64 cnf(i_0_18, plain, (identity=divide(X1,X1)), inference(rename_variables,[],[i_0_10])).
% 0.25/1.64 cnf(i_0_19,plain, ($false), inference(scs_inference,[],[i_0+16, i_0_17]), ['proof']).
% 0.25/1.64 % SZS output end CNFRefutation
% 0.25/1.64 % Total time : 1.274s
%------------------------------------------------------------------------------