# Generated with http://www.agfa.com/w3c/euler/#R28069 on Sun Dec 09 15:49:54 GMT+01:00 2001
# for query file:/euler/lists-query.n3
# given [file:/euler/lists.n3]

@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix dpo: <http://www.daml.org/2001/03/daml+oil#>.
@prefix : <file:/euler/lists#>.

this log:forSome :x.this log:forSome :y.
[ :l1
  dpo:nil; :l2 [ dpo:first :a; dpo:rest
      [ dpo:first :b; dpo:rest
          [ dpo:first :c; dpo:rest
              dpo:nil]]]; :l12
      [ dpo:first :a; dpo:rest
          [ dpo:first :b; dpo:rest
              [ dpo:first :c; dpo:rest
                  dpo:nil]]]]  .

this log:forSome :x.this log:forSome :y.
 {[ :l1
  dpo:nil; :l2 [ dpo:first :b; dpo:rest
      [ dpo:first :c; dpo:rest
          dpo:nil]]; :l12
      [ dpo:first :b; dpo:rest
          [ dpo:first :c; dpo:rest
              dpo:nil]]]  } log:implies
{[ :l1
  [ dpo:first :a; dpo:rest
      dpo:nil]; :l2 [ dpo:first :b; dpo:rest
      [ dpo:first :c; dpo:rest
          dpo:nil]]; :l12
      [ dpo:first :a; dpo:rest
          [ dpo:first :b; dpo:rest
              [ dpo:first :c; dpo:rest
                  dpo:nil]]]]  }.

this log:forSome :x.this log:forSome :y.
 {{[ :l1
  dpo:nil; :l2 [ dpo:first :c; dpo:rest
      dpo:nil]; :l12
      [ dpo:first :c; dpo:rest
          dpo:nil]]  } log:implies
  {[ :l1
  [ dpo:first :b; dpo:rest
      dpo:nil]; :l2 [ dpo:first :c; dpo:rest
      dpo:nil]; :l12
      [ dpo:first :b; dpo:rest
          [ dpo:first :c; dpo:rest
              dpo:nil]]]  }} log:implies
{[ :l1
  [ dpo:first :a; dpo:rest
      [ dpo:first :b; dpo:rest
          dpo:nil]]; :l2 [ dpo:first :c; dpo:rest
      dpo:nil]; :l12
      [ dpo:first :a; dpo:rest
          [ dpo:first :b; dpo:rest
              [ dpo:first :c; dpo:rest
                  dpo:nil]]]]  }.

this log:forSome :x.this log:forSome :y.
 {{{[ :l1
  dpo:nil; :l2 dpo:nil; :l12
      dpo:nil]  } log:implies
    {[ :l1
  [ dpo:first :c; dpo:rest
      dpo:nil]; :l2 dpo:nil; :l12
      [ dpo:first :c; dpo:rest
          dpo:nil]]  }} log:implies
  {[ :l1
  [ dpo:first :b; dpo:rest
      [ dpo:first :c; dpo:rest
          dpo:nil]]; :l2 dpo:nil; :l12
      [ dpo:first :b; dpo:rest
          [ dpo:first :c; dpo:rest
              dpo:nil]]]  }} log:implies
{[ :l1
  [ dpo:first :a; dpo:rest
      [ dpo:first :b; dpo:rest
          [ dpo:first :c; dpo:rest
              dpo:nil]]]; :l2 dpo:nil; :l12
      [ dpo:first :a; dpo:rest
          [ dpo:first :b; dpo:rest
              [ dpo:first :c; dpo:rest
                  dpo:nil]]]]  }.

# Proof found for file:/euler/lists-query.n3 in 15 steps (3192 steps/sec)