% box(or(P,diam(Q))) = or(box(P),diam(Q)).
'$box'('$or'(p,'$diam'(q)))-w.
'$or'('$box'(p),'$diam'(q))-w -> [].

:-option(term_var_weight).


/*



Proof:
======

   2 : r(C,D),min=D                                                     [axiom]
   3 : r(C,D) -> r(E,D)                                                 [axiom]
   4 : C-D -> $or(C,E)-D                                                [axiom]
   5 : C-D -> $or(E,C)-D                                                [axiom]
   6 : $or(C,D)-E -> C-E,D-E                                            [axiom]
   7 : C-D,$not(C)-D                                                    [axiom]
   8 : C-D,$not(C)-D ->                                                 [axiom]
   9 : $diam(C)-D -> C-g(C,D)                                           [axiom]
  10 : $diam(C)-D -> r(D,g(C,D))                                        [axiom]
  11 : r(C,D),E-D -> $diam(E)-C                                         [axiom]
  12 : $box(C)=$not($diam($not(C)))                                     [axiom]
  13 : $box($or(p,$diam(q)))-w                                          [axiom]
  14 : $or($box(p),$diam(q))-w ->                                       [axiom]
  15 : $not($diam($not($or(p,$diam(q)))))-w           [reduction of 13 by [12]]
  16 : $or($not($diam($not(p))),$diam(q))-w ->        [reduction of 14 by [12]]
  20 : r(C,D),E-D -> $or(F,$diam(E))-C         [negative chaining of 11 from 5]
  21 : r(C,D),E-D -> E-g(E,C)                  [negative chaining of 11 from 9]
  22 : r(C,D),E-D -> r(C,g(E,C))              [negative chaining of 11 from 10]
  25 : C-D,$or($not(C),E)-D                     [negative chaining of 7 from 4]
  41 : r(w,C),q-C ->                          [negative chaining of 20 from 16]
  94 : $diam($not(p))-w                       [negative chaining of 25 from 16]
  98 : $not(p)-g($not(p),w)                    [negative chaining of 94 from 9]
  99 : r(w,g($not(p),w))                      [negative chaining of 94 from 10]
 102 : r(C,g($not(p),w))                       [negative chaining of 99 from 3]
 108 : r(C,g($not(p),w)) -> $not(p)-g($not(p),C) [negative chaining of 98 from 21]
 110 : $not(p)-g($not(p),C)                         [reduction of 108 by [102]]
 113 : p-g($not(p),C) ->                      [negative chaining of 110 from 8]
 115 : r(C,g($not(p),D)) -> r(C,g($not(p),C)) [negative chaining of 110 from 22]
 179 : r(C,g($not(p),C))                    [negative chaining of 102 from 115]
 180 : r(C,g($not(p),D))                      [negative chaining of 179 from 3]
 327 : $diam($not($or(p,$diam(q))))-w ->       [negative chaining of 15 from 8]
 330 : r(w,C),$not($or(p,$diam(q)))-C ->     [negative chaining of 11 from 327]
 331 : r(w,C) -> $or(p,$diam(q))-C            [negative chaining of 7 from 330]
 336 : r(w,C) -> p-C,$diam(q)-C               [negative chaining of 331 from 6]
 347 : r(w,C) -> p-C,q-g(q,C)                 [negative chaining of 336 from 9]
 348 : r(w,C) -> p-C,r(C,g(q,C))             [negative chaining of 336 from 10]
 373 : r(w,g($not(p),C)) -> q-g(q,g($not(p),C)) [negative chaining of 347 from 113]
 376 : q-g(q,g($not(p),C))                          [reduction of 373 by [180]]
 377 : r(w,g(q,g($not(p),C))) ->             [negative chaining of 376 from 41]
 378 : min=g(q,g($not(p),C))                  [negative chaining of 2 from 377]
 379 : q-min                                        [reduction of 376 by [378]]
 384 : r(C,min) -> q-g(q,C)                  [negative chaining of 379 from 21]
 385 : r(C,min) -> r(C,g(q,C))               [negative chaining of 379 from 22]
 399 : r(C,min),r(w,g(q,C)) ->               [negative chaining of 384 from 41]
 400 : r(C,min) -> r(D,g(q,C))                [negative chaining of 385 from 3]
 401 : true,r(C,min) ->                             [reduction of 399 by [400]]
 492 : r(w,g($not(p),C)) -> r(g($not(p),C),g(q,g($not(p),C))) [negative chaining of 348 from 113]
 495 : false                                [reduction of 492 by [180,378,401]]


Length = 48, Depth = 17



Total time: 167320 milliseconds
*/