============================== Prover9 ===============================
Prover9 (32) version June-2007, June 2007.
Process 1793 was started by mccune on iflo.local,
Sat Jun 30 03:10:56 2007
The command was "./prover9 -f p2.in".
============================== end of head ===========================
Multiple: <->
Multiple: ->
Multiple: <-
Multiple: !=
Multiple: ==
Multiple: <=
Multiple: >=

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

% Reading from file p2.in

redeclare(false,FFAALLSSEE).
redeclare(equality,==).
    % op(700, infix, ==).
redeclare(negated_equality,"=/=").
Multiple: =/=
    % op(700, infix, =/=).

formulas(assumptions).
1 * x == x.
x * 1 == x.
i(x) * x == 1.
x * i(x) == 1.
i(x) * (x * y) == y.
(y * x) * i(x) == y.
i(x * y) == i(y) * i(x).
((x * y) * x) * z == x * (y * (x * z)).
(x * y) * (z * x) == x * ((y * z) * x).
((z * x) * y) * x == z * (x * (y * x)).
C * x == x * C.
C * (C * C) == D.
D * (A * B) =/= (D * A) * B.
end_of_list.

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

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:

============================== end of process non-clausal formulas ===

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

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
1 * x == x.  [assumption].
x * 1 == x.  [assumption].
i(x) * x == 1.  [assumption].
x * i(x) == 1.  [assumption].
i(x) * (x * y) == y.  [assumption].
(x * y) * i(y) == x.  [assumption].
i(x * y) == i(y) * i(x).  [assumption].
((x * y) * x) * z == x * (y * (x * z)).  [assumption].
(x * y) * (z * x) == x * ((y * z) * x).  [assumption].
((x * y) * z) * y == x * (y * (z * y)).  [assumption].
C * x == x * C.  [assumption].
C * (C * C) == D.  [assumption].
D * (A * B) =/= (D * A) * B.  [assumption].
end_of_list.

formulas(demodulators).
end_of_list.

============================== PREDICATE ELIMINATION =================

No predicates eliminated.

============================== end predicate elimination =============

Auto_denials:  (no changes).

Term ordering decisions:
Predicate symbol precedence:  predicate_order([ == ]).
Function symbol precedence:  function_order([ C, 1, D, A, B, *, i ]).
After inverse_order: Function symbol precedence:  function_order([ C, 1, D, A, B, *, i ]).
Unfolding symbols: D/0.

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

Auto_process settings:  (no changes).

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
1 1 * x == x.  [assumption].
2 x * 1 == x.  [assumption].
3 i(x) * x == 1.  [assumption].
4 x * i(x) == 1.  [assumption].
5 i(x) * (x * y) == y.  [assumption].
6 (x * y) * i(y) == x.  [assumption].
7 i(x * y) == i(y) * i(x).  [assumption].
8 ((x * y) * x) * z == x * (y * (x * z)).  [assumption].
9 (x * y) * (z * x) == x * ((y * z) * x).  [assumption].
10 ((x * y) * z) * y == x * (y * (z * y)).  [assumption].
11 C * x == x * C.  [assumption].
13 D == C * (C * C).  [copy(12),flip(a)].
15 ((C * (C * C)) * A) * B =/= (C * (C * C)) * (A * B).  [copy(14),rewrite([13(1),13(10)]),flip(a)].
end_of_list.

formulas(demodulators).
1 1 * x == x.  [assumption].
2 x * 1 == x.  [assumption].
3 i(x) * x == 1.  [assumption].
4 x * i(x) == 1.  [assumption].
5 i(x) * (x * y) == y.  [assumption].
6 (x * y) * i(y) == x.  [assumption].
7 i(x * y) == i(y) * i(x).  [assumption].
8 ((x * y) * x) * z == x * (y * (x * z)).  [assumption].
10 ((x * y) * z) * y == x * (y * (z * y)).  [assumption].
11 C * x == x * C.  [assumption].
        % (lex-dep)
13 D == C * (C * C).  [copy(12),flip(a)].
end_of_list.

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

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

% Starting search at 0.01 seconds.

given #1 (I,wt=5): 1 1 * x == x.  [assumption].

given #2 (I,wt=5): 2 x * 1 == x.  [assumption].

given #3 (I,wt=6): 3 i(x) * x == 1.  [assumption].

given #4 (I,wt=6): 4 x * i(x) == 1.  [assumption].

