%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW194+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:30 AM UTC 2026
% Result : Theorem 200.34s 29.53s
% Output : CNFRefutation 200.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 16
% Syntax : Number of formulae : 62 ( 37 unt; 0 def)
% Number of atoms : 103 ( 20 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 82 ( 41 ~; 31 |; 0 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-3 aty)
% Number of variables : 39 ( 1 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact__096abs_A_I2_A_K_Ax_J_A_060_061_A1_096,axiom,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),'v$ux')),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')) ).
fof(fact_nat__numeral__1__eq__1,axiom,
'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit1'('c$uInt$uOPls')) = 'c$uGroups$uOone$u$uclass$uOone'('tc$uNat$uOnat') ).
fof(fact_real__le__antisym,axiom,
! [X0,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',X0,X1)
=> X1 = X0 ) ) ).
fof(fact_real__le__linear,axiom,
! [X0,X1] :
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X0,X1)
| 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X1,X0) ) ).
fof(fact_real__le__refl,axiom,
! [X0] : 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X0,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_mult__2__right,axiom,
! [X0,X1] :
( 'class$uInt$uOnumber$u$uring'(X1)
=> hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X1),X0),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'(X1,'c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))) = 'c$uGroups$uOplus$u$uclass$uOplus'(X1,X0,X0) ) ).
fof(fact_power__le__imp__le__base,axiom,
! [X0,X1,X2,X3] :
( 'class$uRings$uOlinordered$u$usemidom'(X3)
=> ( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X3,hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X3),X2),'c$uNat$uOSuc'(X1)),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X3),X0),'c$uNat$uOSuc'(X1)))
=> ( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X3,'c$uGroups$uOzero$u$uclass$uOzero'(X3),X0)
=> 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X3,X2,X0) ) ) ) ).
fof(fact_abs__ge__zero,axiom,
! [X0,X1] :
( 'class$uGroups$uOordered$u$uab$u$ugroup$u$uadd$u$uabs'(X1)
=> 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X1,'c$uGroups$uOzero$u$uclass$uOzero'(X1),'c$uGroups$uOabs$u$uclass$uOabs'(X1,X0)) ) ).
fof(fact_numeral__1__eq__Suc__0,axiom,
'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit1'('c$uInt$uOPls')) = 'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) ).
fof(fact_numeral__2__eq__2,axiom,
'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))) = 'c$uNat$uOSuc'('c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))) ).
fof(fact_power__mono,axiom,
! [X0,X1,X2,X3] :
( 'class$uRings$uOlinordered$u$usemidom'(X3)
=> ( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X3,X2,X1)
=> ( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X3,'c$uGroups$uOzero$u$uclass$uOzero'(X3),X2)
=> 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X3,hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X3),X2),X0),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X3),X1),X0)) ) ) ) ).
fof(arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs,axiom,
'class$uGroups$uOordered$u$uab$u$ugroup$u$uadd$u$uabs'('tc$uRealDef$uOreal') ).
fof(arity_RealDef__Oreal__Rings_Olinordered__semidom,axiom,
'class$uRings$uOlinordered$u$usemidom'('tc$uRealDef$uOreal') ).
fof(arity_RealDef__Oreal__Int_Onumber__ring,axiom,
'class$uInt$uOnumber$u$uring'('tc$uRealDef$uOreal') ).
fof(conj_0,conjecture,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),'v$ux'))),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))) ).
fof(negated_conjecture,negated_conjecture,
~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),'v$ux'))),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c1,plain,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),'v$ux')),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),
inference(clausification,[status(esa)],[fact__096abs_A_I2_A_K_Ax_J_A_060_061_A1_096]) ).
cnf(c17,plain,
'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit1'('c$uInt$uOPls')) = 'c$uGroups$uOone$u$uclass$uOone'('tc$uNat$uOnat'),
inference(clausification,[status(esa)],[fact_nat__numeral__1__eq__1]) ).
cnf(c28,plain,
( X0 = 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',X0,X1) ),
inference(clausification,[status(esa)],[fact_real__le__antisym]) ).
cnf(c30,plain,
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X1,X0)
| 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X0,X1) ),
inference(clausification,[status(esa)],[fact_real__le__linear]) ).
cnf(c31,plain,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',X0,X0),
inference(clausification,[status(esa)],[fact_real__le__refl]) ).
cnf(c33,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(c124,plain,
( hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),X1),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'(X0,'c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))) = 'c$uGroups$uOplus$u$uclass$uOplus'(X0,X1,X1)
| ~ 'class$uInt$uOnumber$u$uring'(X0) ),
inference(clausification,[status(esa)],[fact_mult__2__right]) ).
cnf(c230,plain,
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X0,X1,X3)
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X0,'c$uGroups$uOzero$u$uclass$uOzero'(X0),X3)
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X0,hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),X1),'c$uNat$uOSuc'(X2)),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),X3),'c$uNat$uOSuc'(X2)))
| ~ 'class$uRings$uOlinordered$u$usemidom'(X0) ),
inference(clausification,[status(esa)],[fact_power__le__imp__le__base]) ).
cnf(c267,plain,
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X0,'c$uGroups$uOzero$u$uclass$uOzero'(X0),'c$uGroups$uOabs$u$uclass$uOabs'(X0,X1))
| ~ 'class$uGroups$uOordered$u$uab$u$ugroup$u$uadd$u$uabs'(X0) ),
inference(clausification,[status(esa)],[fact_abs__ge__zero]) ).
cnf(c273,plain,
'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit1'('c$uInt$uOPls')) = 'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),
inference(clausification,[status(esa)],[fact_numeral__1__eq__Suc__0]) ).
cnf(c294,plain,
'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))) = 'c$uNat$uOSuc'('c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),
inference(clausification,[status(esa)],[fact_numeral__2__eq__2]) ).
cnf(c307,plain,
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X0,hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),X1),X3),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),X2),X3))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X0,'c$uGroups$uOzero$u$uclass$uOzero'(X0),X1)
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'(X0,X1,X2)
| ~ 'class$uRings$uOlinordered$u$usemidom'(X0) ),
inference(clausification,[status(esa)],[fact_power__mono]) ).
cnf(c1142,plain,
'class$uGroups$uOordered$u$uab$u$ugroup$u$uadd$u$uabs'('tc$uRealDef$uOreal'),
inference(clausification,[status(esa)],[arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs]) ).
cnf(c1146,plain,
'class$uRings$uOlinordered$u$usemidom'('tc$uRealDef$uOreal'),
inference(clausification,[status(esa)],[arity_RealDef__Oreal__Rings_Olinordered__semidom]) ).
cnf(c1150,plain,
'class$uInt$uOnumber$u$uring'('tc$uRealDef$uOreal'),
inference(clausification,[status(esa)],[arity_RealDef__Oreal__Int_Onumber__ring]) ).
cnf(c1158,plain,
~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),'v$ux'))),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),X0),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal',X0,X0),
inference(resolution,[status(thm)],[c124,c1150]) ).
cnf(d1,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),'v$ux')))
| 'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),'v$ux')) = 'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal') ),
inference(resolution,[status(thm)],[c28,c1]) ).
cnf(d2,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),'v$ux')))
| 'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))) = 'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal') ),
inference(demodulation,[status(thm)],[d1,c33]) ).
cnf(d3,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))))
| 'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))) = 'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal') ),
inference(demodulation,[status(thm)],[d2,c33]) ).
cnf(d4,plain,
'c$uGroups$uOone$u$uclass$uOone'('tc$uNat$uOnat') = 'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),
inference(demodulation,[status(thm)],[c273,c17]) ).
cnf(d5,plain,
'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))) = 'c$uNat$uOSuc'('c$uGroups$uOone$u$uclass$uOone'('tc$uNat$uOnat')),
inference(demodulation,[status(thm)],[c294,d4]) ).
cnf(d6,plain,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),'v$ux'))),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))),
inference(resolution,[status(thm)],[c30,c1158]) ).
cnf(d7,plain,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))))),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))),
inference(demodulation,[status(thm)],[d6,c33]) ).
cnf(d8,plain,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),'c$uNat$uOSuc'('c$uGroups$uOone$u$uclass$uOone'('tc$uNat$uOnat'))),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))))),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))),
inference(demodulation,[status(thm)],[d7,d5]) ).
cnf(d9,plain,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),'c$uNat$uOSuc'('c$uGroups$uOone$u$uclass$uOone'('tc$uNat$uOnat'))),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))))),'c$uNat$uOSuc'('c$uGroups$uOone$u$uclass$uOone'('tc$uNat$uOnat')))),
inference(demodulation,[status(thm)],[d8,d5]) ).
cnf(d10,plain,
( ~ 'class$uRings$uOlinordered$u$usemidom'('tc$uRealDef$uOreal')
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))))
| 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))))) ),
inference(resolution,[status(thm)],[d9,c230]) ).
cnf(d11,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))))
| 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))))) ),
inference(resolution,[status(thm)],[c1146,d10]) ).
cnf(d12,plain,
( ~ 'class$uGroups$uOordered$u$uab$u$ugroup$u$uadd$u$uabs'('tc$uRealDef$uOreal')
| 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))))) ),
inference(resolution,[status(thm)],[d11,c267]) ).
cnf(d13,plain,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))))),
inference(resolution,[status(thm)],[c1142,d12]) ).
cnf(d14,plain,
'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))) = 'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),
inference(resolution,[status(thm)],[d13,d3]) ).
cnf(d15,plain,
'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','v$ux','v$ux')) = 'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),
inference(demodulation,[status(thm)],[d14,d0]) ).
cnf(d16,plain,
~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))))),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))),
inference(demodulation,[status(thm)],[c1158,c33]) ).
cnf(d17,plain,
~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))))),'c$uNat$uOSuc'('c$uGroups$uOone$u$uclass$uOone'('tc$uNat$uOnat'))),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uNat$uOnat','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))),
inference(demodulation,[status(thm)],[d16,d5]) ).
cnf(d18,plain,
~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal',hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls')))))),'c$uNat$uOSuc'('c$uGroups$uOone$u$uclass$uOone'('tc$uNat$uOnat'))),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),'c$uNat$uOSuc'('c$uGroups$uOone$u$uclass$uOone'('tc$uNat$uOnat')))),
inference(demodulation,[status(thm)],[d17,d5]) ).
cnf(d19,plain,
( ~ 'class$uRings$uOlinordered$u$usemidom'('tc$uRealDef$uOreal')
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')) ),
inference(resolution,[status(thm)],[c307,d18]) ).
cnf(d20,plain,
( ~ 'class$uRings$uOlinordered$u$usemidom'('tc$uRealDef$uOreal')
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','v$ux','v$ux')),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')) ),
inference(demodulation,[status(thm)],[d19,d0]) ).
cnf(d21,plain,
( ~ 'class$uRings$uOlinordered$u$usemidom'('tc$uRealDef$uOreal')
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal',hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uRealDef$uOreal'),'v$ux'),'c$uInt$uOnumber$u$uclass$uOnumber$u$uof'('tc$uRealDef$uOreal','c$uInt$uOBit0'('c$uInt$uOBit1'('c$uInt$uOPls'))))))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')) ),
inference(demodulation,[status(thm)],[d20,d15]) ).
cnf(d22,plain,
( ~ 'class$uRings$uOlinordered$u$usemidom'('tc$uRealDef$uOreal')
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOabs$u$uclass$uOabs'('tc$uRealDef$uOreal','c$uGroups$uOplus$u$uclass$uOplus'('tc$uRealDef$uOreal','v$ux','v$ux')))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')) ),
inference(demodulation,[status(thm)],[d21,d0]) ).
cnf(d23,plain,
( ~ 'class$uRings$uOlinordered$u$usemidom'('tc$uRealDef$uOreal')
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'))
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')) ),
inference(demodulation,[status(thm)],[d22,d15]) ).
cnf(d24,plain,
( ~ 'class$uRings$uOlinordered$u$usemidom'('tc$uRealDef$uOreal')
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')) ),
inference(resolution,[status(thm)],[c31,d23]) ).
cnf(d25,plain,
~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),
inference(resolution,[status(thm)],[c1146,d24]) ).
cnf(d26,plain,
( ~ 'class$uGroups$uOordered$u$uab$u$ugroup$u$uadd$u$uabs'('tc$uRealDef$uOreal')
| 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')) ),
inference(superposition,[status(thm)],[d14,c267]) ).
cnf(d27,plain,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uRealDef$uOreal','c$uGroups$uOzero$u$uclass$uOzero'('tc$uRealDef$uOreal'),'c$uGroups$uOone$u$uclass$uOone'('tc$uRealDef$uOreal')),
inference(resolution,[status(thm)],[c1142,d26]) ).
cnf(d28,plain,
$false,
inference(resolution,[status(thm)],[d27,d25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW194+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n009.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sat Sep 26 15:25:59 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 200.34/29.53 % SZS status Theorem for theBenchmark.p
% 200.34/29.53 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------