----- Prover9 July-2005D, 18 July 2005 -----
Process 14885 was started by mccune on theorem.mcs.anl.gov,
Fri Jul 22 15:32:06 2005
The command was "prover9 -f dist-long-short.in".

% Reading from file dist-long-short.in

set(auto).
    % set(auto) -> set(auto1).
    % set(auto1) -> set(auto_inference).
    % set(auto1) -> set(fof_reduction).
    % set(auto1) -> set(predicate_elimination).
    % set(auto1) -> set(unfold_eq).
    % set(unfold_eq) -> assign(unfold_eq_limit, 2147483647).
    % set(unfold_eq) -> clear(fold_eq).
    % set(auto1) -> set(inverse_order).
    % set(auto1) -> assign(new_constants, 1).
    % assign(new_constants, 1) -> clear(x_proofs).
    % assign(new_constants, 1) -> clear(rx_proofs).
    % set(auto1) -> assign(lex_dep_demod_lim, 11).
    % set(auto1) -> set(lex_dep_demod_sane).
    % set(auto1) -> assign(max_weight, 100).
    % set(auto1) -> assign(age_part, 1).
    % set(auto1) -> assign(weight_part, 2).
    % set(auto1) -> assign(weight_neg_part, 2).
    % set(auto1) -> assign(sos_limit, 10000).
    % set(auto1) -> clear(x_proofs).
    % set(auto1) -> assign(stats, lots).
    % set(auto1) -> assign(max_megs, 200).
    % set(auto1) -> clear(clocks).
assign(order,kbo).
set(lex_order_vars).

clauses(sos).
f(x,x,y) = x # label(majority).
f(x,y,z) = f(z,x,y) # label(2a).
f(x,y,z) = f(x,z,y) # label(2b).
f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity).
f(f(x,y,z),u,v) = f(f(x,u,v),f(y,u,v),f(z,u,v)) # label(dist_long).
f(f(A,B,C),D,E) != f(A,f(B,D,E),f(C,D,E)) # answer(dist_short).
end_of_list.

% Finished reading the input.

% Entering prover search function.
% Assigned IDs to 6 clauses.

% Predicate elimination: (none).
% Function symbol KB weights:  A=1. B=1. C=1. D=1. E=1. f=1.
% Relation symbol precedence:  lex([ = ]).
% Function symbol precedence:  lex([ A, B, C, D, E, f ]).
% Skipping inverse_order, because term ordering is KBO.
% Unfolding symbols: (none).

% Auto inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).

% Reasonable options, based on the structure of the clauses:
  % (nothing changed)

% Clauses after input processing:

clauses(usable).
end_of_list.

clauses(sos).
7 f(x,x,y) = x # label(majority).  [input]
8 f(x,y,z) = f(z,x,y) # label(2a).  [input]
9 f(x,y,z) = f(x,z,y) # label(2b).  [input]
10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity).  [copy 4 demod (8 8 8 (R) 9)]
11 f(f(x,y,z),f(u,y,z),f(v,y,z)) = f(y,z,f(x,u,v)) # label(dist_long).  [copy 5 demod (8 8) flip a]
12 f(A,f(B,D,E),f(C,D,E)) != f(D,E,f(A,B,C)) # answer(dist_short).  [copy 6 demod (8 8) flip a]
end_of_list.

clauses(demodulators).
7 f(x,x,y) = x # label(majority).  [input]
8 f(x,y,z) = f(z,x,y) # label(2a).  [input]
        % (lex-dep)
9 f(x,y,z) = f(x,z,y) # label(2b).  [input]
        % (lex-dep)
11 f(f(x,y,z),f(u,y,z),f(v,y,z)) = f(y,z,f(x,u,v)) # label(dist_long).  [copy 5 demod (8 8) flip a]
end_of_list.

clauses(goals).
end_of_list.

% Starting search at 0.00 seconds.

given #1 (wt=6): 7 f(x,x,y) = x # label(majority).  [input]

given #2 (wt=9): 8 f(x,y,z) = f(z,x,y) # label(2a).  [input]

given #3 (wt=9): 9 f(x,y,z) = f(x,z,y) # label(2b).  [input]

given #4 (wt=15): 10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity).  [copy 4 demod (8 8 8 (R) 9)]

given #5 (wt=21): 11 f(f(x,y,z),f(u,y,z),f(v,y,z)) = f(y,z,f(x,u,v)) # label(dist_long).  [copy 5 demod (8 8) flip a]

given #6 (wt=18): 12 f(A,f(B,D,E),f(C,D,E)) != f(D,E,f(A,B,C)) # answer(dist_short).  [copy 6 demod (8 8) flip a]

given #7 (wt=6): 13 f(x,y,y) = y.  [para (8 (a 1) 7 (a 1))]

given #8 (wt=12): 20 f(x,y,f(x,z,y)) = f(x,z,y).  [para (10 (a 2) 10 (a 1)) demod (8 (R) 13 8 9) flip a]

given #9 (wt=12): 48 f(x,y,f(x,y,z)) = f(x,y,z).  [para (13 (a 1) 10 (a 2 3)) demod (8 8 8 8)]

given #10 (wt=15): 14 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)).  [para (10 (a 2) 8 (a 1)) demod (8 (R) 9 9 8 9)]

given #11 (wt=15): 15 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)).  [para (10 (a 1) 8 (a 2)) demod (9 8)]

given #12 (wt=15): 16 f(x,y,f(x,z,u)) = f(x,u,f(x,z,y)).  [para (10 (a 2) 8 (a 2)) demod (9 8 8)]

given #13 (wt=15): 17 f(x,y,f(x,z,u)) = f(x,u,f(x,y,z)).  [para (8 (a 1) 10 (a 1 3)) demod (8 9 8 (R) 9)]

given #14 (wt=15): 39 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)).  [para (10 (a 1) 11 (a 2)) demod (7 8 8 8 (R) 24 9)]

given #15 (wt=18): 23 f(x,f(x,y,z),f(x,z,u)) = f(x,z,f(x,y,u)).  [para (7 (a 1) 11 (a 1 1)) demod (8 (R) 9 8 8)]

given #16 (wt=21): 18 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(x,y,f(z,u,v))).  [para (10 (a 1) 10 (a 1 3)) demod (8 9 8 (R) 9)]

given #17 (wt=18): 24 f(x,f(x,y,z),f(u,x,y)) = f(x,y,f(u,x,z)).  [para (7 (a 1) 11 (a 1 2)) demod (8 8 8 (R))]

given #18 (wt=18): 25 f(x,f(y,x,z),f(x,z,u)) = f(x,z,f(y,x,u)).  [para (7 (a 1) 11 (a 1 3)) demod (8 8 8 9)]

given #19 (wt=18): 50 f(x,y,f(x,z,f(x,y,u))) = f(x,z,f(x,y,u)).  [para (20 (a 1) 10 (a 1 3)) demod (8 8 9 8 (R) 9) flip a]

given #20 (wt=18): 56 f(x,y,f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)).  [para (10 (a 2) 48 (a 1 3)) demod (9)]

given #21 (wt=21): 19 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,z,v))).  [para (10 (a 2) 10 (a 1 3)) demod (8 (R) 9 9 9 8 (R) 9)]

given #22 (wt=18): 67 f(x,y,f(x,z,f(x,u,y))) = f(x,z,f(x,u,y)).  [para (20 (a 1) 14 (a 1 3)) flip a]

given #23 (wt=18): 77 f(x,f(y,x,z),f(u,y,x)) = f(u,x,f(y,x,z)).  [para (15 (a 1) 11 (a 2)) demod (8 (R) 13 8 8 8 (R))]

given #24 (wt=15): 350 f(x,y,f(z,u,f(x,y,u))) = f(x,y,u).  [back_demod 234 demod (319 13) flip a]

given #25 (wt=15): 353 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z).  [para (350 (a 1) 8 (a 1)) demod (8 (R) 9 8 8) flip a]

given #26 (wt=21): 26 f(f(x,y,z),f(x,y,u),f(x,y,v)) = f(x,y,f(u,v,z)).  [para (11 (a 1) 8 (a 1)) demod (8 8 8 8 8 8) flip a]

given #27 (wt=12): 401 f(x,y,f(z,x,y)) = f(z,x,y).  [para (353 (a 1) 15 (a 1)) demod (48 8 (R) 9) flip a]

given #28 (wt=15): 391 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y).  [back_demod 349 demod (353) flip a]

given #29 (wt=15): 392 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z).  [back_demod 219 demod (9 142 9 9 353)]

given #30 (wt=15): 394 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y).  [back_demod 209 demod (8 (R) 9 8 (R) 9 392 8 (R) 9 8 (R) 9) flip a]

given #31 (wt=21): 27 f(f(x,y,z),f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)).  [para (11 (a 1) 8 (a 2)) demod (8 8 8 8 8 8)]

given #32 (wt=15): 395 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z).  [back_demod 157 demod (8 (R) 9 8 (R) 9 8 (R) 9 8 (R) 9 394)]