given #5 (I,wt=8): 5 i(x) * (x * y) == y.  [assumption].

given #6 (I,wt=8): 6 (x * y) * i(y) == x.  [assumption].

given #7 (I,wt=10): 7 i(x * y) == i(y) * i(x).  [assumption].

given #8 (I,wt=15): 8 ((x * y) * x) * z == x * (y * (x * z)).  [assumption].

given #9 (I,wt=15): 9 (x * y) * (z * x) == x * ((y * z) * x).  [assumption].

given #10 (I,wt=15): 10 ((x * y) * z) * y == x * (y * (z * y)).  [assumption].

given #11 (I,wt=7): 11 C * x == x * C.  [assumption].

given #12 (I,wt=7): 13 D == C * (C * C).  [copy(12),flip(a)].

given #13 (A,wt=4): 16 i(1) == 1.  [para(3(a,1),2(a,1)),flip(a)].

given #14 (F,wt=19): 45 (C * (C * (C * A))) * B =/= C * (C * (C * (A * B))).  [back_rewrite(15),rewrite([41(7),41(18)])].

given #15 (T,wt=5): 17 i(i(x)) == x.  [para(3(a,1),5(a,1,2)),rewrite([2(4)])].

given #16 (T,wt=8): 27 (x * i(y)) * y == x.  [para(3(a,1),8(a,2,2)),rewrite([7(2),25(5),18(4),2(5)])].

given #17 (T,wt=8): 70 x * (i(x) * y) == y.  [para(4(a,1),10(a,1,1)),rewrite([1(2),7(2),48(5)]),flip(a)].

given #18 (T,wt=8): 92 i(C) * (x * C) == x.  [para(11(a,1),5(a,1,2))].

given #19 (A,wt=11): 20 (i(x) * i(y)) * (y * x) == 1.  [para(7(a,1),3(a,1,1))].

given #20 (T,wt=8): 93 i(x) * (C * x) == C.  [para(11(a,2),5(a,1,2))].

given #21 (T,wt=8): 94 (x * C) * i(x) == C.  [para(11(a,1),6(a,1,1))].

given #22 (T,wt=8): 95 (C * x) * i(C) == x.  [para(11(a,2),6(a,1,1))].

given #23 (T,wt=8): 118 C * (x * i(C)) == x.  [para(27(a,1),11(a,2))].

given #24 (A,wt=11): 21 (x * y) * (i(y) * i(x)) == 1.  [para(7(a,1),4(a,1,2))].

given #25 (T,wt=8): 126 x * (C * i(x)) == C.  [para(11(a,2),70(a,1,2))].

given #26 (T,wt=9): 133 i(C) * x == x * i(C).  [para(27(a,1),92(a,1,2))].

given #27 (T,wt=10): 127 x * (i(C) * i(x)) == i(C).  [para(92(a,1),6(a,1,1)),rewrite([7(3)])].

given #28 (T,wt=10): 145 (i(x) * i(C)) * x == i(C).  [para(93(a,1),7(a,1,1)),rewrite([7(5),17(8)]),flip(a)].

given #29 (A,wt=13): 22 (i(x) * i(y)) * ((y * x) * z) == z.  [para(7(a,1),5(a,1,1))].

given #30 (T,wt=10): 178 (x * i(C)) * i(x) == i(C).  [para(126(a,1),7(a,1,1)),rewrite([7(6),17(4)]),flip(a)].

given #31 (T,wt=10): 186 i(x) * (i(C) * x) == i(C).  [para(133(a,2),5(a,1,2))].

given #32 (T,wt=11): 24 (x * x) * y == x * (x * y).  [para(1(a,1),8(a,2,2)),rewrite([2(2)])].

given #33 (T,wt=11): 25 (x * y) * x == x * (y * x).  [para(8(a,1),2(a,1)),rewrite([2(2)]),flip(a)].

given #34 (A,wt=13): 23 (x * (y * z)) * (i(z) * i(y)) == x.  [para(7(a,1),6(a,1,2))].

given #35 (T,wt=11): 68 (x * y) * y == x * (y * y).  [para(1(a,1),10(a,2,2,2)),rewrite([2(3)])].

given #36 (T,wt=11): 141 (i(x) * i(C)) * (x * C) == 1.  [para(11(a,1),20(a,1,2))].

given #37 (T,wt=11): 142 (i(C) * i(x)) * (C * x) == 1.  [para(11(a,2),20(a,1,2))].

