%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW252+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:35 AM UTC 2026
% Result : Theorem 157.76s 36.72s
% Output : CNFRefutation 157.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW252+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n007.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sat Sep 26 15:30:10 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 157.76/36.72 % SZS status Theorem for theBenchmark.p
% 157.76/36.72 % SZS output start CNFRefutation for theBenchmark.p
% 157.76/36.72 fof(fact_zero__less__Suc, axiom, ! [X0] : hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),hAPP('c$uNat$uOSuc',X0)))).
% 157.76/36.72 fof(fact_qr, axiom, ! [X0] : hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq')),X0)),hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')))).
% 157.76/36.72 fof(fact_less__zeroE, axiom, ! [X0] : ~hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')))).
% 157.76/36.72 fof(fact_smult__0__left, axiom, ! [X0] : ! [X1] : (('class$uRings$uOcomm$u$usemiring$u$u0'(X1) => 'c$uPolynomial$uOsmult'(X1,'c$uGroups$uOzero$u$uclass$uOzero'(X1),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X1))))).
% 157.76/36.72 fof(fact_smult__eq__0__iff, axiom, ! [X0] : ! [X1] : ! [X2] : (('class$uRings$uOidom'(X2) => ('c$uPolynomial$uOsmult'(X2,X1,X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X2)) <=> (X1 = 'c$uGroups$uOzero$u$uclass$uOzero'(X2) | X0 = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X2))))))).
% 157.76/36.72 fof(fact_poly__0, axiom, ! [X0] : ! [X1] : (('class$uRings$uOcomm$u$usemiring$u$u0'(X1) => hAPP('c$uPolynomial$uOpoly'(X1,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X1))),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'(X1)))).
% 157.76/36.72 fof(fact_gr0__conv__Suc, axiom, ! [X0] : ((hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),X0)) <=> ? [X1] : X0 = hAPP('c$uNat$uOSuc',X1)))).
% 157.76/36.72 fof(fact_poly__smult, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (('class$uRings$uOcomm$u$usemiring$u$u0'(X3) => hAPP('c$uPolynomial$uOpoly'(X3,'c$uPolynomial$uOsmult'(X3,X2,X1)),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X3),X2),hAPP('c$uPolynomial$uOpoly'(X3,X1),X0))))).
% 157.76/36.72 fof(fact_not__less__eq, axiom, ! [X0] : ! [X1] : ((~hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),X1),X0)) <=> hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),X0),hAPP('c$uNat$uOSuc',X1)))))).
% 157.76/36.72 fof(fact_pc0, axiom, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')).
% 157.76/36.72 fof(fact_pqc0, axiom, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc') = hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))).
% 157.76/36.72 fof(fact_degree__def, axiom, ! [X0] : ! [X1] : (('class$uGroups$uOzero'(X1) => 'c$uPolynomial$uOdegree'(X1,X0) = 'c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat',X1,'tc$uHOL$uObool',hAPP('c$uCOMBB'(X1,'tc$ufun'(X1,'tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'(X1,X0)),'c$uGroups$uOzero$u$uclass$uOzero'(X1)))))))).
% 157.76/36.72 fof(fact_degree__smult__eq, axiom, ! [X0] : ! [X1] : ! [X2] : (('class$uRings$uOidom'(X2) => ((X1 = 'c$uGroups$uOzero$u$uclass$uOzero'(X2) => 'c$uPolynomial$uOdegree'(X2,'c$uPolynomial$uOsmult'(X2,X1,X0)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) & (X1 != 'c$uGroups$uOzero$u$uclass$uOzero'(X2) => 'c$uPolynomial$uOdegree'(X2,'c$uPolynomial$uOsmult'(X2,X1,X0)) = 'c$uPolynomial$uOdegree'(X2,X0)))))).
% 157.76/36.72 fof(arity_Complex__Ocomplex__Rings_Ocomm__semiring__0, axiom, 'class$uRings$uOcomm$u$usemiring$u$u0'('tc$uComplex$uOcomplex')).
% 157.76/36.72 fof(arity_Complex__Ocomplex__Groups_Ozero, axiom, 'class$uGroups$uOzero'('tc$uComplex$uOcomplex')).
% 157.76/36.72 fof(arity_Complex__Ocomplex__Rings_Oidom, axiom, 'class$uRings$uOidom'('tc$uComplex$uOcomplex')).
% 157.76/36.72 fof(conj_0, conjecture, (('c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) => ('v$uq' != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) => hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','v$uq')),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')))))) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))) & ('c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) => (('v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) => 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat') = hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))))))) & ('v$uq' != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) => hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','v$uq')),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')))))) = hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))))))))))).
% 157.76/36.72 fof(negated_conjecture, negated_conjecture, ~((('c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) => ('v$uq' != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) => hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','v$uq')),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')))))) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))) & ('c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) => (('v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) => 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat') = hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))))))) & ('v$uq' != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) => hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','v$uq')),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')))))) = hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))))))))))), inference(negate_conjecture, [status(cth)], [conj_0])).
% 157.76/36.72 cnf(c4, plain, hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),hAPP('c$uNat$uOSuc',X0))), inference(clausification, [status(esa)], [fact_zero__less__Suc])).
% 157.76/36.72 cnf(c5, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq')),X0)),hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))), inference(clausification, [status(esa)], [fact_qr])).
% 157.76/36.72 cnf(c8, plain, ~hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))), inference(clausification, [status(esa)], [fact_less__zeroE])).
% 157.76/36.72 cnf(c11, plain, ~'class$uRings$uOcomm$u$usemiring$u$u0'(X0) | 'c$uPolynomial$uOsmult'(X0,'c$uGroups$uOzero$u$uclass$uOzero'(X0),X1) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0)), inference(clausification, [status(esa)], [fact_smult__0__left])).
% 157.76/36.72 cnf(c12, plain, ~'class$uRings$uOidom'(X0) | 'c$uPolynomial$uOsmult'(X0,X1,X2) != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0)) | X1 = 'c$uGroups$uOzero$u$uclass$uOzero'(X0) | X2 = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0)), inference(clausification, [status(esa)], [fact_smult__eq__0__iff])).
% 157.76/36.72 cnf(c15, plain, ~'class$uRings$uOcomm$u$usemiring$u$u0'(X0) | hAPP('c$uPolynomial$uOpoly'(X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0))),X1) = 'c$uGroups$uOzero$u$uclass$uOzero'(X0), inference(clausification, [status(esa)], [fact_poly__0])).
% 157.76/36.72 cnf(c16, plain, ~hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')),X0)) | X0 = hAPP('c$uNat$uOSuc',sK21(X0)), inference(clausification, [status(esa)], [fact_gr0__conv__Suc])).
% 157.76/36.72 cnf(c25, plain, ~'class$uRings$uOcomm$u$usemiring$u$u0'(X0) | hAPP('c$uPolynomial$uOpoly'(X0,'c$uPolynomial$uOsmult'(X0,X1,X2)),X3) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),X1),hAPP('c$uPolynomial$uOpoly'(X0,X2),X3)), inference(clausification, [status(esa)], [fact_poly__smult])).
% 157.76/36.72 cnf(c78, plain, hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),X0),X1)) | hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),X1),hAPP('c$uNat$uOSuc',X0))), inference(clausification, [status(esa)], [fact_not__less__eq])).
% 157.76/36.72 cnf(c89, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'), inference(clausification, [status(esa)], [fact_pc0])).
% 157.76/36.72 cnf(c132, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc') = hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')), inference(clausification, [status(esa)], [fact_pqc0])).
% 157.76/36.72 cnf(c275, plain, ~'class$uGroups$uOzero'(X0) | 'c$uPolynomial$uOdegree'(X0,X1) = 'c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat',X0,'tc$uHOL$uObool',hAPP('c$uCOMBB'(X0,'tc$ufun'(X0,'tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'(X0,X1)),'c$uGroups$uOzero$u$uclass$uOzero'(X0))))), inference(clausification, [status(esa)], [fact_degree__def])).
% 157.76/36.72 cnf(c350, plain, ~'class$uRings$uOidom'(X0) | X1 = 'c$uGroups$uOzero$u$uclass$uOzero'(X0) | 'c$uPolynomial$uOdegree'(X0,'c$uPolynomial$uOsmult'(X0,X1,X2)) = 'c$uPolynomial$uOdegree'(X0,X2), inference(clausification, [status(esa)], [fact_degree__smult__eq])).
% 157.76/36.72 cnf(c1166, plain, 'class$uRings$uOcomm$u$usemiring$u$u0'('tc$uComplex$uOcomplex'), inference(clausification, [status(esa)], [arity_Complex__Ocomplex__Rings_Ocomm__semiring__0])).
% 157.76/36.72 cnf(c1172, plain, 'class$uGroups$uOzero'('tc$uComplex$uOcomplex'), inference(clausification, [status(esa)], [arity_Complex__Ocomplex__Groups_Ozero])).
% 157.76/36.72 cnf(c1173, plain, 'class$uRings$uOidom'('tc$uComplex$uOcomplex'), inference(clausification, [status(esa)], [arity_Complex__Ocomplex__Rings_Oidom])).
% 157.76/36.72 cnf(c1209, plain, 'c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | ~X0, inference(clausification, [status(esa)], [negated_conjecture])).
% 157.76/36.72 cnf(c1212, plain, X0 | 'c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')), inference(clausification, [status(esa)], [negated_conjecture])).
% 157.76/36.72 cnf(c1214, plain, X0 | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','v$uq')),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')))))) != hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))),'v$uq'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')))))), inference(clausification, [status(esa)], [negated_conjecture])).
% 157.76/36.72 cnf(d0, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'), inference(resolution, [status(thm)], [c1166,c15])).
% 157.76/36.72 cnf(d1, plain, 'c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')), inference(resolution, [status(thm)], [c1166,c11])).
% 157.76/36.72 cnf(d2, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex',X0,X1)),X2) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),X0),hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex',X1),X2)), inference(resolution, [status(thm)], [c1166,c25])).
% 157.76/36.72 cnf(d3, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')),'v$uq')),X0)),hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))), inference(demodulation, [status(thm)], [c5,c132])).
% 157.76/36.72 cnf(d4, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),X0) = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uComplex$uOcomplex'),hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')),'v$uq')),X0)),hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')), inference(demodulation, [status(thm)], [d3,c132])).
% 157.76/36.72 cnf(d5, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),X0) = hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')),'v$uq')),X0),'v$upa')),'v$uc'), inference(demodulation, [status(thm)], [d4,d2])).
% 157.76/36.72 cnf(d6, plain, 'c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')),'v$uq') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | ~'Ts2156', inference(demodulation, [status(thm)], [c1209,c132])).
% 157.76/36.72 cnf(d7, plain, 'c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')),'v$uq') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'Ts2156', inference(demodulation, [status(thm)], [c1212,c132])).
% 157.76/36.72 cnf(d8, plain, 'c$uPolynomial$uOdegree'('tc$uComplex$uOcomplex',X0) = 'c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex',X0)),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'))))), inference(resolution, [status(thm)], [c275,c1172])).
% 157.76/36.72 cnf(d9, plain, hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','v$uq')),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')))))) != hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')),'v$uq'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')))))) | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'Ts2156', inference(demodulation, [status(thm)], [c1214,c132])).
% 157.76/36.72 cnf(d10, plain, hAPP('c$uNat$uOSuc','c$uPolynomial$uOdegree'('tc$uComplex$uOcomplex','v$uq')) != hAPP('c$uNat$uOSuc','c$uOrderings$uOord$u$uclass$uOLeast'('tc$uNat$uOnat',hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$uHOL$uObool','tc$uNat$uOnat','c$uHOL$uOAll'('tc$uNat$uOnat')),'c$uCOMBC'('tc$uNat$uOnat','tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$ufun'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBS'('tc$uNat$uOnat','tc$uHOL$uObool','tc$uHOL$uObool')),hAPP('c$uCOMBB'('tc$ufun'('tc$uNat$uOnat','tc$uHOL$uObool'),'tc$ufun'('tc$uNat$uOnat','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool')),'tc$uNat$uOnat','c$uCOMBB'('tc$uHOL$uObool','tc$ufun'('tc$uHOL$uObool','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufimplies')),'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'))),'c$uCOMBC'('tc$uNat$uOnat','tc$uComplex$uOcomplex','tc$uHOL$uObool',hAPP('c$uCOMBB'('tc$uComplex$uOcomplex','tc$ufun'('tc$uComplex$uOcomplex','tc$uHOL$uObool'),'tc$uNat$uOnat','c$ufequal'),'c$uPolynomial$uOcoeff'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')),'v$uq'))),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')))))) | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'Ts2156', inference(demodulation, [status(thm)], [d9,d8])).
% 157.76/36.72 cnf(d11, plain, hAPP('c$uNat$uOSuc','c$uPolynomial$uOdegree'('tc$uComplex$uOcomplex','v$uq')) != hAPP('c$uNat$uOSuc','c$uPolynomial$uOdegree'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')),'v$uq'))) | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'Ts2156', inference(demodulation, [status(thm)], [d10,d8])).
% 157.76/36.72 cnf(d12, plain, X0 = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') | 'c$uPolynomial$uOdegree'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex',X0,X1)) = 'c$uPolynomial$uOdegree'('tc$uComplex$uOcomplex',X1), inference(resolution, [status(thm)], [c350,c1173])).
% 157.76/36.72 cnf(d13, plain, hAPP('c$uNat$uOSuc','c$uPolynomial$uOdegree'('tc$uComplex$uOcomplex','v$uq')) != hAPP('c$uNat$uOSuc','c$uPolynomial$uOdegree'('tc$uComplex$uOcomplex','v$uq')) | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'Ts2156' | 'c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'), inference(superposition, [status(thm)], [d12,d11])).
% 157.76/36.72 cnf(d14, plain, hAPP('c$uNat$uOSuc',X0) = hAPP('c$uNat$uOSuc',sK21(hAPP('c$uNat$uOSuc',X0))), inference(resolution, [status(thm)], [c16,c4])).
% 157.76/36.72 cnf(d15, plain, hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))) | hAPP('c$uNat$uOSuc',X0) = hAPP('c$uNat$uOSuc',sK21(hAPP('c$uNat$uOSuc',X0))), inference(resolution, [status(thm)], [c78,c16])).
% 157.76/36.72 cnf(d16, plain, hAPP('c$uNat$uOSuc',X0) = hAPP('c$uNat$uOSuc',X0) | hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat'),X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'))), inference(demodulation, [status(thm)], [d15,d14])).
% 157.76/36.72 cnf(d17, plain, hAPP('c$uNat$uOSuc',X0) = hAPP('c$uNat$uOSuc',X0), inference(resolution, [status(thm)], [c8,d16])).
% 157.76/36.72 cnf(d18, plain, 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') | 'Ts2156', inference(resolution, [status(thm)], [d17,d13])).
% 157.76/36.72 cnf(d19, plain, 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') | 'c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')),'v$uq') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')), inference(resolution, [status(thm)], [d18,d6])).
% 157.76/36.72 cnf(d20, plain, 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') | ~'class$uRings$uOidom'('tc$uComplex$uOcomplex') | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'), inference(superposition, [status(thm)], [d19,c12])).
% 157.76/36.72 cnf(d21, plain, 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'), inference(resolution, [status(thm)], [c1173,d20])).
% 157.76/36.72 cnf(d22, plain, 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'), inference(equality_resolution, [status(thm)], [d21])).
% 157.76/36.72 cnf(d23, plain, 'c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),'v$uq') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'Ts2156' | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')), inference(superposition, [status(thm)], [d22,d7])).
% 157.76/36.72 cnf(d24, plain, 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'Ts2156', inference(demodulation, [status(thm)], [d23,d1])).
% 157.76/36.72 cnf(d25, plain, 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'Ts2156', inference(equality_resolution, [status(thm)], [d24])).
% 157.76/36.72 cnf(d26, plain, 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) | 'c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uRings$uOinverse$u$uclass$uOinverse'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc')),'v$uq') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')), inference(resolution, [status(thm)], [d25,d6])).
% 157.76/36.72 cnf(d27, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),X0) = hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex',hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))),X0),'v$upa')),'v$uc') | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')), inference(superposition, [status(thm)], [d26,d5])).
% 157.76/36.72 cnf(d28, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),X0) = hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uPolynomial$uOsmult'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),'v$upa')),'v$uc') | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')), inference(demodulation, [status(thm)], [d27,d0])).
% 157.76/36.72 cnf(d29, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),X0) = hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))),'v$uc') | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')), inference(demodulation, [status(thm)], [d28,d1])).
% 157.76/36.72 cnf(d30, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')), inference(demodulation, [status(thm)], [d29,d0])).
% 157.76/36.72 cnf(d31, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') | 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')), inference(superposition, [status(thm)], [d30,c132])).
% 157.76/36.72 cnf(d32, plain, 'v$uq' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')), inference(resolution, [status(thm)], [c89,d31])).
% 157.76/36.72 cnf(d33, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$uq'),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'), inference(demodulation, [status(thm)], [d0,d32])).
% 157.76/36.72 cnf(d34, plain, hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$uc') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'), inference(demodulation, [status(thm)], [c132,d33])).
% 157.76/36.72 cnf(d35, plain, $false, inference(resolution, [status(thm)], [c89,d34])).
% 157.76/36.72 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------