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