%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW224+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:50 PM UTC 2026
% Result : Theorem 20.05s 8.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW224+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/5.43 % Computer : n011.cluster.edu
% 0.17/5.43 % Model : x86_64 x86_64
% 0.17/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.43 % Memory : 8046.5625MB
% 0.17/5.43 % OS : Linux 6.8.0-71-generic
% 0.17/5.44 % CPULimit : 300
% 0.17/5.44 % WCLimit : 300
% 0.17/5.44 % DateTime : Mon Sep 21 09:42:45 UTC 2026
% 0.17/5.44 % CPUTime :
% 0.21/5.58 % Drodi V4.1.1
% 20.05/8.21 % Refutation found
% 20.05/8.21 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.05/8.21 % SZS output start CNFRefutation for theBenchmark
% 20.05/8.21 fof(f2,axiom,(
% 20.05/8.21 (! [V_ra_2,V_a_2,V_x_2,T_a] :( class_Rings_Olinordered__idom(T_a)=> ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2)<=> ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2)& c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2)) ) ) ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f9,axiom,(
% 20.05/8.21 (! [V_d,V_c,V_b,V_a,T_a] :( class_Groups_Oordered__cancel__ab__semigroup__add(T_a)=> ( c_Orderings_Oord__class_Oless(T_a,V_a,V_b)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_c,V_d)=> c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_d)) ) ) ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f60,axiom,(
% 20.05/8.21 (! [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) ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f64,axiom,(
% 20.05/8.21 (! [V_z,V_y,V_x,T_a] :( class_Orderings_Opreorder(T_a)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)=> ( c_Orderings_Oord__class_Oless(T_a,V_y,V_z)=> c_Orderings_Oord__class_Oless(T_a,V_x,V_z) ) ) ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f79,axiom,(
% 20.05/8.21 (! [V_y_2,V_x_2,T_a] :( class_Orderings_Opreorder(T_a)=> ( c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)<=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)& ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2) ) ) ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f100,axiom,(
% 20.05/8.21 (! [V_b,V_a,T_a] :( class_Groups_Ogroup__add(T_a)=> c_Groups_Ominus__class_Ominus(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_b),V_b) = V_a ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f101,axiom,(
% 20.05/8.21 (! [V_b,V_a,T_a] :( class_Groups_Ogroup__add(T_a)=> c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_b) = V_a ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f105,axiom,(
% 20.05/8.21 (! [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 ) ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f108,axiom,(
% 20.05/8.21 (! [V_y_2,V_x_2] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)<=> c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_y_2,V_x_2)) ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f116,axiom,(
% 20.05/8.21 (! [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) ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f132,axiom,(
% 20.05/8.21 (! [V_a,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a) = V_a ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f142,axiom,(
% 20.05/8.21 (! [V_a,T_a] :( class_Groups_Ogroup__add(T_a)=> c_Groups_Ominus__class_Ominus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a ) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f414,axiom,(
% 20.05/8.21 (! [V_r] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,V_r) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) )),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f1098,axiom,(
% 20.05/8.21 class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal) ),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f1131,axiom,(
% 20.05/8.21 class_Rings_Olinordered__idom(tc_RealDef_Oreal) ),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f1132,axiom,(
% 20.05/8.21 class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal) ),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f1137,axiom,(
% 20.05/8.21 class_Orderings_Opreorder(tc_RealDef_Oreal) ),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f1143,axiom,(
% 20.05/8.21 class_Groups_Ogroup__add(tc_RealDef_Oreal) ),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f1186,hypothesis,(
% 20.05/8.21 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_m,v_x) ),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f1187,hypothesis,(
% 20.05/8.21 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_x,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_m,v_e)) ),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f1188,conjecture,(
% 20.05/8.21 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_x,v_m)),v_e) ),
% 20.05/8.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.05/8.21 fof(f1189,negated_conjecture,(
% 20.05/8.21 ~(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_x,v_m)),v_e) )),
% 20.05/8.21 inference(negated_conjecture,[status(cth)],[f1188])).
% 20.05/8.21 fof(f1193,plain,(
% 20.05/8.21 ![V_ra_2,V_a_2,V_x_2,T_a]: (~class_Rings_Olinordered__idom(T_a)|(c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2)<=>(c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2)&c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2)))))),
% 20.05/8.21 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 20.05/8.21 fof(f1194,plain,(
% 20.05/8.21 ![V_ra_2,V_a_2,V_x_2,T_a]: (~class_Rings_Olinordered__idom(T_a)|((~c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2)|(c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2)&c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2))))&(c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2)|(~c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2)|~c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2))))))),
% 20.05/8.21 inference(NNF_transformation,[status(thm)],[f1193])).
% 20.05/8.21 fof(f1195,plain,(
% 20.05/8.21 ![T_a]: (~class_Rings_Olinordered__idom(T_a)|((![V_ra_2,V_a_2,V_x_2]: (~c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2)|(c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2)&c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2)))))&(![V_ra_2,V_a_2,V_x_2]: (c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2)|(~c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2)|~c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2)))))))),
% 20.05/8.21 inference(miniscoping,[status(thm)],[f1194])).
% 20.05/8.21 fof(f1198,plain,(
% 20.05/8.21 ![X0,X1,X2,X3]: (~class_Rings_Olinordered__idom(X0)|c_Orderings_Oord__class_Oless(X0,c_Groups_Oabs__class_Oabs(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2)),X3)|~c_Orderings_Oord__class_Oless(X0,c_Groups_Ominus__class_Ominus(X0,X2,X3),X1)|~c_Orderings_Oord__class_Oless(X0,X1,c_Groups_Oplus__class_Oplus(X0,X2,X3)))),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1195])).
% 20.05/8.21 fof(f1217,plain,(
% 20.05/8.21 ![V_d,V_c,V_b,V_a,T_a]: (~class_Groups_Oordered__cancel__ab__semigroup__add(T_a)|(~c_Orderings_Oord__class_Oless(T_a,V_a,V_b)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_c,V_d)|c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_d)))))),
% 20.05/8.21 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 20.05/8.21 fof(f1218,plain,(
% 20.05/8.21 ![T_a]: (~class_Groups_Oordered__cancel__ab__semigroup__add(T_a)|(![V_b,V_a]: (~c_Orderings_Oord__class_Oless(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(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_d)))))))),
% 20.05/8.21 inference(miniscoping,[status(thm)],[f1217])).
% 20.05/8.21 fof(f1219,plain,(
% 20.05/8.21 ![X0,X1,X2,X3,X4]: (~class_Groups_Oordered__cancel__ab__semigroup__add(X0)|~c_Orderings_Oord__class_Oless(X0,X1,X2)|~c_Orderings_Oord__class_Oless__eq(X0,X3,X4)|c_Orderings_Oord__class_Oless(X0,c_Groups_Oplus__class_Oplus(X0,X1,X3),c_Groups_Oplus__class_Oplus(X0,X2,X4)))),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1218])).
% 20.05/8.21 fof(f1391,plain,(
% 20.05/8.21 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f60])).
% 20.05/8.21 fof(f1399,plain,(
% 20.05/8.21 ![V_z,V_y,V_x,T_a]: (~class_Orderings_Opreorder(T_a)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)|(~c_Orderings_Oord__class_Oless(T_a,V_y,V_z)|c_Orderings_Oord__class_Oless(T_a,V_x,V_z))))),
% 20.05/8.21 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 20.05/8.21 fof(f1400,plain,(
% 20.05/8.21 ![T_a]: (~class_Orderings_Opreorder(T_a)|(![V_y,V_x]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)|(![V_z]: (~c_Orderings_Oord__class_Oless(T_a,V_y,V_z)|c_Orderings_Oord__class_Oless(T_a,V_x,V_z))))))),
% 20.05/8.21 inference(miniscoping,[status(thm)],[f1399])).
% 20.05/8.21 fof(f1401,plain,(
% 20.05/8.21 ![X0,X1,X2,X3]: (~class_Orderings_Opreorder(X0)|~c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|~c_Orderings_Oord__class_Oless(X0,X2,X3)|c_Orderings_Oord__class_Oless(X0,X1,X3))),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1400])).
% 20.05/8.21 fof(f1451,plain,(
% 20.05/8.21 ![V_y_2,V_x_2,T_a]: (~class_Orderings_Opreorder(T_a)|(c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)<=>(c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)&~c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2))))),
% 20.05/8.21 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 20.05/8.21 fof(f1452,plain,(
% 20.05/8.21 ![V_y_2,V_x_2,T_a]: (~class_Orderings_Opreorder(T_a)|((~c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)&~c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2)))&(c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)|c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2)))))),
% 20.05/8.21 inference(NNF_transformation,[status(thm)],[f1451])).
% 20.05/8.21 fof(f1453,plain,(
% 20.05/8.21 ![T_a]: (~class_Orderings_Opreorder(T_a)|((![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)&~c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2))))&(![V_y_2,V_x_2]: (c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)|c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2))))))),
% 20.05/8.21 inference(miniscoping,[status(thm)],[f1452])).
% 20.05/8.21 fof(f1456,plain,(
% 20.05/8.21 ![X0,X1,X2]: (~class_Orderings_Opreorder(X0)|c_Orderings_Oord__class_Oless(X0,X1,X2)|~c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|c_Orderings_Oord__class_Oless__eq(X0,X2,X1))),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1453])).
% 20.05/8.21 fof(f1536,plain,(
% 20.05/8.21 ![V_b,V_a,T_a]: (~class_Groups_Ogroup__add(T_a)|c_Groups_Ominus__class_Ominus(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_b),V_b)=V_a)),
% 20.05/8.21 inference(pre_NNF_transformation,[status(thm)],[f100])).
% 20.05/8.21 fof(f1537,plain,(
% 20.05/8.21 ![T_a]: (~class_Groups_Ogroup__add(T_a)|(![V_b,V_a]: c_Groups_Ominus__class_Ominus(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_b),V_b)=V_a))),
% 20.05/8.21 inference(miniscoping,[status(thm)],[f1536])).
% 20.05/8.21 fof(f1538,plain,(
% 20.05/8.21 ![X0,X1,X2]: (~class_Groups_Ogroup__add(X0)|c_Groups_Ominus__class_Ominus(X0,c_Groups_Oplus__class_Oplus(X0,X1,X2),X2)=X1)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1537])).
% 20.05/8.21 fof(f1539,plain,(
% 20.05/8.21 ![V_b,V_a,T_a]: (~class_Groups_Ogroup__add(T_a)|c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_b)=V_a)),
% 20.05/8.21 inference(pre_NNF_transformation,[status(thm)],[f101])).
% 20.05/8.21 fof(f1540,plain,(
% 20.05/8.21 ![T_a]: (~class_Groups_Ogroup__add(T_a)|(![V_b,V_a]: c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_b)=V_a))),
% 20.05/8.21 inference(miniscoping,[status(thm)],[f1539])).
% 20.05/8.21 fof(f1541,plain,(
% 20.05/8.21 ![X0,X1,X2]: (~class_Groups_Ogroup__add(X0)|c_Groups_Oplus__class_Oplus(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2),X2)=X1)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1540])).
% 20.05/8.21 fof(f1553,plain,(
% 20.05/8.21 ![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)))),
% 20.05/8.21 inference(NNF_transformation,[status(thm)],[f105])).
% 20.05/8.21 fof(f1554,plain,(
% 20.05/8.21 (![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)))),
% 20.05/8.21 inference(miniscoping,[status(thm)],[f1553])).
% 20.05/8.21 fof(f1556,plain,(
% 20.05/8.21 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|~X0=X1)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1554])).
% 20.05/8.21 fof(f1564,plain,(
% 20.05/8.21 ![V_y_2,V_x_2]: ((~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_y_2,V_x_2)))&(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|~c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_y_2,V_x_2))))),
% 20.05/8.21 inference(NNF_transformation,[status(thm)],[f108])).
% 20.05/8.21 fof(f1565,plain,(
% 20.05/8.21 (![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_y_2,V_x_2))))&(![V_y_2,V_x_2]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|~c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_y_2,V_x_2))))),
% 20.05/8.21 inference(miniscoping,[status(thm)],[f1564])).
% 20.05/8.21 fof(f1566,plain,(
% 20.05/8.21 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0)))),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1565])).
% 20.05/8.21 fof(f1567,plain,(
% 20.05/8.21 ![X0,X1]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|~c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0)))),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1565])).
% 20.05/8.21 fof(f1587,plain,(
% 20.05/8.21 ![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))),
% 20.05/8.21 inference(pre_NNF_transformation,[status(thm)],[f116])).
% 20.05/8.21 fof(f1588,plain,(
% 20.05/8.21 ![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)))),
% 20.05/8.21 inference(miniscoping,[status(thm)],[f1587])).
% 20.05/8.21 fof(f1589,plain,(
% 20.05/8.21 ![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))),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1588])).
% 20.05/8.21 fof(f1628,plain,(
% 20.05/8.21 ![V_a,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)=V_a)),
% 20.05/8.21 inference(pre_NNF_transformation,[status(thm)],[f132])).
% 20.05/8.21 fof(f1629,plain,(
% 20.05/8.21 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_a]: c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)=V_a))),
% 20.05/8.21 inference(miniscoping,[status(thm)],[f1628])).
% 20.05/8.21 fof(f1630,plain,(
% 20.05/8.21 ![X0,X1]: (~class_Rings_Ocomm__semiring__1(X0)|c_Groups_Oplus__class_Oplus(X0,c_Groups_Ozero__class_Ozero(X0),X1)=X1)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1629])).
% 20.05/8.21 fof(f1660,plain,(
% 20.05/8.21 ![V_a,T_a]: (~class_Groups_Ogroup__add(T_a)|c_Groups_Ominus__class_Ominus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a)),
% 20.05/8.21 inference(pre_NNF_transformation,[status(thm)],[f142])).
% 20.05/8.21 fof(f1661,plain,(
% 20.05/8.21 ![T_a]: (~class_Groups_Ogroup__add(T_a)|(![V_a]: c_Groups_Ominus__class_Ominus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a))),
% 20.05/8.21 inference(miniscoping,[status(thm)],[f1660])).
% 20.05/8.21 fof(f1662,plain,(
% 20.05/8.21 ![X0,X1]: (~class_Groups_Ogroup__add(X0)|c_Groups_Ominus__class_Ominus(X0,X1,c_Groups_Ozero__class_Ozero(X0))=X1)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1661])).
% 20.05/8.21 fof(f2553,plain,(
% 20.05/8.21 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f414])).
% 20.05/8.21 fof(f4417,plain,(
% 20.05/8.21 class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1098])).
% 20.05/8.21 fof(f4450,plain,(
% 20.05/8.21 class_Rings_Olinordered__idom(tc_RealDef_Oreal)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1131])).
% 20.05/8.21 fof(f4451,plain,(
% 20.05/8.21 class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1132])).
% 20.05/8.21 fof(f4456,plain,(
% 20.05/8.21 class_Orderings_Opreorder(tc_RealDef_Oreal)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1137])).
% 20.05/8.21 fof(f4462,plain,(
% 20.05/8.21 class_Groups_Ogroup__add(tc_RealDef_Oreal)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1143])).
% 20.05/8.21 fof(f4505,plain,(
% 20.05/8.21 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_m,v_x)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1186])).
% 20.05/8.21 fof(f4506,plain,(
% 20.05/8.21 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_x,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_m,v_e))),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1187])).
% 20.05/8.21 fof(f4507,plain,(
% 20.05/8.21 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_x,v_m)),v_e)),
% 20.05/8.21 inference(cnf_transformation,[status(thm)],[f1189])).
% 20.05/8.21 fof(f4603,plain,(
% 20.05/8.21 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X0))),
% 20.05/8.21 inference(destructive_equality_resolution,[status(thm)],[f1556])).
% 20.05/8.21 fof(f4658,plain,(
% 20.05/8.21 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_x,v_m)),v_e)),
% 20.05/8.21 inference(backward_demodulation,[status(thm)],[f2553,f4507])).
% 20.05/8.21 fof(f4808,plain,(
% 20.05/8.21 ~class_Rings_Olinordered__idom(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_x,v_m)),v_e)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e),v_x)),
% 20.05/8.21 inference(resolution,[status(thm)],[f4506,f1198])).
% 20.05/8.21 fof(f4809,plain,(
% 20.05/8.21 ~class_Rings_Olinordered__idom(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_x,v_m)),v_e)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e),v_x)),
% 20.05/8.21 inference(forward_demodulation,[status(thm)],[f2553,f4808])).
% 20.05/8.21 fof(f4810,plain,(
% 20.05/8.21 ~class_Rings_Olinordered__idom(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e),v_x)),
% 20.05/8.21 inference(forward_subsumption_resolution,[status(thm)],[f4809,f4658])).
% 20.05/8.21 fof(f6397,plain,(
% 20.05/8.21 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e),v_x)),
% 20.05/8.21 inference(backward_subsumption_resolution,[status(thm)],[f4810,f4450])).
% 20.05/8.21 fof(f8835,plain,(
% 20.05/8.21 ![X0]: (~class_Orderings_Opreorder(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_x,X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_m,X0))),
% 20.05/8.21 inference(resolution,[status(thm)],[f1401,f4505])).
% 20.05/8.21 fof(f8904,plain,(
% 20.05/8.21 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_x,X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_m,X0))),
% 20.05/8.21 inference(forward_subsumption_resolution,[status(thm)],[f8835,f4456])).
% 20.05/8.21 fof(f10630,plain,(
% 20.05/8.21 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)=X0)),
% 20.05/8.21 inference(resolution,[status(thm)],[f1630,f4451])).
% 20.05/8.21 fof(f10775,plain,(
% 20.05/8.21 ![X0]: (c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=X0)),
% 20.05/8.21 inference(resolution,[status(thm)],[f1662,f4462])).
% 20.05/8.21 fof(f11507,plain,(
% 20.05/8.21 ![X0,X1]: (~class_Orderings_Opreorder(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 20.05/8.21 inference(resolution,[status(thm)],[f1456,f1391])).
% 20.05/8.21 fof(f11550,plain,(
% 20.05/8.21 ![X0,X1]: (~class_Orderings_Opreorder(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 20.05/8.21 inference(duplicate_literals_removal,[status(thm)],[f11507])).
% 20.05/8.21 fof(f11551,plain,(
% 20.05/8.21 ![X0,X1]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 20.05/8.21 inference(forward_subsumption_resolution,[status(thm)],[f11550,f4456])).
% 20.05/8.21 fof(f11777,plain,(
% 20.05/8.21 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_x,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e))),
% 20.05/8.21 inference(resolution,[status(thm)],[f11551,f6397])).
% 20.05/8.21 fof(f12177,plain,(
% 20.05/8.21 ![X0,X1]: (~class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,v_x),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e))))),
% 20.05/8.21 inference(resolution,[status(thm)],[f11777,f1219])).
% 20.05/8.21 fof(f12187,plain,(
% 20.05/8.21 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,v_x),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e))))),
% 20.05/8.21 inference(forward_subsumption_resolution,[status(thm)],[f12177,f4417])).
% 20.05/8.21 fof(f18076,plain,(
% 20.05/8.21 ![X0,X1]: (c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),X1)=X0)),
% 20.05/8.21 inference(resolution,[status(thm)],[f1538,f4462])).
% 20.05/8.21 fof(f18079,plain,(
% 20.05/8.21 ![X0,X1]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1),X1)=X0)),
% 20.05/8.21 inference(resolution,[status(thm)],[f1541,f4462])).
% 20.05/8.21 fof(f19024,plain,(
% 20.05/8.21 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_m,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_m,v_e))),
% 20.05/8.21 inference(resolution,[status(thm)],[f8904,f4506])).
% 20.05/8.21 fof(f19369,plain,(
% 20.05/8.21 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|~c_RealDef_Opositive(X0))),
% 20.05/8.21 inference(paramodulation,[status(thm)],[f10775,f1567])).
% 20.05/8.21 fof(f20357,plain,(
% 20.05/8.21 ![X0,X1]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)=c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))),
% 20.05/8.21 inference(resolution,[status(thm)],[f1589,f4451])).
% 20.05/8.21 fof(f20495,plain,(
% 20.05/8.21 ![X0,X1]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0))=X1)),
% 20.05/8.21 inference(backward_demodulation,[status(thm)],[f20357,f18079])).
% 20.05/8.21 fof(f30739,plain,(
% 20.05/8.21 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_m,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_e,v_m))),
% 20.05/8.21 inference(forward_demodulation,[status(thm)],[f20357,f19024])).
% 20.05/8.21 fof(f30742,plain,(
% 20.05/8.21 c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_e,v_m),v_m))),
% 20.05/8.21 inference(resolution,[status(thm)],[f30739,f1566])).
% 20.05/8.21 fof(f30779,plain,(
% 20.05/8.21 c_RealDef_Opositive(v_e)),
% 20.05/8.21 inference(forward_demodulation,[status(thm)],[f18076,f30742])).
% 20.05/8.21 fof(f30818,plain,(
% 20.05/8.21 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_e)),
% 20.05/8.21 inference(resolution,[status(thm)],[f30779,f19369])).
% 20.05/8.21 fof(f30829,plain,(
% 20.05/8.21 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_x),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_e,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e)))),
% 20.05/8.21 inference(resolution,[status(thm)],[f30818,f12187])).
% 20.05/8.21 fof(f30870,plain,(
% 20.05/8.21 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_x,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_e,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e)))),
% 20.05/8.21 inference(forward_demodulation,[status(thm)],[f10630,f30829])).
% 20.05/8.21 fof(f30871,plain,(
% 20.05/8.21 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_x,v_m)),
% 20.05/8.21 inference(forward_demodulation,[status(thm)],[f20495,f30870])).
% 20.05/8.21 fof(f30920,plain,(
% 20.05/8.21 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_m,v_m)),
% 20.05/8.21 inference(resolution,[status(thm)],[f30871,f8904])).
% 20.19/8.25 fof(f30961,plain,(
% 20.19/8.25 $false),
% 20.19/8.25 inference(forward_subsumption_resolution,[status(thm)],[f30920,f4603])).
% 20.19/8.25 % SZS output end CNFRefutation for theBenchmark.p
% 20.19/8.27 % Elapsed time: 2.813786 seconds
% 20.19/8.27 % CPU time: 21.053488 seconds
% 20.19/8.27 % Total memory used: 346.184 MB
% 20.19/8.27 % Net memory used: 335.146 MB
%------------------------------------------------------------------------------