%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV617-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Wed Jul 20 21:44:35 EDT 2022
% Result : Unsatisfiable 20.41s 20.59s
% Output : Refutation 25.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 46
% Syntax : Number of clauses : 95 ( 42 unt; 9 nHn; 95 RR)
% Number of literals : 176 ( 0 equ; 77 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 30 ( 29 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(12,axiom,
( ~ class_Ring__and__Field_Odvd(u)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_HOL_Otimes__class_Otimes(v,w,u),u) ),
file('SWV617-1.p',unknown),
[] ).
cnf(24,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| equal(c_HOL_Otimes__class_Otimes(v,w,u),c_HOL_Otimes__class_Otimes(w,v,u)) ),
file('SWV617-1.p',unknown),
[] ).
cnf(108,axiom,
( ~ class_OrderedGroup_Ogroup__add(u)
| ~ equal(c_HOL_Ouminus__class_Ouminus(v,u),c_HOL_Ouminus__class_Ouminus(w,u))
| equal(v,w) ),
file('SWV617-1.p',unknown),
[] ).
cnf(152,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| ~ c_Ring__and__Field_Odvd__class_Odvd(v,w,u)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_HOL_Otimes__class_Otimes(w,x,u),u) ),
file('SWV617-1.p',unknown),
[] ).
cnf(153,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Otimes__class_Otimes(v,w,u),x,u)
| c_Ring__and__Field_Odvd__class_Odvd(v,x,u) ),
file('SWV617-1.p',unknown),
[] ).
cnf(186,axiom,
( ~ class_OrderedGroup_Ogroup__add(u)
| equal(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v,u),u),v) ),
file('SWV617-1.p',unknown),
[] ).
cnf(214,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ozero__class_Ozero(u),v,u)
| equal(v,c_HOL_Ozero__class_Ozero(u)) ),
file('SWV617-1.p',unknown),
[] ).
cnf(229,axiom,
( ~ class_Ring__and__Field_Odivision__ring(u)
| equal(v,c_HOL_Ozero__class_Ozero(u))
| equal(c_HOL_Otimes__class_Otimes(v,c_HOL_Oinverse__class_Oinverse(v,u),u),c_HOL_Oone__class_Oone(u)) ),
file('SWV617-1.p',unknown),
[] ).
cnf(309,axiom,
( ~ class_Ring__and__Field_Oidom(u)
| equal(c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(v,u),c_HOL_Ouminus__class_Ouminus(v,u),u),c_HOL_Otimes__class_Otimes(v,v,u)) ),
file('SWV617-1.p',unknown),
[] ).
cnf(321,axiom,
( ~ class_Ring__and__Field_Ocomm__ring__1(u)
| ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(v,u),w,u)
| c_Ring__and__Field_Odvd__class_Odvd(v,w,u) ),
file('SWV617-1.p',unknown),
[] ).
cnf(401,axiom,
( ~ class_OrderedGroup_Ocomm__monoid__mult(u)
| equal(c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(u),v,u),v) ),
file('SWV617-1.p',unknown),
[] ).
cnf(404,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| equal(c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(u),v,u),v) ),
file('SWV617-1.p',unknown),
[] ).
cnf(429,axiom,
( ~ class_OrderedGroup_Ocomm__monoid__mult(u)
| equal(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v,w,u),c_Power_Opower__class_Opower(x,w,u),u),c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(v,x,u),w,u)) ),
file('SWV617-1.p',unknown),
[] ).
cnf(529,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Otimes__class_Otimes(v,c_HOL_Oinverse__class_Oinverse(w,u),u),c_HOL_Oinverse__class_Odivide(v,w,u)) ),
file('SWV617-1.p',unknown),
[] ).
cnf(625,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(u),v,u),c_HOL_Oinverse__class_Oinverse(v,u)) ),
file('SWV617-1.p',unknown),
[] ).
cnf(647,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Oinverse__class_Odivide(v,c_HOL_Oone__class_Oone(u),u),v) ),
file('SWV617-1.p',unknown),
[] ).
cnf(652,axiom,
equal(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(u),u,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
file('SWV617-1.p',unknown),
[] ).
cnf(656,axiom,
( ~ class_OrderedGroup_Oab__group__add(u)
| equal(c_HOL_Ominus__class_Ominus(v,v,u),c_HOL_Ozero__class_Ozero(u)) ),
file('SWV617-1.p',unknown),
[] ).
cnf(739,axiom,
class_Ring__and__Field_Oring__1__no__zero__divisors(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(740,axiom,
class_Ring__and__Field_Oring__no__zero__divisors(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(741,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(742,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(743,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(744,axiom,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(745,axiom,
class_OrderedGroup_Oab__semigroup__mult(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(746,axiom,
class_OrderedGroup_Ocomm__monoid__mult(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(747,axiom,
class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(748,axiom,
class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(749,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(750,axiom,
class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(751,axiom,
class_Ring__and__Field_Osemiring__0(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(752,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(753,axiom,
class_Ring__and__Field_Omult__zero(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(754,axiom,
class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(755,axiom,
class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(756,axiom,
class_Ring__and__Field_Oring__1(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(757,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(758,axiom,
class_Ring__and__Field_Oring(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(759,axiom,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(760,axiom,
class_Ring__and__Field_Odvd(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(761,axiom,
class_Int_Oring__char__0(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(762,axiom,
class_Int_Onumber__ring(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(763,axiom,
class_Power_Opower(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(764,axiom,
class_SEQ_Obanach(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(765,axiom,
class_Int_Onumber(tc_Complex_Ocomplex),
file('SWV617-1.p',unknown),
[] ).
cnf(766,axiom,
~ equal(c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_n,tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
file('SWV617-1.p',unknown),
[] ).
cnf(793,plain,
~ equal(c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(rew,[status(thm),theory(equality)],[652,766]),
[iquote('0:Rew:652.0,766.0')] ).
cnf(1134,plain,
( ~ class_Ring__and__Field_Ofield(u)
| ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(u),u),c_HOL_Oone__class_Oone(u)) ),
inference(spr,[status(thm),theory(equality)],[625,647]),
[iquote('0:SpR:625.1,647.1')] ).
cnf(1136,plain,
( ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(u),u),c_HOL_Oone__class_Oone(u)) ),
inference(obv,[status(thm),theory(equality)],[1134]),
[iquote('0:Obv:1134.0')] ).
cnf(2155,plain,
( ~ class_OrderedGroup_Ogroup__add(u)
| ~ class_OrderedGroup_Ogroup__add(u)
| ~ equal(v,c_HOL_Ouminus__class_Ouminus(w,u))
| equal(c_HOL_Ouminus__class_Ouminus(v,u),w) ),
inference(spl,[status(thm),theory(equality)],[186,108]),
[iquote('0:SpL:186.1,108.1')] ).
cnf(2168,plain,
( ~ class_OrderedGroup_Ogroup__add(u)
| ~ equal(v,c_HOL_Ouminus__class_Ouminus(w,u))
| equal(c_HOL_Ouminus__class_Ouminus(v,u),w) ),
inference(obv,[status(thm),theory(equality)],[2155]),
[iquote('0:Obv:2155.0')] ).
cnf(2199,plain,
( ~ class_OrderedGroup_Ogroup__add(u)
| ~ class_OrderedGroup_Ogroup__add(u)
| ~ equal(v,w)
| equal(c_HOL_Ouminus__class_Ouminus(v,u),c_HOL_Ouminus__class_Ouminus(w,u)) ),
inference(spl,[status(thm),theory(equality)],[186,2168]),
[iquote('0:SpL:186.1,2168.1')] ).
cnf(2202,plain,
( ~ class_OrderedGroup_Ogroup__add(u)
| ~ equal(v,w)
| equal(c_HOL_Ouminus__class_Ouminus(v,u),c_HOL_Ouminus__class_Ouminus(w,u)) ),
inference(obv,[status(thm),theory(equality)],[2199]),
[iquote('0:Obv:2199.0')] ).
cnf(2430,plain,
( ~ class_Ring__and__Field_Ofield(u)
| ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Otimes__class_Otimes(v,c_HOL_Oone__class_Oone(u),u),c_HOL_Oinverse__class_Odivide(v,c_HOL_Oone__class_Oone(u),u)) ),
inference(spr,[status(thm),theory(equality)],[1136,529]),
[iquote('0:SpR:1136.1,529.1')] ).
cnf(2436,plain,
( ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Otimes__class_Otimes(v,c_HOL_Oone__class_Oone(u),u),c_HOL_Oinverse__class_Odivide(v,c_HOL_Oone__class_Oone(u),u)) ),
inference(obv,[status(thm),theory(equality)],[2430]),
[iquote('0:Obv:2430.0')] ).
cnf(2437,plain,
( ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Otimes__class_Otimes(v,c_HOL_Oone__class_Oone(u),u),v) ),
inference(rew,[status(thm),theory(equality)],[647,2436]),
[iquote('0:Rew:647.1,2436.1')] ).
cnf(4744,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| ~ c_Ring__and__Field_Odvd__class_Odvd(v,c_HOL_Oone__class_Oone(u),u)
| c_Ring__and__Field_Odvd__class_Odvd(v,w,u) ),
inference(spr,[status(thm),theory(equality)],[404,152]),
[iquote('0:SpR:404.1,152.2')] ).
cnf(4767,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| ~ c_Ring__and__Field_Odvd__class_Odvd(v,c_HOL_Oone__class_Oone(u),u)
| c_Ring__and__Field_Odvd__class_Odvd(v,w,u) ),
inference(obv,[status(thm),theory(equality)],[4744]),
[iquote('0:Obv:4744.0')] ).
cnf(9087,plain,
( ~ class_Ring__and__Field_Oidom(u)
| ~ class_Ring__and__Field_Odvd(u)
| c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(v,u),c_HOL_Otimes__class_Otimes(v,v,u),u) ),
inference(spr,[status(thm),theory(equality)],[309,12]),
[iquote('0:SpR:309.1,12.1')] ).
cnf(46691,plain,
( ~ class_OrderedGroup_Ocomm__monoid__mult(tc_Complex_Ocomplex)
| equal(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(u,v,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(u,c_FFT__Mirabelle_Oroot(v),tc_Complex_Ocomplex),v,tc_Complex_Ocomplex)) ),
inference(spr,[status(thm),theory(equality)],[652,429]),
[iquote('0:SpR:652.0,429.1')] ).
cnf(46701,plain,
( ~ class_OrderedGroup_Ocomm__monoid__mult(tc_Complex_Ocomplex)
| equal(c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_Power_Opower__class_Opower(u,v,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_FFT__Mirabelle_Oroot(v),u,tc_Complex_Ocomplex),v,tc_Complex_Ocomplex)) ),
inference(spr,[status(thm),theory(equality)],[652,429]),
[iquote('0:SpR:652.0,429.1')] ).
cnf(46718,plain,
( ~ class_OrderedGroup_Ocomm__monoid__mult(tc_Complex_Ocomplex)
| equal(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_FFT__Mirabelle_Oroot(u),v,tc_Complex_Ocomplex),u,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v,u,tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[401,46701]),
[iquote('0:Rew:401.1,46701.1')] ).
cnf(46719,plain,
equal(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_FFT__Mirabelle_Oroot(u),v,tc_Complex_Ocomplex),u,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v,u,tc_Complex_Ocomplex)),
inference(ssi,[status(thm)],[46718,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:46718.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(46720,plain,
equal(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(u,v,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(u,c_FFT__Mirabelle_Oroot(v),tc_Complex_Ocomplex),v,tc_Complex_Ocomplex)),
inference(ssi,[status(thm)],[46691,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:46691.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(46778,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)
| equal(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(u,c_FFT__Mirabelle_Oroot(v),tc_Complex_Ocomplex),v,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(u,v,tc_Complex_Ocomplex)) ),
inference(spr,[status(thm),theory(equality)],[24,46719]),
[iquote('0:SpR:24.1,46719.0')] ).
cnf(46779,plain,
( ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| equal(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(u),u,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),u,tc_Complex_Ocomplex)) ),
inference(spr,[status(thm),theory(equality)],[2437,46719]),
[iquote('0:SpR:2437.1,46719.0')] ).
cnf(46806,plain,
( ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| equal(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),u,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[652,46779]),
[iquote('0:Rew:652.0,46779.1')] ).
cnf(46807,plain,
equal(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),u,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
inference(ssi,[status(thm)],[46806,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:46806.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(46815,plain,
~ equal(c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(rew,[status(thm),theory(equality)],[46807,793]),
[iquote('0:Rew:46807.0,793.0')] ).
cnf(46820,plain,
equal(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(u,c_FFT__Mirabelle_Oroot(v),tc_Complex_Ocomplex),v,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(u,v,tc_Complex_Ocomplex)),
inference(ssi,[status(thm)],[46778,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:46778.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(46821,plain,
equal(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(u,v,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Power_Opower__class_Opower(u,v,tc_Complex_Ocomplex)),
inference(rew,[status(thm),theory(equality)],[46820,46720]),
[iquote('0:Rew:46820.0,46720.0')] ).
cnf(46949,plain,
equal(c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
inference(spr,[status(thm),theory(equality)],[652,46821]),
[iquote('0:SpR:652.0,46821.0')] ).
cnf(47000,plain,
( ~ class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex)
| ~ equal(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(spl,[status(thm),theory(equality)],[656,46815]),
[iquote('0:SpL:656.1,46815.0')] ).
cnf(47004,plain,
~ equal(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(ssi,[status(thm)],[47000,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:47000.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(47011,plain,
( ~ class_Ring__and__Field_Oidom(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Odvd(tc_Complex_Ocomplex)
| c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(spr,[status(thm),theory(equality)],[46949,9087]),
[iquote('0:SpR:46949.0,9087.2')] ).
cnf(47080,plain,
c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(ssi,[status(thm)],[47011,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:47011.1,47011.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(47112,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)
| c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),u,tc_Complex_Ocomplex) ),
inference(res,[status(thm),theory(equality)],[47080,4767]),
[iquote('0:Res:47080.0,4767.1')] ).
cnf(47114,plain,
c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),u,tc_Complex_Ocomplex),
inference(ssi,[status(thm)],[47112,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:47112.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(47122,plain,
( ~ class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex)
| ~ equal(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),u)
| c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(u,tc_Complex_Ocomplex),v,tc_Complex_Ocomplex) ),
inference(spr,[status(thm),theory(equality)],[2202,47114]),
[iquote('0:SpR:2202.2,47114.0')] ).
cnf(47143,plain,
( ~ equal(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),u)
| c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(u,tc_Complex_Ocomplex),v,tc_Complex_Ocomplex) ),
inference(ssi,[status(thm)],[47122,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:47122.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(48284,plain,
( ~ class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex)
| ~ equal(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),u)
| c_Ring__and__Field_Odvd__class_Odvd(u,v,tc_Complex_Ocomplex) ),
inference(res,[status(thm),theory(equality)],[47143,321]),
[iquote('0:Res:47143.1,321.1')] ).
cnf(48285,plain,
( ~ equal(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),u)
| c_Ring__and__Field_Odvd__class_Odvd(u,v,tc_Complex_Ocomplex) ),
inference(ssi,[status(thm)],[48284,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:48284.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(48302,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)
| ~ equal(c_HOL_Otimes__class_Otimes(u,v,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(u,w,tc_Complex_Ocomplex) ),
inference(res,[status(thm),theory(equality)],[48285,153]),
[iquote('0:Res:48285.1,153.1')] ).
cnf(48307,plain,
( ~ equal(c_HOL_Otimes__class_Otimes(u,v,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(u,w,tc_Complex_Ocomplex) ),
inference(ssi,[status(thm)],[48302,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:48302.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(48674,plain,
( ~ class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex)
| ~ equal(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex))
| equal(u,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(u,v,tc_Complex_Ocomplex) ),
inference(spl,[status(thm),theory(equality)],[229,48307]),
[iquote('0:SpL:229.2,48307.0')] ).
cnf(48700,plain,
( ~ class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex)
| equal(u,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(u,v,tc_Complex_Ocomplex) ),
inference(obv,[status(thm),theory(equality)],[48674]),
[iquote('0:Obv:48674.1')] ).
cnf(48701,plain,
( equal(u,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(u,v,tc_Complex_Ocomplex) ),
inference(ssi,[status(thm)],[48700,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:48700.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(48737,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)
| equal(c_HOL_Otimes__class_Otimes(u,v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(u,w,tc_Complex_Ocomplex) ),
inference(res,[status(thm),theory(equality)],[48701,153]),
[iquote('0:Res:48701.1,153.1')] ).
cnf(48746,plain,
( equal(c_HOL_Otimes__class_Otimes(u,v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(u,w,tc_Complex_Ocomplex) ),
inference(ssi,[status(thm)],[48737,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:48737.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(49665,plain,
( ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| c_Ring__and__Field_Odvd__class_Odvd(u,v,tc_Complex_Ocomplex)
| equal(c_HOL_Oinverse__class_Odivide(u,w,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(spr,[status(thm),theory(equality)],[48746,529]),
[iquote('0:SpR:48746.0,529.1')] ).
cnf(49748,plain,
( c_Ring__and__Field_Odvd__class_Odvd(u,v,tc_Complex_Ocomplex)
| equal(c_HOL_Oinverse__class_Odivide(u,w,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(ssi,[status(thm)],[49665,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:49665.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(50276,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)
| equal(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(v,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(res,[status(thm),theory(equality)],[49748,214]),
[iquote('0:Res:49748.0,214.1')] ).
cnf(50292,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)
| equal(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(con,[status(thm)],[50276]),
[iquote('0:Con:50276.2')] ).
cnf(50293,plain,
equal(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(ssi,[status(thm)],[50292,761,756,739,760,751,745,764,746,740,752,749,741,763,758,754,753,750,744,765,762,748,755,759,747,743,757,742]),
[iquote('0:SSi:50292.0,761.0,756.0,739.0,760.0,751.0,745.0,764.0,746.0,740.0,752.0,749.0,741.0,763.0,758.0,754.0,753.0,750.0,744.0,765.0,762.0,748.0,755.0,759.0,747.0,743.0,757.0,742.0')] ).
cnf(50294,plain,
$false,
inference(unc,[status(thm)],[50293,47004]),
[iquote('0:UnC:50293.0,47004.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SWV617-1 : TPTP v8.1.0. Released v4.1.0.
% 0.08/0.14 % Command : run_spass %d %s
% 0.14/0.35 % Computer : n027.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Thu Jun 16 05:40:05 EDT 2022
% 0.14/0.35 % CPUTime :
% 20.41/20.59
% 20.41/20.59 SPASS V 3.9
% 20.41/20.59 SPASS beiseite: Proof found.
% 20.41/20.59 % SZS status Theorem
% 20.41/20.59 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.41/20.59 SPASS derived 39430 clauses, backtracked 1 clauses, performed 3 splits and kept 9116 clauses.
% 20.41/20.59 SPASS allocated 113729 KBytes.
% 20.41/20.59 SPASS spent 0:0:20.19 on the problem.
% 20.41/20.59 0:00:00.06 for the input.
% 20.41/20.59 0:00:00.00 for the FLOTTER CNF translation.
% 20.41/20.59 0:00:00.40 for inferences.
% 20.41/20.59 0:00:00.05 for the backtracking.
% 20.41/20.59 0:0:19.41 for the reduction.
% 20.41/20.59
% 20.41/20.59
% 20.41/20.59 Here is a proof with depth 11, length 95 :
% 20.41/20.59 % SZS output start Refutation
% See solution above
% 25.08/25.34 Formulae used in the proof : cls_dvdI_0 cls_class__semiring_Osemiring__rules_I7_J_0 cls_neg__equal__iff__equal_0 cls_dvd__mult2_0 cls_dvd__mult__left_0 cls_minus__minus_0 cls_dvd__0__left_0 cls_right__inverse_0 cls_square__eq__iff_1 cls_minus__dvd__iff_0 cls_mult__1_0 cls_class__semiring_Osemiring__rules_I11_J_0 cls_power__mult__distrib_0 cls_divide__inverse_0 cls_inverse__eq__divide_0 cls_divide__1_0 cls_root__unity_0 cls_eq__iff__diff__eq__0_0 clsarity_Complex__Ocomplex__Ring__and__Field_Oring__1__no__zero__divisors clsarity_Complex__Ocomplex__Ring__and__Field_Oring__no__zero__divisors clsarity_Complex__Ocomplex__Ring__and__Field_Ono__zero__divisors clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__by__zero clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1 clsarity_Complex__Ocomplex__RealVector_Oreal__normed__algebra clsarity_Complex__Ocomplex__OrderedGroup_Oab__semigroup__mult clsarity_Complex__Ocomplex__OrderedGroup_Ocomm__monoid__mult clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__ring clsarity_Complex__Ocomplex__RealVector_Oreal__normed__field clsarity_Complex__Ocomplex__Ring__and__Field_Ozero__neq__one clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__ring__1 clsarity_Complex__Ocomplex__Ring__and__Field_Osemiring__0 clsarity_Complex__Ocomplex__OrderedGroup_Oab__group__add clsarity_Complex__Ocomplex__Ring__and__Field_Omult__zero clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__mult clsarity_Complex__Ocomplex__OrderedGroup_Ogroup__add clsarity_Complex__Ocomplex__Ring__and__Field_Oring__1 clsarity_Complex__Ocomplex__Ring__and__Field_Ofield clsarity_Complex__Ocomplex__Ring__and__Field_Oring clsarity_Complex__Ocomplex__Ring__and__Field_Oidom clsarity_Complex__Ocomplex__Ring__and__Field_Odvd clsarity_Complex__Ocomplex__Int_Oring__char__0 clsarity_Complex__Ocomplex__Int_Onumber__ring clsarity_Complex__Ocomplex__Power_Opower clsarity_Complex__Ocomplex__SEQ_Obanach clsarity_Complex__Ocomplex__Int_Onumber cls_conjecture_0
% 25.08/25.34
%------------------------------------------------------------------------------