============================== Prover9 ===============================
Prover9 (32) version 2009-02A, February 2009.
Process 15841 was started by mccune on cleo,
Wed Feb 25 12:26:11 2009
The command was "/home/mccune/bin/prover9 -f redeclare.in".
============================== end of head ===========================

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

% Reading from file redeclare.in

redeclare(true,TRUE).
redeclare(false,FALSE).
redeclare(negation,~).
  % op(350, prefix, ~).  % copying parse/print properties from - to ~
redeclare(disjunction,OR).
  % op(790, infix_right, OR).  % copying parse/print properties from | to OR
redeclare(conjunction,AND).
  % op(780, infix_right, AND).  % copying parse/print properties from & to AND
redeclare(implication,IMPLIES).
  % op(800, infix, IMPLIES).  % copying parse/print properties from -> to IMPLIES
redeclare(backward_implication,"<--").
  % op(800, infix, <--).  % copying parse/print properties from <- to <--
redeclare(equivalence,IFF).
  % op(800, infix, IFF).  % copying parse/print properties from <-> to IFF
redeclare(universal_quantification,ALL).
redeclare(existential_quantification,EXISTS).
redeclare(equality,"==").
  % op(700, infix, ==).  % copying parse/print properties from = to ==
redeclare(negated_equality,"=/=").
  % op(700, infix, =/=).  % copying parse/print properties from != to =/=
redeclare(attribute,@).
  % op(810, infix_right, @).  % copying parse/print properties from # to @

formulas(assumptions).
(x * y) * z == z * (y * z) @ label(associativity).
(EXISTS e ((ALL x e * x == x) AND (ALL x EXISTS y y * x == e))) @ label(left_identity_inverse).
end_of_list.

formulas(goals).
x * y == x * z IMPLIES y == z @ label(right_cancellation).
end_of_list.

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

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

% Formulas that are not ordinary clauses:
1 (EXISTS e ((ALL x e * x == x) AND (ALL x EXISTS y y * x == e))) @ label(left_identity_inverse) @ label(non_clause).  [assumption].
2 x * y == x * z IMPLIES y == z @ label(right_cancellation) @ label(non_clause) @ label(goal).  [goal].

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

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

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
(x * y) * z == z * (y * z) @ label(associativity).  [assumption].
c1 * x == x @ label(left_identity_inverse).  [clausify(1)].
f1(x) * x == c1 @ label(left_identity_inverse).  [clausify(1)].
c2 * c4 == c2 * c3 @ label(right_cancellation).  [deny(2)].
c4 =/= c3 @ label(right_cancellation).  [deny(2)].
end_of_list.

formulas(demodulators).
end_of_list.

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

No predicates eliminated.

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

Auto_denials:
  % copying label right_cancellation to answer in negative clause

Term ordering decisions:
Predicate symbol precedence:  predicate_order([ == ]).
Function symbol precedence:  function_order([ c1, c2, c3, c4, *, f1 ]).
After inverse_order: Function symbol precedence:  function_order([ c1, c2, c3, c4, *, f1 ]).
Unfolding symbols: (none).

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

Auto_process settings:  (no changes).

kept:      3 (x * y) * z == z * (y * z) @ label(associativity).  [assumption].
kept:      4 c1 * x == x @ label(left_identity_inverse).  [clausify(1)].
kept:      5 f1(x) * x == c1 @ label(left_identity_inverse).  [clausify(1)].
kept:      6 c2 * c4 == c2 * c3 @ label(right_cancellation).  [deny(2)].
kept:      7 c4 =/= c3 @ label(right_cancellation) @ answer(right_cancellation).  [deny(2)].

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
3 (x * y) * z == z * (y * z) @ label(associativity).  [assumption].
4 c1 * x == x @ label(left_identity_inverse).  [clausify(1)].
5 f1(x) * x == c1 @ label(left_identity_inverse).  [clausify(1)].
6 c2 * c4 == c2 * c3 @ label(right_cancellation).  [deny(2)].
7 c4 =/= c3 @ label(right_cancellation) @ answer(right_cancellation).  [deny(2)].
end_of_list.

