op(400, infix, ^). op(400, infix, v). lex([C, B, A, x v x, c(x), x ^ x, f(x,x)]). % rewrite to join/complement set(anl_eq). assign(pick_given_ratio, 4). assign(max_weight, 40). set(discard_commutativity_consequences). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). clear(sigint_interact). clear(detailed_history). list(usable). x = x. end_of_list. list(sos). f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z))) = x. % OML_Sh x v y = f(f(x,x),f(y,y)). % DEF_J x ^ y = f(f(x,y),f(x,y)). % DEF_M c(x) = f(x,x). % DEF_C end_of_list. assign(max_proofs, 5). list(passive). % A v (A ^ B) != A | $Ans(B1). % A v (c(A) ^ (A v B)) != A v B | $Ans(OM). A v (B v C) != B v (A v C) | $Ans(AJ). A v c(c(A) v B) != A | $Ans(B1_rewritten). A ^ B != c(c(A) v c(B)) | $Ans(DM). A v c(A v c(A v B)) != A v B | $Ans(OM_rewritten). f(A,B) != c(A) v c(B) | $Ans(DEF_SS). end_of_list.