%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW194+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 : n017.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:47 PM UTC 2026
% Result : Theorem 32.22s 4.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW194+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.11/0.36 % Computer : n017.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 09:36:14 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.41 % Drodi V4.1.1
% 32.22/4.61 % Refutation found
% 32.22/4.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 32.22/4.61 % SZS output start CNFRefutation for theBenchmark
% 32.22/4.61 fof(f2,axiom,(
% 32.22/4.61 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f21,axiom,(
% 32.22/4.61 c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit1(c_Int_OPls)) = c_Groups_Oone__class_Oone(tc_Nat_Onat) ),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f32,axiom,(
% 32.22/4.61 (! [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 ) ) )),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f34,axiom,(
% 32.22/4.61 (! [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) ) )),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f35,axiom,(
% 32.22/4.61 (! [V_w] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_w) )),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f224,axiom,(
% 32.22/4.61 (! [V_b,V_n,V_a,T_a] :( class_Rings_Olinordered__semidom(T_a)=> ( c_Orderings_Oord__class_Oless__eq(T_a,hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a),c_Nat_OSuc(V_n)),hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_b),c_Nat_OSuc(V_n)))=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_b)=> c_Orderings_Oord__class_Oless__eq(T_a,V_a,V_b) ) ) ) )),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f266,axiom,(
% 32.22/4.61 (! [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)) ) )),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f272,axiom,(
% 32.22/4.61 c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit1(c_Int_OPls)) = c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) ),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f288,axiom,(
% 32.22/4.61 c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))) = c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) ),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f1103,axiom,(
% 32.22/4.61 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f1120,axiom,(
% 32.22/4.61 class_Rings_Olinordered__semidom(tc_RealDef_Oreal) ),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f1199,conjecture,(
% 32.22/4.61 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ),
% 32.22/4.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.22/4.61 fof(f1200,negated_conjecture,(
% 32.22/4.61 ~(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) )),
% 32.22/4.61 inference(negated_conjecture,[status(cth)],[f1199])).
% 32.22/4.62 fof(f1204,plain,(
% 32.22/4.62 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f2])).
% 32.22/4.62 fof(f1242,plain,(
% 32.22/4.62 c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit1(c_Int_OPls))=c_Groups_Oone__class_Oone(tc_Nat_Onat)),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f21])).
% 32.22/4.62 fof(f1271,plain,(
% 32.22/4.62 ![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))),
% 32.22/4.62 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 32.22/4.62 fof(f1272,plain,(
% 32.22/4.62 ![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)),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f1271])).
% 32.22/4.62 fof(f1276,plain,(
% 32.22/4.62 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f34])).
% 32.22/4.62 fof(f1277,plain,(
% 32.22/4.62 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X0))),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f35])).
% 32.22/4.62 fof(f1778,plain,(
% 32.22/4.62 ![V_b,V_n,V_a,T_a]: (~class_Rings_Olinordered__semidom(T_a)|(~c_Orderings_Oord__class_Oless__eq(T_a,hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a),c_Nat_OSuc(V_n)),hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_b),c_Nat_OSuc(V_n)))|(~c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_b)|c_Orderings_Oord__class_Oless__eq(T_a,V_a,V_b))))),
% 32.22/4.62 inference(pre_NNF_transformation,[status(thm)],[f224])).
% 32.22/4.62 fof(f1779,plain,(
% 32.22/4.62 ![T_a]: (~class_Rings_Olinordered__semidom(T_a)|(![V_b,V_a]: ((![V_n]: ~c_Orderings_Oord__class_Oless__eq(T_a,hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a),c_Nat_OSuc(V_n)),hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_b),c_Nat_OSuc(V_n))))|(~c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_b)|c_Orderings_Oord__class_Oless__eq(T_a,V_a,V_b)))))),
% 32.22/4.62 inference(miniscoping,[status(thm)],[f1778])).
% 32.22/4.62 fof(f1780,plain,(
% 32.22/4.62 ![X0,X1,X2,X3]: (~class_Rings_Olinordered__semidom(X0)|~c_Orderings_Oord__class_Oless__eq(X0,hAPP(hAPP(c_Power_Opower__class_Opower(X0),X1),c_Nat_OSuc(X2)),hAPP(hAPP(c_Power_Opower__class_Opower(X0),X3),c_Nat_OSuc(X2)))|~c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0),X3)|c_Orderings_Oord__class_Oless__eq(X0,X1,X3))),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f1779])).
% 32.22/4.62 fof(f1896,plain,(
% 32.22/4.62 ![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)))),
% 32.22/4.62 inference(pre_NNF_transformation,[status(thm)],[f266])).
% 32.22/4.62 fof(f1897,plain,(
% 32.22/4.62 ![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))))),
% 32.22/4.62 inference(miniscoping,[status(thm)],[f1896])).
% 32.22/4.62 fof(f1898,plain,(
% 32.22/4.62 ![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)))),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f1897])).
% 32.22/4.62 fof(f1906,plain,(
% 32.22/4.62 c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit1(c_Int_OPls))=c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f272])).
% 32.22/4.62 fof(f1949,plain,(
% 32.22/4.62 c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))=c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f288])).
% 32.22/4.62 fof(f4371,plain,(
% 32.22/4.62 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f1103])).
% 32.22/4.62 fof(f4388,plain,(
% 32.22/4.62 class_Rings_Olinordered__semidom(tc_RealDef_Oreal)),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f1120])).
% 32.22/4.62 fof(f4467,plain,(
% 32.22/4.62 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 32.22/4.62 inference(cnf_transformation,[status(thm)],[f1200])).
% 32.22/4.62 fof(f4651,plain,(
% 32.22/4.62 c_Groups_Oone__class_Oone(tc_Nat_Onat)=c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 32.22/4.62 inference(forward_demodulation,[status(thm)],[f1242,f1906])).
% 32.22/4.62 fof(f4675,plain,(
% 32.22/4.62 c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))=c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),
% 32.22/4.62 inference(forward_demodulation,[status(thm)],[f4651,f1949])).
% 32.22/4.62 fof(f5004,plain,(
% 32.22/4.62 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____))),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 32.22/4.62 inference(forward_demodulation,[status(thm)],[f4675,f4467])).
% 32.22/4.62 fof(f5005,plain,(
% 32.22/4.62 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____))),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))),
% 32.22/4.62 inference(forward_demodulation,[status(thm)],[f4675,f5004])).
% 32.22/4.62 fof(f5050,plain,(
% 32.22/4.62 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____)))|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 32.22/4.62 inference(resolution,[status(thm)],[f1272,f1204])).
% 32.22/4.62 fof(f5088,definition,(
% 32.22/4.62 sQ8_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____))))),
% 32.22/4.62 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 32.22/4.62 fof(f5091,definition,(
% 32.22/4.62 sQ9_spl <=> (c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 32.22/4.62 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 32.22/4.62 fof(f5092,plain,(
% 32.22/4.62 c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)|~sQ9_spl),
% 32.22/4.62 inference(component_clause,[status(thm)],[f5091])).
% 32.22/4.62 fof(f5094,plain,(
% 32.22/4.62 ~sQ8_spl|sQ9_spl),
% 32.22/4.62 inference(split_clause,[status(thm)],[f5050,f5088,f5091])).
% 32.96/4.71 fof(f5128,plain,(
% 32.96/4.71 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____))),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))),
% 32.96/4.71 inference(resolution,[status(thm)],[f1276,f5005])).
% 32.96/4.71 fof(f5459,definition,(
% 32.96/4.71 sQ51_spl <=> (class_Rings_Olinordered__semidom(tc_RealDef_Oreal))),
% 32.96/4.71 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 32.96/4.71 fof(f5461,plain,(
% 32.96/4.71 ~class_Rings_Olinordered__semidom(tc_RealDef_Oreal)|sQ51_spl),
% 32.96/4.71 inference(component_clause,[status(thm)],[f5459])).
% 32.96/4.71 fof(f5492,plain,(
% 32.96/4.71 $false|sQ51_spl),
% 32.96/4.71 inference(forward_subsumption_resolution,[status(thm)],[f5461,f4388])).
% 32.96/4.71 fof(f5493,plain,(
% 32.96/4.71 sQ51_spl),
% 32.96/4.71 inference(contradiction_clause,[status(thm)],[f5492])).
% 32.96/4.71 fof(f10288,plain,(
% 32.96/4.71 ~class_Rings_Olinordered__semidom(tc_RealDef_Oreal)|~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,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____)))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____)))),
% 32.96/4.71 inference(resolution,[status(thm)],[f1780,f5128])).
% 32.96/4.71 fof(f10305,definition,(
% 32.96/4.71 sQ328_spl <=> (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,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____))))),
% 32.96/4.71 introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition])).
% 32.96/4.71 fof(f10307,plain,(
% 32.96/4.71 ~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,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),v_x____)))|sQ328_spl),
% 32.96/4.71 inference(component_clause,[status(thm)],[f10305])).
% 32.96/4.71 fof(f10308,plain,(
% 32.96/4.71 ~sQ51_spl|~sQ328_spl|sQ8_spl),
% 32.96/4.71 inference(split_clause,[status(thm)],[f10288,f5459,f10305,f5088])).
% 32.96/4.71 fof(f11355,plain,(
% 32.96/4.71 ![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)))),
% 32.96/4.71 inference(resolution,[status(thm)],[f1898,f4371])).
% 32.96/4.71 fof(f11358,plain,(
% 32.96/4.71 $false|sQ328_spl),
% 32.96/4.71 inference(backward_subsumption_resolution,[status(thm)],[f10307,f11355])).
% 32.96/4.71 fof(f11361,plain,(
% 32.96/4.71 sQ328_spl),
% 32.96/4.71 inference(contradiction_clause,[status(thm)],[f11358])).
% 32.96/4.71 fof(f11365,plain,(
% 32.96/4.71 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))|~sQ9_spl),
% 32.96/4.71 inference(backward_demodulation,[status(thm)],[f5092,f5005])).
% 32.96/4.71 fof(f11405,plain,(
% 32.96/4.71 $false|~sQ9_spl),
% 32.96/4.71 inference(forward_subsumption_resolution,[status(thm)],[f11365,f1277])).
% 32.96/4.71 fof(f11406,plain,(
% 32.96/4.71 ~sQ9_spl),
% 32.96/4.71 inference(contradiction_clause,[status(thm)],[f11405])).
% 32.96/4.71 fof(f11407,plain,(
% 32.96/4.71 $false),
% 32.96/4.71 inference(sat_refutation,[status(thm)],[f5094,f5493,f10308,f11361,f11406])).
% 32.96/4.71 % SZS output end CNFRefutation for theBenchmark.p
% 32.96/4.73 % Elapsed time: 4.351926 seconds
% 32.96/4.73 % CPU time: 33.633687 seconds
% 32.96/4.73 % Total memory used: 440.391 MB
% 32.96/4.73 % Net memory used: 429.611 MB
%------------------------------------------------------------------------------