given #33 (wt=15): 434 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)).  [para (39 (a 2) 26 (a 2)) demod (13 8 (R) 310)]

given #34 (wt=15): 547 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y).  [para (8 (a 1) 394 (a 1)) demod (8 (R) 9 8 9 8 8)]

given #35 (wt=15): 555 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y).  [para (394 (a 1) 15 (a 1)) flip a]

given #36 (wt=21): 28 f(f(x,y,z),f(x,z,u),f(x,z,v)) = f(x,z,f(y,u,v)).  [para (8 (a 1) 11 (a 1 1)) demod (8 9 8 9 8 (R) 9)]

given #37 (wt=15): 568 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z).  [para (394 (a 1) 26 (a 2)) demod (13 8 9 310 9)]

given #38 (wt=15): 598 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)).  [para (434 (a 1) 8 (a 2)) demod (9 8) flip a]

given #39 (wt=15): 624 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)).  [para (434 (a 1) 547 (a 2)) demod (9 8 (R) 9 523 8) flip a]

given #40 (wt=15): 690 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x).  [para (568 (a 1) 8 (a 2)) demod (9 8 9)]

given #41 (wt=33): 29 f(f(x,y,z),f(u,x,y),f(v,f(u,x,y),f(x,y,w))) = f(v,f(u,x,y),f(x,y,f(u,z,w))).  [para (11 (a 1) 10 (a 1 3)) demod (8 (R) 9 8 (R) 9 8 8 8 8 8) flip a]

given #42 (wt=15): 691 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u).  [para (8 (a 1) 568 (a 1 2)) demod (8 (R) 9 8 (R) 9)]

given #43 (wt=15): 692 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z).  [para (8 (a 2) 568 (a 1 2)) demod (8 8 205 8 8)]

given #44 (wt=15): 748 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)).  [para (598 (a 1) 8 (a 2)) demod (9 8)]

given #45 (wt=15): 767 f(x,f(x,y,z),f(y,u,z)) = f(x,y,z).  [para (26 (a 1) 598 (a 1)) demod (9 429 13 310 446 8 8) flip a]

given #46 (wt=33): 30 f(f(x,y,z),f(y,z,u),f(v,f(x,y,z),f(y,z,w))) = f(v,f(x,y,z),f(y,z,f(x,u,w))).  [para (11 (a 1) 10 (a 2 3)) demod (8 8 8 8 9)]

given #47 (wt=15): 788 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)).  [para (624 (a 1) 8 (a 2)) demod (9 8)]

given #48 (wt=15): 802 f(x,y,f(z,x,f(z,u,y))) = f(z,x,y).  [para (26 (a 1) 624 (a 1)) demod (9 429 13 172 48 758 429) flip a]

given #49 (wt=15): 805 f(x,y,f(z,u,y)) = f(u,y,f(z,x,y)).  [para (624 (a 1) 547 (a 2)) demod (9 8 (R) 9 773 8)]

given #50 (wt=15): 815 f(x,f(y,z,x),f(y,z,u)) = f(y,z,x).  [para (690 (a 1) 9 (a 1)) flip a]

given #51 (wt=33): 32 f(f(x,y,f(y,z,u)),f(u,v,f(x,y,z)),f(u,w,f(x,y,z))) = f(u,f(x,y,z),f(y,v,w)).  [para (10 (a 1) 11 (a 1 1)) demod (8 (R) 9 8 (R) 9)]

given #52 (wt=15): 944 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x).  [para (691 (a 1) 8 (a 2)) demod (8 8 8 8 8)]

given #53 (wt=15): 952 f(x,f(x,y,z),f(u,y,z)) = f(x,y,z).  [para (20 (a 1) 691 (a 1 3)) demod (9 9 9 446 8 8 9 48)]

given #54 (wt=15): 990 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z).  [para (691 (a 1) 395 (a 2)) demod (9 469 405)]

given #55 (wt=15): 1011 f(x,y,f(x,z,f(z,u,y))) = f(x,z,y).  [para (692 (a 1) 26 (a 2)) demod (8 7 8 8 172 48)]

given #56 (wt=33): 33 f(f(x,y,f(z,u,v)),f(z,u,f(y,u,v)),f(y,w,f(z,u,v))) = f(y,f(z,u,v),f(x,u,w)).  [para (10 (a 1) 11 (a 1 2)) demod (8 8 (R) 9)]

given #57 (wt=15): 1028 f(x,y,f(z,x,f(u,z,y))) = f(z,x,y).  [para (401 (a 1) 748 (a 1 3)) demod (13 792 8 (R) 9) flip a]

given #58 (wt=15): 1057 f(x,f(y,z,x),f(y,u,z)) = f(y,z,x).  [para (8 (a 1) 767 (a 1)) demod (8 8 8 (R) 8 8)]

given #59 (wt=15): 1200 f(x,f(y,z,x),f(u,y,z)) = f(y,z,x).  [para (401 (a 1) 788 (a 1 3)) demod (13 835 8 (R) 9) flip a]

given #60 (wt=15): 1211 f(x,y,f(y,z,f(x,u,z))) = f(x,y,z).  [para (10 (a 1) 802 (a 1)) demod (9)]

given #61 (wt=33): 34 f(f(x,y,f(z,u,v)),f(y,w,f(z,u,v)),f(z,u,f(y,u,v))) = f(y,f(z,u,v),f(x,u,w)).  [para (10 (a 1) 11 (a 1 3)) demod (8 (R) 9 8 9)]

given #62 (wt=15): 1418 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z).  [back_demod 818 demod (8 (R) 9 172 391 8 (R) 9)]

given #63 (wt=15): 1424 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u).  [para (8 (a 1) 944 (a 1 2)) demod (8 9 8 9)]

given #64 (wt=15): 1431 f(x,f(y,z,u),f(y,x,u)) = f(y,x,u).  [para (944 (a 1) 11 (a 2)) demod (8 (R) 9 8 (R) 9 8 (R) 9 8 (R) 9 7 8 1347 1211 9)]

given #65 (wt=15): 1813 f(x,f(y,z,u),f(y,u,x)) = f(y,u,x).  [para (1424 (a 1) 8 (a 2)) demod (8 8 8 8 8)]

given #66 (wt=33): 35 f(f(x,y,f(x,z,u)),f(x,v,f(x,y,u)),f(x,w,f(x,y,u))) = f(x,f(x,y,u),f(z,v,w)).  [para (10 (a 2) 11 (a 1 1)) demod (8 (R) 9 9 8 (R) 9 9 8 (R) 9 9)]

given #67 (wt=18): 428 f(x,y,f(z,u,f(x,v,y))) = f(x,y,f(v,z,u)).  [para (20 (a 1) 26 (a 1 1)) demod (28) flip a]

given #68 (wt=18): 429 f(x,y,f(z,u,f(x,y,v))) = f(x,y,f(z,v,u)).  [para (20 (a 1) 26 (a 1 2)) demod (9 26 8 9 8 9) flip a]

given #69 (wt=18): 509 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(v,z,u)).  [para (401 (a 1) 26 (a 1 1)) demod (27) flip a]

given #70 (wt=18): 548 f(x,y,f(y,z,f(x,u,f(x,z,v)))) = f(x,y,z).  [para (10 (a 1) 394 (a 1 3 3)) demod (9 8 (R) 9 8 (R) 9 9)]

given #71 (wt=21): 38 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,v,f(z,u,w))).  [para (10 (a 1) 11 (a 2 3)) demod (8 8 8 (R) 9 8 8 27 9 8 (R) 9)]

given #72 (wt=18): 549 f(x,y,f(y,z,f(z,u,f(x,z,v)))) = f(x,y,z).  [para (10 (a 2) 394 (a 1 3 3)) demod (8 (R) 9 9)]

given #73 (wt=18): 575 f(x,f(y,z,x),f(z,x,u)) = f(z,x,f(y,x,u)).  [para (13 (a 1) 27 (a 1 3)) demod (8 9)]

given #74 (wt=18): 647 f(x,f(y,z,x),f(y,x,u)) = f(y,x,f(z,x,u)).  [para (13 (a 1) 28 (a 1 3)) demod (8 9)]

given #75 (wt=18): 695 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v).  [para (10 (a 1) 568 (a 1 2)) demod (8 (R) 9 8 (R) 9)]

given #76 (wt=21): 40 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,w,u))).  [para (10 (a 2) 11 (a 2 3)) demod (8 8 8 8 27) flip a]

given #77 (wt=18): 704 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u).  [para (15 (a 1) 568 (a 1 2)) demod (8 (R) 9 8 8 8 8)]

given #78 (wt=18): 706 f(x,y,f(x,z,f(y,u,f(y,v,z)))) = f(x,y,z).  [para (16 (a 1) 568 (a 1 2)) demod (8 (R) 9 205 8 (R) 9)]

given #79 (wt=18): 728 f(x,y,f(z,f(y,z,u),f(x,z,v))) = f(x,y,z).  [para (568 (a 1) 391 (a 2)) demod (8 (R) 9 8 (R) 9 8 703 446 485 8 (R) 9)]

