%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NUM925+5 : TPTP v9.0.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 : 300s
% DateTime : Fri Jul 25 12:29:29 PM UTC 2025
% Result : Theorem 7.06s 1.25s
% Output : CNFRefutation 7.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 12
% Syntax : Number of formulae : 39 ( 33 unt; 0 def)
% Number of atoms : 61 ( 18 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 43 ( 21 ~; 14 |; 4 &)
% ( 2 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 16 ( 2 sgn 8 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(conj_0,plain,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(conj_0_negated,plain,
~ ( power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int) ),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(197,plain,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) = zero_zero(int),
inference(cnf,[status(esa)],[conj_0_negated]) ).
cnf(l0,plain,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) = zero_zero(int),
inference(instantiation,[status(thm)],[197]) ).
fof(fact_86_power__eq__0__iff__number__of,plain,
! [X_a] :
( ( power(X_a)
& mult_zero(X_a)
& no_zero_divisors(X_a)
& zero_neq_one(X_a) )
=> ! [A_2,Wa] :
( power_power(X_a,A_2,number_number_of(nat,Wa)) = zero_zero(X_a)
<=> ( ti(X_a,A_2) = zero_zero(X_a)
& number_number_of(nat,Wa) != zero_zero(nat) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_86_power__eq__0__iff__number__of) ).
cnf(158,plain,
( power_power(X0,X1,number_number_of(nat,X2)) != zero_zero(X0)
| ~ power(X0)
| ~ mult_zero(X0)
| ~ no_zero_divisors(X0)
| ~ zero_neq_one(X0)
| ti(X0,X1) = zero_zero(X0) ),
inference(cnf,[status(esa)],[fact_86_power__eq__0__iff__number__of]) ).
cnf(l1,plain,
( power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int)
| ~ power(int)
| ~ mult_zero(int)
| ~ no_zero_divisors(int)
| ~ zero_neq_one(int)
| ti(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))) = zero_zero(int) ),
inference(instantiation,[status(thm)],[158]) ).
fof(arity_Int_Oint___Power_Opower,plain,
power(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Int_Oint___Power_Opower) ).
cnf(186,plain,
power(int),
inference(cnf,[status(esa)],[arity_Int_Oint___Power_Opower]) ).
cnf(l2,plain,
power(int),
inference(instantiation,[status(thm)],[186]) ).
fof(arity_Int_Oint___Rings_Ozero__neq__one,plain,
zero_neq_one(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Ozero__neq__one) ).
cnf(180,plain,
zero_neq_one(int),
inference(cnf,[status(esa)],[arity_Int_Oint___Rings_Ozero__neq__one]) ).
cnf(l46,plain,
zero_neq_one(int),
inference(instantiation,[status(thm)],[180]) ).
fof(arity_Int_Oint___Rings_Ono__zero__divisors,plain,
no_zero_divisors(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Ono__zero__divisors) ).
cnf(177,plain,
no_zero_divisors(int),
inference(cnf,[status(esa)],[arity_Int_Oint___Rings_Ono__zero__divisors]) ).
cnf(l42,plain,
no_zero_divisors(int),
inference(instantiation,[status(thm)],[177]) ).
fof(arity_Int_Oint___Rings_Omult__zero,plain,
mult_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Omult__zero) ).
cnf(183,plain,
mult_zero(int),
inference(cnf,[status(esa)],[arity_Int_Oint___Rings_Omult__zero]) ).
cnf(l38,plain,
mult_zero(int),
inference(instantiation,[status(thm)],[183]) ).
fof(tsy_c_Orderings_Oord__class_Oless_0_arg2,plain,
! [B_1,B_2,X_a] :
( linordered_idom(X_a)
=> ( ord_less(X_a,B_1,ti(X_a,B_2))
<=> ord_less(X_a,B_1,B_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_Orderings_Oord__class_Oless_0_arg2) ).
cnf(23,plain,
( ~ linordered_idom(X0)
| ~ ord_less(X0,X1,X2)
| ord_less(X0,X1,ti(X0,X2)) ),
inference(cnf,[status(esa)],[tsy_c_Orderings_Oord__class_Oless_0_arg2]) ).
cnf(l67,plain,
( ~ linordered_idom(int)
| ~ ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))
| ord_less(int,zero_zero(int),ti(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))) ),
inference(instantiation,[status(thm)],[23]) ).
fof(arity_Int_Oint___Rings_Olinordered__idom,plain,
linordered_idom(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Olinordered__idom) ).
cnf(178,plain,
linordered_idom(int),
inference(cnf,[status(esa)],[arity_Int_Oint___Rings_Olinordered__idom]) ).
cnf(l68,plain,
linordered_idom(int),
inference(instantiation,[status(thm)],[178]) ).
fof(fact_0_n1pos,plain,
ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_n1pos) ).
cnf(36,plain,
ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
inference(cnf,[status(esa)],[fact_0_n1pos]) ).
cnf(l76,plain,
ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
inference(instantiation,[status(thm)],[36]) ).
fof(fact_61_int__less__0__conv,plain,
! [K] : ~ ord_less(int,semiring_1_of_nat(int,K),zero_zero(int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_61_int__less__0__conv) ).
cnf(127,plain,
~ ord_less(int,semiring_1_of_nat(int,X0),zero_zero(int)),
inference(cnf,[status(esa)],[fact_61_int__less__0__conv]) ).
cnf(l101,plain,
~ ord_less(int,semiring_1_of_nat(int,zero_zero(nat)),zero_zero(int)),
inference(instantiation,[status(thm)],[127]) ).
fof(fact_80_zadd__0,plain,
! [Z] : plus_plus(int,zero_zero(int),Z) = Z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_80_zadd__0) ).
cnf(152,plain,
plus_plus(int,zero_zero(int),X0) = X0,
inference(cnf,[status(esa)],[fact_80_zadd__0]) ).
cnf(l81,plain,
plus_plus(int,zero_zero(int),int) = int,
inference(instantiation,[status(thm)],[152]) ).
cnf(l97,plain,
plus_plus(int,zero_zero(int),int) = int,
inference(instantiation,[status(thm)],[152]) ).
fof(fact_28_int__0,plain,
semiring_1_of_nat(int,zero_zero(nat)) = zero_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_int__0) ).
cnf(71,plain,
semiring_1_of_nat(int,zero_zero(nat)) = zero_zero(int),
inference(cnf,[status(esa)],[fact_28_int__0]) ).
cnf(l41,plain,
semiring_1_of_nat(int,zero_zero(nat)) = zero_zero(int),
inference(instantiation,[status(thm)],[71]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l46,l42,l38,l67,l68,l76,l101,l81,l97,l41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : NUM925+5 : TPTP v9.0.0. Released v5.3.0.
% 0.07/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n026.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 : 300
% 0.12/0.33 % DateTime : Mon Jul 21 14:28:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 9
% 0.19/0.38 % launching worker at depth: 10
% 6.46/1.18 % launching worker at depth: 11
% 7.06/1.25 % SZS status Theorem for theBenchmark
% 7.06/1.25 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------