%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NUM925+1 : TPTP v8.1.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %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:47:21 EDT 2022 % Result : Theorem 0.49s 0.66s % Output : Proof 0.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM925+1 : TPTP v8.1.0. Released v5.3.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.34 % Computer : n029.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Tue Jul 5 06:58:42 EDT 2022 % 0.14/0.34 % CPUTime : % 0.49/0.66 % SZS status Theorem % 0.49/0.66 (* PROOF-FOUND *) % 0.49/0.66 (* BEGIN-PROOF *) % 0.49/0.66 % SZS output start Proof % 0.49/0.66 1. ((pls) = (zero_zero_int)) ((zero_zero_int) != (pls)) ### Sym(=) % 0.49/0.66 2. ((plus_plus_int (one_one_int) (semiri1621563631at_int (n))) = (zero_zero_int)) ((plus_plus_int (one_one_int) (semiri1621563631at_int (n))) != (zero_zero_int)) ### Axiom % 0.49/0.66 3. (-. (ord_less_int (pls) (zero_zero_int))) (ord_less_int (zero_zero_int) (plus_plus_int (one_one_int) (semiri1621563631at_int (n)))) ((plus_plus_int (one_one_int) (semiri1621563631at_int (n))) = (zero_zero_int)) ((pls) = (zero_zero_int)) ### P-NotP 1 2 % 0.49/0.66 4. (-. ((plus_plus_int (one_one_int) (semiri1621563631at_int (n))) != (zero_zero_int))) ((pls) = (zero_zero_int)) (ord_less_int (zero_zero_int) (plus_plus_int (one_one_int) (semiri1621563631at_int (n)))) (-. (ord_less_int (pls) (zero_zero_int))) ### NotNot 3 % 0.49/0.66 5. ((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) ((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) != (zero_zero_int)) ### Axiom % 0.49/0.66 6. ((plus_plus_int (one_one_int) (semiri1621563631at_int (n))) != (zero_zero_int)) ((plus_plus_int (one_one_int) (semiri1621563631at_int (n))) = (zero_zero_int)) ### Axiom % 0.49/0.66 7. (((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) <=> ((plus_plus_int (one_one_int) (semiri1621563631at_int (n))) = (zero_zero_int))) ((plus_plus_int (one_one_int) (semiri1621563631at_int (n))) != (zero_zero_int)) ((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) ### Equiv 5 6 % 0.49/0.66 8. (All A_1, (((power_power_int A_1 (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) <=> (A_1 = (zero_zero_int)))) ((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) ((plus_plus_int (one_one_int) (semiri1621563631at_int (n))) != (zero_zero_int)) ### All 7 % 0.49/0.66 9. ((ord_less_int (zero_zero_int) (power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls)))))) <=> ((plus_plus_int (one_one_int) (semiri1621563631at_int (n))) != (zero_zero_int))) ((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) (All A_1, (((power_power_int A_1 (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) <=> (A_1 = (zero_zero_int)))) (-. (ord_less_int (pls) (zero_zero_int))) (ord_less_int (zero_zero_int) (plus_plus_int (one_one_int) (semiri1621563631at_int (n)))) ((pls) = (zero_zero_int)) ### Equiv 4 8 % 0.49/0.66 10. (All A_1, ((ord_less_int (zero_zero_int) (power_power_int A_1 (number_number_of_nat (bit0 (bit1 (pls)))))) <=> (A_1 != (zero_zero_int)))) ((pls) = (zero_zero_int)) (ord_less_int (zero_zero_int) (plus_plus_int (one_one_int) (semiri1621563631at_int (n)))) (-. (ord_less_int (pls) (zero_zero_int))) (All A_1, (((power_power_int A_1 (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) <=> (A_1 = (zero_zero_int)))) ((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) ### All 9 % 0.49/0.66 11. (-. ((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) != (zero_zero_int))) (All A_1, (((power_power_int A_1 (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) <=> (A_1 = (zero_zero_int)))) (-. (ord_less_int (pls) (zero_zero_int))) (ord_less_int (zero_zero_int) (plus_plus_int (one_one_int) (semiri1621563631at_int (n)))) ((pls) = (zero_zero_int)) (All A_1, ((ord_less_int (zero_zero_int) (power_power_int A_1 (number_number_of_nat (bit0 (bit1 (pls)))))) <=> (A_1 != (zero_zero_int)))) ### NotNot 10 % 0.49/0.66 % SZS output end Proof % 0.49/0.66 (* END-PROOF *) %------------------------------------------------------------------------------