%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NUM925+2 : 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 : n021.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:28 PM UTC 2025
% Result : Theorem 6.99s 1.25s
% Output : CNFRefutation 6.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 11
% Syntax : Number of formulae : 39 ( 24 unt; 0 def)
% Number of atoms : 72 ( 31 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 67 ( 34 ~; 26 |; 1 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-2 aty)
% Number of variables : 26 ( 3 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(conj_0,plain,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_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,
~ ( hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(973,plain,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(cnf,[status(esa)],[conj_0_negated]) ).
cnf(l0,plain,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(instantiation,[status(thm)],[973]) ).
fof(fact_476_add__nonneg__eq__0__iff,plain,
! [Ya,Xa] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),Xa))
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),Ya))
=> ( hAPP_int_int(plus_plus_int(Xa),Ya) = zero_zero_int
<=> ( Xa = zero_zero_int
& Ya = zero_zero_int ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_476_add__nonneg__eq__0__iff) ).
cnf(673,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),X0))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),X1))
| X0 != zero_zero_int
| X1 != zero_zero_int
| hAPP_int_int(plus_plus_int(X1),X0) = zero_zero_int ),
inference(cnf,[status(esa)],[fact_476_add__nonneg__eq__0__iff]) ).
cnf(l1,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls))))))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),one_one_int))
| hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int
| one_one_int != zero_zero_int
| hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls))))) = zero_zero_int ),
inference(instantiation,[status(thm)],[673]) ).
fof(fact_684_ord__eq__le__trans,plain,
! [C,A_1,B_1] :
( A_1 = B_1
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,B_1),C))
=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A_1),C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_684_ord__eq__le__trans) ).
cnf(946,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| X2 != X0
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X2),X1)) ),
inference(cnf,[status(esa)],[fact_684_ord__eq__le__trans]) ).
cnf(l6,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls))))))
| zero_zero_int != hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))))) ),
inference(instantiation,[status(thm)],[946]) ).
fof(fact_657_order__refl,plain,
! [X_7] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X_7),X_7)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_657_order__refl) ).
cnf(919,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X0)),
inference(cnf,[status(esa)],[fact_657_order__refl]) ).
cnf(l7,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))))),
inference(instantiation,[status(thm)],[919]) ).
cnf(671,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),X0))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),X1))
| hAPP_int_int(plus_plus_int(X1),X0) != zero_zero_int
| X1 = zero_zero_int ),
inference(cnf,[status(esa)],[fact_476_add__nonneg__eq__0__iff]) ).
cnf(l8,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls))))))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),one_one_int))
| hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls))))) != zero_zero_int
| one_one_int = zero_zero_int ),
inference(instantiation,[status(thm)],[671]) ).
fof(fact_226_one__neq__zero,plain,
one_one_int != zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_226_one__neq__zero) ).
cnf(331,plain,
one_one_int != zero_zero_int,
inference(cnf,[status(esa)],[fact_226_one__neq__zero]) ).
cnf(l21,plain,
one_one_int != zero_zero_int,
inference(instantiation,[status(thm)],[331]) ).
fof(fact_521_Nat__Transfer_Otransfer__nat__int__function__closures_I6_J,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),one_one_int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_521_Nat__Transfer_Otransfer__nat__int__function__closures_I6_J) ).
cnf(726,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),one_one_int)),
inference(cnf,[status(esa)],[fact_521_Nat__Transfer_Otransfer__nat__int__function__closures_I6_J]) ).
cnf(l9,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),one_one_int)),
inference(instantiation,[status(thm)],[726]) ).
fof(fact_591_zero__le__power2,plain,
! [A_5] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(power_power_int(A_5),number_number_of_nat(bit0(bit1(pls)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_591_zero__le__power2) ).
cnf(813,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls)))))),
inference(cnf,[status(esa)],[fact_591_zero__le__power2]) ).
cnf(l10,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))))),
inference(instantiation,[status(thm)],[813]) ).
fof(fact_439_zle__linear,plain,
! [Z_2,W] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,W),Z_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_439_zle__linear) ).
cnf(607,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X1),X0)) ),
inference(cnf,[status(esa)],[fact_439_zle__linear]) ).
cnf(l2,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),one_one_int))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),zero_zero_int)) ),
inference(instantiation,[status(thm)],[607]) ).
fof(fact_494_not__one__le__zero,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),zero_zero_int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_494_not__one__le__zero) ).
cnf(691,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),zero_zero_int)),
inference(cnf,[status(esa)],[fact_494_not__one__le__zero]) ).
cnf(l4,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),zero_zero_int)),
inference(instantiation,[status(thm)],[691]) ).
cnf(l11,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(semiri1621563631at_int,n)))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),one_one_int))
| hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)) != zero_zero_int
| one_one_int = zero_zero_int ),
inference(instantiation,[status(thm)],[671]) ).
cnf(l13,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),one_one_int)),
inference(instantiation,[status(thm)],[726]) ).
fof(fact_231_field__power__not__zero,plain,
! [N_23,A_62] :
( A_62 != zero_zero_int
=> hAPP_nat_int(power_power_int(A_62),N_23) != zero_zero_int ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_231_field__power__not__zero) ).
cnf(336,plain,
( hAPP_nat_int(power_power_int(X0),X1) != zero_zero_int
| X0 = zero_zero_int ),
inference(cnf,[status(esa)],[fact_231_field__power__not__zero]) ).
cnf(l14,plain,
( hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int
| hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)) = zero_zero_int ),
inference(instantiation,[status(thm)],[336]) ).
fof(fact_524_Nat__Transfer_Otransfer__nat__int__function__closures_I9_J,plain,
! [Z_2] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(semiri1621563631at_int,Z_2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_524_Nat__Transfer_Otransfer__nat__int__function__closures_I9_J) ).
cnf(729,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(semiri1621563631at_int,X0))),
inference(cnf,[status(esa)],[fact_524_Nat__Transfer_Otransfer__nat__int__function__closures_I9_J]) ).
cnf(l12,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(semiri1621563631at_int,n))),
inference(instantiation,[status(thm)],[729]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l6,l7,l8,l21,l9,l10,l2,l4,l11,l13,l14,l12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM925+2 : TPTP v9.0.0. Released v5.3.0.
% 0.06/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n021.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:26:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.37 % launching worker at depth: 2
% 0.12/0.37 % launching worker at depth: 4
% 0.12/0.37 % launching worker at depth: 5
% 0.12/0.37 % launching worker at depth: 1
% 0.12/0.37 % launching worker at depth: 3
% 0.12/0.37 % launching worker at depth: 6
% 0.12/0.37 % launching worker at depth: 7
% 0.12/0.37 % launching worker at depth: 8
% 0.12/0.38 % launching worker at depth: 9
% 0.19/0.57 % launching worker at depth: 10
% 6.99/1.25 % SZS status Theorem for theBenchmark
% 6.99/1.25 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------