%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW207+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 : n014.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 0.27s 0.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW207+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.52 % Computer : n014.cluster.edu
% 0.11/0.52 % Model : x86_64 x86_64
% 0.11/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.52 % Memory : 8046.5625MB
% 0.11/0.52 % OS : Linux 6.8.0-71-generic
% 0.11/0.52 % CPULimit : 300
% 0.11/0.52 % WCLimit : 300
% 0.11/0.52 % DateTime : Mon Sep 21 09:41:20 UTC 2026
% 0.11/0.52 % CPUTime :
% 0.25/0.63 % Drodi V4.1.1
% 0.27/0.77 % Refutation found
% 0.27/0.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.27/0.77 % SZS output start CNFRefutation for theBenchmark
% 0.27/0.77 fof(f4,axiom,(
% 0.27/0.77 hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)) ),
% 0.27/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.77 fof(f12,axiom,(
% 0.27/0.77 (! [B_n] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,B_n))),v_r)) )),
% 0.27/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.77 fof(f13,axiom,(
% 0.27/0.77 (! [V_y_2,V_x_2] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2))<=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))& V_x_2 != V_y_2 ) ) )),
% 0.27/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.77 fof(f56,axiom,(
% 0.27/0.77 (! [V_w,V_z] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z),V_w))=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w),V_z))=> V_z = V_w ) ) )),
% 0.27/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.77 fof(f57,axiom,(
% 0.27/0.77 (! [V_k,V_j,V_i] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_j))=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j),V_k))=> hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_k)) ) ) )),
% 0.27/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.77 fof(f58,axiom,(
% 0.27/0.77 (! [V_w,V_z] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z),V_w))| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w),V_z)) ) )),
% 0.27/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.77 fof(f84,axiom,(
% 0.27/0.77 (! [V_x] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,V_x))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,V_x))) )),
% 0.27/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.77 fof(f133,axiom,(
% 0.27/0.77 (! [V_x] : hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_x)))) )),
% 0.27/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.77 fof(f1269,conjecture,(
% 0.27/0.77 (? [B_K] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),B_K))& (! [B_n] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,B_n)))))),B_K)) )) )),
% 0.27/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.77 fof(f1270,negated_conjecture,(
% 0.27/0.77 ~((? [B_K] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),B_K))& (! [B_n] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,B_n)))))),B_K)) )) ))),
% 0.27/0.77 inference(negated_conjecture,[status(cth)],[f1269])).
% 0.27/0.77 fof(f1276,plain,(
% 0.27/0.77 hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r))),
% 0.27/0.77 inference(cnf_transformation,[status(thm)],[f4])).
% 0.27/0.77 fof(f1302,plain,(
% 0.27/0.77 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,X0))),v_r)))),
% 0.27/0.77 inference(cnf_transformation,[status(thm)],[f12])).
% 0.27/0.77 fof(f1303,plain,(
% 0.27/0.77 ![V_y_2,V_x_2]: ((~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2))|(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))&~V_x_2=V_y_2))&(hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2))|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))|V_x_2=V_y_2)))),
% 0.27/0.77 inference(NNF_transformation,[status(thm)],[f13])).
% 0.27/0.77 fof(f1304,plain,(
% 0.27/0.77 (![V_y_2,V_x_2]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2))|(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))&~V_x_2=V_y_2)))&(![V_y_2,V_x_2]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2))|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))|V_x_2=V_y_2)))),
% 0.27/0.77 inference(miniscoping,[status(thm)],[f1303])).
% 0.27/0.77 fof(f1305,plain,(
% 0.27/0.77 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X1))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1)))),
% 0.27/0.77 inference(cnf_transformation,[status(thm)],[f1304])).
% 0.27/0.77 fof(f1306,plain,(
% 0.27/0.77 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X1))|~X0=X1)),
% 0.27/0.77 inference(cnf_transformation,[status(thm)],[f1304])).
% 0.27/0.77 fof(f1307,plain,(
% 0.27/0.77 ![X0,X1]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X1))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1))|X0=X1)),
% 0.27/0.77 inference(cnf_transformation,[status(thm)],[f1304])).
% 0.27/0.77 fof(f1452,plain,(
% 0.27/0.77 ![V_w,V_z]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z),V_w))|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w),V_z))|V_z=V_w))),
% 0.27/0.77 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 0.27/0.77 fof(f1453,plain,(
% 0.27/0.77 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),X0))|X0=X1)),
% 0.27/0.77 inference(cnf_transformation,[status(thm)],[f1452])).
% 0.27/0.77 fof(f1454,plain,(
% 0.27/0.77 ![V_k,V_j,V_i]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_j))|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j),V_k))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_k))))),
% 0.27/0.77 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.27/0.77 fof(f1455,plain,(
% 0.27/0.77 ![V_j,V_i]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_j))|(![V_k]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j),V_k))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_k)))))),
% 0.27/0.77 inference(miniscoping,[status(thm)],[f1454])).
% 0.27/0.77 fof(f1456,plain,(
% 0.27/0.77 ![X0,X1,X2]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),X2))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X2)))),
% 0.27/0.77 inference(cnf_transformation,[status(thm)],[f1455])).
% 0.27/0.77 fof(f1457,plain,(
% 0.27/0.77 ![X0,X1]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),X0)))),
% 0.27/0.77 inference(cnf_transformation,[status(thm)],[f58])).
% 0.27/0.77 fof(f1549,plain,(
% 0.27/0.77 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,X0))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))))),
% 0.27/0.77 inference(cnf_transformation,[status(thm)],[f84])).
% 0.27/0.77 fof(f1713,plain,(
% 0.27/0.77 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)))))),
% 0.27/0.77 inference(cnf_transformation,[status(thm)],[f133])).
% 0.27/0.77 fof(f4607,plain,(
% 0.27/0.77 (![B_K]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),B_K))|(?[B_n]: ~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,B_n)))))),B_K)))))),
% 0.27/0.77 inference(pre_NNF_transformation,[status(thm)],[f1270])).
% 0.27/0.77 fof(f4608,plain,(
% 0.27/0.77 ![B_K]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),B_K))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(B_K))))))),B_K)))),
% 0.27/0.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK73_skl]),skolemize(B_n,sK73_skl(B_K))],[f4607])).
% 0.27/0.77 fof(f4609,plain,(
% 0.27/0.77 ![X0]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),X0))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(X0))))))),X0)))),
% 0.27/0.77 inference(cnf_transformation,[status(thm)],[f4608])).
% 0.27/0.77 fof(f4657,plain,(
% 0.27/0.77 ![X0]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X0)))),
% 0.27/0.77 inference(destructive_equality_resolution,[status(thm)],[f1306])).
% 0.27/0.77 fof(f4791,plain,(
% 0.27/0.77 hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r))|c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r),
% 0.27/0.77 inference(resolution,[status(thm)],[f1276,f1307])).
% 0.27/0.77 fof(f4809,plain,(
% 0.27/0.77 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,X1))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X1))))),
% 0.27/0.77 inference(resolution,[status(thm)],[f1549,f1456])).
% 0.27/0.77 fof(f4813,plain,(
% 0.27/0.77 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,X1))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),v_r)))),
% 0.27/0.77 inference(resolution,[status(thm)],[f1302,f1456])).
% 0.27/0.77 fof(f4816,plain,(
% 0.27/0.77 ![X0]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))))))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)))))),
% 0.27/0.77 inference(resolution,[status(thm)],[f1713,f4609])).
% 0.27/0.77 fof(f4817,plain,(
% 0.27/0.77 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)))))),
% 0.27/0.77 inference(resolution,[status(thm)],[f1713,f1305])).
% 0.27/0.77 fof(f4821,plain,(
% 0.27/0.77 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))))))))),X1))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)))))),
% 0.27/0.77 inference(resolution,[status(thm)],[f4816,f1456])).
% 0.27/0.77 fof(f4838,plain,(
% 0.27/0.77 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))))))))),X1))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),X1)))),
% 0.27/0.77 inference(resolution,[status(thm)],[f4821,f1457])).
% 0.27/0.77 fof(f4854,plain,(
% 0.27/0.77 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))))))))))),
% 0.27/0.77 inference(resolution,[status(thm)],[f4838,f1549])).
% 0.27/0.78 fof(f5019,plain,(
% 0.27/0.78 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(v_r))))))),v_r))),
% 0.27/0.78 inference(resolution,[status(thm)],[f4791,f4609])).
% 0.27/0.78 fof(f5048,plain,(
% 0.27/0.78 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(v_r))))))))),
% 0.27/0.78 inference(resolution,[status(thm)],[f5019,f1457])).
% 0.27/0.78 fof(f5189,plain,(
% 0.27/0.78 hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(v_r)))))))|c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r),
% 0.27/0.78 inference(resolution,[status(thm)],[f4809,f5048])).
% 0.27/0.78 fof(f5211,plain,(
% 0.27/0.78 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(v_r)))))),v_r))|c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(v_r)))))=v_r),
% 0.27/0.78 inference(resolution,[status(thm)],[f5189,f1453])).
% 0.27/0.78 fof(f5213,plain,(
% 0.27/0.78 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r|c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(v_r)))))=v_r),
% 0.27/0.78 inference(forward_subsumption_resolution,[status(thm)],[f5211,f1302])).
% 0.27/0.78 fof(f5272,plain,(
% 0.27/0.78 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),v_r)))),
% 0.27/0.78 inference(resolution,[status(thm)],[f4813,f4854])).
% 0.27/0.78 fof(f5440,plain,(
% 0.27/0.78 hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(v_r))))))),v_r))|c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r),
% 0.27/0.78 inference(paramodulation,[status(thm)],[f5213,f1549])).
% 0.27/0.78 fof(f5443,plain,(
% 0.27/0.78 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r),
% 0.27/0.78 inference(forward_subsumption_resolution,[status(thm)],[f5440,f5019])).
% 0.27/0.78 fof(f5471,plain,(
% 0.27/0.78 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)))))),
% 0.27/0.78 inference(backward_demodulation,[status(thm)],[f5443,f4817])).
% 0.27/0.78 fof(f5491,plain,(
% 0.27/0.78 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_r),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)))))),
% 0.27/0.78 inference(backward_demodulation,[status(thm)],[f5443,f1713])).
% 0.27/0.78 fof(f5642,plain,(
% 0.27/0.78 ![X0]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),v_r))|hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))=v_r)),
% 0.27/0.78 inference(resolution,[status(thm)],[f5471,f1453])).
% 0.27/0.78 fof(f5645,plain,(
% 0.27/0.78 ![X0]: (hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))=v_r)),
% 0.27/0.78 inference(forward_subsumption_resolution,[status(thm)],[f5642,f5272])).
% 0.27/0.78 fof(f5653,plain,(
% 0.27/0.78 hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_r),v_r))),
% 0.27/0.78 inference(backward_demodulation,[status(thm)],[f5645,f5491])).
% 0.27/0.78 fof(f5672,plain,(
% 0.27/0.78 $false),
% 0.27/0.78 inference(forward_subsumption_resolution,[status(thm)],[f5653,f4657])).
% 0.27/0.78 % SZS output end CNFRefutation for theBenchmark.p
% 0.28/0.82 % Elapsed time: 0.282937 seconds
% 0.28/0.82 % CPU time: 1.235896 seconds
% 0.28/0.82 % Total memory used: 220.575 MB
% 0.28/0.82 % Net memory used: 219.094 MB
%------------------------------------------------------------------------------