%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW207+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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:07:26 PM UTC 2026
% Result : Theorem 0.24s 0.66s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 14
% Syntax : Number of formulae : 71 ( 19 unt; 3 def)
% Number of atoms : 161 ( 30 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 158 ( 68 ~; 75 |; 7 &)
% ( 4 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 4 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-2 aty)
% Number of variables : 80 ( 77 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [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)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [V_y_2,V_x_2] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2))
<=> ( V_x_2 != V_y_2
& hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [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 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [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)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [V_w,V_z] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w),V_z))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z),V_w)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [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))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
hAPP(c_Complex_OIm,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,axiom,
! [V_r] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,V_r) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f133,axiom,
! [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)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1269,conjecture,
? [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))
& hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),B_K)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1270,negated_conjecture,
~ ? [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))
& hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),B_K)) ),
inference(negated_conjecture,[status(cth)],[f1269]) ).
fof(f1276,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f1302,plain,
! [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)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f1303,plain,
! [V_y_2,V_x_2] :
( ( V_x_2 = V_y_2
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2)) )
& ( ( V_x_2 != V_y_2
& hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2)) )
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2)) ) ),
inference(NNF_transformation,[status(thm)],[f13]) ).
fof(f1304,plain,
( ! [V_y_2,V_x_2] :
( V_x_2 = V_y_2
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2)) )
& ! [V_y_2,V_x_2] :
( ( V_x_2 != V_y_2
& hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2)) )
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2)) ) ),
inference(miniscoping,[status(thm)],[f1303]) ).
fof(f1305,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f1304]) ).
fof(f1306,plain,
! [X0,X1] :
( X0 != X1
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f1304]) ).
fof(f1307,plain,
! [X0,X1] :
( X0 = X1
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f1304]) ).
fof(f1452,plain,
! [V_w,V_z] :
( V_z = V_w
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w),V_z))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z),V_w)) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f1453,plain,
! [X0,X1] :
( X0 = X1
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),X0))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f1452]) ).
fof(f1454,plain,
! [V_k,V_j,V_i] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),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_j)) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f1455,plain,
! [V_j,V_i] :
( ! [V_k] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),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_j)) ),
inference(miniscoping,[status(thm)],[f1454]) ).
fof(f1456,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X2))
| ~ 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),X1)) ),
inference(cnf_transformation,[status(thm)],[f1455]) ).
fof(f1457,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),X0))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f1549,plain,
! [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))),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f1576,plain,
hAPP(c_Complex_OIm,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f1622,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f1713,plain,
! [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)))),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f4607,plain,
! [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))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),B_K)) ),
inference(pre_NNF_transformation,[status(thm)],[f1270]) ).
fof(f4608,plain,
! [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))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),B_K)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK73_skl]),skolemize(B_n,sK73_skl(B_K))],[f4607]) ).
fof(f4609,plain,
! [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))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),X0)) ),
inference(cnf_transformation,[status(thm)],[f4608]) ).
fof(f4657,plain,
! [X0] : ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X0)),
inference(destructive_equality_resolution,[status(thm)],[f1306]) ).
fof(f4789,plain,
! [X0] :
( ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(X0))))))),X0))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),X0)) ),
inference(backward_demodulation,[status(thm)],[f1622,f4609]) ).
fof(f4796,definition,
( sQ1_spl
<=> c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = v_r ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f4797,plain,
( ~ sQ1_spl
| c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = v_r ),
inference(component_clause,[status(thm)],[f4796]) ).
fof(f4800,plain,
( v_r = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))) ),
inference(resolution,[status(thm)],[f1453,f1276]) ).
fof(f4802,definition,
( sQ2_spl
<=> hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f4804,plain,
( sQ2_spl
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))) ),
inference(component_clause,[status(thm)],[f4802]) ).
fof(f4805,plain,
( sQ1_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f4800,f4802,f4796]) ).
fof(f4810,plain,
! [X0] :
( ~ sQ1_spl
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(X0))))))),X0))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_r),X0)) ),
inference(backward_demodulation,[status(thm)],[f4797,f4789]) ).
fof(f4822,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2),X0))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2),X1))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1)) ),
inference(resolution,[status(thm)],[f1457,f1456]) ).
fof(f4824,plain,
! [X0,X1] :
( X1 = X0
| hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1),X0))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1)) ),
inference(resolution,[status(thm)],[f1457,f1307]) ).
fof(f4834,plain,
( ~ sQ1_spl
| hAPP(c_Complex_OIm,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = v_r ),
inference(backward_demodulation,[status(thm)],[f4797,f1576]) ).
fof(f4839,plain,
! [X0] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,X0))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))),
inference(forward_demodulation,[status(thm)],[f1622,f1549]) ).
fof(f4866,plain,
! [X0] :
( ~ sQ1_spl
| 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)))) ),
inference(forward_demodulation,[status(thm)],[f4797,f1713]) ).
fof(f4867,plain,
! [X0] :
( ~ sQ1_spl
| 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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)))) ),
inference(forward_demodulation,[status(thm)],[f1622,f4866]) ).
fof(f4870,plain,
! [X0] :
( ~ sQ1_spl
| 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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)))) ),
inference(resolution,[status(thm)],[f4867,f1305]) ).
fof(f4873,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),v_r))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,X1)))) ),
inference(resolution,[status(thm)],[f1302,f1456]) ).
fof(f4935,plain,
! [X0] :
( ~ sQ1_spl
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(X0))))))),X0))
| v_r = X0
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),v_r)) ),
inference(resolution,[status(thm)],[f4824,f4810]) ).
fof(f5189,plain,
! [X0] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,X0)))),v_r)),
inference(resolution,[status(thm)],[f4873,f4839]) ).
fof(f5211,plain,
! [X0,X1] :
( ~ sQ1_spl
| v_r = X0
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),v_r))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(X0))))))),X1))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1)) ),
inference(resolution,[status(thm)],[f4822,f4935]) ).
fof(f5253,plain,
! [X0,X1] :
( ~ sQ1_spl
| v_r = X0
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),X0))
| v_r = X0
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(X0))))))),X1))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1)) ),
inference(resolution,[status(thm)],[f5211,f1453]) ).
fof(f5259,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),X0))
| v_r = X0
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(X0))))))),X1))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f5253]) ).
fof(f5264,plain,
! [X0] :
( ~ sQ1_spl
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),X0))
| v_r = X0
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),v_r)) ),
inference(resolution,[status(thm)],[f5259,f5189]) ).
fof(f5276,plain,
! [X0] :
( ~ sQ1_spl
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),X0))
| v_r = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f5264,f1453]) ).
fof(f5294,plain,
! [X0] :
( ~ sQ1_spl
| v_r = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)) ),
inference(resolution,[status(thm)],[f5276,f4870]) ).
fof(f5325,plain,
! [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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)))),
inference(forward_demodulation,[status(thm)],[f1622,f1713]) ).
fof(f5345,plain,
( ~ sQ1_spl
| c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = v_r ),
inference(forward_demodulation,[status(thm)],[f1576,f4834]) ).
fof(f5369,plain,
! [X0] :
( c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = X0
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(X0))))))),X0)) ),
inference(resolution,[status(thm)],[f4789,f4824]) ).
fof(f5413,plain,
( sQ2_spl
| 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_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(v_r))))))),v_r)) ),
inference(resolution,[status(thm)],[f4804,f5369]) ).
fof(f5417,definition,
( sQ41_spl
<=> hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(v_r))))))),v_r)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f5419,plain,
( sQ41_spl
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl(v_r))))))),v_r)) ),
inference(component_clause,[status(thm)],[f5417]) ).
fof(f5420,plain,
( sQ2_spl
| sQ1_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f5413,f5417,f4796,f4802]) ).
fof(f5425,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5419,f5189]) ).
fof(f5426,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f5425]) ).
fof(f5451,plain,
! [X0] :
( ~ sQ1_spl
| 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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)))) ),
inference(forward_demodulation,[status(thm)],[f5345,f5325]) ).
fof(f5525,plain,
( ~ sQ1_spl
| hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_r),v_r)) ),
inference(backward_demodulation,[status(thm)],[f5294,f5451]) ).
fof(f5528,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5525,f4657]) ).
fof(f5529,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f5528]) ).
fof(f5530,plain,
$false,
inference(sat_refutation,[status(thm)],[f4805,f5420,f5426,f5529]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW207+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.02/0.35 % CPULimit : 300
% 0.02/0.36 % WCLimit : 300
% 0.02/0.36 % DateTime : Mon Sep 21 09:41:20 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.24/0.51 % Drodi V4.1.1
% 0.24/0.66 % Refutation found
% 0.24/0.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.24/0.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.31/0.69 % Elapsed time: 0.320958 seconds
% 0.31/0.69 % CPU time: 1.041599 seconds
% 0.31/0.69 % Total memory used: 219.573 MB
% 0.31/0.69 % Net memory used: 217.969 MB
%------------------------------------------------------------------------------