%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWW272+1 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n025.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 : Thu Jul 21 01:28:13 EDT 2022
% Result : Theorem 8.41s 8.63s
% Output : Refutation 8.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 78
% Syntax : Number of clauses : 84 ( 47 unt; 0 nHn; 84 RR)
% Number of literals : 121 ( 0 equ; 39 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 43 ( 42 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
class_Groups_Ocancel__comm__monoid__add(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(106,axiom,
class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(107,axiom,
class_Rings_Odivision__ring__inverse__zero(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(108,axiom,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(109,axiom,
class_Groups_Ocancel__ab__semigroup__add(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(110,axiom,
class_Rings_Oring__1__no__zero__divisors(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(111,axiom,
class_Rings_Oring__no__zero__divisors(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(112,axiom,
class_Groups_Ocancel__semigroup__add(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(113,axiom,
class_Fields_Ofield__inverse__zero(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(114,axiom,
class_Groups_Oab__semigroup__mult(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(115,axiom,
class_Groups_Ocomm__monoid__mult(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(116,axiom,
class_Groups_Oab__semigroup__add(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(117,axiom,
class_Rings_Ono__zero__divisors(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(118,axiom,
class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(119,axiom,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(120,axiom,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(121,axiom,
class_Rings_Odivision__ring(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(122,axiom,
class_Rings_Ocomm__semiring(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(123,axiom,
class_Groups_Oab__group__add(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(124,axiom,
class_Rings_Ozero__neq__one(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(125,axiom,
class_Groups_Omonoid__mult(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(126,axiom,
class_Rings_Ocomm__ring__1(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(127,axiom,
class_Groups_Omonoid__add(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(128,axiom,
class_Rings_Osemiring__0(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(129,axiom,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(130,axiom,
class_Rings_Omult__zero(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(131,axiom,
class_Rings_Ocomm__ring(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(132,axiom,
class_Int_Oring__char__0(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(133,axiom,
class_Rings_Osemiring(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(134,axiom,
class_Groups_Ouminus(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(135,axiom,
class_Rings_Oring__1(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(136,axiom,
class_Groups_Ominus(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(137,axiom,
class_Fields_Ofield(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(138,axiom,
class_Power_Opower(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(139,axiom,
class_Groups_Ozero(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(140,axiom,
class_Rings_Oring(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(141,axiom,
class_Rings_Oidom(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(142,axiom,
class_Groups_Oone(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(143,axiom,
class_Rings_Odvd(tc_Complex_Ocomplex),
file('SWW272+1.p',unknown),
[] ).
cnf(148,axiom,
equal(c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____),
file('SWW272+1.p',unknown),
[] ).
cnf(162,axiom,
~ equal(c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____),
file('SWW272+1.p',unknown),
[] ).
cnf(181,axiom,
( ~ class_Groups_Ocancel__comm__monoid__add(u)
| class_Groups_Ocancel__comm__monoid__add(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(182,axiom,
( ~ class_Rings_Oidom(u)
| class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(191,axiom,
( ~ class_Groups_Ocancel__comm__monoid__add(u)
| class_Groups_Ocancel__ab__semigroup__add(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(192,axiom,
( ~ class_Rings_Oidom(u)
| class_Rings_Oring__1__no__zero__divisors(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(195,axiom,
( ~ class_Rings_Oidom(u)
| class_Rings_Oring__no__zero__divisors(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(199,axiom,
( ~ class_Groups_Ocancel__comm__monoid__add(u)
| class_Groups_Ocancel__semigroup__add(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(202,axiom,
( ~ class_Rings_Ocomm__semiring__0(u)
| class_Groups_Oab__semigroup__mult(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(203,axiom,
( ~ class_Rings_Ocomm__semiring__1(u)
| class_Groups_Ocomm__monoid__mult(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(204,axiom,
( ~ class_Groups_Ocomm__monoid__add(u)
| class_Groups_Oab__semigroup__add(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(206,axiom,
( ~ class_Rings_Oidom(u)
| class_Rings_Ono__zero__divisors(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(207,axiom,
( ~ class_Groups_Ocomm__monoid__add(u)
| class_Groups_Ocomm__monoid__add(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(210,axiom,
( ~ class_Rings_Ocomm__semiring__1(u)
| class_Rings_Ocomm__semiring__1(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(211,axiom,
( ~ class_Rings_Ocomm__semiring__0(u)
| class_Rings_Ocomm__semiring__0(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(212,axiom,
( ~ class_Fields_Ofield(u)
| class_Divides_Osemiring__div(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(213,axiom,
( ~ class_Rings_Ocomm__semiring__0(u)
| class_Rings_Ocomm__semiring(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(214,axiom,
( ~ class_Groups_Oab__group__add(u)
| class_Groups_Oab__group__add(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(215,axiom,
( ~ class_Rings_Ocomm__semiring__1(u)
| class_Rings_Ozero__neq__one(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(219,axiom,
( ~ class_Rings_Ocomm__semiring__1(u)
| class_Groups_Omonoid__mult(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(220,axiom,
( ~ class_Rings_Ocomm__ring__1(u)
| class_Rings_Ocomm__ring__1(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(221,axiom,
( ~ class_Groups_Ocomm__monoid__add(u)
| class_Groups_Omonoid__add(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(222,axiom,
( ~ class_Rings_Ocomm__semiring__0(u)
| class_Rings_Osemiring__0(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(223,axiom,
( ~ class_Groups_Oab__group__add(u)
| class_Groups_Ogroup__add(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(224,axiom,
( ~ class_Fields_Ofield(u)
| class_Divides_Oring__div(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(225,axiom,
( ~ class_Rings_Ocomm__semiring__0(u)
| class_Rings_Omult__zero(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(226,axiom,
( ~ class_Rings_Ocomm__ring(u)
| class_Rings_Ocomm__ring(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(229,axiom,
( ~ class_Rings_Ocomm__semiring__0(u)
| class_Rings_Osemiring(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(231,axiom,
( ~ class_Groups_Oab__group__add(u)
| class_Groups_Ouminus(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(232,axiom,
( ~ class_Rings_Ocomm__ring__1(u)
| class_Rings_Oring__1(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(233,axiom,
( ~ class_Groups_Oab__group__add(u)
| class_Groups_Ominus(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(234,axiom,
( ~ class_Rings_Ocomm__semiring__1(u)
| class_Power_Opower(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(235,axiom,
( ~ class_Groups_Ozero(u)
| class_Groups_Ozero(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(236,axiom,
( ~ class_Rings_Ocomm__ring(u)
| class_Rings_Oring(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(237,axiom,
( ~ class_Rings_Oidom(u)
| class_Rings_Oidom(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(238,axiom,
( ~ class_Rings_Ocomm__semiring__1(u)
| class_Groups_Oone(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(239,axiom,
( ~ class_Rings_Ocomm__semiring__1(u)
| class_Rings_Odvd(tc_Polynomial_Opoly(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(488,axiom,
( ~ class_Rings_Omult__zero(u)
| equal(hAPP(hAPP(c_Groups_Otimes__class_Otimes(u),v),c_Groups_Ozero__class_Ozero(u)),c_Groups_Ozero__class_Ozero(u)) ),
file('SWW272+1.p',unknown),
[] ).
cnf(1420,axiom,
equal(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_s____),v_pa____),
file('SWW272+1.p',unknown),
[] ).
cnf(1540,plain,
~ equal(v_s____,v_pa____),
inference(rew,[status(thm),theory(equality)],[148,162]),
[iquote('0:Rew:148.0,162.0')] ).
cnf(1631,plain,
equal(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),v_s____))),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_s____),v_pa____),
inference(rew,[status(thm),theory(equality)],[148,1420]),
[iquote('0:Rew:148.0,1420.0')] ).
cnf(23176,plain,
( ~ class_Rings_Omult__zero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),u),v_s____),v_s____) ),
inference(spr,[status(thm),theory(equality)],[148,488]),
[iquote('0:SpR:148.0,488.1')] ).
cnf(23187,plain,
equal(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),u),v_s____),v_s____),
inference(ssi,[status(thm)],[23176,232,135,142,133,122,116,114,113,127,111,134,132,115,110,109,1,143,136,124,117,140,130,108,131,128,112,107,138,125,121,118,106,126,123,129,141,120,139,137,119,204,229,213,202,238,221,195,191,181,231,192,224,203,233,206,239,215,236,225,226,222,199,234,219,207,182,220,214,223,212,237,211,235,210]),
[iquote('0:SSi:23176.0,232.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,204.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,229.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,213.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,202.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,238.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,221.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,195.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,191.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,181.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,231.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,192.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,224.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,203.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,233.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,206.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,239.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,215.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,236.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,225.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,226.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,222.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,199.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,234.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,219.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,207.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,182.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,220.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,214.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,223.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,212.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,237.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,211.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,235.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1,210.0,135.0,142.0,133.0,122.0,116.0,114.0,113.0,127.0,111.0,134.0,132.0,115.0,110.0,109.0,1.0,143.0,136.0,124.0,117.0,140.0,130.0,108.0,131.0,128.0,112.0,107.0,138.0,125.0,121.0,118.0,106.0,126.0,123.0,129.0,141.0,120.0,139.0,137.0,119.1')] ).
cnf(23189,plain,
equal(v_s____,v_pa____),
inference(rew,[status(thm),theory(equality)],[23187,1631]),
[iquote('0:Rew:23187.0,1631.0')] ).
cnf(23190,plain,
$false,
inference(mrr,[status(thm)],[23189,1540]),
[iquote('0:MRR:23189.0,1540.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SWW272+1 : TPTP v8.1.0. Released v5.2.0.
% 0.08/0.14 % Command : run_spass %d %s
% 0.15/0.36 % Computer : n025.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 600
% 0.15/0.36 % DateTime : Mon Jun 6 06:47:18 EDT 2022
% 0.15/0.36 % CPUTime :
% 8.41/8.63
% 8.41/8.63 SPASS V 3.9
% 8.41/8.63 SPASS beiseite: Proof found.
% 8.41/8.63 % SZS status Theorem
% 8.41/8.63 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.41/8.63 SPASS derived 18307 clauses, backtracked 0 clauses, performed 5 splits and kept 6051 clauses.
% 8.41/8.63 SPASS allocated 112876 KBytes.
% 8.41/8.63 SPASS spent 0:00:08.24 on the problem.
% 8.41/8.63 0:00:00.06 for the input.
% 8.41/8.63 0:00:00.48 for the FLOTTER CNF translation.
% 8.41/8.63 0:00:00.21 for inferences.
% 8.41/8.63 0:00:00.33 for the backtracking.
% 8.41/8.63 0:00:06.66 for the reduction.
% 8.41/8.63
% 8.41/8.63
% 8.41/8.63 Here is a proof with depth 1, length 84 :
% 8.41/8.63 % SZS output start Refutation
% See solution above
% 8.56/8.75 Formulae used in the proof : arity_Complex__Ocomplex__Groups_Ocancel__comm__monoid__add arity_Complex__Ocomplex__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct arity_Complex__Ocomplex__Rings_Odivision__ring__inverse__zero arity_Complex__Ocomplex__RealVector_Oreal__normed__algebra arity_Complex__Ocomplex__Groups_Ocancel__ab__semigroup__add arity_Complex__Ocomplex__Rings_Oring__1__no__zero__divisors arity_Complex__Ocomplex__Rings_Oring__no__zero__divisors arity_Complex__Ocomplex__Groups_Ocancel__semigroup__add arity_Complex__Ocomplex__Fields_Ofield__inverse__zero arity_Complex__Ocomplex__Groups_Oab__semigroup__mult arity_Complex__Ocomplex__Groups_Ocomm__monoid__mult arity_Complex__Ocomplex__Groups_Oab__semigroup__add arity_Complex__Ocomplex__Rings_Ono__zero__divisors arity_Complex__Ocomplex__Groups_Ocomm__monoid__add arity_Complex__Ocomplex__Rings_Ocomm__semiring__1 arity_Complex__Ocomplex__Rings_Ocomm__semiring__0 arity_Complex__Ocomplex__Rings_Odivision__ring arity_Complex__Ocomplex__Rings_Ocomm__semiring arity_Complex__Ocomplex__Groups_Oab__group__add arity_Complex__Ocomplex__Rings_Ozero__neq__one arity_Complex__Ocomplex__Groups_Omonoid__mult arity_Complex__Ocomplex__Rings_Ocomm__ring__1 arity_Complex__Ocomplex__Groups_Omonoid__add arity_Complex__Ocomplex__Rings_Osemiring__0 arity_Complex__Ocomplex__Groups_Ogroup__add arity_Complex__Ocomplex__Rings_Omult__zero arity_Complex__Ocomplex__Rings_Ocomm__ring arity_Complex__Ocomplex__Int_Oring__char__0 arity_Complex__Ocomplex__Rings_Osemiring arity_Complex__Ocomplex__Groups_Ouminus arity_Complex__Ocomplex__Rings_Oring__1 arity_Complex__Ocomplex__Groups_Ominus arity_Complex__Ocomplex__Fields_Ofield arity_Complex__Ocomplex__Power_Opower arity_Complex__Ocomplex__Groups_Ozero arity_Complex__Ocomplex__Rings_Oring arity_Complex__Ocomplex__Rings_Oidom arity_Complex__Ocomplex__Groups_Oone arity_Complex__Ocomplex__Rings_Odvd conj_0 fact_pne arity_Polynomial__Opoly__Groups_Ocancel__comm__monoid__add arity_Polynomial__Opoly__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct arity_Polynomial__Opoly__Groups_Ocancel__ab__semigroup__add arity_Polynomial__Opoly__Rings_Oring__1__no__zero__divisors arity_Polynomial__Opoly__Rings_Oring__no__zero__divisors arity_Polynomial__Opoly__Groups_Ocancel__semigroup__add arity_Polynomial__Opoly__Groups_Oab__semigroup__mult arity_Polynomial__Opoly__Groups_Ocomm__monoid__mult arity_Polynomial__Opoly__Groups_Oab__semigroup__add arity_Polynomial__Opoly__Rings_Ono__zero__divisors arity_Polynomial__Opoly__Groups_Ocomm__monoid__add arity_Polynomial__Opoly__Rings_Ocomm__semiring__1 arity_Polynomial__Opoly__Rings_Ocomm__semiring__0 arity_Polynomial__Opoly__Divides_Osemiring__div arity_Polynomial__Opoly__Rings_Ocomm__semiring arity_Polynomial__Opoly__Groups_Oab__group__add arity_Polynomial__Opoly__Rings_Ozero__neq__one arity_Polynomial__Opoly__Groups_Omonoid__mult arity_Polynomial__Opoly__Rings_Ocomm__ring__1 arity_Polynomial__Opoly__Groups_Omonoid__add arity_Polynomial__Opoly__Rings_Osemiring__0 arity_Polynomial__Opoly__Groups_Ogroup__add arity_Polynomial__Opoly__Divides_Oring__div arity_Polynomial__Opoly__Rings_Omult__zero arity_Polynomial__Opoly__Rings_Ocomm__ring arity_Polynomial__Opoly__Rings_Osemiring arity_Polynomial__Opoly__Groups_Ouminus arity_Polynomial__Opoly__Rings_Oring__1 arity_Polynomial__Opoly__Groups_Ominus arity_Polynomial__Opoly__Power_Opower arity_Polynomial__Opoly__Groups_Ozero arity_Polynomial__Opoly__Rings_Oring arity_Polynomial__Opoly__Rings_Oidom arity_Polynomial__Opoly__Groups_Oone arity_Polynomial__Opoly__Rings_Odvd fact_mult__zero__right fact_s
% 8.56/8.75
%------------------------------------------------------------------------------