Inference procedure has parameters: Ice fuel: 200 Timeout: 60s Convolution: right Learning problem is: env: { nat -> {s, z} ; nat_bin_tree -> {leaf, node} } definition: { } properties: {() -> eq_nat([j, j])} over-approximation: {} under-approximation: {} Clause system for inference is: { () -> eq_nat([j, j]) -> 0 } Solving took 0.004920 seconds. Proved Model: |_ { } -- Equality automata are defined for: {eq_nat, eq_nat_bin_tree} _| ------------------- STEPS: Total time: 0.004920 Reason for stopping: Proved