----- Prover9 July-2005D, 18 July 2005 -----
Process 14304 was started by mccune on theorem.mcs.anl.gov,
Fri Jul 22 14:47:28 2005
The command was "prover9 -f 2basis.in".

% Reading from file 2basis.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).

clauses(sos).
f(x,x,y) = x # label(majority).
f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2).
f(A,B,C) != f(C,A,B) | f(A,B,C) != f(A,C,B) # answer(2a_2b).
end_of_list.

% Finished reading the input.

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

% Predicate elimination: (none).
% Function symbol KB weights:  A=1. B=1. C=1. f=1.
% Relation symbol precedence:  lex([ = ]).
% Function symbol precedence:  lex([ A, B, C, 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).
  % set(hyper_resolution).  % (nonunit Horn with equality)
  % set(neg_ur_resolution).  % (nonunit Horn with equality)
  % assign(para_lit_limit, 2).  % (nonunit Horn with equality)

% Reasonable options, based on the structure of the clauses:
  % set(back_unit_deletion), because Horn and neg nonunits.
    % set(back_unit_deletion) -> set(unit_deletion).

% Clauses after input processing:

clauses(usable).
end_of_list.

clauses(sos).
4 f(x,x,y) = x # label(majority).  [input]
5 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2).  [input]
6 f(C,A,B) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b).  [copy 3 flip a flip b]
end_of_list.

clauses(demodulators).
4 f(x,x,y) = x # label(majority).  [input]
5 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2).  [input]
end_of_list.

clauses(goals).
end_of_list.

% Starting search at 0.01 seconds.

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

given #2 (wt=15): 5 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2).  [input]

given #3 (wt=18): 6 f(C,A,B) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b).  [copy 3 flip a flip b]

given #4 (wt=6): 8 f(x,y,x) = x.  [para (4 (a 1) 5 (a 1 1)) demod (4)]

given #5 (wt=12): 10 f(x,y,f(x,z,y)) = f(y,z,x).  [para (8 (a 1) 5 (a 1 1)) flip a]

given #6 (wt=15): 7 f(x,y,f(x,f(y,x,z),z)) = f(y,x,z).  [para (5 (a 1) 4 (a 1))]

given #7 (wt=6): 11 f(x,y,y) = y.  [para (4 (a 1) 10 (a 1 3)) demod (8) flip a]

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

given #9 (wt=18): 12 f(x,y,f(x,z,f(y,u,x))) = f(f(x,u,y),z,x).  [para (10 (a 1) 5 (a 1 1)) flip a]

given #10 (wt=12): 34 f(f(x,y,z),x,z) = f(z,y,x).  [para (19 (a 1) 12 (a 1 3)) demod (11 10) flip a]

given #11 (wt=21): 13 f(f(x,y,z),y,f(y,x,f(y,u,z))) = f(y,u,f(x,y,z)).  [para (5 (a 1) 10 (a 1 3))]

given #12 (wt=18): 72 f(B,A,C) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b).  [back_demod 6 demod (51)]

given #13 (wt=9): 51 f(x,y,z) = f(z,y,x).  [back_demod 19 demod (39 44 10)]

given #14 (wt=12): 44 f(x,y,f(y,z,x)) = f(x,z,y).  [para (19 (a 1) 34 (a 2)) demod (39 39 34 12 39)]

given #15 (wt=12): 78 f(x,y,f(z,y,x)) = f(x,y,z).  [para (11 (a 1) 13 (a 1 3)) demod (51 44 53 51 44) flip a]

given #16 (wt=24): 16 f(x,f(y,z,u),f(x,f(z,y,f(z,x,u)),z)) = f(z,y,f(z,x,u)).  [para (5 (a 1) 7 (a 1 3 2)) demod (5)]

given #17 (wt=12): 89 f(x,y,f(y,x,z)) = f(y,x,z).  [para (7 (a 1) 78 (a 2)) demod (51 7)]

given #18 (wt=12): 93 f(x,y,f(x,y,z)) = f(x,y,z).  [para (51 (a 1) 78 (a 1 3))]

given #19 (wt=12): 95 f(x,f(y,x,z),z) = f(y,x,z).  [back_demod 58 demod (89)]

given #20 (wt=12): 121 f(x,y,f(z,x,y)) = f(z,x,y).  [para (89 (a 1) 13 (a 2)) demod (93 77)]

given #21 (wt=27): 17 f(f(x,y,z),u,f(y,x,f(y,f(u,f(x,y,z),y),z))) = f(u,f(x,y,z),y).  [para (5 (a 1) 7 (a 1 3))]

given #22 (wt=12): 128 f(x,f(y,z,x),z) = f(y,z,x).  [para (95 (a 1) 10 (a 1 3)) demod (121) flip a]

given #23 (wt=12): 132 f(x,f(y,x,z),y) = f(z,x,y).  [para (51 (a 1) 95 (a 1 2))]

given #24 (wt=12): 151 f(x,f(x,y,z),y) = f(z,y,x).  [para (51 (a 1) 128 (a 1 2))]

given #25 (wt=12): 152 f(x,f(x,y,z),z) = f(x,y,z).  [para (10 (a 1) 132 (a 1 2)) demod (51 10)]

given #26 (wt=27): 46 f(f(x,y,z),z,f(f(x,y,z),u,f(z,y,x))) = f(f(z,y,x),u,f(x,y,z)).  [para (34 (a 1) 12 (a 2 1)) demod (44)]

given #27 (wt=12): 156 f(x,f(y,z,x),y) = f(y,z,x).  [para (44 (a 1) 132 (a 1 2)) demod (51 44)]

given #28 (wt=15): 52 f(x,f(x,y,z),f(z,y,x)) = f(z,y,x).  [back_demod 14 demod (51 10)]

