null
```
Starting on goal: [think [user says [what is the text of [theory tennis]]]] and [say $x]
Goal arity 3: [think [user says [what is the text of [theory tennis]]]] and [say $x]
nextSolution
Got clause: _1 and _2
  Clause unifies to: [think [user says [what is the text of [theory tennis]]]] and [say $x]
  gdash: think [user says [what is the text of [theory tennis]]]
Goal arity 2: think [user says [what is the text of [theory tennis]]]
 Got clause: think _7
   Clause unifies to: think [user says [what is the text of [theory tennis]]]
  Clause is native.
   gdash: say $x
 Goal arity 2: say $x
  Got clause: say [it's _21 !]
    Clause unifies to: say [it's _21 !]
    gdash: user says [_22 * _23]
  Goal arity 3: user says [_22 * _23]
  Got clause: say [_53 is _54 !]
    Clause unifies to: say [_53 is _54 !]
    gdash: rewrite with theory "add question mark to user input"
  Goal arity 4: rewrite with theory "add question mark to user input"
   Got clause: rewrite with theory _86
     Clause unifies to: rewrite with theory "add question mark to user input"
    Clause is native.
  REW user says $e1 :- ...
Starting on goal: user says _88
Goal arity 3: user says _88
Got clause: user says [what is the text of [theory tennis]]
  Clause unifies to: user says [what is the text of [theory tennis]]
  gdash: _87 = add question mark ([what is the text of [theory tennis]])
Goal arity 6: _87 = add question mark ([what is the text of [theory tennis]])
 Got clause: _123 = add question mark (_124)
   Clause unifies to: _87 = add question mark ([what is the text of [theory tennis]])
   gdash: _125 = tocons ([what is the text of [theory tennis]])
 Goal arity 4: _125 = tocons ([what is the text of [theory tennis]])
  Got clause: _142 = tocons (_143)
    Clause unifies to: _125 = tocons ([what is the text of [theory tennis]])
   Clause is native.
    gdash: not ([endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?])
  Goal arity 2: not ([endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?])
   Got clause: not (_154)
     Clause unifies to: not ([endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?])
     gdash: endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?
   Goal arity 3: endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?
    Got clause: endswithword_c [cons _158 _159] _160
      Clause unifies to: endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?
      gdash: endswithword_c [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]] ?
    Goal arity 3: endswithword_c [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]] ?
     Got clause: endswithword_c [cons _164 _165] _166
       Clause unifies to: endswithword_c [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]] ?
       gdash: endswithword_c [cons the [cons text [cons of [cons [theory tennis] end]]]] ?
     Goal arity 3: endswithword_c [cons the [cons text [cons of [cons [theory tennis] end]]]] ?
      Got clause: endswithword_c [cons _170 _171] _172
        Clause unifies to: endswithword_c [cons the [cons text [cons of [cons [theory tennis] end]]]] ?
        gdash: endswithword_c [cons text [cons of [cons [theory tennis] end]]] ?
      Goal arity 3: endswithword_c [cons text [cons of [cons [theory tennis] end]]] ?
       Got clause: endswithword_c [cons _176 _177] _178
         Clause unifies to: endswithword_c [cons text [cons of [cons [theory tennis] end]]] ?
         gdash: endswithword_c [cons of [cons [theory tennis] end]] ?
       Goal arity 3: endswithword_c [cons of [cons [theory tennis] end]] ?
        Got clause: endswithword_c [cons _182 _183] _184
          Clause unifies to: endswithword_c [cons of [cons [theory tennis] end]] ?
          gdash: endswithword_c [cons [theory tennis] end] ?
        Goal arity 3: endswithword_c [cons [theory tennis] end] ?
         Got clause: endswithword_c [cons _188 _189] _190
           Clause unifies to: endswithword_c [cons [theory tennis] end] ?
           gdash: endswithword_c end ?
         Goal arity 3: endswithword_c end ?
   Got clause: not (_344)
     Clause unifies to: not ([endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?])
     gdash: _126 = append_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] [cons ? end]
   Goal arity 5: _126 = append_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] [cons ? end]
    Got clause: [cons _356 _357] = append_c [cons _356 _358] _359
      Clause unifies to: [cons what _357] = append_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] [cons ? end]
      gdash: _357 = append_c [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]] [cons ? end]
    Goal arity 5: _357 = append_c [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]] [cons ? end]
     Got clause: [cons _371 _372] = append_c [cons _371 _373] _374
       Clause unifies to: [cons is _372] = append_c [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]] [cons ? end]
       gdash: _372 = append_c [cons the [cons text [cons of [cons [theory tennis] end]]]] [cons ? end]
     Goal arity 5: _372 = append_c [cons the [cons text [cons of [cons [theory tennis] end]]]] [cons ? end]
      Got clause: [cons _386 _387] = append_c [cons _386 _388] _389
        Clause unifies to: [cons the _387] = append_c [cons the [cons text [cons of [cons [theory tennis] end]]]] [cons ? end]
        gdash: _387 = append_c [cons text [cons of [cons [theory tennis] end]]] [cons ? end]
      Goal arity 5: _387 = append_c [cons text [cons of [cons [theory tennis] end]]] [cons ? end]
       Got clause: [cons _401 _402] = append_c [cons _401 _403] _404
         Clause unifies to: [cons text _402] = append_c [cons text [cons of [cons [theory tennis] end]]] [cons ? end]
         gdash: _402 = append_c [cons of [cons [theory tennis] end]] [cons ? end]
       Goal arity 5: _402 = append_c [cons of [cons [theory tennis] end]] [cons ? end]
        Got clause: [cons _416 _417] = append_c [cons _416 _418] _419
          Clause unifies to: [cons of _417] = append_c [cons of [cons [theory tennis] end]] [cons ? end]
          gdash: _417 = append_c [cons [theory tennis] end] [cons ? end]
        Goal arity 5: _417 = append_c [cons [theory tennis] end] [cons ? end]
         Got clause: [cons _431 _432] = append_c [cons _431 _433] _434
           Clause unifies to: [cons [theory tennis] _432] = append_c [cons [theory tennis] end] [cons ? end]
           gdash: _432 = append_c end [cons ? end]
         Goal arity 5: _432 = append_c end [cons ? end]
          Got clause: _445 = append_c end _445
            Clause unifies to: [cons ? end] = append_c end [cons ? end]
            gdash: _87 = fromcons ([cons what [cons is [cons the [cons text [cons of [cons [theory tennis] [cons ? end]]]]]]])
          Goal arity 4: _87 = fromcons ([cons what [cons is [cons the [cons text [cons of [cons [theory tennis] [cons ? end]]]]]]])
           Got clause: _463 = fromcons (_464)
             Clause unifies to: _87 = fromcons ([cons what [cons is [cons the [cons text [cons of [cons [theory tennis] [cons ? end]]]]]]])
            Clause is native.
             gdash: -
SUCCESS!
Found new statement: "[]"(user, says, "[]"(what, is, the, text, of, "[]"(theory, tennis), "?"))
   Got clause: not _675
     Clause unifies to: not ([endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?])
     gdash: not (["()" = operator (([endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?]))])
   Goal arity 2: not (["()" = operator (([endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?]))])
    Got clause: not (_686)
      Clause unifies to: not (["()" = operator (([endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?]))])
      gdash: "()" = operator (([endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?]))
    Goal arity 4: "()" = operator (([endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?]))
     Got clause: _706 = operator (_707)
       Clause unifies to: "()" = operator (([endswithword_c [cons what [cons is [cons the [cons text [cons of [cons [theory tennis] end]]]]]] ?]))
      Clause is native.
       gdash: ?? "!"("5")
     Goal arity 1: ?? "!"("5")
cut -1. Prolog$Goal(car=l("!", "5"), cdr=Prolog$Goal(car=l("false"), cdr=Prolog$Goal(car=l("[]", "not", l("()", Prolog$Var(id=675L, instance=l("()", l("[]", "endswithword_c", Prolog$Var(id=125L, instance=l("[]", "cons", "what", l("[]", "cons", "is", l("[]", "cons", "the", l("[]", "cons", "text", l("[]", "cons", "of", l("[]", "cons", l("[]", "theory", "tennis"), "end"))))))), "?"))))), cdr=Prolog$Goal(car=l("[]", Prolog$Var(id=126L, instance=r21), "=", "append_c", r11, l("[]", "cons", "?", "end")), cdr=Prolog$Goal(car=l("[]", Prolog$Var(id=123L, instance=Prolog$Var(id=87L, instance=r26)), "=", "fromcons", l("()", r21)))))))
      Goal arity 0: false
cut 0. Prolog$Goal(car=l("!", "5"), cdr=Prolog$Goal(car=l("false"), cdr=Prolog$Goal(car=l("[]", "not", l("()", Prolog$Var(id=675L, instance=l("()", l("[]", "endswithword_c", Prolog$Var(id=125L, instance=l("[]", "cons", "what", l("[]", "cons", "is", l("[]", "cons", "the", l("[]", "cons", "text", l("[]", "cons", "of", l("[]", "cons", l("[]", "theory", "tennis"), "end"))))))), "?"))))), cdr=Prolog$Goal(car=l("[]", Prolog$Var(id=126L, instance=r21), "=", "append_c", r11, l("[]", "cons", "?", "end")), cdr=Prolog$Goal(car=l("[]", Prolog$Var(id=123L, instance=Prolog$Var(id=87L, instance=r26)), "=", "fromcons", l("()", r21)))))))
back to cut point 5
cut: dropping Prolog$Goal(car=l("!", "5"), cdr=Prolog$Goal(car=l("false"), cdr=Prolog$Goal(car=l("[]", "not", l("()", Prolog$Var(id=675L, instance=l("()", l("[]", "endswithword_c", Prolog$Var(id=125L, instance=l("[]", "cons", "what", l("[]", "cons", "is", l("[]", "cons", "the", l("[]", "cons", "text", l("[]", "cons", "of", l("[]", "cons", l("[]", "theory", "tennis"), "end"))))))), "?"))))), cdr=Prolog$Goal(car=l("[]", Prolog$Var(id=126L, instance=r21), "=", "append_c", r11, l("[]", "cons", "?", "end")), cdr=Prolog$Goal(car=l("[]", Prolog$Var(id=123L, instance=Prolog$Var(id=87L, instance=r26)), "=", "fromcons", l("()", r21)))))))
cut: dropping Prolog$Goal(car=Prolog$Var(id=686L, instance=l("[]", "\"()\"", "=", "operator", l("()", Prolog$Var(id=675L, instance=l("()", l("[]", "endswithword_c", Prolog$Var(id=125L, instance=l("[]", "cons", "what", l("[]", "cons", "is", l("[]", "cons", "the", l("[]", "cons", "text", l("[]", "cons", "of", l("[]", "cons", l("[]", "theory", "tennis"), "end"))))))), "?")))))), cdr=Prolog$Goal(car=l("!", "5"), cdr=Prolog$Goal(car=l("false"), cdr=Prolog$Goal(car=l("[]", "not", l("()", r5)), cdr=Prolog$Goal(car=l("[]", Prolog$Var(id=126L, instance=r25), "=", "append_c", r8, l("[]", "cons", "?", "end")), cdr=Prolog$Goal(car=l("[]", Prolog$Var(id=123L, instance=Prolog$Var(id=87L, instance=r30)), "=", "fromcons", l("()", r25))))))))
cut: dropping Prolog$Goal(car=l("[]", "not", l("()", l("[]", "\"()\"", "=", "operator", l("()", Prolog$Var(id=675L, instance=l("()", l("[]", "endswithword_c", Prolog$Var(id=125L, instance=l("[]", "cons", "what", l("[]", "cons", "is", l("[]", "cons", "the", l("[]", "cons", "text", l("[]", "cons", "of", l("[]", "cons", l("[]", "theory", "tennis"), "end"))))))), "?"))))))), cdr=Prolog$Goal(car=l("[]", "not", l("()", r6)), cdr=Prolog$Goal(car=l("[]", Prolog$Var(id=126L, instance=r22), "=", "append_c", r9, l("[]", "cons", "?", "end")), cdr=Prolog$Goal(car=l("[]", Prolog$Var(id=123L, instance=Prolog$Var(id=87L, instance=r27)), "=", "fromcons", l("()", r22))))))
Got 1 rewritten terms.
Adding rewritten term: user says [what is the text of [theory tennis] ?]
     gdash: user says _55
   Goal arity 3: user says _55
    Got clause: user says [what is the text of [theory tennis]]
      Clause unifies to: user says [what is the text of [theory tennis]]
      gdash: rew ! [what is the text of [theory tennis]] to [what is _53 ?]
    Goal arity 5: rew ! [what is the text of [theory tennis]] to [what is _53 ?]
     Got clause: rew ! _858 to _859
       Clause unifies to: rew ! [what is the text of [theory tennis]] to [what is _53 ?]
       gdash: rew [what is the text of [theory tennis]] to [what is _53 ?]
     Goal arity 4: rew [what is the text of [theory tennis]] to [what is _53 ?]
      Got clause: rew _923 to _924
        Clause unifies to: rew [what is the text of [theory tennis]] to [what is _53 ?]
        gdash: rewrite [what is the text of [theory tennis]] to _925
      Goal arity 4: rewrite [what is the text of [theory tennis]] to _925
    Got clause: user says [what is the text of [theory tennis] ?]
      Clause unifies to: user says [what is the text of [theory tennis] ?]
      gdash: rew ! [what is the text of [theory tennis] ?] to [what is _53 ?]
    Goal arity 5: rew ! [what is the text of [theory tennis] ?] to [what is _53 ?]
     Got clause: rew ! _1076 to _1077
       Clause unifies to: rew ! [what is the text of [theory tennis] ?] to [what is _53 ?]
       gdash: rew [what is the text of [theory tennis] ?] to [what is _53 ?]
     Goal arity 4: rew [what is the text of [theory tennis] ?] to [what is _53 ?]
      Got clause: rew _1141 to _1142
        Clause unifies to: rew [what is the text of [theory tennis] ?] to [what is _53 ?]
        gdash: rewrite [what is the text of [theory tennis] ?] to _1143
      Goal arity 4: rewrite [what is the text of [theory tennis] ?] to _1143
       Got clause: rewrite [what is the _1180 of _1181 ?] to [what is [the _1180 of _1181] ?]
         Clause unifies to: rewrite [what is the text of [theory tennis] ?] to [what is [the text of [theory tennis]] ?]
         gdash: rew [what is [the text of [theory tennis]] ?] to [what is _53 ?]
       Goal arity 4: rew [what is [the text of [theory tennis]] ?] to [what is _53 ?]
        Got clause: rew _1245 to _1246
          Clause unifies to: rew [what is [the text of [theory tennis]] ?] to [what is _53 ?]
          gdash: rewrite [what is [the text of [theory tennis]] ?] to _1247
        Goal arity 4: rewrite [what is [the text of [theory tennis]] ?] to _1247
        Got clause: rew _1340 to _1340
          Clause unifies to: rew [what is [the text of [theory tennis]] ?] to [what is [the text of [theory tennis]] ?]
          gdash: ?? "!"("6")
        Goal arity 1: ?? "!"("6")
cut -1. Prolog$Goal(car=l("!", "6"), cdr=Prolog$Goal(car=l("[]", Prolog$Var(id=53L, instance=l("[]", "the", Prolog$Var(id=1180L, instance=l("text")), "of", Prolog$Var(id=1181L, instance=l("[]", "theory", "tennis")))), "is", Prolog$Var(id=54L, instance=r11))))
         Goal arity 3: [the text of [theory tennis]] is _54
          Got clause: [the _1347 of _1348] is _1349
            Clause unifies to: [the text of [theory tennis]] is _54
            gdash: the text of [theory tennis] is _54
          Goal arity 6: the text of [theory tennis] is _54
           Got clause: the text of [theory _1365] is _1366
             Clause unifies to: the text of [theory tennis] is _54
             gdash: _54 = text of theory tennis
           Goal arity 6: _54 = text of theory tennis
            Got clause: _1372 = text of theory _1373
              Clause unifies to: _54 = text of theory tennis
             Clause is native.
              gdash: -
SUCCESS!
  solution found in step 362```