given #80 (wt=18): 774 f(x,y,f(z,x,f(z,u,f(z,y,v)))) = f(z,x,y).  [para (568 (a 1) 598 (a 1 3)) demod (8 (R) 13 8 753 758) flip a]

given #81 (wt=45): 42 f(f(x,y,f(z,u,v)),f(w,f(x,y,u),f(x,y,v)),f(v6,f(x,y,u),f(x,y,v))) = f(f(x,y,u),f(x,y,v),f(w,v6,f(x,y,z))).  [para (11 (a 1) 11 (a 1 1)) demod (8 8 8 8 8 8 8 8 8 8 8 8 8 8 8 8)]

given #82 (wt=18): 821 f(f(x,y,z),f(x,z,u),f(x,y,z)) = f(x,y,z).  [para (20 (a 1) 690 (a 1 3)) demod (20)]

given #83 (wt=18): 918 f(x,y,f(x,z,f(u,y,f(z,y,v)))) = f(x,z,y).  [para (391 (a 1) 29 (a 1 3)) demod (8 8 8 8 48 13 8 8 8 8 9 8 (R) 9 453 9 172 48) flip a]

given #84 (wt=18): 922 f(x,y,f(z,x,f(y,u,f(z,y,v)))) = f(z,x,y).  [para (394 (a 1) 29 (a 2 3)) demod (13 8 8 8 8 468 758 48 8 8 9 13)]

given #85 (wt=18): 926 f(x,y,f(z,x,f(u,y,f(z,y,v)))) = f(z,x,y).  [para (547 (a 1) 29 (a 1 3)) demod (8 8 8 8 48 13 8 8 8 8 9 8 (R) 9 452 9 758 48) flip a]

given #86 (wt=45): 43 f(f(x,f(y,z,u),f(z,u,v)),f(z,u,f(y,v,w)),f(v6,f(y,z,u),f(z,u,v))) = f(f(y,z,u),f(z,u,v),f(x,v6,f(z,u,w))).  [para (11 (a 1) 11 (a 1 2)) demod (8 8 8 8 8 8 8 8 8 8 9)]

given #87 (wt=18): 1004 f(x,y,f(x,z,f(u,y,f(v,z,y)))) = f(x,z,y).  [para (691 (a 1) 691 (a 1 3)) demod (9 446 8 (R) 9 579 691)]

given #88 (wt=18): 1035 f(x,y,f(z,x,f(u,z,f(z,y,v)))) = f(z,x,y).  [para (568 (a 1) 748 (a 1 3)) demod (13 792 8 (R) 9) flip a]

given #89 (wt=18): 1053 f(x,f(y,z,x),f(y,u,f(v,y,z))) = f(y,z,x).  [back_demod 997 demod (1036)]

given #90 (wt=18): 1056 f(x,y,f(z,f(x,y,z),f(x,u,v))) = f(x,y,z).  [back_demod 390 demod (8 (R) 9 1036 9)]

given #91 (wt=45): 44 f(f(x,f(y,z,u),f(z,u,v)),f(w,f(y,z,u),f(z,u,v)),f(z,u,f(y,v,v6))) = f(f(y,z,u),f(z,u,v),f(x,w,f(z,u,v6))).  [para (11 (a 1) 11 (a 1 3)) demod (8 8 8 8 8 8 8 8 8 8)]

given #92 (wt=18): 1097 f(x,f(y,z,x),f(y,u,f(y,v,z))) = f(y,z,x).  [para (767 (a 1) 690 (a 1 3)) demod (8 8 9 8 8 9 1036 8 8 1057)]

given #93 (wt=18): 1220 f(x,y,f(z,f(x,y,z),f(y,u,v))) = f(x,y,z).  [para (802 (a 1) 395 (a 2)) demod (8 8 (R) 9 8 8 (R) 9 9 469 9 8 (R) 9 1017 1033 8 (R) 9 8 8)]

given #94 (wt=18): 1462 f(x,y,f(z,f(u,y,z),f(x,z,v))) = f(x,y,z).  [para (691 (a 1) 952 (a 2)) demod (691 446 485)]

given #95 (wt=18): 1669 f(x,y,f(z,x,f(z,u,f(z,v,y)))) = f(z,x,y).  [para (1028 (a 1) 690 (a 1 3)) demod (8 (R) 9 8 1639 9 8 (R) 9 802)]

given #96 (wt=21): 58 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,u,v))).  [para (14 (a 1) 10 (a 1 3)) demod (8 (R) 9 9 8 (R) 9)]

given #97 (wt=18): 1801 f(x,f(y,z,f(y,u,v)),f(x,y,u)) = f(x,y,u).  [para (10 (a 2) 1418 (a 1 2)) demod (8 (R) 9 9 9)]

given #98 (wt=18): 1802 f(x,f(y,z,f(y,u,v)),f(x,y,v)) = f(x,y,v).  [para (16 (a 1) 1418 (a 1 2))]

given #99 (wt=18): 1836 f(x,y,f(x,z,f(u,y,f(z,v,y)))) = f(x,z,y).  [para (1424 (a 1) 691 (a 1 3)) demod (9 446 8 (R) 9 579 1424)]

given #100 (wt=18): 1843 f(x,y,f(z,f(y,u,z),f(x,z,v))) = f(x,y,z).  [para (1424 (a 1) 952 (a 2)) demod (1424 446 485)]

given #101 (wt=21): 59 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,z,u))).  [para (10 (a 1) 14 (a 1 3)) demod (8 (R) 9 8 (R) 9)]

given #102 (wt=18): 2186 f(x,y,f(x,z,f(y,u,f(z,y,v)))) = f(x,z,y).  [para (548 (a 1) 8 (a 2)) demod (8 (R) 9 9 8 8)]

given #103 (wt=18): 2248 f(x,f(y,z,f(y,u,v)),f(y,x,u)) = f(y,x,u).  [para (548 (a 1) 548 (a 2)) demod (9 1876 2190)]

given #104 (wt=18): 2302 f(x,y,f(x,z,f(z,u,f(z,y,v)))) = f(x,z,y).  [para (549 (a 1) 8 (a 2)) demod (8 (R) 9 9 8 8)]

given #105 (wt=18): 2305 f(x,y,f(z,f(x,z,u),f(y,z,v))) = f(x,y,z).  [para (10 (a 2) 549 (a 1 3))]

given #106 (wt=21): 60 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,v,u))).  [para (10 (a 2) 14 (a 2 3)) flip a]

given #107 (wt=18): 2365 f(x,f(y,z,f(u,y,v)),f(u,x,y)) = f(u,x,y).  [para (549 (a 1) 548 (a 2)) demod (9 1876 2190)]

given #108 (wt=18): 2455 f(x,f(y,z,f(z,u,v)),f(z,v,x)) = f(z,v,x).  [para (695 (a 1) 8 (a 2)) demod (8 8 8 8 8)]

given #109 (wt=15): 4873 f(x,y,f(x,z,f(u,z,y))) = f(x,z,y).  [para (2455 (a 1) 748 (a 1 3)) demod (13 9 8 (R) 9 835 8 (R) 9 3481 8 8 (R) 9) flip a]

given #110 (wt=18): 2464 f(x,y,f(x,z,f(u,y,f(y,v,z)))) = f(x,y,z).  [para (695 (a 1) 11 (a 2)) demod (7 8 (R) 9 8 (R) 9 1876 20)]

given #111 (wt=33): 61 f(f(x,y,f(x,z,u)),f(z,v,f(x,y,u)),f(z,w,f(x,y,u))) = f(z,f(x,y,u),f(x,v,w)).  [para (14 (a 1) 11 (a 1 1)) demod (8 (R) 9 8 (R) 9)]

given #112 (wt=18): 2467 f(x,y,f(z,u,f(x,u,f(u,v,y)))) = f(x,u,y).  [para (20 (a 1) 695 (a 1 3)) demod (9 9 9 1876 2035 8 8 9 48)]

given #113 (wt=18): 2543 f(x,y,f(z,u,f(z,y,f(x,v,z)))) = f(x,z,y).  [para (695 (a 1) 34 (a 2)) demod (7 1876 1021 8 7 8 1876)]

given #114 (wt=18): 2625 f(x,f(y,z,f(z,u,v)),f(z,u,x)) = f(z,u,x).  [para (704 (a 1) 8 (a 2)) demod (8 8 8 8 8)]

given #115 (wt=18): 2676 f(x,y,f(z,y,f(z,u,f(x,v,z)))) = f(x,z,y).  [para (704 (a 1) 34 (a 2)) demod (7 1876 1021 8 7 8 1876)]

given #116 (wt=33): 62 f(f(x,y,f(z,u,v)),f(z,u,f(y,z,v)),f(y,w,f(z,u,v))) = f(y,f(z,u,v),f(x,z,w)).  [para (14 (a 1) 11 (a 1 2)) demod (8 (R) 9 8 (R) 9)]

given #117 (wt=15): 5512 f(x,y,f(y,z,f(u,x,z))) = f(x,y,z).  [para (568 (a 1) 62 (a 1 3)) demod (8 (R) 9 8 (R) 9 48 8 (R) 9 13 8 (R) 9 1876 1921 8 (R) 9 8 (R) 9) flip a]

