%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM926+7 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n029.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:51 EDT 2022
% Result : Theorem 278.03s 278.27s
% Output : Refutation 278.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 88
% Syntax : Number of clauses : 142 ( 127 unt; 4 nHn; 142 RR)
% Number of literals : 159 ( 0 equ; 20 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 61 ( 60 usr; 1 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 17 con; 0-5 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
semiri456707255roduct(int),
file('NUM926+7.p',unknown),
[] ).
cnf(2,axiom,
ordere223160158up_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(3,axiom,
ordere236663937imp_le(int),
file('NUM926+7.p',unknown),
[] ).
cnf(4,axiom,
linord893533164strict(int),
file('NUM926+7.p',unknown),
[] ).
cnf(5,axiom,
linord626643107strict(int),
file('NUM926+7.p',unknown),
[] ).
cnf(6,axiom,
linord20386208strict(int),
file('NUM926+7.p',unknown),
[] ).
cnf(7,axiom,
ordere779506340up_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(8,axiom,
ordere216010020id_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(9,axiom,
linord219039673up_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(10,axiom,
cancel146912293up_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(11,axiom,
ring_11004092258visors(int),
file('NUM926+7.p',unknown),
[] ).
cnf(12,axiom,
ordere453448008miring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(13,axiom,
linord581940658strict(int),
file('NUM926+7.p',unknown),
[] ).
cnf(14,axiom,
ring_n68954251visors(int),
file('NUM926+7.p',unknown),
[] ).
cnf(15,axiom,
ordere1490568538miring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(16,axiom,
linord1278240602ring_1(int),
file('NUM926+7.p',unknown),
[] ).
cnf(17,axiom,
ordered_ab_group_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(18,axiom,
cancel_semigroup_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(19,axiom,
linordered_semiring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(20,axiom,
linordered_semidom(int),
file('NUM926+7.p',unknown),
[] ).
cnf(21,axiom,
ab_semigroup_mult(int),
file('NUM926+7.p',unknown),
[] ).
cnf(22,axiom,
comm_monoid_mult(int),
file('NUM926+7.p',unknown),
[] ).
cnf(23,axiom,
ab_semigroup_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(24,axiom,
ordered_semiring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(25,axiom,
no_zero_divisors(int),
file('NUM926+7.p',unknown),
[] ).
cnf(26,axiom,
comm_monoid_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(27,axiom,
linordered_ring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(28,axiom,
linordered_idom(int),
file('NUM926+7.p',unknown),
[] ).
cnf(29,axiom,
comm_semiring_1(int),
file('NUM926+7.p',unknown),
[] ).
cnf(30,axiom,
semiring_div(int),
file('NUM926+7.p',unknown),
[] ).
cnf(31,axiom,
comm_semiring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(32,axiom,
number_semiring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(33,axiom,
ab_group_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(34,axiom,
zero_neq_one(int),
file('NUM926+7.p',unknown),
[] ).
cnf(35,axiom,
ordered_ring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(36,axiom,
linorder(int),
file('NUM926+7.p',unknown),
[] ).
cnf(37,axiom,
monoid_mult(int),
file('NUM926+7.p',unknown),
[] ).
cnf(38,axiom,
comm_ring_1(int),
file('NUM926+7.p',unknown),
[] ).
cnf(39,axiom,
monoid_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(40,axiom,
semiring_1(int),
file('NUM926+7.p',unknown),
[] ).
cnf(41,axiom,
semiring_0(int),
file('NUM926+7.p',unknown),
[] ).
cnf(42,axiom,
group_add(int),
file('NUM926+7.p',unknown),
[] ).
cnf(43,axiom,
ring_div(int),
file('NUM926+7.p',unknown),
[] ).
cnf(44,axiom,
mult_zero(int),
file('NUM926+7.p',unknown),
[] ).
cnf(45,axiom,
comm_ring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(46,axiom,
order(int),
file('NUM926+7.p',unknown),
[] ).
cnf(47,axiom,
ring_char_0(int),
file('NUM926+7.p',unknown),
[] ).
cnf(48,axiom,
number_ring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(49,axiom,
semiring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(50,axiom,
ring_1(int),
file('NUM926+7.p',unknown),
[] ).
cnf(51,axiom,
power(int),
file('NUM926+7.p',unknown),
[] ).
cnf(52,axiom,
zero(int),
file('NUM926+7.p',unknown),
[] ).
cnf(53,axiom,
plus(int),
file('NUM926+7.p',unknown),
[] ).
cnf(54,axiom,
ring(int),
file('NUM926+7.p',unknown),
[] ).
cnf(55,axiom,
idom(int),
file('NUM926+7.p',unknown),
[] ).
cnf(56,axiom,
number(int),
file('NUM926+7.p',unknown),
[] ).
cnf(57,axiom,
one(int),
file('NUM926+7.p',unknown),
[] ).
cnf(58,axiom,
dvd(int),
file('NUM926+7.p',unknown),
[] ).
cnf(156,axiom,
equal(zero_zero(int),pls),
file('NUM926+7.p',unknown),
[] ).
cnf(160,axiom,
equal(ti(int,min),min),
file('NUM926+7.p',unknown),
[] ).
cnf(162,axiom,
equal(ti(int,m),m),
file('NUM926+7.p',unknown),
[] ).
cnf(165,axiom,
equal(ti(int,t),t),
file('NUM926+7.p',unknown),
[] ).
cnf(180,axiom,
equal(ti(int,zfact(u)),zfact(u)),
file('NUM926+7.p',unknown),
[] ).
cnf(182,axiom,
equal(bit0(ti(int,u)),bit0(u)),
file('NUM926+7.p',unknown),
[] ).
cnf(183,axiom,
equal(ti(int,bit0(u)),bit0(u)),
file('NUM926+7.p',unknown),
[] ).
cnf(184,axiom,
equal(bit1(ti(int,u)),bit1(u)),
file('NUM926+7.p',unknown),
[] ).
cnf(185,axiom,
equal(ti(int,bit1(u)),bit1(u)),
file('NUM926+7.p',unknown),
[] ).
cnf(194,axiom,
equal(ti(int,u),number_number_of(int,u)),
file('NUM926+7.p',unknown),
[] ).
cnf(195,axiom,
equal(number_number_of(int,bit1(pls)),one_one(int)),
file('NUM926+7.p',unknown),
[] ).
cnf(270,axiom,
equal(hAPP(int,int,plus_plus(int,pls),u),ti(int,u)),
file('NUM926+7.p',unknown),
[] ).
cnf(293,axiom,
equal(hAPP(int,int,times_times(int,u),one_one(int)),ti(int,u)),
file('NUM926+7.p',unknown),
[] ).
cnf(294,axiom,
equal(hAPP(int,int,times_times(int,one_one(int)),u),ti(int,u)),
file('NUM926+7.p',unknown),
[] ).
cnf(311,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),min),pls)),
file('NUM926+7.p',unknown),
[] ).
cnf(334,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
file('NUM926+7.p',unknown),
[] ).
cnf(341,axiom,
( ~ monoid_mult(u)
| equal(hAPP(nat,u,power_power(u,one_one(u)),v),one_one(u)) ),
file('NUM926+7.p',unknown),
[] ).
cnf(373,axiom,
equal(hAPP(int,int,times_times(int,u),v),hAPP(int,int,times_times(int,v),u)),
file('NUM926+7.p',unknown),
[] ).
cnf(374,axiom,
equal(hAPP(int,int,plus_plus(int,u),v),hAPP(int,int,plus_plus(int,v),u)),
file('NUM926+7.p',unknown),
[] ).
cnf(449,axiom,
equal(hAPP(int,int,times_times(int,bit0(u)),v),bit0(hAPP(int,int,times_times(int,u),v))),
file('NUM926+7.p',unknown),
[] ).
cnf(486,axiom,
equal(hAPP(int,int,plus_plus(int,bit1(u)),bit0(v)),bit1(hAPP(int,int,plus_plus(int,u),v))),
file('NUM926+7.p',unknown),
[] ).
cnf(558,axiom,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),u),zero_zero(int)))
| equal(zfact(u),one_one(int)) ),
file('NUM926+7.p',unknown),
[] ).
cnf(593,axiom,
equal(hAPP(u,v,combc(u,w,v,x,y),z),hAPP(w,v,hAPP(u,fun(w,v),x,z),y)),
file('NUM926+7.p',unknown),
[] ).
cnf(962,axiom,
equal(hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),twoSqu1929807760sum2sq(product_Pair(int,int,s,one_one(int)))),
file('NUM926+7.p',unknown),
[] ).
cnf(1006,axiom,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),u),v))
| equal(ti(int,u),ti(int,v))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),u),v)) ),
file('NUM926+7.p',unknown),
[] ).
cnf(1130,axiom,
equal(hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),number_number_of(int,min)),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),
file('NUM926+7.p',unknown),
[] ).
cnf(1280,axiom,
equal(hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),skc12),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),
file('NUM926+7.p',unknown),
[] ).
cnf(1281,axiom,
equal(hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),
file('NUM926+7.p',unknown),
[] ).
cnf(1323,axiom,
~ equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,u),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,v),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),
file('NUM926+7.p',unknown),
[] ).
cnf(1544,axiom,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
| equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,skc11),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,skc10),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))) ),
file('NUM926+7.p',unknown),
[] ).
cnf(1650,plain,
equal(number_number_of(int,min),min),
inference(rew,[status(thm),theory(equality)],[194,160]),
[iquote('0:Rew:194.0,160.0')] ).
cnf(1652,plain,
equal(number_number_of(int,m),m),
inference(rew,[status(thm),theory(equality)],[194,162]),
[iquote('0:Rew:194.0,162.0')] ).
cnf(1655,plain,
equal(number_number_of(int,t),t),
inference(rew,[status(thm),theory(equality)],[194,165]),
[iquote('0:Rew:194.0,165.0')] ).
cnf(1659,plain,
equal(number_number_of(int,bit1(u)),bit1(u)),
inference(rew,[status(thm),theory(equality)],[194,185]),
[iquote('0:Rew:194.0,185.0')] ).
cnf(1660,plain,
equal(one_one(int),bit1(pls)),
inference(rew,[status(thm),theory(equality)],[1659,195]),
[iquote('0:Rew:1659.0,195.0')] ).
cnf(1662,plain,
equal(bit1(number_number_of(int,u)),bit1(u)),
inference(rew,[status(thm),theory(equality)],[194,184]),
[iquote('0:Rew:194.0,184.0')] ).
cnf(1663,plain,
equal(number_number_of(int,bit0(u)),bit0(u)),
inference(rew,[status(thm),theory(equality)],[194,183]),
[iquote('0:Rew:194.0,183.0')] ).
cnf(1664,plain,
equal(bit0(number_number_of(int,u)),bit0(u)),
inference(rew,[status(thm),theory(equality)],[194,182]),
[iquote('0:Rew:194.0,182.0')] ).
cnf(1665,plain,
equal(number_number_of(int,zfact(u)),zfact(u)),
inference(rew,[status(thm),theory(equality)],[194,180]),
[iquote('0:Rew:194.0,180.0')] ).
cnf(1706,plain,
equal(hAPP(int,int,plus_plus(int,pls),u),number_number_of(int,u)),
inference(rew,[status(thm),theory(equality)],[194,270]),
[iquote('0:Rew:194.0,270.0')] ).
cnf(1715,plain,
equal(hAPP(int,int,times_times(int,bit1(pls)),u),number_number_of(int,u)),
inference(rew,[status(thm),theory(equality)],[1660,294,194]),
[iquote('0:Rew:1660.0,294.0,194.0,294.0')] ).
cnf(1716,plain,
equal(hAPP(int,int,times_times(int,u),bit1(pls)),number_number_of(int,u)),
inference(rew,[status(thm),theory(equality)],[1660,293,194]),
[iquote('0:Rew:1660.0,293.0,194.0,293.0')] ).
cnf(1730,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),bit1(pls)),t)),
inference(rew,[status(thm),theory(equality)],[1660,334]),
[iquote('0:Rew:1660.0,334.0')] ).
cnf(1763,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),u),pls))
| equal(zfact(u),bit1(pls)) ),
inference(rew,[status(thm),theory(equality)],[1660,558,156]),
[iquote('0:Rew:1660.0,558.1,156.0,558.0')] ).
cnf(1825,plain,
hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less_eq(int),t),bit1(pls))),
inference(rew,[status(thm),theory(equality)],[593,1730]),
[iquote('0:Rew:593.0,1730.0')] ).
cnf(1838,plain,
( ~ hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less_eq(int),pls),u))
| equal(zfact(u),bit1(pls)) ),
inference(rew,[status(thm),theory(equality)],[593,1763]),
[iquote('0:Rew:593.0,1763.0')] ).
cnf(1842,plain,
hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less_eq(int),pls),min)),
inference(rew,[status(thm),theory(equality)],[593,311]),
[iquote('0:Rew:593.0,311.0')] ).
cnf(2101,plain,
equal(hAPP(int,int,times_times(int,t),bit1(bit0(m))),twoSqu1929807760sum2sq(product_Pair(int,int,s,bit1(pls)))),
inference(rew,[status(thm),theory(equality)],[373,962,1663,1706,486,374,1652,1716,449,1660]),
[iquote('0:Rew:373.0,962.0,1663.0,962.0,1706.0,962.0,486.0,962.0,374.0,962.0,1652.0,962.0,1716.0,962.0,373.0,962.0,449.0,962.0,449.0,962.0,1663.0,962.0,1660.0,962.0')] ).
cnf(2142,plain,
( ~ hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less_eq(int),u),v))
| hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less(int),u),v))
| equal(number_number_of(int,v),number_number_of(int,u)) ),
inference(rew,[status(thm),theory(equality)],[593,1006,194]),
[iquote('0:Rew:593.0,1006.2,194.0,1006.1,194.0,1006.1,593.0,1006.0')] ).
cnf(2227,plain,
equal(hAPP(int,int,plus_plus(int,bit1(pls)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),min)),
inference(rew,[status(thm),theory(equality)],[1650,1130,374,1660]),
[iquote('0:Rew:1650.0,1130.0,374.0,1130.0,1660.0,1130.0')] ).
cnf(2366,plain,
equal(hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),min),hAPP(int,int,times_times(int,skc12),bit1(bit0(m)))),
inference(rew,[status(thm),theory(equality)],[373,1280,1663,1706,486,374,1652,1716,449,2227,1660]),
[iquote('0:Rew:373.0,1280.0,1663.0,1280.0,1706.0,1280.0,486.0,1280.0,374.0,1280.0,1652.0,1280.0,1716.0,1280.0,373.0,1280.0,449.0,1280.0,449.0,1280.0,1663.0,1280.0,2227.0,1280.0,374.0,1280.0,1660.0,1280.0')] ).
cnf(2367,plain,
equal(hAPP(int,int,plus_plus(int,bit1(pls)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,times_times(int,skc12),bit1(bit0(m)))),
inference(rew,[status(thm),theory(equality)],[2366,2227]),
[iquote('0:Rew:2366.0,2227.0')] ).
cnf(2368,plain,
equal(hAPP(int,int,times_times(int,skc12),bit1(bit0(m))),twoSqu1929807760sum2sq(product_Pair(int,int,s,bit1(pls)))),
inference(rew,[status(thm),theory(equality)],[2101,1281,373,1663,1706,486,374,1652,1716,449,2367,1660]),
[iquote('0:Rew:2101.0,1281.0,373.0,1281.0,1663.0,1281.0,1706.0,1281.0,486.0,1281.0,374.0,1281.0,1652.0,1281.0,1716.0,1281.0,373.0,1281.0,449.0,1281.0,449.0,1281.0,1663.0,1281.0,2367.0,1281.0,374.0,1281.0,1660.0,1281.0')] ).
cnf(2370,plain,
equal(hAPP(int,int,plus_plus(int,bit1(pls)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),twoSqu1929807760sum2sq(product_Pair(int,int,s,bit1(pls)))),
inference(rew,[status(thm),theory(equality)],[2368,2367]),
[iquote('0:Rew:2368.0,2367.0')] ).
cnf(2405,plain,
~ equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,u),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,v),number_number_of(nat,bit0(bit1(pls))))),bit1(bit0(m))),
inference(rew,[status(thm),theory(equality)],[1663,1323,1706,486,374,1652,1716,373,449,1660]),
[iquote('0:Rew:1663.0,1323.0,1706.0,1323.0,486.0,1323.0,374.0,1323.0,1652.0,1323.0,1716.0,1323.0,373.0,1323.0,449.0,1323.0,449.0,1323.0,1663.0,1323.0,1660.0,1323.0')] ).
cnf(2615,plain,
( ~ hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less(int),t),bit1(pls)))
| equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,skc10),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,skc11),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,bit1(pls)),hAPP(int,int,times_times(int,m),bit0(bit0(bit1(pls)))))) ),
inference(rew,[status(thm),theory(equality)],[374,1544,1660,1663,373,593]),
[iquote('0:Rew:374.0,1544.1,1660.0,1544.1,1663.0,1544.1,373.0,1544.1,374.0,1544.1,1660.0,1544.0,593.0,1544.0')] ).
cnf(14729,plain,
( ~ monoid_mult(int)
| equal(hAPP(nat,int,power_power(int,bit1(pls)),u),bit1(pls)) ),
inference(spr,[status(thm),theory(equality)],[1660,341]),
[iquote('0:SpR:1660.0,341.1')] ).
cnf(14733,plain,
equal(hAPP(nat,int,power_power(int,bit1(pls)),u),bit1(pls)),
inference(ssi,[status(thm)],[14729,50,38,16,5,57,52,47,45,43,31,15,11,10,4,53,40,33,26,19,14,34,27,23,22,21,12,7,54,41,39,36,24,55,49,25,17,2,46,44,18,1,42,32,3,56,9,51,58,37,35,8,6,30,20,13,48,28,29]),
[iquote('0:SSi:14729.0,50.0,38.0,16.0,5.0,57.0,52.0,47.0,45.0,43.0,31.0,15.0,11.0,10.0,4.0,53.0,40.0,33.0,26.0,19.0,14.0,34.0,27.0,23.0,22.0,21.0,12.0,7.0,54.0,41.0,39.0,36.0,24.0,55.0,49.0,25.0,17.0,2.0,46.0,44.0,18.0,1.0,42.0,32.0,3.0,56.0,9.0,51.0,58.0,37.0,35.0,8.0,6.0,30.0,20.0,13.0,48.0,28.0,29.0')] ).
cnf(34482,plain,
equal(hAPP(int,int,times_times(int,u),bit0(v)),bit0(hAPP(int,int,times_times(int,v),u))),
inference(spr,[status(thm),theory(equality)],[449,373]),
[iquote('0:SpR:449.0,373.0')] ).
cnf(34550,plain,
( ~ hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less(int),t),bit1(pls)))
| equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,skc10),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,skc11),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,bit1(pls)),bit0(hAPP(int,int,times_times(int,bit0(bit1(pls))),m)))) ),
inference(rew,[status(thm),theory(equality)],[34482,2615]),
[iquote('0:Rew:34482.0,2615.1')] ).
cnf(34616,plain,
( ~ hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less(int),t),bit1(pls)))
| equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,skc10),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,skc11),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,bit1(pls)),bit0(hAPP(int,int,times_times(int,m),bit0(bit1(pls)))))) ),
inference(rew,[status(thm),theory(equality)],[373,34550]),
[iquote('0:Rew:373.0,34550.1')] ).
cnf(34617,plain,
( ~ hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less(int),t),bit1(pls)))
| equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,skc10),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,skc11),number_number_of(nat,bit0(bit1(pls))))),bit1(hAPP(int,int,plus_plus(int,pls),bit0(hAPP(int,int,times_times(int,bit1(pls)),m))))) ),
inference(rew,[status(thm),theory(equality)],[34482,34616,486]),
[iquote('0:Rew:34482.0,34616.1,486.0,34616.1')] ).
cnf(34618,plain,
( ~ hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less(int),t),bit1(pls)))
| equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,skc10),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,skc11),number_number_of(nat,bit0(bit1(pls))))),bit1(bit0(m))) ),
inference(rew,[status(thm),theory(equality)],[1664,34617,1716,373,1662,1706]),
[iquote('0:Rew:1664.0,34617.1,1716.0,34617.1,373.0,34617.1,1662.0,34617.1,1706.0,34617.1')] ).
cnf(34619,plain,
~ hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less(int),t),bit1(pls))),
inference(mrr,[status(thm)],[34618,2405]),
[iquote('0:MRR:34618.1,2405.0')] ).
cnf(37393,plain,
equal(bit1(pls),zfact(min)),
inference(res,[status(thm),theory(equality)],[1842,1838]),
[iquote('0:Res:1842.0,1838.0')] ).
cnf(37439,plain,
equal(hAPP(int,int,times_times(int,t),bit1(bit0(m))),twoSqu1929807760sum2sq(product_Pair(int,int,s,zfact(min)))),
inference(rew,[status(thm),theory(equality)],[37393,2101]),
[iquote('0:Rew:37393.0,2101.0')] ).
cnf(37441,plain,
equal(hAPP(int,int,times_times(int,zfact(min)),u),number_number_of(int,u)),
inference(rew,[status(thm),theory(equality)],[37393,1715]),
[iquote('0:Rew:37393.0,1715.0')] ).
cnf(37456,plain,
hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less_eq(int),t),zfact(min))),
inference(rew,[status(thm),theory(equality)],[37393,1825]),
[iquote('0:Rew:37393.0,1825.0')] ).
cnf(37470,plain,
equal(hAPP(nat,int,power_power(int,zfact(min)),u),zfact(min)),
inference(rew,[status(thm),theory(equality)],[37393,14733]),
[iquote('0:Rew:37393.0,14733.0')] ).
cnf(37494,plain,
~ hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less(int),t),zfact(min))),
inference(rew,[status(thm),theory(equality)],[37393,34619]),
[iquote('0:Rew:37393.0,34619.0')] ).
cnf(37531,plain,
~ equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,u),number_number_of(nat,bit0(zfact(min))))),hAPP(nat,int,power_power(int,v),number_number_of(nat,bit0(zfact(min))))),bit1(bit0(m))),
inference(rew,[status(thm),theory(equality)],[37393,2405]),
[iquote('0:Rew:37393.0,2405.0')] ).
cnf(37700,plain,
equal(hAPP(int,int,plus_plus(int,zfact(min)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(zfact(min))))),twoSqu1929807760sum2sq(product_Pair(int,int,s,zfact(min)))),
inference(rew,[status(thm),theory(equality)],[37393,2370]),
[iquote('0:Rew:37393.0,2370.0')] ).
cnf(157710,plain,
~ equal(hAPP(int,int,plus_plus(int,zfact(min)),hAPP(nat,int,power_power(int,u),number_number_of(nat,bit0(zfact(min))))),bit1(bit0(m))),
inference(spl,[status(thm),theory(equality)],[37470,37531]),
[iquote('0:SpL:37470.0,37531.0')] ).
cnf(163447,plain,
( hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less(int),t),zfact(min)))
| equal(number_number_of(int,zfact(min)),number_number_of(int,t)) ),
inference(res,[status(thm),theory(equality)],[37456,2142]),
[iquote('0:Res:37456.0,2142.0')] ).
cnf(163478,plain,
( hBOOL(hAPP(int,bool,combc(int,int,bool,ord_less(int),t),zfact(min)))
| equal(zfact(min),t) ),
inference(rew,[status(thm),theory(equality)],[1665,163447,1655]),
[iquote('0:Rew:1665.0,163447.1,1655.0,163447.1')] ).
cnf(163479,plain,
equal(zfact(min),t),
inference(mrr,[status(thm)],[163478,37494]),
[iquote('0:MRR:163478.0,37494.0')] ).
cnf(163642,plain,
equal(hAPP(int,int,times_times(int,t),bit1(bit0(m))),twoSqu1929807760sum2sq(product_Pair(int,int,s,t))),
inference(rew,[status(thm),theory(equality)],[163479,37439]),
[iquote('0:Rew:163479.0,37439.0')] ).
cnf(163658,plain,
equal(hAPP(int,int,times_times(int,t),u),number_number_of(int,u)),
inference(rew,[status(thm),theory(equality)],[163479,37441]),
[iquote('0:Rew:163479.0,37441.0')] ).
cnf(163783,plain,
equal(hAPP(int,int,plus_plus(int,t),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(t)))),twoSqu1929807760sum2sq(product_Pair(int,int,s,t))),
inference(rew,[status(thm),theory(equality)],[163479,37700]),
[iquote('0:Rew:163479.0,37700.0')] ).
cnf(167521,plain,
~ equal(hAPP(int,int,plus_plus(int,t),hAPP(nat,int,power_power(int,u),number_number_of(nat,bit0(t)))),bit1(bit0(m))),
inference(rew,[status(thm),theory(equality)],[163479,157710]),
[iquote('0:Rew:163479.0,157710.0')] ).
cnf(172885,plain,
equal(twoSqu1929807760sum2sq(product_Pair(int,int,s,t)),number_number_of(int,bit1(bit0(m)))),
inference(rew,[status(thm),theory(equality)],[163658,163642]),
[iquote('0:Rew:163658.0,163642.0')] ).
cnf(172886,plain,
equal(twoSqu1929807760sum2sq(product_Pair(int,int,s,t)),bit1(bit0(m))),
inference(rew,[status(thm),theory(equality)],[1659,172885]),
[iquote('0:Rew:1659.0,172885.0')] ).
cnf(173327,plain,
equal(hAPP(int,int,plus_plus(int,t),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(t)))),bit1(bit0(m))),
inference(rew,[status(thm),theory(equality)],[172886,163783]),
[iquote('0:Rew:172886.0,163783.0')] ).
cnf(173328,plain,
$false,
inference(mrr,[status(thm)],[173327,167521]),
[iquote('0:MRR:173327.0,167521.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.14 % Problem : NUM926+7 : TPTP v8.1.0. Released v5.3.0.
% 0.10/0.15 % Command : run_spass %d %s
% 0.15/0.37 % Computer : n029.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 600
% 0.15/0.37 % DateTime : Wed Jul 6 09:20:28 EDT 2022
% 0.15/0.37 % CPUTime :
% 278.03/278.27
% 278.03/278.27 SPASS V 3.9
% 278.03/278.27 SPASS beiseite: Proof found.
% 278.03/278.27 % SZS status Theorem
% 278.03/278.27 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 278.03/278.27 SPASS derived 122124 clauses, backtracked 0 clauses, performed 0 splits and kept 38579 clauses.
% 278.03/278.27 SPASS allocated 228267 KBytes.
% 278.03/278.27 SPASS spent 0:4:37.66 on the problem.
% 278.03/278.27 0:00:00.07 for the input.
% 278.03/278.27 0:00:01.20 for the FLOTTER CNF translation.
% 278.03/278.27 0:00:02.17 for inferences.
% 278.03/278.27 0:00:00.00 for the backtracking.
% 278.03/278.27 0:4:31.93 for the reduction.
% 278.03/278.27
% 278.03/278.27
% 278.03/278.27 Here is a proof with depth 2, length 142 :
% 278.03/278.27 % SZS output start Refutation
% See solution above
% 278.03/278.27 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__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_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___Divides_Osemiring__div arity_Int_Oint___Rings_Ocomm__semiring 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___Divides_Oring__div 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___Groups_Oplus 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_204_Pls__def tsy_c_Int_OMin_res tsy_v_m_res tsy_v_t_____res tsy_c_IntFact_Ozfact_res tsy_c_Int_OBit0_arg1 tsy_c_Int_OBit0_res tsy_c_Int_OBit1_arg1 tsy_c_Int_OBit1_res fact_88_number__of__is__id fact_160_one__is__num__one fact_126_add__Pls fact_129_zmult__1__right fact_130_zmult__1 fact_309_rel__simps_I23_J fact_0_tpos fact_262_power__one fact_87_zmult__commute fact_91_zadd__commute fact_124_mult__Bit0 fact_151_add__Bit1__Bit0 fact_754_zfact_Osimps help_COMBC_1_1_U fact_173__096sum2sq_A_Is_M_A1_J_A_061_A_I4_A_K_Am_A_L_A1_J_A_K_At_096 fact_22_zless__le fact_366__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096 fact_19__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_ fact_5_t conj_0 fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06
% 283.11/283.36
%------------------------------------------------------------------------------