============================== Prover9 ===============================
Prover9 (32) version June-2006C, June 2006.
Process 13019 was started by mccune on cleo.thornwood,
Mon Jun 19 16:40:30 2006
The command was "/home/mccune/bin/prover9 -f cg1.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file cg1.in


formulas(sos).
(all x all y all z (x * y = x * z -> y = z)).
(all x all y all z (y * x = z * x -> y = z)).
end_of_list.

clauses(sos).
(x * y) * (z * u) = (x * z) * (y * u).
end_of_list.

clauses(goals).
(x * (y * z)) * ((u * v) * w) = (x * (u * z)) * ((y * v) * w).
end_of_list.

============================== end of input ==========================

============================== PROCESS GOALS =========================

% Each goal clause was negated; the result (to be placed in sos):

clauses(negated_goals).
(c1 * (c4 * c3)) * ((c2 * c5) * c6) != (c1 * (c2 * c3)) * ((c4 * c5) * c6).
end_of_list.

============================== end of process goals ==================

============================== PROCESS INITIAL CLAUSES ===============

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 (x * y) * (z * u) = (x * z) * (y * u).  [input].
2 x * y != x * z | y = z.  [clausify].
3 x * y != z * y | x = z.  [clausify].
4 (c1 * (c4 * c3)) * ((c2 * c5) * c6) != (c1 * (c2 * c3)) * ((c4 * c5) * c6).  [clausify].
end_of_list.

clauses(demodulators).
end_of_list.

Predicate elimination: (none).

Auto_denials:  no changes.

Term ordering decisions:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ c1, c2, c3, c4, c5, c6, * ]).
After inverse_order: Function symbol precedence:  lex([ c1, c2, c3, c4, c5, c6, * ]).
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)

Auto_process settings:  no changes.

============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================

% Clauses after input processing:

clauses(usable).
end_of_list.

clauses(sos).
5 (x * y) * (z * u) = (x * z) * (y * u).  [input].
6 x * y != x * z | y = z.  [clausify].
7 x * y != z * y | x = z.  [clausify].
8 (c1 * (c2 * c3)) * ((c4 * c5) * c6) != (c1 * (c4 * c3)) * ((c2 * c5) * c6).  [copy(4),flip(a)].
end_of_list.

clauses(demodulators).
end_of_list.

clauses(denials).
end_of_list.

============================== end of clauses for search =============

============================== SEARCH ================================

% Starting search at 0.00 seconds.

given #1 (I,wt=15): 5 (x * y) * (z * u) = (x * z) * (y * u).  [input].

given #2 (I,wt=10): 6 x * y != x * z | y = z.  [clausify].

given #3 (I,wt=10): 7 x * y != z * y | x = z.  [clausify].

given #4 (I,wt=23): 8 (c1 * (c2 * c3)) * ((c4 * c5) * c6) != (c1 * (c4 * c3)) * ((c2 * c5) * c6).  [copy(4),flip(a)].

given #5 (T,wt=18): 11 (x * y) * (z * u) != (x * z) * v | y * u = v.  [para(5(a,1),6(a,1))].

given #6 (A,wt=23): 9 ((x * y) * (z * u)) * (v * w) = ((x * z) * v) * ((y * u) * w).  [para(5(a,1),5(a,1,1))].

given #7 (F,wt=23): 15 (c1 * (c4 * c5)) * ((c2 * c3) * c6) != (c1 * (c4 * c3)) * ((c2 * c5) * c6).  [para(5(a,1),8(a,1))].

given #8 (F,wt=23): 16 (c1 * (c2 * c3)) * ((c4 * c5) * c6) != (c1 * (c2 * c5)) * ((c4 * c3) * c6).  [para(5(a,1),8(a,2))].

given #9 (T,wt=18): 12 (x * y) * (z * u) != v * (y * u) | x * z = v.  [para(5(a,1),7(a,1))].

given #10 (T,wt=22): 22 (x * y) * (z * u) != (x * v) * (z * w) | y * u = v * w.  [para(5(a,1),11(a,2))].