given #118 (wt=18): 2739 f(x,y,f(z,y,f(z,u,f(x,z,v)))) = f(x,z,y).  [para (728 (a 1) 9 (a 2)) demod (8 (R) 9 1876 9 9)]

given #119 (wt=18): 2750 f(x,y,f(z,y,f(z,u,f(z,x,v)))) = f(z,x,y).  [para (728 (a 1) 11 (a 2)) demod (8 (R) 9 8 8 8 (R) 9 8 8 27 1876 8)]

given #120 (wt=18): 2881 f(x,f(y,z,f(u,y,v)),f(x,u,y)) = f(x,u,y).  [para (548 (a 1) 774 (a 2)) demod (8 (R) 9 8 (R) 9 9 8 (R) 9 1876 2838 8 8)]

given #121 (wt=33): 63 f(f(x,y,f(z,u,v)),f(y,w,f(z,u,v)),f(z,u,f(y,z,v))) = f(y,f(z,u,v),f(x,z,w)).  [para (14 (a 1) 11 (a 1 3)) demod (8 (R) 9 8 (R) 9 9)]

given #122 (wt=18): 2894 f(x,y,f(z,y,f(x,u,f(z,x,v)))) = f(z,x,y).  [para (774 (a 1) 774 (a 2)) demod (8 (R) 9 8 (R) 9 9 8 (R) 9 2837 8)]

given #123 (wt=18): 3189 f(x,y,f(z,y,f(x,u,f(x,z,v)))) = f(x,z,y).  [para (922 (a 1) 8 (a 2)) demod (8 (R) 9 9 8)]

given #124 (wt=18): 3233 f(x,y,f(y,z,f(u,z,f(x,z,v)))) = f(x,y,z).  [para (10 (a 1) 926 (a 1)) demod (9)]

given #125 (wt=18): 3459 f(x,f(y,z,f(y,u,v)),f(y,u,x)) = f(y,u,x).  [para (1053 (a 1) 9 (a 1)) demod (8 8) flip a]

given #126 (wt=21): 68 f(x,f(y,z,u),f(x,z,v)) = f(x,v,f(y,z,f(x,z,u))).  [para (15 (a 1) 10 (a 2 3)) demod (8 8 8 (R) 9)]

given #127 (wt=18): 3578 f(x,y,f(z,f(x,z,y),f(y,u,v))) = f(x,z,y).  [para (1056 (a 1) 8 (a 2)) demod (8 8 9 8 8)]

given #128 (wt=18): 3674 f(x,y,f(z,f(u,y,z),f(x,u,z))) = f(x,y,z).  [para (13 (a 1) 44 (a 2)) demod (8 (R) 9 48 1876 48 8 (R) 9 48 647 9 429 13 8 418 48)]

given #129 (wt=18): 3751 f(x,y,f(z,f(x,z,y),f(u,z,y))) = f(x,z,y).  [para (1097 (a 1) 15 (a 1 3)) demod (13 9 3481 8) flip a]

given #130 (wt=18): 3859 f(x,y,f(z,f(x,z,u),f(y,v,z))) = f(x,y,z).  [para (1462 (a 1) 428 (a 2)) demod (8 (R) 9 9 429 8 (R))]

given #131 (wt=21): 69 f(x,y,f(z,u,f(y,u,v))) = f(y,u,f(x,y,f(z,u,v))).  [para (10 (a 1) 15 (a 1 3)) demod (8 8 (R) 9)]

given #132 (wt=18): 3893 f(x,y,f(x,z,f(z,u,f(z,v,y)))) = f(x,z,y).  [para (1669 (a 1) 9 (a 2)) demod (8 (R) 9 9 8 (R) 9)]

given #133 (wt=18): 3896 f(x,y,f(y,z,f(x,u,f(x,v,z)))) = f(x,y,z).  [para (10 (a 1) 1669 (a 1)) demod (9)]

given #134 (wt=18): 4204 f(x,f(y,z,f(y,u,v)),f(y,v,x)) = f(y,v,x).  [para (1802 (a 1) 8 (a 2)) demod (8 8 8 8 8)]

given #135 (wt=18): 4209 f(x,y,f(z,u,f(x,z,f(z,v,y)))) = f(x,z,y).  [para (20 (a 1) 1802 (a 1 3)) demod (9 9 9 1876 4046 8 8 9 48)]

given #136 (wt=21): 70 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,u,f(x,y,v))).  [para (10 (a 2) 15 (a 1 3)) demod (8 (R) 9 9 8 (R) 9) flip a]

given #137 (wt=18): 4767 f(x,f(y,z,f(u,z,v)),f(x,u,z)) = f(x,u,z).  [para (8 (a 2) 2365 (a 1 2)) demod (9 8 (R) 9 8 (R) 9)]

given #138 (wt=18): 4855 f(x,f(y,z,f(y,u,v)),f(y,x,v)) = f(y,x,v).  [para (2455 (a 1) 11 (a 2)) demod (8 (R) 9 8 (R) 9 8 (R) 9 8 (R) 9 7 8 1347 3896 9)]

given #139 (wt=18): 4931 f(x,y,f(x,z,f(y,u,f(v,y,z)))) = f(x,y,z).  [para (1200 (a 1) 4873 (a 2)) demod (8 8 1876 1579 9 1463 428 8)]

given #140 (wt=18): 5114 f(x,y,f(z,u,f(u,x,f(u,v,y)))) = f(u,x,y).  [para (8 (a 1) 2467 (a 1)) demod (8 (R) 9 8 8 8 (R) 9)]

given #141 (wt=21): 71 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(x,y,f(z,u,v))).  [para (10 (a 1) 15 (a 2 3)) demod (8 (R) 9 8 (R) 9 9 8 (R) 9 8 (R) 9) flip a]

given #142 (wt=18): 5425 f(x,f(y,z,f(u,y,v)),f(u,y,x)) = f(u,y,x).  [para (728 (a 1) 2676 (a 2)) demod (8 (R) 9 1876 8 (R) 9 1876 9 1347 412 8 922 9)]

given #143 (wt=18): 6625 f(x,f(y,x,z),f(u,x,z)) = f(y,x,f(u,x,z)).  [para (691 (a 1) 69 (a 2 3)) demod (8 8 401 20 8 (R)) flip a]

given #144 (wt=18): 6653 f(x,f(y,z,x),f(u,z,x)) = f(y,x,f(u,z,x)).  [para (944 (a 1) 69 (a 2 3)) demod (8 9 509 8 (R) 9 2168 13 9 8 8 (R)) flip a]

given #145 (wt=18): 6670 f(x,f(y,z,x),f(z,u,x)) = f(y,x,f(z,u,x)).  [para (1813 (a 1) 69 (a 2 3)) demod (8 9 428 8 (R) 9 2093 13 9 8 8 (R)) flip a]

given #146 (wt=21): 72 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,v,f(x,y,u))).  [para (10 (a 2) 15 (a 2 3)) demod (8 (R) 9 8 (R) 9)]

given #147 (wt=18): 6934 f(x,y,f(z,u,f(z,x,f(z,v,y)))) = f(z,x,y).  [para (8 (a 1) 4209 (a 1)) demod (8 (R) 9 8 8 8 (R) 9)]

given #148 (wt=18): 7158 f(x,y,f(x,z,f(u,z,f(z,y,v)))) = f(x,z,y).  [para (4767 (a 1) 11 (a 2)) demod (8 (R) 9 7 8 (R) 9 8 (R) 9 8 (R) 9 8 (R) 9 1876 20 9)]

given #149 (wt=21): 76 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,u,w))).  [para (15 (a 1) 11 (a 2 3)) demod (8 8 8 (R) 9 8 8 27 8 (R) 9) flip a]

given #150 (wt=21): 81 f(x,y,f(z,u,f(y,z,v))) = f(y,z,f(x,y,f(z,u,v))).  [para (14 (a 1) 15 (a 1 3)) demod (8 (R) 9 8 (R) 9)]

given #151 (wt=33): 73 f(f(x,y,f(y,z,u)),f(y,v,f(x,y,u)),f(y,w,f(x,y,u))) = f(y,f(x,y,u),f(z,v,w)).  [para (15 (a 1) 11 (a 1 1)) demod (8 (R) 9 8 (R) 9 8 (R) 9)]

given #152 (wt=21): 82 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,u,f(x,y,v))).  [para (15 (a 1) 15 (a 2 3)) demod (8 (R) 9 8 (R) 9 8 (R) 9 8 (R) 9)]

given #153 (wt=21): 84 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,z,f(x,y,u))).  [para (10 (a 2) 16 (a 1 3)) demod (9 9) flip a]

given #154 (wt=21): 89 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,u,v))).  [para (16 (a 1) 11 (a 2 3)) demod (8 8 8 8 27 9)]

given #155 (wt=21): 92 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,v,z))).  [para (16 (a 1) 14 (a 2 3)) demod (9) flip a]

