%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG402-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n020.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 14 18:03:35 EDT 2022
% Result : Unsatisfiable 228.45s 228.65s
% Output : Refutation 234.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 45
% Syntax : Number of clauses : 60 ( 42 unt; 2 nHn; 60 RR)
% Number of literals : 84 ( 0 equ; 26 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 36 ( 35 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(88,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(u),v,u),c_HOL_Ozero__class_Ozero(u)) ),
file('ALG402-1.p',unknown),
[] ).
cnf(287,axiom,
( ~ class_OrderedGroup_Omonoid__mult(u)
| equal(c_HOL_Otimes__class_Otimes(v,c_HOL_Oone__class_Oone(u),u),v) ),
file('ALG402-1.p',unknown),
[] ).
cnf(323,axiom,
~ equal(c_Fact_Ofact__class_Ofact(u,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),
file('ALG402-1.p',unknown),
[] ).
cnf(385,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| ~ equal(c_HOL_Oinverse__class_Odivide(v,w,u),c_HOL_Oone__class_Oone(u))
| equal(v,w)
| equal(w,c_HOL_Ozero__class_Ozero(u)) ),
file('ALG402-1.p',unknown),
[] ).
cnf(447,axiom,
( ~ class_OrderedGroup_Omonoid__mult(u)
| equal(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(u),v,u),c_HOL_Oone__class_Oone(u)) ),
file('ALG402-1.p',unknown),
[] ).
cnf(716,axiom,
equal(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oone__class_Oone(tc_nat)),
file('ALG402-1.p',unknown),
[] ).
cnf(872,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| equal(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(u),v,u),c_HOL_Ozero__class_Ozero(u)) ),
file('ALG402-1.p',unknown),
[] ).
cnf(876,axiom,
( ~ class_OrderedGroup_Omonoid__mult(u)
| equal(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v,w,u),v,u),c_HOL_Otimes__class_Otimes(v,c_Power_Opower__class_Opower(v,w,u),u)) ),
file('ALG402-1.p',unknown),
[] ).
cnf(914,axiom,
( ~ class_OrderedGroup_Omonoid__mult(u)
| equal(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v,w,u),v,u),c_Power_Opower__class_Opower(v,c_Suc(w),u)) ),
file('ALG402-1.p',unknown),
[] ).
cnf(916,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| equal(c_HOL_Otimes__class_Otimes(v,c_Power_Opower__class_Opower(v,w,u),u),c_Power_Opower__class_Opower(v,c_Suc(w),u)) ),
file('ALG402-1.p',unknown),
[] ).
cnf(1012,axiom,
class_Ring__and__Field_Oring__1__no__zero__divisors(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1013,axiom,
class_Ring__and__Field_Oring__no__zero__divisors(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1014,axiom,
class_OrderedGroup_Ocancel__ab__semigroup__add(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1015,axiom,
class_OrderedGroup_Ocancel__semigroup__add(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1016,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1017,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1018,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1019,axiom,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1020,axiom,
class_OrderedGroup_Oab__semigroup__mult(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1021,axiom,
class_OrderedGroup_Ocomm__monoid__mult(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1022,axiom,
class_OrderedGroup_Oab__semigroup__add(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1023,axiom,
class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1024,axiom,
class_Ring__and__Field_Ocomm__semiring(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1025,axiom,
class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1026,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1027,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1028,axiom,
class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1029,axiom,
class_Ring__and__Field_Osemiring__0(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1030,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1031,axiom,
class_Ring__and__Field_Omult__zero(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1032,axiom,
class_Ring__and__Field_Ocomm__ring(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1033,axiom,
class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1034,axiom,
class_Ring__and__Field_Osemiring(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1035,axiom,
class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1036,axiom,
class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1037,axiom,
class_RealVector_Oreal__field(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1038,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1039,axiom,
class_Ring__and__Field_Oring(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1040,axiom,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1041,axiom,
class_Ring__and__Field_Odvd(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1042,axiom,
class_Int_Oring__char__0(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1043,axiom,
class_Int_Onumber__ring(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1044,axiom,
class_Power_Opower(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1045,axiom,
class_Int_Onumber(tc_Complex_Ocomplex),
file('ALG402-1.p',unknown),
[] ).
cnf(1046,axiom,
equal(c_HOL_Otimes__class_Otimes(u,c_Power_Opower__class_Opower(u,c_HOL_Ominus__class_Ominus(v_k____,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v,c_Power_Opower__class_Opower(v,c_HOL_Ominus__class_Ominus(v_k____,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
file('ALG402-1.p',unknown),
[] ).
cnf(1071,plain,
( ~ class_OrderedGroup_Omonoid__mult(u)
| equal(c_HOL_Otimes__class_Otimes(v,c_Power_Opower__class_Opower(v,w,u),u),c_Power_Opower__class_Opower(v,c_Suc(w),u)) ),
inference(rew,[status(thm),theory(equality)],[914,876]),
[iquote('0:Rew:914.1,876.1')] ).
cnf(1096,plain,
equal(c_HOL_Otimes__class_Otimes(u,c_Power_Opower__class_Opower(u,c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v,c_Power_Opower__class_Opower(v,c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(rew,[status(thm),theory(equality)],[716,1046]),
[iquote('0:Rew:716.0,1046.0')] ).
cnf(71378,plain,
( ~ class_Ring__and__Field_Ofield(u)
| ~ class_Ring__and__Field_Ofield(u)
| ~ equal(c_HOL_Oone__class_Oone(u),c_HOL_Ozero__class_Ozero(u))
| equal(c_HOL_Ozero__class_Ozero(u),v)
| equal(v,c_HOL_Ozero__class_Ozero(u)) ),
inference(spl,[status(thm),theory(equality)],[88,385]),
[iquote('0:SpL:88.1,385.1')] ).
cnf(71386,plain,
( ~ class_Ring__and__Field_Ofield(u)
| ~ equal(c_HOL_Oone__class_Oone(u),c_HOL_Ozero__class_Ozero(u))
| equal(v,c_HOL_Ozero__class_Ozero(u)) ),
inference(obv,[status(thm),theory(equality)],[71378]),
[iquote('0:Obv:71378.3')] ).
cnf(71387,plain,
( ~ class_Ring__and__Field_Ofield(u)
| ~ equal(c_HOL_Oone__class_Oone(u),c_HOL_Ozero__class_Ozero(u)) ),
inference(aed,[status(thm),theory(equality)],[323,71386]),
[iquote('0:AED:323.0,71386.2')] ).
cnf(167179,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)
| equal(c_HOL_Otimes__class_Otimes(u,c_Power_Opower__class_Opower(u,c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(spr,[status(thm),theory(equality)],[1096,872]),
[iquote('0:SpR:1096.0,872.1')] ).
cnf(167309,plain,
( ~ class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex)
| equal(c_HOL_Otimes__class_Otimes(u,c_Power_Opower__class_Opower(u,c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)) ),
inference(spr,[status(thm),theory(equality)],[447,1096]),
[iquote('0:SpR:447.1,1096.0')] ).
cnf(167348,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)
| equal(c_Power_Opower__class_Opower(u,c_Suc(c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat)),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[916,167179]),
[iquote('0:Rew:916.1,167179.1')] ).
cnf(167349,plain,
equal(c_Power_Opower__class_Opower(u,c_Suc(c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat)),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(ssi,[status(thm)],[167348,1037,1042,1028,1012,1032,1025,1024,1022,1020,1014,1035,1021,1015,1013,1041,1039,1034,1029,1036,1030,1027,1016,1031,1019,1045,1033,1044,1043,1026,1023,1040,1038,1018,1017]),
[iquote('0:SSi:167348.0,1037.0,1042.0,1028.0,1012.0,1032.0,1025.0,1024.0,1022.0,1020.0,1014.0,1035.0,1021.0,1015.0,1013.0,1041.0,1039.0,1034.0,1029.0,1036.0,1030.0,1027.0,1016.0,1031.0,1019.0,1045.0,1033.0,1044.0,1043.0,1026.0,1023.0,1040.0,1038.0,1018.0,1017.0')] ).
cnf(167359,plain,
( ~ class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex)
| equal(c_Power_Opower__class_Opower(u,c_Suc(c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat)),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[1071,167309,287]),
[iquote('0:Rew:1071.1,167309.1,287.1,167309.1')] ).
cnf(167360,plain,
( ~ class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex)
| equal(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[167349,167359]),
[iquote('0:Rew:167349.0,167359.1')] ).
cnf(167361,plain,
equal(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(ssi,[status(thm)],[167360,1037,1042,1028,1012,1032,1025,1024,1022,1020,1014,1035,1021,1015,1013,1041,1039,1034,1029,1036,1030,1027,1016,1031,1019,1045,1033,1044,1043,1026,1023,1040,1038,1018,1017]),
[iquote('0:SSi:167360.0,1037.0,1042.0,1028.0,1012.0,1032.0,1025.0,1024.0,1022.0,1020.0,1014.0,1035.0,1021.0,1015.0,1013.0,1041.0,1039.0,1034.0,1029.0,1036.0,1030.0,1027.0,1016.0,1031.0,1019.0,1045.0,1033.0,1044.0,1043.0,1026.0,1023.0,1040.0,1038.0,1018.0,1017.0')] ).
cnf(167643,plain,
( ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| ~ equal(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(spl,[status(thm),theory(equality)],[167361,71387]),
[iquote('0:SpL:167361.0,71387.1')] ).
cnf(167658,plain,
~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
inference(obv,[status(thm),theory(equality)],[167643]),
[iquote('0:Obv:167643.1')] ).
cnf(167659,plain,
$false,
inference(ssi,[status(thm)],[167658,1037,1042,1028,1012,1032,1025,1024,1022,1020,1014,1035,1021,1015,1013,1041,1039,1034,1029,1036,1030,1027,1016,1031,1019,1045,1033,1044,1043,1026,1023,1040,1038,1018,1017]),
[iquote('0:SSi:167658.0,1037.0,1042.0,1028.0,1012.0,1032.0,1025.0,1024.0,1022.0,1020.0,1014.0,1035.0,1021.0,1015.0,1013.0,1041.0,1039.0,1034.0,1029.0,1036.0,1030.0,1027.0,1016.0,1031.0,1019.0,1045.0,1033.0,1044.0,1043.0,1026.0,1023.0,1040.0,1038.0,1018.0,1017.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG402-1 : TPTP v8.1.0. Released v4.1.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Wed Jun 8 13:06:06 EDT 2022
% 0.13/0.34 % CPUTime :
% 228.45/228.65
% 228.45/228.65 SPASS V 3.9
% 228.45/228.65 SPASS beiseite: Proof found.
% 228.45/228.65 % SZS status Theorem
% 228.45/228.65 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 228.45/228.65 SPASS derived 134336 clauses, backtracked 0 clauses, performed 0 splits and kept 25211 clauses.
% 228.45/228.65 SPASS allocated 171116 KBytes.
% 228.45/228.65 SPASS spent 0:3:48.11 on the problem.
% 228.45/228.65 0:00:00.08 for the input.
% 228.45/228.65 0:00:00.00 for the FLOTTER CNF translation.
% 228.45/228.65 0:00:01.59 for inferences.
% 228.45/228.65 0:00:00.00 for the backtracking.
% 228.45/228.65 0:3:45.45 for the reduction.
% 228.45/228.65
% 228.45/228.65
% 228.45/228.65 Here is a proof with depth 2, length 60 :
% 228.45/228.65 % SZS output start Refutation
% See solution above
% 234.38/234.60 Formulae used in the proof : cls_divide__zero__left_0 cls_mult__1__right_0 cls_fact__nonzero__nat_0 cls_right__inverse__eq_0 cls_power__one_0 cls_One__nat__def_0 cls_class__semiring_Osemiring__rules_I9_J_0 cls_power__commutes_0 cls_power__Suc2_0 cls_class__semiring_Osemiring__rules_I35_J_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__OrderedGroup_Ocancel__ab__semigroup__add clsarity_Complex__Ocomplex__OrderedGroup_Ocancel__semigroup__add 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__OrderedGroup_Oab__semigroup__add clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__ring clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring clsarity_Complex__Ocomplex__RealVector_Oreal__normed__field clsarity_Complex__Ocomplex__OrderedGroup_Ocomm__monoid__add 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__Ring__and__Field_Ocomm__ring clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__mult clsarity_Complex__Ocomplex__Ring__and__Field_Osemiring clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__add clsarity_Complex__Ocomplex__OrderedGroup_Ogroup__add clsarity_Complex__Ocomplex__RealVector_Oreal__field 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__Int_Onumber cls_conjecture_0
% 234.38/234.60
%------------------------------------------------------------------------------