%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SWX217+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n003.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 : Tue May 5 07:08:38 PM UTC 2026 % Result : Unknown 2.86s 3.05s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX217+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_zenon_modulo %d %s % 0.17/0.33 % Computer : n003.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Tue May 5 12:14:56 EDT 2026 % 0.17/0.33 % CPUTime : % 2.86/3.05 Zenon error: exhausted search space without finding a proof % 2.86/3.05 (* Current branch: % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((suc (rd (nil))) != (half (zero))) % 2.86/3.05 (zenon_X7 != (shw (suc zenon_X4))) % 2.86/3.05 (zenon_X7 != (shw (zero))) % 2.86/3.05 ((rd (append (shw zenon_X6) (shw zenon_X5))) != (half (suc (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (shw (suc zenon_X3))) % 2.86/3.05 ((shw (half (suc zenon_X4))) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (shw (suc (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (shw (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons (o) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((half (suc zenon_X4)) != (suc (half (suc (zero))))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc zenon_X3))))) != (shw (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (cons (i) zenon_X8)) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (cons (o) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (o) (cons (o) (shw (half (suc (zero)))))) != (shw (zero))) % 2.86/3.05 ((append (shw zenon_X5) (shw zenon_X6)) != (shw (suc (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((zero) != (rd (append (shw zenon_X6) (shw zenon_X5)))) % 2.86/3.05 ((cons (i) (cons (i) (shw (half (suc zenon_X4))))) != (shw (zero))) % 2.86/3.05 ((append (shw zenon_X5) (shw zenon_X6)) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons (i) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((half (suc (rd (nil)))) != (suc (zero))) % 2.86/3.05 ((nil) != (cons (o) (cons (i) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != zenon_X1) % 2.86/3.05 ((cons (i) (shw (suc zenon_X4))) != (shw (zero))) % 2.86/3.05 ((cons (o) (cons (i) (shw (half (suc (rd (nil))))))) != (shw (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != zenon_X1) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != zenon_X1) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (shw (suc (half (zero))))) % 2.86/3.05 ((suc zenon_X4) != (suc (zero))) % 2.86/3.05 ((nil) != (cons (o) zenon_X7)) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X3))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (shw (half (suc (half (zero)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((half (suc zenon_X4)) != (half (zero))) % 2.86/3.05 ((nil) != (cons (i) (cons (i) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((nil) != (cons (i) (shw (suc (rd (nil)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons (o) (shw (half (suc zenon_X4))))) % 2.86/3.05 (zenon_X1 != (shw (suc (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((shw (half (suc (half (suc (zero)))))) != zenon_X7) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons (i) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (o) (cons (i) (shw (half (suc (half (suc (zero)))))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((o) != zenon_X0) % 2.86/3.05 ((half (suc (half (suc (zero))))) != (suc (zero))) % 2.86/3.05 ((cons (o) (shw (suc (rd (nil))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != zenon_X7) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((nil) != (cons (o) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc zenon_X4))))) != (shw (zero))) % 2.86/3.05 ((shw (half (suc (rd (nil))))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 (zenon_X3 != (rd (nil))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc (zero)))))) != (shw (zero))) % 2.86/3.05 ((cons (i) (cons (o) (shw (half (suc (rd (nil))))))) != (shw (zero))) % 2.86/3.05 ((half (suc zenon_X3)) != (suc (zero))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc zenon_X3))))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (cons (o) (shw (half (suc (half (suc (zero)))))))) != (shw (zero))) % 2.86/3.05 ((half (suc (half (suc (zero))))) != (suc (half (zero)))) % 2.86/3.05 ((suc zenon_X2) != (rd (nil))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != zenon_X1) % 2.86/3.05 ((cons (i) (cons (o) (shw (half (suc zenon_X3))))) != (shw (zero))) % 2.86/3.05 ((nil) != (cons (i) (shw (suc (half (zero)))))) % 2.86/3.05 (zenon_X8 != (shw (zero))) % 2.86/3.05 ((cons (i) (cons (o) (shw (half (suc (zero)))))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (suc zenon_X3))) != (shw (zero))) % 2.86/3.05 ((rd (append (shw zenon_X6) (shw zenon_X5))) != (half (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X4)))) != (shw (suc zenon_X4))) % 2.86/3.05 ((nil) != (cons (o) (cons (i) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((nil) != (cons (o) (shw (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (shw (suc (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons (i) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((half (suc (rd (nil)))) != (suc (half (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons (i) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((cons zenon_X0 (nil)) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc (half (zero))))))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc (rd (nil))))))) != (shw (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (shw (half (suc (half (zero)))))) % 2.86/3.05 ((nil) != (cons (o) (shw (suc (rd (nil)))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons zenon_X0 (shw (suc (zero)))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons (i) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((nil) != (cons (o) (cons (o) (shw (half (suc (half (suc (zero))))))))) % 2.86/3.05 (zenon_X4 != zenon_X3) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((shw (half (suc zenon_X3))) != (shw (suc (half (zero))))) % 2.86/3.05 ((nil) != (cons zenon_X0 (shw (suc (zero))))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc zenon_X4))))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc zenon_X3))))) != (shw (zero))) % 2.86/3.05 ((nil) != (cons zenon_X0 (shw (suc (rd (nil)))))) % 2.86/3.05 ((nil) != (cons (o) (cons (i) (shw (half (suc (half (zero)))))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((suc zenon_X2) != (half (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (cons (i) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (shw (half (suc (rd (nil)))))) % 2.86/3.05 ((shw (suc (zero))) = (cons (i) (shw (half (suc (zero)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != zenon_X1) % 2.86/3.05 ((rd (nil)) = (zero)) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((shw (zero)) != (shw (suc (rd (nil))))) % 2.86/3.05 ((append (shw zenon_X6) (shw zenon_X5)) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons (i) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((nil) != (cons (o) (shw (suc (zero))))) % 2.86/3.05 ((shw (suc zenon_X4)) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != zenon_X7) % 2.86/3.05 ((nil) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != zenon_X8) % 2.86/3.05 ((half (suc (half (suc (zero))))) != (suc (rd (nil)))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((shw (suc (half (zero)))) = (cons (i) (shw (half (suc (half (zero))))))) % 2.86/3.05 ((nil) != zenon_X8) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc zenon_X4))))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((shw (half (suc zenon_X4))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((shw (suc (rd (nil)))) = (cons (o) (shw (half (suc (rd (nil))))))) % 2.86/3.05 (zenon_X4 != (zero)) % 2.86/3.05 ((append (shw zenon_X6) (shw zenon_X5)) != (shw (suc zenon_X4))) % 2.86/3.05 ((shw (zero)) != (shw (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc (rd (nil)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((half (suc zenon_X4)) != (rd (nil))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons (i) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (o) (shw (suc zenon_X4))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons (i) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons (o) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons zenon_X0 zenon_X1) != (shw (suc (rd (nil))))) % 2.86/3.05 ((shw (suc (half (suc (zero))))) = (cons (i) (shw (half (suc (half (suc (zero)))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons (i) zenon_X8)) % 2.86/3.05 ((nil) != (cons (o) (cons (i) (shw (half (suc (half (suc (zero))))))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (shw (half (suc (half (suc (zero))))))) % 2.86/3.05 ((shw (half (suc zenon_X3))) != zenon_X1) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (shw (zero))) % 2.86/3.05 ((nil) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (i) zenon_X8) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != zenon_X1) % 2.86/3.05 ((shw (half (suc (half (zero))))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((suc (rd (nil))) != (rd (nil))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons (o) zenon_X7)) % 2.86/3.05 ((shw (half (suc (half (zero))))) != zenon_X8) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons (o) zenon_X7)) % 2.86/3.05 ((nil) != (cons (i) (cons (i) (shw (half (suc (rd (nil)))))))) % 2.86/3.05 ((cons (i) (shw (suc (half (zero))))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X4)))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((suc (half (zero))) != (suc zenon_X3)) % 2.86/3.05 ((half (suc (half (suc (zero))))) != (half (suc zenon_X3))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((suc (half (zero))) != (suc zenon_X4)) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != zenon_X8) % 2.86/3.05 ((suc zenon_X4) != (suc zenon_X3)) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((zero) != (suc (rd (nil)))) % 2.86/3.05 ((suc zenon_X3) != (half (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != zenon_X7) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (shw (suc zenon_X3))) % 2.86/3.05 ((shw (half (suc (zero)))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((shw (suc zenon_X4)) != (shw (suc (zero)))) % 2.86/3.05 ((shw (half (suc (rd (nil))))) != zenon_X7) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (cons (o) zenon_X7)) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (shw (suc zenon_X3))) % 2.86/3.05 ((shw (half (suc (zero)))) != zenon_X7) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons (i) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (o) (cons (o) (shw (half (suc zenon_X3))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X4))) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != zenon_X7) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (cons (i) zenon_X8)) % 2.86/3.05 ((cons zenon_X0 zenon_X1) != (shw (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((half (suc (rd (nil)))) != (suc (rd (nil)))) % 2.86/3.05 (zenon_X7 != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != zenon_X8) % 2.86/3.05 ((nil) != (cons (i) (shw (half (suc (half (zero))))))) % 2.86/3.05 ((half (suc zenon_X4)) != (suc zenon_X3)) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((half (suc (zero))) = (zero)) % 2.86/3.05 ((i) != zenon_X0) % 2.86/3.05 ((shw (suc zenon_X4)) != (shw (zero))) % 2.86/3.05 ((append (shw zenon_X5) (shw zenon_X6)) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (shw (suc zenon_X4))) % 2.86/3.05 ((half (suc zenon_X3)) != (suc zenon_X3)) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc (zero))))) % 2.86/3.05 ((rd (append (shw zenon_X6) (shw zenon_X5))) != (rd (nil))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc zenon_X3))))) != (shw (suc (zero)))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc (zero)))))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (cons (o) zenon_X7)) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((rd (append (shw zenon_X5) (shw zenon_X6))) = (rd (append (shw zenon_X6) (shw zenon_X5)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (shw (half (suc (zero))))) % 2.86/3.05 ((cons (o) (cons (o) (shw (half (suc (zero)))))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((suc zenon_X4) != (rd (nil))) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X4))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (o) (shw (suc (half (zero))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (nil)) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((half (suc zenon_X4)) != (suc (half (zero)))) % 2.86/3.05 ((shw (half (suc (zero)))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (shw (half (suc (rd (nil)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((nil) != (cons (o) (cons (i) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (i) (shw (suc (rd (nil))))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc zenon_X3))))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((suc (half (suc (zero)))) != (rd (nil))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (shw (half (suc (half (suc (zero))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons (i) zenon_X8)) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons (i) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((shw (half (suc zenon_X3))) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons (i) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X3)))) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons (i) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 (evenNat (zero)) % 2.86/3.05 ((shw (suc (zero))) = (cons (o) (shw (half (suc (zero)))))) % 2.86/3.05 ((append (shw zenon_X5) (shw zenon_X6)) != (shw (zero))) % 2.86/3.05 ((shw (half (suc zenon_X3))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (o) (cons (o) (shw (half (suc (half (zero))))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((half (suc (half (suc (zero))))) != (suc (half (suc (zero))))) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X3)))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons zenon_X0 (shw (suc (rd (nil))))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc (zero)))))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons (i) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((suc (zero)) != (rd (nil))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != zenon_X8) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X4))) != (shw (zero))) % 2.86/3.05 ((shw (suc zenon_X3)) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc (zero)))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X4)))) != (shw (suc zenon_X3))) % 2.86/3.05 ((suc zenon_X2) != (half (suc (zero)))) % 2.86/3.05 ((shw (half (suc zenon_X4))) != (shw (suc (zero)))) % 2.86/3.05 ((cons zenon_X0 (nil)) != (shw (zero))) % 2.86/3.05 ((shw (half (suc (rd (nil))))) != zenon_X8) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (shw (half (suc (half (suc (zero))))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (cons (i) zenon_X8)) % 2.86/3.05 ((append (shw zenon_X5) (shw zenon_X6)) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (o) (cons (o) (shw (half (suc zenon_X4))))) != (shw (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (shw (half (suc (half (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons zenon_X0 (shw (zero))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((shw (half (suc (half (suc (zero)))))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (shw (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc (half (suc (zero))))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != zenon_X7) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((shw (half (suc (half (suc (zero)))))) != (shw (suc (zero)))) % 2.86/3.05 ((cons (o) (cons (i) (shw (half (suc (half (zero))))))) != (shw (zero))) % 2.86/3.05 ((suc zenon_X2) != (rd (append (shw zenon_X5) (shw zenon_X6)))) % 2.86/3.05 ((shw (suc zenon_X4)) = (cons (i) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((shw (half (suc zenon_X3))) != (shw (suc (zero)))) % 2.86/3.05 ((nil) != (cons (o) (cons (o) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons (i) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons (i) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((nil) != (cons (o) (shw (half (suc (half (zero))))))) % 2.86/3.05 ((shw (zero)) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (i) (cons (o) (shw (half (suc (half (zero))))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons (o) zenon_X7)) % 2.86/3.05 ((nil) != (cons (o) (nil))) % 2.86/3.05 ((cons (o) zenon_X7) != (shw (suc (half (zero))))) % 2.86/3.05 ((shw (half (suc zenon_X4))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((nil) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons (i) zenon_X8)) % 2.86/3.05 ((zero) != (suc (half (suc (zero))))) % 2.86/3.05 ((half (suc (half (zero)))) != (half (suc zenon_X4))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc (rd (nil))))))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 (nil)) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc (half (suc (zero))))))) % 2.86/3.05 ((suc zenon_X4) != (suc (half (suc (zero))))) % 2.86/3.05 ((nil) != zenon_X7) % 2.86/3.05 ((half (suc zenon_X3)) != (suc zenon_X4)) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons (i) zenon_X8)) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X3)))) != (shw (zero))) % 2.86/3.05 ((cons (o) zenon_X7) != (shw (suc (zero)))) % 2.86/3.05 ((nil) != (shw (suc zenon_X4))) % 2.86/3.05 ((rd (append (shw zenon_X5) (shw zenon_X6))) != (half (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons zenon_X0 (nil)) != (shw (suc (rd (nil))))) % 2.86/3.05 ((suc (half (zero))) != (half (suc (zero)))) % 2.86/3.05 ((nil) != (cons (o) (cons (o) (shw (half (suc (rd (nil)))))))) % 2.86/3.05 ((cons (i) (cons (i) (shw (half (suc (half (zero))))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (cons (o) (shw (half (suc (zero)))))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons (i) zenon_X8)) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X3))) != (shw (suc zenon_X3))) % 2.86/3.05 ((half (suc (half (zero)))) != (half (suc zenon_X3))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != zenon_X7) % 2.86/3.05 ((suc zenon_X3) != (rd (nil))) % 2.86/3.05 ((cons (o) zenon_X7) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((nil) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((half (suc zenon_X3)) != (suc (rd (nil)))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (shw (half (suc (zero))))) % 2.86/3.05 ((cons zenon_X0 (shw (suc (half (zero))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((shw (suc zenon_X3)) != (shw (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (o) (cons (o) (shw (half (suc (rd (nil))))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((nil) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((nil) != (cons (i) (cons (i) (shw (half (suc (zero))))))) % 2.86/3.05 ((zero) != (suc (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X3)))) != (shw (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != zenon_X8) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (o) (cons (i) (shw (half (suc zenon_X3))))) != (shw (zero))) % 2.86/3.05 ((half (suc (half (zero)))) != (suc (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((cons (i) (shw (suc (zero)))) != (shw (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (cons (o) zenon_X7)) % 2.86/3.05 ((nil) != (cons (i) (nil))) % 2.86/3.05 ((shw (half (suc (rd (nil))))) != (shw (suc (half (zero))))) % 2.86/3.05 ((shw (suc zenon_X4)) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (o) (cons (o) (shw (half (suc (zero)))))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (shw (half (suc (half (suc (zero))))))) % 2.86/3.05 (zenon_X8 != (shw (suc (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((append (shw zenon_X5) (shw zenon_X6)) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons (o) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (shw (suc (zero)))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc (half (suc (zero)))))))) != (shw (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != zenon_X8) % 2.86/3.05 ((cons (i) zenon_X8) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (o) zenon_X7) != (shw (zero))) % 2.86/3.05 ((half (suc zenon_X3)) != (rd (nil))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons (i) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc zenon_X4))))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons (o) zenon_X7)) % 2.86/3.05 (zenon_X1 != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (o) zenon_X7) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons (o) zenon_X7)) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons (o) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((append (shw zenon_X6) (shw zenon_X5)) != (shw (zero))) % 2.86/3.05 ((shw (suc zenon_X3)) = (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((shw (suc (rd (nil)))) = (cons (i) (shw (half (suc (rd (nil))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((shw (suc zenon_X3)) = (cons (i) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X4))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((shw (half (suc (rd (nil))))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((suc zenon_X3) != (suc (zero))) % 2.86/3.05 ((zero) != (half (suc zenon_X4))) % 2.86/3.05 ((suc zenon_X4) != (half (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons (o) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((shw (half (suc zenon_X3))) != zenon_X7) % 2.86/3.05 ((nil) != (cons (i) (shw (zero)))) % 2.86/3.05 ((shw (half (suc (zero)))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons (o) zenon_X7)) % 2.86/3.05 ((nil) != (cons (i) (cons (i) (shw (half (suc (half (zero)))))))) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X4)))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc (half (suc (zero)))))))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X3)))) != (shw (suc zenon_X3))) % 2.86/3.05 ((nil) != (cons (i) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc zenon_X3))))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((nil) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((nil) != (cons zenon_X0 (shw (suc (half (suc (zero))))))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc zenon_X4))))) != (shw (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((half (suc (rd (nil)))) != (suc (half (suc (zero))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons zenon_X0 (shw (suc (half (suc (zero)))))) != (shw (zero))) % 2.86/3.05 ((shw (zero)) = (nil)) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons (i) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((nil) != (cons zenon_X0 (nil))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (shw (suc zenon_X4))) % 2.86/3.05 ((shw (suc zenon_X4)) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((append (shw zenon_X6) (shw zenon_X5)) != (shw (suc (zero)))) % 2.86/3.05 ((nil) != (cons (o) (shw (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((nil) != (cons (o) (shw (suc (half (suc (zero))))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((cons (i) (cons (i) (shw (half (suc (half (suc (zero)))))))) != (shw (zero))) % 2.86/3.05 (zenon_X1 != (shw (zero))) % 2.86/3.05 ((append (shw zenon_X6) (shw zenon_X5)) != (nil)) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X3)))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc (zero)))))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((nil) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((suc (half (suc (zero)))) != (half (suc (zero)))) % 2.86/3.05 (zenon_X1 != (shw (suc (half (zero))))) % 2.86/3.05 ((shw (half (suc zenon_X3))) != zenon_X8) % 2.86/3.05 ((cons (o) zenon_X7) != (shw (suc (rd (nil))))) % 2.86/3.05 ((nil) != (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((zero) != (half (suc zenon_X3))) % 2.86/3.05 ((suc zenon_X3) != (half (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != zenon_X1) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons (i) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != zenon_X1) % 2.86/3.05 ((nil) != (cons (o) (cons (o) (shw (half (suc (half (zero)))))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (shw (half (suc (rd (nil)))))) % 2.86/3.05 ((cons (i) zenon_X8) != (shw (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != zenon_X1) % 2.86/3.05 ((half (suc zenon_X4)) != (suc (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((shw (half (suc (half (suc (zero)))))) != (cons (o) (shw (half (suc (zero)))))) % 2.86/3.05 ((shw (suc zenon_X3)) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (cons (o) zenon_X7)) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X4))) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != zenon_X8) % 2.86/3.05 (zenon_X3 != (half (suc (zero)))) % 2.86/3.05 ((nil) != (cons (i) (cons (o) (shw (half (suc (rd (nil)))))))) % 2.86/3.05 ((cons (i) zenon_X8) != (shw (suc (rd (nil))))) % 2.86/3.05 ((append (shw zenon_X6) (shw zenon_X5)) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((shw (half (suc (rd (nil))))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != zenon_X7) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc zenon_X4))))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (i) (shw (half (suc (rd (nil)))))))) % 2.86/3.05 ((cons (o) (shw (suc (zero)))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 (shw (zero))) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X3))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc (half (zero)))))) % 2.86/3.05 ((half (zero)) = (zero)) % 2.86/3.05 ((shw (half (suc (half (suc (zero)))))) != (shw (suc (rd (nil))))) % 2.86/3.05 (zenon_X8 != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X3))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons zenon_X0 zenon_X1) != (shw (zero))) % 2.86/3.05 ((half (suc (half (zero)))) != (suc (half (suc (zero))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (o) zenon_X7) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc zenon_X3))))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (shw (half (suc (rd (nil)))))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc zenon_X4))))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons (i) zenon_X8)) % 2.86/3.05 ((cons (o) (cons (o) (shw (half (suc (half (suc (zero)))))))) != (shw (zero))) % 2.86/3.05 ((cons (i) (cons (o) (shw (half (suc (zero)))))) != (shw (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((half (suc zenon_X4)) != (half (suc (zero)))) % 2.86/3.05 (zenon_X3 != (zero)) % 2.86/3.05 ((shw (suc zenon_X4)) != (shw (suc (half (zero))))) % 2.86/3.05 ((half (suc (half (zero)))) != (suc (half (zero)))) % 2.86/3.05 (zenon_X7 != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X3)))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons (o) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((nil) != (cons (i) (shw (suc zenon_X4)))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons (i) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (shw (zero))) % 2.86/3.05 ((cons (o) (cons (o) (shw (half (suc (zero)))))) != (shw (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons (o) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((nil) != (cons (i) zenon_X8)) % 2.86/3.05 ((shw (half (suc zenon_X4))) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (shw (zero))) % 2.86/3.05 (zenon_X7 != (shw (suc zenon_X3))) % 2.86/3.05 ((half (suc zenon_X3)) != (half (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons (o) zenon_X7)) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((nil) != (cons (i) (shw (half (suc (zero)))))) % 2.86/3.05 ((nil) != (cons (i) (cons (i) (shw (half (suc (half (suc (zero))))))))) % 2.86/3.05 ((cons (i) (shw (suc (half (suc (zero)))))) != (shw (zero))) % 2.86/3.05 ((nil) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons (i) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (shw (suc zenon_X3))) % 2.86/3.05 ((suc zenon_X4) != (half (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != zenon_X1) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((zero) != (suc (half (zero)))) % 2.86/3.05 ((cons zenon_X0 (shw (zero))) != (shw (suc zenon_X4))) % 2.86/3.05 (zenon_X3 != (half (zero))) % 2.86/3.05 (zenon_X7 != (shw (suc (half (zero))))) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X3))) != (shw (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons zenon_X0 zenon_X1) != (shw (suc (half (zero))))) % 2.86/3.05 (zenon_X1 != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (shw (half (suc (half (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != zenon_X7) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (shw (half (suc (half (zero)))))) % 2.86/3.05 ((nil) != (cons (o) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((shw (half (suc (half (zero))))) != (shw (suc (half (zero))))) % 2.86/3.05 ((nil) != (cons (i) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (i) (cons (i) (shw (half (suc zenon_X3))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons (i) zenon_X8)) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons (o) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((shw (half (suc zenon_X4))) != (shw (zero))) % 2.86/3.05 ((shw (half (suc zenon_X4))) != zenon_X1) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((append (shw zenon_X6) (shw zenon_X5)) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (shw (half (suc (zero))))) % 2.86/3.05 ((cons zenon_X0 (nil)) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (o) (shw (zero))) != (shw (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc zenon_X3))))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((shw (suc zenon_X3)) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((nil) != (cons (i) (shw (suc zenon_X3)))) % 2.86/3.05 (zenon_X4 != (half (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons (i) zenon_X8)) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != zenon_X7) % 2.86/3.05 ((cons (o) (shw (suc zenon_X3))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != zenon_X7) % 2.86/3.05 ((shw (half (suc (half (zero))))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (nil)) != (shw (zero))) % 2.86/3.05 ((shw (half (suc (half (zero))))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((shw (zero)) != (shw (suc zenon_X3))) % 2.86/3.05 ((half (suc zenon_X3)) != (suc (half (suc (zero))))) % 2.86/3.05 (zenon_X7 != (shw (suc (zero)))) % 2.86/3.05 ((nil) != (cons (i) (shw (suc (half (suc (zero))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != zenon_X8) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons (o) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((shw (suc zenon_X4)) = (cons (o) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((nil) != (cons (i) (shw (half (suc (rd (nil))))))) % 2.86/3.05 ((zero) != (suc zenon_X2)) % 2.86/3.05 ((rd (append (shw zenon_X6) (shw zenon_X5))) != (suc zenon_X2)) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X4)))) != (shw (suc (zero)))) % 2.86/3.05 ((nil) != (cons (i) (cons (o) (shw (half (suc (half (suc (zero))))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((shw (half (suc zenon_X3))) != (shw (suc zenon_X4))) % 2.86/3.05 ((suc (half (suc (zero)))) != (half (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons (i) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (shw (half (suc (zero))))) % 2.86/3.05 ((half (suc (rd (nil)))) != (half (suc zenon_X4))) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X4))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc (zero)))))) != (shw (suc (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (shw (suc zenon_X4))) % 2.86/3.05 ((shw (half (suc (half (zero))))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((half (suc zenon_X3)) != (suc (half (zero)))) % 2.86/3.05 ((shw (half (suc zenon_X4))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (i) (cons (o) (shw (half (suc (zero)))))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc zenon_X4))))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons (o) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc zenon_X4))))) != (shw (suc (zero)))) % 2.86/3.05 ((half (suc zenon_X4)) != (half (suc zenon_X3))) % 2.86/3.05 ((suc (half (zero))) != (half (zero))) % 2.86/3.05 ((cons zenon_X0 zenon_X1) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != zenon_X8) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (shw (zero))) % 2.86/3.05 (zenon_X8 != (shw (suc zenon_X4))) % 2.86/3.05 ((shw (half (suc (rd (nil))))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((nil) != (cons (i) (shw (suc (zero))))) % 2.86/3.05 ((cons (i) (cons (o) (shw (half (suc zenon_X4))))) != (shw (zero))) % 2.86/3.05 ((nil) != (cons (o) (cons (o) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (cons (i) zenon_X8)) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((nil) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (shw (suc zenon_X3))) % 2.86/3.05 ((nil) != (cons (i) (shw (half (suc (half (suc (zero)))))))) % 2.86/3.05 ((half (suc (rd (nil)))) != (half (suc zenon_X3))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (i) (shw (half (suc (half (zero)))))))) % 2.86/3.05 ((suc zenon_X3) != (suc (half (suc (zero))))) % 2.86/3.05 (zenon_X4 != (rd (nil))) % 2.86/3.05 (zenon_X1 != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc zenon_X3))))) != (shw (suc (zero)))) % 2.86/3.05 ((suc (zero)) != (half (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (shw (zero))) % 2.86/3.05 ((nil) != (cons (i) (cons (i) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((half (suc (half (suc (zero))))) != (half (suc zenon_X4))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (shw (half (suc (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons (i) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((append (shw zenon_X5) (shw zenon_X6)) != (shw (suc (half (zero))))) % 2.86/3.05 ((nil) != (shw (suc (half (zero))))) % 2.86/3.05 ((shw (half (suc (zero)))) != (cons (o) (shw (half (suc (zero)))))) % 2.86/3.05 ((i) != (o)) % 2.86/3.05 ((nil) != (cons (o) (shw (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (i) zenon_X8) != (shw (suc (half (zero))))) % 2.86/3.05 ((nil) != (cons (i) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((shw (half (suc (half (suc (zero)))))) != zenon_X8) % 2.86/3.05 ((cons (o) (cons (i) (shw (half (suc zenon_X4))))) != (shw (zero))) % 2.86/3.05 ((shw (half (suc (half (zero))))) != (shw (suc (zero)))) % 2.86/3.05 ((nil) != (cons (o) (shw (suc zenon_X4)))) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X4)))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons (o) zenon_X7)) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (i) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != zenon_X8) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 (zenon_X8 != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((suc (rd (nil))) != (half (suc (zero)))) % 2.86/3.05 ((nil) != (cons (i) (cons (o) (shw (half (suc (half (zero)))))))) % 2.86/3.05 ((nil) != (cons (o) (cons (i) (shw (half (suc (rd (nil)))))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (o) (shw (half (suc (half (zero)))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((shw (half (suc (half (zero))))) != (cons (o) (shw (half (suc (zero)))))) % 2.86/3.05 ((cons zenon_X0 (shw (zero))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != zenon_X7) % 2.86/3.05 ((nil) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (i) (shw (half (suc (half (suc (zero))))))))) % 2.86/3.05 ((shw (half (suc (half (suc (zero)))))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons (o) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != zenon_X8) % 2.86/3.05 ((cons zenon_X0 (shw (half (suc zenon_X4)))) != (shw (suc (half (zero))))) % 2.86/3.05 ((shw (half (suc (half (suc (zero)))))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc (zero))))) % 2.86/3.05 ((shw (half (suc (zero)))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons (o) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((shw (half (suc zenon_X4))) != (shw (half (suc zenon_X3)))) % 2.86/3.05 ((cons zenon_X0 (nil)) != (shw (suc (zero)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((cons (i) (cons (i) (shw (half (suc (rd (nil))))))) != (shw (zero))) % 2.86/3.05 ((cons (i) (cons (o) (shw (half (suc (zero)))))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 (nil)) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((shw (half (suc zenon_X3))) != (shw (zero))) % 2.86/3.05 ((half (suc zenon_X4)) != (suc zenon_X4)) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (o) (shw (half (suc (rd (nil)))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((shw (half (suc (zero)))) != zenon_X8) % 2.86/3.05 ((nil) != (cons zenon_X0 (shw (suc (half (zero)))))) % 2.86/3.05 ((cons zenon_X0 (shw (zero))) != (shw (suc (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (shw (suc zenon_X4)))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (shw (half (suc zenon_X4))))) % 2.86/3.05 ((half (suc (half (zero)))) != (suc (rd (nil)))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons (i) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons (o) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (i) zenon_X8) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((shw (half (suc (half (suc (zero)))))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (shw (half (suc (rd (nil)))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != zenon_X1) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != zenon_X8) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc (half (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((append (shw zenon_X6) (shw zenon_X5)) != (shw (suc zenon_X3))) % 2.86/3.05 ((nil) != (cons (i) (cons (o) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((cons (i) (shw (zero))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 (cons (o) (shw (half (suc zenon_X3))))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((nil) != zenon_X1) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != zenon_X1) % 2.86/3.05 ((cons (i) zenon_X8) != (shw (suc (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((rd (append (shw zenon_X5) (shw zenon_X6))) != (half (suc (zero)))) % 2.86/3.05 ((suc (zero)) != (half (suc (zero)))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((shw (zero)) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (shw (suc zenon_X4))) % 2.86/3.05 ((shw (half (suc (zero)))) != (shw (suc (zero)))) % 2.86/3.05 ((shw (half (suc zenon_X3))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc (rd (nil)))))) % 2.86/3.05 ((shw (suc (half (suc (zero))))) = (cons (o) (shw (half (suc (half (suc (zero)))))))) % 2.86/3.05 (zenon_X8 != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((nil) != (cons (i) (cons (o) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (zero)))))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (i) (cons (i) (shw (half (suc (zero)))))) != (shw (zero))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X4)))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((nil) != (shw (suc (zero)))) % 2.86/3.05 ((shw (half (suc (zero)))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (shw (suc (half (zero))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 (shw (zero)))) % 2.86/3.05 ((shw (half (suc zenon_X4))) != zenon_X8) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((shw (half (suc zenon_X4))) != zenon_X7) % 2.86/3.05 ((cons zenon_X0 (shw (zero))) != (shw (suc (half (zero))))) % 2.86/3.05 ((suc (half (zero))) != (rd (nil))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 (zenon_X4 != (half (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X3))) != (shw (suc (rd (nil))))) % 2.86/3.05 ((half (suc zenon_X3)) != (half (zero))) % 2.86/3.05 ((cons (o) (cons (i) (shw (half (suc (zero)))))) != (shw (zero))) % 2.86/3.05 ((shw (suc (half (zero)))) = (cons (o) (shw (half (suc (half (zero))))))) % 2.86/3.05 ((nil) != (shw (suc (rd (nil))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons zenon_X0 zenon_X1) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (cons (o) (shw (half (suc zenon_X3))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (shw (half (suc (half (suc (zero))))))) % 2.86/3.05 (zenon_X1 != (shw (suc zenon_X4))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons (o) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 (shw (zero))) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != zenon_X7) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((nil) != (cons (o) (shw (suc (half (zero)))))) % 2.86/3.05 ((nil) != (cons zenon_X0 (cons (o) (shw (half (suc (half (suc (zero))))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (nil))) % 2.86/3.05 ((cons (o) (shw (suc (half (suc (zero)))))) != (shw (zero))) % 2.86/3.05 ((rd (nil)) != (rd (append (shw zenon_X5) (shw zenon_X6)))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (shw (half (suc zenon_X4)))) % 2.86/3.05 ((cons (i) (cons (o) (shw (half (suc (zero)))))) != (shw (suc (rd (nil))))) % 2.86/3.05 (zenon_X8 != (shw (suc zenon_X3))) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X4))) != (shw (suc (zero)))) % 2.86/3.05 ((suc zenon_X4) != (zero)) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc zenon_X4))))) != (shw (zero))) % 2.86/3.05 ((cons zenon_X0 zenon_X1) != (shw (suc (half (suc (zero)))))) % 2.86/3.05 ((suc zenon_X3) != (zero)) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons (i) (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (nil)) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (i) (shw (half (suc (zero))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((suc zenon_X3) != (suc (rd (nil)))) % 2.86/3.05 ((nil) != (append (shw zenon_X5) (shw zenon_X6))) % 2.86/3.05 ((cons (i) (shw (half (suc (half (suc (zero))))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X3)))))) % 2.86/3.05 ((zero) != (rd (append (shw zenon_X5) (shw zenon_X6)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X4)))) != (cons zenon_X0 (shw (suc zenon_X3)))) % 2.86/3.05 ((cons (o) (shw (half (suc zenon_X3)))) != (shw (suc zenon_X4))) % 2.86/3.05 ((shw (half (suc (rd (nil))))) != (cons (o) (shw (half (suc (zero)))))) % 2.86/3.05 ((cons zenon_X0 (cons (i) (shw (half (suc (half (zero))))))) != (shw (zero))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (zero)))))) != (cons zenon_X0 zenon_X1)) % 2.86/3.05 ((suc zenon_X4) != (suc (rd (nil)))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (nil)) % 2.86/3.05 ((cons (i) (shw (half (suc zenon_X3)))) != (append (shw zenon_X6) (shw zenon_X5))) % 2.86/3.05 ((shw (half (suc (rd (nil))))) != (shw (suc (zero)))) % 2.86/3.05 ((cons zenon_X0 (shw (suc zenon_X3))) != (shw (suc zenon_X4))) % 2.86/3.05 ((shw (half (suc (half (zero))))) != zenon_X7) % 2.86/3.05 ((half (suc zenon_X4)) != (suc (rd (nil)))) % 2.86/3.05 ((cons (o) (shw (half (suc (zero))))) != (cons zenon_X0 (cons (o) (shw (half (suc (zero))))))) % 2.86/3.05 ((cons (o) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (cons (i) (shw (half (suc zenon_X4)))))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (shw (suc zenon_X3))) % 2.86/3.05 ((cons (o) (shw (half (suc (half (suc (zero))))))) != (cons (o) (shw (half (suc zenon_X4))))) % 2.86/3.05 ((cons (i) (shw (half (suc (rd (nil)))))) != (cons zenon_X0 (cons (o) (shw (half (suc zenon_X4)))))) % 2.86/3.05 *) % 2.86/3.05 (* NO-PROOF *) % 2.86/3.05 % SZS status GaveUp % 2.86/3.05 Number of rewrites on terms: 2 % 2.86/3.05 Number of rewrites on props: 8 % 2.86/3.05 nodes searched: 68523 % 2.86/3.05 max branch formulas: 863 % 2.86/3.05 proof nodes created: 585 % 2.86/3.05 formulas created: 70775 % 2.86/3.05 %------------------------------------------------------------------------------