%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW233+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 : n013.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:51 PM UTC 2026
% Result : Theorem 39.18s 5.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW233+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n013.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:42:21 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.22/0.46 % Drodi V4.1.1
% 39.18/5.57 % Refutation found
% 39.18/5.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 39.18/5.57 % SZS output start CNFRefutation for theBenchmark
% 39.18/5.57 fof(f4,axiom,(
% 39.18/5.57 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)) ),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f5,axiom,(
% 39.18/5.57 (! [V_w] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_w) )),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f6,axiom,(
% 39.18/5.57 (! [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) ) )),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f7,axiom,(
% 39.18/5.57 (! [V_k,V_j,V_i] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j)=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k) ) ) )),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f8,axiom,(
% 39.18/5.57 (! [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)=> V_z = V_w ) ) )),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f31,axiom,(
% 39.18/5.57 (! [V_a,T_a] :( class_Groups_Oordered__ab__group__add__abs(T_a)=> c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Oabs__class_Oabs(T_a,V_a)) ) )),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f33,axiom,(
% 39.18/5.57 (! [V_a,T_a] :( class_Groups_Oordered__ab__group__add__abs(T_a)=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)=> c_Groups_Oabs__class_Oabs(T_a,V_a) = V_a ) ) )),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f41,axiom,(
% 39.18/5.57 (! [V_x,T_a] :( class_RealVector_Oreal__normed__vector(T_a)=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x)) ) )),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f74,axiom,(
% 39.18/5.57 (! [V_a,T_a] :( class_RealVector_Oreal__normed__vector(T_a)=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a)) = c_RealVector_Onorm__class_Onorm(T_a,V_a) ) )),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f212,axiom,(
% 39.18/5.57 (! [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) ) ) )),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f303,axiom,(
% 39.18/5.57 (! [V_a,T_a] :( class_Rings_Olinordered__semidom(T_a)=> c_Orderings_Oord__class_Oless(T_a,V_a,c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Oone__class_Oone(T_a))) ) )),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f326,axiom,(
% 39.18/5.57 (! [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) ) )),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f1112,axiom,(
% 39.18/5.57 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f1127,axiom,(
% 39.18/5.57 class_Rings_Olinordered__semidom(tc_RealDef_Oreal) ),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f1137,axiom,(
% 39.18/5.57 class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal) ),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f1145,axiom,(
% 39.18/5.57 class_Orderings_Olinorder(tc_RealDef_Oreal) ),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f1171,axiom,(
% 39.18/5.57 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f1261,conjecture,(
% 39.18/5.57 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)) ),
% 39.18/5.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.18/5.57 fof(f1262,negated_conjecture,(
% 39.18/5.57 ~(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)) )),
% 39.18/5.57 inference(negated_conjecture,[status(cth)],[f1261])).
% 39.18/5.57 fof(f1270,plain,(
% 39.18/5.57 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____))),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f4])).
% 39.18/5.57 fof(f1271,plain,(
% 39.18/5.57 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X0))),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f5])).
% 39.18/5.57 fof(f1272,plain,(
% 39.18/5.57 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f6])).
% 39.18/5.57 fof(f1273,plain,(
% 39.18/5.57 ![V_k,V_j,V_i]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j)|(~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k)))),
% 39.18/5.57 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 39.18/5.57 fof(f1274,plain,(
% 39.18/5.57 ![V_j,V_i]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j)|(![V_k]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k))))),
% 39.18/5.57 inference(miniscoping,[status(thm)],[f1273])).
% 39.18/5.57 fof(f1275,plain,(
% 39.18/5.57 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X2))),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1274])).
% 39.18/5.57 fof(f1276,plain,(
% 39.18/5.57 ![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)|V_z=V_w))),
% 39.18/5.57 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 39.18/5.57 fof(f1277,plain,(
% 39.18/5.57 ![X0,X1]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)|X0=X1)),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1276])).
% 39.18/5.57 fof(f1351,plain,(
% 39.18/5.57 ![V_a,T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Oabs__class_Oabs(T_a,V_a)))),
% 39.18/5.57 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 39.18/5.57 fof(f1352,plain,(
% 39.18/5.57 ![T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|(![V_a]: c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Oabs__class_Oabs(T_a,V_a))))),
% 39.18/5.57 inference(miniscoping,[status(thm)],[f1351])).
% 39.18/5.57 fof(f1353,plain,(
% 39.18/5.57 ![X0,X1]: (~class_Groups_Oordered__ab__group__add__abs(X0)|c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0),c_Groups_Oabs__class_Oabs(X0,X1)))),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1352])).
% 39.18/5.57 fof(f1359,plain,(
% 39.18/5.57 ![V_a,T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|(~c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)|c_Groups_Oabs__class_Oabs(T_a,V_a)=V_a))),
% 39.18/5.57 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 39.18/5.57 fof(f1360,plain,(
% 39.18/5.57 ![T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|(![V_a]: (~c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)|c_Groups_Oabs__class_Oabs(T_a,V_a)=V_a)))),
% 39.18/5.57 inference(miniscoping,[status(thm)],[f1359])).
% 39.18/5.57 fof(f1361,plain,(
% 39.18/5.57 ![X0,X1]: (~class_Groups_Oordered__ab__group__add__abs(X0)|~c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0),X1)|c_Groups_Oabs__class_Oabs(X0,X1)=X1)),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1360])).
% 39.18/5.57 fof(f1381,plain,(
% 39.18/5.57 ![V_x,T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x)))),
% 39.18/5.57 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 39.18/5.57 fof(f1382,plain,(
% 39.18/5.57 ![T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|(![V_x]: c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x))))),
% 39.18/5.57 inference(miniscoping,[status(thm)],[f1381])).
% 39.18/5.57 fof(f1383,plain,(
% 39.18/5.57 ![X0,X1]: (~class_RealVector_Oreal__normed__vector(X0)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X0,X1)))),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1382])).
% 39.18/5.57 fof(f1491,plain,(
% 39.18/5.57 ![V_a,T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a))=c_RealVector_Onorm__class_Onorm(T_a,V_a))),
% 39.18/5.57 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 39.18/5.57 fof(f1492,plain,(
% 39.18/5.57 ![T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|(![V_a]: c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a))=c_RealVector_Onorm__class_Onorm(T_a,V_a)))),
% 39.18/5.57 inference(miniscoping,[status(thm)],[f1491])).
% 39.18/5.57 fof(f1493,plain,(
% 39.18/5.57 ![X0,X1]: (~class_RealVector_Oreal__normed__vector(X0)|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X0,X1))=c_RealVector_Onorm__class_Onorm(X0,X1))),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1492])).
% 39.18/5.57 fof(f1981,plain,(
% 39.18/5.57 ![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)))),
% 39.18/5.57 inference(pre_NNF_transformation,[status(thm)],[f212])).
% 39.18/5.57 fof(f1982,plain,(
% 39.18/5.57 ![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))))),
% 39.18/5.57 inference(miniscoping,[status(thm)],[f1981])).
% 39.18/5.57 fof(f1983,plain,(
% 39.18/5.57 ![X0,X1,X2]: (~class_Orderings_Olinorder(X0)|~c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|~c_Orderings_Oord__class_Oless(X0,X2,X1))),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1982])).
% 39.18/5.57 fof(f2302,plain,(
% 39.18/5.57 ![V_a,T_a]: (~class_Rings_Olinordered__semidom(T_a)|c_Orderings_Oord__class_Oless(T_a,V_a,c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Oone__class_Oone(T_a))))),
% 39.18/5.57 inference(pre_NNF_transformation,[status(thm)],[f303])).
% 39.18/5.57 fof(f2303,plain,(
% 39.18/5.57 ![T_a]: (~class_Rings_Olinordered__semidom(T_a)|(![V_a]: c_Orderings_Oord__class_Oless(T_a,V_a,c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Oone__class_Oone(T_a)))))),
% 39.18/5.57 inference(miniscoping,[status(thm)],[f2302])).
% 39.18/5.57 fof(f2304,plain,(
% 39.18/5.57 ![X0,X1]: (~class_Rings_Olinordered__semidom(X0)|c_Orderings_Oord__class_Oless(X0,X1,c_Groups_Oplus__class_Oplus(X0,X1,c_Groups_Oone__class_Oone(X0))))),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f2303])).
% 39.18/5.57 fof(f2379,plain,(
% 39.18/5.57 ![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))),
% 39.18/5.57 inference(pre_NNF_transformation,[status(thm)],[f326])).
% 39.18/5.57 fof(f2380,plain,(
% 39.18/5.57 ![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)))),
% 39.18/5.57 inference(miniscoping,[status(thm)],[f2379])).
% 39.18/5.57 fof(f2381,plain,(
% 39.18/5.57 ![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))),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f2380])).
% 39.18/5.57 fof(f4506,plain,(
% 39.18/5.57 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1112])).
% 39.18/5.57 fof(f4521,plain,(
% 39.18/5.57 class_Rings_Olinordered__semidom(tc_RealDef_Oreal)),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1127])).
% 39.18/5.57 fof(f4531,plain,(
% 39.18/5.57 class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal)),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1137])).
% 39.18/5.57 fof(f4539,plain,(
% 39.18/5.57 class_Orderings_Olinorder(tc_RealDef_Oreal)),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1145])).
% 39.18/5.57 fof(f4565,plain,(
% 39.18/5.57 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1171])).
% 39.18/5.57 fof(f4713,plain,(
% 39.18/5.57 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____))),
% 39.18/5.57 inference(cnf_transformation,[status(thm)],[f1262])).
% 39.18/5.57 fof(f4939,plain,(
% 39.18/5.57 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),v_r____)),
% 39.18/5.57 inference(resolution,[status(thm)],[f1272,f4713])).
% 39.18/5.57 fof(f4941,plain,(
% 39.18/5.57 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)))),
% 39.18/5.57 inference(resolution,[status(thm)],[f1275,f4713])).
% 39.18/5.57 fof(f4957,plain,(
% 39.18/5.57 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|X0=X1|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X0))),
% 39.18/5.57 inference(resolution,[status(thm)],[f1277,f1275])).
% 39.18/5.57 fof(f5124,plain,(
% 39.18/5.57 ![X0,X1,X2,X3]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|X0=X1|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X3)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X3,X2))),
% 39.18/5.57 inference(resolution,[status(thm)],[f4957,f1275])).
% 39.18/5.57 fof(f5460,plain,(
% 39.18/5.57 ![X0,X1,X2,X3]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|X0=X1|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X3,X2)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X3,X1))),
% 39.18/5.57 inference(resolution,[status(thm)],[f5124,f1272])).
% 39.18/5.57 fof(f5756,plain,(
% 39.18/5.57 ![X0,X1]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|X0=X1|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,X0)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),X1))),
% 39.18/5.57 inference(resolution,[status(thm)],[f5460,f4939])).
% 39.18/5.57 fof(f5798,plain,(
% 39.18/5.57 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,X0)|v_r____=X0|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),X0))),
% 39.18/5.57 inference(resolution,[status(thm)],[f5756,f1272])).
% 39.18/5.57 fof(f5931,definition,(
% 39.18/5.57 sQ41_spl <=> (c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r____)),
% 39.18/5.57 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 39.18/5.57 fof(f5932,plain,(
% 39.18/5.57 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r____|~sQ41_spl),
% 39.18/5.57 inference(component_clause,[status(thm)],[f5931])).
% 39.18/5.57 fof(f6000,definition,(
% 39.18/5.57 sQ46_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)))),
% 39.18/5.57 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 39.18/5.57 fof(f6002,plain,(
% 39.18/5.57 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____))|sQ46_spl),
% 39.18/5.57 inference(component_clause,[status(thm)],[f6000])).
% 39.18/5.57 fof(f6003,definition,(
% 39.18/5.57 sQ47_spl <=> (c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____))),
% 39.18/5.57 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 39.18/5.57 fof(f6004,plain,(
% 39.18/5.57 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)|~sQ47_spl),
% 39.18/5.57 inference(component_clause,[status(thm)],[f6003])).
% 39.18/5.57 fof(f6006,definition,(
% 39.18/5.57 sQ48_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 39.18/5.57 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 39.18/5.57 fof(f6007,plain,(
% 39.18/5.57 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~sQ48_spl),
% 39.18/5.57 inference(component_clause,[status(thm)],[f6006])).
% 39.18/5.57 fof(f6122,plain,(
% 39.18/5.57 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)=X0)),
% 39.18/5.57 inference(resolution,[status(thm)],[f4506,f1361])).
% 39.18/5.57 fof(f6125,plain,(
% 39.18/5.57 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)))),
% 39.18/5.57 inference(resolution,[status(thm)],[f4506,f1353])).
% 39.18/5.57 fof(f6144,plain,(
% 39.18/5.57 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____))|c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____))|~sQ48_spl),
% 39.18/5.57 inference(resolution,[status(thm)],[f6007,f5124])).
% 39.18/5.57 fof(f6153,plain,(
% 39.18/5.57 ~sQ46_spl|sQ47_spl|~sQ48_spl),
% 39.18/5.57 inference(split_clause,[status(thm)],[f6144,f6000,f6003,f6006])).
% 39.18/5.57 fof(f6354,plain,(
% 39.18/5.57 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_r____)|~sQ47_spl),
% 39.18/5.57 inference(backward_demodulation,[status(thm)],[f6004,f4939])).
% 39.18/5.57 fof(f6376,plain,(
% 39.18/5.57 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|v_r____=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~sQ47_spl),
% 39.18/5.57 inference(resolution,[status(thm)],[f6354,f5124])).
% 39.18/5.57 fof(f6383,definition,(
% 39.18/5.57 sQ50_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 39.18/5.57 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 39.18/5.57 fof(f6384,plain,(
% 39.18/5.57 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~sQ50_spl),
% 39.18/5.57 inference(component_clause,[status(thm)],[f6383])).
% 39.18/5.57 fof(f6385,plain,(
% 39.18/5.57 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|sQ50_spl),
% 39.18/5.57 inference(component_clause,[status(thm)],[f6383])).
% 39.18/5.57 fof(f6391,plain,(
% 39.18/5.57 ~sQ50_spl|sQ41_spl|~sQ47_spl),
% 39.18/5.57 inference(split_clause,[status(thm)],[f6376,f6383,f5931,f6003])).
% 39.18/5.57 fof(f6397,plain,(
% 39.18/5.57 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|sQ50_spl)),
% 39.18/5.57 inference(resolution,[status(thm)],[f6385,f1275])).
% 39.18/5.57 fof(f6485,plain,(
% 39.18/5.57 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,v_r____)|sQ50_spl)),
% 39.18/5.57 inference(resolution,[status(thm)],[f6397,f1272])).
% 39.18/5.57 fof(f6757,plain,(
% 39.18/5.57 ![X0,X1]: (~class_RealVector_Oreal__normed__vector(X0)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(X0,X1))|~sQ41_spl)),
% 39.18/5.57 inference(backward_demodulation,[status(thm)],[f5932,f1383])).
% 39.18/5.57 fof(f6828,plain,(
% 39.18/5.57 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))|~sQ41_spl)),
% 39.18/5.57 inference(resolution,[status(thm)],[f4565,f6757])).
% 39.18/5.57 fof(f6863,plain,(
% 39.18/5.57 $false|~sQ41_spl),
% 39.18/5.57 inference(backward_subsumption_resolution,[status(thm)],[f4713,f6828])).
% 39.18/5.57 fof(f6885,plain,(
% 39.18/5.57 ~sQ41_spl),
% 39.18/5.57 inference(contradiction_clause,[status(thm)],[f6863])).
% 39.18/5.57 fof(f7257,plain,(
% 39.18/5.57 ![X0]: (c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))=c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))),
% 39.18/5.57 inference(resolution,[status(thm)],[f1493,f4565])).
% 39.18/5.57 fof(f9749,definition,(
% 39.18/5.57 sQ134_spl <=> (v_r____=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____))),
% 39.18/5.57 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 39.18/5.57 fof(f9750,plain,(
% 39.18/5.57 v_r____=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____)|~sQ134_spl),
% 39.18/5.57 inference(component_clause,[status(thm)],[f9749])).
% 39.18/5.57 fof(f9961,plain,(
% 39.18/5.57 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_r____)|sQ50_spl),
% 39.18/5.57 inference(resolution,[status(thm)],[f6485,f1271])).
% 39.18/5.57 fof(f10178,plain,(
% 39.18/5.57 v_r____=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~sQ50_spl),
% 39.18/5.62 inference(resolution,[status(thm)],[f6384,f5798])).
% 39.18/5.62 fof(f10198,plain,(
% 39.18/5.62 sQ41_spl|sQ48_spl|~sQ50_spl),
% 39.18/5.62 inference(split_clause,[status(thm)],[f10178,f5931,f6006,f6383])).
% 39.18/5.62 fof(f14441,plain,(
% 39.18/5.62 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),v_r____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____))|~sQ134_spl),
% 39.18/5.62 inference(forward_demodulation,[status(thm)],[f9750,f1270])).
% 39.18/5.62 fof(f14659,plain,(
% 39.18/5.62 ![X0,X1]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0))),
% 39.18/5.62 inference(resolution,[status(thm)],[f1983,f4539])).
% 39.18/5.62 fof(f14694,plain,(
% 39.18/5.62 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),v_r____))|~sQ134_spl),
% 39.18/5.62 inference(resolution,[status(thm)],[f4941,f14441])).
% 39.18/5.62 fof(f15019,plain,(
% 39.18/5.62 ![X0,X1]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)=c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))),
% 39.18/5.62 inference(resolution,[status(thm)],[f2381,f4531])).
% 39.18/5.62 fof(f15272,plain,(
% 39.18/5.62 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),v_r____),v_r____)|~sQ134_spl),
% 39.18/5.62 inference(resolution,[status(thm)],[f14694,f1272])).
% 39.18/5.62 fof(f17518,plain,(
% 39.18/5.62 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))),
% 39.18/5.62 inference(resolution,[status(thm)],[f2304,f4521])).
% 39.18/5.62 fof(f20043,plain,(
% 39.18/5.62 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0)))),
% 39.18/5.62 inference(paramodulation,[status(thm)],[f7257,f6125])).
% 39.18/5.62 fof(f20102,plain,(
% 39.18/5.62 $false|sQ46_spl),
% 39.18/5.62 inference(backward_subsumption_resolution,[status(thm)],[f6002,f20043])).
% 39.18/5.62 fof(f20129,plain,(
% 39.18/5.62 sQ46_spl),
% 39.18/5.62 inference(contradiction_clause,[status(thm)],[f20102])).
% 39.18/5.62 fof(f20937,plain,(
% 39.18/5.62 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X0))),
% 39.18/5.62 inference(resolution,[status(thm)],[f17518,f14659])).
% 39.18/5.62 fof(f24229,plain,(
% 39.18/5.62 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0),X0))),
% 39.18/5.62 inference(paramodulation,[status(thm)],[f15019,f20937])).
% 39.18/5.62 fof(f28052,plain,(
% 39.18/5.62 c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____)=v_r____|sQ50_spl),
% 39.18/5.62 inference(resolution,[status(thm)],[f6122,f9961])).
% 39.18/5.62 fof(f28069,plain,(
% 39.18/5.62 sQ134_spl|sQ50_spl),
% 39.18/5.62 inference(split_clause,[status(thm)],[f28052,f9749,f6383])).
% 39.18/5.62 fof(f28080,plain,(
% 39.18/5.62 $false|~sQ134_spl),
% 39.18/5.62 inference(forward_subsumption_resolution,[status(thm)],[f15272,f24229])).
% 39.18/5.62 fof(f28081,plain,(
% 39.18/5.62 ~sQ134_spl),
% 39.18/5.62 inference(contradiction_clause,[status(thm)],[f28080])).
% 39.18/5.62 fof(f28082,plain,(
% 39.18/5.62 $false),
% 39.18/5.62 inference(sat_refutation,[status(thm)],[f6153,f6391,f6885,f10198,f20129,f28069,f28081])).
% 39.18/5.62 % SZS output end CNFRefutation for theBenchmark.p
% 5.31/5.63 % Elapsed time: 5.259580 seconds
% 5.31/5.63 % CPU time: 40.802089 seconds
% 5.31/5.63 % Total memory used: 490.469 MB
% 5.31/5.63 % Net memory used: 462.019 MB
%------------------------------------------------------------------------------