%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM925+6 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n015.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 3.38s 3.55s
% Output : Refutation 3.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 48
% Syntax : Number of clauses : 63 ( 55 unt; 0 nHn; 63 RR)
% Number of literals : 74 ( 0 equ; 13 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 41 ( 40 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 11 con; 0-4 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
semiri456707255roduct(int),
file('NUM925+6.p',unknown),
[] ).
cnf(2,axiom,
ordere223160158up_add(int),
file('NUM925+6.p',unknown),
[] ).
cnf(3,axiom,
ordere236663937imp_le(int),
file('NUM925+6.p',unknown),
[] ).
cnf(4,axiom,
linord893533164strict(int),
file('NUM925+6.p',unknown),
[] ).
cnf(5,axiom,
linord20386208strict(int),
file('NUM925+6.p',unknown),
[] ).
cnf(6,axiom,
ordere779506340up_add(int),
file('NUM925+6.p',unknown),
[] ).
cnf(7,axiom,
ordere216010020id_add(int),
file('NUM925+6.p',unknown),
[] ).
cnf(8,axiom,
linord219039673up_add(int),
file('NUM925+6.p',unknown),
[] ).
cnf(9,axiom,
cancel146912293up_add(int),
file('NUM925+6.p',unknown),
[] ).
cnf(10,axiom,
ring_11004092258visors(int),
file('NUM925+6.p',unknown),
[] ).
cnf(11,axiom,
linord581940658strict(int),
file('NUM925+6.p',unknown),
[] ).
cnf(12,axiom,
cancel_semigroup_add(int),
file('NUM925+6.p',unknown),
[] ).
cnf(13,axiom,
linordered_semiring(int),
file('NUM925+6.p',unknown),
[] ).
cnf(14,axiom,
linordered_semidom(int),
file('NUM925+6.p',unknown),
[] ).
cnf(15,axiom,
ab_semigroup_add(int),
file('NUM925+6.p',unknown),
[] ).
cnf(16,axiom,
no_zero_divisors(int),
file('NUM925+6.p',unknown),
[] ).
cnf(17,axiom,
comm_monoid_add(int),
file('NUM925+6.p',unknown),
[] ).
cnf(18,axiom,
linordered_ring(int),
file('NUM925+6.p',unknown),
[] ).
cnf(19,axiom,
linordered_idom(int),
file('NUM925+6.p',unknown),
[] ).
cnf(20,axiom,
comm_semiring_1(int),
file('NUM925+6.p',unknown),
[] ).
cnf(21,axiom,
semiring_char_0(int),
file('NUM925+6.p',unknown),
[] ).
cnf(22,axiom,
number_semiring(int),
file('NUM925+6.p',unknown),
[] ).
cnf(23,axiom,
zero_neq_one(int),
file('NUM925+6.p',unknown),
[] ).
cnf(24,axiom,
preorder(int),
file('NUM925+6.p',unknown),
[] ).
cnf(25,axiom,
linorder(int),
file('NUM925+6.p',unknown),
[] ).
cnf(26,axiom,
monoid_mult(int),
file('NUM925+6.p',unknown),
[] ).
cnf(27,axiom,
monoid_add(int),
file('NUM925+6.p',unknown),
[] ).
cnf(28,axiom,
semiring_1(int),
file('NUM925+6.p',unknown),
[] ).
cnf(29,axiom,
semiring_0(int),
file('NUM925+6.p',unknown),
[] ).
cnf(30,axiom,
mult_zero(int),
file('NUM925+6.p',unknown),
[] ).
cnf(31,axiom,
order(int),
file('NUM925+6.p',unknown),
[] ).
cnf(32,axiom,
ring_char_0(int),
file('NUM925+6.p',unknown),
[] ).
cnf(33,axiom,
number_ring(int),
file('NUM925+6.p',unknown),
[] ).
cnf(34,axiom,
ord(int),
file('NUM925+6.p',unknown),
[] ).
cnf(35,axiom,
power(int),
file('NUM925+6.p',unknown),
[] ).
cnf(36,axiom,
zero(int),
file('NUM925+6.p',unknown),
[] ).
cnf(37,axiom,
number(int),
file('NUM925+6.p',unknown),
[] ).
cnf(38,axiom,
one(int),
file('NUM925+6.p',unknown),
[] ).
cnf(112,axiom,
equal(zero_zero(int),pls),
file('NUM925+6.p',unknown),
[] ).
cnf(120,axiom,
equal(number_number_of(int,u),u),
file('NUM925+6.p',unknown),
[] ).
cnf(154,axiom,
equal(number_number_of(int,hAPP(int,int,bit1,pls)),one_one(int)),
file('NUM925+6.p',unknown),
[] ).
cnf(174,axiom,
( ~ number(u)
| equal(number_number_of(u,ti(int,v)),number_number_of(u,v)) ),
file('NUM925+6.p',unknown),
[] ).
cnf(216,axiom,
equal(hAPP(int,int,plus_plus(int,u),one_one(int)),hAPP(int,int,succ,u)),
file('NUM925+6.p',unknown),
[] ).
cnf(224,axiom,
equal(hAPP(int,int,plus_plus(int,u),v),hAPP(int,int,plus_plus(int,v),u)),
file('NUM925+6.p',unknown),
[] ).
cnf(295,axiom,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),u),v))
| ~ equal(u,v) ),
file('NUM925+6.p',unknown),
[] ).
cnf(325,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+6.p',unknown),
[] ).
cnf(406,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n)))),
file('NUM925+6.p',unknown),
[] ).
cnf(520,axiom,
equal(hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),zero_zero(int)),
file('NUM925+6.p',unknown),
[] ).
cnf(884,plain,
equal(hAPP(int,int,bit1,pls),one_one(int)),
inference(rew,[status(thm),theory(equality)],[120,154]),
[iquote('0:Rew:120.0,154.0')] ).
cnf(932,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(rew,[status(thm),theory(equality)],[112,406]),
[iquote('0:Rew:112.0,406.0')] ).
cnf(956,plain,
equal(hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,one_one(int)))),pls),
inference(rew,[status(thm),theory(equality)],[884,520,112]),
[iquote('0:Rew:884.0,520.0,112.0,520.0')] ).
cnf(1208,plain,
( ~ number(int)
| equal(number_number_of(int,u),ti(int,u)) ),
inference(spr,[status(thm),theory(equality)],[174,120]),
[iquote('0:SpR:174.1,120.0')] ).
cnf(1217,plain,
( ~ number(int)
| equal(ti(int,u),u) ),
inference(rew,[status(thm),theory(equality)],[120,1208]),
[iquote('0:Rew:120.0,1208.1')] ).
cnf(1218,plain,
equal(ti(int,u),u),
inference(ssi,[status(thm)],[1217,18,38,36,32,10,9,4,29,26,21,17,1,37,30,16,15,13,6,27,23,2,12,28,22,3,20,8,11,35,25,7,5,24,34,33,14,19,31]),
[iquote('0:SSi:1217.0,18.0,38.0,36.0,32.0,10.0,9.0,4.0,29.0,26.0,21.0,17.0,1.0,37.0,30.0,16.0,15.0,13.0,6.0,27.0,23.0,2.0,12.0,28.0,22.0,3.0,20.0,8.0,11.0,35.0,25.0,7.0,5.0,24.0,34.0,33.0,14.0,19.0,31.0')] ).
cnf(1762,plain,
equal(hAPP(int,int,plus_plus(int,one_one(int)),u),hAPP(int,int,succ,u)),
inference(spr,[status(thm),theory(equality)],[224,216]),
[iquote('0:SpR:224.0,216.0')] ).
cnf(1784,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),hAPP(int,int,succ,hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(rew,[status(thm),theory(equality)],[1762,932]),
[iquote('0:Rew:1762.0,932.0')] ).
cnf(1786,plain,
equal(hAPP(nat,int,power_power(int,hAPP(int,int,succ,hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,one_one(int)))),pls),
inference(rew,[status(thm),theory(equality)],[1762,956]),
[iquote('0:Rew:1762.0,956.0')] ).
cnf(9566,plain,
~ equal(hAPP(int,int,succ,hAPP(nat,int,semiring_1_of_nat(int),n)),pls),
inference(res,[status(thm),theory(equality)],[1784,295]),
[iquote('0:Res:1784.0,295.0')] ).
cnf(13411,plain,
( ~ ring_11004092258visors(int)
| ~ equal(zero_zero(int),pls)
| equal(ti(int,hAPP(int,int,succ,hAPP(nat,int,semiring_1_of_nat(int),n))),zero_zero(int)) ),
inference(spl,[status(thm),theory(equality)],[1786,325]),
[iquote('0:SpL:1786.0,325.1')] ).
cnf(13412,plain,
( ~ ring_11004092258visors(int)
| ~ equal(pls,pls)
| equal(hAPP(int,int,succ,hAPP(nat,int,semiring_1_of_nat(int),n)),pls) ),
inference(rew,[status(thm),theory(equality)],[1218,13411,112]),
[iquote('0:Rew:1218.0,13411.2,112.0,13411.2,112.0,13411.1')] ).
cnf(13413,plain,
( ~ ring_11004092258visors(int)
| equal(hAPP(int,int,succ,hAPP(nat,int,semiring_1_of_nat(int),n)),pls) ),
inference(obv,[status(thm),theory(equality)],[13412]),
[iquote('0:Obv:13412.1')] ).
cnf(13414,plain,
equal(hAPP(int,int,succ,hAPP(nat,int,semiring_1_of_nat(int),n)),pls),
inference(ssi,[status(thm)],[13413,18,38,36,32,10,9,4,29,26,21,17,1,37,30,16,15,13,6,27,23,2,12,28,22,3,20,8,11,35,25,7,5,24,34,33,14,19,31]),
[iquote('0:SSi:13413.0,18.0,38.0,36.0,32.0,10.0,9.0,4.0,29.0,26.0,21.0,17.0,1.0,37.0,30.0,16.0,15.0,13.0,6.0,27.0,23.0,2.0,12.0,28.0,22.0,3.0,20.0,8.0,11.0,35.0,25.0,7.0,5.0,24.0,34.0,33.0,14.0,19.0,31.0')] ).
cnf(13415,plain,
$false,
inference(mrr,[status(thm)],[13414,9566]),
[iquote('0:MRR:13414.0,9566.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM925+6 : TPTP v8.1.0. Released v5.3.0.
% 0.03/0.13 % Command : run_spass %d %s
% 0.13/0.35 % Computer : n015.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Thu Jul 7 09:39:19 EDT 2022
% 0.13/0.35 % CPUTime :
% 3.38/3.55
% 3.38/3.55 SPASS V 3.9
% 3.38/3.55 SPASS beiseite: Proof found.
% 3.38/3.55 % SZS status Theorem
% 3.38/3.55 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.38/3.55 SPASS derived 9229 clauses, backtracked 57 clauses, performed 2 splits and kept 2302 clauses.
% 3.38/3.55 SPASS allocated 108841 KBytes.
% 3.38/3.55 SPASS spent 0:00:03.10 on the problem.
% 3.38/3.55 0:00:00.05 for the input.
% 3.38/3.55 0:00:00.68 for the FLOTTER CNF translation.
% 3.38/3.55 0:00:00.15 for inferences.
% 3.38/3.55 0:00:00.10 for the backtracking.
% 3.38/3.55 0:00:01.97 for the reduction.
% 3.38/3.55
% 3.38/3.55
% 3.38/3.55 Here is a proof with depth 1, length 63 :
% 3.38/3.55 % SZS output start Refutation
% See solution above
% 3.38/3.55 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__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_Olinordered__ring__strict 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__add 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___Nat_Osemiring__char__0 arity_Int_Oint___Int_Onumber__semiring arity_Int_Oint___Rings_Ozero__neq__one arity_Int_Oint___Orderings_Opreorder arity_Int_Oint___Orderings_Olinorder arity_Int_Oint___Groups_Omonoid__mult arity_Int_Oint___Groups_Omonoid__add arity_Int_Oint___Rings_Osemiring__1 arity_Int_Oint___Rings_Osemiring__0 arity_Int_Oint___Rings_Omult__zero arity_Int_Oint___Orderings_Oorder arity_Int_Oint___Int_Oring__char__0 arity_Int_Oint___Int_Onumber__ring arity_Int_Oint___Orderings_Oord arity_Int_Oint___Power_Opower arity_Int_Oint___Groups_Ozero arity_Int_Oint___Int_Onumber arity_Int_Oint___Groups_Oone fact_73_Pls__def fact_119_number__of__is__id fact_37_one__is__num__one tsy_c_Int_Onumber__class_Onumber__of_arg1 fact_320_succ__def fact_47_zadd__commute fact_254_zless__le fact_164_field__power__not__zero fact_0_n1pos conj_0
% 3.38/3.55
%------------------------------------------------------------------------------