regulation proof

============================== Prover9 ===============================
Prover9 (32) version 2008-11A, November 2008.
Process 8186 was started by cjm on skerryvore,
Wed Aug  5 13:44:32 2009
The command was "prover9".
============================== end of head ===========================

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

formulas(sos).
A(x) -> B(x).
RA(x) <-> P(X) & (exists y A(y)) & regulates(x,y).
RB(x) <-> P(X) & (exists y B(y)) & regulates(x,y).
end_of_list.

formulas(goals).
RA(x) -> RB(x).
end_of_list.

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

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

% Formulas that are not ordinary clauses:
1 A(x) -> B(x) # label(non_clause).  [assumption].
2 RA(x) <-> P(X) & (exists y A(y)) & regulates(x,y) # label(non_clause).  [assumption].
3 RB(x) <-> P(X) & (exists y B(y)) & regulates(x,y) # label(non_clause).  [assumption].
4 RA(x) -> RB(x) # 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).
-A(x) | B(x).  [clausify(1)].
-RA(x) | P(X).  [clausify(2)].
-RA(x) | A(f1(x,y)).  [clausify(2)].
-RA(x) | regulates(x,y).  [clausify(2)].
RA(x) | -P(X) | -A(y) | -regulates(x,z).  [clausify(2)].
-RB(x) | P(X).  [clausify(3)].
-RB(x) | B(f2(x,y)).  [clausify(3)].
-RB(x) | regulates(x,y).  [clausify(3)].
RB(x) | -P(X) | -B(y) | -regulates(x,z).  [clausify(3)].
RA(c1).  [deny(4)].
-RB(c1).  [deny(4)].
end_of_list.

formulas(demodulators).
end_of_list.

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

Eliminating A/1
5 -RA(x) | A(f1(x,y)).  [clausify(2)].
6 -A(x) | B(x).  [clausify(1)].
Derived: -RA(x) | B(f1(x,y)).  [resolve(5,b,6,a)].
7 RA(x) | -P(X) | -A(y) | -regulates(x,z).  [clausify(2)].
Derived: RA(x) | -P(X) | -regulates(x,y) | -RA(z).  [resolve(7,c,5,b)].

Eliminating P/1
8 RB(x) | -P(X) | -B(y) | -regulates(x,z).  [clausify(3)].
9 -RA(x) | P(X).  [clausify(2)].
10 -RB(x) | P(X).  [clausify(3)].
Derived: RB(x) | -B(y) | -regulates(x,z) | -RA(u).  [resolve(8,b,9,b)].
Derived: RB(x) | -B(y) | -regulates(x,z) | -RB(u).  [resolve(8,b,10,b)].
11 RA(x) | -P(X) | -regulates(x,y) | -RA(z).  [resolve(7,c,5,b)].
Derived: RA(x) | -regulates(x,y) | -RA(z) | -RA(u).  [resolve(11,b,9,b)].

Eliminating regulates/2
12 RB(x) | -B(y) | -regulates(x,z) | -RA(u).  [resolve(8,b,9,b)].
13 -RA(x) | regulates(x,y).  [clausify(2)].
14 -RB(x) | regulates(x,y).  [clausify(3)].
Derived: RB(x) | -B(y) | -RA(z) | -RA(x).  [resolve(12,c,13,b)].
15 RB(x) | -B(y) | -regulates(x,z) | -RB(u).  [resolve(8,b,10,b)].
16 RA(x) | -regulates(x,y) | -RA(z) | -RA(u).  [resolve(11,b,9,b)].
Derived: RA(x) | -RA(y) | -RA(z) | -RB(x).  [resolve(16,b,14,b)].

Eliminating RB/1
17 RB(x) | -B(y) | -RA(z) | -RA(x).  [resolve(12,c,13,b)].
18 -RB(x) | B(f2(x,y)).  [clausify(3)].
19 -RB(c1).  [deny(4)].
Derived: -B(x) | -RA(y) | -RA(z) | B(f2(z,u)).  [resolve(17,a,18,a)].
Derived: -B(x) | -RA(y) | -RA(c1).  [resolve(17,a,19,a)].
20 RA(x) | -RA(y) | -RA(z) | -RB(x).  [resolve(16,b,14,b)].

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

