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