%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUM925+6 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n023.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 11:45:52 EDT 2022
% Result : Theorem 0.62s 1.40s
% Output : Proof 0.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM925+6 : TPTP v8.1.0. Released v5.3.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n023.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 : 600
% 0.12/0.33 % DateTime : Thu Jul 7 09:50:11 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.62/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.62/1.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.62/1.41
% 0.62/1.41 %-----------------------------------------------------
% 0.62/1.41 fof(conj_0, conjecture, (! 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('/export/starexec/sandbox/benchmark/theBenchmark.p', conj_0)).
% 0.62/1.41 fof(fact_0_n1pos, 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('/export/starexec/sandbox/benchmark/theBenchmark.p', fact_0_n1pos)).
% 0.62/1.41 fof(fact_5_zero__eq__power2, axiom, ! [_348632] : (ring_11004092258visors(_348632) => ! [_348647] : (hAPP(nat, _348632, power_power(_348632, _348647), number_number_of(nat, hAPP(int, int, bit0, hAPP(int, int, bit1, pls)))) = zero_zero(_348632) <=> ti(_348632, _348647) = zero_zero(_348632))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fact_5_zero__eq__power2)).
% 0.62/1.41 fof(fact_95_zero__less__power2, axiom, ! [_349091] : (linordered_idom(_349091) => ! [_349106] : (hBOOL(hAPP(_349091, bool, hAPP(_349091, fun(_349091, bool), ord_less(_349091), zero_zero(_349091)), hAPP(nat, _349091, power_power(_349091, _349106), number_number_of(nat, hAPP(int, int, bit0, hAPP(int, int, bit1, pls)))))) <=> (! ti(_349091, _349106)) = zero_zero(_349091))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fact_95_zero__less__power2)).
% 0.62/1.41 fof(fact_178_zero__less__power, axiom, ! [_349631] : (linordered_semidom(_349631) => ! [_349646, _349649] : (hBOOL(hAPP(_349631, bool, hAPP(_349631, fun(_349631, bool), ord_less(_349631), zero_zero(_349631)), _349649)) => hBOOL(hAPP(_349631, bool, hAPP(_349631, fun(_349631, bool), ord_less(_349631), zero_zero(_349631)), hAPP(nat, _349631, power_power(_349631, _349649), _349646))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fact_178_zero__less__power)).
% 0.62/1.41 fof(arity_Int_Oint___Rings_Oring__1__no__zero__divisors, axiom, ring_11004092258visors(int), file('/export/starexec/sandbox/benchmark/theBenchmark.p', arity_Int_Oint___Rings_Oring__1__no__zero__divisors)).
% 0.62/1.41 fof(arity_Int_Oint___Rings_Olinordered__semidom, axiom, linordered_semidom(int), file('/export/starexec/sandbox/benchmark/theBenchmark.p', arity_Int_Oint___Rings_Olinordered__semidom)).
% 0.62/1.41 fof(arity_Int_Oint___Rings_Olinordered__idom, axiom, linordered_idom(int), file('/export/starexec/sandbox/benchmark/theBenchmark.p', arity_Int_Oint___Rings_Olinordered__idom)).
% 0.62/1.41
% 0.62/1.41 cnf(1, plain, [-(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))], clausify(conj_0)).
% 0.62/1.41 cnf(2, plain, [-(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)))))], clausify(fact_0_n1pos)).
% 0.62/1.41 cnf(3, plain, [ring_11004092258visors(_46631), hAPP(nat, _46631, power_power(_46631, _46634), number_number_of(nat, hAPP(int, int, bit0, hAPP(int, int, bit1, pls)))) = zero_zero(_46631), -(ti(_46631, _46634) = zero_zero(_46631))], clausify(fact_5_zero__eq__power2)).
% 0.62/1.41 cnf(4, plain, [linordered_idom(_51732), hBOOL(hAPP(_51732, bool, hAPP(_51732, fun(_51732, bool), ord_less(_51732), zero_zero(_51732)), hAPP(nat, _51732, power_power(_51732, _51735), number_number_of(nat, hAPP(int, int, bit0, hAPP(int, int, bit1, pls)))))), ti(_51732, _51735) = zero_zero(_51732)], clausify(fact_95_zero__less__power2)).
% 0.62/1.41 cnf(5, plain, [linordered_semidom(_57614), hBOOL(hAPP(_57614, bool, hAPP(_57614, fun(_57614, bool), ord_less(_57614), zero_zero(_57614)), _57618)), -(hBOOL(hAPP(_57614, bool, hAPP(_57614, fun(_57614, bool), ord_less(_57614), zero_zero(_57614)), hAPP(nat, _57614, power_power(_57614, _57618), _57617))))], clausify(fact_178_zero__less__power)).
% 0.62/1.41 cnf(6, plain, [-(ring_11004092258visors(int))], clausify(arity_Int_Oint___Rings_Oring__1__no__zero__divisors)).
% 0.62/1.41 cnf(7, plain, [-(linordered_semidom(int))], clausify(arity_Int_Oint___Rings_Olinordered__semidom)).
% 0.62/1.41 cnf(8, plain, [-(linordered_idom(int))], clausify(arity_Int_Oint___Rings_Olinordered__idom)).
% 0.62/1.41
% 0.62/1.41 cnf('1',plain,[linordered_idom(int), hBOOL(hAPP(int, bool, hAPP(int, fun(int, bool), ord_less(int), zero_zero(int)), 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)))))), ti(int, hAPP(int, int, plus_plus(int, one_one(int)), hAPP(nat, int, semiring_1_of_nat(int), n))) = zero_zero(int)],start(4,bind([[_51735, _51732], [hAPP(int, int, plus_plus(int, one_one(int)), hAPP(nat, int, semiring_1_of_nat(int), n)), int]]))).
% 0.62/1.41 cnf('1.1',plain,[-(linordered_idom(int))],extension(8)).
% 0.62/1.41 cnf('1.2',plain,[-(hBOOL(hAPP(int, bool, hAPP(int, fun(int, bool), ord_less(int), zero_zero(int)), 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))))))), linordered_semidom(int), 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))))],extension(5,bind([[_57617, _57614, _57618], [number_number_of(nat, hAPP(int, int, bit0, hAPP(int, int, bit1, pls))), int, hAPP(int, int, plus_plus(int, one_one(int)), hAPP(nat, int, semiring_1_of_nat(int), n))]]))).
% 0.62/1.41 cnf('1.2.1',plain,[-(linordered_semidom(int))],extension(7)).
% 0.62/1.41 cnf('1.2.2',plain,[-(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)))))],extension(2)).
% 0.62/1.41 cnf('1.3',plain,[-(ti(int, hAPP(int, int, plus_plus(int, one_one(int)), hAPP(nat, int, semiring_1_of_nat(int), n))) = zero_zero(int)), ring_11004092258visors(int), 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)],extension(3,bind([[_46634, _46631], [hAPP(int, int, plus_plus(int, one_one(int)), hAPP(nat, int, semiring_1_of_nat(int), n)), int]]))).
% 0.62/1.41 cnf('1.3.1',plain,[-(ring_11004092258visors(int))],extension(6)).
% 0.62/1.41 cnf('1.3.2',plain,[-(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))],extension(1)).
% 0.62/1.41 %-----------------------------------------------------
% 0.62/1.42
% 0.62/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------