Auto_denials:  (no changes).

Term ordering decisions:
Predicate symbol precedence:  predicate_order([ RA, B ]).
Function symbol precedence:  function_order([ c1, f1, f2 ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(neg_binary_resolution).  % (HNE depth_diff=-2)
  % clear(ordered_res).  % (HNE depth_diff=-2)
  % set(ur_resolution).  % (HNE depth_diff=-2)
    % set(ur_resolution) -> set(pos_ur_resolution).
    % set(ur_resolution) -> set(neg_ur_resolution).

Auto_process settings:
  % set(unit_deletion).  % (Horn set with negative nonunits)

kept:      21 RA(c1).  [deny(4)].
kept:      22 -RA(x) | B(f1(x,y)).  [resolve(5,b,6,a)].
kept:      23 -B(x) | -RA(y) | -RA(z) | B(f2(z,u)).  [resolve(17,a,18,a)].
           24 -B(x) | -RA(y) | -RA(c1).  [resolve(17,a,19,a)].
kept:      25 -B(x) | -RA(y).  [copy(24),unit_del(c,21)].

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
21 RA(c1).  [deny(4)].
22 -RA(x) | B(f1(x,y)).  [resolve(5,b,6,a)].
25 -B(x) | -RA(y).  [copy(24),unit_del(c,21)].
end_of_list.

formulas(demodulators).
end_of_list.

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

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

% Starting search at 0.01 seconds.

given #1 (I,wt=2): 21 RA(c1).  [deny(4)].

given #2 (I,wt=6): 22 -RA(x) | B(f1(x,y)).  [resolve(5,b,6,a)].

given #3 (I,wt=4): 25 -B(x) | -RA(y).  [copy(24),unit_del(c,21)].
-------- Proof 1 -------- 

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

% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 19.
% Level of proof is 7.
% Maximum clause weight is 6.
% Given clauses 3.

1 A(x) -> B(x) # label(non_clause).  [assumption].
2 RA(x) <-> P(X) & (exists y A(y)) & regulates(x,y) # label(non_clause).  [assumption].
3 RB(x) <-> P(X) & (exists y B(y)) & regulates(x,y) # label(non_clause).  [assumption].
4 RA(x) -> RB(x) # label(non_clause) # label(goal).  [goal].
5 -RA(x) | A(f1(x,y)).  [clausify(2)].
6 -A(x) | B(x).  [clausify(1)].
8 RB(x) | -P(X) | -B(y) | -regulates(x,z).  [clausify(3)].
9 -RA(x) | P(X).  [clausify(2)].
12 RB(x) | -B(y) | -regulates(x,z) | -RA(u).  [resolve(8,b,9,b)].
13 -RA(x) | regulates(x,y).  [clausify(2)].
17 RB(x) | -B(y) | -RA(z) | -RA(x).  [resolve(12,c,13,b)].
19 -RB(c1).  [deny(4)].
21 RA(c1).  [deny(4)].
22 -RA(x) | B(f1(x,y)).  [resolve(5,b,6,a)].
24 -B(x) | -RA(y) | -RA(c1).  [resolve(17,a,19,a)].
25 -B(x) | -RA(y).  [copy(24),unit_del(c,21)].
26 B(f1(c1,x)).  [ur(22,a,21,a)].
28 -B(x).  [resolve(25,b,21,a)].
29 $F.  [resolve(28,a,26,a)].

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

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

Given=3. Generated=7. Kept=7. proofs=1.
Usable=3. Sos=1. Demods=0. Limbo=1, Disabled=21. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=0. Back_subsumed=1.
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=0. Nonunit_bsub_feature_tests=4.
Megabytes=0.03.
User_CPU=0.01, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

THEOREM PROVED

Exiting with 1 proof.

------ process 8186 exit (max_proofs) ------

Process 8186 exit (max_proofs) Wed Aug  5 13:44:32 2009