%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% This Otter input file is for translating some problems
% so that Larry Wos can work on them with Otter.  The problems
% are about associativity properties in the system LR (also R?).
%
% If you run this file through Otter, the sos list at
% the end of the output file will contain 16 axioms, 2
% rules (CD and a rule for conjunction), and 16 big denials.
% of the associativity properties, all in terms of the primitives
% and in prefix.
%
% This has Bob Meyer's TSMALL/TBIG correction.

op(800, infix, [->, &, v, o, +, <->]).
op(700, prefix_assoc, ~).

set(demod_inf).
clear(demod_history).
set(sos_queue).
clear(for_sub).
clear(back_sub).
assign(max_given, 34).
set(print_lists_at_end).

list(sos).   % This list contains axioms and rules for LR

% Implication Axioms

P(x -> x).                                    % A1 Identity
P((x -> y) -> ((z -> x) -> (z -> y))).        % A2 Prefixing
P((x -> y) -> ((y -> z) -> (x -> z))).        % A3 Suffixing
P((x -> (x -> y)) -> (x -> y)).               % A4 Contraction
P((x -> (y -> z)) -> (y -> (x -> z))).        % A5 Contraction

% Implication/Negation Axioms

P(~ ~x -> x).                                 % A6 Double Negation
P((x -> ~x) -> ~x).                           % A7 Reductio
P((x -> ~y) -> (y -> ~x)).                    % A8 Contraposition

% Conjuction/Disjunction Axioms

P((x & y) -> x).                              % A9 Simplification
P((x & y) -> y).                              % A10 Simplification
P(((x -> y) & (x -> z)) -> (x -> (y & z))).   % A11 & Introduction
P(x -> (x v y)).                              % A12 Addition
P(y -> (x v y)).                              % A13 Addition
P(((x -> z) & (y -> z)) -> ((x v y) -> z)).   % A14 v Introduction

% Axioms for Constants

P(((TSMALL -> x) -> x) & (x -> (TSMALL -> x))). % A15
P(x -> TBIG).                                   % A16

% Rules

-P(x -> y) | -P(x) | P(y).                    % CD
-P(x) | -P(y) | P(x & y).                     % Adjunction

end_of_list.

list(demodulators).   % This list is used to rewrite clauses in list(sos).

% The 16 operations in question.

c1(x,y) = (x o ((x + x) o (y v ~y))).               % C1
c2(x,y) = (x o (y v (~y v (~x o ~x)))).             % C2
c3(x,y) = (x + (x o (~x o (y v ~y)))).              % C3
c4(x,y) = (x v (x o (~x o (y v ~y)))).              % C4
c5(x,y) = (x o ((x v ~x) o (y v ~y))).              % C5
c6(x,y) = (x o (x v (~y v (~x o y)))).              % C6
c7(x,y) = (x o (y v (~y v (~x o y)))).              % C7
c8(x,y) = ((x + x) o (~y v (x o y))).               % C8
c9(x,y) = (x o (x + (~x o (y v ~y)))).              % C9
c10(x,y) = (x o (x v (~x o (y v ~y)))).             % C10
c11(x,y) = (x v (x o (~y v (~x o y)))).             % C11
c12(x,y) = (x o (~y v (x + (~x o y)))).             % C12
c13(x,y) = (x o (~y v (y o (x v ~x)))).             % C13
c14(x,y) = (x o (~y v (y + (~x o y)))).             % C14
c15(x,y) = (x o (~y v (y o (~x v y)))).             % C15
c16(x,y) = ((x v (x o ~x)) o (y v ~y)).             % C16

% Definitions of fusion and fission.

(x o y) = ~(x -> ~y).
(x + y) = (~x -> y).
(x <-> y) = ((x -> y) & (y -> x)).

% Rewrite the operations into prefix.

(x -> y) = i(x,y).
(~x) = n(x).
(x & y) = and(x,y).
(x v y) = or(x,y).

