%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW216+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:49 PM UTC 2026
% Result : Theorem 0.13s 5.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW216+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/5.36 % Computer : n010.cluster.edu
% 0.10/5.36 % Model : x86_64 x86_64
% 0.10/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36 % Memory : 8046.5625MB
% 0.10/5.36 % OS : Linux 6.8.0-71-generic
% 0.10/5.36 % CPULimit : 300
% 0.10/5.36 % WCLimit : 300
% 0.10/5.36 % DateTime : Mon Sep 21 09:42:34 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.13/5.47 % Drodi V4.1.1
% 0.13/5.61 % Refutation found
% 0.13/5.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.61 % SZS output start CNFRefutation for theBenchmark
% 0.13/5.61 fof(f2,axiom,(
% 0.13/5.61 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_m____) ),
% 0.13/5.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.61 fof(f3,axiom,(
% 0.13/5.61 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_da____,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e,v_m____)) ),
% 0.13/5.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.61 fof(f47,axiom,(
% 0.13/5.61 (! [V_b_2,V_a_2,V_ca_2,T_a] :( class_Fields_Olinordered__field(T_a)=> ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_ca_2)=> ( c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Rings_Oinverse__class_Odivide(T_a,V_b_2,V_ca_2))<=> c_Orderings_Oord__class_Oless(T_a,hAPP(c_Groups_Otimes__class_Otimes(T_a,V_a_2),V_ca_2),V_b_2) ) ) ) )),
% 0.13/5.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.61 fof(f1134,axiom,(
% 0.13/5.61 class_Fields_Olinordered__field(tc_RealDef_Oreal) ),
% 0.13/5.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.61 fof(f1250,conjecture,(
% 0.13/5.61 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,v_da____),v_m____),v_e) ),
% 0.13/5.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.61 fof(f1251,negated_conjecture,(
% 0.13/5.61 ~(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,v_da____),v_m____),v_e) )),
% 0.13/5.61 inference(negated_conjecture,[status(cth)],[f1250])).
% 0.13/5.61 fof(f1255,plain,(
% 0.13/5.61 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_m____)),
% 0.13/5.61 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/5.61 fof(f1256,plain,(
% 0.13/5.61 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_da____,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e,v_m____))),
% 0.13/5.61 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/5.61 fof(f1373,plain,(
% 0.13/5.61 ![V_b_2,V_a_2,V_ca_2,T_a]: (~class_Fields_Olinordered__field(T_a)|(~c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_ca_2)|(c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Rings_Oinverse__class_Odivide(T_a,V_b_2,V_ca_2))<=>c_Orderings_Oord__class_Oless(T_a,hAPP(c_Groups_Otimes__class_Otimes(T_a,V_a_2),V_ca_2),V_b_2))))),
% 0.13/5.61 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.13/5.61 fof(f1374,plain,(
% 0.13/5.61 ![V_b_2,V_a_2,V_ca_2,T_a]: (~class_Fields_Olinordered__field(T_a)|(~c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_ca_2)|((~c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Rings_Oinverse__class_Odivide(T_a,V_b_2,V_ca_2))|c_Orderings_Oord__class_Oless(T_a,hAPP(c_Groups_Otimes__class_Otimes(T_a,V_a_2),V_ca_2),V_b_2))&(c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Rings_Oinverse__class_Odivide(T_a,V_b_2,V_ca_2))|~c_Orderings_Oord__class_Oless(T_a,hAPP(c_Groups_Otimes__class_Otimes(T_a,V_a_2),V_ca_2),V_b_2)))))),
% 0.13/5.61 inference(NNF_transformation,[status(thm)],[f1373])).
% 0.13/5.61 fof(f1375,plain,(
% 0.13/5.61 ![T_a]: (~class_Fields_Olinordered__field(T_a)|(![V_ca_2]: (~c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_ca_2)|((![V_b_2,V_a_2]: (~c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Rings_Oinverse__class_Odivide(T_a,V_b_2,V_ca_2))|c_Orderings_Oord__class_Oless(T_a,hAPP(c_Groups_Otimes__class_Otimes(T_a,V_a_2),V_ca_2),V_b_2)))&(![V_b_2,V_a_2]: (c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Rings_Oinverse__class_Odivide(T_a,V_b_2,V_ca_2))|~c_Orderings_Oord__class_Oless(T_a,hAPP(c_Groups_Otimes__class_Otimes(T_a,V_a_2),V_ca_2),V_b_2)))))))),
% 0.13/5.61 inference(miniscoping,[status(thm)],[f1374])).
% 0.13/5.61 fof(f1376,plain,(
% 0.13/5.61 ![X0,X1,X2,X3]: (~class_Fields_Olinordered__field(X0)|~c_Orderings_Oord__class_Oless(X0,c_Groups_Ozero__class_Ozero(X0),X1)|~c_Orderings_Oord__class_Oless(X0,X2,c_Rings_Oinverse__class_Odivide(X0,X3,X1))|c_Orderings_Oord__class_Oless(X0,hAPP(c_Groups_Otimes__class_Otimes(X0,X2),X1),X3))),
% 0.13/5.61 inference(cnf_transformation,[status(thm)],[f1375])).
% 0.13/5.61 fof(f4652,plain,(
% 0.13/5.61 class_Fields_Olinordered__field(tc_RealDef_Oreal)),
% 0.13/5.61 inference(cnf_transformation,[status(thm)],[f1134])).
% 0.13/5.61 fof(f4768,plain,(
% 0.13/5.61 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,v_da____),v_m____),v_e)),
% 0.13/5.63 inference(cnf_transformation,[status(thm)],[f1251])).
% 0.13/5.63 fof(f6016,definition,(
% 0.13/5.63 sQ43_spl <=> (class_Fields_Olinordered__field(tc_RealDef_Oreal))),
% 0.13/5.63 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.13/5.63 fof(f6018,plain,(
% 0.13/5.63 ~class_Fields_Olinordered__field(tc_RealDef_Oreal)|sQ43_spl),
% 0.13/5.63 inference(component_clause,[status(thm)],[f6016])).
% 0.13/5.63 fof(f6095,plain,(
% 0.13/5.63 $false|sQ43_spl),
% 0.13/5.63 inference(forward_subsumption_resolution,[status(thm)],[f6018,f4652])).
% 0.13/5.63 fof(f6096,plain,(
% 0.13/5.63 sQ43_spl),
% 0.13/5.63 inference(contradiction_clause,[status(thm)],[f6095])).
% 0.13/5.63 fof(f6488,definition,(
% 0.13/5.63 sQ104_spl <=> (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_m____))),
% 0.13/5.63 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.13/5.63 fof(f6490,plain,(
% 0.13/5.63 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_m____)|sQ104_spl),
% 0.13/5.63 inference(component_clause,[status(thm)],[f6488])).
% 0.13/5.63 fof(f6525,plain,(
% 0.13/5.63 $false|sQ104_spl),
% 0.13/5.63 inference(forward_subsumption_resolution,[status(thm)],[f6490,f1255])).
% 0.13/5.63 fof(f6526,plain,(
% 0.13/5.63 sQ104_spl),
% 0.13/5.63 inference(contradiction_clause,[status(thm)],[f6525])).
% 0.13/5.63 fof(f6843,plain,(
% 0.13/5.63 ~class_Fields_Olinordered__field(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_m____)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,v_da____),v_m____),v_e)),
% 0.13/5.63 inference(resolution,[status(thm)],[f1376,f1256])).
% 0.13/5.63 fof(f6873,definition,(
% 0.13/5.63 sQ168_spl <=> (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,v_da____),v_m____),v_e))),
% 0.13/5.63 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 0.13/5.63 fof(f6874,plain,(
% 0.13/5.63 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,v_da____),v_m____),v_e)|~sQ168_spl),
% 0.13/5.63 inference(component_clause,[status(thm)],[f6873])).
% 0.13/5.63 fof(f6876,plain,(
% 0.13/5.63 ~sQ43_spl|~sQ104_spl|sQ168_spl),
% 0.13/5.63 inference(split_clause,[status(thm)],[f6843,f6016,f6488,f6873])).
% 0.13/5.63 fof(f6885,plain,(
% 0.13/5.63 $false|~sQ168_spl),
% 0.13/5.63 inference(forward_subsumption_resolution,[status(thm)],[f6874,f4768])).
% 0.13/5.63 fof(f6886,plain,(
% 0.13/5.63 ~sQ168_spl),
% 0.13/5.63 inference(contradiction_clause,[status(thm)],[f6885])).
% 0.13/5.63 fof(f6887,plain,(
% 0.13/5.63 $false),
% 0.13/5.63 inference(sat_refutation,[status(thm)],[f6096,f6526,f6876,f6886])).
% 0.13/5.63 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.64 % Elapsed time: 0.264364 seconds
% 0.13/5.64 % CPU time: 1.242368 seconds
% 0.13/5.64 % Total memory used: 220.558 MB
% 0.13/5.64 % Net memory used: 218.664 MB
%------------------------------------------------------------------------------