%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW211+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 : n019.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 28.04s 14.19s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW211+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/10.48 % Computer : n019.cluster.edu
% 0.18/10.48 % Model : x86_64 x86_64
% 0.18/10.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/10.48 % Memory : 8046.5625MB
% 0.18/10.48 % OS : Linux 6.8.0-71-generic
% 0.18/10.48 % CPULimit : 300
% 0.18/10.48 % WCLimit : 300
% 0.18/10.48 % DateTime : Mon Sep 21 09:41:16 UTC 2026
% 0.18/10.48 % CPUTime :
% 0.21/10.57 % Drodi V4.1.1
% 28.04/14.19 % Refutation found
% 28.04/14.19 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.04/14.19 % SZS output start CNFRefutation for theBenchmark
% 28.04/14.19 fof(f10,axiom,(
% 28.04/14.19 (! [V_real2_H_2,V_real1_H_2,V_real2_2,V_real1_2] :( c_Complex_Ocomplex_OComplex(V_real1_2,V_real2_2) = c_Complex_Ocomplex_OComplex(V_real1_H_2,V_real2_H_2)<=> ( V_real1_2 = V_real1_H_2& V_real2_2 = V_real2_H_2 ) ) )),
% 28.04/14.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.04/14.19 fof(f12,axiom,(
% 28.04/14.19 (! [V_xa_2,V_gb_2,V_fa_2,T_c,T_a,T_b] : hAPP(c_Fun_Ocomp(T_b,T_a,T_c,V_fa_2,V_gb_2),V_xa_2) = hAPP(V_fa_2,hAPP(V_gb_2,V_xa_2)) )),
% 28.04/14.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.04/14.19 fof(f48,axiom,(
% 28.04/14.19 (! [V_z,V_x,V_y,T_a] :( class_Orderings_Oorder(T_a)=> ( c_Orderings_Oord__class_Oless(T_a,V_y,V_x)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_z,V_y)=> c_Orderings_Oord__class_Oless(T_a,V_z,V_x) ) ) ) )),
% 28.04/14.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.04/14.19 fof(f274,axiom,(
% 28.04/14.19 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_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),c_Groups_Oplus__class_Oplus(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____,hAPP(v_ga____,v_n____)))),c_Complex_ORe(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))),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____,v_n____)))),c_Complex_OIm(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))))) ),
% 28.04/14.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.04/14.19 fof(f282,axiom,(
% 28.04/14.19 (! [V_z] : c_Complex_Ocomplex_OComplex(c_Complex_ORe(V_z),c_Complex_OIm(V_z)) = V_z )),
% 28.04/14.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.04/14.19 fof(f283,axiom,(
% 28.04/14.19 (! [V_r] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,V_r) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) )),
% 28.04/14.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.04/14.19 fof(f348,axiom,(
% 28.04/14.19 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(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____,hAPP(v_ga____,v_n____)))),v_x____)),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____,v_n____)))),v_y____))),c_Groups_Oplus__class_Oplus(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)))),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)))))) ),
% 28.04/14.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.04/14.19 fof(f358,axiom,(
% 28.04/14.19 (! [V_x] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,V_x,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,V_x,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = V_x )),
% 28.04/14.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.04/14.19 fof(f1144,axiom,(
% 28.04/14.19 class_Orderings_Oorder(tc_RealDef_Oreal) ),
% 28.04/14.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.04/14.19 fof(f1230,conjecture,(
% 28.04/14.19 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_s(hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),v_n____)),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),v_e____) ),
% 28.04/14.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.04/14.19 fof(f1231,negated_conjecture,(
% 28.04/14.19 ~(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_s(hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),v_n____)),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),v_e____) )),
% 28.04/14.19 inference(negated_conjecture,[status(cth)],[f1230])).
% 28.04/14.19 fof(f1249,plain,(
% 28.04/14.19 ![V_real2_H_2,V_real1_H_2,V_real2_2,V_real1_2]: ((~c_Complex_Ocomplex_OComplex(V_real1_2,V_real2_2)=c_Complex_Ocomplex_OComplex(V_real1_H_2,V_real2_H_2)|(V_real1_2=V_real1_H_2&V_real2_2=V_real2_H_2))&(c_Complex_Ocomplex_OComplex(V_real1_2,V_real2_2)=c_Complex_Ocomplex_OComplex(V_real1_H_2,V_real2_H_2)|(~V_real1_2=V_real1_H_2|~V_real2_2=V_real2_H_2)))),
% 28.04/14.19 inference(NNF_transformation,[status(thm)],[f10])).
% 28.04/14.19 fof(f1250,plain,(
% 28.04/14.19 (![V_real2_H_2,V_real1_H_2,V_real2_2,V_real1_2]: (~c_Complex_Ocomplex_OComplex(V_real1_2,V_real2_2)=c_Complex_Ocomplex_OComplex(V_real1_H_2,V_real2_H_2)|(V_real1_2=V_real1_H_2&V_real2_2=V_real2_H_2)))&(![V_real2_H_2,V_real1_H_2,V_real2_2,V_real1_2]: (c_Complex_Ocomplex_OComplex(V_real1_2,V_real2_2)=c_Complex_Ocomplex_OComplex(V_real1_H_2,V_real2_H_2)|(~V_real1_2=V_real1_H_2|~V_real2_2=V_real2_H_2)))),
% 28.04/14.19 inference(miniscoping,[status(thm)],[f1249])).
% 28.04/14.19 fof(f1251,plain,(
% 28.04/14.19 ![X0,X1,X2,X3]: (~c_Complex_Ocomplex_OComplex(X0,X1)=c_Complex_Ocomplex_OComplex(X2,X3)|X0=X2)),
% 28.04/14.19 inference(cnf_transformation,[status(thm)],[f1250])).
% 28.04/14.19 fof(f1252,plain,(
% 28.04/14.19 ![X0,X1,X2,X3]: (~c_Complex_Ocomplex_OComplex(X0,X1)=c_Complex_Ocomplex_OComplex(X2,X3)|X1=X3)),
% 28.04/14.19 inference(cnf_transformation,[status(thm)],[f1250])).
% 28.04/14.19 fof(f1255,plain,(
% 28.04/14.19 ![X0,X1,X2,X3,X4,X5]: (hAPP(c_Fun_Ocomp(X0,X1,X2,X3,X4),X5)=hAPP(X3,hAPP(X4,X5)))),
% 28.04/14.19 inference(cnf_transformation,[status(thm)],[f12])).
% 28.04/14.19 fof(f1370,plain,(
% 28.04/14.19 ![V_z,V_x,V_y,T_a]: (~class_Orderings_Oorder(T_a)|(~c_Orderings_Oord__class_Oless(T_a,V_y,V_x)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_z,V_y)|c_Orderings_Oord__class_Oless(T_a,V_z,V_x))))),
% 28.04/14.19 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 28.04/14.19 fof(f1371,plain,(
% 28.04/14.19 ![T_a]: (~class_Orderings_Oorder(T_a)|(![V_x,V_y]: (~c_Orderings_Oord__class_Oless(T_a,V_y,V_x)|(![V_z]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_z,V_y)|c_Orderings_Oord__class_Oless(T_a,V_z,V_x))))))),
% 28.04/14.19 inference(miniscoping,[status(thm)],[f1370])).
% 28.04/14.19 fof(f1372,plain,(
% 28.04/14.19 ![X0,X1,X2,X3]: (~class_Orderings_Oorder(X0)|~c_Orderings_Oord__class_Oless(X0,X1,X2)|~c_Orderings_Oord__class_Oless__eq(X0,X3,X1)|c_Orderings_Oord__class_Oless(X0,X3,X2))),
% 28.04/14.19 inference(cnf_transformation,[status(thm)],[f1371])).
% 28.04/14.19 fof(f2080,plain,(
% 28.04/14.19 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_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),c_Groups_Oplus__class_Oplus(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____,hAPP(v_ga____,v_n____)))),c_Complex_ORe(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))),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____,v_n____)))),c_Complex_OIm(c_Complex_Ocomplex_OComplex(v_x____,v_y____))))))),
% 28.04/14.19 inference(cnf_transformation,[status(thm)],[f274])).
% 28.04/14.19 fof(f2114,plain,(
% 28.04/14.19 ![X0]: (c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(X0))=X0)),
% 28.04/14.19 inference(cnf_transformation,[status(thm)],[f282])).
% 28.04/14.19 fof(f2115,plain,(
% 28.04/14.19 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 28.04/14.19 inference(cnf_transformation,[status(thm)],[f283])).
% 28.04/14.19 fof(f2284,plain,(
% 28.04/14.19 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(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____,hAPP(v_ga____,v_n____)))),v_x____)),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____,v_n____)))),v_y____))),c_Groups_Oplus__class_Oplus(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)))),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))))))),
% 28.04/14.19 inference(cnf_transformation,[status(thm)],[f348])).
% 28.04/14.19 fof(f2320,plain,(
% 28.04/14.19 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))=X0)),
% 28.04/14.19 inference(cnf_transformation,[status(thm)],[f358])).
% 28.04/14.19 fof(f4421,plain,(
% 28.04/14.19 class_Orderings_Oorder(tc_RealDef_Oreal)),
% 28.04/14.19 inference(cnf_transformation,[status(thm)],[f1144])).
% 28.04/14.19 fof(f4507,plain,(
% 28.04/14.19 ~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_s(hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),v_n____)),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),v_e____)),
% 28.04/14.19 inference(cnf_transformation,[status(thm)],[f1231])).
% 28.04/14.19 fof(f4593,plain,(
% 28.04/14.19 ~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_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),v_e____)),
% 28.04/14.19 inference(backward_demodulation,[status(thm)],[f1255,f4507])).
% 28.04/14.19 fof(f5649,plain,(
% 28.04/14.19 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_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),c_Complex_ORe(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))),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____,v_n____)))),c_Complex_OIm(c_Complex_Ocomplex_OComplex(v_x____,v_y____))))))),
% 28.04/14.19 inference(forward_demodulation,[status(thm)],[f2115,f2080])).
% 28.04/14.19 fof(f5650,plain,(
% 28.04/14.19 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_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),c_Complex_ORe(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),c_Complex_OIm(c_Complex_Ocomplex_OComplex(v_x____,v_y____))))))),
% 28.04/14.19 inference(forward_demodulation,[status(thm)],[f2115,f5649])).
% 28.04/14.19 fof(f5658,plain,(
% 28.04/14.19 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),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____,v_n____)))),v_y____))),c_Groups_Oplus__class_Oplus(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)))),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))))))),
% 28.04/14.19 inference(forward_demodulation,[status(thm)],[f2115,f2284])).
% 28.04/14.19 fof(f5659,plain,(
% 28.04/14.19 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))),c_Groups_Oplus__class_Oplus(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)))),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))))))),
% 28.04/14.19 inference(forward_demodulation,[status(thm)],[f2115,f5658])).
% 28.04/14.19 fof(f5661,plain,(
% 28.04/14.19 ![X0]: (~class_Orderings_Oorder(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(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)))),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)))))))),
% 28.04/14.19 inference(resolution,[status(thm)],[f5659,f1372])).
% 28.04/14.19 fof(f18128,plain,(
% 28.04/14.19 ![X0,X1]: (c_Complex_OIm(c_Complex_Ocomplex_OComplex(X0,X1))=X1)),
% 28.04/14.19 inference(resolution,[status(thm)],[f2114,f1252])).
% 28.04/14.19 fof(f18129,plain,(
% 28.04/14.19 ![X0,X1]: (c_Complex_ORe(c_Complex_Ocomplex_OComplex(X0,X1))=X0)),
% 28.04/14.19 inference(resolution,[status(thm)],[f2114,f1251])).
% 28.04/14.19 fof(f18240,plain,(
% 28.04/14.19 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_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),c_Complex_ORe(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))))),
% 28.04/14.19 inference(backward_demodulation,[status(thm)],[f18128,f5650])).
% 28.04/14.19 fof(f18372,plain,(
% 28.04/14.19 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_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))))),
% 28.04/14.19 inference(backward_demodulation,[status(thm)],[f18129,f18240])).
% 28.04/14.19 fof(f35408,plain,(
% 28.04/14.19 ![X0]: (~class_Orderings_Oorder(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_e____))),
% 28.04/14.19 inference(forward_demodulation,[status(thm)],[f2320,f5661])).
% 28.04/14.19 fof(f35409,plain,(
% 28.04/14.19 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_e____))),
% 28.89/14.25 inference(forward_subsumption_resolution,[status(thm)],[f35408,f4421])).
% 28.89/14.25 fof(f35410,plain,(
% 28.89/14.25 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_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),v_e____)),
% 28.89/14.25 inference(resolution,[status(thm)],[f35409,f18372])).
% 28.89/14.25 fof(f35416,plain,(
% 28.89/14.25 $false),
% 28.89/14.25 inference(forward_subsumption_resolution,[status(thm)],[f35410,f4593])).
% 28.89/14.25 % SZS output end CNFRefutation for theBenchmark.p
% 28.89/14.27 % Elapsed time: 3.770601 seconds
% 28.89/14.27 % CPU time: 29.134271 seconds
% 28.89/14.27 % Total memory used: 547.187 MB
% 28.89/14.27 % Net memory used: 531.252 MB
%------------------------------------------------------------------------------