%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG337-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 : Thu Sep 24 11:50:03 AM UTC 2026
% Result : Unsatisfiable 17.60s 2.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG337-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Mon Sep 21 13:16:36 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 17.60/2.69 % Refutation found
% 17.60/2.69 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 17.60/2.69 % SZS output start CNFRefutation for theBenchmark
% 17.60/2.69 fof(f438,axiom,(
% 17.60/2.69 (![T_a,V_b]: (( ~ class_OrderedGroup_Ogroup__add(T_a)| c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) = V_b ) ))),
% 17.60/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.60/2.69 fof(f1081,axiom,(
% 17.60/2.69 (![V_r,V_s]: (c_HOL_Ominus__class_Ominus(V_r,V_s,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(V_r,c_HOL_Ouminus__class_Ouminus(V_s,tc_RealDef_Oreal),tc_RealDef_Oreal) ))),
% 17.60/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.60/2.69 fof(f1162,axiom,(
% 17.60/2.69 (![T_a,V_a,V_b]: (( ~ class_OrderedGroup_Ocomm__monoid__add(T_a)| c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) = c_HOL_Oplus__class_Oplus(V_b,V_a,T_a) ) ))),
% 17.60/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.60/2.69 fof(f1185,axiom,(
% 17.60/2.69 (![V_a,V_b]: (c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(V_a,V_b,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),V_a,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(V_b,V_a,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) ))),
% 17.60/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.60/2.69 fof(f1225,axiom,(
% 17.60/2.69 (![T_a,V_a,V_b]: (( ~ class_OrderedGroup_Ogroup__add(T_a)| c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_b,T_a) = V_a ) ))),
% 17.60/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.60/2.69 fof(f1258,axiom,(
% 17.60/2.69 c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 17.60/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.60/2.69 fof(f1259,axiom,(
% 17.60/2.69 c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 17.60/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.60/2.69 fof(f1260,negated_conjecture,(
% 17.60/2.69 c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) != v_x____ ),
% 17.60/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.60/2.69 fof(f1386,axiom,(
% 17.60/2.69 class_OrderedGroup_Ocomm__monoid__add(tc_RealDef_Oreal) ),
% 17.60/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.60/2.69 fof(f1403,axiom,(
% 17.60/2.69 class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal) ),
% 17.60/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.60/2.69 fof(f2074,plain,(
% 17.60/2.69 ![T_a]: (~class_OrderedGroup_Ogroup__add(T_a)|(![V_b]: c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a)=V_b))),
% 17.60/2.69 inference(miniscoping,[status(thm)],[f438])).
% 17.60/2.69 fof(f2075,plain,(
% 17.60/2.69 ![X0,X1]: (~class_OrderedGroup_Ogroup__add(X0)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X1,X0),X0)=X1)),
% 17.60/2.69 inference(cnf_transformation,[status(thm)],[f2074])).
% 17.60/2.69 fof(f3052,plain,(
% 17.60/2.69 ![X0,X1]: (c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)=c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 17.60/2.69 inference(cnf_transformation,[status(thm)],[f1081])).
% 17.60/2.69 fof(f3163,plain,(
% 17.60/2.69 ![T_a]: (~class_OrderedGroup_Ocomm__monoid__add(T_a)|(![V_a,V_b]: c_HOL_Oplus__class_Oplus(V_a,V_b,T_a)=c_HOL_Oplus__class_Oplus(V_b,V_a,T_a)))),
% 17.60/2.69 inference(miniscoping,[status(thm)],[f1162])).
% 17.60/2.69 fof(f3164,plain,(
% 17.60/2.69 ![X0,X1,X2]: (~class_OrderedGroup_Ocomm__monoid__add(X0)|c_HOL_Oplus__class_Oplus(X1,X2,X0)=c_HOL_Oplus__class_Oplus(X2,X1,X0))),
% 17.60/2.69 inference(cnf_transformation,[status(thm)],[f3163])).
% 17.60/2.69 fof(f3199,plain,(
% 17.60/2.69 ![X0,X1]: (c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)=c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 17.60/2.69 inference(cnf_transformation,[status(thm)],[f1185])).
% 17.60/2.69 fof(f3270,plain,(
% 17.60/2.69 ![T_a]: (~class_OrderedGroup_Ogroup__add(T_a)|(![V_a,V_b]: c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_b,T_a)=V_a))),
% 17.60/2.69 inference(miniscoping,[status(thm)],[f1225])).
% 17.60/2.69 fof(f3271,plain,(
% 17.60/2.69 ![X0,X1,X2]: (~class_OrderedGroup_Ogroup__add(X0)|c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X1,X2,X0),X2,X0)=X1)),
% 17.60/2.69 inference(cnf_transformation,[status(thm)],[f3270])).
% 17.60/2.69 fof(f3332,plain,(
% 17.60/2.69 c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 17.60/2.69 inference(cnf_transformation,[status(thm)],[f1258])).
% 17.60/2.69 fof(f3333,plain,(
% 17.60/2.69 c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 17.60/2.69 inference(cnf_transformation,[status(thm)],[f1259])).
% 17.60/2.69 fof(f3334,plain,(
% 17.60/2.69 ~c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal)=v_x____),
% 17.60/2.69 inference(cnf_transformation,[status(thm)],[f1260])).
% 17.60/2.69 fof(f3460,plain,(
% 17.60/2.69 class_OrderedGroup_Ocomm__monoid__add(tc_RealDef_Oreal)),
% 17.60/2.69 inference(cnf_transformation,[status(thm)],[f1386])).
% 17.60/2.69 fof(f3477,plain,(
% 17.60/2.69 class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal)),
% 17.60/2.69 inference(cnf_transformation,[status(thm)],[f1403])).
% 17.60/2.69 fof(f3720,plain,(
% 17.60/2.69 ~c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal)=v_x____),
% 17.60/2.69 inference(forward_demodulation,[status(thm)],[f3333,f3334])).
% 17.60/2.69 fof(f3721,plain,(
% 17.60/2.69 ~c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)=v_x____),
% 17.60/2.69 inference(forward_demodulation,[status(thm)],[f3332,f3720])).
% 17.60/2.69 fof(f8858,plain,(
% 17.60/2.69 ![X0]: (c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)=X0)),
% 17.60/2.69 inference(resolution,[status(thm)],[f2075,f3477])).
% 17.60/2.69 fof(f8872,plain,(
% 17.60/2.69 ![X0,X1]: (c_HOL_Ominus__class_Ominus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal))),
% 17.60/2.69 inference(paramodulation,[status(thm)],[f8858,f3052])).
% 17.60/2.69 fof(f15754,plain,(
% 17.60/2.69 ![X0,X1]: (c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal)=c_HOL_Oplus__class_Oplus(X1,X0,tc_RealDef_Oreal))),
% 17.60/2.69 inference(resolution,[status(thm)],[f3164,f3460])).
% 17.60/2.69 fof(f16298,plain,(
% 17.60/2.69 ~c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)=v_x____),
% 17.60/2.69 inference(paramodulation,[status(thm)],[f15754,f3721])).
% 17.60/2.69 fof(f16466,plain,(
% 17.60/2.69 ![X0,X1]: (c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)=X0)),
% 17.60/2.69 inference(resolution,[status(thm)],[f3271,f3477])).
% 17.60/2.69 fof(f16472,plain,(
% 17.60/2.69 ![X0,X1]: (c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)=X0)),
% 17.60/2.69 inference(paramodulation,[status(thm)],[f3052,f16466])).
% 17.60/2.69 fof(f16473,plain,(
% 17.60/2.69 ![X0,X1]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)=X1)),
% 17.60/2.69 inference(paramodulation,[status(thm)],[f15754,f16466])).
% 17.60/2.69 fof(f16505,plain,(
% 17.60/2.69 ![X0,X1]: (c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)=X0)),
% 17.60/2.69 inference(forward_demodulation,[status(thm)],[f8872,f16472])).
% 17.60/2.69 fof(f16567,plain,(
% 17.60/2.69 ![X0,X1]: (c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)=X1)),
% 17.60/2.69 inference(paramodulation,[status(thm)],[f16473,f16505])).
% 17.60/2.69 fof(f16681,plain,(
% 17.60/2.69 ![X0,X1]: (c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)=X0)),
% 16.61/2.74 inference(paramodulation,[status(thm)],[f3199,f16567])).
% 16.61/2.74 fof(f16701,plain,(
% 16.61/2.74 ~v_x____=v_x____),
% 16.61/2.74 inference(backward_demodulation,[status(thm)],[f16681,f16298])).
% 16.61/2.74 fof(f16719,plain,(
% 16.61/2.74 $false),
% 16.61/2.74 inference(trivial_equality_resolution,[status(thm)],[f16701])).
% 16.61/2.74 % SZS output end CNFRefutation for theBenchmark.p
% 2.26/2.82 % Elapsed time: 2.496868 seconds
% 2.26/2.82 % CPU time: 18.872388 seconds
% 2.26/2.82 % Total memory used: 524.518 MB
% 2.26/2.82 % Net memory used: 512.711 MB
%------------------------------------------------------------------------------