given #156 (wt=33): 86 f(f(x,y,f(x,z,u)),f(u,v,f(x,y,z)),f(u,w,f(x,y,z))) = f(u,f(x,y,z),f(x,v,w)).  [para (16 (a 1) 11 (a 1 1)) demod (9 8 (R) 9 9 8 (R) 9 9)]

given #157 (wt=21): 94 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(x,y,f(z,v,u))).  [para (16 (a 1) 15 (a 2 3)) demod (8 (R) 9 9 8 (R) 9) flip a]

given #158 (wt=21): 95 f(x,f(y,z,u),f(x,v,z)) = f(x,v,f(y,z,f(x,z,u))).  [para (15 (a 1) 16 (a 1 3)) demod (9) flip a]

given #159 (wt=21): 116 f(x,y,f(z,u,f(u,y,v))) = f(u,y,f(x,y,f(z,u,v))).  [para (18 (a 1) 8 (a 2)) demod (8 (R) 9 9 8 (R) 9 8 (R) 9)]

given #160 (wt=18): 9059 f(x,f(y,z,x),f(u,y,x)) = f(u,x,f(y,z,x)).  [para (1813 (a 1) 116 (a 2 3)) demod (8 428 8 (R) 9 2093 13 9 8) flip a]

given #161 (wt=33): 87 f(f(x,y,f(z,u,v)),f(z,v,f(y,z,u)),f(y,w,f(z,u,v))) = f(y,f(z,u,v),f(x,z,w)).  [para (16 (a 1) 11 (a 1 2)) demod (8 8 (R) 9)]

given #162 (wt=21): 117 f(x,y,f(z,u,f(u,x,v))) = f(u,x,f(x,y,f(z,u,v))).  [para (8 (a 1) 18 (a 1)) demod (8 (R) 9 8 8 8 (R) 9)]

given #163 (wt=18): 9315 f(x,y,f(y,z,f(z,u,f(x,v,z)))) = f(x,y,z).  [para (117 (a 1) 4767 (a 1)) demod (9 469 9 8 (R) 9 9 758 48 429 9 8 (R) 9 48)]

given #164 (wt=21): 173 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,u,z))).  [para (10 (a 2) 24 (a 2 3)) demod (8 8 41 8 8) flip a]

given #165 (wt=21): 180 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,u,f(x,y,z))).  [para (15 (a 1) 24 (a 1 3)) demod (8 (R) 9 9 8 8 8 (R) 9 172 41 172 9 172 48 8 (R) 9 8 8 172) flip a]

given #166 (wt=33): 88 f(f(x,y,f(z,u,v)),f(y,w,f(z,u,v)),f(z,v,f(y,z,u))) = f(y,f(z,u,v),f(x,z,w)).  [para (16 (a 1) 11 (a 1 3)) demod (8 (R) 9 8 9)]

given #167 (wt=18): 9504 f(x,y,f(z,u,f(z,v,f(z,x,y)))) = f(z,x,y).  [para (180 (a 1) 69 (a 2 3)) demod (392) flip a]

given #168 (wt=18): 9588 f(x,y,f(z,u,f(z,v,f(x,z,y)))) = f(x,z,y).  [para (1802 (a 1) 88 (a 2)) demod (7 1876 1876 9385 8 20)]

given #169 (wt=18): 9598 f(x,y,f(z,f(x,y,z),f(z,u,v))) = f(x,y,z).  [para (16 (a 1) 9504 (a 1 3)) demod (8 8 8 8)]

given #170 (wt=21): 184 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,u,f(x,y,z))).  [para (16 (a 1) 24 (a 2 3)) demod (8 8 9 41 8)]

given #171 (wt=33): 100 f(f(x,y,f(y,z,u)),f(z,v,f(x,y,u)),f(z,w,f(x,y,u))) = f(z,f(x,y,u),f(y,v,w)).  [para (39 (a 1) 11 (a 1 1)) demod (8 (R) 9 8 (R) 9)]

given #172 (wt=18): 9965 f(x,y,f(z,x,f(u,z,f(z,v,y)))) = f(z,x,y).  [para (2455 (a 1) 100 (a 2)) demod (7 8 7452 7 9 9)]

given #173 (wt=21): 186 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,z,f(x,u,y))).  [para (24 (a 1) 23 (a 1 2)) demod (8 (R) 9 8 8 9 172 48 172 20 8 8 9 172 48)]

given #174 (wt=21): 187 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,u,f(x,z,y))).  [para (24 (a 1) 23 (a 1 3)) demod (8 8 172 41 172 172 20 8 8 172 48)]

given #175 (wt=21): 228 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,z,f(x,y,v))).  [para (50 (a 1) 25 (a 1 3)) demod (8 (R) 9 172 181 8 (R) 9 181)]

given #176 (wt=42): 108 f(f(x,y,f(x,z,u)),f(v,f(x,z,y),f(x,y,u)),f(w,f(x,z,y),f(x,y,u))) = f(f(x,z,y),f(x,y,u),f(w,x,v)).  [para (23 (a 1) 11 (a 1 2)) demod (8 (R))]

given #177 (wt=21): 264 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,z,f(x,y,u))).  [para (19 (a 1) 16 (a 1)) demod (9 172)]

given #178 (wt=21): 267 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,v,f(x,y,z))).  [para (19 (a 1) 16 (a 2)) demod (172 9)]

given #179 (wt=21): 316 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,v,u))).  [para (77 (a 1) 11 (a 2 3)) demod (8 (R) 9 8 8 8 9 8 8 27 172 48 8 (R) 9 8 (R) 9)]

given #180 (wt=21): 377 f(x,y,f(x,z,f(u,v,f(x,v,y)))) = f(x,z,f(x,v,y)).  [para (350 (a 1) 24 (a 2 3)) demod (8 8 8 8 9 172 48 8 8)]

given #181 (wt=36): 109 f(f(x,y,z),f(u,f(y,z,v),f(x,y,z)),f(y,z,f(x,v,w))) = f(u,f(x,y,z),f(y,z,f(x,v,w))).  [para (11 (a 1) 23 (a 1 3)) demod (8 8 8 (R) 8 8 8 8 8 (R) 65)]

given #182 (wt=21): 398 f(x,f(y,z,u),f(x,v,f(x,y,u))) = f(x,v,f(x,y,u)).  [para (353 (a 1) 10 (a 2 3)) demod (9 8 8 203 9 8 (R) 9)]

given #183 (wt=21): 404 f(x,y,f(x,z,f(x,u,f(u,v,y)))) = f(x,z,f(x,u,y)).  [para (353 (a 1) 24 (a 1 3)) demod (8 8 9 8 8 9 172 56 8 8 8 (R) 9 203 398)]

given #184 (wt=21): 405 f(x,y,f(x,z,f(u,v,f(x,u,y)))) = f(x,z,f(x,u,y)).  [para (353 (a 1) 24 (a 2 3)) demod (8 8 8 8 9 172 48 8 8)]

given #185 (wt=21): 406 f(x,f(y,z,u),f(x,u,f(x,y,v))) = f(x,v,f(x,y,u)).  [para (353 (a 1) 67 (a 1 3 3)) demod (9 9 203 172 48 9 396)]

given #186 (wt=27): 118 f(x,y,f(z,u,f(x,z,f(u,v,w)))) = f(x,z,f(x,y,f(u,v,f(z,u,w)))).  [para (18 (a 1) 10 (a 1 3)) demod (8 (R) 9 8 (R) 9 8 (R) 9 9 8 (R) 9)]

given #187 (wt=18): 10826 f(f(x,y,z),f(y,u,v),f(x,y,z)) = f(x,y,z).  [para (690 (a 1) 118 (a 2 3)) demod (9 8 (R) 1418 48 8 (R) 9 1876 428 7 9 48)]

given #188 (wt=18): 10870 f(f(x,y,z),f(z,u,v),f(x,y,z)) = f(x,y,z).  [para (8 (a 1) 10826 (a 1 1)) demod (8 8)]

given #189 (wt=18): 10871 f(f(x,y,z),f(x,u,v),f(x,y,z)) = f(x,y,z).  [para (8 (a 2) 10826 (a 1 1)) demod (8 8 8 8)]

given #190 (wt=21): 437 f(x,f(y,z,u),f(v,x,y)) = f(v,x,f(y,z,f(x,y,u))).  [para (26 (a 1) 18 (a 2 3)) demod (8 8 56 9 26 8 8 8 (R) 9 310) flip a]

given #191 (wt=27): 119 f(x,y,f(z,u,f(x,v,f(x,z,w)))) = f(x,z,f(x,y,f(z,u,f(x,v,w)))).  [para (18 (a 2) 10 (a 1 3)) demod (8 (R) 9 8 (R) 9 8 (R) 9 9 8 (R) 9)]

given #192 (wt=18): 11045 f(x,y,f(z,u,f(z,y,f(z,v,x)))) = f(z,x,y).  [back_demod 4228 demod (10978 9)]

given #193 (wt=21): 473 f(x,y,f(z,u,f(x,v,z))) = f(x,y,f(x,z,f(y,v,u))).  [back_demod 162 demod (469 9 48 428)]

