%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW186+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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:11:29 AM UTC 2026
% Result : Theorem 171.10s 30.75s
% Output : CNFRefutation 171.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 20
% Syntax : Number of formulae : 83 ( 46 unt; 0 def)
% Number of atoms : 125 ( 76 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 73 ( 31 ~; 24 |; 2 &)
% ( 3 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-3 aty)
% Number of variables : 102 ( 17 sgn 31 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_offset__poly__0,axiom,
! [X0,X1] :
( 'class$uRings$uOcomm$u$usemiring$u$u0'(X1)
=> 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'(X1,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X1)),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X1)) ) ).
fof(fact_offset__poly__pCons,axiom,
! [X0,X1,X2,X3] :
( 'class$uRings$uOcomm$u$usemiring$u$u0'(X3)
=> 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'(X3,'c$uPolynomial$uOpCons'(X3,X2,X1),X0) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'(X3),'c$uPolynomial$uOsmult'(X3,X0,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'(X3,X1,X0)),'c$uPolynomial$uOpCons'(X3,X2,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'(X3,X1,X0))) ) ).
fof(fact_offset__poly__eq__0__lemma,axiom,
! [X0,X1,X2,X3] :
( 'class$uRings$uOcomm$u$usemiring$u$u0'(X3)
=> ( 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'(X3),'c$uPolynomial$uOsmult'(X3,X2,X1),'c$uPolynomial$uOpCons'(X3,X0,X1)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X3))
=> X1 = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X3)) ) ) ).
fof(fact_add__poly__code_I1_J,axiom,
! [X0,X1] :
( 'class$uGroups$uOcomm$u$umonoid$u$uadd'(X1)
=> 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'(X1),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X1)),X0) = X0 ) ).
fof(fact_smult__0__right,axiom,
! [X0,X1] :
( 'class$uRings$uOcomm$u$usemiring$u$u0'(X1)
=> 'c$uPolynomial$uOsmult'(X1,X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X1))) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X1)) ) ).
fof(fact_le__refl,axiom,
! [X0] : 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',X0,X0) ).
fof(fact_le__antisym,axiom,
! [X0,X1] :
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',X1,X0)
=> ( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',X0,X1)
=> X1 = X0 ) ) ).
fof(fact_coeff__0,axiom,
! [X0,X1] :
( 'class$uGroups$uOzero'(X1)
=> hAPP('c$uPolynomial$uOcoeff'(X1,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X1))),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'(X1) ) ).
fof(fact_coeff__pCons__0,axiom,
! [X0,X1,X2] :
( 'class$uGroups$uOzero'(X2)
=> hAPP('c$uPolynomial$uOcoeff'(X2,'c$uPolynomial$uOpCons'(X2,X1,X0)),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) = X1 ) ).
fof(fact_zero__less__Suc,axiom,
! [X0] : 'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat','c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'(X0)) ).
fof(fact_not__less__eq__eq,axiom,
! [X0,X1] :
( ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',X1,X0)
<=> 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat','c$uNat$uOSuc'(X0),X1) ) ).
fof(fact_Suc__n__not__le__n,axiom,
! [X0] : ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat','c$uNat$uOSuc'(X0),X0) ).
fof(fact_nat_Oinject,axiom,
! [X0,X1] :
( 'c$uNat$uOSuc'(X1) = 'c$uNat$uOSuc'(X0)
<=> X1 = X0 ) ).
fof(fact_gr0__conv__Suc,axiom,
! [X0] :
( 'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat','c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),X0)
<=> ? [X1] : X0 = 'c$uNat$uOSuc'(X1) ) ).
fof(clrel_Rings_Ocomm__semiring__0__Groups_Ocomm__monoid__add,axiom,
! [X0] :
( 'class$uRings$uOcomm$u$usemiring$u$u0'(X0)
=> 'class$uGroups$uOcomm$u$umonoid$u$uadd'(X0) ) ).
fof(clrel_Rings_Ocomm__semiring__0__Groups_Ozero,axiom,
! [X0] :
( 'class$uRings$uOcomm$u$usemiring$u$u0'(X0)
=> 'class$uGroups$uOzero'(X0) ) ).
fof(conj_0,hypothesis,
( 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up','v$uh') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
=> 'v$up' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ) ).
fof(conj_1,hypothesis,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'('t$ua'),'c$uPolynomial$uOsmult'('t$ua','v$uh','c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up','v$uh')),'c$uPolynomial$uOpCons'('t$ua','v$ua','c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up','v$uh'))) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ).
fof(tfree_0,hypothesis,
'class$uRings$uOcomm$u$usemiring$u$u0'('t$ua') ).
fof(conj_2,conjecture,
( 'v$up' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
& 'v$ua' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') ) ).
fof(negated_conjecture,negated_conjecture,
~ ( 'v$up' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
& 'v$ua' = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') ),
inference(negate_conjecture,[status(cth)],[conj_2]) ).
cnf(c1,plain,
( 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'(X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0)),X1) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u0'(X0) ),
inference(clausification,[status(esa)],[fact_offset__poly__0]) ).
cnf(c3,plain,
( 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'(X0,'c$uPolynomial$uOpCons'(X0,X1,X2),X3) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'(X0),'c$uPolynomial$uOsmult'(X0,X3,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'(X0,X2,X3)),'c$uPolynomial$uOpCons'(X0,X1,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'(X0,X2,X3)))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u0'(X0) ),
inference(clausification,[status(esa)],[fact_offset__poly__pCons]) ).
cnf(c4,plain,
( X2 = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0))
| 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'(X0),'c$uPolynomial$uOsmult'(X0,X1,X2),'c$uPolynomial$uOpCons'(X0,X3,X2)) != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u0'(X0) ),
inference(clausification,[status(esa)],[fact_offset__poly__eq__0__lemma]) ).
cnf(c17,plain,
( 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'(X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0)),X1) = X1
| ~ 'class$uGroups$uOcomm$u$umonoid$u$uadd'(X0) ),
inference(clausification,[status(esa)],[fact_add__poly__code_I1_J]) ).
cnf(c19,plain,
( 'c$uPolynomial$uOsmult'(X0,X1,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0))) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u0'(X0) ),
inference(clausification,[status(esa)],[fact_smult__0__right]) ).
cnf(c109,plain,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',X0,X0),
inference(clausification,[status(esa)],[fact_le__refl]) ).
cnf(c128,plain,
( X0 = X1
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',X1,X0)
| ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',X0,X1) ),
inference(clausification,[status(esa)],[fact_le__antisym]) ).
cnf(c358,plain,
( hAPP('c$uPolynomial$uOcoeff'(X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0))),X1) = 'c$uGroups$uOzero$u$uclass$uOzero'(X0)
| ~ 'class$uGroups$uOzero'(X0) ),
inference(clausification,[status(esa)],[fact_coeff__0]) ).
cnf(c359,plain,
( hAPP('c$uPolynomial$uOcoeff'(X0,'c$uPolynomial$uOpCons'(X0,X1,X2)),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) = X1
| ~ 'class$uGroups$uOzero'(X0) ),
inference(clausification,[status(esa)],[fact_coeff__pCons__0]) ).
cnf(c420,plain,
'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat','c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),'c$uNat$uOSuc'(X0)),
inference(clausification,[status(esa)],[fact_zero__less__Suc]) ).
cnf(c481,plain,
( 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat','c$uNat$uOSuc'(X1),X0)
| 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',X0,X1) ),
inference(clausification,[status(esa)],[fact_not__less__eq__eq]) ).
cnf(c483,plain,
~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat','c$uNat$uOSuc'(X0),X0),
inference(clausification,[status(esa)],[fact_Suc__n__not__le__n]) ).
cnf(c486,plain,
( X0 = X1
| 'c$uNat$uOSuc'(X0) != 'c$uNat$uOSuc'(X1) ),
inference(clausification,[status(esa)],[fact_nat_Oinject]) ).
cnf(c497,plain,
( X0 = 'c$uNat$uOSuc'(sK1001(X0))
| ~ 'c$uOrderings$uOord$u$uclass$uOless'('tc$uNat$uOnat','c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat'),X0) ),
inference(clausification,[status(esa)],[fact_gr0__conv__Suc]) ).
cnf(c809,plain,
( 'class$uGroups$uOcomm$u$umonoid$u$uadd'(X0)
| ~ 'class$uRings$uOcomm$u$usemiring$u$u0'(X0) ),
inference(clausification,[status(esa)],[clrel_Rings_Ocomm__semiring__0__Groups_Ocomm__monoid__add]) ).
cnf(c810,plain,
( 'class$uGroups$uOzero'(X0)
| ~ 'class$uRings$uOcomm$u$usemiring$u$u0'(X0) ),
inference(clausification,[status(esa)],[clrel_Rings_Ocomm__semiring__0__Groups_Ozero]) ).
cnf(c830,plain,
( 'v$up' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up','v$uh') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(clausification,[status(esa)],[conj_0]) ).
cnf(c831,plain,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'('t$ua'),'c$uPolynomial$uOsmult'('t$ua','v$uh','c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up','v$uh')),'c$uPolynomial$uOpCons'('t$ua','v$ua','c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up','v$uh'))) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),
inference(clausification,[status(esa)],[conj_1]) ).
cnf(c832,plain,
'class$uRings$uOcomm$u$usemiring$u$u0'('t$ua'),
inference(clausification,[status(esa)],[tfree_0]) ).
cnf(c833,plain,
( 'v$up' != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| 'v$ua' != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u0'('t$ua')
| 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up','v$uh') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('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)],[c831,c4]) ).
cnf(d1,plain,
( 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))
| 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up','v$uh') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')) ),
inference(resolution,[status(thm)],[c832,d0]) ).
cnf(d2,plain,
'c$uNat$uOSuc'(X0) = 'c$uNat$uOSuc'(sK1001('c$uNat$uOSuc'(X0))),
inference(resolution,[status(thm)],[c497,c420]) ).
cnf(d3,plain,
( X1 = sK1001('c$uNat$uOSuc'(X0))
| 'c$uNat$uOSuc'(X1) != 'c$uNat$uOSuc'(X0) ),
inference(superposition,[status(thm)],[d2,c486]) ).
cnf(d4,plain,
X0 = sK1001('c$uNat$uOSuc'(X0)),
inference(equality_resolution,[status(thm)],[d3]) ).
cnf(d5,plain,
~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat','c$uNat$uOSuc'(X0),sK1001('c$uNat$uOSuc'(X0))),
inference(superposition,[status(thm)],[d2,c483]) ).
cnf(d6,plain,
'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',sK1001('c$uNat$uOSuc'(X0)),X0),
inference(resolution,[status(thm)],[d5,c481]) ).
cnf(d7,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',X0,sK1001('c$uNat$uOSuc'(X0)))
| sK1001('c$uNat$uOSuc'(X0)) = X0 ),
inference(resolution,[status(thm)],[d6,c128]) ).
cnf(d8,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',X0,sK1001('c$uNat$uOSuc'(X0)))
| X0 = X0 ),
inference(demodulation,[status(thm)],[d7,d4]) ).
cnf(d9,plain,
( ~ 'c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$uNat$uOnat',X0,X0)
| X0 = X0 ),
inference(demodulation,[status(thm)],[d8,d4]) ).
cnf(d10,plain,
X0 = X0,
inference(resolution,[status(thm)],[c109,d9]) ).
cnf(d11,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up','v$uh') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),
inference(resolution,[status(thm)],[d10,d1]) ).
cnf(d12,plain,
'v$up' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),
inference(resolution,[status(thm)],[d11,c830]) ).
cnf(d13,plain,
'class$uGroups$uOzero'('t$ua'),
inference(resolution,[status(thm)],[c810,c832]) ).
cnf(d14,plain,
hAPP('c$uPolynomial$uOcoeff'('t$ua','c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua'),
inference(resolution,[status(thm)],[c358,d13]) ).
cnf(d15,plain,
hAPP('c$uPolynomial$uOcoeff'('t$ua','v$up'),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua'),
inference(demodulation,[status(thm)],[d14,d12]) ).
cnf(d16,plain,
hAPP('c$uPolynomial$uOcoeff'('t$ua','c$uPolynomial$uOpCons'('t$ua',X0,X1)),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) = X0,
inference(resolution,[status(thm)],[c359,d13]) ).
cnf(d17,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),
inference(resolution,[status(thm)],[c832,c1]) ).
cnf(d18,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up',X0) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),
inference(demodulation,[status(thm)],[d17,d12]) ).
cnf(d19,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up',X0) = 'v$up',
inference(demodulation,[status(thm)],[d18,d12]) ).
cnf(d20,plain,
'class$uGroups$uOcomm$u$umonoid$u$uadd'('t$ua'),
inference(resolution,[status(thm)],[c809,c832]) ).
cnf(d21,plain,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'('t$ua'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),X0) = X0,
inference(resolution,[status(thm)],[c17,d20]) ).
cnf(d22,plain,
'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'('t$ua'),'v$up',X0) = X0,
inference(demodulation,[status(thm)],[d21,d12]) ).
cnf(d23,plain,
'c$uPolynomial$uOsmult'('t$ua',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),
inference(resolution,[status(thm)],[c19,c832]) ).
cnf(d24,plain,
'c$uPolynomial$uOsmult'('t$ua',X0,'v$up') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),
inference(demodulation,[status(thm)],[d23,d12]) ).
cnf(d25,plain,
'c$uPolynomial$uOsmult'('t$ua',X0,'v$up') = 'v$up',
inference(demodulation,[status(thm)],[d24,d12]) ).
cnf(d26,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X0,X1),X2) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'('t$ua'),'c$uPolynomial$uOsmult'('t$ua',X2,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua',X1,X2)),'c$uPolynomial$uOpCons'('t$ua',X0,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua',X1,X2))),
inference(resolution,[status(thm)],[c832,c3]) ).
cnf(d27,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X1,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),X0) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'('t$ua'),'c$uPolynomial$uOsmult'('t$ua',X0,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uPolynomial$uOpCons'('t$ua',X1,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),X0))),
inference(superposition,[status(thm)],[d17,d26]) ).
cnf(d28,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X0,'v$up'),X1) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'('t$ua'),'c$uPolynomial$uOsmult'('t$ua',X1,'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua'))),'c$uPolynomial$uOpCons'('t$ua',X0,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),X1))),
inference(demodulation,[status(thm)],[d27,d12]) ).
cnf(d29,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X0,'v$up'),X1) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'('t$ua'),'c$uPolynomial$uOsmult'('t$ua',X1,'v$up'),'c$uPolynomial$uOpCons'('t$ua',X0,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),X1))),
inference(demodulation,[status(thm)],[d28,d12]) ).
cnf(d30,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X1,'v$up'),X0) = 'c$uGroups$uOplus$u$uclass$uOplus'('tc$uPolynomial$uOpoly'('t$ua'),'v$up','c$uPolynomial$uOpCons'('t$ua',X1,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),X0))),
inference(demodulation,[status(thm)],[d29,d25]) ).
cnf(d31,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X0,'v$up'),X1) = 'c$uPolynomial$uOpCons'('t$ua',X0,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),X1)),
inference(demodulation,[status(thm)],[d30,d22]) ).
cnf(d32,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X0,'v$up'),X1) = 'c$uPolynomial$uOpCons'('t$ua',X0,'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','v$up',X1)),
inference(demodulation,[status(thm)],[d31,d12]) ).
cnf(d33,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uPolynomial$uOpCons'('t$ua',X1,'v$up'),X0) = 'c$uPolynomial$uOpCons'('t$ua',X1,'v$up'),
inference(demodulation,[status(thm)],[d32,d19]) ).
cnf(d34,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$ua','v$up'),'v$uh') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('t$ua')),
inference(demodulation,[status(thm)],[c831,d26]) ).
cnf(d35,plain,
'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOoffset$u$upoly'('t$ua','c$uPolynomial$uOpCons'('t$ua','v$ua','v$up'),'v$uh') = 'v$up',
inference(demodulation,[status(thm)],[d34,d12]) ).
cnf(d36,plain,
'c$uPolynomial$uOpCons'('t$ua','v$ua','v$up') = 'v$up',
inference(demodulation,[status(thm)],[d35,d33]) ).
cnf(d37,plain,
hAPP('c$uPolynomial$uOcoeff'('t$ua','v$up'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uNat$uOnat')) = 'v$ua',
inference(superposition,[status(thm)],[d36,d16]) ).
cnf(d38,plain,
'c$uGroups$uOzero$u$uclass$uOzero'('t$ua') = 'v$ua',
inference(demodulation,[status(thm)],[d37,d15]) ).
cnf(d39,plain,
'v$ua' != 'c$uGroups$uOzero$u$uclass$uOzero'('t$ua'),
inference(resolution,[status(thm)],[d12,c833]) ).
cnf(d40,plain,
'v$ua' != 'v$ua',
inference(demodulation,[status(thm)],[d39,d38]) ).
cnf(d41,plain,
$false,
inference(resolution,[status(thm)],[d10,d40]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW186+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 : n009.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.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 15:26:44 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 171.10/30.75 % SZS status Theorem for theBenchmark.p
% 171.10/30.75 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------