Checker "kiota" on test "reachability"
Checker: kiota 路 Version: 0.1.0 路 馃搫 Declaration 路 馃敆 Source
Test: reachability 路 Expected: 馃憤 accept 路 Size: 18.1鈥疢B 路 Lines: 361.8鈥痥 路 lean4export: 3.1.0 路 Lean: 4.34.1 路 Timeout: 15.2鈥痬in 路 馃搫 Declaration 路 馃敆 Source
Result: 馃憤 accepted 路 exit code 0 路 wall time: 25.0鈥痵 路 instructions: 141.5鈥疓 路 max rss memory: 2.0鈥疓B 路 run 2026-10-24 16:26:28 UTC
stderr:
[decl #100] theorem Or.comm [decl #200] def Set.instMembership [decl #300] theorem Classical.propDecidable._proof_1 [decl #400] def _private.Init.Data.Nat.Basic.0.Nat.lt_trichotomy.match_1_3 [decl #500] def Nat.mod.match_1 [decl #600] def Int.sub [decl #700] theorem Nat.le_antisymm [decl #800] def Lean.Omega.tidy?.match_1 [decl #900] theorem Int.natAbs_negOfNat [decl #1000] def _private.Init.Data.Int.DivMod.Bootstrap.0.Int.add_ediv_of_dvd_right.match_1_1 [decl #1100] def _private.Init.Data.Int.DivMod.Bootstrap.0.Int.dvd_neg.match_1_3 [decl #1200] theorem Lean.Omega.IntList.mul_smul_left [decl #1300] def List.get [decl #1400] def String.toByteArray [decl #1500] theorem List.count_pos_iff [decl #1600] def List.decidableBAll.match_3 [decl #1700] def Int.Internal.Linear.Var [decl #1800] theorem Lean.Data.AC.evalList.eq_2 [decl #1900] theorem _private.Init.Data.Int.LemmasAux.0.Int.ble'_eq_true._proof_1_4 [decl #2000] theorem not_not_of_not_imp [decl #2100] def Prod.Lex.casesOn [decl #2200] def Nat.Internal.Linear.Poly.denote_append._f [decl #2300] def Lean.Grind.Ring.toNeg [decl #2400] theorem Lean.Grind.Semiring.natCast_add [decl #2500] theorem Lean.Grind.CommRing.Poly.insert.go.match_1.congr_eq_2 [decl #2600] theorem _private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqMon.beq.match_1.eq_3 [decl #2700] theorem Lean.Grind.OrderedRing.zero_lt_one [decl #2800] def _private.Init.Data.List.Find.0.List.filter.match_1.splitter [decl #2900] def List.diff._f [decl #3000] theorem Multiset.add._proof_1 [decl #3100] def NSMul.nsmul [decl #3200] def AdjList.reachableWithin._f [decl #3300] def PartialOrder.ofSetLike [decl #3400] theorem Lean.Grind.AC.eq_expr_seq_seq [decl #3500] theorem AdjList.searchFrom_reachableWithin._proof_1_4 [decl #3600] theorem sup_le_sup_right [decl #3700] theorem sdiff_le [decl #3800] theorem lt_trans [decl #3900] def AdjList.transGen_iff_mem_reachableWithin_of_le.match_1_3 INTERN_CALLS 100000000 nodes=6548866 [decl #4000] theorem Multiset.attach._proof_1 [decl #4100] theorem WithTop.semilatticeInf._proof_5 [decl #4200] theorem Fin.coe_max