-- FRUIT1PROOF



Derivation of

p1(x,y)

Narrowing the preceding tree leads to the summand

  x0 =/= himbeere
& p0(x0,y0)

Adding the other summands leads to

    x0 =/= himbeere
  & p0(x0,y0)
|   y0 =/= kuehlschrank
  & p0(x0,y0)

Applying the axiom

     p0(x,y)
<===   obst(x)
     & konservierung(y)

at positions [1,1],[0,1] of the preceding tree leads to the formula

    x0 =/= himbeere
  & (  obst(x0)
     & konservierung(y0))
|   y0 =/= kuehlschrank
  & (  obst(x0)
     & konservierung(y0))

Applying the axioms

  (     konservierung(x)
   <===   kuehlen(x)
        | erhitzen(x))
& (     obst(x)
   <===   steinobst(x)
        | beerenobst(x))

at positions [1,1,1],[0,1,0] of the preceding tree leads to the formula

    x0 =/= himbeere
  & (  (  steinobst(x0)
        | beerenobst(x0))
     & konservierung(y0))
|   y0 =/= kuehlschrank
  & (  obst(x0)
     & (  kuehlen(y0)
        | erhitzen(y0)))

Applying the axioms

  (     erhitzen(x)
   <===   x = dose
        | x = glas)
& (     beerenobst(x)
   <===   x = himbeere
        | x = brombeere)
& (     steinobst(x)
   <===   x = kirsche
        | x = pflaume
        | x = pfirsich)
& (     kuehlen(x)
   <===   x = kuehlschrank
        | gefrieren(x))

at positions [1,1,1,1],[1,1,1,0],[0,1,0,1],[0,1,0,0] of the preceding tree leads to the formula

    x0 =/= himbeere
  & (  (  (  x0 = kirsche
           | x0 = pflaume
           | x0 = pfirsich)
        | (  x0 = himbeere
           | x0 = brombeere))
     & konservierung(y0))
|   y0 =/= kuehlschrank
  & (  obst(x0)
     & (  (  y0 = kuehlschrank
           | gefrieren(y0))
        | (  y0 = dose
           | y0 = glas)))

Applying the axiom

     gefrieren(x)
<===   x = gefrierfach
     | x = tiefkuehltruhe

at position [1,1,1,0,1] of the preceding tree leads to the formula

    x0 =/= himbeere
  & (  (  (  x0 = kirsche
           | x0 = pflaume
           | x0 = pfirsich)
        | (  x0 = himbeere
           | x0 = brombeere))
     & konservierung(y0))
|   y0 =/= kuehlschrank
  & (  obst(x0)
     & (  (  y0 = kuehlschrank
           | (  y0 = gefrierfach
              | y0 = tiefkuehltruhe))
        | (  y0 = dose
           | y0 = glas)))

Simplifying (32 steps) the preceding tree leads to the summand

  x0 = kirsche
& konservierung(y0)

Adding the other summands leads to

    x0 = kirsche
  & konservierung(y0)
|   x0 = pflaume
  & konservierung(y0)
|   x0 = pfirsich
  & konservierung(y0)
|   x0 = brombeere
  & konservierung(y0)
|   y0 = dose
  & obst(x0)
|   y0 = glas
  & obst(x0)
|   y0 = gefrierfach
  & obst(x0)
|   y0 = tiefkuehltruhe
  & obst(x0)

Applying the theorem

       x = kirsche
     | x = pflaume
     | x = pfirsich
<=== steinobst(x)

at position [] of the preceding tree leads to the formula

    steinobst(x0)
  & konservierung(y0)
|   x0 = brombeere
  & konservierung(y0)
|   y0 = dose
  & obst(x0)
|   y0 = glas
  & obst(x0)
|   y0 = gefrierfach
  & obst(x0)
|   y0 = tiefkuehltruhe
  & obst(x0)

Applying the theorem

       x = dose
     | x = glas
<=== erhitzen(x)

at position [] of the preceding tree leads to the formula

    erhitzen(y0)
  & obst(x0)
|   steinobst(x0)
  & konservierung(y0)
|   x0 = brombeere
  & konservierung(y0)
|   y0 = gefrierfach
  & obst(x0)
|   y0 = tiefkuehltruhe
  & obst(x0)

Applying the theorem

       x = gefrierfach
     | x = tiefkuehltruhe
<=== gefrieren(x)

at position [] of the preceding tree leads to the formula

    gefrieren(y0)
  & obst(x0)
|   erhitzen(y0)
  & obst(x0)
|   steinobst(x0)
  & konservierung(y0)
|   x0 = brombeere
  & konservierung(y0)