%------------------------------------------------------------------------------ % File : Satallax---3.5 % Problem : NUM636^3 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % Computer : n012.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 : Thu Oct 9 02:11:34 PM UTC 2025 % Result : Theorem 13.29s 13.30s % Output : Proof 13.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : NUM636^3 : TPTP v9.2.0. Released v3.7.0. % 0.12/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % 0.12/0.33 % Computer : n012.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 : Wed Oct 8 23:10:23 EDT 2025 % 0.12/0.33 % CPUTime : % 13.29/13.30 % SZS status Theorem % 13.29/13.30 % Mode: mode454 % 13.29/13.30 % Inferences: 4 % 13.29/13.30 % SZS output start Proof % 13.29/13.30 thf(ty_succ, type, succ : ($i>$i)). % 13.29/13.30 thf(ty_one, type, one : $i). % 13.29/13.30 thf(sP1,plain,sP1 <=> (![X1:$i]:((~(((succ @ X1) = X1))) => (~(((succ @ (succ @ X1)) = (succ @ X1)))))),introduced(definition,[new_symbols(definition,[sP1])])). % 13.29/13.30 thf(sP2,plain,sP2 <=> ((~(((succ @ one) = one))) => (~(sP1))),introduced(definition,[new_symbols(definition,[sP2])])). % 13.29/13.30 thf(sP3,plain,sP3 <=> ((succ @ one) = one),introduced(definition,[new_symbols(definition,[sP3])])). % 13.29/13.30 thf(sP4,plain,sP4 <=> (![X1:$i]:(~(((succ @ X1) = X1)))),introduced(definition,[new_symbols(definition,[sP4])])). % 13.29/13.30 thf(sP5,plain,sP5 <=> (![X1:$i>$o]:((~(((X1 @ one) => (~((![X2:$i]:((X1 @ X2) => (X1 @ (succ @ X2))))))))) => ((!!) @ X1))),introduced(definition,[new_symbols(definition,[sP5])])). % 13.29/13.30 thf(sP6,plain,sP6 <=> ((~(sP2)) => sP4),introduced(definition,[new_symbols(definition,[sP6])])). % 13.29/13.30 thf(def_m,definition,(m = (^[X1:$i]:(~(((succ @ X1) = X1)))))). % 13.29/13.30 thf(m_is_all,conjecture,sP4). % 13.29/13.30 thf(h0,negated_conjecture,(~(sP4)),inference(assume_negation,[status(cth)],[m_is_all])). % 13.29/13.30 thf(1,plain,(~(sP5) | sP6),inference(all_rule,[status(thm)],[])). % 13.29/13.30 thf(2,plain,((~(sP6) | sP2) | sP4),inference(prop_rule,[status(thm)],[])). % 13.29/13.30 thf(3,plain,((~(sP2) | sP3) | ~(sP1)),inference(prop_rule,[status(thm)],[])). % 13.29/13.30 thf(induction,axiom,sP5). % 13.29/13.30 thf(m_is_one,axiom,(m @ one)). % 13.29/13.30 thf(4,plain,(~(sP3)),inference(preprocess,[status(thm)],[m_is_one]). % 13.29/13.30 thf(m_is_next,axiom,(![X1:$i]:((m @ X1) => (m @ (succ @ X1))))). % 13.29/13.30 thf(5,plain,sP1,inference(preprocess,[status(thm)],[m_is_next]). % 13.29/13.30 thf(6,plain,$false,inference(prop_unsat,[status(thm),assumptions([h0])],[1,2,3,induction,4,5,h0])). % 13.29/13.30 thf(0,theorem,sP4,inference(contra,[status(thm),contra(discharge,[h0])],[6,h0])). % 13.29/13.30 % SZS output end Proof %------------------------------------------------------------------------------