%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW210+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 : n001.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:48 PM UTC 2026
% Result : Theorem 37.35s 10.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW210+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/5.44 % Computer : n001.cluster.edu
% 0.17/5.44 % Model : x86_64 x86_64
% 0.17/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.44 % Memory : 8046.5625MB
% 0.17/5.44 % OS : Linux 6.8.0-71-generic
% 0.17/5.44 % CPULimit : 300
% 0.17/5.44 % WCLimit : 300
% 0.17/5.44 % DateTime : Mon Sep 21 09:46:50 UTC 2026
% 0.17/5.45 % CPUTime :
% 0.22/5.59 % Drodi V4.1.1
% 37.35/10.35 % Refutation found
% 37.35/10.35 % SZS status Theorem for theBenchmark: Theorem is valid
% 37.35/10.35 % SZS output start CNFRefutation for theBenchmark
% 37.35/10.35 fof(f5,axiom,(
% 37.35/10.35 (? [B_n0] :(! [B_n] :( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_n0,B_n)=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,B_n))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ) ))),
% 37.35/10.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.35/10.35 fof(f7,axiom,(
% 37.35/10.35 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ),
% 37.35/10.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.35/10.35 fof(f10,axiom,(
% 37.35/10.35 (! [B_r] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_r)=> (? [B_n0] :(! [B_n] :( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_n0,B_n)=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,B_n)))),v_y____)),B_r) ) ))) )),
% 37.35/10.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.35/10.35 fof(f259,axiom,(
% 37.35/10.35 (! [V_k,V_j,V_i] :( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_i,V_j)=> ( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_j,V_k)=> c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_i,V_k) ) ) )),
% 37.35/10.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.35/10.35 fof(f928,axiom,(
% 37.35/10.35 (! [V_m] : c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m,c_Groups_Otimes__class_Otimes(tc_Nat_Onat,V_m,V_m)) )),
% 37.35/10.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.35/10.35 fof(f1201,hypothesis,(
% 37.35/10.35 ( (? [B_N1] :(! [B_n] :( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N1,B_n)=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,B_n))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) )))=> ( (? [B_N2] :(! [B_n] :( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N2,B_n)=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,B_n)))),v_y____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) )))=> v_thesis____ ) ) ),
% 37.35/10.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.35/10.35 fof(f1202,conjecture,(
% 37.35/10.35 v_thesis____ ),
% 37.35/10.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.35/10.35 fof(f1203,negated_conjecture,(
% 37.35/10.35 ~(v_thesis____ )),
% 37.35/10.35 inference(negated_conjecture,[status(cth)],[f1202])).
% 37.35/10.35 fof(f1210,plain,(
% 37.35/10.35 ?[B_n0]: (![B_n]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_n0,B_n)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,B_n))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))),
% 37.35/10.35 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 37.35/10.35 fof(f1211,plain,(
% 37.35/10.35 ![B_n]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK1_skl,B_n)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,B_n))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))),
% 37.35/10.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B_n0,sK1_skl)],[f1210])).
% 37.35/10.35 fof(f1212,plain,(
% 37.35/10.35 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK1_skl,X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,X0))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))),
% 37.35/10.35 inference(cnf_transformation,[status(thm)],[f1211])).
% 37.35/10.35 fof(f1216,plain,(
% 37.35/10.35 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 37.35/10.35 inference(cnf_transformation,[status(thm)],[f7])).
% 37.35/10.35 fof(f1223,plain,(
% 37.35/10.35 ![B_r]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_r)|(?[B_n0]: ![B_n]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_n0,B_n)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,B_n)))),v_y____)),B_r))))),
% 37.35/10.35 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 37.35/10.35 fof(f1224,plain,(
% 37.35/10.35 ![B_r]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_r)|![B_n]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK3_skl(B_r),B_n)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,B_n)))),v_y____)),B_r)))),
% 37.35/10.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(B_n0,sK3_skl(B_r))],[f1223])).
% 37.35/10.35 fof(f1225,plain,(
% 37.35/10.35 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK3_skl(X0),X1)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,X1)))),v_y____)),X0))),
% 37.35/10.35 inference(cnf_transformation,[status(thm)],[f1224])).
% 37.35/10.35 fof(f2028,plain,(
% 37.35/10.35 ![V_k,V_j,V_i]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_i,V_j)|(~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_j,V_k)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_i,V_k)))),
% 37.35/10.35 inference(pre_NNF_transformation,[status(thm)],[f259])).
% 37.35/10.35 fof(f2029,plain,(
% 37.35/10.35 ![V_j,V_i]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_i,V_j)|(![V_k]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_j,V_k)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_i,V_k))))),
% 37.35/10.35 inference(miniscoping,[status(thm)],[f2028])).
% 37.35/10.35 fof(f2030,plain,(
% 37.35/10.35 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,X1)|~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,X2)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,X2))),
% 37.35/10.35 inference(cnf_transformation,[status(thm)],[f2029])).
% 37.35/10.35 fof(f4211,plain,(
% 37.35/10.35 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,c_Groups_Otimes__class_Otimes(tc_Nat_Onat,X0,X0)))),
% 37.35/10.35 inference(cnf_transformation,[status(thm)],[f928])).
% 37.35/10.35 fof(f4614,plain,(
% 37.35/10.35 (![B_N1]: ?[B_n]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N1,B_n)&~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,B_n))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))|((![B_N2]: ?[B_n]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N2,B_n)&~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,B_n)))),v_y____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))|v_thesis____)),
% 37.35/10.35 inference(pre_NNF_transformation,[status(thm)],[f1201])).
% 37.35/10.35 fof(f4615,definition,(
% 37.35/10.35 ![B_N1,B_n]: (sP15_prd(B_n,B_N1)<=>(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N1,B_n)&~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,B_n))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))),
% 37.35/10.35 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 37.35/10.35 fof(f4616,plain,(
% 37.35/10.35 (![B_N1]: ?[B_n]: sP15_prd(B_n,B_N1))|((![B_N2]: ?[B_n]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N2,B_n)&~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,B_n)))),v_y____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))|v_thesis____)),
% 37.35/10.35 inference(formula_renaming,[status(thm)],[f4614,f4615])).
% 37.35/10.35 fof(f4617,plain,(
% 37.35/10.35 (![B_N1]: sP15_prd(sK15_skl(B_N1),B_N1))|((![B_N2]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N2,sK16_skl(B_N2))&~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,sK16_skl(B_N2))))),v_y____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))|v_thesis____)),
% 37.35/10.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(B_n,sK15_skl(B_N1)),skolemize(B_n,sK16_skl(B_N2))],[f4616])).
% 37.35/10.35 fof(f4618,plain,(
% 37.35/10.35 ![X0,X1]: (sP15_prd(sK15_skl(X0),X0)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,sK16_skl(X1))|v_thesis____)),
% 37.35/10.35 inference(cnf_transformation,[status(thm)],[f4617])).
% 37.35/10.35 fof(f4619,plain,(
% 37.35/10.35 ![X0,X1]: (sP15_prd(sK15_skl(X0),X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,sK16_skl(X1))))),v_y____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))|v_thesis____)),
% 37.35/10.35 inference(cnf_transformation,[status(thm)],[f4617])).
% 37.35/10.35 fof(f4620,plain,(
% 37.35/10.35 ~v_thesis____),
% 37.35/10.35 inference(cnf_transformation,[status(thm)],[f1203])).
% 37.35/10.35 fof(f4732,plain,(
% 37.35/10.35 ![B_N1,B_n]: ((~sP15_prd(B_n,B_N1)|(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N1,B_n)&~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,B_n))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))&(sP15_prd(B_n,B_N1)|(~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N1,B_n)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,B_n))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))))),
% 37.35/10.35 inference(NNF_transformation,[status(thm)],[f4615])).
% 37.35/10.35 fof(f4733,plain,(
% 37.35/10.35 (![B_N1,B_n]: (~sP15_prd(B_n,B_N1)|(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N1,B_n)&~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,B_n))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))))&(![B_N1,B_n]: (sP15_prd(B_n,B_N1)|(~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N1,B_n)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,B_n))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))))),
% 12.24/10.43 inference(miniscoping,[status(thm)],[f4732])).
% 12.24/10.43 fof(f4734,plain,(
% 12.24/10.43 ![X0,X1]: (~sP15_prd(X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,X0))),
% 12.24/10.43 inference(cnf_transformation,[status(thm)],[f4733])).
% 12.24/10.43 fof(f4735,plain,(
% 12.24/10.43 ![X0,X1]: (~sP15_prd(X0,X1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,X0))),v_x____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))),
% 12.24/10.43 inference(cnf_transformation,[status(thm)],[f4733])).
% 12.24/10.43 fof(f14027,plain,(
% 12.24/10.43 ![X0,X1]: (sP15_prd(sK15_skl(X0),X0)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,sK16_skl(X1)))),
% 12.24/10.43 inference(forward_subsumption_resolution,[status(thm)],[f4618,f4620])).
% 12.24/10.43 fof(f14034,plain,(
% 12.24/10.43 ![X0,X1]: (sP15_prd(sK15_skl(X0),X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X1)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,sK16_skl(sK3_skl(X1)))))),v_y____)),X1))),
% 12.24/10.43 inference(resolution,[status(thm)],[f14027,f1225])).
% 12.24/10.43 fof(f14358,plain,(
% 12.24/10.43 ![X0,X1]: (sP15_prd(sK15_skl(X0),X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,sK16_skl(X1))))),v_y____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))),
% 12.24/10.43 inference(forward_subsumption_resolution,[status(thm)],[f4619,f4620])).
% 12.24/10.43 fof(f14390,plain,(
% 12.24/10.43 ![X0]: (sP15_prd(sK15_skl(X0),X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,sK16_skl(sK3_skl(c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))))),v_y____)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))),
% 12.24/10.43 inference(resolution,[status(thm)],[f14034,f1216])).
% 12.24/10.43 fof(f14393,plain,(
% 12.24/10.43 ![X0]: (sP15_prd(sK15_skl(X0),X0))),
% 12.24/10.43 inference(forward_subsumption_resolution,[status(thm)],[f14390,f14358])).
% 12.24/10.43 fof(f14396,plain,(
% 12.24/10.43 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,sK15_skl(X0)))),
% 12.24/10.43 inference(resolution,[status(thm)],[f14393,f4734])).
% 12.24/10.43 fof(f14421,plain,(
% 12.24/10.43 ![X0,X1]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,sK15_skl(X1)))),
% 12.24/10.43 inference(resolution,[status(thm)],[f14396,f2030])).
% 12.24/10.43 fof(f17468,plain,(
% 12.24/10.43 ![X0,X1]: (~sP15_prd(X0,X1)|~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK1_skl,X0))),
% 12.24/10.43 inference(resolution,[status(thm)],[f4735,f1212])).
% 12.24/10.43 fof(f17587,plain,(
% 12.24/10.43 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,sK15_skl(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,X0,X0))))),
% 12.24/10.43 inference(resolution,[status(thm)],[f14421,f4211])).
% 12.24/10.43 fof(f19770,plain,(
% 12.24/10.43 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK1_skl,sK15_skl(X0)))),
% 12.24/10.43 inference(resolution,[status(thm)],[f17468,f14393])).
% 12.24/10.43 fof(f19771,plain,(
% 12.24/10.43 $false),
% 12.24/10.43 inference(resolution,[status(thm)],[f19770,f17587])).
% 12.24/10.43 % SZS output end CNFRefutation for theBenchmark.p
% 12.24/10.45 % Elapsed time: 4.986063 seconds
% 12.24/10.45 % CPU time: 38.126693 seconds
% 12.24/10.45 % Total memory used: 465.209 MB
% 12.24/10.45 % Net memory used: 448.460 MB
%------------------------------------------------------------------------------