%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM925+7 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n028.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 : Mon Jul 18 14:31:46 EDT 2022
% Result : Theorem 68.17s 68.36s
% Output : Refutation 71.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 89
% Syntax : Number of clauses : 142 ( 114 unt; 0 nHn; 142 RR)
% Number of literals : 175 ( 0 equ; 39 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 60 ( 59 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 8 con; 0-4 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
semiri456707255roduct(int),
file('NUM925+7.p',unknown),
[] ).
cnf(2,axiom,
ordere223160158up_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(3,axiom,
ordere236663937imp_le(int),
file('NUM925+7.p',unknown),
[] ).
cnf(4,axiom,
linord893533164strict(int),
file('NUM925+7.p',unknown),
[] ).
cnf(5,axiom,
linord626643107strict(int),
file('NUM925+7.p',unknown),
[] ).
cnf(6,axiom,
linord20386208strict(int),
file('NUM925+7.p',unknown),
[] ).
cnf(7,axiom,
ordere779506340up_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(8,axiom,
ordere142940540dd_abs(int),
file('NUM925+7.p',unknown),
[] ).
cnf(9,axiom,
ordere216010020id_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(10,axiom,
linord219039673up_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(11,axiom,
cancel146912293up_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(12,axiom,
ring_11004092258visors(int),
file('NUM925+7.p',unknown),
[] ).
cnf(13,axiom,
ordere453448008miring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(14,axiom,
linord581940658strict(int),
file('NUM925+7.p',unknown),
[] ).
cnf(15,axiom,
ring_n68954251visors(int),
file('NUM925+7.p',unknown),
[] ).
cnf(16,axiom,
ordere1490568538miring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(17,axiom,
linord1278240602ring_1(int),
file('NUM925+7.p',unknown),
[] ).
cnf(18,axiom,
ordered_ab_group_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(19,axiom,
cancel_semigroup_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(20,axiom,
linordered_semiring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(21,axiom,
linordered_semidom(int),
file('NUM925+7.p',unknown),
[] ).
cnf(22,axiom,
ab_semigroup_mult(int),
file('NUM925+7.p',unknown),
[] ).
cnf(23,axiom,
comm_monoid_mult(int),
file('NUM925+7.p',unknown),
[] ).
cnf(24,axiom,
ab_semigroup_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(25,axiom,
ordered_semiring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(26,axiom,
ordered_ring_abs(int),
file('NUM925+7.p',unknown),
[] ).
cnf(27,axiom,
no_zero_divisors(int),
file('NUM925+7.p',unknown),
[] ).
cnf(28,axiom,
comm_monoid_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(29,axiom,
linordered_ring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(30,axiom,
linordered_idom(int),
file('NUM925+7.p',unknown),
[] ).
cnf(31,axiom,
comm_semiring_1(int),
file('NUM925+7.p',unknown),
[] ).
cnf(32,axiom,
comm_semiring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(33,axiom,
semiring_char_0(int),
file('NUM925+7.p',unknown),
[] ).
cnf(34,axiom,
number_semiring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(35,axiom,
ab_group_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(36,axiom,
zero_neq_one(int),
file('NUM925+7.p',unknown),
[] ).
cnf(37,axiom,
ordered_ring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(38,axiom,
linorder(int),
file('NUM925+7.p',unknown),
[] ).
cnf(39,axiom,
monoid_mult(int),
file('NUM925+7.p',unknown),
[] ).
cnf(40,axiom,
comm_ring_1(int),
file('NUM925+7.p',unknown),
[] ).
cnf(41,axiom,
monoid_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(42,axiom,
semiring_1(int),
file('NUM925+7.p',unknown),
[] ).
cnf(43,axiom,
semiring_0(int),
file('NUM925+7.p',unknown),
[] ).
cnf(44,axiom,
group_add(int),
file('NUM925+7.p',unknown),
[] ).
cnf(45,axiom,
mult_zero(int),
file('NUM925+7.p',unknown),
[] ).
cnf(46,axiom,
comm_ring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(47,axiom,
order(int),
file('NUM925+7.p',unknown),
[] ).
cnf(48,axiom,
ring_char_0(int),
file('NUM925+7.p',unknown),
[] ).
cnf(49,axiom,
number_ring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(50,axiom,
semiring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(51,axiom,
ring_1(int),
file('NUM925+7.p',unknown),
[] ).
cnf(52,axiom,
power(int),
file('NUM925+7.p',unknown),
[] ).
cnf(53,axiom,
zero(int),
file('NUM925+7.p',unknown),
[] ).
cnf(54,axiom,
ring(int),
file('NUM925+7.p',unknown),
[] ).
cnf(55,axiom,
idom(int),
file('NUM925+7.p',unknown),
[] ).
cnf(56,axiom,
number(int),
file('NUM925+7.p',unknown),
[] ).
cnf(57,axiom,
one(int),
file('NUM925+7.p',unknown),
[] ).
cnf(58,axiom,
dvd(int),
file('NUM925+7.p',unknown),
[] ).
cnf(156,axiom,
equal(zero_zero(int),pls),
file('NUM925+7.p',unknown),
[] ).
cnf(158,axiom,
~ equal(pls,min),
file('NUM925+7.p',unknown),
[] ).
cnf(159,axiom,
equal(bit1(min),min),
file('NUM925+7.p',unknown),
[] ).
cnf(160,axiom,
equal(succ(min),pls),
file('NUM925+7.p',unknown),
[] ).
cnf(161,axiom,
equal(ti(int,min),min),
file('NUM925+7.p',unknown),
[] ).
cnf(176,axiom,
equal(bit1(pls),succ(pls)),
file('NUM925+7.p',unknown),
[] ).
cnf(179,axiom,
equal(number_number_of(int,pls),zero_zero(int)),
file('NUM925+7.p',unknown),
[] ).
cnf(190,axiom,
equal(succ(bit0(u)),bit1(u)),
file('NUM925+7.p',unknown),
[] ).
cnf(193,axiom,
equal(bit0(ti(int,u)),bit0(u)),
file('NUM925+7.p',unknown),
[] ).
cnf(195,axiom,
equal(bit1(ti(int,u)),bit1(u)),
file('NUM925+7.p',unknown),
[] ).
cnf(196,axiom,
equal(ti(int,bit1(u)),bit1(u)),
file('NUM925+7.p',unknown),
[] ).
cnf(197,axiom,
equal(nat_1(ti(int,u)),nat_1(u)),
file('NUM925+7.p',unknown),
[] ).
cnf(200,axiom,
equal(ti(int,succ(u)),succ(u)),
file('NUM925+7.p',unknown),
[] ).
cnf(205,axiom,
equal(number_number_of(int,bit1(pls)),one_one(int)),
file('NUM925+7.p',unknown),
[] ).
cnf(209,axiom,
equal(ti(int,u),number_number_of(int,u)),
file('NUM925+7.p',unknown),
[] ).
cnf(215,axiom,
equal(bit0(succ(u)),succ(bit1(u))),
file('NUM925+7.p',unknown),
[] ).
cnf(220,axiom,
equal(plus_plus(int,u,pls),ti(int,u)),
file('NUM925+7.p',unknown),
[] ).
cnf(221,axiom,
equal(plus_plus(int,pls,u),ti(int,u)),
file('NUM925+7.p',unknown),
[] ).
cnf(225,axiom,
equal(nat_1(number_number_of(int,u)),number_number_of(nat,u)),
file('NUM925+7.p',unknown),
[] ).
cnf(226,axiom,
equal(plus_plus(int,u,one_one(int)),succ(u)),
file('NUM925+7.p',unknown),
[] ).
cnf(240,axiom,
equal(plus_plus(int,u,v),plus_plus(int,v,u)),
file('NUM925+7.p',unknown),
[] ).
cnf(271,axiom,
( ~ equal(ti(int,u),pls)
| equal(bit0(u),pls) ),
file('NUM925+7.p',unknown),
[] ).
cnf(280,axiom,
( ~ equal(bit1(u),min)
| equal(ti(int,u),min) ),
file('NUM925+7.p',unknown),
[] ).
cnf(291,axiom,
equal(plus_plus(int,plus_plus(int,one_one(int),u),u),bit1(u)),
file('NUM925+7.p',unknown),
[] ).
cnf(304,axiom,
( ~ ordere142940540dd_abs(u)
| equal(ti(u,abs_abs(u,v)),abs_abs(u,v)) ),
file('NUM925+7.p',unknown),
[] ).
cnf(346,axiom,
( ~ ordere142940540dd_abs(u)
| equal(abs_abs(u,abs_abs(u,v)),abs_abs(u,v)) ),
file('NUM925+7.p',unknown),
[] ).
cnf(365,axiom,
equal(plus_plus(int,bit1(u),bit1(v)),bit0(plus_plus(int,u,succ(v)))),
file('NUM925+7.p',unknown),
[] ).
cnf(446,axiom,
( ~ equal(ti(int,u),number_number_of(int,min))
| equal(abs_abs(int,u),one_one(int)) ),
file('NUM925+7.p',unknown),
[] ).
cnf(488,axiom,
equal(abs_abs(int,hAPP(nat,int,semiring_1_of_nat(int),u)),hAPP(nat,int,semiring_1_of_nat(int),u)),
file('NUM925+7.p',unknown),
[] ).
cnf(686,axiom,
( ~ ring_11004092258visors(u)
| ~ equal(hAPP(nat,u,power_power(u,v),w),zero_zero(u))
| equal(ti(u,v),zero_zero(u)) ),
file('NUM925+7.p',unknown),
[] ).
cnf(769,axiom,
equal(hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))),zero_zero(int)),
file('NUM925+7.p',unknown),
[] ).
cnf(1684,plain,
equal(number_number_of(int,pls),pls),
inference(rew,[status(thm),theory(equality)],[156,179]),
[iquote('0:Rew:156.0,179.0')] ).
cnf(1689,plain,
equal(number_number_of(int,min),min),
inference(rew,[status(thm),theory(equality)],[209,161]),
[iquote('0:Rew:209.0,161.0')] ).
cnf(1700,plain,
equal(number_number_of(int,succ(pls)),one_one(int)),
inference(rew,[status(thm),theory(equality)],[176,205]),
[iquote('0:Rew:176.0,205.0')] ).
cnf(1702,plain,
equal(number_number_of(int,succ(u)),succ(u)),
inference(rew,[status(thm),theory(equality)],[209,200]),
[iquote('0:Rew:209.0,200.0')] ).
cnf(1703,plain,
equal(one_one(int),succ(pls)),
inference(rew,[status(thm),theory(equality)],[1702,1700]),
[iquote('0:Rew:1702.0,1700.0')] ).
cnf(1707,plain,
equal(nat_1(number_number_of(int,u)),nat_1(u)),
inference(rew,[status(thm),theory(equality)],[209,197]),
[iquote('0:Rew:209.0,197.0')] ).
cnf(1708,plain,
equal(number_number_of(int,bit1(u)),bit1(u)),
inference(rew,[status(thm),theory(equality)],[209,196]),
[iquote('0:Rew:209.0,196.0')] ).
cnf(1709,plain,
equal(bit1(number_number_of(int,u)),bit1(u)),
inference(rew,[status(thm),theory(equality)],[209,195]),
[iquote('0:Rew:209.0,195.0')] ).
cnf(1711,plain,
equal(bit0(number_number_of(int,u)),bit0(u)),
inference(rew,[status(thm),theory(equality)],[209,193]),
[iquote('0:Rew:209.0,193.0')] ).
cnf(1716,plain,
equal(plus_plus(int,u,succ(pls)),succ(u)),
inference(rew,[status(thm),theory(equality)],[1703,226]),
[iquote('0:Rew:1703.0,226.0')] ).
cnf(1717,plain,
equal(number_number_of(nat,u),nat_1(u)),
inference(rew,[status(thm),theory(equality)],[1707,225]),
[iquote('0:Rew:1707.0,225.0')] ).
cnf(1721,plain,
equal(plus_plus(int,pls,u),number_number_of(int,u)),
inference(rew,[status(thm),theory(equality)],[209,221]),
[iquote('0:Rew:209.0,221.0')] ).
cnf(1722,plain,
equal(plus_plus(int,u,pls),number_number_of(int,u)),
inference(rew,[status(thm),theory(equality)],[209,220]),
[iquote('0:Rew:209.0,220.0')] ).
cnf(1735,plain,
( ~ equal(bit1(u),min)
| equal(number_number_of(int,u),min) ),
inference(rew,[status(thm),theory(equality)],[209,280]),
[iquote('0:Rew:209.0,280.1')] ).
cnf(1743,plain,
( ~ equal(number_number_of(int,u),pls)
| equal(bit0(u),pls) ),
inference(rew,[status(thm),theory(equality)],[209,271]),
[iquote('0:Rew:209.0,271.0')] ).
cnf(1752,plain,
equal(plus_plus(int,u,plus_plus(int,succ(pls),u)),bit1(u)),
inference(rew,[status(thm),theory(equality)],[240,291,1703]),
[iquote('0:Rew:240.0,291.0,1703.0,291.0')] ).
cnf(1774,plain,
( ~ equal(number_number_of(int,u),min)
| equal(abs_abs(int,u),succ(pls)) ),
inference(rew,[status(thm),theory(equality)],[1703,446,209,1689]),
[iquote('0:Rew:1703.0,446.1,209.0,446.0,1689.0,446.0')] ).
cnf(1928,plain,
equal(hAPP(nat,int,power_power(int,plus_plus(int,succ(pls),hAPP(nat,int,semiring_1_of_nat(int),n))),nat_1(succ(succ(pls)))),pls),
inference(rew,[status(thm),theory(equality)],[1703,769,1717,176,215,156]),
[iquote('0:Rew:1703.0,769.0,1717.0,769.0,176.0,769.0,215.0,769.0,176.0,769.0,156.0,769.0')] ).
cnf(2643,plain,
equal(plus_plus(int,succ(pls),u),succ(u)),
inference(spr,[status(thm),theory(equality)],[240,1716]),
[iquote('0:SpR:240.0,1716.0')] ).
cnf(2659,plain,
equal(hAPP(nat,int,power_power(int,succ(hAPP(nat,int,semiring_1_of_nat(int),n))),nat_1(succ(succ(pls)))),pls),
inference(rew,[status(thm),theory(equality)],[2643,1928]),
[iquote('0:Rew:2643.0,1928.0')] ).
cnf(2689,plain,
equal(plus_plus(int,u,succ(u)),bit1(u)),
inference(rew,[status(thm),theory(equality)],[2643,1752]),
[iquote('0:Rew:2643.0,1752.0')] ).
cnf(2904,plain,
( ~ equal(bit1(pls),min)
| equal(pls,min) ),
inference(spr,[status(thm),theory(equality)],[1735,1684]),
[iquote('0:SpR:1735.1,1684.0')] ).
cnf(2932,plain,
( ~ equal(succ(pls),min)
| equal(pls,min) ),
inference(rew,[status(thm),theory(equality)],[176,2904]),
[iquote('0:Rew:176.0,2904.0')] ).
cnf(2933,plain,
~ equal(succ(pls),min),
inference(mrr,[status(thm)],[2932,158]),
[iquote('0:MRR:2932.1,158.0')] ).
cnf(3022,plain,
( ~ equal(succ(u),pls)
| equal(bit0(succ(u)),pls) ),
inference(spl,[status(thm),theory(equality)],[1702,1743]),
[iquote('0:SpL:1702.0,1743.0')] ).
cnf(3033,plain,
( ~ equal(succ(u),pls)
| equal(succ(bit1(u)),pls) ),
inference(rew,[status(thm),theory(equality)],[215,3022]),
[iquote('0:Rew:215.0,3022.1')] ).
cnf(8888,plain,
( ~ equal(succ(u),pls)
| equal(plus_plus(int,bit1(u),pls),bit1(bit1(u))) ),
inference(spr,[status(thm),theory(equality)],[3033,2689]),
[iquote('0:SpR:3033.1,2689.0')] ).
cnf(8916,plain,
( ~ equal(succ(u),pls)
| equal(bit1(bit1(u)),bit1(u)) ),
inference(rew,[status(thm),theory(equality)],[1708,8888,1721,240]),
[iquote('0:Rew:1708.0,8888.1,1721.0,8888.1,240.0,8888.1')] ).
cnf(11244,plain,
( ~ equal(bit1(u),min)
| ~ equal(min,min)
| equal(abs_abs(int,u),succ(pls)) ),
inference(spl,[status(thm),theory(equality)],[1735,1774]),
[iquote('0:SpL:1735.1,1774.0')] ).
cnf(11258,plain,
( ~ equal(bit1(u),min)
| equal(abs_abs(int,u),succ(pls)) ),
inference(obv,[status(thm),theory(equality)],[11244]),
[iquote('0:Obv:11244.1')] ).
cnf(17328,plain,
( ~ ordere142940540dd_abs(int)
| ~ equal(bit1(abs_abs(int,u)),min)
| equal(abs_abs(int,u),succ(pls)) ),
inference(spr,[status(thm),theory(equality)],[346,11258]),
[iquote('0:SpR:346.1,11258.1')] ).
cnf(17347,plain,
( ~ equal(bit1(abs_abs(int,u)),min)
| equal(abs_abs(int,u),succ(pls)) ),
inference(ssi,[status(thm)],[17328,40,26,17,5,57,53,51,48,46,32,16,12,11,4,38,35,33,28,20,15,36,29,23,13,7,54,43,25,24,22,55,41,18,2,50,27,1,45,19,44,3,56,42,10,47,39,37,34,9,52,6,58,8,21,14,31,49,30]),
[iquote('0:SSi:17328.0,40.0,26.0,17.0,5.0,57.0,53.0,51.0,48.0,46.0,32.0,16.0,12.0,11.0,4.0,38.0,35.0,33.0,28.0,20.0,15.0,36.0,29.0,23.0,13.0,7.0,54.0,43.0,25.0,24.0,22.0,55.0,41.0,18.0,2.0,50.0,27.0,1.0,45.0,19.0,44.0,3.0,56.0,42.0,10.0,47.0,39.0,37.0,34.0,9.0,52.0,6.0,58.0,8.0,21.0,14.0,31.0,49.0,30.0')] ).
cnf(18686,plain,
( ~ ordere142940540dd_abs(int)
| equal(number_number_of(int,abs_abs(int,u)),abs_abs(int,u)) ),
inference(spr,[status(thm),theory(equality)],[304,209]),
[iquote('0:SpR:304.1,209.0')] ).
cnf(18716,plain,
equal(number_number_of(int,abs_abs(int,u)),abs_abs(int,u)),
inference(ssi,[status(thm)],[18686,40,26,17,5,57,53,51,48,46,32,16,12,11,4,38,35,33,28,20,15,36,29,23,13,7,54,43,25,24,22,55,41,18,2,50,27,1,45,19,44,3,56,42,10,47,39,37,34,9,52,6,58,8,21,14,31,49,30]),
[iquote('0:SSi:18686.0,40.0,26.0,17.0,5.0,57.0,53.0,51.0,48.0,46.0,32.0,16.0,12.0,11.0,4.0,38.0,35.0,33.0,28.0,20.0,15.0,36.0,29.0,23.0,13.0,7.0,54.0,43.0,25.0,24.0,22.0,55.0,41.0,18.0,2.0,50.0,27.0,1.0,45.0,19.0,44.0,3.0,56.0,42.0,10.0,47.0,39.0,37.0,34.0,9.0,52.0,6.0,58.0,8.0,21.0,14.0,31.0,49.0,30.0')] ).
cnf(18741,plain,
( ~ equal(bit1(abs_abs(int,u)),min)
| equal(abs_abs(int,u),min) ),
inference(spr,[status(thm),theory(equality)],[18716,1735]),
[iquote('0:SpR:18716.0,1735.1')] ).
cnf(18774,plain,
( ~ equal(bit1(abs_abs(int,u)),min)
| equal(succ(pls),min) ),
inference(rew,[status(thm),theory(equality)],[17347,18741]),
[iquote('0:Rew:17347.1,18741.1')] ).
cnf(18775,plain,
~ equal(bit1(abs_abs(int,u)),min),
inference(mrr,[status(thm)],[18774,2933]),
[iquote('0:MRR:18774.1,2933.0')] ).
cnf(24775,plain,
equal(bit0(plus_plus(int,u,succ(min))),plus_plus(int,bit1(u),min)),
inference(spr,[status(thm),theory(equality)],[159,365]),
[iquote('0:SpR:159.0,365.0')] ).
cnf(24815,plain,
equal(bit0(plus_plus(int,min,succ(u))),plus_plus(int,min,bit1(u))),
inference(spr,[status(thm),theory(equality)],[159,365]),
[iquote('0:SpR:159.0,365.0')] ).
cnf(24857,plain,
equal(plus_plus(int,min,bit1(u)),bit0(u)),
inference(rew,[status(thm),theory(equality)],[1711,24775,1722,160,240]),
[iquote('0:Rew:1711.0,24775.0,1722.0,24775.0,160.0,24775.0,240.0,24775.0')] ).
cnf(24858,plain,
equal(bit0(plus_plus(int,min,succ(u))),bit0(u)),
inference(rew,[status(thm),theory(equality)],[24857,24815]),
[iquote('0:Rew:24857.0,24815.0')] ).
cnf(25060,plain,
equal(bit1(plus_plus(int,min,succ(u))),succ(bit0(u))),
inference(spr,[status(thm),theory(equality)],[24858,190]),
[iquote('0:SpR:24858.0,190.0')] ).
cnf(25175,plain,
equal(bit1(plus_plus(int,min,succ(u))),bit1(u)),
inference(rew,[status(thm),theory(equality)],[190,25060]),
[iquote('0:Rew:190.0,25060.0')] ).
cnf(25423,plain,
( ~ equal(succ(u),pls)
| equal(bit1(plus_plus(int,min,pls)),bit1(bit1(u))) ),
inference(spr,[status(thm),theory(equality)],[3033,25175]),
[iquote('0:SpR:3033.1,25175.0')] ).
cnf(25546,plain,
( ~ equal(succ(u),pls)
| equal(bit1(u),min) ),
inference(rew,[status(thm),theory(equality)],[159,25423,1709,1722,8916]),
[iquote('0:Rew:159.0,25423.1,1709.0,25423.1,1722.0,25423.1,8916.1,25423.1')] ).
cnf(25978,plain,
( ~ equal(succ(abs_abs(int,u)),pls)
| ~ equal(min,min) ),
inference(spl,[status(thm),theory(equality)],[25546,18775]),
[iquote('0:SpL:25546.1,18775.0')] ).
cnf(25990,plain,
~ equal(succ(abs_abs(int,u)),pls),
inference(obv,[status(thm),theory(equality)],[25978]),
[iquote('0:Obv:25978.1')] ).
cnf(51082,plain,
~ equal(succ(hAPP(nat,int,semiring_1_of_nat(int),u)),pls),
inference(spl,[status(thm),theory(equality)],[488,25990]),
[iquote('0:SpL:488.0,25990.0')] ).
cnf(136090,plain,
( ~ ring_11004092258visors(int)
| ~ equal(zero_zero(int),pls)
| equal(ti(int,succ(hAPP(nat,int,semiring_1_of_nat(int),n))),zero_zero(int)) ),
inference(spl,[status(thm),theory(equality)],[2659,686]),
[iquote('0:SpL:2659.0,686.1')] ).
cnf(136109,plain,
( ~ ring_11004092258visors(int)
| ~ equal(pls,pls)
| equal(succ(hAPP(nat,int,semiring_1_of_nat(int),n)),pls) ),
inference(rew,[status(thm),theory(equality)],[1702,136090,209,156]),
[iquote('0:Rew:1702.0,136090.2,209.0,136090.2,156.0,136090.2,156.0,136090.1')] ).
cnf(136110,plain,
( ~ ring_11004092258visors(int)
| equal(succ(hAPP(nat,int,semiring_1_of_nat(int),n)),pls) ),
inference(obv,[status(thm),theory(equality)],[136109]),
[iquote('0:Obv:136109.1')] ).
cnf(136111,plain,
equal(succ(hAPP(nat,int,semiring_1_of_nat(int),n)),pls),
inference(ssi,[status(thm)],[136110,40,26,17,5,57,53,51,48,46,32,16,12,11,4,38,35,33,28,20,15,36,29,23,13,7,54,43,25,24,22,55,41,18,2,50,27,1,45,19,44,3,56,42,10,47,39,37,34,9,52,6,58,8,21,14,31,49,30]),
[iquote('0:SSi:136110.0,40.0,26.0,17.0,5.0,57.0,53.0,51.0,48.0,46.0,32.0,16.0,12.0,11.0,4.0,38.0,35.0,33.0,28.0,20.0,15.0,36.0,29.0,23.0,13.0,7.0,54.0,43.0,25.0,24.0,22.0,55.0,41.0,18.0,2.0,50.0,27.0,1.0,45.0,19.0,44.0,3.0,56.0,42.0,10.0,47.0,39.0,37.0,34.0,9.0,52.0,6.0,58.0,8.0,21.0,14.0,31.0,49.0,30.0')] ).
cnf(136112,plain,
$false,
inference(mrr,[status(thm)],[136111,51082]),
[iquote('0:MRR:136111.0,51082.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM925+7 : TPTP v8.1.0. Released v5.3.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n028.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 : Thu Jul 7 05:00:38 EDT 2022
% 0.13/0.34 % CPUTime :
% 68.17/68.36
% 68.17/68.36 SPASS V 3.9
% 68.17/68.36 SPASS beiseite: Proof found.
% 68.17/68.36 % SZS status Theorem
% 68.17/68.36 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 68.17/68.36 SPASS derived 84997 clauses, backtracked 2747 clauses, performed 3 splits and kept 20473 clauses.
% 68.17/68.36 SPASS allocated 185912 KBytes.
% 68.17/68.36 SPASS spent 0:01:07.87 on the problem.
% 68.17/68.36 0:00:00.07 for the input.
% 68.17/68.36 0:00:00.72 for the FLOTTER CNF translation.
% 68.17/68.36 0:00:00.71 for inferences.
% 68.17/68.36 0:00:00.04 for the backtracking.
% 68.17/68.36 0:01:05.43 for the reduction.
% 68.17/68.36
% 68.17/68.36
% 68.17/68.36 Here is a proof with depth 5, length 142 :
% 68.17/68.36 % SZS output start Refutation
% See solution above
% 71.22/71.42 Formulae used in the proof : arity_Int_Oint___Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduc arity_Int_Oint___Groups_Oordered__cancel__ab__semigroup__add arity_Int_Oint___Groups_Oordered__ab__semigroup__add__imp__le arity_Int_Oint___Rings_Olinordered__comm__semiring__strict arity_Int_Oint___Rings_Olinordered__semiring__1__strict arity_Int_Oint___Rings_Olinordered__semiring__strict arity_Int_Oint___Groups_Oordered__ab__semigroup__add arity_Int_Oint___Groups_Oordered__ab__group__add__abs arity_Int_Oint___Groups_Oordered__comm__monoid__add arity_Int_Oint___Groups_Olinordered__ab__group__add arity_Int_Oint___Groups_Ocancel__ab__semigroup__add arity_Int_Oint___Rings_Oring__1__no__zero__divisors arity_Int_Oint___Rings_Oordered__cancel__semiring arity_Int_Oint___Rings_Olinordered__ring__strict arity_Int_Oint___Rings_Oring__no__zero__divisors arity_Int_Oint___Rings_Oordered__comm__semiring arity_Int_Oint___Rings_Olinordered__semiring__1 arity_Int_Oint___Groups_Oordered__ab__group__add arity_Int_Oint___Groups_Ocancel__semigroup__add arity_Int_Oint___Rings_Olinordered__semiring arity_Int_Oint___Rings_Olinordered__semidom arity_Int_Oint___Groups_Oab__semigroup__mult arity_Int_Oint___Groups_Ocomm__monoid__mult arity_Int_Oint___Groups_Oab__semigroup__add arity_Int_Oint___Rings_Oordered__semiring arity_Int_Oint___Rings_Oordered__ring__abs arity_Int_Oint___Rings_Ono__zero__divisors arity_Int_Oint___Groups_Ocomm__monoid__add arity_Int_Oint___Rings_Olinordered__ring arity_Int_Oint___Rings_Olinordered__idom arity_Int_Oint___Rings_Ocomm__semiring__1 arity_Int_Oint___Rings_Ocomm__semiring arity_Int_Oint___Nat_Osemiring__char__0 arity_Int_Oint___Int_Onumber__semiring arity_Int_Oint___Groups_Oab__group__add arity_Int_Oint___Rings_Ozero__neq__one arity_Int_Oint___Rings_Oordered__ring arity_Int_Oint___Orderings_Olinorder arity_Int_Oint___Groups_Omonoid__mult arity_Int_Oint___Rings_Ocomm__ring__1 arity_Int_Oint___Groups_Omonoid__add arity_Int_Oint___Rings_Osemiring__1 arity_Int_Oint___Rings_Osemiring__0 arity_Int_Oint___Groups_Ogroup__add arity_Int_Oint___Rings_Omult__zero arity_Int_Oint___Rings_Ocomm__ring arity_Int_Oint___Orderings_Oorder arity_Int_Oint___Int_Oring__char__0 arity_Int_Oint___Int_Onumber__ring arity_Int_Oint___Rings_Osemiring arity_Int_Oint___Rings_Oring__1 arity_Int_Oint___Power_Opower arity_Int_Oint___Groups_Ozero arity_Int_Oint___Rings_Oring arity_Int_Oint___Rings_Oidom arity_Int_Oint___Int_Onumber arity_Int_Oint___Groups_Oone arity_Int_Oint___Rings_Odvd fact_73_Pls__def fact_768_rel__simps_I37_J fact_769_Bit1__Min fact_776_succ__Min tsy_c_Int_OMin_res fact_513_succ__Pls fact_19_zero__is__num__zero fact_514_succ__Bit0 tsy_c_Int_OBit0_arg1 tsy_c_Int_OBit1_arg1 tsy_c_Int_OBit1_res tsy_c_Int_Onat_arg1 tsy_c_Int_Osucc_res fact_37_one__is__num__one fact_120_number__of__is__id fact_515_succ__Bit1 fact_75_add__Pls__right fact_76_add__Pls fact_427_nat__number__of__def fact_519_succ__def fact_47_zadd__commute fact_71_rel__simps_I38_J fact_771_rel__simps_I47_J fact_92_Bit1__def tsy_c_Groups_Oabs__class_Oabs_res fact_937_abs__idempotent fact_533_add__Bit1__Bit1 fact_957_abs__eq__1__iff fact_936_abs__int__eq fact_165_field__power__not__zero conj_0
% 71.22/71.42
%------------------------------------------------------------------------------