%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW215+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 : 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:49 PM UTC 2026
% Result : Theorem 1.30s 0.68s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW215+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.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 09:41:42 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.21/0.46 % Drodi V4.1.1
% 1.30/0.68 % Refutation found
% 1.30/0.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.30/0.68 % SZS output start CNFRefutation for theBenchmark
% 1.30/0.68 fof(f3,axiom,(
% 1.30/0.68 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_da____,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
% 1.30/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.68 fof(f4,axiom,(
% 1.30/0.68 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),v_da____) ),
% 1.30/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.68 fof(f11,axiom,(
% 1.30/0.68 (! [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) ) )),
% 1.30/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.68 fof(f12,axiom,(
% 1.30/0.68 (! [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) ) ) )),
% 1.30/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.68 fof(f55,axiom,(
% 1.30/0.68 (! [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) ) ) ) )),
% 1.30/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.68 fof(f61,axiom,(
% 1.30/0.68 (! [V_y_2,V_x_2] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)<=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)| V_x_2 = V_y_2 ) ) )),
% 1.30/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.68 fof(f1155,axiom,(
% 1.30/0.68 class_Orderings_Opreorder(tc_RealDef_Oreal) ),
% 1.30/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.68 fof(f1278,conjecture,(
% 1.30/0.68 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
% 1.30/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.68 fof(f1279,negated_conjecture,(
% 1.30/0.68 ~(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) )),
% 1.30/0.68 inference(negated_conjecture,[status(cth)],[f1278])).
% 1.30/0.68 fof(f1284,plain,(
% 1.30/0.68 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_da____,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 1.30/0.68 inference(cnf_transformation,[status(thm)],[f3])).
% 1.30/0.68 fof(f1285,plain,(
% 1.30/0.68 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),v_da____)),
% 1.30/0.68 inference(cnf_transformation,[status(thm)],[f4])).
% 1.30/0.68 fof(f1303,plain,(
% 1.30/0.68 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 1.30/0.68 inference(cnf_transformation,[status(thm)],[f11])).
% 1.30/0.68 fof(f1304,plain,(
% 1.30/0.68 ![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)))),
% 1.30/0.68 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 1.30/0.68 fof(f1305,plain,(
% 1.30/0.68 ![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))))),
% 1.30/0.68 inference(miniscoping,[status(thm)],[f1304])).
% 1.30/0.68 fof(f1306,plain,(
% 1.30/0.68 ![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))),
% 1.30/0.68 inference(cnf_transformation,[status(thm)],[f1305])).
% 1.30/0.68 fof(f1445,plain,(
% 1.30/0.68 ![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))))),
% 1.30/0.68 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 1.30/0.68 fof(f1446,plain,(
% 1.30/0.68 ![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)))))),
% 1.30/0.68 inference(NNF_transformation,[status(thm)],[f1445])).
% 1.30/0.68 fof(f1447,plain,(
% 1.30/0.68 ![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))))))),
% 1.30/0.68 inference(miniscoping,[status(thm)],[f1446])).
% 1.30/0.68 fof(f1449,plain,(
% 1.30/0.68 ![X0,X1,X2]: (~class_Orderings_Opreorder(X0)|~c_Orderings_Oord__class_Oless(X0,X1,X2)|~c_Orderings_Oord__class_Oless__eq(X0,X2,X1))),
% 1.30/0.68 inference(cnf_transformation,[status(thm)],[f1447])).
% 1.30/0.68 fof(f1475,plain,(
% 1.30/0.68 ![V_y_2,V_x_2]: ((~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|V_x_2=V_y_2))&(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)&~V_x_2=V_y_2)))),
% 1.30/0.68 inference(NNF_transformation,[status(thm)],[f61])).
% 1.30/0.68 fof(f1476,plain,(
% 1.30/0.68 (![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless(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__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)&~V_x_2=V_y_2)))),
% 1.30/0.68 inference(miniscoping,[status(thm)],[f1475])).
% 1.30/0.68 fof(f1478,plain,(
% 1.30/0.68 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1))),
% 1.30/0.68 inference(cnf_transformation,[status(thm)],[f1476])).
% 1.30/0.68 fof(f4713,plain,(
% 1.30/0.68 class_Orderings_Opreorder(tc_RealDef_Oreal)),
% 1.30/0.68 inference(cnf_transformation,[status(thm)],[f1155])).
% 1.30/0.68 fof(f4895,plain,(
% 1.30/0.68 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 1.30/0.68 inference(cnf_transformation,[status(thm)],[f1279])).
% 1.30/0.68 fof(f5139,plain,(
% 1.30/0.68 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
% 1.30/0.68 inference(resolution,[status(thm)],[f1306,f4895])).
% 1.30/0.68 fof(f5141,plain,(
% 1.30/0.68 ![X0,X1]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),X1)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 1.30/0.68 inference(resolution,[status(thm)],[f5139,f1306])).
% 1.30/0.68 fof(f5147,plain,(
% 1.30/0.68 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),X2)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1))),
% 1.30/0.68 inference(resolution,[status(thm)],[f5141,f1306])).
% 1.30/0.68 fof(f5191,plain,(
% 1.30/0.68 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 1.30/0.68 inference(resolution,[status(thm)],[f1478,f1284])).
% 1.30/0.68 fof(f5194,plain,(
% 1.30/0.68 ![X0,X1]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,v_da____)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),X1)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 1.30/0.70 inference(resolution,[status(thm)],[f5191,f5147])).
% 1.30/0.70 fof(f5209,plain,(
% 1.30/0.70 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,v_da____))),
% 1.30/0.70 inference(resolution,[status(thm)],[f5194,f1303])).
% 1.30/0.70 fof(f5216,plain,(
% 1.30/0.70 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),X0)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,X0))),
% 1.30/0.70 inference(resolution,[status(thm)],[f5209,f1303])).
% 1.30/0.70 fof(f5393,plain,(
% 1.30/0.70 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,X0)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))))),
% 1.30/0.70 inference(resolution,[status(thm)],[f5216,f1303])).
% 1.30/0.70 fof(f5397,definition,(
% 1.30/0.70 sQ17_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))))),
% 1.30/0.70 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 1.30/0.70 fof(f5402,plain,(
% 1.30/0.70 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))),
% 1.30/0.70 inference(resolution,[status(thm)],[f5393,f5216])).
% 1.30/0.70 fof(f5406,plain,(
% 1.30/0.70 sQ17_spl),
% 1.30/0.70 inference(split_clause,[status(thm)],[f5402,f5397])).
% 1.30/0.70 fof(f6243,plain,(
% 1.30/0.70 ~class_Orderings_Opreorder(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))),
% 1.30/0.70 inference(resolution,[status(thm)],[f1449,f1285])).
% 1.30/0.70 fof(f6252,definition,(
% 1.30/0.70 sQ51_spl <=> (class_Orderings_Opreorder(tc_RealDef_Oreal))),
% 1.30/0.70 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 1.30/0.70 fof(f6254,plain,(
% 1.30/0.70 ~class_Orderings_Opreorder(tc_RealDef_Oreal)|sQ51_spl),
% 1.30/0.70 inference(component_clause,[status(thm)],[f6252])).
% 1.30/0.70 fof(f6255,plain,(
% 1.30/0.70 ~sQ51_spl|~sQ17_spl),
% 1.30/0.70 inference(split_clause,[status(thm)],[f6243,f6252,f5397])).
% 1.30/0.70 fof(f6260,plain,(
% 1.30/0.70 $false|sQ51_spl),
% 1.30/0.70 inference(forward_subsumption_resolution,[status(thm)],[f6254,f4713])).
% 1.30/0.70 fof(f6261,plain,(
% 1.30/0.70 sQ51_spl),
% 1.30/0.70 inference(contradiction_clause,[status(thm)],[f6260])).
% 1.30/0.70 fof(f6262,plain,(
% 1.30/0.70 $false),
% 1.30/0.70 inference(sat_refutation,[status(thm)],[f5406,f6255,f6261])).
% 1.30/0.70 % SZS output end CNFRefutation for theBenchmark.p
% 1.30/0.70 % Elapsed time: 0.335038 seconds
% 1.30/0.70 % CPU time: 1.693762 seconds
% 1.30/0.70 % Total memory used: 224.939 MB
% 1.30/0.70 % Net memory used: 222.577 MB
%------------------------------------------------------------------------------