<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
----- Otter 3.0.4, August 1995 -----
The job was started by wos on eagle.mcs.anl.gov, Mon Oct 16 16:46:37 1995
The command was "otter304".

%%%%%%%%%%%%%%%%%%%%%  Basic options

op(400, xfx, [*,+,^,v,/,\,#]).  % infix operators
op(300,yf,@).                   % postfix operator


clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).

assign(max_mem,20000).   %  Limit the memory usage in kilobytes.

%%%%%%%%%%%%%%%%%%%%%  Standard for equational problems

set(knuth_bendix).
   dependent: set(para_from).   %  Paramodulate from the chosen clause.
   dependent: set(para_into).   %  Paramodulate into the chosen clause.
   dependent: clear(para_from_right).
   dependent: clear(para_into_right).
   dependent: set(para_from_vars).
   dependent: set(eq_units_both_ways).
   dependent: set(dynamic_demod_all).
   dependent: set(dynamic_demod).   %  Adjoin demodulators during the run.
   dependent: set(order_eq).   %  Flip arguments if righthand heavier than lefthand.
   dependent: set(back_demod).  %  Apply new demodulators to retained clauses.
   dependent: set(process_input).  % Treat input clauses as if they were generated by applying an inference rule.
   dependent: set(lrpo).   %  Activate the LRPO ordering for orienting equalities and deciding dynamic demodulators.
set(ancestor_subsume).   %  Compare path lengths for derivations to the same conclusion.
WARNING: set(back_sub) flag already set.
set(back_sub).   %  Purge an existing clauses when a new clause captures such.

set(build_proof_object).
   dependent: set(order_history).   %  List ancestors in the order nucleus, clause unifying with first literal, clause unifying with second.

%%%%%%%%%%%%%%%%%%%%%  Modifications to strategy

assign(max_weight,7).  %  Disallow clauses with weight strictly greater than 7.
WARNING: assign(heat,1) already has that value.
assign(heat,1).

%  Used to direct the reasoning and to purge unwanted clauses.
weight_list(pick_and_purge).
weight(x^ (y v x)=x,2).
weight((x v y)^x=x,2).
weight((x^y) v (x^ (y^z))=x^y,2).
weight(x v (y^x)=x,2).
weight((x^y) v x=x,2).
weight(x* (y v x)=x,2).
weight((x v y)*x=x,2).
weight(x v (y*x)=x,2).
weight((x*y) v x=x,2).
weight((x v y)^y=y,2).
weight((x^y) v y=y,2).
weight(x* (y* (z v (x*y)))=x*y,2).
weight(x* (x^y)=x^y,2).
weight(x^ (x*y)=x*y,2).
weight(x^ (y*x)=y*x,2).
weight(x* (y^x)=y^x,2).
weight((x^y) v (x^ (z*y))=x^y,2).
weight((x^y) v (x*y)=x^y,2).
weight(x^y=x*y,2).
end_of_list.

%%%%%%%%%%%%%%%%%%%%%  Clauses

list(usable).
0 [] x=x.
end_of_list.

list(sos).
0 [] x^x=x.
0 [] x^y=y^x.
0 [] (x^y)^z=x^ (y^z).

0 [] x v x=x.
0 [] x v y=y v x.
0 [] (x v y) v z=x v (y v z).

0 [] x^ (x v y)=x.
0 [] x v (x^y)=x.

% add equations to make (v,*) a lattice.

0 [] x*x=x.
0 [] x*y=y*x.
0 [] (x*y)*z=x* (y*z).

0 [] x* (x v y)=x.
0 [] x v (x*y)=x.

end_of_list.

list(passive).
1 [] A^B!=A*B.
end_of_list.

list(hot).
2 [] x^x=x.
3 [] x v x=x.
end_of_list.

<h2>
Output:
</h2>

------------> process usable:
** KEPT (pick-wt=3): 4 [] x=x.
  Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] x=x.

------------> process sos:
** KEPT (pick-wt=5): 5 [] x^x=x.
---> New Demodulator: 6 [new_demod,5] x^x=x.
** KEPT (pick-wt=7): 7 [] x^y=y^x.
** KEPT (pick-wt=11): 8 [] (x^y)^z=x^ (y^z).
---> New Demodulator: 9 [new_demod,8] (x^y)^z=x^ (y^z).
** KEPT (pick-wt=5): 10 [] x v x=x.
---> New Demodulator: 11 [new_demod,10] x v x=x.
** KEPT (pick-wt=7): 12 [] x v y=y v x.
** KEPT (pick-wt=11): 13 [] (x v y) v z=x v (y v z).
---> New Demodulator: 14 [new_demod,13] (x v y) v z=x v (y v z).
** KEPT (pick-wt=2): 15 [] x^ (x v y)=x.
---> New Demodulator: 16 [new_demod,15] x^ (x v y)=x.
** KEPT (pick-wt=2): 17 [] x v (x^y)=x.
---> New Demodulator: 18 [new_demod,17] x v (x^y)=x.
** KEPT (pick-wt=5): 19 [] x*x=x.
---> New Demodulator: 20 [new_demod,19] x*x=x.
** KEPT (pick-wt=7): 21 [] x*y=y*x.
** KEPT (pick-wt=11): 22 [] (x*y)*z=x* (y*z).
---> New Demodulator: 23 [new_demod,22] (x*y)*z=x* (y*z).
** KEPT (pick-wt=2): 24 [] x* (x v y)=x.
---> New Demodulator: 25 [new_demod,24] x* (x v y)=x.
** KEPT (pick-wt=2): 26 [] x v (x*y)=x.
---> New Demodulator: 27 [new_demod,26] x v (x*y)=x.
>>>> Starting back demodulation with 6.
  Following clause subsumed by 7 during input processing: 0 [copy,7,flip.1] x^y=y^x.
