%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW234+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 : n003.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 29.31s 4.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW234+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n003.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 09:44:31 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 29.31/4.47 % Refutation found
% 29.31/4.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 29.31/4.47 % SZS output start CNFRefutation for theBenchmark
% 29.31/4.47 fof(f6,axiom,(
% 29.31/4.47 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____)) ),
% 29.31/4.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.31/4.47 fof(f9,axiom,(
% 29.31/4.47 (! [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) ) ) )),
% 29.31/4.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.31/4.47 fof(f18,axiom,(
% 29.31/4.47 (! [V_r] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,V_r) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) )),
% 29.31/4.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.31/4.47 fof(f28,axiom,(
% 29.31/4.47 (! [V_a,T_a] :( class_Groups_Ocomm__monoid__add(T_a)=> c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a ) )),
% 29.31/4.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.31/4.47 fof(f55,axiom,(
% 29.31/4.47 (! [V_z,V_y,V_x] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x,V_y)=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_x),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_y)) ) )),
% 29.31/4.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.31/4.47 fof(f185,axiom,(
% 29.31/4.47 (! [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)) ) )),
% 29.31/4.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.31/4.47 fof(f1127,axiom,(
% 29.31/4.47 class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal) ),
% 29.31/4.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.31/4.47 fof(f1142,axiom,(
% 29.31/4.47 class_Groups_Ocomm__monoid__add(tc_RealDef_Oreal) ),
% 29.31/4.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.31/4.47 fof(f1274,conjecture,(
% 29.31/4.47 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)) ),
% 29.31/4.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.31/4.47 fof(f1275,negated_conjecture,(
% 29.31/4.47 ~(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)) )),
% 29.31/4.47 inference(negated_conjecture,[status(cth)],[f1274])).
% 29.31/4.47 fof(f1286,plain,(
% 29.31/4.47 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____))),
% 29.31/4.47 inference(cnf_transformation,[status(thm)],[f6])).
% 29.31/4.47 fof(f1289,plain,(
% 29.31/4.47 ![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)))),
% 29.31/4.47 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 29.31/4.47 fof(f1290,plain,(
% 29.31/4.47 ![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))))),
% 29.31/4.47 inference(miniscoping,[status(thm)],[f1289])).
% 29.31/4.47 fof(f1291,plain,(
% 29.31/4.47 ![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))),
% 29.31/4.47 inference(cnf_transformation,[status(thm)],[f1290])).
% 29.31/4.47 fof(f1316,plain,(
% 29.31/4.47 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 29.31/4.47 inference(cnf_transformation,[status(thm)],[f18])).
% 29.31/4.47 fof(f1350,plain,(
% 29.31/4.47 ![V_a,T_a]: (~class_Groups_Ocomm__monoid__add(T_a)|c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a)),
% 29.31/4.47 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 29.31/4.47 fof(f1351,plain,(
% 29.31/4.47 ![T_a]: (~class_Groups_Ocomm__monoid__add(T_a)|(![V_a]: c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a))),
% 29.31/4.47 inference(miniscoping,[status(thm)],[f1350])).
% 29.31/4.47 fof(f1352,plain,(
% 29.31/4.47 ![X0,X1]: (~class_Groups_Ocomm__monoid__add(X0)|c_Groups_Oplus__class_Oplus(X0,X1,c_Groups_Ozero__class_Ozero(X0))=X1)),
% 29.31/4.47 inference(cnf_transformation,[status(thm)],[f1351])).
% 29.31/4.47 fof(f1450,plain,(
% 29.31/4.47 ![V_z,V_y,V_x]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x,V_y)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_x),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_y)))),
% 29.31/4.47 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 29.31/4.47 fof(f1451,plain,(
% 29.31/4.47 ![V_y,V_x]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x,V_y)|(![V_z]: c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_x),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_y))))),
% 29.31/4.47 inference(miniscoping,[status(thm)],[f1450])).
% 29.31/4.47 fof(f1452,plain,(
% 29.31/4.47 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X0),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X1)))),
% 29.31/4.47 inference(cnf_transformation,[status(thm)],[f1451])).
% 29.31/4.47 fof(f1902,plain,(
% 29.31/4.47 ![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)))),
% 29.31/4.47 inference(pre_NNF_transformation,[status(thm)],[f185])).
% 29.31/4.47 fof(f1903,plain,(
% 29.31/4.47 ![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))))),
% 29.31/4.47 inference(miniscoping,[status(thm)],[f1902])).
% 29.31/4.47 fof(f1904,plain,(
% 29.31/4.47 ![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)))),
% 29.31/4.47 inference(cnf_transformation,[status(thm)],[f1903])).
% 29.31/4.47 fof(f4575,plain,(
% 29.31/4.47 class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal)),
% 29.31/4.47 inference(cnf_transformation,[status(thm)],[f1127])).
% 29.31/4.47 fof(f4590,plain,(
% 29.31/4.47 class_Groups_Ocomm__monoid__add(tc_RealDef_Oreal)),
% 29.31/4.47 inference(cnf_transformation,[status(thm)],[f1142])).
% 29.31/4.47 fof(f4782,plain,(
% 29.31/4.47 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____))),
% 29.31/4.47 inference(cnf_transformation,[status(thm)],[f1275])).
% 29.31/4.47 fof(f4949,plain,(
% 29.31/4.47 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)))),
% 29.31/4.47 inference(resolution,[status(thm)],[f1291,f4782])).
% 29.31/4.47 fof(f4992,plain,(
% 29.31/4.47 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(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____)))),
% 29.31/4.47 inference(resolution,[status(thm)],[f1286,f4949])).
% 29.31/4.47 fof(f6060,plain,(
% 29.31/4.47 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=X0)),
% 29.31/4.47 inference(resolution,[status(thm)],[f4590,f1352])).
% 29.31/4.47 fof(f30482,plain,(
% 29.31/4.47 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)))),
% 29.31/4.47 inference(resolution,[status(thm)],[f1904,f4575])).
% 29.31/4.47 fof(f30483,plain,(
% 29.31/4.47 ![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)))),
% 29.31/4.47 inference(forward_demodulation,[status(thm)],[f1316,f30482])).
% 29.31/4.47 fof(f30605,plain,(
% 29.31/4.47 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1))))),
% 29.31/4.52 inference(resolution,[status(thm)],[f30483,f1452])).
% 29.31/4.52 fof(f30648,plain,(
% 29.31/4.52 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1))))),
% 29.31/4.52 inference(forward_demodulation,[status(thm)],[f6060,f30605])).
% 29.31/4.52 fof(f30677,plain,(
% 29.31/4.52 $false),
% 29.31/4.52 inference(backward_subsumption_resolution,[status(thm)],[f4992,f30648])).
% 29.31/4.52 % SZS output end CNFRefutation for theBenchmark.p
% 19.41/4.56 % Elapsed time: 4.200012 seconds
% 19.41/4.56 % CPU time: 32.589552 seconds
% 19.41/4.56 % Total memory used: 372.610 MB
% 19.41/4.56 % Net memory used: 356.586 MB
%------------------------------------------------------------------------------