given #11 (A,wt=23): 10 (x * (y * z)) * (u * (v * w)) = (x * u) * ((y * v) * (z * w)).  [para(5(a,1),5(a,1,2)),flip(a)].

given #12 (F,wt=23): 67 (c1 * (c4 * c5)) * ((c2 * c3) * c6) != (c1 * (c2 * c5)) * ((c4 * c3) * c6).  [para(5(a,1),15(a,2))].

given #13 (F,wt=27): 13 ((c1 * (c2 * c3)) * ((c4 * c5) * c6)) * x != ((c1 * (c4 * c3)) * ((c2 * c5) * c6)) * x.  [ur(7,b,8,a)].

given #14 (T,wt=22): 80 (x * y) * (z * u) != (v * y) * (w * u) | x * z = v * w.  [para(5(a,1),12(a,2))].

given #15 (T,wt=22): 95 (x * y) * (z * u) != (x * v) * (y * w) | z * u = v * w.  [para(5(a,1),22(a,1))].

given #16 (A,wt=27): 14 x * ((c1 * (c2 * c3)) * ((c4 * c5) * c6)) != x * ((c1 * (c4 * c3)) * ((c2 * c5) * c6)).  [ur(6,b,8,a)].

given #17 (F,wt=27): 64 ((c1 * (c4 * c5)) * ((c2 * c3) * c6)) * x != ((c1 * (c4 * c3)) * ((c2 * c5) * c6)) * x.  [ur(7,b,15,a)].

given #18 (F,wt=27): 65 x * ((c1 * (c4 * c5)) * ((c2 * c3) * c6)) != x * ((c1 * (c4 * c3)) * ((c2 * c5) * c6)).  [ur(6,b,15,a)].

given #19 (T,wt=22): 96 (x * y) * (z * u) != (x * v) * (y * w) | v * w = z * u.  [para(5(a,1),22(a,2)),flip(a)].

given #20 (T,wt=22): 209 (x * y) * (z * u) != (v * w) * (y * u) | v * w = x * z.  [para(5(a,1),80(a,1)),flip(a)].

given #21 (A,wt=31): 17 (x * (c1 * (c2 * c3))) * (y * ((c4 * c5) * c6)) != (x * y) * ((c1 * (c4 * c3)) * ((c2 * c5) * c6)).  [ur(11,b,8,a)].

given #22 (F,wt=27): 69 ((c1 * (c2 * c3)) * ((c4 * c5) * c6)) * x != ((c1 * (c2 * c5)) * ((c4 * c3) * c6)) * x.  [ur(7,b,16,a)].

given #23 (F,wt=27): 70 x * ((c1 * (c2 * c3)) * ((c4 * c5) * c6)) != x * ((c1 * (c2 * c5)) * ((c4 * c3) * c6)).  [ur(6,b,16,a)].

given #24 (T,wt=22): 263 (x * y) * (z * u) != (x * v) * (z * w) | v * w = y * u.  [para(5(a,1),96(a,1))].

given #25 (T,wt=22): 264 (x * y) * (z * u) != (x * y) * (v * w) | v * w = z * u.  [para(5(a,1),96(a,2))].

given #26 (A,wt=31): 18 (x * (c1 * (c4 * c3))) * (y * ((c2 * c5) * c6)) != (x * y) * ((c1 * (c2 * c3)) * ((c4 * c5) * c6)).  [ur(11,b,8,a(flip))].

given #27 (F,wt=27): 189 ((c1 * (c4 * c5)) * ((c2 * c3) * c6)) * x != ((c1 * (c2 * c5)) * ((c4 * c3) * c6)) * x.  [ur(7,b,67,a)].

given #28 (F,wt=27): 190 x * ((c1 * (c4 * c5)) * ((c2 * c3) * c6)) != x * ((c1 * (c2 * c5)) * ((c4 * c3) * c6)).  [ur(6,b,67,a)].

given #29 (T,wt=22): 267 (x * y) * (z * u) != (v * w) * (z * u) | v * w = x * y.  [para(5(a,1),209(a,1))].