given #29 (wt=15): 54 f(x,f(y,z,x),f(x,z,y)) = f(x,z,y).  [back_demod 31 demod (51 44)]

given #30 (wt=15): 55 f(x,y,f(z,u,x)) = f(x,y,f(x,u,z)).  [back_demod 50 demod (51 51)]

given #31 (wt=24): 56 f(f(x,y,f(x,z,u)),x,f(x,y,f(u,z,x))) = f(x,y,f(x,z,u)).  [back_demod 47 demod (51 51 12 51)]

given #32 (wt=15): 67 f(x,y,f(z,x,u)) = f(x,z,f(x,y,u)).  [back_demod 21 demod (51 13 44 51)]

given #33 (wt=9): 310 f(A,C,B) != f(A,B,C) # answer(2a_2b).  [back_demod 72 demod (219) xx a]

given #34 (wt=9): 219 f(x,y,z) = f(y,x,z).  [para (11 (a 1) 67 (a 2 3)) demod (121)]

-------- Proof 1 -------- (0.10 + 0.00 seconds) 2a_2b.

-------- PROOF --------
Length of proof is 30.
Maximum clause weight is 27.
3 f(A,B,C) != f(C,A,B) | f(A,B,C) != f(A,C,B) # answer(2a_2b).  [input]
4 f(x,x,y) = x # label(majority).  [input]
5 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2).  [input]
6 f(C,A,B) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b).  [copy 3 flip a flip b]
7 f(x,y,f(x,f(y,x,z),z)) = f(y,x,z).  [para (5 (a 1) 4 (a 1))]
8 f(x,y,x) = x.  [para (4 (a 1) 5 (a 1 1)) demod (4)]
10 f(x,y,f(x,z,y)) = f(y,z,x).  [para (8 (a 1) 5 (a 1 1)) flip a]
11 f(x,y,y) = y.  [para (4 (a 1) 10 (a 1 3)) demod (8) flip a]
12 f(x,y,f(x,z,f(y,u,x))) = f(f(x,u,y),z,x).  [para (10 (a 1) 5 (a 1 1)) flip a]
13 f(f(x,y,z),y,f(y,x,f(y,u,z))) = f(y,u,f(x,y,z)).  [para (5 (a 1) 10 (a 1 3))]
14 f(x,f(x,y,z),f(z,y,x)) = f(f(x,y,z),z,x).  [para (10 (a 1) 10 (a 1 3))]
19 f(x,y,f(f(x,z,y),y,x)) = f(x,z,y).  [para (10 (a 1) 7 (a 1 3 2)) demod (14 10)]
21 f(f(x,y,z),y,f(f(y,x,f(y,u,z)),y,f(x,y,z))) = f(y,x,f(y,u,z)).  [para (5 (a 1) 19 (a 1 3 1)) demod (5)]
34 f(f(x,y,z),x,z) = f(z,y,x).  [para (19 (a 1) 12 (a 1 3)) demod (11 10) flip a]
38 f(f(x,y,z),z,f(z,y,x)) = f(z,x,f(x,y,z)).  [para (34 (a 1) 10 (a 1 3))]
39 f(f(x,y,z),z,x) = f(x,z,f(z,y,x)).  [para (10 (a 1) 34 (a 1 1)) demod (38) flip a]
44 f(x,y,f(y,z,x)) = f(x,z,y).  [para (19 (a 1) 34 (a 2)) demod (39 39 34 12 39)]
51 f(x,y,z) = f(z,y,x).  [back_demod 19 demod (39 44 10)]
53 f(f(x,y,z),z,f(z,y,x)) = f(z,y,x).  [back_demod 38 demod (44)]
67 f(x,y,f(z,x,u)) = f(x,z,f(x,y,u)).  [back_demod 21 demod (51 13 44 51)]
72 f(B,A,C) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b).  [back_demod 6 demod (51)]
77 f(f(x,y,z),y,f(y,x,z)) = f(y,z,f(x,y,z)).  [para (11 (a 1) 13 (a 1 3 3))]
78 f(x,y,f(z,y,x)) = f(x,y,z).  [para (11 (a 1) 13 (a 1 3)) demod (51 44 53 51 44) flip a]
89 f(x,y,f(y,x,z)) = f(y,x,z).  [para (7 (a 1) 78 (a 2)) demod (51 7)]
93 f(x,y,f(x,y,z)) = f(x,y,z).  [para (51 (a 1) 78 (a 1 3))]
121 f(x,y,f(z,x,y)) = f(z,x,y).  [para (89 (a 1) 13 (a 2)) demod (93 77)]
219 f(x,y,z) = f(y,x,z).  [para (11 (a 1) 67 (a 2 3)) demod (121)]
310 f(A,C,B) != f(A,B,C) # answer(2a_2b).  [back_demod 72 demod (219) xx a]
326 f(x,y,z) = f(x,z,y).  [para (219 (a 1) 44 (a 1 3)) demod (78)]
327 $F # answer(2a_2b).  [resolve (326 a 310 a)]

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

Given=34. Generated=2035. Kept=323. Proofs=1.
Usable=16. Sos=151. Demods=140. Goals=0. Limbo=1, Disabled=157. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=1712. Back_subsumed=1.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=287 (3 lex), Back_demodulated=153. Back_unit_deleted=0.
Demod_attempts=19612. Demod_rewrites=5453.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=4. Nonunit_bsub_feature_tests=2.
Megabytes=0.28.
User_CPU=0.10, System_CPU=0.00, Wall_clock=0.

THEOREM PROVED

Exiting with 1 proof.

Process 14304 exit (max_proofs) Fri Jul 22 14:47:28 2005