end_of_list.

list(sos).

% Here are the denials of the associativity properties for C1 -- C16.
% I guess the challenge is to prove these in LR.

-P(c1(c1(a,b),c) <-> c1(a,c1(b,c))) | $Ans(C1).
-P(c2(c2(a,b),c) <-> c2(a,c2(b,c))) | $Ans(C2).
-P(c3(c3(a,b),c) <-> c3(a,c3(b,c))) | $Ans(C3).
-P(c4(c4(a,b),c) <-> c4(a,c4(b,c))) | $Ans(C4).
-P(c5(c5(a,b),c) <-> c5(a,c5(b,c))) | $Ans(C5).
-P(c6(c6(a,b),c) <-> c6(a,c6(b,c))) | $Ans(C6).
-P(c7(c7(a,b),c) <-> c7(a,c7(b,c))) | $Ans(C7).
-P(c8(c8(a,b),c) <-> c8(a,c8(b,c))) | $Ans(C8).
-P(c9(c9(a,b),c) <-> c9(a,c9(b,c))) | $Ans(C9).
-P(c10(c10(a,b),c) <-> c10(a,c10(b,c))) | $Ans(C10).
-P(c11(c11(a,b),c) <-> c11(a,c11(b,c))) | $Ans(C11).
-P(c12(c12(a,b),c) <-> c12(a,c12(b,c))) | $Ans(C12).
-P(c13(c13(a,b),c) <-> c13(a,c13(b,c))) | $Ans(C13).
-P(c14(c14(a,b),c) <-> c14(a,c14(b,c))) | $Ans(C14).
-P(c15(c15(a,b),c) <-> c15(a,c15(b,c))) | $Ans(C15).
-P(c16(c16(a,b),c) <-> c16(a,c16(b,c))) | $Ans(C16).

end_of_list.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here is a second input file, constructed from the output of the
% preceding input file.
%
% This might be the set of problems that Bob Meyer was thinking of
% for Larry Wos to try.

set(hyper_res).
set(order_history).
clear(print_kept).
clear(back_sub).
assign(pick_given_ratio, 4).

list(usable).
-P(i(x,y)) | -P(x) | P(y).              % Condensed Detachment
-P(x) | -P(y) | P(and(x,y)).            % Adjunction
end_of_list.

list(sos).
P(i(x,x)).                              % A1 Identity
P(i(i(x,y),i(i(z,x),i(z,y)))).          % A2 Prefixing
P(i(i(x,y),i(i(y,z),i(x,z)))).          % A3 Suffixing
P(i(i(x,i(x,y)),i(x,y))).               % A4 Contraction
P(i(i(x,i(y,z)),i(y,i(x,z)))).          % A5 Contraction
P(i(n(n(x)),x)).                        % A6 Double Negation
P(i(i(x,n(x)),n(x))).                   % A7 Reductio
P(i(i(x,n(y)),i(y,n(x)))).              % A8 Contraposition
P(i(and(x,y),x)).                       % A9 Simplification
P(i(and(x,y),y)).                       % A10 Simplification
P(i(and(i(x,y),i(x,z)),i(x,and(y,z)))). % A11 & Introduction
P(i(x,or(x,y))).                        % A12 Addition
P(i(x,or(y,x))).                        % A13 Addition
P(i(and(i(x,y),i(z,y)),i(or(x,z),y))).  % A14 v Introduction
P(and(i(i(TSMALL,x),x),i(x,i(TSMALL,x)))).  % A15
P(i(x,TBIG)).                               % A16
end_of_list.

