%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW256+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 : n006.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:35 AM UTC 2026
% Result : Theorem 76.12s 11.61s
% Output : CNFRefutation 76.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 16
% Syntax : Number of formulae : 101 ( 56 unt; 0 def)
% Number of atoms : 146 ( 102 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 83 ( 38 ~; 33 |; 0 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-3 aty)
% Number of variables : 165 ( 53 sgn 35 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_ext,axiom,
! [X0,X1] :
( ! [X2] : hAPP(X1,X2) = hAPP(X0,X2)
=> X1 = X0 ) ).
fof(fact_kas_I2_J,axiom,
'v$uk' != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat') ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I35_J,axiom,
! [X0,X1,X2] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X2)
=> hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X2),X1),'c$uNat$uOSuc'(X0)) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X2),X1),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X2),X1),X0)) ) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I28_J,axiom,
! [X0,X1,X2] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X2)
=> hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X2),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X2),X1),X0)),X1) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X2),X1),'c$uNat$uOSuc'(X0)) ) ).
fof(fact_mult__0,axiom,
! [X0] : hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uNat$uOnat'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat') ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,axiom,
! [X0,X1,X2,X3] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X3)
=> hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X3),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X3),X2),X1)),X0) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X3),X2),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uNat$uOnat'),X1),X0)) ) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,axiom,
! [X0,X1,X2] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X2)
=> hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X2),X1),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X2),X0),X1) ) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J,axiom,
! [X0,X1] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X1)
=> hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X1),X0),'c$uGroups$uOzero$u$uclass$uOzero'(X1)) = 'c$uGroups$uOzero$u$uclass$uOzero'(X1) ) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J,axiom,
! [X0,X1] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X1)
=> hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X1),'c$uGroups$uOzero$u$uclass$uOzero'(X1)),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'(X1) ) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I2_J,axiom,
! [X0,X1,X2] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X2)
=> 'c$uGroups$uOplus$u$uclass$uOplus'(X2,hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X2),X1),X0),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X2),'c$uGroups$uOplus$u$uclass$uOplus'(X2,X1,'c$uGroups$uOone$u$uclass$uOone'(X2))),X0) ) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I3_J,axiom,
! [X0,X1,X2] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X2)
=> 'c$uGroups$uOplus$u$uclass$uOplus'(X2,X1,hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X2),X0),X1)) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X2),'c$uGroups$uOplus$u$uclass$uOplus'(X2,X0,'c$uGroups$uOone$u$uclass$uOone'(X2))),X1) ) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,axiom,
! [X0,X1,X2,X3] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X3)
=> 'c$uGroups$uOplus$u$uclass$uOplus'(X3,'c$uGroups$uOplus$u$uclass$uOplus'(X3,X2,X1),X0) = 'c$uGroups$uOplus$u$uclass$uOplus'(X3,X2,'c$uGroups$uOplus$u$uclass$uOplus'(X3,X1,X0)) ) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I6_J,axiom,
! [X0,X1] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X1)
=> 'c$uGroups$uOplus$u$uclass$uOplus'(X1,X0,'c$uGroups$uOzero$u$uclass$uOzero'(X1)) = X0 ) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J,axiom,
! [X0,X1] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X1)
=> hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X1),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) = 'c$uGroups$uOone$u$uclass$uOone'(X1) ) ).
fof(arity_Complex__Ocomplex__Rings_Ocomm__semiring__1,axiom,
'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex') ).
fof(conj_0,conjecture,
? [X0,X1] : hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) != hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X1),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1] : hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) != hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X1),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c0,plain,
( X0 = X1
| hAPP(X0,sK2(X1,X0)) != hAPP(X1,sK2(X1,X0)) ),
inference(clausification,[status(esa)],[fact_ext]) ).
cnf(c1,plain,
'v$uk' != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),
inference(clausification,[status(esa)],[fact_kas_I2_J]) ).
cnf(c2,plain,
( hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),X1),'c$uNat$uOSuc'(X2)) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),X1),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),X1),X2))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I35_J]) ).
cnf(c4,plain,
( hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),X1),X2)),X1) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),X1),'c$uNat$uOSuc'(X2))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I28_J]) ).
cnf(c19,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uNat$uOnat'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),
inference(clausification,[status(esa)],[fact_mult__0]) ).
cnf(c20,plain,
( hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),X1),X2)),X3) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),X1),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uNat$uOnat'),X2),X3))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J]) ).
cnf(c39,plain,
( hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),X1),X2) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),X2),X1)
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J]) ).
cnf(c46,plain,
( hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),X1),'c$uGroups$uOzero$u$uclass$uOzero'(X0)) = 'c$uGroups$uOzero$u$uclass$uOzero'(X0)
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J]) ).
cnf(c47,plain,
( hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),'c$uGroups$uOzero$u$uclass$uOzero'(X0)),X1) = 'c$uGroups$uOzero$u$uclass$uOzero'(X0)
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J]) ).
cnf(c77,plain,
( 'c$uGroups$uOplus$u$uclass$uOplus'(X0,hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),X1),X2),X2) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),'c$uGroups$uOplus$u$uclass$uOplus'(X0,X1,'c$uGroups$uOone$u$uclass$uOone'(X0))),X2)
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I2_J]) ).
cnf(c78,plain,
( 'c$uGroups$uOplus$u$uclass$uOplus'(X0,X1,hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),X2),X1)) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),'c$uGroups$uOplus$u$uclass$uOplus'(X0,X2,'c$uGroups$uOone$u$uclass$uOone'(X0))),X1)
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I3_J]) ).
cnf(c111,plain,
( 'c$uGroups$uOplus$u$uclass$uOplus'(X0,'c$uGroups$uOplus$u$uclass$uOplus'(X0,X1,X2),X3) = 'c$uGroups$uOplus$u$uclass$uOplus'(X0,X1,'c$uGroups$uOplus$u$uclass$uOplus'(X0,X2,X3))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J]) ).
cnf(c194,plain,
( 'c$uGroups$uOplus$u$uclass$uOplus'(X0,X1,'c$uGroups$uOzero$u$uclass$uOzero'(X0)) = X1
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I6_J]) ).
cnf(c305,plain,
( hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'(X0),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) = 'c$uGroups$uOone$u$uclass$uOone'(X0)
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J]) ).
cnf(c600,plain,
'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[arity_Complex__Ocomplex__Rings_Ocomm__semiring__1]) ).
cnf(c602,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X1),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X1),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) ),
inference(superposition,[status(thm)],[c2,c602]) ).
cnf(d1,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))),
inference(resolution,[status(thm)],[c600,d0]) ).
cnf(d2,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X2),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X2),'c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))),
inference(superposition,[status(thm)],[d1,c602]) ).
cnf(d3,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X2),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))),
inference(superposition,[status(thm)],[d1,d1]) ).
cnf(d4,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X2),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uNat$uOnat'),X1),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))) ),
inference(superposition,[status(thm)],[c20,d3]) ).
cnf(d5,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uNat$uOnat'),X2),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))),
inference(resolution,[status(thm)],[c600,d4]) ).
cnf(d6,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),
inference(superposition,[status(thm)],[c19,d5]) ).
cnf(d7,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X2),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X2),'c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))))),
inference(superposition,[status(thm)],[d6,d2]) ).
cnf(d8,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(superposition,[status(thm)],[c47,d7]) ).
cnf(d9,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[c600,d8]) ).
cnf(d10,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X2),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),
inference(superposition,[status(thm)],[d6,d6]) ).
cnf(d11,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),X0) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))) ),
inference(superposition,[status(thm)],[d10,c4]) ).
cnf(d12,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),X1) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),
inference(resolution,[status(thm)],[c600,d11]) ).
cnf(d13,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),X1) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),
inference(demodulation,[status(thm)],[d12,d9]) ).
cnf(d14,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))),X0) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uNat$uOSuc'('c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))) ),
inference(superposition,[status(thm)],[d3,c4]) ).
cnf(d15,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))),X1) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))),
inference(resolution,[status(thm)],[c600,d14]) ).
cnf(d16,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),X2) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X2),'c$uNat$uOSuc'('c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))),
inference(superposition,[status(thm)],[d6,d15]) ).
cnf(d17,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))),
inference(demodulation,[status(thm)],[d16,d12]) ).
cnf(d18,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uNat$uOSuc'('c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))) ),
inference(superposition,[status(thm)],[d3,c2]) ).
cnf(d19,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uNat$uOSuc'('c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))),
inference(resolution,[status(thm)],[c600,d18]) ).
cnf(d20,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X2),'c$uNat$uOSuc'('c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X2),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),
inference(superposition,[status(thm)],[d6,d19]) ).
cnf(d21,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),
inference(demodulation,[status(thm)],[d20,d17]) ).
cnf(d22,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),
inference(demodulation,[status(thm)],[d21,d9]) ).
cnf(d23,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),
inference(superposition,[status(thm)],[d22,d13]) ).
cnf(d24,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')) ),
inference(superposition,[status(thm)],[c47,d23]) ).
cnf(d25,plain,
'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),
inference(resolution,[status(thm)],[c600,d24]) ).
cnf(d26,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(superposition,[status(thm)],[c305,d9]) ).
cnf(d27,plain,
'c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[c600,d26]) ).
cnf(d28,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),X2) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uNat$uOnat'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),X2)) ),
inference(superposition,[status(thm)],[d10,c20]) ).
cnf(d29,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),X0) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X2),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) ),
inference(demodulation,[status(thm)],[d28,c19]) ).
cnf(d30,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),X1) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X2),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),
inference(resolution,[status(thm)],[c600,d29]) ).
cnf(d31,plain,
hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X3),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),X2),
inference(superposition,[status(thm)],[d30,d10]) ).
cnf(d32,plain,
'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),X2),
inference(demodulation,[status(thm)],[d31,d9]) ).
cnf(d33,plain,
'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),X1),
inference(demodulation,[status(thm)],[d32,d9]) ).
cnf(d34,plain,
( X0 = hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))
| hAPP(X0,sK2(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),X0)) != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(superposition,[status(thm)],[d33,c0]) ).
cnf(d35,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),
inference(demodulation,[status(thm)],[d23,d25]) ).
cnf(d36,plain,
( hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')) = hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(superposition,[status(thm)],[d35,d34]) ).
cnf(d37,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X1),'c$uNat$uOSuc'('c$uGroups$uOminus$u$uclass$uOminus'('tc$uNat$uOnat','v$uk','c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))))),X2) = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),X2),'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),
inference(superposition,[status(thm)],[d6,d12]) ).
cnf(d38,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))) ),
inference(superposition,[status(thm)],[c46,d37]) ).
cnf(d39,plain,
'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))),
inference(resolution,[status(thm)],[c600,d38]) ).
cnf(d40,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),'c$uNat$uOSuc'('c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))) ),
inference(superposition,[status(thm)],[c46,d12]) ).
cnf(d41,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(demodulation,[status(thm)],[d40,d39]) ).
cnf(d42,plain,
'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[c600,d41]) ).
cnf(d43,plain,
hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')) = hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),
inference(resolution,[status(thm)],[d42,d36]) ).
cnf(d44,plain,
'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),X0),
inference(demodulation,[status(thm)],[d33,d43]) ).
cnf(d45,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),'c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'))),X0) ),
inference(superposition,[status(thm)],[d44,c77]) ).
cnf(d46,plain,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),'c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'))),X0),
inference(resolution,[status(thm)],[c600,d45]) ).
cnf(d47,plain,
'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),
inference(superposition,[status(thm)],[d46,d25]) ).
cnf(d48,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),X0)) ),
inference(superposition,[status(thm)],[c78,d46]) ).
cnf(d49,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')) ),
inference(demodulation,[status(thm)],[d48,d35]) ).
cnf(d50,plain,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),
inference(resolution,[status(thm)],[c600,d49]) ).
cnf(d51,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,X1)) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X1,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))) ),
inference(superposition,[status(thm)],[c111,d50]) ).
cnf(d52,plain,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,X1)) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X1,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),
inference(resolution,[status(thm)],[c600,d51]) ).
cnf(d53,plain,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),
inference(superposition,[status(thm)],[d47,d52]) ).
cnf(d54,plain,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),
inference(superposition,[status(thm)],[d53,d52]) ).
cnf(d55,plain,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),
inference(demodulation,[status(thm)],[d54,d47]) ).
cnf(d56,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| X0 = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')) ),
inference(superposition,[status(thm)],[c194,d55]) ).
cnf(d57,plain,
X0 = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),
inference(resolution,[status(thm)],[c600,d56]) ).
cnf(d58,plain,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')),
inference(demodulation,[status(thm)],[d53,d57]) ).
cnf(d59,plain,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0) = X0,
inference(demodulation,[status(thm)],[d58,d57]) ).
cnf(d60,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex')
| hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),'c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'))) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0) ),
inference(superposition,[status(thm)],[d46,c39]) ).
cnf(d61,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),'c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'))) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0),
inference(resolution,[status(thm)],[c600,d60]) ).
cnf(d62,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex')) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0),
inference(demodulation,[status(thm)],[d61,d59]) ).
cnf(d63,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex')) = X0,
inference(demodulation,[status(thm)],[d62,d59]) ).
cnf(d64,plain,
hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')) = X0,
inference(demodulation,[status(thm)],[d63,d27]) ).
cnf(d65,plain,
'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = X0,
inference(superposition,[status(thm)],[d64,d25]) ).
cnf(d66,plain,
X0 = X1,
inference(superposition,[status(thm)],[d65,d65]) ).
cnf(d67,plain,
$false,
inference(resolution,[status(thm)],[d66,c1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW256+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n006.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Sat Sep 26 15:32:41 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 76.12/11.61 % SZS status Theorem for theBenchmark.p
% 76.12/11.61 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------