%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW245+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 : n007.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:34 AM UTC 2026
% Result : Theorem 67.63s 15.39s
% Output : CNFRefutation 67.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 5
% Syntax : Number of formulae : 50 ( 11 unt; 0 def)
% Number of atoms : 153 ( 137 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 170 ( 67 ~; 79 |; 12 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 10 con; 0-4 aty)
% Number of variables : 30 ( 1 sgn 5 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact__096c_A_126_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096,axiom,
( 'class$uRings$uOidom'('t$ua')
=> ( 'v$uc' != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
=> ? [X0,X1] :
( ? [X2] :
( ! [X3] : hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),X3) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),X3),X0)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X1,X2)),X3))
& ( 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
=> 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(X2,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',X2))),X0)) = 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs'))) )
& ( 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
=> 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(X2,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',X2))),X0)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat') ) )
& X1 != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') ) ) ) ).
fof(fact__096c_A_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096,axiom,
( 'class$uRings$uOidom'('t$ua')
=> ( 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
=> ? [X0,X1] :
( ? [X2] :
( ! [X3] : hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),X3) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),X3),X0)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X1,X2)),X3))
& ( 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
=> 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(X2,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',X2))),X0)) = 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs'))) )
& ( 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
=> 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(X2,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',X2))),X0)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat') ) )
& X1 != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') ) ) ) ).
fof(fact_Suc__not__Zero,axiom,
! [X0] : 'c$uNat$uOSuc'(X0) != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat') ).
fof(tfree_0,hypothesis,
'class$uRings$uOidom'('t$ua') ).
fof(conj_0,conjecture,
? [X0,X1] :
( ? [X2] :
( ! [X3] : hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),X3) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),X3),X0)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X1,X2)),X3))
& ( 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
=> 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(X2,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',X2))),X0)) = 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs'))) )
& ( 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
=> 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(X2,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',X2))),X0)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat') ) )
& X1 != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1] :
( ? [X2] :
( ! [X3] : hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),X3) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),X3),X0)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X1,X2)),X3))
& ( 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
=> 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(X2,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',X2))),X0)) = 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs'))) )
& ( 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
=> 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(X2,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',X2))),X0)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat') ) )
& X1 != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') ),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c3,plain,
( sK5 != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| ~ 'class$uRings$uOidom'('t$ua') ),
inference(clausification,[status(esa)],[fact__096c_A_126_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096]) ).
cnf(c4,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK6,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK6))),sK4)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| ~ 'class$uRings$uOidom'('t$ua') ),
inference(clausification,[status(esa)],[fact__096c_A_126_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096]) ).
cnf(c5,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK6,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK6))),sK4)) = 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| ~ 'class$uRings$uOidom'('t$ua') ),
inference(clausification,[status(esa)],[fact__096c_A_126_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096]) ).
cnf(c6,plain,
( hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),X0),sK4)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',sK5,sK6)),X0))
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| ~ 'class$uRings$uOidom'('t$ua') ),
inference(clausification,[status(esa)],[fact__096c_A_126_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096]) ).
cnf(c7,plain,
( sK9 != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'v$uc' != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| ~ 'class$uRings$uOidom'('t$ua') ),
inference(clausification,[status(esa)],[fact__096c_A_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096]) ).
cnf(c8,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK10,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK10))),sK8)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| 'v$uc' != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| ~ 'class$uRings$uOidom'('t$ua') ),
inference(clausification,[status(esa)],[fact__096c_A_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096]) ).
cnf(c9,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK10,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK10))),sK8)) = 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| 'v$uc' != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| ~ 'class$uRings$uOidom'('t$ua') ),
inference(clausification,[status(esa)],[fact__096c_A_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096]) ).
cnf(c10,plain,
( hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),X0),sK8)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',sK9,sK10)),X0))
| 'v$uc' != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| ~ 'class$uRings$uOidom'('t$ua') ),
inference(clausification,[status(esa)],[fact__096c_A_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096]) ).
cnf(c112,plain,
'c$uNat$uOSuc'(X0) != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),
inference(clausification,[status(esa)],[fact_Suc__not__Zero]) ).
cnf(c802,plain,
'class$uRings$uOidom'('t$ua'),
inference(clausification,[status(esa)],[tfree_0]) ).
cnf(c804,plain,
( hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(X2,X0,X1)) != hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),sK1474(X2,X0,X1)),X2)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X0,X1)),sK1474(X2,X0,X1)))
| 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(X1,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',X1))),X2)) != 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| X0 = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( sK5 != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') ),
inference(resolution,[status(thm)],[c802,c3]) ).
cnf(d1,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK6,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK6))),sK4)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(resolution,[status(thm)],[c802,c4]) ).
cnf(d2,plain,
( 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(resolution,[status(thm)],[c112,d1]) ).
cnf(d3,plain,
( 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),X0),sK4)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',sK5,sK6)),X0)) ),
inference(resolution,[status(thm)],[c802,c6]) ).
cnf(d4,plain,
( 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK6,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK6))),sK4)) != 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| sK5 = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(sK4,sK5,sK6)) != hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(sK4,sK5,sK6)) ),
inference(superposition,[status(thm)],[d3,c804]) ).
cnf(d5,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK6,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK6))),sK4)) = 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(resolution,[status(thm)],[c802,c5]) ).
cnf(d6,plain,
( 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| sK5 = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(sK4,sK5,sK6)) != hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(sK4,sK5,sK6))
| 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs'))) != 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs'))) ),
inference(superposition,[status(thm)],[d5,d4]) ).
cnf(d7,plain,
( 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs'))) != 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| sK5 = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(equality_resolution,[status(thm)],[d6]) ).
cnf(d8,plain,
( sK5 = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(equality_resolution,[status(thm)],[d7]) ).
cnf(d9,plain,
( sK5 = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(superposition,[status(thm)],[d8,d2]) ).
cnf(d10,plain,
( sK5 = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') ),
inference(equality_resolution,[status(thm)],[d9]) ).
cnf(d11,plain,
( 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| sK5 != sK5 ),
inference(superposition,[status(thm)],[d10,d0]) ).
cnf(d12,plain,
'v$uc' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua'),
inference(equality_resolution,[status(thm)],[d11]) ).
cnf(d13,plain,
( ~ 'class$uRings$uOidom'('t$ua')
| 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK10,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK10))),sK8)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')
| 'v$uc' != 'v$uc'
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(demodulation,[status(thm)],[c8,d12]) ).
cnf(d14,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK10,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK10))),sK8)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')
| 'v$uc' != 'v$uc'
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(resolution,[status(thm)],[c802,d13]) ).
cnf(d15,plain,
( 'v$uc' != 'v$uc'
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(resolution,[status(thm)],[c112,d14]) ).
cnf(d16,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(X2,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',X2))),X1)) != 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(X1,X0,X2)) != hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),sK1474(X1,X0,X2)),X1)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X0,X2)),sK1474(X1,X0,X2)))
| X0 = 'v$uc' ),
inference(demodulation,[status(thm)],[c804,d12]) ).
cnf(d17,plain,
( ~ 'class$uRings$uOidom'('t$ua')
| 'v$uc' != 'v$uc'
| hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),X0),sK8)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',sK9,sK10)),X0)) ),
inference(demodulation,[status(thm)],[c10,d12]) ).
cnf(d18,plain,
( 'v$uc' != 'v$uc'
| hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),X0),sK8)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',sK9,sK10)),X0)) ),
inference(resolution,[status(thm)],[c802,d17]) ).
cnf(d19,plain,
hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('t$ua'),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('t$ua'),X0),sK8)),hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',sK9,sK10)),X0)),
inference(equality_resolution,[status(thm)],[d18]) ).
cnf(d20,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK10,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK10))),sK8)) != 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| sK9 = 'v$uc'
| hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(sK8,sK9,sK10)) != hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(sK8,sK9,sK10)) ),
inference(superposition,[status(thm)],[d19,d16]) ).
cnf(d21,plain,
( sK9 != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua')
| 'v$uc' != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') ),
inference(resolution,[status(thm)],[c802,c7]) ).
cnf(d22,plain,
sK9 != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua'),
inference(resolution,[status(thm)],[d12,d21]) ).
cnf(d23,plain,
sK9 != 'v$uc',
inference(demodulation,[status(thm)],[d22,d12]) ).
cnf(d24,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK10,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK10))),sK8)) != 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(sK8,sK9,sK10)) != hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(sK8,sK9,sK10)) ),
inference(resolution,[status(thm)],[d23,d20]) ).
cnf(d25,plain,
( ~ 'class$uRings$uOidom'('t$ua')
| 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK10,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK10))),sK8)) = 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'v$uc' != 'v$uc'
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(demodulation,[status(thm)],[c9,d12]) ).
cnf(d26,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK10,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK10))),sK8)) = 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'v$uc' != 'v$uc'
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(resolution,[status(thm)],[c802,d25]) ).
cnf(d27,plain,
( 'c$uNat$uOSuc'('c$uGroups$uOplus$u$uclass$uOplus'('tc$uNat$uOnat','c$uIf'('tc$uNat$uOnat','c$ufequal'(sK10,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua',sK10))),sK8)) = 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(equality_resolution,[status(thm)],[d26]) ).
cnf(d28,plain,
( 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(sK8,sK9,sK10)) != hAPP('c$uPolynomial$uOpoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')),sK1474(sK8,sK9,sK10))
| 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs'))) != 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs'))) ),
inference(superposition,[status(thm)],[d27,d24]) ).
cnf(d29,plain,
( 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs'))) != 'c$uNat$uOSuc'('c$uPolynomial$uOdegree'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs')))
| 'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(equality_resolution,[status(thm)],[d28]) ).
cnf(d30,plain,
'c$uPolynomial$uOpCons'('t$ua','v$uc','v$ucs') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),
inference(equality_resolution,[status(thm)],[d29]) ).
cnf(d31,plain,
'v$uc' != 'v$uc',
inference(resolution,[status(thm)],[d30,d15]) ).
cnf(d32,plain,
$false,
inference(equality_resolution,[status(thm)],[d31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW245+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.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 15:29:39 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 67.63/15.39 % SZS status Theorem for theBenchmark.p
% 67.63/15.39 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------