list(passive).
-P(and(i(n(i(n(i(a,n(n(i(i(n(a),a),n(or(b,n(b)))))))),n(n(i(i(n(n(i(a,n(n(i(i(n(a),a),n(or(b,n(b))))))))),n(i(a,n(n(i(i(n(a),a),n(or(b,n(b))))))))),n(or(c,n(c)))))))),n(i(a,n(n(i(i(n(a),a),n(or(n(i(b,n(n(i(i(n(b),b),n(or(c,n(c)))))))),n(n(i(b,n(n(i(i(n(b),b),n(or(c,n(c))))))))))))))))),i(n(i(a,n(n(i(i(n(a),a),n(or(n(i(b,n(n(i(i(n(b),b),n(or(c,n(c)))))))),n(n(i(b,n(n(i(i(n(b),b),n(or(c,n(c)))))))))))))))),n(i(n(i(a,n(n(i(i(n(a),a),n(or(b,n(b)))))))),n(n(i(i(n(n(i(a,n(n(i(i(n(a),a),n(or(b,n(b))))))))),n(i(a,n(n(i(i(n(a),a),n(or(b,n(b))))))))),n(or(c,n(c))))))))))) | $Ans(C1).
-P(and(i(n(i(n(i(a,n(or(b,or(n(b),n(i(n(a),n(n(a))))))))),n(or(c,or(n(c),n(i(n(n(i(a,n(or(b,or(n(b),n(i(n(a),n(n(a)))))))))),n(n(n(i(a,n(or(b,or(n(b),n(i(n(a),n(n(a)))))))))))))))))),n(i(a,n(or(n(i(b,n(or(c,or(n(c),n(i(n(b),n(n(b))))))))),or(n(n(i(b,n(or(c,or(n(c),n(i(n(b),n(n(b)))))))))),n(i(n(a),n(n(a)))))))))),i(n(i(a,n(or(n(i(b,n(or(c,or(n(c),n(i(n(b),n(n(b))))))))),or(n(n(i(b,n(or(c,or(n(c),n(i(n(b),n(n(b)))))))))),n(i(n(a),n(n(a))))))))),n(i(n(i(a,n(or(b,or(n(b),n(i(n(a),n(n(a))))))))),n(or(c,or(n(c),n(i(n(n(i(a,n(or(b,or(n(b),n(i(n(a),n(n(a)))))))))),n(n(n(i(a,n(or(b,or(n(b),n(i(n(a),n(n(a))))))))))))))))))))) | $Ans(C2).
-P(and(i(i(n(i(n(a),n(i(a,n(n(i(n(a),n(or(b,n(b)))))))))),n(i(i(n(a),n(i(a,n(n(i(n(a),n(or(b,n(b))))))))),n(n(i(n(i(n(a),n(i(a,n(n(i(n(a),n(or(b,n(b)))))))))),n(or(c,n(c))))))))),i(n(a),n(i(a,n(n(i(n(a),n(or(i(n(b),n(i(b,n(n(i(n(b),n(or(c,n(c))))))))),n(i(n(b),n(i(b,n(n(i(n(b),n(or(c,n(c))))))))))))))))))),i(i(n(a),n(i(a,n(n(i(n(a),n(or(i(n(b),n(i(b,n(n(i(n(b),n(or(c,n(c))))))))),n(i(n(b),n(i(b,n(n(i(n(b),n(or(c,n(c)))))))))))))))))),i(n(i(n(a),n(i(a,n(n(i(n(a),n(or(b,n(b)))))))))),n(i(i(n(a),n(i(a,n(n(i(n(a),n(or(b,n(b))))))))),n(n(i(n(i(n(a),n(i(a,n(n(i(n(a),n(or(b,n(b)))))))))),n(or(c,n(c)))))))))))) | $Ans(C3).
-P(and(i(or(or(a,n(i(a,n(n(i(n(a),n(or(b,n(b))))))))),n(i(or(a,n(i(a,n(n(i(n(a),n(or(b,n(b))))))))),n(n(i(n(or(a,n(i(a,n(n(i(n(a),n(or(b,n(b)))))))))),n(or(c,n(c))))))))),or(a,n(i(a,n(n(i(n(a),n(or(or(b,n(i(b,n(n(i(n(b),n(or(c,n(c))))))))),n(or(b,n(i(b,n(n(i(n(b),n(or(c,n(c))))))))))))))))))),i(or(a,n(i(a,n(n(i(n(a),n(or(or(b,n(i(b,n(n(i(n(b),n(or(c,n(c))))))))),n(or(b,n(i(b,n(n(i(n(b),n(or(c,n(c)))))))))))))))))),or(or(a,n(i(a,n(n(i(n(a),n(or(b,n(b))))))))),n(i(or(a,n(i(a,n(n(i(n(a),n(or(b,n(b))))))))),n(n(i(n(or(a,n(i(a,n(n(i(n(a),n(or(b,n(b)))))))))),n(or(c,n(c)))))))))))) | $Ans(C4).
-P(and(i(n(i(n(i(a,n(n(i(or(a,n(a)),n(or(b,n(b)))))))),n(n(i(or(n(i(a,n(n(i(or(a,n(a)),n(or(b,n(b)))))))),n(n(i(a,n(n(i(or(a,n(a)),n(or(b,n(b)))))))))),n(or(c,n(c)))))))),n(i(a,n(n(i(or(a,n(a)),n(or(n(i(b,n(n(i(or(b,n(b)),n(or(c,n(c)))))))),n(n(i(b,n(n(i(or(b,n(b)),n(or(c,n(c))))))))))))))))),i(n(i(a,n(n(i(or(a,n(a)),n(or(n(i(b,n(n(i(or(b,n(b)),n(or(c,n(c)))))))),n(n(i(b,n(n(i(or(b,n(b)),n(or(c,n(c)))))))))))))))),n(i(n(i(a,n(n(i(or(a,n(a)),n(or(b,n(b)))))))),n(n(i(or(n(i(a,n(n(i(or(a,n(a)),n(or(b,n(b)))))))),n(n(i(a,n(n(i(or(a,n(a)),n(or(b,n(b)))))))))),n(or(c,n(c))))))))))) | $Ans(C5).
-P(and(i(n(i(n(i(a,n(or(a,or(n(b),n(i(n(a),n(b)))))))),n(or(n(i(a,n(or(a,or(n(b),n(i(n(a),n(b)))))))),or(n(c),n(i(n(n(i(a,n(or(a,or(n(b),n(i(n(a),n(b))))))))),n(c)))))))),n(i(a,n(or(a,or(n(n(i(b,n(or(b,or(n(c),n(i(n(b),n(c))))))))),n(i(n(a),n(n(i(b,n(or(b,or(n(c),n(i(n(b),n(c))))))))))))))))),i(n(i(a,n(or(a,or(n(n(i(b,n(or(b,or(n(c),n(i(n(b),n(c))))))))),n(i(n(a),n(n(i(b,n(or(b,or(n(c),n(i(n(b),n(c)))))))))))))))),n(i(n(i(a,n(or(a,or(n(b),n(i(n(a),n(b)))))))),n(or(n(i(a,n(or(a,or(n(b),n(i(n(a),n(b)))))))),or(n(c),n(i(n(n(i(a,n(or(a,or(n(b),n(i(n(a),n(b))))))))),n(c))))))))))) | $Ans(C6).
-P(and(i(n(i(n(i(a,n(or(b,or(n(b),n(i(n(a),n(b)))))))),n(or(c,or(n(c),n(i(n(n(i(a,n(or(b,or(n(b),n(i(n(a),n(b))))))))),n(c)))))))),n(i(a,n(or(n(i(b,n(or(c,or(n(c),n(i(n(b),n(c)))))))),or(n(n(i(b,n(or(c,or(n(c),n(i(n(b),n(c))))))))),n(i(n(a),n(n(i(b,n(or(c,or(n(c),n(i(n(b),n(c))))))))))))))))),i(n(i(a,n(or(n(i(b,n(or(c,or(n(c),n(i(n(b),n(c)))))))),or(n(n(i(b,n(or(c,or(n(c),n(i(n(b),n(c))))))))),n(i(n(a),n(n(i(b,n(or(c,or(n(c),n(i(n(b),n(c)))))))))))))))),n(i(n(i(a,n(or(b,or(n(b),n(i(n(a),n(b)))))))),n(or(c,or(n(c),n(i(n(n(i(a,n(or(b,or(n(b),n(i(n(a),n(b))))))))),n(c))))))))))) | $Ans(C7).
-P(and(i(n(i(i(n(n(i(i(n(a),a),n(or(n(b),n(i(a,n(b)))))))),n(i(i(n(a),a),n(or(n(b),n(i(a,n(b)))))))),n(or(n(c),n(i(n(i(i(n(a),a),n(or(n(b),n(i(a,n(b))))))),n(c))))))),n(i(i(n(a),a),n(or(n(n(i(i(n(b),b),n(or(n(c),n(i(b,n(c)))))))),n(i(a,n(n(i(i(n(b),b),n(or(n(c),n(i(b,n(c))))))))))))))),i(n(i(i(n(a),a),n(or(n(n(i(i(n(b),b),n(or(n(c),n(i(b,n(c)))))))),n(i(a,n(n(i(i(n(b),b),n(or(n(c),n(i(b,n(c)))))))))))))),n(i(i(n(n(i(i(n(a),a),n(or(n(b),n(i(a,n(b)))))))),n(i(i(n(a),a),n(or(n(b),n(i(a,n(b)))))))),n(or(n(c),n(i(n(i(i(n(a),a),n(or(n(b),n(i(a,n(b))))))),n(c)))))))))) | $Ans(C8).
-P(and(i(n(i(n(i(a,n(i(n(a),n(i(n(a),n(or(b,n(b))))))))),n(i(n(n(i(a,n(i(n(a),n(i(n(a),n(or(b,n(b)))))))))),n(i(n(n(i(a,n(i(n(a),n(i(n(a),n(or(b,n(b)))))))))),n(or(c,n(c))))))))),n(i(a,n(i(n(a),n(i(n(a),n(or(n(i(b,n(i(n(b),n(i(n(b),n(or(c,n(c))))))))),n(n(i(b,n(i(n(b),n(i(n(b),n(or(c,n(c))))))))))))))))))),i(n(i(a,n(i(n(a),n(i(n(a),n(or(n(i(b,n(i(n(b),n(i(n(b),n(or(c,n(c))))))))),n(n(i(b,n(i(n(b),n(i(n(b),n(or(c,n(c)))))))))))))))))),n(i(n(i(a,n(i(n(a),n(i(n(a),n(or(b,n(b))))))))),n(i(n(n(i(a,n(i(n(a),n(i(n(a),n(or(b,n(b)))))))))),n(i(n(n(i(a,n(i(n(a),n(i(n(a),n(or(b,n(b)))))))))),n(or(c,n(c)))))))))))) | $Ans(C9).
-P(and(i(n(i(n(i(a,n(or(a,n(i(n(a),n(or(b,n(b))))))))),n(or(n(i(a,n(or(a,n(i(n(a),n(or(b,n(b))))))))),n(i(n(n(i(a,n(or(a,n(i(n(a),n(or(b,n(b)))))))))),n(or(c,n(c))))))))),n(i(a,n(or(a,n(i(n(a),n(or(n(i(b,n(or(b,n(i(n(b),n(or(c,n(c))))))))),n(n(i(b,n(or(b,n(i(n(b),n(or(c,n(c))))))))))))))))))),i(n(i(a,n(or(a,n(i(n(a),n(or(n(i(b,n(or(b,n(i(n(b),n(or(c,n(c))))))))),n(n(i(b,n(or(b,n(i(n(b),n(or(c,n(c)))))))))))))))))),n(i(n(i(a,n(or(a,n(i(n(a),n(or(b,n(b))))))))),n(or(n(i(a,n(or(a,n(i(n(a),n(or(b,n(b))))))))),n(i(n(n(i(a,n(or(a,n(i(n(a),n(or(b,n(b)))))))))),n(or(c,n(c)))))))))))) | $Ans(C10).
-P(and(i(or(or(a,n(i(a,n(or(n(b),n(i(n(a),n(b)))))))),n(i(or(a,n(i(a,n(or(n(b),n(i(n(a),n(b)))))))),n(or(n(c),n(i(n(or(a,n(i(a,n(or(n(b),n(i(n(a),n(b))))))))),n(c)))))))),or(a,n(i(a,n(or(n(or(b,n(i(b,n(or(n(c),n(i(n(b),n(c))))))))),n(i(n(a),n(or(b,n(i(b,n(or(n(c),n(i(n(b),n(c))))))))))))))))),i(or(a,n(i(a,n(or(n(or(b,n(i(b,n(or(n(c),n(i(n(b),n(c))))))))),n(i(n(a),n(or(b,n(i(b,n(or(n(c),n(i(n(b),n(c)))))))))))))))),or(or(a,n(i(a,n(or(n(b),n(i(n(a),n(b)))))))),n(i(or(a,n(i(a,n(or(n(b),n(i(n(a),n(b)))))))),n(or(n(c),n(i(n(or(a,n(i(a,n(or(n(b),n(i(n(a),n(b))))))))),n(c))))))))))) | $Ans(C11).
-P(and(i(n(i(n(i(a,n(or(n(b),i(n(a),n(i(n(a),n(b)))))))),n(or(n(c),i(n(n(i(a,n(or(n(b),i(n(a),n(i(n(a),n(b))))))))),n(i(n(n(i(a,n(or(n(b),i(n(a),n(i(n(a),n(b))))))))),n(c)))))))),n(i(a,n(or(n(n(i(b,n(or(n(c),i(n(b),n(i(n(b),n(c))))))))),i(n(a),n(i(n(a),n(n(i(b,n(or(n(c),i(n(b),n(i(n(b),n(c))))))))))))))))),i(n(i(a,n(or(n(n(i(b,n(or(n(c),i(n(b),n(i(n(b),n(c))))))))),i(n(a),n(i(n(a),n(n(i(b,n(or(n(c),i(n(b),n(i(n(b),n(c)))))))))))))))),n(i(n(i(a,n(or(n(b),i(n(a),n(i(n(a),n(b)))))))),n(or(n(c),i(n(n(i(a,n(or(n(b),i(n(a),n(i(n(a),n(b))))))))),n(i(n(n(i(a,n(or(n(b),i(n(a),n(i(n(a),n(b))))))))),n(c))))))))))) | $Ans(C12).
-P(and(i(n(i(n(i(a,n(or(n(b),n(i(b,n(or(a,n(a))))))))),n(or(n(c),n(i(c,n(or(n(i(a,n(or(n(b),n(i(b,n(or(a,n(a))))))))),n(n(i(a,n(or(n(b),n(i(b,n(or(a,n(a)))))))))))))))))),n(i(a,n(or(n(n(i(b,n(or(n(c),n(i(c,n(or(b,n(b)))))))))),n(i(n(i(b,n(or(n(c),n(i(c,n(or(b,n(b))))))))),n(or(a,n(a)))))))))),i(n(i(a,n(or(n(n(i(b,n(or(n(c),n(i(c,n(or(b,n(b)))))))))),n(i(n(i(b,n(or(n(c),n(i(c,n(or(b,n(b))))))))),n(or(a,n(a))))))))),n(i(n(i(a,n(or(n(b),n(i(b,n(or(a,n(a))))))))),n(or(n(c),n(i(c,n(or(n(i(a,n(or(n(b),n(i(b,n(or(a,n(a))))))))),n(n(i(a,n(or(n(b),n(i(b,n(or(a,n(a))))))))))))))))))))) | $Ans(C13).
-P(and(i(n(i(n(i(a,n(or(n(b),i(n(b),n(i(n(a),n(b)))))))),n(or(n(c),i(n(c),n(i(n(n(i(a,n(or(n(b),i(n(b),n(i(n(a),n(b))))))))),n(c)))))))),n(i(a,n(or(n(n(i(b,n(or(n(c),i(n(c),n(i(n(b),n(c))))))))),i(n(n(i(b,n(or(n(c),i(n(c),n(i(n(b),n(c))))))))),n(i(n(a),n(n(i(b,n(or(n(c),i(n(c),n(i(n(b),n(c))))))))))))))))),i(n(i(a,n(or(n(n(i(b,n(or(n(c),i(n(c),n(i(n(b),n(c))))))))),i(n(n(i(b,n(or(n(c),i(n(c),n(i(n(b),n(c))))))))),n(i(n(a),n(n(i(b,n(or(n(c),i(n(c),n(i(n(b),n(c)))))))))))))))),n(i(n(i(a,n(or(n(b),i(n(b),n(i(n(a),n(b)))))))),n(or(n(c),i(n(c),n(i(n(n(i(a,n(or(n(b),i(n(b),n(i(n(a),n(b))))))))),n(c))))))))))) | $Ans(C14).
-P(and(i(n(i(n(i(a,n(or(n(b),n(i(b,n(or(n(a),b)))))))),n(or(n(c),n(i(c,n(or(n(n(i(a,n(or(n(b),n(i(b,n(or(n(a),b))))))))),c)))))))),n(i(a,n(or(n(n(i(b,n(or(n(c),n(i(c,n(or(n(b),c))))))))),n(i(n(i(b,n(or(n(c),n(i(c,n(or(n(b),c)))))))),n(or(n(a),n(i(b,n(or(n(c),n(i(c,n(or(n(b),c))))))))))))))))),i(n(i(a,n(or(n(n(i(b,n(or(n(c),n(i(c,n(or(n(b),c))))))))),n(i(n(i(b,n(or(n(c),n(i(c,n(or(n(b),c)))))))),n(or(n(a),n(i(b,n(or(n(c),n(i(c,n(or(n(b),c)))))))))))))))),n(i(n(i(a,n(or(n(b),n(i(b,n(or(n(a),b)))))))),n(or(n(c),n(i(c,n(or(n(n(i(a,n(or(n(b),n(i(b,n(or(n(a),b))))))))),c))))))))))) | $Ans(C15).
-P(and(i(n(i(or(n(i(or(a,n(i(a,n(n(a))))),n(or(b,n(b))))),n(i(n(i(or(a,n(i(a,n(n(a))))),n(or(b,n(b))))),n(n(n(i(or(a,n(i(a,n(n(a))))),n(or(b,n(b)))))))))),n(or(c,n(c))))),n(i(or(a,n(i(a,n(n(a))))),n(or(n(i(or(b,n(i(b,n(n(b))))),n(or(c,n(c))))),n(n(i(or(b,n(i(b,n(n(b))))),n(or(c,n(c))))))))))),i(n(i(or(a,n(i(a,n(n(a))))),n(or(n(i(or(b,n(i(b,n(n(b))))),n(or(c,n(c))))),n(n(i(or(b,n(i(b,n(n(b))))),n(or(c,n(c)))))))))),n(i(or(n(i(or(a,n(i(a,n(n(a))))),n(or(b,n(b))))),n(i(n(i(or(a,n(i(a,n(n(a))))),n(or(b,n(b))))),n(n(n(i(or(a,n(i(a,n(n(a))))),n(or(b,n(b)))))))))),n(or(c,n(c)))))))) | $Ans(C16).
end_of_list.