formulas(demodulators).
3 (x * y) * z == z * (y * z) @ label(associativity).  [assumption].
        % (lex-dep)
4 c1 * x == x @ label(left_identity_inverse).  [clausify(1)].
5 f1(x) * x == c1 @ label(left_identity_inverse).  [clausify(1)].
6 c2 * c4 == c2 * c3 @ label(right_cancellation).  [deny(2)].
end_of_list.

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

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

% Starting search at 0.01 seconds.

given #1 (I,wt=11): 3 (x * y) * z == z * (y * z) @ label(associativity).  [assumption].

given #2 (I,wt=5): 4 c1 * x == x @ label(left_identity_inverse).  [clausify(1)].

given #3 (I,wt=6): 5 f1(x) * x == c1 @ label(left_identity_inverse).  [clausify(1)].

given #4 (I,wt=7): 6 c2 * c4 == c2 * c3 @ label(right_cancellation).  [deny(2)].

given #5 (I,wt=3): 7 c4 =/= c3 @ label(right_cancellation) @ answer(right_cancellation).  [deny(2)].

given #6 (A,wt=9): 14 x * (y * x) == y * x.  [para(4(a,1),3(a,1,1)),flip(a)].

given #7 (T,wt=5): 20 x * x == x.  [back_rewrite(15),rewrite([18(3),4(2)]),flip(a)].

given #8 (T,wt=5): 21 x * c1 == c1.  [para(5(a,1),14(a,1,2)),rewrite([5(4)])].

given #9 (T,wt=9): 18 (x * y) * z == y * z.  [back_rewrite(8),rewrite([14(2),14(4)])].

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

% Proof 1 at 0.01 (+ 0.00) seconds: right_cancellation.
% Length of proof is 13.
% Level of proof is 6.
% Maximum clause weight is 13.
% Given clauses 9.

1 (EXISTS e ((ALL x e * x == x) AND (ALL x EXISTS y y * x == e))) @ label(left_identity_inverse) @ label(non_clause).  [assumption].
2 x * y == x * z IMPLIES y == z @ label(right_cancellation) @ label(non_clause) @ label(goal).  [goal].
3 (x * y) * z == z * (y * z) @ label(associativity).  [assumption].
4 c1 * x == x @ label(left_identity_inverse).  [clausify(1)].
5 f1(x) * x == c1 @ label(left_identity_inverse).  [clausify(1)].
6 c2 * c4 == c2 * c3 @ label(right_cancellation).  [deny(2)].
7 c4 =/= c3 @ label(right_cancellation) @ answer(right_cancellation).  [deny(2)].
8 (x * (y * x)) * z == z * (x * z).  [para(3(a,1),3(a,1,1))].
14 x * (y * x) == y * x.  [para(4(a,1),3(a,1,1)),flip(a)].
18 (x * y) * z == y * z.  [back_rewrite(8),rewrite([14(2),14(4)])].
23 x * y == y.  [para(5(a,1),18(a,1,1)),rewrite([4(2)]),flip(a)].
25 c4 == c3.  [para(6(a,1),18(a,2)),rewrite([23(2),23(3),23(4)])].
26 FALSE @ answer(right_cancellation).  [resolve(25,a,7,a)].

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

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

Given=9. Generated=61. Kept=23. proofs=1.
Usable=8. Sos=2. Demods=10. Limbo=2, Disabled=15. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=38. Back_subsumed=0.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=12 (1 lex), Back_demodulated=10. Back_unit_deleted=0.
Demod_attempts=383. Demod_rewrites=58.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=0.04.
User_CPU=0.01, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 15841 exit (max_proofs) Wed Feb 25 12:26:11 2009
