%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW177+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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 03:08:46 PM UTC 2026
% Result : Theorem 72.81s 9.82s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW177+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n010.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 09:39:25 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.27/0.52 % Drodi V4.1.1
% 72.81/9.82 % Refutation found
% 72.81/9.82 % SZS status Theorem for theBenchmark: Theorem is valid
% 72.81/9.82 % SZS output start CNFRefutation for theBenchmark
% 72.81/9.82 fof(f66,axiom,(
% 72.81/9.82 (! [V_k] : c_Int_Onumber__class_Onumber__of(tc_Int_Oint,V_k) = V_k )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f83,axiom,(
% 72.81/9.82 c_Groups_Oone__class_Oone(tc_Int_Oint) = c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit1(c_Int_OPls)) ),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f109,axiom,(
% 72.81/9.82 (! [V_b,V_a,T_a] :( class_Orderings_Olinorder(T_a)=> c_Orderings_Oord__class_Omin(T_a,V_a,V_b) = c_Orderings_Oord__class_Omin(T_a,V_b,V_a) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f184,axiom,(
% 72.81/9.82 (! [V_z,V_y,V_x,T_a] :( class_Orderings_Opreorder(T_a)=> ( c_Orderings_Oord__class_Oless(T_a,V_x,V_y)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_z)=> c_Orderings_Oord__class_Oless(T_a,V_x,V_z) ) ) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f194,axiom,(
% 72.81/9.82 (! [V_x,V_y,T_a] :( class_Orderings_Olinorder(T_a)=> ( ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)=> c_Orderings_Oord__class_Oless(T_a,V_x,V_y) ) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f206,axiom,(
% 72.81/9.82 (! [V_x,V_y,T_a] :( class_Orderings_Olinorder(T_a)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)=> c_Orderings_Oord__class_Omin(T_a,V_x,V_y) = V_y ) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f207,axiom,(
% 72.81/9.82 (! [V_y,V_x,T_a] :( class_Orderings_Olinorder(T_a)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)=> c_Orderings_Oord__class_Omin(T_a,V_x,V_y) = V_x ) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f208,axiom,(
% 72.81/9.82 (! [V_a,V_x,V_b,T_a] :( class_Orderings_Olinorder(T_a)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_b,V_x)=> c_Orderings_Oord__class_Oless__eq(T_a,c_Orderings_Oord__class_Omin(T_a,V_a,V_b),V_x) ) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f212,axiom,(
% 72.81/9.82 (! [V_y_2,V_x_2,T_a] :( class_Orderings_Olinorder(T_a)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)<=> c_Orderings_Oord__class_Omin(T_a,V_x_2,V_y_2) = V_x_2 ) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f227,axiom,(
% 72.81/9.82 c_Transcendental_Osin(c_Transcendental_Opi) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f338,axiom,(
% 72.81/9.82 (! [V_w,V_z] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z,V_w)| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_z) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f352,axiom,(
% 72.81/9.82 (! [V_y_2,V_x_2] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)<=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)& V_x_2 != V_y_2 ) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f427,axiom,(
% 72.81/9.82 (! [V_a,T_a] :( class_Groups_Omonoid__add(T_a)=> c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a) = V_a ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f430,axiom,(
% 72.81/9.82 (! [V_a,T_a] :( class_Groups_Omonoid__add(T_a)=> c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f434,axiom,(
% 72.81/9.82 (! [V_d,V_c,V_b,V_a,T_a] :( class_Groups_Oordered__ab__semigroup__add(T_a)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_a,V_b)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_c,V_d)=> c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_d)) ) ) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f436,axiom,(
% 72.81/9.82 (! [V_c,V_b,V_a,T_a] :( class_Groups_Oordered__ab__semigroup__add(T_a)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_a,V_b)=> c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_c)) ) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f674,axiom,(
% 72.81/9.82 (! [V_y,V_x] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x,V_y)=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x,V_y),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f675,axiom,(
% 72.81/9.82 (! [V_y,V_x] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x,V_y)=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x,V_y),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),V_y) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f689,axiom,(
% 72.81/9.82 (! [V_x] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,V_x,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,V_x,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = V_x )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f795,axiom,(
% 72.81/9.82 (! [V_c,V_a,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> c_Groups_Oplus__class_Oplus(T_a,V_a,V_c) = c_Groups_Oplus__class_Oplus(T_a,V_c,V_a) ) )),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f1108,axiom,(
% 72.81/9.82 class_Groups_Oordered__ab__semigroup__add(tc_RealDef_Oreal) ),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f1134,axiom,(
% 72.81/9.82 class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal) ),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f1141,axiom,(
% 72.81/9.82 class_Orderings_Opreorder(tc_RealDef_Oreal) ),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f1142,axiom,(
% 72.81/9.82 class_Orderings_Olinorder(tc_RealDef_Oreal) ),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f1145,axiom,(
% 72.81/9.82 class_Groups_Omonoid__add(tc_RealDef_Oreal) ),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f1198,hypothesis,(
% 72.81/9.82 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1) ),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f1199,hypothesis,(
% 72.81/9.82 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2) ),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f1200,conjecture,(
% 72.81/9.82 ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d1)& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d2) ) ),
% 72.81/9.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.81/9.82 fof(f1201,negated_conjecture,(
% 72.81/9.82 ~(( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d1)& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d2) ) )),
% 72.81/9.82 inference(negated_conjecture,[status(cth)],[f1200])).
% 72.81/9.82 fof(f1415,plain,(
% 72.81/9.82 ![X0]: (c_Int_Onumber__class_Onumber__of(tc_Int_Oint,X0)=X0)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f66])).
% 72.81/9.82 fof(f1452,plain,(
% 72.81/9.82 c_Groups_Oone__class_Oone(tc_Int_Oint)=c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit1(c_Int_OPls))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f83])).
% 72.81/9.82 fof(f1534,plain,(
% 72.81/9.82 ![V_b,V_a,T_a]: (~class_Orderings_Olinorder(T_a)|c_Orderings_Oord__class_Omin(T_a,V_a,V_b)=c_Orderings_Oord__class_Omin(T_a,V_b,V_a))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f109])).
% 72.81/9.82 fof(f1535,plain,(
% 72.81/9.82 ![T_a]: (~class_Orderings_Olinorder(T_a)|(![V_b,V_a]: c_Orderings_Oord__class_Omin(T_a,V_a,V_b)=c_Orderings_Oord__class_Omin(T_a,V_b,V_a)))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f1534])).
% 72.81/9.82 fof(f1536,plain,(
% 72.81/9.82 ![X0,X1,X2]: (~class_Orderings_Olinorder(X0)|c_Orderings_Oord__class_Omin(X0,X1,X2)=c_Orderings_Oord__class_Omin(X0,X2,X1))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1535])).
% 72.81/9.82 fof(f1726,plain,(
% 72.81/9.82 ![V_z,V_y,V_x,T_a]: (~class_Orderings_Opreorder(T_a)|(~c_Orderings_Oord__class_Oless(T_a,V_x,V_y)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_z)|c_Orderings_Oord__class_Oless(T_a,V_x,V_z))))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f184])).
% 72.81/9.82 fof(f1727,plain,(
% 72.81/9.82 ![T_a]: (~class_Orderings_Opreorder(T_a)|(![V_y,V_x]: (~c_Orderings_Oord__class_Oless(T_a,V_x,V_y)|(![V_z]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_z)|c_Orderings_Oord__class_Oless(T_a,V_x,V_z))))))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f1726])).
% 72.81/9.82 fof(f1728,plain,(
% 72.81/9.82 ![X0,X1,X2,X3]: (~class_Orderings_Opreorder(X0)|~c_Orderings_Oord__class_Oless(X0,X1,X2)|~c_Orderings_Oord__class_Oless__eq(X0,X2,X3)|c_Orderings_Oord__class_Oless(X0,X1,X3))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1727])).
% 72.81/9.82 fof(f1760,plain,(
% 72.81/9.82 ![V_x,V_y,T_a]: (~class_Orderings_Olinorder(T_a)|(c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)|c_Orderings_Oord__class_Oless(T_a,V_x,V_y)))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f194])).
% 72.81/9.82 fof(f1761,plain,(
% 72.81/9.82 ![T_a]: (~class_Orderings_Olinorder(T_a)|(![V_x,V_y]: (c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)|c_Orderings_Oord__class_Oless(T_a,V_x,V_y))))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f1760])).
% 72.81/9.82 fof(f1762,plain,(
% 72.81/9.82 ![X0,X1,X2]: (~class_Orderings_Olinorder(X0)|c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|c_Orderings_Oord__class_Oless(X0,X2,X1))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1761])).
% 72.81/9.82 fof(f1810,plain,(
% 72.81/9.82 ![V_x,V_y,T_a]: (~class_Orderings_Olinorder(T_a)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)|c_Orderings_Oord__class_Omin(T_a,V_x,V_y)=V_y))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f206])).
% 72.81/9.82 fof(f1811,plain,(
% 72.81/9.82 ![T_a]: (~class_Orderings_Olinorder(T_a)|(![V_x,V_y]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)|c_Orderings_Oord__class_Omin(T_a,V_x,V_y)=V_y)))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f1810])).
% 72.81/9.82 fof(f1812,plain,(
% 72.81/9.82 ![X0,X1,X2]: (~class_Orderings_Olinorder(X0)|~c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|c_Orderings_Oord__class_Omin(X0,X2,X1)=X1)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1811])).
% 72.81/9.82 fof(f1813,plain,(
% 72.81/9.82 ![V_y,V_x,T_a]: (~class_Orderings_Olinorder(T_a)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)|c_Orderings_Oord__class_Omin(T_a,V_x,V_y)=V_x))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f207])).
% 72.81/9.82 fof(f1814,plain,(
% 72.81/9.82 ![T_a]: (~class_Orderings_Olinorder(T_a)|(![V_y,V_x]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)|c_Orderings_Oord__class_Omin(T_a,V_x,V_y)=V_x)))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f1813])).
% 72.81/9.82 fof(f1815,plain,(
% 72.81/9.82 ![X0,X1,X2]: (~class_Orderings_Olinorder(X0)|~c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|c_Orderings_Oord__class_Omin(X0,X1,X2)=X1)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1814])).
% 72.81/9.82 fof(f1816,plain,(
% 72.81/9.82 ![V_a,V_x,V_b,T_a]: (~class_Orderings_Olinorder(T_a)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_b,V_x)|c_Orderings_Oord__class_Oless__eq(T_a,c_Orderings_Oord__class_Omin(T_a,V_a,V_b),V_x)))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f208])).
% 72.81/9.82 fof(f1817,plain,(
% 72.81/9.82 ![T_a]: (~class_Orderings_Olinorder(T_a)|(![V_x,V_b]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_b,V_x)|(![V_a]: c_Orderings_Oord__class_Oless__eq(T_a,c_Orderings_Oord__class_Omin(T_a,V_a,V_b),V_x)))))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f1816])).
% 72.81/9.82 fof(f1818,plain,(
% 72.81/9.82 ![X0,X1,X2,X3]: (~class_Orderings_Olinorder(X0)|~c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|c_Orderings_Oord__class_Oless__eq(X0,c_Orderings_Oord__class_Omin(X0,X3,X1),X2))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1817])).
% 72.81/9.82 fof(f1834,plain,(
% 72.81/9.82 ![V_y_2,V_x_2,T_a]: (~class_Orderings_Olinorder(T_a)|(c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)<=>c_Orderings_Oord__class_Omin(T_a,V_x_2,V_y_2)=V_x_2))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f212])).
% 72.81/9.82 fof(f1835,plain,(
% 72.81/9.82 ![V_y_2,V_x_2,T_a]: (~class_Orderings_Olinorder(T_a)|((~c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)|c_Orderings_Oord__class_Omin(T_a,V_x_2,V_y_2)=V_x_2)&(c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)|~c_Orderings_Oord__class_Omin(T_a,V_x_2,V_y_2)=V_x_2)))),
% 72.81/9.82 inference(NNF_transformation,[status(thm)],[f1834])).
% 72.81/9.82 fof(f1836,plain,(
% 72.81/9.82 ![T_a]: (~class_Orderings_Olinorder(T_a)|((![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)|c_Orderings_Oord__class_Omin(T_a,V_x_2,V_y_2)=V_x_2))&(![V_y_2,V_x_2]: (c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)|~c_Orderings_Oord__class_Omin(T_a,V_x_2,V_y_2)=V_x_2))))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f1835])).
% 72.81/9.82 fof(f1838,plain,(
% 72.81/9.82 ![X0,X1,X2]: (~class_Orderings_Olinorder(X0)|c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|~c_Orderings_Oord__class_Omin(X0,X1,X2)=X1)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1836])).
% 72.81/9.82 fof(f1886,plain,(
% 72.81/9.82 c_Transcendental_Osin(c_Transcendental_Opi)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f227])).
% 72.81/9.82 fof(f2227,plain,(
% 72.81/9.82 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f338])).
% 72.81/9.82 fof(f2284,plain,(
% 72.81/9.82 ![V_y_2,V_x_2]: ((~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)&~V_x_2=V_y_2))&(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|V_x_2=V_y_2)))),
% 72.81/9.82 inference(NNF_transformation,[status(thm)],[f352])).
% 72.81/9.82 fof(f2285,plain,(
% 72.81/9.82 (![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)&~V_x_2=V_y_2)))&(![V_y_2,V_x_2]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|V_x_2=V_y_2)))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f2284])).
% 72.81/9.82 fof(f2286,plain,(
% 72.81/9.82 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f2285])).
% 72.81/9.82 fof(f2481,plain,(
% 72.81/9.82 ![V_a,T_a]: (~class_Groups_Omonoid__add(T_a)|c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)=V_a)),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f427])).
% 72.81/9.82 fof(f2482,plain,(
% 72.81/9.82 ![T_a]: (~class_Groups_Omonoid__add(T_a)|(![V_a]: c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)=V_a))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f2481])).
% 72.81/9.82 fof(f2483,plain,(
% 72.81/9.82 ![X0,X1]: (~class_Groups_Omonoid__add(X0)|c_Groups_Oplus__class_Oplus(X0,c_Groups_Ozero__class_Ozero(X0),X1)=X1)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f2482])).
% 72.81/9.82 fof(f2492,plain,(
% 72.81/9.82 ![V_a,T_a]: (~class_Groups_Omonoid__add(T_a)|c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a)),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f430])).
% 72.81/9.82 fof(f2493,plain,(
% 72.81/9.82 ![T_a]: (~class_Groups_Omonoid__add(T_a)|(![V_a]: c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f2492])).
% 72.81/9.82 fof(f2494,plain,(
% 72.81/9.82 ![X0,X1]: (~class_Groups_Omonoid__add(X0)|c_Groups_Oplus__class_Oplus(X0,X1,c_Groups_Ozero__class_Ozero(X0))=X1)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f2493])).
% 72.81/9.82 fof(f2504,plain,(
% 72.81/9.82 ![V_d,V_c,V_b,V_a,T_a]: (~class_Groups_Oordered__ab__semigroup__add(T_a)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_a,V_b)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_c,V_d)|c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_d)))))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f434])).
% 72.81/9.82 fof(f2505,plain,(
% 72.81/9.82 ![T_a]: (~class_Groups_Oordered__ab__semigroup__add(T_a)|(![V_b,V_a]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_a,V_b)|(![V_d,V_c]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_c,V_d)|c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_d)))))))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f2504])).
% 72.81/9.82 fof(f2506,plain,(
% 72.81/9.82 ![X0,X1,X2,X3,X4]: (~class_Groups_Oordered__ab__semigroup__add(X0)|~c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|~c_Orderings_Oord__class_Oless__eq(X0,X3,X4)|c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Oplus__class_Oplus(X0,X1,X3),c_Groups_Oplus__class_Oplus(X0,X2,X4)))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f2505])).
% 72.81/9.82 fof(f2510,plain,(
% 72.81/9.82 ![V_c,V_b,V_a,T_a]: (~class_Groups_Oordered__ab__semigroup__add(T_a)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_a,V_b)|c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_c))))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f436])).
% 72.81/9.82 fof(f2511,plain,(
% 72.81/9.82 ![T_a]: (~class_Groups_Oordered__ab__semigroup__add(T_a)|(![V_b,V_a]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_a,V_b)|(![V_c]: c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_c))))))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f2510])).
% 72.81/9.82 fof(f2512,plain,(
% 72.81/9.82 ![X0,X1,X2,X3]: (~class_Groups_Oordered__ab__semigroup__add(X0)|~c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Oplus__class_Oplus(X0,X1,X3),c_Groups_Oplus__class_Oplus(X0,X2,X3)))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f2511])).
% 72.81/9.82 fof(f3439,plain,(
% 72.81/9.82 ![V_y,V_x]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x,V_y)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x,V_y),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f674])).
% 72.81/9.82 fof(f3440,plain,(
% 72.81/9.82 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f3439])).
% 72.81/9.82 fof(f3441,plain,(
% 72.81/9.82 ![V_y,V_x]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x,V_y)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x,V_y),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),V_y))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f675])).
% 72.81/9.82 fof(f3442,plain,(
% 72.81/9.82 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),X1))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f3441])).
% 72.81/9.82 fof(f3466,plain,(
% 72.81/9.82 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))=X0)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f689])).
% 72.81/9.82 fof(f3741,plain,(
% 72.81/9.82 ![V_c,V_a,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|c_Groups_Oplus__class_Oplus(T_a,V_a,V_c)=c_Groups_Oplus__class_Oplus(T_a,V_c,V_a))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f795])).
% 72.81/9.82 fof(f3742,plain,(
% 72.81/9.82 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_c,V_a]: c_Groups_Oplus__class_Oplus(T_a,V_a,V_c)=c_Groups_Oplus__class_Oplus(T_a,V_c,V_a)))),
% 72.81/9.82 inference(miniscoping,[status(thm)],[f3741])).
% 72.81/9.82 fof(f3743,plain,(
% 72.81/9.82 ![X0,X1,X2]: (~class_Rings_Ocomm__semiring__1(X0)|c_Groups_Oplus__class_Oplus(X0,X1,X2)=c_Groups_Oplus__class_Oplus(X0,X2,X1))),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f3742])).
% 72.81/9.82 fof(f4463,plain,(
% 72.81/9.82 class_Groups_Oordered__ab__semigroup__add(tc_RealDef_Oreal)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1108])).
% 72.81/9.82 fof(f4489,plain,(
% 72.81/9.82 class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1134])).
% 72.81/9.82 fof(f4496,plain,(
% 72.81/9.82 class_Orderings_Opreorder(tc_RealDef_Oreal)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1141])).
% 72.81/9.82 fof(f4497,plain,(
% 72.81/9.82 class_Orderings_Olinorder(tc_RealDef_Oreal)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1142])).
% 72.81/9.82 fof(f4500,plain,(
% 72.81/9.82 class_Groups_Omonoid__add(tc_RealDef_Oreal)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1145])).
% 72.81/9.82 fof(f4553,plain,(
% 72.81/9.82 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1198])).
% 72.81/9.82 fof(f4554,plain,(
% 72.81/9.82 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f1199])).
% 72.81/9.82 fof(f4555,plain,(
% 72.81/9.82 ((~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d1))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d2))),
% 72.81/9.82 inference(pre_NNF_transformation,[status(thm)],[f1201])).
% 72.81/9.82 fof(f4556,plain,(
% 72.81/9.82 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d2)),
% 72.81/9.82 inference(cnf_transformation,[status(thm)],[f4555])).
% 72.81/9.82 fof(f5684,plain,(
% 72.81/9.82 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 72.81/9.82 inference(resolution,[status(thm)],[f3440,f4554])).
% 72.81/9.82 fof(f5685,plain,(
% 72.81/9.82 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 72.81/9.82 inference(resolution,[status(thm)],[f3440,f4553])).
% 72.81/9.82 fof(f5863,plain,(
% 72.81/9.82 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d2)),
% 72.81/9.82 inference(resolution,[status(thm)],[f3442,f4554])).
% 72.81/9.82 fof(f5864,plain,(
% 72.81/9.82 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d1)),
% 72.81/9.82 inference(resolution,[status(thm)],[f3442,f4553])).
% 72.81/9.82 fof(f8975,plain,(
% 72.81/9.82 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),v_d2)),
% 72.81/9.82 inference(backward_demodulation,[status(thm)],[f1886,f4554])).
% 72.81/9.82 fof(f8977,plain,(
% 72.81/9.82 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d2)),
% 72.81/9.82 inference(backward_demodulation,[status(thm)],[f1886,f4556])).
% 72.81/9.82 fof(f10054,plain,(
% 72.81/9.82 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)),
% 72.81/9.82 inference(backward_demodulation,[status(thm)],[f10123,f8977])).
% 72.81/9.82 fof(f10084,plain,(
% 72.81/9.82 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))=X0)),
% 72.81/9.82 inference(backward_demodulation,[status(thm)],[f10123,f3466])).
% 72.81/9.82 fof(f10123,plain,(
% 72.81/9.82 c_Groups_Oone__class_Oone(tc_Int_Oint)=c_Int_OBit1(c_Int_OPls)),
% 72.81/9.82 inference(forward_demodulation,[status(thm)],[f1415,f1452])).
% 72.81/9.82 fof(f10159,plain,(
% 72.81/9.82 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f10123,f10054])).
% 72.81/9.83 fof(f10160,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f10123,f10159])).
% 72.81/9.83 fof(f10167,plain,(
% 72.81/9.83 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))=X0)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f10123,f10084])).
% 72.81/9.83 fof(f11906,plain,(
% 72.81/9.83 ![X0,X1]: (c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,X1)=c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X1,X0))),
% 72.81/9.83 inference(resolution,[status(thm)],[f1536,f4497])).
% 72.81/9.83 fof(f12541,plain,(
% 72.81/9.83 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)=X0)),
% 72.81/9.83 inference(resolution,[status(thm)],[f2483,f4500])).
% 72.81/9.83 fof(f12544,plain,(
% 72.81/9.83 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),X0)=X0)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f1886,f12541])).
% 72.81/9.83 fof(f12581,plain,(
% 72.81/9.83 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=X0)),
% 72.81/9.83 inference(resolution,[status(thm)],[f2494,f4500])).
% 72.81/9.83 fof(f12584,plain,(
% 72.81/9.83 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Transcendental_Osin(c_Transcendental_Opi))=X0)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f1886,f12581])).
% 72.81/9.83 fof(f14809,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),v_d2)),
% 72.81/9.83 inference(resolution,[status(thm)],[f2286,f8975])).
% 72.81/9.83 fof(f16517,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)),
% 72.81/9.83 inference(backward_demodulation,[status(thm)],[f11906,f10160])).
% 72.81/9.83 fof(f16532,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f11906,f16517])).
% 72.81/9.83 fof(f16533,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f11906,f16532])).
% 72.81/9.83 fof(f18157,plain,(
% 72.81/9.83 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0))),
% 72.81/9.83 inference(resolution,[status(thm)],[f1762,f4497])).
% 72.81/9.83 fof(f22222,plain,(
% 72.81/9.83 ![X0,X1]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)=c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))),
% 72.81/9.83 inference(resolution,[status(thm)],[f3743,f4489])).
% 72.81/9.83 fof(f26160,plain,(
% 72.81/9.83 ![X0,X1]: (~class_Orderings_Olinorder(tc_RealDef_Oreal)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,X1)=X1|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1))),
% 72.81/9.83 inference(resolution,[status(thm)],[f1812,f2227])).
% 72.81/9.83 fof(f26267,plain,(
% 72.81/9.83 ![X0,X1]: (c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,X1)=X1|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1))),
% 72.81/9.83 inference(forward_subsumption_resolution,[status(thm)],[f26160,f4497])).
% 72.81/9.83 fof(f28669,plain,(
% 72.81/9.83 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|~c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,X1)=X0)),
% 72.81/9.83 inference(resolution,[status(thm)],[f1838,f4497])).
% 72.81/9.83 fof(f30175,plain,(
% 72.81/9.83 ![X0,X1]: (c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,X1)=X1|~class_Orderings_Olinorder(tc_RealDef_Oreal)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,X1)=X0)),
% 72.81/9.83 inference(resolution,[status(thm)],[f26267,f1815])).
% 72.81/9.83 fof(f30176,plain,(
% 72.81/9.83 ![X0,X1]: (c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,X1)=X1|~class_Orderings_Olinorder(tc_RealDef_Oreal)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X1,X0)=X0)),
% 72.81/9.83 inference(resolution,[status(thm)],[f26267,f1812])).
% 72.81/9.83 fof(f30240,plain,(
% 72.81/9.83 ![X0,X1]: (c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,X1)=X1|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,X1)=X0)),
% 72.81/9.83 inference(forward_subsumption_resolution,[status(thm)],[f30175,f4497])).
% 72.81/9.83 fof(f30241,plain,(
% 72.81/9.83 ![X0,X1]: (c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,X1)=X1|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X1,X0)=X0)),
% 72.81/9.83 inference(forward_subsumption_resolution,[status(thm)],[f30176,f4497])).
% 72.81/9.83 fof(f45395,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(paramodulation,[status(thm)],[f30240,f16533])).
% 72.81/9.83 fof(f48415,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2)=v_d2),
% 72.81/9.83 inference(paramodulation,[status(thm)],[f30241,f45395])).
% 72.81/9.83 fof(f48419,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f11906,f48415])).
% 72.81/9.83 fof(f48420,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(duplicate_literals_removal,[status(thm)],[f48419])).
% 72.81/9.83 fof(f52318,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d1,v_d2)=v_d2),
% 72.81/9.83 inference(paramodulation,[status(thm)],[f30241,f48420])).
% 72.81/9.83 fof(f52321,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f11906,f52318])).
% 72.81/9.83 fof(f52322,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(duplicate_literals_removal,[status(thm)],[f52321])).
% 72.81/9.83 fof(f62648,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f1886,f5684])).
% 72.81/9.83 fof(f62649,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f22222,f62648])).
% 72.81/9.83 fof(f62650,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,c_Transcendental_Osin(c_Transcendental_Opi)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f1886,f62649])).
% 72.81/9.83 fof(f62651,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f12584,f62650])).
% 72.81/9.83 fof(f62653,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f10123,f62651])).
% 72.81/9.83 fof(f63436,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f1886,f5685])).
% 72.81/9.83 fof(f63437,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d1,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f22222,f63436])).
% 72.81/9.83 fof(f63438,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d1,c_Transcendental_Osin(c_Transcendental_Opi)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f1886,f63437])).
% 72.81/9.83 fof(f63439,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f12584,f63438])).
% 72.81/9.83 fof(f63442,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(backward_subsumption_resolution,[status(thm)],[f52322,f63443])).
% 72.81/9.83 fof(f63443,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f10123,f63439])).
% 72.81/9.83 fof(f75381,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d2)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f22222,f5863])).
% 72.81/9.83 fof(f75382,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,c_Transcendental_Osin(c_Transcendental_Opi)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d2)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f1886,f75381])).
% 72.81/9.83 fof(f75383,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d2)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f12584,f75382])).
% 72.81/9.83 fof(f75390,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f10123,f75383])).
% 72.81/9.83 fof(f76340,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d1,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d1)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f22222,f5864])).
% 72.81/9.83 fof(f76341,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d1,c_Transcendental_Osin(c_Transcendental_Opi)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d1)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f1886,f76340])).
% 72.81/9.83 fof(f76342,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_d1)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f12584,f76341])).
% 72.81/9.83 fof(f76347,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(backward_subsumption_resolution,[status(thm)],[f63442,f76348])).
% 72.81/9.83 fof(f76348,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f10123,f76342])).
% 72.81/9.83 fof(f78832,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_d2,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))),
% 72.81/9.83 inference(resolution,[status(thm)],[f76347,f18157])).
% 72.81/9.83 fof(f82434,plain,(
% 72.81/9.83 ~class_Groups_Oordered__ab__semigroup__add(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,v_d2),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))))))|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(resolution,[status(thm)],[f2506,f78832])).
% 72.81/9.83 fof(f83189,plain,(
% 72.81/9.83 ~class_Groups_Oordered__ab__semigroup__add(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,v_d2),v_d1)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f10167,f82434])).
% 72.81/9.83 fof(f83190,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,v_d2),v_d1)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(forward_subsumption_resolution,[status(thm)],[f83189,f4463])).
% 72.81/9.83 fof(f85092,plain,(
% 72.81/9.83 ![X0]: (~class_Groups_Oordered__ab__semigroup__add(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),X0),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,X0)))),
% 72.81/9.83 inference(resolution,[status(thm)],[f2512,f14809])).
% 72.81/9.83 fof(f85411,plain,(
% 72.81/9.83 ![X0]: (~class_Groups_Oordered__ab__semigroup__add(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,X0)))),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f12544,f85092])).
% 72.81/9.83 fof(f85412,plain,(
% 72.81/9.83 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,X0)))),
% 72.81/9.83 inference(forward_subsumption_resolution,[status(thm)],[f85411,f4463])).
% 72.81/9.83 fof(f85558,plain,(
% 72.81/9.83 ![X0]: (c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2|~class_Orderings_Olinorder(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,v_d2)),v_d1))),
% 72.81/9.83 inference(resolution,[status(thm)],[f83190,f1818])).
% 72.81/9.83 fof(f85617,plain,(
% 72.81/9.83 ![X0]: (c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,v_d2)),v_d1))),
% 72.81/9.83 inference(forward_subsumption_resolution,[status(thm)],[f85558,f4497])).
% 72.81/9.83 fof(f86893,plain,(
% 72.81/9.83 ![X0]: (~class_Orderings_Olinorder(tc_RealDef_Oreal)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,X0))=X0)),
% 72.81/9.83 inference(resolution,[status(thm)],[f85412,f1815])).
% 72.81/9.83 fof(f87095,plain,(
% 72.81/9.83 ![X0]: (c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_d2,X0))=X0)),
% 72.81/9.83 inference(forward_subsumption_resolution,[status(thm)],[f86893,f4497])).
% 72.81/9.83 fof(f96213,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_d2,v_d1)),
% 72.81/9.83 inference(paramodulation,[status(thm)],[f87095,f85617])).
% 72.81/9.83 fof(f96282,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_d2,v_d1)),
% 72.81/9.83 inference(forward_subsumption_resolution,[status(thm)],[f96213,f28669])).
% 72.81/9.83 fof(f96314,plain,(
% 72.81/9.83 ~class_Orderings_Olinorder(tc_RealDef_Oreal)|c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(resolution,[status(thm)],[f96282,f1815])).
% 72.81/9.83 fof(f96327,plain,(
% 72.81/9.83 ![X0]: (~class_Orderings_Opreorder(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_d2)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_d1))),
% 72.81/9.83 inference(resolution,[status(thm)],[f96282,f1728])).
% 72.81/9.83 fof(f96376,plain,(
% 72.81/9.83 c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1)=v_d2),
% 72.81/9.83 inference(forward_subsumption_resolution,[status(thm)],[f96314,f4497])).
% 72.81/9.83 fof(f96391,plain,(
% 72.81/9.83 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_d2)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_d1))),
% 72.81/9.83 inference(forward_subsumption_resolution,[status(thm)],[f96327,f4496])).
% 72.81/9.83 fof(f96551,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)),
% 72.81/9.83 inference(backward_demodulation,[status(thm)],[f96376,f16533])).
% 72.81/9.83 fof(f96791,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Orderings_Oord__class_Omin(tc_RealDef_Oreal,v_d2,v_d1),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f96376,f96551])).
% 72.81/9.83 fof(f96792,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Osin(c_Transcendental_Opi),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)),
% 72.81/9.83 inference(forward_demodulation,[status(thm)],[f96376,f96791])).
% 72.81/9.83 fof(f96793,plain,(
% 72.81/9.83 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d2)),
% 72.81/9.94 inference(forward_subsumption_resolution,[status(thm)],[f96792,f62653])).
% 72.81/9.94 fof(f96799,plain,(
% 72.81/9.94 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)),
% 72.81/9.94 inference(forward_subsumption_resolution,[status(thm)],[f96793,f75390])).
% 72.81/9.94 fof(f102633,plain,(
% 72.81/9.94 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_d2,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),v_d1)),
% 72.81/9.94 inference(resolution,[status(thm)],[f96391,f75390])).
% 72.81/9.94 fof(f102641,plain,(
% 72.81/9.94 $false),
% 72.81/9.94 inference(forward_subsumption_resolution,[status(thm)],[f102633,f96799])).
% 72.81/9.94 % SZS output end CNFRefutation for theBenchmark.p
% 2.83/10.03 % Elapsed time: 9.644106 seconds
% 2.83/10.03 % CPU time: 74.301166 seconds
% 2.83/10.03 % Total memory used: 640.630 MB
% 2.83/10.03 % Net memory used: 611.089 MB
%------------------------------------------------------------------------------