given #38 (T,wt=11): 143 (x * i(y)) * (y * i(x)) == 1.  [para(17(a,1),20(a,1,1,1))].

given #39 (A,wt=18): 31 i(x) * ((x * y) * (i(x) * z)) == (y * i(x)) * z.  [para(5(a,1),8(a,1,1,1)),flip(a)].

given #40 (T,wt=11): 144 (i(x) * y) * (i(y) * x) == 1.  [para(17(a,1),20(a,1,1,2))].

given #41 (T,wt=11): 176 (x * C) * (i(x) * i(C)) == 1.  [para(11(a,1),21(a,1,1))].

given #42 (T,wt=11): 177 (C * x) * (i(C) * i(x)) == 1.  [para(11(a,2),21(a,1,1))].

given #43 (T,wt=11): 259 C * (x * x) == x * (x * C).  [para(24(a,1),11(a,2))].

given #44 (A,wt=16): 33 (x * (y * (x * z))) * i(z) == x * (y * x).  [para(8(a,1),6(a,1,1)),rewrite([25(7)])].

given #45 (T,wt=11): 261 C * (x * x) == x * (C * x).  [para(11(a,2),24(a,2,2)),rewrite([11(3,R)])].

given #46 (T,wt=11): 322 C * (x * C) == x * (C * C).  [para(68(a,1),11(a,2))].

given #47 (T,wt=11): 323 C * (C * x) == x * (C * C).  [para(11(a,2),68(a,1,1)),rewrite([11(4,R)])].

given #48 (T,wt=11): 485 x * (C * y) == x * (y * C).  [back_rewrite(164),rewrite([398(6),70(12),109(8),70(6)])].

given #49 (A,wt=20): 34 (x * (x * y)) * z == (x * y) * (i(y) * ((x * y) * z)).  [para(6(a,1),8(a,1,1,1))].

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

% Proof 1 at 0.66 (+ 0.10) seconds.
% Length of proof is 17.
% Level of proof is 5.
% Maximum clause weight is 20.
% Given clauses 49.

2 x * 1 == x.  [assumption].
6 (x * y) * i(y) == x.  [assumption].
8 ((x * y) * x) * z == x * (y * (x * z)).  [assumption].
9 (x * y) * (z * x) == x * ((y * z) * x).  [assumption].
11 C * x == x * C.  [assumption].
12 C * (C * C) == D.  [assumption].
13 D == C * (C * C).  [copy(12),flip(a)].
14 D * (A * B) =/= (D * A) * B.  [assumption].
15 ((C * (C * C)) * A) * B =/= (C * (C * C)) * (A * B).  [copy(14),rewrite([13(1),13(10)]),flip(a)].
25 (x * y) * x == x * (y * x).  [para(8(a,1),2(a,1)),rewrite([2(2)]),flip(a)].
34 (x * (x * y)) * z == (x * y) * (i(y) * ((x * y) * z)).  [para(6(a,1),8(a,1,1,1))].
41 (x * (y * x)) * z == x * (y * (x * z)).  [back_rewrite(8),rewrite([25(2)])].
45 (C * (C * (C * A))) * B =/= C * (C * (C * (A * B))).  [back_rewrite(15),rewrite([41(7),41(18)])].
102 (C * x) * (C * y) == C * (C * (x * y)).  [para(11(a,2),9(a,1,2)),rewrite([11(9,R)])].
828 (C * x) * (i(x) * ((C * x) * y)) == C * (x * (C * y)).  [para(11(a,1),34(a,1,1,2)),rewrite([41(5)]),flip(a)].
829 (C * (C * x)) * y == C * (x * (C * y)).  [para(11(a,1),34(a,1,1)),rewrite([11(4,R),828(13)])].
938 FFAALLSSEE.  [back_rewrite(45),rewrite([829(9),102(8)]),xx(a)].

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

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

Given=49. Generated=2872. Kept=935. proofs=1.
Usable=41. Sos=602. Demods=480. Limbo=109, Disabled=196. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=1936. Back_subsumed=17.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=614 (11 lex), Back_demodulated=166. Back_unit_deleted=0.
Demod_attempts=47095. Demod_rewrites=6972.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=1.00.
User_CPU=0.66, System_CPU=0.10, Wall_clock=1.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 1793 exit (max_proofs) Sat Jun 30 03:10:57 2007