>>>> Starting back demodulation with 9.
>>>> Starting back demodulation with 11.
  Following clause subsumed by 12 during input processing: 0 [copy,12,flip.1] x v y=y v x.
>>>> Starting back demodulation with 14.
>>>> Starting back demodulation with 16.
>>>> Starting back demodulation with 18.
>>>> Starting back demodulation with 20.
  Following clause subsumed by 21 during input processing: 0 [copy,21,flip.1] x*y=y*x.
>>>> Starting back demodulation with 23.
>>>> Starting back demodulation with 25.
>>>> Starting back demodulation with 27.

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

=========== start of search ===========

given clause #1: (wt=2) 15 [] x^ (x v y)=x.

----> UNIT CONFLICT at   0.72 sec ----> 84 [binary,82.1,1.1] $F.

Length of proof is 13.  Level of proof is 6.

---------------- PROOF ----------------

1 [] A^B!=A*B.
7 [] x^y=y^x.
8 [] (x^y)^z=x^ (y^z).
12 [] x v y=y v x.
15 [] x^ (x v y)=x.
17 [] x v (x^y)=x.
21 [] x*y=y*x.
23,22 [] (x*y)*z=x* (y*z).
24 [] x* (x v y)=x.
26 [] x v (x*y)=x.
28 [para_into,7.1.1,15.1.1,flip.1] (x v y)^x=x.
30 [para_from,7.1.1,17.1.1.2] x v (y^x)=x.
34 [para_into,12.1.1,26.1.1,flip.1] (x*y) v x=x.
40 [para_from,12.1.1,24.1.1.2] x* (y v x)=x.
44 [para_from,34.1.1,28.1.1.1] x^ (x*y)=x*y.
46 [para_into,21.1.1,40.1.1,flip.1] (x v y)*y=y.
50 [para_from,21.1.1,44.1.1.2] x^ (y*x)=x*y.
57,56 [para_into,46.1.1.1,30.1.1] x* (y^x)=y^x.
59,58 [para_into,46.1.1.1,17.1.1] x* (x^y)=x^y.
60 [para_from,8.1.1,17.1.1.2] (x^y) v (x^ (y^z))=x^y.
64 [para_into,60.1.1.2.2,50.1.1] (x^y) v (x^ (y*z))=x^y.
74 [para_into,64.1.1.2,50.1.1] (x^y) v (x*y)=x^y.
82 [para_from,74.1.1,40.1.1.2,demod,23,57,59] x^y=x*y.
84 [binary,82.1,1.1] $F.

-------------- statistics -------------
clauses given                 35
clauses generated            656
  (hot clauses generated)     36
  para_from generated        238
  para_into generated        418
demod & eval rewrites        553
clauses wt,lit,sk delete     241
tautologies deleted            0
clauses forward subsumed     391
cl not subsumed due to ancestor_subsume       0
  (subsumed by sos)            3
unit deletions                 0
factor simplifications         0
clauses kept                  42
  (hot clauses kept)           0
new demodulators              38
empty clauses                  1
clauses back demodulated       0
clauses back subsumed          0
usable size                   36
sos size                       6
demodulators size             38
passive size                   1
hot size                       2
Kbytes malloced              255

----------- times (seconds) -----------
user CPU time          0.78          (0 hr, 0 min, 0 sec)
system CPU time        0.35          (0 hr, 0 min, 0 sec)
wall-clock time        1             (0 hr, 0 min, 1 sec)
input time             0.10
  clausify time        0.00
  process input        0.04
para_into time         0.04
para_from time         0.05
pre_process time       0.40
  renumber time        0.00
  demod time           0.09
  order equalities     0.02
  unit deleletion      0.00
  factor simplify      0.00
  weigh cl time        0.02
  hints keep time      0.00
  sort lits time       0.00
  forward subsume      0.07
  delete cl time       0.01
  keep cl time         0.03
    hints time         0.00
  print_cl time        0.00
  conflict time        0.06
  new demod time       0.02
post_process time      0.01
  back demod time      0.00
  back subsume         0.01
  factor time          0.00
  hot list time        0.03
  unindex time         0.00

The job finished        Mon Oct 16 16:46:38 1995