%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW272+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 : n018.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 21.05s 12.24s
% Output : CNFRefutation 21.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 7
% Syntax : Number of formulae : 24 ( 14 unt; 0 def)
% Number of atoms : 39 ( 14 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 34 ( 19 ~; 11 |; 0 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-3 aty)
% Number of variables : 14 ( 1 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_pne,axiom,
'v$upa' != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) ).
fof(fact_dvd__0__left,axiom,
! [X0,X1] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X1)
=> ( hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'(X1),'c$uGroups$uOzero$u$uclass$uOzero'(X1)),X0))
=> X0 = 'c$uGroups$uOzero$u$uclass$uOzero'(X1) ) ) ).
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_dvd__triv__right,axiom,
! [X0,X1,X2] :
( 'class$uRings$uOcomm$u$usemiring$u$u1'(X2)
=> hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'(X2),X1),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X2),X0),X1))) ) ).
fof(arity_Complex__Ocomplex__Rings_Ocomm__semiring__1,axiom,
'class$uRings$uOcomm$u$usemiring$u$u1'('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,
'v$us' != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) ).
fof(negated_conjecture,negated_conjecture,
~ ( 'v$us' != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) ),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c1,plain,
'v$upa' != 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),
inference(clausification,[status(esa)],[fact_pne]) ).
cnf(c86,plain,
( X1 = 'c$uGroups$uOzero$u$uclass$uOzero'(X0)
| ~ hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'(X0),'c$uGroups$uOzero$u$uclass$uOzero'(X0)),X1))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_dvd__0__left]) ).
cnf(c91,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(c267,plain,
( hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'(X0),X1),hAPP(hAPP('c$uGroups$uOtimes$u$uclass$uOtimes'(X0),X2),X1)))
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[fact_dvd__triv__right]) ).
cnf(c1506,plain,
'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[arity_Complex__Ocomplex__Rings_Ocomm__semiring__1]) ).
cnf(c1559,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(c1591,plain,
'v$us' = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))
| X0 = 'c$uGroups$uOzero$u$uclass$uOzero'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))
| ~ hBOOL(hAPP(hAPP('c$uRings$uOdvd$u$uclass$uOdvd'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),'v$us'),X0)) ),
inference(superposition,[status(thm)],[c1591,c86]) ).
cnf(d1,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')),'v$us'),X0))
| X0 = 'v$us' ),
inference(demodulation,[status(thm)],[d0,c1591]) ).
cnf(d2,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'),'v$us'))),'c$uPolynomial$uOorder'('tc$uComplex$uOcomplex','v$ua','v$upa'))),'v$us'),
inference(demodulation,[status(thm)],[c91,c1591]) ).
cnf(d3,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')),'v$us'),'v$upa')) ),
inference(superposition,[status(thm)],[d2,c267]) ).
cnf(d4,plain,
( ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex'))
| 'v$upa' = 'v$us'
| ~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')) ),
inference(resolution,[status(thm)],[d3,d1]) ).
cnf(d5,plain,
'v$upa' != 'v$us',
inference(demodulation,[status(thm)],[c1,c1591]) ).
cnf(d6,plain,
~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uPolynomial$uOpoly'('tc$uComplex$uOcomplex')),
inference(resolution,[status(thm)],[d5,d4]) ).
cnf(d7,plain,
~ 'class$uRings$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[c1559,d6]) ).
cnf(d8,plain,
$false,
inference(resolution,[status(thm)],[c1506,d7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW272+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.45 % Computer : n018.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sat Sep 26 15:36:52 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.05/12.24 % SZS status Theorem for theBenchmark.p
% 21.05/12.24 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------