%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG347-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n023.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:25 EDT 2022
% Result : Unsatisfiable 70.74s 71.01s
% Output : Refutation 72.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 21
% Syntax : Number of clauses : 50 ( 24 unt; 2 nHn; 50 RR)
% Number of literals : 83 ( 0 equ; 37 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(136,axiom,
( ~ c_lessequals(u,v,tc_nat)
| ~ c_lessequals(v,u,tc_nat)
| equal(u,v) ),
file('ALG347-1.p',unknown),
[] ).
cnf(138,axiom,
( equal(u,v)
| c_HOL_Oord__class_Oless(u,v,tc_nat)
| c_HOL_Oord__class_Oless(v,u,tc_nat) ),
file('ALG347-1.p',unknown),
[] ).
cnf(707,axiom,
( ~ c_HOL_Oord__class_Oless(u,v,tc_nat)
| c_lessequals(u,v,tc_nat) ),
file('ALG347-1.p',unknown),
[] ).
cnf(941,axiom,
( ~ class_HOL_Ozero(u)
| ~ c_HOL_Oord__class_Oless(c_Polynomial_Odegree(v,u),w,tc_nat)
| equal(c_Polynomial_Ocoeff(v,w,u),c_HOL_Ozero__class_Ozero(u)) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1002,axiom,
( ~ class_HOL_Ozero(u)
| equal(c_Polynomial_Ocoeff(c_Polynomial_OpCons(v,w,u),c_Suc(x),u),c_Polynomial_Ocoeff(w,x,u)) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1010,axiom,
( ~ class_HOL_Ozero(u)
| ~ equal(c_Polynomial_Ocoeff(v,c_Polynomial_Odegree(v,u),u),c_HOL_Ozero__class_Ozero(u))
| equal(v,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(u))) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1011,axiom,
( ~ class_HOL_Ozero(u)
| c_lessequals(c_Polynomial_Odegree(c_Polynomial_OpCons(v,w,u),u),c_Suc(c_Polynomial_Odegree(w,u)),tc_nat) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1017,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__0(u)
| ~ equal(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v,w,u),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(u)))
| equal(v,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(u))) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1026,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__0(u)
| class_OrderedGroup_Oab__semigroup__mult(u) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1027,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__0(u)
| class_OrderedGroup_Oab__semigroup__add(u) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1028,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__0(u)
| class_Ring__and__Field_Ocomm__semiring(u) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1029,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__0(u)
| class_OrderedGroup_Ocomm__monoid__add(u) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1030,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__0(u)
| class_Ring__and__Field_Osemiring__0(u) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1031,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__0(u)
| class_Ring__and__Field_Omult__zero(u) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1032,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__0(u)
| class_Ring__and__Field_Osemiring(u) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1033,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__0(u)
| class_OrderedGroup_Omonoid__add(u) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1034,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__0(u)
| class_HOL_Ozero(u) ),
file('ALG347-1.p',unknown),
[] ).
cnf(1127,axiom,
class_Ring__and__Field_Ocomm__semiring__0(t_a),
file('ALG347-1.p',unknown),
[] ).
cnf(1128,axiom,
equal(c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),c_Polynomial_Odegree(v_pa,t_a)),
file('ALG347-1.p',unknown),
[] ).
cnf(1129,axiom,
~ equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),v_pa),
file('ALG347-1.p',unknown),
[] ).
cnf(1130,axiom,
~ equal(c_Polynomial_Odegree(c_Polynomial_OpCons(v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),c_Suc(c_Polynomial_Odegree(v_pa,t_a))),
file('ALG347-1.p',unknown),
[] ).
cnf(1231,plain,
class_OrderedGroup_Oab__semigroup__mult(t_a),
inference(res,[status(thm),theory(equality)],[1127,1026]),
[iquote('0:Res:1127.0,1026.0')] ).
cnf(1232,plain,
class_OrderedGroup_Oab__semigroup__add(t_a),
inference(res,[status(thm),theory(equality)],[1127,1027]),
[iquote('0:Res:1127.0,1027.0')] ).
cnf(1233,plain,
class_Ring__and__Field_Ocomm__semiring(t_a),
inference(res,[status(thm),theory(equality)],[1127,1028]),
[iquote('0:Res:1127.0,1028.0')] ).
cnf(1234,plain,
class_OrderedGroup_Ocomm__monoid__add(t_a),
inference(res,[status(thm),theory(equality)],[1127,1029]),
[iquote('0:Res:1127.0,1029.0')] ).
cnf(1235,plain,
class_Ring__and__Field_Osemiring__0(t_a),
inference(res,[status(thm),theory(equality)],[1127,1030]),
[iquote('0:Res:1127.0,1030.0')] ).
cnf(1236,plain,
class_Ring__and__Field_Omult__zero(t_a),
inference(res,[status(thm),theory(equality)],[1127,1031]),
[iquote('0:Res:1127.0,1031.0')] ).
cnf(1237,plain,
class_Ring__and__Field_Osemiring(t_a),
inference(res,[status(thm),theory(equality)],[1127,1032]),
[iquote('0:Res:1127.0,1032.0')] ).
cnf(1238,plain,
class_OrderedGroup_Omonoid__add(t_a),
inference(res,[status(thm),theory(equality)],[1127,1033]),
[iquote('0:Res:1127.0,1033.0')] ).
cnf(1239,plain,
class_HOL_Ozero(t_a),
inference(res,[status(thm),theory(equality)],[1127,1034]),
[iquote('0:Res:1127.0,1034.0')] ).
cnf(1353,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__0(t_a)
| ~ equal(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,u,t_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) ),
inference(res,[status(thm),theory(equality)],[1017,1129]),
[iquote('0:Res:1017.2,1129.0')] ).
cnf(1442,plain,
( ~ c_lessequals(c_Suc(c_Polynomial_Odegree(v_pa,t_a)),c_Polynomial_Odegree(c_Polynomial_OpCons(v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),tc_nat)
| ~ c_lessequals(c_Polynomial_Odegree(c_Polynomial_OpCons(v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),c_Suc(c_Polynomial_Odegree(v_pa,t_a)),tc_nat) ),
inference(res,[status(thm),theory(equality)],[136,1130]),
[iquote('0:Res:136.2,1130.0')] ).
cnf(1443,plain,
( c_HOL_Oord__class_Oless(c_Suc(c_Polynomial_Odegree(v_pa,t_a)),c_Polynomial_Odegree(c_Polynomial_OpCons(v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),tc_nat)
| c_HOL_Oord__class_Oless(c_Polynomial_Odegree(c_Polynomial_OpCons(v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),c_Suc(c_Polynomial_Odegree(v_pa,t_a)),tc_nat) ),
inference(res,[status(thm),theory(equality)],[138,1130]),
[iquote('0:Res:138.2,1130.0')] ).
cnf(1484,plain,
~ equal(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,u,t_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
inference(mrr,[status(thm)],[1353,1127]),
[iquote('0:MRR:1353.0,1127.0')] ).
cnf(1505,plain,
c_HOL_Oord__class_Oless(c_Suc(c_Polynomial_Odegree(v_pa,t_a)),c_Polynomial_Odegree(c_Polynomial_OpCons(v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),tc_nat),
inference(spt,[spt(split,[position(s1)])],[1443]),
[iquote('1:Spt:1443.0')] ).
cnf(1575,plain,
c_lessequals(c_Suc(c_Polynomial_Odegree(v_pa,t_a)),c_Polynomial_Odegree(c_Polynomial_OpCons(v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),tc_nat),
inference(res,[status(thm),theory(equality)],[1505,707]),
[iquote('1:Res:1505.0,707.0')] ).
cnf(1586,plain,
~ c_lessequals(c_Polynomial_Odegree(c_Polynomial_OpCons(v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),c_Suc(c_Polynomial_Odegree(v_pa,t_a)),tc_nat),
inference(mrr,[status(thm)],[1442,1575]),
[iquote('1:MRR:1442.0,1575.0')] ).
cnf(43781,plain,
( ~ class_HOL_Ozero(t_a)
| c_lessequals(c_Polynomial_Odegree(c_Polynomial_OpCons(u,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),c_Suc(c_Polynomial_Odegree(v_pa,t_a)),tc_nat) ),
inference(spr,[status(thm),theory(equality)],[1128,1011]),
[iquote('0:SpR:1128.0,1011.1')] ).
cnf(43794,plain,
c_lessequals(c_Polynomial_Odegree(c_Polynomial_OpCons(u,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),c_Suc(c_Polynomial_Odegree(v_pa,t_a)),tc_nat),
inference(ssi,[status(thm)],[43781,1127,1232,1238,1237,1233,1231,1235,1236,1234,1239]),
[iquote('0:SSi:43781.0,1127.0,1232.0,1238.0,1237.0,1233.0,1231.0,1235.0,1236.0,1234.0,1239.0')] ).
cnf(43795,plain,
$false,
inference(unc,[status(thm)],[43794,1586]),
[iquote('1:UnC:43794.0,1586.0')] ).
cnf(43804,plain,
~ c_HOL_Oord__class_Oless(c_Suc(c_Polynomial_Odegree(v_pa,t_a)),c_Polynomial_Odegree(c_Polynomial_OpCons(v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),tc_nat),
inference(spt,[spt(split,[position(sa)])],[43795,1505]),
[iquote('1:Spt:43795.0,1443.0,1505.0')] ).
cnf(43805,plain,
c_HOL_Oord__class_Oless(c_Polynomial_Odegree(c_Polynomial_OpCons(v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),t_a),c_Suc(c_Polynomial_Odegree(v_pa,t_a)),tc_nat),
inference(spt,[spt(split,[position(s2)])],[1443]),
[iquote('1:Spt:43795.0,1443.1')] ).
cnf(77487,plain,
( ~ class_HOL_Ozero(t_a)
| equal(c_Polynomial_Ocoeff(c_Polynomial_OpCons(v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),t_a),c_Suc(c_Polynomial_Odegree(v_pa,t_a)),t_a),c_HOL_Ozero__class_Ozero(t_a)) ),
inference(res,[status(thm),theory(equality)],[43805,941]),
[iquote('1:Res:43805.0,941.1')] ).
cnf(77511,plain,
( ~ class_HOL_Ozero(t_a)
| equal(c_Polynomial_Ocoeff(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),c_Polynomial_Odegree(v_pa,t_a),t_a),c_HOL_Ozero__class_Ozero(t_a)) ),
inference(rew,[status(thm),theory(equality)],[1002,77487]),
[iquote('1:Rew:1002.1,77487.1')] ).
cnf(77512,plain,
equal(c_Polynomial_Ocoeff(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),c_Polynomial_Odegree(v_pa,t_a),t_a),c_HOL_Ozero__class_Ozero(t_a)),
inference(ssi,[status(thm)],[77511,1127,1232,1238,1237,1233,1231,1235,1236,1234,1239]),
[iquote('1:SSi:77511.0,1127.0,1232.0,1238.0,1237.0,1233.0,1231.0,1235.0,1236.0,1234.0,1239.0')] ).
cnf(98480,plain,
( ~ class_HOL_Ozero(t_a)
| ~ equal(c_Polynomial_Ocoeff(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),c_Polynomial_Odegree(v_pa,t_a),t_a),c_HOL_Ozero__class_Ozero(t_a))
| equal(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) ),
inference(spl,[status(thm),theory(equality)],[1128,1010]),
[iquote('0:SpL:1128.0,1010.1')] ).
cnf(99673,plain,
( ~ class_HOL_Ozero(t_a)
| ~ equal(c_HOL_Ozero__class_Ozero(t_a),c_HOL_Ozero__class_Ozero(t_a))
| equal(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) ),
inference(rew,[status(thm),theory(equality)],[77512,98480]),
[iquote('1:Rew:77512.0,98480.1')] ).
cnf(99674,plain,
( ~ class_HOL_Ozero(t_a)
| equal(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) ),
inference(obv,[status(thm),theory(equality)],[99673]),
[iquote('1:Obv:99673.1')] ).
cnf(99675,plain,
equal(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_pa,v_h,t_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
inference(ssi,[status(thm)],[99674,1127,1232,1238,1237,1233,1231,1235,1236,1234,1239]),
[iquote('1:SSi:99674.0,1127.0,1232.0,1238.0,1237.0,1233.0,1231.0,1235.0,1236.0,1234.0,1239.0')] ).
cnf(99676,plain,
$false,
inference(mrr,[status(thm)],[99675,1484]),
[iquote('1:MRR:99675.0,1484.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : ALG347-1 : TPTP v8.1.0. Released v4.1.0.
% 0.04/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Wed Jun 8 23:21:38 EDT 2022
% 0.12/0.33 % CPUTime :
% 70.74/71.01
% 70.74/71.01 SPASS V 3.9
% 70.74/71.01 SPASS beiseite: Proof found.
% 70.74/71.01 % SZS status Theorem
% 70.74/71.01 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 70.74/71.01 SPASS derived 85011 clauses, backtracked 2482 clauses, performed 5 splits and kept 18540 clauses.
% 70.74/71.01 SPASS allocated 134810 KBytes.
% 70.74/71.01 SPASS spent 0:1:10.56 on the problem.
% 70.74/71.01 0:00:00.08 for the input.
% 70.74/71.01 0:00:00.00 for the FLOTTER CNF translation.
% 70.74/71.01 0:00:00.99 for inferences.
% 70.74/71.01 0:00:01.69 for the backtracking.
% 70.74/71.01 0:01:07.03 for the reduction.
% 70.74/71.01
% 70.74/71.01
% 70.74/71.01 Here is a proof with depth 3, length 50 :
% 70.74/71.01 % SZS output start Refutation
% See solution above
% 72.77/72.96 Formulae used in the proof : cls_le__antisym_0 cls_linorder__neqE__nat_0 cls_termination__basic__simps_I5_J_0 cls_coeff__eq__0_0 cls_coeff__pCons__Suc_0 cls_leading__coeff__0__iff_0 cls_degree__pCons__le_0 cls_offset__poly__eq__0__iff_0 clsrel_Ring__and__Field_Ocomm__semiring__0_OrderedGroup_Oab__semigroup__mult clsrel_Ring__and__Field_Ocomm__semiring__0_OrderedGroup_Oab__semigroup__add clsrel_Ring__and__Field_Ocomm__semiring__0_Ring__and__Field_Ocomm__semiring clsrel_Ring__and__Field_Ocomm__semiring__0_OrderedGroup_Ocomm__monoid__add clsrel_Ring__and__Field_Ocomm__semiring__0_Ring__and__Field_Osemiring__0 clsrel_Ring__and__Field_Ocomm__semiring__0_Ring__and__Field_Omult__zero clsrel_Ring__and__Field_Ocomm__semiring__0_Ring__and__Field_Osemiring clsrel_Ring__and__Field_Ocomm__semiring__0_OrderedGroup_Omonoid__add clsrel_Ring__and__Field_Ocomm__semiring__0_HOL_Ozero tfree_tcs cls_conjecture_0 cls_conjecture_1 cls_conjecture_2
% 72.77/72.96
%------------------------------------------------------------------------------