%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW181+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 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 : Sun Sep 27 09:11:29 AM UTC 2026
% Result : Theorem 80.50s 15.91s
% Output : CNFRefutation 80.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 11
% Syntax : Number of formulae : 43 ( 17 unt; 0 def)
% Number of atoms : 78 ( 12 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 66 ( 31 ~; 23 |; 3 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-3 aty)
% Number of variables : 41 ( 2 sgn 15 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_pCons,axiom,
? [X0] :
( ! [X1] :
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',X1),'v$ur')
=> 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$ucs'),X1)),X0) )
& 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),X0) ) ).
fof(fact_norm__ge__zero,axiom,
! [X0,X1] :
( 'class$uRealVector$uOreal$u$unormed$u$uvector'(X1)
=> 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'(X1,X0)) ) ).
fof(fact_real__le__trans,axiom,
! [X0,X1,X2] :
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X2,X1)
=> ( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X1,X0)
=> 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X2,X0) ) ) ).
fof(fact__096_B_Bz_O_Acmod_Az_A_060_061_Ar_A_061_061_062_Acmod_A_Ipoly_A_IpCons_Ac_Acs_J_Az_J_A_060_061_A1_A_L_Acmod_Ac_A_L_Aabs_A_Ir_A_K_Am_J_096,axiom,
! [X0] :
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',X0),'v$ur')
=> 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','v$uc','v$ucs')),X0)),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'v$um')))) ) ).
fof(fact_kp,axiom,
'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'v$um')))) ).
fof(fact_real__norm__def,axiom,
! [X0] : 'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',X0) = 'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',X0) ).
fof(fact_real__mult__commute,axiom,
! [X0,X1] : hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),X1),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),X0),X1) ).
fof(fact_abs__mult__pos,axiom,
! [X0,X1,X2] :
( 'class$uRings$uOlinordered$u$uidom'(X2)
=> ( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X2,'c$uGroups$uOzero$u$uclass$uOzero'(X2),X1)
=> hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X2),'c$uGroups$uOabs$u$uclass$uOabs'(X2,X0)),X1) = 'c$uGroups$uOabs$u$uclass$uOabs'(X2,hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X2),X0),X1)) ) ) ).
fof(arity_RealDef__Oreal__Rings_Olinordered__idom,axiom,
'class$uRings$uOlinordered$u$uidom'('tc$uRealDef$uOreal') ).
fof(arity_Complex__Ocomplex__RealVector_Oreal__normed__vector,axiom,
'class$uRealVector$uOreal$u$unormed$u$uvector'('tc$uComplex$uOcomplex') ).
fof(conj_0,conjecture,
? [X0] :
( ! [X1] :
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',X1),'v$ur')
=> 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','v$uc','v$ucs')),X1)),X0) )
& 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),X0) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0] :
( ! [X1] :
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',X1),'v$ur')
=> 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','v$uc','v$ucs')),X1)),X0) )
& 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),X0) ),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c2,plain,
'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),sK4),
inference(clausification,[status(esa)],[fact_pCons]) ).
cnf(c9,plain,
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'(X0,X1))
| ~ 'class$uRealVector$uOreal$u$unormed$u$uvector'(X0) ),
inference(clausification,[status(esa)],[fact_norm__ge__zero]) ).
cnf(c23,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X1,X2)
| 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X0,X2)
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X0,X1) ),
inference(clausification,[status(esa)],[fact_real__le__trans]) ).
cnf(c32,plain,
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','v$uc','v$ucs')),X0)),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'v$um'))))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',X0),'v$ur') ),
inference(clausification,[status(esa)],[fact__096_B_Bz_O_Acmod_Az_A_060_061_Ar_A_061_061_062_Acmod_A_Ipoly_A_IpCons_Ac_Acs_J_Az_J_A_060_061_A1_A_L_Acmod_Ac_A_L_Aabs_A_Ir_A_K_Am_J_096]) ).
cnf(c33,plain,
'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'v$um')))),
inference(clausification,[status(esa)],[fact_kp]) ).
cnf(c36,plain,
'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',X0) = 'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',X0),
inference(clausification,[status(esa)],[fact_real__norm__def]) ).
cnf(c38,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),X0),X1) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),X1),X0),
inference(clausification,[status(esa)],[fact_real__mult__commute]) ).
cnf(c64,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X0,'c$uGroups$uOzero$u$uclass$uOzero'(X0),X2)
| 'c$uGroups$uOabs$u$uclass$uOabs'(X0,hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),X1),X2)) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),'c$uGroups$uOabs$u$uclass$uOabs'(X0,X1)),X2)
| ~ 'class$uRings$uOlinordered$u$uidom'(X0) ),
inference(clausification,[status(esa)],[fact_abs__mult__pos]) ).
cnf(c911,plain,
'class$uRings$uOlinordered$u$uidom'('tc$uRealDef$uOreal'),
inference(clausification,[status(esa)],[arity_RealDef__Oreal__Rings_Olinordered__idom]) ).
cnf(c920,plain,
'class$uRealVector$uOreal$u$unormed$u$uvector'('tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[arity_Complex__Ocomplex__RealVector_Oreal__normed__vector]) ).
cnf(c941,plain,
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',sK1601(X0)),'v$ur')
| ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),X0) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c942,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','v$uc','v$ucs')),sK1601(X0))),X0)
| ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),X0) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),X1)
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X0,'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',sK1601(X1)))
| 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X0,'v$ur') ),
inference(resolution,[status(thm)],[c23,c941]) ).
cnf(d1,plain,
( ~ 'class$uRealVector$uOreal$u$unormed$u$uvector'('tc$uComplex$uOcomplex')
| ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),X0)
| 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'v$ur') ),
inference(resolution,[status(thm)],[d0,c9]) ).
cnf(d2,plain,
( ~ 'class$uRealVector$uOreal$u$unormed$u$uvector'('tc$uComplex$uOcomplex')
| 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'v$ur') ),
inference(resolution,[status(thm)],[d1,c2]) ).
cnf(d3,plain,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'v$ur'),
inference(resolution,[status(thm)],[c920,d2]) ).
cnf(d4,plain,
( ~ 'class$uRings$uOlinordered$u$uidom'('tc$uRealDef$uOreal')
| 'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),X0),'v$ur')) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',X0)),'v$ur') ),
inference(resolution,[status(thm)],[d3,c64]) ).
cnf(d5,plain,
( ~ 'class$uRings$uOlinordered$u$uidom'('tc$uRealDef$uOreal')
| 'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),X0),'v$ur')) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',X0)),'v$ur') ),
inference(demodulation,[status(thm)],[d4,c36]) ).
cnf(d6,plain,
( ~ 'class$uRings$uOlinordered$u$uidom'('tc$uRealDef$uOreal')
| 'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),X0),'v$ur')) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',X0)) ),
inference(demodulation,[status(thm)],[d5,c38]) ).
cnf(d7,plain,
( ~ 'class$uRings$uOlinordered$u$uidom'('tc$uRealDef$uOreal')
| 'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),X0),'v$ur')) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',X0)) ),
inference(demodulation,[status(thm)],[d6,c36]) ).
cnf(d8,plain,
'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),X0),'v$ur')) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',X0)),
inference(resolution,[status(thm)],[c911,d7]) ).
cnf(d9,plain,
'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),X0)) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',X0)),
inference(superposition,[status(thm)],[c38,d8]) ).
cnf(d10,plain,
'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'v$um')))),
inference(demodulation,[status(thm)],[c33,c36]) ).
cnf(d11,plain,
'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal','v$um')))),
inference(demodulation,[status(thm)],[d10,d9]) ).
cnf(d12,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'v$um'))))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',sK1601('c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'v$um'))))),'v$ur') ),
inference(resolution,[status(thm)],[c32,c942]) ).
cnf(d13,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'v$um'))))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',sK1601('c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'v$um'))))),'v$ur') ),
inference(demodulation,[status(thm)],[d12,c36]) ).
cnf(d14,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'v$um'))))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',sK1601('c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal','v$um'))))),'v$ur') ),
inference(demodulation,[status(thm)],[d13,d9]) ).
cnf(d15,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'v$um'))))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',sK1601('c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal','v$um'))))),'v$ur') ),
inference(demodulation,[status(thm)],[d14,c36]) ).
cnf(d16,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal','v$um'))))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex',sK1601('c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal','v$um'))))),'v$ur') ),
inference(demodulation,[status(thm)],[d15,d9]) ).
cnf(d17,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal','v$um'))))
| ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uComplex$uOcomplex','v$uc')),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ur'),'c$uRealVector$uOnorm$u$uclass$uOnorm'('tc$uRealDef$uOreal','v$um')))) ),
inference(resolution,[status(thm)],[c941,d16]) ).
cnf(d18,plain,
$false,
inference(resolution,[status(thm)],[d17,d11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW181+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n017.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sat Sep 26 15:19:48 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 80.50/15.91 % SZS status Theorem for theBenchmark.p
% 80.50/15.91 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------