given #30 (T,wt=22): 268 (x * y) * (z * u) != (v * y) * (w * u) | v * w = x * z.  [para(5(a,1),209(a,2))].

given #31 (A,wt=26): 19 ((x * y) * (z * u)) * (v * w) != ((x * z) * v) * v6 | (y * u) * w = v6.  [para(5(a,1),11(a,1,1))].

given #32 (F,wt=31): 63 (x * (c1 * (c4 * c5))) * (y * ((c2 * c3) * c6)) != (x * y) * ((c1 * (c4 * c3)) * ((c2 * c5) * c6)).  [ur(11,b,15,a)].

given #33 (F,wt=31): 66 (x * (c1 * (c4 * c3))) * (y * ((c2 * c5) * c6)) != (x * y) * ((c1 * (c4 * c5)) * ((c2 * c3) * c6)).  [ur(11,b,15,a(flip))].

given #34 (T,wt=23): 25 ((x * y) * z) * ((u * v) * w) = ((x * u) * z) * ((y * v) * w).  [para(9(a,1),5(a,1))].

============================== PROOF =================================

% Proof 1 at 0.12 (+ 0.00) seconds.
% Length of proof is 13.
% Level of proof is 5.
% Maximum clause weight is 47.
% Given clauses 34.

4 (c1 * (c4 * c3)) * ((c2 * c5) * c6) != (c1 * (c2 * c3)) * ((c4 * c5) * c6).  [clausify].
5 (x * y) * (z * u) = (x * z) * (y * u).  [input].
6 x * y != x * z | y = z.  [clausify].
8 (c1 * (c2 * c3)) * ((c4 * c5) * c6) != (c1 * (c4 * c3)) * ((c2 * c5) * c6).  [copy(4),flip(a)].
9 ((x * y) * (z * u)) * (v * w) = ((x * z) * v) * ((y * u) * w).  [para(5(a,1),5(a,1,1))].
10 (x * (y * z)) * (u * (v * w)) = (x * u) * ((y * v) * (z * w)).  [para(5(a,1),5(a,1,2)),flip(a)].
11 (x * y) * (z * u) != (x * z) * v | y * u = v.  [para(5(a,1),6(a,1))].
15 (c1 * (c4 * c5)) * ((c2 * c3) * c6) != (c1 * (c4 * c3)) * ((c2 * c5) * c6).  [para(5(a,1),8(a,1))].
25 ((x * y) * z) * ((u * v) * w) = ((x * u) * z) * ((y * v) * w).  [para(9(a,1),5(a,1))].
66 (x * (c1 * (c4 * c3))) * (y * ((c2 * c5) * c6)) != (x * y) * ((c1 * (c4 * c5)) * ((c2 * c3) * c6)).  [ur(11,b,15,a(flip))].
483 ((x * (y * z)) * (u * (v * w))) * ((c1 * (c4 * c5)) * ((c2 * c3) * c6)) != ((x * u) * (c1 * (c4 * c3))) * (((y * v) * (z * w)) * ((c2 * c5) * c6)).  [para(10(a,2),66(a,2,1)),flip(a)].
499 ((x * (y * z)) * u) * ((v * (w * v6)) * (v7 * v8)) = ((x * v) * u) * (((y * w) * v7) * ((z * v6) * v8)).  [para(9(a,1),25(a,1,2)),flip(a)].
500 $F.  [resolve(499,a,483,a)].

============================== end of proof ==========================

============================== STATISTICS ============================

Given=34. Generated=1365. Kept=495. proofs=1.
Usable=34. Sos=428. Demods=0. Denials=0. Limbo=15, Disabled=21. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=870. Back_subsumed=17.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
Demod_attempts=0. Demod_rewrites=0.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=13618. Nonunit_bsub_feature_tests=2543.
Megabytes=0.73.
User_CPU=0.12, System_CPU=0.00, Wall_clock=0.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 13019 exit (max_proofs) Mon Jun 19 16:40:30 2006