lex([1,A,B,C,D,\,/,*,i]). assign(order,kbo). set(lex_order_vars). clear(auto_denials). assign(sos_limit,75000). assign(max_megs,950). clear(print_given). formulas(sos). % loop axioms 1 * x = x. x * 1 = x. x * (x \ y) = y. x \ (x * y) = y. (x * y) / y = x. (x / y) * y = x. % axioms for a conjugacy closed loop ((x * y) / x) * (x * z) = x * (y * z) # label(LCC). (z * x) * (x \ (y * x)) = (z * y) * x # label(RCC). end_of_list. formulas(sos). A * (B * ((D * C) \ (C * D))) != (A * B) * ((D * C) \ (C * D)) # label("orig"). end_of_list. formulas(extra_assumptions). % theorem instances by renaming % A * (B * ((C * C) \ (C * C))) != (A * B) * ((C * C) \ (C * C)) # label("DC"). x * (y * ((z * z) \ (z * z))) = (x * y) * ((z * z) \ (z * z)) # label("DC"). % A * (C * ((D * C) \ (C * D))) != (A * C) * ((D * C) \ (C * D)) # label("BC"). x * (z * ((w * z) \ (z * w))) = (x * z) * ((w * z) \ (z * w)) # label("BC"). % A * (B * ((B * C) \ (C * B))) != (A * B) * ((B * C) \ (C * B)) # label("DB"). x * (y * ((y * z) \ (z * y))) = (x * y) * ((y * z) \ (z * y)) # label("DB"). % D * (B * ((D * C) \ (C * D))) != (D * B) * ((D * C) \ (C * D)) # label("AD"). w * (y * ((w * z) \ (z * w))) = (w * y) * ((w * z) \ (z * w)) # label("AD"). % A * (B * ((D * A) \ (A * D))) != (A * B) * ((D * A) \ (A * D)) # label("CA"). x * (y * ((w * x) \ (x * w))) = (x * y) * ((w * x) \ (x * w)) # label("CA"). % A * (A * ((D * C) \ (C * D))) != (A * A) * ((D * C) \ (C * D)) # label("BA"). x * (x * ((w * z) \ (z * w))) = (x * x) * ((w * z) \ (z * w)) # label("BA"). % extra definition (with basic properties) i(x) = x \ 1. i(x) = 1 / x. x * i(x) = 1. i(x) * x = 1. % WIP y * i(x * y) = i(x). i(y * x) * y = i(x). % WIP with i() expanded by i(x) = x \ 1 y * ((x * y) \ 1) = x \ 1. (1 / (y * x)) * y = 1 / x. end_of_list. formulas(hints). x * (y * ((w * z) \ (z * w))) = (x * y) * ((w * z) \ (z * w)) # label("orig"). end_of_list.