given #194 (wt=18): 11169 f(x,f(y,z,u),f(v,y,z)) = f(y,z,f(v,x,u)).  [para (11 (a 1) 473 (a 2 3)) demod (8 8 8 8 8 (R) 1876 509 8 (R) 9 758 48 1028 8 (R) 9 8 (R) 9 10465)]

-------- Proof 1 -------- (56.84 + 0.08 seconds) dist_short.

-------- PROOF --------
Length of proof is 132.
Maximum clause weight is 54.
4 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity).  [input]
5 f(f(x,y,z),u,v) = f(f(x,u,v),f(y,u,v),f(z,u,v)) # label(dist_long).  [input]
6 f(f(A,B,C),D,E) != f(A,f(B,D,E),f(C,D,E)) # answer(dist_short).  [input]
7 f(x,x,y) = x # label(majority).  [input]
8 f(x,y,z) = f(z,x,y) # label(2a).  [input]
9 f(x,y,z) = f(x,z,y) # label(2b).  [input]
10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity).  [copy 4 demod (8 8 8 (R) 9)]
11 f(f(x,y,z),f(u,y,z),f(v,y,z)) = f(y,z,f(x,u,v)) # label(dist_long).  [copy 5 demod (8 8) flip a]
12 f(A,f(B,D,E),f(C,D,E)) != f(D,E,f(A,B,C)) # answer(dist_short).  [copy 6 demod (8 8) flip a]
13 f(x,y,y) = y.  [para (8 (a 1) 7 (a 1))]
14 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)).  [para (10 (a 2) 8 (a 1)) demod (8 (R) 9 9 8 9)]
15 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)).  [para (10 (a 1) 8 (a 2)) demod (9 8)]
18 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(x,y,f(z,u,v))).  [para (10 (a 1) 10 (a 1 3)) demod (8 9 8 (R) 9)]
20 f(x,y,f(x,z,y)) = f(x,z,y).  [para (10 (a 2) 10 (a 1)) demod (8 (R) 13 8 9) flip a]
23 f(x,f(x,y,z),f(x,z,u)) = f(x,z,f(x,y,u)).  [para (7 (a 1) 11 (a 1 1)) demod (8 (R) 9 8 8)]
24 f(x,f(x,y,z),f(u,x,y)) = f(x,y,f(u,x,z)).  [para (7 (a 1) 11 (a 1 2)) demod (8 8 8 (R))]
25 f(x,f(y,x,z),f(x,z,u)) = f(x,z,f(y,x,u)).  [para (7 (a 1) 11 (a 1 3)) demod (8 8 8 9)]
26 f(f(x,y,z),f(x,y,u),f(x,y,v)) = f(x,y,f(u,v,z)).  [para (11 (a 1) 8 (a 1)) demod (8 8 8 8 8 8) flip a]
27 f(f(x,y,z),f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)).  [para (11 (a 1) 8 (a 2)) demod (8 8 8 8 8 8)]
28 f(f(x,y,z),f(x,z,u),f(x,z,v)) = f(x,z,f(y,u,v)).  [para (8 (a 1) 11 (a 1 1)) demod (8 9 8 9 8 (R) 9)]
30 f(f(x,y,z),f(y,z,u),f(v,f(x,y,z),f(y,z,w))) = f(v,f(x,y,z),f(y,z,f(x,u,w))).  [para (11 (a 1) 10 (a 2 3)) demod (8 8 8 8 9)]
33 f(f(x,y,f(z,u,v)),f(z,u,f(y,u,v)),f(y,w,f(z,u,v))) = f(y,f(z,u,v),f(x,u,w)).  [para (10 (a 1) 11 (a 1 2)) demod (8 8 (R) 9)]
34 f(f(x,y,f(z,u,v)),f(y,w,f(z,u,v)),f(z,u,f(y,u,v))) = f(y,f(z,u,v),f(x,u,w)).  [para (10 (a 1) 11 (a 1 3)) demod (8 (R) 9 8 9)]
35 f(f(x,y,f(x,z,u)),f(x,v,f(x,y,u)),f(x,w,f(x,y,u))) = f(x,f(x,y,u),f(z,v,w)).  [para (10 (a 2) 11 (a 1 1)) demod (8 (R) 9 9 8 (R) 9 9 8 (R) 9 9)]
38 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,v,f(z,u,w))).  [para (10 (a 1) 11 (a 2 3)) demod (8 8 8 (R) 9 8 8 27 9 8 (R) 9)]
39 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)).  [para (10 (a 1) 11 (a 2)) demod (7 8 8 8 (R) 24 9)]
41 f(x,f(x,y,z),f(x,y,u)) = f(x,u,f(x,y,z)).  [para (10 (a 2) 11 (a 2)) demod (8 7 8 9 8 9 8 (R) 9)]
48 f(x,y,f(x,y,z)) = f(x,y,z).  [para (13 (a 1) 10 (a 2 3)) demod (8 8 8 8)]
50 f(x,y,f(x,z,f(x,y,u))) = f(x,z,f(x,y,u)).  [para (20 (a 1) 10 (a 1 3)) demod (8 8 9 8 (R) 9) flip a]
53 f(f(x,y,z),f(z,u,f(x,y,z)),f(z,v,f(x,y,z))) = f(z,f(x,y,z),f(x,u,v)).  [para (20 (a 1) 11 (a 1 1)) demod (8 (R) 9 8 (R) 9)]
56 f(x,y,f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)).  [para (10 (a 2) 48 (a 1 3)) demod (9)]
57 f(f(x,y,z),f(y,u,f(x,y,z)),f(y,v,f(x,y,z))) = f(y,f(x,y,z),f(x,u,v)).  [para (48 (a 1) 11 (a 1 1)) demod (8 (R) 9 8 (R) 9)]
62 f(f(x,y,f(z,u,v)),f(z,u,f(y,z,v)),f(y,w,f(z,u,v))) = f(y,f(z,u,v),f(x,z,w)).  [para (14 (a 1) 11 (a 1 2)) demod (8 (R) 9 8 (R) 9)]
63 f(f(x,y,f(z,u,v)),f(y,w,f(z,u,v)),f(z,u,f(y,z,v))) = f(y,f(z,u,v),f(x,z,w)).  [para (14 (a 1) 11 (a 1 3)) demod (8 (R) 9 8 (R) 9 9)]
64 f(x,f(y,x,z),f(z,f(y,x,z),f(x,z,u))) = f(x,z,f(y,u,f(y,x,z))).  [para (14 (a 1) 11 (a 1)) demod (8 8 8 8 (R) 9)]
65 f(f(x,y,z),f(y,z,u),f(v,f(y,z,w),f(x,y,z))) = f(v,f(x,y,z),f(y,z,f(x,u,w))).  [para (11 (a 1) 14 (a 1 3)) demod (8 (R) 9 8 8 8 8 8 (R)) flip a]
66 f(x,f(x,y,z),f(y,f(x,y,z),f(x,y,u))) = f(x,y,f(z,u,f(x,y,z))).  [para (11 (a 1) 14 (a 1)) demod (8 8 8 8 8 8 8 8 8 8 (R) 9) flip a]
77 f(x,f(y,x,z),f(u,y,x)) = f(u,x,f(y,x,z)).  [para (15 (a 1) 11 (a 2)) demod (8 (R) 13 8 8 8 (R))]
107 f(x,f(x,y,z),f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,u,v))).  [para (10 (a 2) 23 (a 1 3)) demod (9)]
109 f(f(x,y,z),f(u,f(y,z,v),f(x,y,z)),f(y,z,f(x,v,w))) = f(u,f(x,y,z),f(y,z,f(x,v,w))).  [para (11 (a 1) 23 (a 1 3)) demod (8 8 8 (R) 8 8 8 8 8 (R) 65)]
121 f(x,f(y,z,u),f(x,y,z)) = f(y,z,f(x,y,f(x,z,u))).  [para (18 (a 1) 10 (a 2)) demod (8 (R) 9 8 (R) 9)]
137 f(f(x,y,z),f(y,z,u),f(y,v,f(y,z,f(x,y,z)))) = f(y,z,f(x,y,f(x,u,v))).  [para (11 (a 1) 18 (a 2 3)) demod (8 8 8 8 8 (R) 9 8 (R) 9 25)]
142 f(x,y,f(x,z,f(y,u,f(x,y,v)))) = f(x,y,f(x,z,f(y,u,v))).  [para (18 (a 2) 48 (a 1 3)) demod (8 (R) 9 8 (R) 9)]
159 f(x,f(x,y,f(x,z,f(y,u,v))),f(x,w,f(y,u,f(x,y,v)))) = f(x,f(y,u,f(x,y,v)),f(x,z,w)).  [para (18 (a 1) 23 (a 1 2)) demod (8 (R) 9 8 (R) 9 9 8 (R) 9)]
162 f(x,y,f(z,f(x,y,u),f(x,v,f(x,y,u)))) = f(x,y,f(x,u,f(z,v,f(x,y,u)))).  [para (18 (a 2) 23 (a 1)) demod (9 9 9 9 9)]
168 f(x,f(x,y,z),f(u,f(x,y,z),f(x,y,v))) = f(u,f(x,y,z),f(x,y,f(x,z,v))).  [para (24 (a 1) 10 (a 1 3)) demod (8 8 8 (R) 9 8 8 8) flip a]
169 f(x,f(x,y,f(x,z,u)),f(x,u,v)) = f(x,u,f(x,v,f(x,y,z))).  [para (10 (a 1) 24 (a 1 2)) demod (8 (R) 9 8 8 8 (R) 9 8 (R) 9)]
171 f(x,f(y,z,f(x,y,u)),f(x,y,v)) = f(x,y,f(x,v,f(y,z,u))).  [para (10 (a 2) 24 (a 1 2)) demod (8 8 9 8 (R) 9)]
172 f(x,f(x,y,z),f(x,u,v)) = f(x,z,f(x,u,f(x,y,v))).  [para (10 (a 2) 24 (a 1 3)) demod (9 8 8 169 9 41 8 8) flip a]
197 f(x,y,f(x,z,f(x,u,f(x,v,y)))) = f(x,y,f(x,z,f(x,v,u))).  [para (24 (a 1) 24 (a 1 2)) demod (8 (R) 9 8 (R) 9 172 48 172 8 8 8 (R) 9 172 48)]
198 f(f(x,y,z),f(x,y,f(x,z,u)),f(v,f(x,y,z),f(x,y,u))) = f(f(x,y,z),f(x,y,u),f(x,v,f(x,y,z))).  [para (24 (a 1) 24 (a 1 3)) demod (8 8 8 8 8 9 8 8 9)]
200 f(x,f(y,x,z),f(y,x,f(y,z,u))) = f(y,x,f(z,u,f(y,x,z))).  [back_demod 66 demod (168)]
203 f(x,f(y,z,f(x,y,u)),f(x,v,w)) = f(x,f(y,z,u),f(x,w,f(x,y,v))).  [back_demod 159 demod (172 56 172 197) flip a]
205 f(x,f(y,z,u),f(x,y,v)) = f(x,y,f(x,v,f(y,z,u))).  [back_demod 171 demod (203 13 9)]
209 f(x,y,f(z,x,f(z,y,u))) = f(z,x,f(z,y,f(x,y,u))).  [back_demod 121 demod (205) flip a]
217 f(f(x,y,z),f(y,z,u),f(y,v,f(x,y,z))) = f(v,f(x,y,z),f(y,z,f(x,y,u))).  [para (25 (a 1) 24 (a 1 3)) demod (8 9 30 9 20 9) flip a]
219 f(x,y,f(x,z,f(y,u,f(x,z,y)))) = f(x,y,f(z,u,f(x,z,y))).  [back_demod 64 demod (8 (R) 9 8 (R) 9 107 9 8 (R) 9)]
234 f(f(x,y,z),f(y,z,u),f(y,f(y,z,u),f(z,f(x,y,z),f(y,z,u)))) = f(y,z,f(x,u,f(y,z,u))).  [para (11 (a 1) 56 (a 2)) demod (8 8 8 8 8 8 8 8 (R) 9 8 8)]
310 f(x,f(y,x,z),f(y,x,u)) = f(x,u,f(y,x,z)).  [para (77 (a 1) 8 (a 2)) demod (8 8 8 8 (R) 9)]
319 f(x,f(x,y,z),f(y,u,f(x,y,z))) = f(x,y,z).  [para (48 (a 1) 77 (a 1 3)) demod (9 8 7 9) flip a]
325 f(f(x,y,z),f(x,u,f(x,y,z)),f(x,y,f(x,z,v))) = f(v,f(x,y,z),f(x,u,f(x,y,z))).  [para (39 (a 2) 77 (a 1 3)) demod (9 8 8 9)]
347 f(x,f(y,z,u),f(z,v,f(y,z,u))) = f(z,f(y,z,u),f(y,v,x)).  [para (77 (a 1) 77 (a 1 2)) demod (8 (R) 9 8 (R) 9 57 8 8 310) flip a]
349 f(x,y,f(z,u,f(x,y,z))) = f(x,z,f(x,y,f(y,z,u))).  [back_demod 200 demod (8 (R) 9 8 (R) 9 172 48 8 (R) 9 8 (R) 9) flip a]
350 f(x,y,f(z,u,f(x,y,u))) = f(x,y,u).  [back_demod 234 demod (319 13) flip a]
353 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z).  [para (350 (a 1) 8 (a 1)) demod (8 (R) 9 8 8) flip a]
391 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y).  [back_demod 349 demod (353) flip a]
392 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z).  [back_demod 219 demod (9 142 9 9 353)]
394 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y).  [back_demod 209 demod (8 (R) 9 8 (R) 9 392 8 (R) 9 8 (R) 9) flip a]
398 f(x,f(y,z,u),f(x,v,f(x,y,u))) = f(x,v,f(x,y,u)).  [para (353 (a 1) 10 (a 2 3)) demod (9 8 8 203 9 8 (R) 9)]
401 f(x,y,f(z,x,y)) = f(z,x,y).  [para (353 (a 1) 15 (a 1)) demod (48 8 (R) 9) flip a]
412 f(x,f(y,z,u),f(z,u,f(y,z,v))) = f(z,u,f(y,z,f(y,v,x))).  [back_demod 137 demod (401 217)]
416 f(f(x,y,z),f(x,y,u),f(v,f(x,y,z),f(x,y,w))) = f(v,f(x,y,z),f(x,y,f(z,u,w))).  [para (26 (a 1) 10 (a 2 3)) demod (8 9)]
418 f(f(x,y,z),f(x,u,f(x,y,v)),f(x,y,w)) = f(x,y,f(z,w,f(x,u,v))).  [para (10 (a 1) 26 (a 1 2)) demod (9 8 (R) 9 8 (R) 9 8 9)]
419 f(f(x,y,z),f(x,y,u),f(x,v,f(x,y,w))) = f(x,y,f(z,u,f(x,v,w))).  [para (10 (a 1) 26 (a 1 3)) demod (9 8 (R) 9 8 (R) 9 8)]
420 f(f(x,y,f(x,z,u)),f(x,z,v),f(x,z,w)) = f(x,z,f(v,w,f(x,y,u))).  [para (10 (a 2) 26 (a 1 1)) demod (8 (R) 9 8 (R) 9 8 (R) 9 9 8 (R) 9)]
428 f(x,y,f(z,u,f(x,v,y))) = f(x,y,f(v,z,u)).  [para (20 (a 1) 26 (a 1 1)) demod (28) flip a]
434 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)).  [para (39 (a 2) 26 (a 2)) demod (13 8 (R) 310)]
452 f(x,y,f(z,u,f(x,v,f(x,y,w)))) = f(x,y,f(z,u,f(x,v,w))).  [para (50 (a 1) 26 (a 1 1)) demod (420) flip a]
468 f(x,f(y,z,u),f(y,z,f(y,u,v))) = f(y,z,f(u,v,f(y,u,x))).  [back_demod 198 demod (416 9 401 419 9)]
469 f(x,f(y,z,u),f(y,v,f(y,z,u))) = f(y,z,f(u,v,f(y,u,x))).  [back_demod 325 demod (418 9 310) flip a]
473 f(x,y,f(z,u,f(x,v,z))) = f(x,y,f(x,z,f(y,v,u))).  [back_demod 162 demod (469 9 48 428)]
509 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(v,z,u)).  [para (401 (a 1) 26 (a 1 1)) demod (27) flip a]
523 f(x,f(y,z,u),f(x,z,f(z,v,f(y,z,u)))) = f(y,z,f(x,z,u)).  [para (15 (a 1) 391 (a 2)) demod (9)]
547 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y).  [para (8 (a 1) 394 (a 1)) demod (8 (R) 9 8 9 8 8)]
568 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z).  [para (394 (a 1) 26 (a 2)) demod (13 8 9 310 9)]
575 f(x,f(y,z,x),f(z,x,u)) = f(z,x,f(y,x,u)).  [para (13 (a 1) 27 (a 1 3)) demod (8 9)]
598 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)).  [para (434 (a 1) 8 (a 2)) demod (9 8) flip a]
624 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)).  [para (434 (a 1) 547 (a 2)) demod (9 8 (R) 9 523 8) flip a]
636 f(f(x,y,f(y,z,u)),f(y,v,f(x,y,z)),f(y,w,f(x,y,z))) = f(y,f(x,y,z),f(u,v,w)).  [para (10 (a 1) 28 (a 1 1)) demod (9 9)]
664 f(x,f(y,x,z),f(u,v,f(x,z,w))) = f(x,f(y,x,z),f(w,u,v)).  [para (77 (a 1) 28 (a 1 1)) demod (8 (R) 9 9 9 9 9 636 9 8 (R) 9 8 8) flip a]
690 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x).  [para (568 (a 1) 8 (a 2)) demod (9 8 9)]
691 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u).  [para (8 (a 1) 568 (a 1 2)) demod (8 (R) 9 8 (R) 9)]
704 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u).  [para (15 (a 1) 568 (a 1 2)) demod (8 (R) 9 8 8 8 8)]
748 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)).  [para (598 (a 1) 8 (a 2)) demod (9 8)]
752 f(x,f(y,z,u),f(y,z,f(z,u,v))) = f(z,f(y,z,u),f(y,x,v)).  [para (15 (a 1) 598 (a 1 3)) demod (8 8 8 (R) 9 9 347)]
753 f(x,f(y,x,z),f(u,v,f(y,x,z))) = f(x,f(y,x,z),f(y,u,v)).  [para (39 (a 1) 598 (a 1 3)) demod (9 8 (R) 9 752 8) flip a]
758 f(x,f(y,x,z),f(y,u,v)) = f(x,z,f(y,x,f(y,u,v))).  [para (24 (a 1) 598 (a 1 3)) demod (8 (R) 9 412 9 8 753 664 8 8) flip a]
774 f(x,y,f(z,x,f(z,u,f(z,y,v)))) = f(z,x,y).  [para (568 (a 1) 598 (a 1 3)) demod (8 (R) 13 8 753 758) flip a]
779 f(x,f(y,z,u),f(y,z,f(z,u,v))) = f(z,f(y,z,u),f(x,y,v)).  [back_demod 752 demod (8 (R) 9)]
783 f(x,f(y,z,u),f(z,v,f(y,z,u))) = f(z,f(y,z,u),f(x,y,v)).  [back_demod 347 demod (8)]
788 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)).  [para (624 (a 1) 8 (a 2)) demod (9 8)]
792 f(x,f(y,x,z),f(u,v,f(y,x,z))) = f(x,z,f(y,x,f(y,u,v))).  [para (15 (a 1) 624 (a 1 3)) demod (8 8 8 (R) 9 779 8 (R) 9 758 8) flip a]
818 f(x,f(y,x,f(y,z,u)),f(x,z,f(y,z,u))) = f(y,x,z).  [para (690 (a 1) 11 (a 2)) demod (8 (R) 9 7 8 9)]
835 f(x,f(y,z,x),f(u,v,f(y,z,w))) = f(x,f(y,z,x),f(y,u,v)).  [para (690 (a 1) 28 (a 1 1)) demod (9 9 53 8 8) flip a]
944 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x).  [para (691 (a 1) 8 (a 2)) demod (8 8 8 8 8)]
1016 f(x,f(y,x,z),f(u,y,v)) = f(x,z,f(y,x,f(u,y,v))).  [para (10 (a 1) 748 (a 1 3)) demod (779 792 8 (R) 9)]
1021 f(x,f(y,z,u),f(y,z,f(v,z,u))) = f(z,u,f(y,z,f(v,y,x))).  [para (15 (a 1) 748 (a 2 3)) demod (8 (R) 9 783 1016) flip a]
1028 f(x,y,f(z,x,f(u,z,y))) = f(z,x,y).  [para (401 (a 1) 748 (a 1 3)) demod (13 792 8 (R) 9) flip a]
1200 f(x,f(y,z,x),f(u,y,z)) = f(y,z,x).  [para (401 (a 1) 788 (a 1 3)) demod (13 835 8 (R) 9) flip a]
1418 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z).  [back_demod 818 demod (8 (R) 9 172 391 8 (R) 9)]
1424 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u).  [para (8 (a 1) 944 (a 1 2)) demod (8 9 8 9)]
1770 f(f(x,y,f(z,u,v)),f(z,v,f(y,u,v)),f(z,u,f(y,u,v))) = f(y,f(z,u,v),f(x,u,v)).  [para (748 (a 1) 34 (a 1 2))]
1876 f(x,f(x,y,z),f(u,v,w)) = f(x,y,f(x,z,f(u,v,w))).  [para (14 (a 1) 35 (a 1 2)) demod (9 419 9 28) flip a]
1921 f(x,y,f(x,z,f(u,v,f(y,z,w)))) = f(x,y,f(z,v,f(x,u,z))).  [para (691 (a 1) 35 (a 1 2)) demod (469 428 8 8 452 9 8 8 9 1876) flip a]
2054 f(x,f(y,z,u),f(v,w,f(z,u,f(x,y,z)))) = f(x,f(y,z,u),f(z,v,w)).  [para (598 (a 2) 428 (a 1 3 3))]
2294 f(x,y,f(z,u,f(x,z,f(v,x,y)))) = f(x,y,f(x,z,f(v,y,u))).  [para (38 (a 1) 33 (a 1)) demod (48 9 468 428 8 8 1876)]
2676 f(x,y,f(z,y,f(z,u,f(x,v,z)))) = f(x,z,y).  [para (704 (a 1) 34 (a 2)) demod (7 1876 1021 8 7 8 1876)]
2837 f(x,f(y,z,u),f(x,z,f(z,v,f(z,w,f(y,z,u))))) = f(y,z,f(x,z,u)).  [para (10 (a 1) 774 (a 2)) demod (9 8 (R) 9 8)]
2894 f(x,y,f(z,y,f(x,u,f(z,x,v)))) = f(z,x,y).  [para (774 (a 1) 774 (a 2)) demod (8 (R) 9 8 (R) 9 9 8 (R) 9 2837 8)]
5415 f(x,f(y,z,f(x,u,v)),f(y,v,f(x,u,v))) = f(x,v,f(y,u,z)).  [para (1418 (a 1) 2676 (a 1 3)) demod (9 8 (R) 9 9 428 8 (R) 9)]
5512 f(x,y,f(y,z,f(u,x,z))) = f(x,y,z).  [para (568 (a 1) 62 (a 1 3)) demod (8 (R) 9 8 (R) 9 48 8 (R) 9 13 8 (R) 9 1876 1921 8 (R) 9 8 (R) 9) flip a]
5644 f(x,f(y,z,u),f(u,v,f(z,u,f(y,z,x)))) = f(x,f(z,u,v),f(y,z,u)).  [para (575 (a 1) 5512 (a 1 3 3)) demod (1021 8 (R) 9 8 (R))]
5914 f(x,f(y,z,f(u,v,w)),f(x,f(y,v6,f(u,v,w)),f(v7,f(y,z,f(u,v,w)),f(y,f(u,v,w),f(z,u,v6))))) = f(x,f(y,v6,f(u,v,w)),f(y,z,f(u,v,w))).  [para (63 (a 1) 2894 (a 1 3 3 3)) demod (8 (R) 9 8 9 8 (R) 9 8 (R) 9 8 (R) 9 8 (R) 9 8)]
10465 f(x,f(y,z,u),f(z,u,f(y,x,v))) = f(z,u,f(y,x,v)).  [para (1200 (a 1) 109 (a 1 2)) demod (27 48) flip a]
10512 f(x,y,f(x,z,f(u,v,f(y,w,z)))) = f(x,y,f(x,z,f(u,y,v))).  [para (398 (a 1) 33 (a 1 2)) demod (1424 1424 1424 469 428 8 8 2294 1424 9 1876) flip a]
11169 f(x,f(y,z,u),f(v,y,z)) = f(y,z,f(v,x,u)).  [para (11 (a 1) 473 (a 2 3)) demod (8 8 8 8 8 (R) 1876 509 8 (R) 9 758 48 1028 8 (R) 9 8 (R) 9 10465)]
11483 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)).  [back_demod 5644 demod (8 2054 11169 8 (R) 9)]
11934 f(x,f(y,z,u),f(y,u,v)) = f(y,u,f(x,z,v)).  [para (8 (a 2) 11169 (a 1 2)) demod (8 9 8 8 8 (R) 9)]
12105 f(x,f(y,z,f(u,v,w)),f(y,v6,f(u,v,w))) = f(y,f(u,v,w),f(x,v6,z)).  [back_demod 5914 demod (11934 8 (R) 9 11934 11934 10512 7 9 48) flip a]
12368 f(x,f(y,z,u),f(y,v,u)) = f(y,u,f(x,v,z)).  [back_demod 5415 demod (12105 9 9)]
12400 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(v,x,y)).  [back_demod 1770 demod (12368 8 8 509 8 8 11483 8 (R) 9 401) flip a]
12501 $F # answer(dist_short).  [back_demod 12 demod (12400 8 8) xx a]

-------- end of proof  -------

Given=194. Generated=191817. Kept=12494. Proofs=1.
Usable=123. Sos=6556. Demods=4541. Goals=0. Limbo=101, Disabled=5720. Hints=0.
Weight_deleted=1012. Literals_deleted=0.
Forward_subsumed=159407. Back_subsumed=303.
Sos_limit_deleted=18903. Sos_displaced=0. Sos_removed=0.
New_demodulators=9748 (2 lex), Back_demodulated=5411. Back_unit_deleted=0.
Demod_attempts=3902654. Demod_rewrites=1424919.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=14.56.
User_CPU=56.84, System_CPU=0.08, Wall_clock=58.

THEOREM PROVED

Exiting with 1 proof.

Process 14885 exit (max_proofs) Fri Jul 22 15:33:04 2005