%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW278+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 : n008.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:37 AM UTC 2026
% Result : Theorem 69.34s 25.49s
% Output : CNFRefutation 69.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 14
% Syntax : Number of formulae : 56 ( 24 unt; 0 def)
% Number of atoms : 99 ( 42 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 80 ( 37 ~; 34 |; 0 &)
% ( 2 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 5 con; 0-3 aty)
% Number of variables : 50 ( 8 sgn 17 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_h,axiom,
hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$us'),'v$ux') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ).
fof(fact_a,axiom,
hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$ua') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ).
fof(fact_fundamental__theorem__of__algebra,axiom,
! [X0] :
( ~ 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOconstant'('tc$uComplex$uOcomplex','tc$uComplex$uOcomplex','c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex',X0))
=> ? [X1] : hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex',X0),X1) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ) ).
fof(fact_constant__def,axiom,
! [X0,X1,X2] :
( 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOconstant'(X2,X1,X0)
<=> ! [X3,X4] : hAPP(X0,X3) = hAPP(X0,X4) ) ).
fof(fact_s,axiom,
'v$upa' = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex','v$ua'),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))))),'c$uPolynomial$uOorder'('tc$uComplex$uOcomplex','v$ua','v$upa'))),'v$us') ).
fof(fact_minus__minus,axiom,
! [X0,X1] :
( 'class$uGroups$uOgroup$u$uadd'(X1)
=> 'c$uGroups$uOuminus$u$uclass$uOuminus'(X1,'c$uGroups$uOuminus$u$uclass$uOuminus'(X1,X0)) = X0 ) ).
fof(fact_one__poly__def,axiom,
! [X0] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X0)
=> 'c$uGroups$uOone$u$uclass$uOone'('tc$uPolynomial$uOpoly'(X0)) = 'c$uPolynomial$uOpCons'(X0,'c$uGroups$uOone$u$uclass$uOone'(X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0))) ) ).
fof(fact_poly__eq__0__iff__dvd,axiom,
! [X0,X1,X2] :
( 'class$uRings$uOidom'(X2)
=> ( hAPP('c$uPolynomial$uOpoly'(X2,X1),X0) = 'c$uGroups$uOzero$u$uclass$uOzero'(X2)
<=> hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'(X2)),'c$uPolynomial$uOpCons'(X2,'c$uGroups$uOuminus$u$uclass$uOuminus'(X2,X0),'c$uPolynomial$uOpCons'(X2,'c$uGroups$uOone$u$uclass$uOone'(X2),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X2))))),X1)) ) ) ).
fof(fact_dvd__mult,axiom,
! [X0,X1,X2,X3] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X3)
=> ( hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'(X3),X2),X1))
=> hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'(X3),X2),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X3),X0),X1))) ) ) ).
fof(arity_Complex__Ocomplex__Rings_Ocomm__semiring__1,axiom,
'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex') ).
fof(arity_Complex__Ocomplex__Groups_Ogroup__add,axiom,
'class$uGroups$uOgroup$u$uadd'('tc$uComplex$uOcomplex') ).
fof(arity_Complex__Ocomplex__Rings_Oidom,axiom,
'class$uRings$uOidom'('tc$uComplex$uOcomplex') ).
fof(arity_Polynomial__Opoly__Rings_Ocomm__semiring__1,axiom,
! [X0] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X0)
=> 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uPolynomial$uOpoly'(X0)) ) ).
fof(conj_0,conjecture,
hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$ux') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ).
fof(negated_conjecture,negated_conjecture,
hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$ux') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c2,plain,
hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$us'),'v$ux') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[fact_h]) ).
cnf(c4,plain,
hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$ua') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[fact_a]) ).
cnf(c17,plain,
( hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex',X0),sK16(X0)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')
| 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOconstant'('tc$uComplex$uOcomplex','tc$uComplex$uOcomplex','c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex',X0)) ),
inference(clausification,[status(esa)],[fact_fundamental__theorem__of__algebra]) ).
cnf(c29,plain,
( hAPP(X2,X3) = hAPP(X2,X4)
| ~ 'c$uFundamental$u$uTheorem$u$uAlgebra$u$uMirabelle$uOconstant'(X0,X1,X2) ),
inference(clausification,[status(esa)],[fact_constant__def]) ).
cnf(c178,plain,
'v$upa' = hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),hAPP(hAPP('c$uPower$uOpower$u$uclass$uOpower'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex','v$ua'),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))))),'c$uPolynomial$uOorder'('tc$uComplex$uOcomplex','v$ua','v$upa'))),'v$us'),
inference(clausification,[status(esa)],[fact_s]) ).
cnf(c222,plain,
( 'c$uGroups$uOuminus$u$uclass$uOuminus'(X0,'c$uGroups$uOuminus$u$uclass$uOuminus'(X0,X1)) = X1
| ~ 'class$uGroups$uOgroup$u$uadd'(X0) ),
inference(clausification,[status(esa)],[fact_minus__minus]) ).
cnf(c237,plain,
( 'c$uGroups$uOone$u$uclass$uOone'('tc$uPolynomial$uOpoly'(X0)) = 'c$uPolynomial$uOpCons'(X0,'c$uGroups$uOone$u$uclass$uOone'(X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0)))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_one__poly__def]) ).
cnf(c298,plain,
( hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'(X0)),'c$uPolynomial$uOpCons'(X0,'c$uGroups$uOuminus$u$uclass$uOuminus'(X0,X2),'c$uPolynomial$uOpCons'(X0,'c$uGroups$uOone$u$uclass$uOone'(X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0))))),X1))
| hAPP('c$uPolynomial$uOpoly'(X0,X1),X2) != 'c$uGroups$uOzero$u$uclass$uOzero'(X0)
| ~ 'class$uRings$uOidom'(X0) ),
inference(clausification,[status(esa)],[fact_poly__eq__0__iff__dvd]) ).
cnf(c299,plain,
( ~ hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'(X0)),'c$uPolynomial$uOpCons'(X0,'c$uGroups$uOuminus$u$uclass$uOuminus'(X0,X2),'c$uPolynomial$uOpCons'(X0,'c$uGroups$uOone$u$uclass$uOone'(X0),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'(X0))))),X1))
| hAPP('c$uPolynomial$uOpoly'(X0,X1),X2) = 'c$uGroups$uOzero$u$uclass$uOzero'(X0)
| ~ 'class$uRings$uOidom'(X0) ),
inference(clausification,[status(esa)],[fact_poly__eq__0__iff__dvd]) ).
cnf(c488,plain,
( hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'(X0),X1),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),X3),X2)))
| ~ hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'(X0),X1),X2))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_dvd__mult]) ).
cnf(c1502,plain,
'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[arity_Complex__Ocomplex__Rings_Ocomm__semiring__1]) ).
cnf(c1512,plain,
'class$uGroups$uOgroup$u$uadd'('tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[arity_Complex__Ocomplex__Groups_Ogroup__add]) ).
cnf(c1523,plain,
'class$uRings$uOidom'('tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[arity_Complex__Ocomplex__Rings_Oidom]) ).
cnf(c1554,plain,
( 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uPolynomial$uOpoly'(X0))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[arity_Polynomial__Opoly__Rings_Ocomm__semiring__1]) ).
cnf(c1585,plain,
hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$ux') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
'c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex',X0)) = X0,
inference(resolution,[status(thm)],[c222,c1512]) ).
cnf(d1,plain,
'c$uGroups$uOone$u$uclass$uOone'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) = 'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))),
inference(resolution,[status(thm)],[c237,c1502]) ).
cnf(d2,plain,
( ~ 'class$uRings$uOidom'('tc$uComplex$uOcomplex')
| hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex',X1),'c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex',X0)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')
| ~ hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex',X0,'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))))),X1)) ),
inference(superposition,[status(thm)],[d0,c299]) ).
cnf(d3,plain,
( ~ hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex',X1,'c$uGroups$uOone$u$uclass$uOone'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')))),X0))
| ~ 'class$uRings$uOidom'('tc$uComplex$uOcomplex')
| hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex',X0),'c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex',X1)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(demodulation,[status(thm)],[d2,d1]) ).
cnf(d4,plain,
( ~ hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex',X1,'c$uGroups$uOone$u$uclass$uOone'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')))),X0))
| hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex',X0),'c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex',X1)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(resolution,[status(thm)],[c1523,d3]) ).
cnf(d5,plain,
( hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex','v$ux'),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))))),'v$us'))
| ~ 'class$uRings$uOidom'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(superposition,[status(thm)],[c2,c298]) ).
cnf(d6,plain,
( hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex','v$ux'),'c$uGroups$uOone$u$uclass$uOone'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')))),'v$us'))
| ~ 'class$uRings$uOidom'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(demodulation,[status(thm)],[d5,d1]) ).
cnf(d7,plain,
( hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex','v$ux'),'c$uGroups$uOone$u$uclass$uOone'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')))),'v$us'))
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(resolution,[status(thm)],[c1523,d6]) ).
cnf(d8,plain,
( hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex',X0),sK16(X0)) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')
| hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex',X0),X1) = hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex',X0),X2) ),
inference(resolution,[status(thm)],[c29,c17]) ).
cnf(d9,plain,
( hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),sK16('v$upa')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')
| hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),X0) != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(superposition,[status(thm)],[d8,c1585]) ).
cnf(d10,plain,
( hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),sK16('v$upa')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(superposition,[status(thm)],[c4,d9]) ).
cnf(d11,plain,
hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),sK16('v$upa')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),
inference(equality_resolution,[status(thm)],[d10]) ).
cnf(d12,plain,
( hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex',sK16('v$upa')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))))),'v$upa'))
| ~ 'class$uRings$uOidom'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(superposition,[status(thm)],[d11,c298]) ).
cnf(d13,plain,
( hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex',sK16('v$upa')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))))),'v$upa'))
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(resolution,[status(thm)],[c1523,d12]) ).
cnf(d14,plain,
hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex',sK16('v$upa')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))))),'v$upa')),
inference(equality_resolution,[status(thm)],[d13]) ).
cnf(d15,plain,
( ~ 'class$uRings$uOidom'('tc$uComplex$uOcomplex')
| hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),sK16('v$upa')) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(resolution,[status(thm)],[d14,c299]) ).
cnf(d16,plain,
( ~ 'class$uRings$uOidom'('tc$uComplex$uOcomplex')
| 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(demodulation,[status(thm)],[d15,d11]) ).
cnf(d17,plain,
'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[c1523,d16]) ).
cnf(d18,plain,
hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex','v$ux'),'c$uGroups$uOone$u$uclass$uOone'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')))),'v$us')),
inference(resolution,[status(thm)],[d17,d7]) ).
cnf(d19,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))
| ~ hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),X0),'v$us'))
| hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),X0),'v$upa')) ),
inference(superposition,[status(thm)],[c178,c488]) ).
cnf(d20,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))
| hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'c$uPolynomial$uOpCons'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex','v$ux'),'c$uGroups$uOone$u$uclass$uOone'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')))),'v$upa')) ),
inference(resolution,[status(thm)],[d19,d18]) ).
cnf(d21,plain,
( hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex','c$uGroups$uOuminus$u$uclass$uOuminus'('tc$uComplex$uOcomplex','v$ux'))) = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex')
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) ),
inference(resolution,[status(thm)],[d20,d4]) ).
cnf(d22,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))
| hAPP('c$uPolynomial$uOpoly'('tc$uComplex$uOcomplex','v$upa'),'v$ux') = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ),
inference(demodulation,[status(thm)],[d21,d0]) ).
cnf(d23,plain,
~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),
inference(resolution,[status(thm)],[c1585,d22]) ).
cnf(d24,plain,
~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[d23,c1554]) ).
cnf(d25,plain,
$false,
inference(resolution,[status(thm)],[c1502,d24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW278+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.11/10.38 % Computer : n008.cluster.edu
% 0.11/10.38 % Model : x86_64 x86_64
% 0.11/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.38 % Memory : 8046.5625MB
% 0.11/10.38 % OS : Linux 6.8.0-71-generic
% 0.11/10.38 % CPULimit : 300
% 0.11/10.38 % WCLimit : 300
% 0.11/10.38 % DateTime : Sat Sep 26 15:36:08 UTC 2026
% 0.11/10.39 % CPUTime :
% 0.11/10.39 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 69.34/25.49 % SZS status Theorem for theBenchmark.p
% 69.34/25.49 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------