Starting on goal: Prolog$Goal(car=l("[]", "not", l("()", l("[]", "not", l("()", l("[]", "not", l("()", l("[]", "not", l("()", l("[]", "not", l("()", l("[]", "true", "or", "true")))))))))))) Trying clause: "[]"(verify, "[]"(_1, should, be, true)) :- _1 No match for clause. Trying clause: "[]"(verify, "[]"(_2, should, be, false)) :- "[]"(not, "()"(_2)) No match for clause. Trying clause: "[]"(not, "()"(_3)) :- _3; "!"; false New goal: "[]"(not, "()"("[]"(not, "()"("[]"(not, "()"("[]"(not, "()"("[]"(true, or, true))))))))); "!"; false Trying clause: nativeTest2 :- native No match for clause. Trying clause: nativeFail :- native No match for clause. Trying clause: "[]"(_4, "=", intmul, "()"("[]"(_5, ",", _6))) :- native No match for clause. Trying clause: "[]"(_7, "=", intdiv, "()"("[]"(_8, ",", _9))) :- native No match for clause. Trying clause: "[]"(_10, "=", intadd, "()"("[]"(_11, ",", _12))) :- native No match for clause. Trying clause: "[]"(_13, "=", intminus, "()"("[]"(_14, ",", _15))) :- native No match for clause. Trying clause: "[]"(_16, is, greater, than, _17) :- native No match for clause. Trying clause: "[]"(head, _18, exists, in, theory, _19) :- native No match for clause. Trying clause: "[]"(_20, "=", all, theory, names) :- native No match for clause. Trying clause: "[]"(_21, "=", tocons, "()"(_22)) :- native No match for clause. Trying clause: "[]"(_23, in, _24) :- "[]"(_24, "=", tocons, "()"(_25)); "[]"(_23, "=", iter, _24) No match for clause. Trying clause: "[]"(_26, or, _27) :- _26 No match for clause. Trying clause: "[]"(_28, or, _29) :- _29 No match for clause. Trying clause: "[]"(_30, "=", iter, "[]"(cons, _30, _31)) No match for clause. Trying clause: "[]"(_32, "=", iter, "[]"(cons, _33, _34)) :- "[]"(_32, "=", iter, _34) No match for clause. Trying clause: "[]"(verify, "[]"(_35, should, be, true)) :- _35 No match for clause. Trying clause: "[]"(_36, "=", smartmul, "()"("[]"(_37, ",", _38))) :- "[]"(_36, "=", intmul, "()"("[]"(_37, ",", _38))) No match for clause. Trying clause: "[]"(_39, "=", smartmul, "()"("[]"(_40, ",", _41))) :- "[]"(_40, "=", intdiv, "()"("[]"(_39, ",", _41))) No match for clause. Trying clause: "[]"(_42, "=", smartmul, "()"("[]"(_43, ",", _44))) :- "[]"(_44, "=", intdiv, "()"("[]"(_42, ",", _43))) No match for clause. Trying clause: "[]"(verify, "[]"(_45, should, be, false)) :- "[]"(not, "()"(_45)) No match for clause. Trying clause: "()"(_46) :- _46 No match for clause. Trying clause: "[]"("\"and\"", is, a, fill, word) No match for clause. Trying clause: "[]"("\",\"", is, a, fill, word) No match for clause. Trying clause: "[]"("[]"(not, "()"(true)), should, be, false) No match for clause. Trying clause: "[]"(mrshutco, is, a, human) No match for clause. Trying clause: "[]"("[]"(not, "()"(false)), should, be, true) No match for clause. Trying clause: "[]"(not, "()"(_47)) :- _47; "!"; false New goal: "[]"(not, "()"("[]"(not, "()"("[]"(not, "()"("[]"(true, or, true))))))); "!"; false Trying clause: nativeTest2 :- native No match for clause. Trying clause: nativeFail :- native No match for clause. Trying clause: "[]"(_48, "=", intmul, "()"("[]"(_49, ",", _50))) :- native No match for clause. Trying clause: "[]"(_51, "=", intdiv, "()"("[]"(_52, ",", _53))) :- native No match for clause. Trying clause: "[]"(_54, "=", intadd, "()"("[]"(_55, ",", _56))) :- native No match for clause. Trying clause: "[]"(_57, "=", intminus, "()"("[]"(_58, ",", _59))) :- native No match for clause. Trying clause: "[]"(_60, is, greater, than, _61) :- native No match for clause. Trying clause: "[]"(head, _62, exists, in, theory, _63) :- native No match for clause. Trying clause: "[]"(_64, "=", all, theory, names) :- native No match for clause. Trying clause: "[]"(_65, "=", tocons, "()"(_66)) :- native No match for clause. Trying clause: "[]"(_67, in, _68) :- "[]"(_68, "=", tocons, "()"(_69)); "[]"(_67, "=", iter, _68) No match for clause. Trying clause: "[]"(_70, or, _71) :- _70 No match for clause. Trying clause: "[]"(_72, or, _73) :- _73 No match for clause. Trying clause: "[]"(_74, "=", iter, "[]"(cons, _74, _75)) No match for clause. Trying clause: "[]"(_76, "=", iter, "[]"(cons, _77, _78)) :- "[]"(_76, "=", iter, _78) No match for clause. Trying clause: "[]"(verify, "[]"(_79, should, be, true)) :- _79 No match for clause. Trying clause: "[]"(_80, "=", smartmul, "()"("[]"(_81, ",", _82))) :- "[]"(_80, "=", intmul, "()"("[]"(_81, ",", _82))) No match for clause. Trying clause: "[]"(_83, "=", smartmul, "()"("[]"(_84, ",", _85))) :- "[]"(_84, "=", intdiv, "()"("[]"(_83, ",", _85))) No match for clause. Trying clause: "[]"(_86, "=", smartmul, "()"("[]"(_87, ",", _88))) :- "[]"(_88, "=", intdiv, "()"("[]"(_86, ",", _87))) No match for clause. Trying clause: "[]"(verify, "[]"(_89, should, be, false)) :- "[]"(not, "()"(_89)) No match for clause. Trying clause: "()"(_90) :- _90 No match for clause. Trying clause: "[]"("\"and\"", is, a, fill, word) No match for clause. Trying clause: "[]"("\",\"", is, a, fill, word) No match for clause. Trying clause: "[]"("[]"(not, "()"(true)), should, be, false) No match for clause. Trying clause: "[]"(mrshutco, is, a, human) No match for clause. Trying clause: "[]"("[]"(not, "()"(false)), should, be, true) No match for clause. Trying clause: "[]"(not, "()"(_91)) :- _91; "!"; false New goal: "[]"(not, "()"("[]"(not, "()"("[]"(true, or, true))))); "!"; false Trying clause: nativeTest2 :- native No match for clause. Trying clause: nativeFail :- native No match for clause. Trying clause: "[]"(_92, "=", intmul, "()"("[]"(_93, ",", _94))) :- native No match for clause. Trying clause: "[]"(_95, "=", intdiv, "()"("[]"(_96, ",", _97))) :- native No match for clause. Trying clause: "[]"(_98, "=", intadd, "()"("[]"(_99, ",", _100))) :- native No match for clause. Trying clause: "[]"(_101, "=", intminus, "()"("[]"(_102, ",", _103))) :- native No match for clause. Trying clause: "[]"(_104, is, greater, than, _105) :- native No match for clause. Trying clause: "[]"(head, _106, exists, in, theory, _107) :- native No match for clause. Trying clause: "[]"(_108, "=", all, theory, names) :- native No match for clause. Trying clause: "[]"(_109, "=", tocons, "()"(_110)) :- native No match for clause. Trying clause: "[]"(_111, in, _112) :- "[]"(_112, "=", tocons, "()"(_113)); "[]"(_111, "=", iter, _112) No match for clause. Trying clause: "[]"(_114, or, _115) :- _114 No match for clause. Trying clause: "[]"(_116, or, _117) :- _117 No match for clause. Trying clause: "[]"(_118, "=", iter, "[]"(cons, _118, _119)) No match for clause. Trying clause: "[]"(_120, "=", iter, "[]"(cons, _121, _122)) :- "[]"(_120, "=", iter, _122) No match for clause. Trying clause: "[]"(verify, "[]"(_123, should, be, true)) :- _123 No match for clause. Trying clause: "[]"(_124, "=", smartmul, "()"("[]"(_125, ",", _126))) :- "[]"(_124, "=", intmul, "()"("[]"(_125, ",", _126))) No match for clause. Trying clause: "[]"(_127, "=", smartmul, "()"("[]"(_128, ",", _129))) :- "[]"(_128, "=", intdiv, "()"("[]"(_127, ",", _129))) No match for clause. Trying clause: "[]"(_130, "=", smartmul, "()"("[]"(_131, ",", _132))) :- "[]"(_132, "=", intdiv, "()"("[]"(_130, ",", _131))) No match for clause. Trying clause: "[]"(verify, "[]"(_133, should, be, false)) :- "[]"(not, "()"(_133)) No match for clause. Trying clause: "()"(_134) :- _134 No match for clause. Trying clause: "[]"("\"and\"", is, a, fill, word) No match for clause. Trying clause: "[]"("\",\"", is, a, fill, word) No match for clause. Trying clause: "[]"("[]"(not, "()"(true)), should, be, false) No match for clause. Trying clause: "[]"(mrshutco, is, a, human) No match for clause. Trying clause: "[]"("[]"(not, "()"(false)), should, be, true) No match for clause. Trying clause: "[]"(not, "()"(_135)) :- _135; "!"; false New goal: "[]"(not, "()"("[]"(true, or, true))); "!"; false Trying clause: nativeTest2 :- native No match for clause. Trying clause: nativeFail :- native No match for clause. Trying clause: "[]"(_136, "=", intmul, "()"("[]"(_137, ",", _138))) :- native No match for clause. Trying clause: "[]"(_139, "=", intdiv, "()"("[]"(_140, ",", _141))) :- native No match for clause. Trying clause: "[]"(_142, "=", intadd, "()"("[]"(_143, ",", _144))) :- native No match for clause. Trying clause: "[]"(_145, "=", intminus, "()"("[]"(_146, ",", _147))) :- native No match for clause. Trying clause: "[]"(_148, is, greater, than, _149) :- native No match for clause. Trying clause: "[]"(head, _150, exists, in, theory, _151) :- native No match for clause. Trying clause: "[]"(_152, "=", all, theory, names) :- native No match for clause. Trying clause: "[]"(_153, "=", tocons, "()"(_154)) :- native No match for clause. Trying clause: "[]"(_155, in, _156) :- "[]"(_156, "=", tocons, "()"(_157)); "[]"(_155, "=", iter, _156) No match for clause. Trying clause: "[]"(_158, or, _159) :- _158 No match for clause. Trying clause: "[]"(_160, or, _161) :- _161 No match for clause. Trying clause: "[]"(_162, "=", iter, "[]"(cons, _162, _163)) No match for clause. Trying clause: "[]"(_164, "=", iter, "[]"(cons, _165, _166)) :- "[]"(_164, "=", iter, _166) No match for clause. Trying clause: "[]"(verify, "[]"(_167, should, be, true)) :- _167 No match for clause. Trying clause: "[]"(_168, "=", smartmul, "()"("[]"(_169, ",", _170))) :- "[]"(_168, "=", intmul, "()"("[]"(_169, ",", _170))) No match for clause. Trying clause: "[]"(_171, "=", smartmul, "()"("[]"(_172, ",", _173))) :- "[]"(_172, "=", intdiv, "()"("[]"(_171, ",", _173))) No match for clause. Trying clause: "[]"(_174, "=", smartmul, "()"("[]"(_175, ",", _176))) :- "[]"(_176, "=", intdiv, "()"("[]"(_174, ",", _175))) No match for clause. Trying clause: "[]"(verify, "[]"(_177, should, be, false)) :- "[]"(not, "()"(_177)) No match for clause. Trying clause: "()"(_178) :- _178 No match for clause. Trying clause: "[]"("\"and\"", is, a, fill, word) No match for clause. Trying clause: "[]"("\",\"", is, a, fill, word) No match for clause. Trying clause: "[]"("[]"(not, "()"(true)), should, be, false) No match for clause. Trying clause: "[]"(mrshutco, is, a, human) No match for clause. Trying clause: "[]"("[]"(not, "()"(false)), should, be, true) No match for clause. Trying clause: "[]"(not, "()"(_179)) :- _179; "!"; false New goal: "[]"(true, or, true); "!"; false Trying clause: nativeTest2 :- native No match for clause. Trying clause: nativeFail :- native No match for clause. Trying clause: "[]"(_180, "=", intmul, "()"("[]"(_181, ",", _182))) :- native No match for clause. Trying clause: "[]"(_183, "=", intdiv, "()"("[]"(_184, ",", _185))) :- native No match for clause. Trying clause: "[]"(_186, "=", intadd, "()"("[]"(_187, ",", _188))) :- native No match for clause. Trying clause: "[]"(_189, "=", intminus, "()"("[]"(_190, ",", _191))) :- native No match for clause. Trying clause: "[]"(_192, is, greater, than, _193) :- native No match for clause. Trying clause: "[]"(head, _194, exists, in, theory, _195) :- native No match for clause. Trying clause: "[]"(_196, "=", all, theory, names) :- native No match for clause. Trying clause: "[]"(_197, "=", tocons, "()"(_198)) :- native No match for clause. Trying clause: "[]"(_199, in, _200) :- "[]"(_200, "=", tocons, "()"(_201)); "[]"(_199, "=", iter, _200) No match for clause. Trying clause: "[]"(_202, or, _203) :- _202 New goal: true Trying clause: nativeTest2 :- native No match for clause. Trying clause: nativeFail :- native No match for clause. Trying clause: "[]"(_204, "=", intmul, "()"("[]"(_205, ",", _206))) :- native No match for clause. Trying clause: "[]"(_207, "=", intdiv, "()"("[]"(_208, ",", _209))) :- native No match for clause. Trying clause: "[]"(_210, "=", intadd, "()"("[]"(_211, ",", _212))) :- native No match for clause. Trying clause: "[]"(_213, "=", intminus, "()"("[]"(_214, ",", _215))) :- native No match for clause. Trying clause: "[]"(_216, is, greater, than, _217) :- native No match for clause. Trying clause: "[]"(head, _218, exists, in, theory, _219) :- native No match for clause. Trying clause: "[]"(_220, "=", all, theory, names) :- native No match for clause. Trying clause: "[]"(_221, "=", tocons, "()"(_222)) :- native No match for clause. Trying clause: "[]"(_223, in, _224) :- "[]"(_224, "=", tocons, "()"(_225)); "[]"(_223, "=", iter, _224) No match for clause. Trying clause: "[]"(_226, or, _227) :- _226 No match for clause. Trying clause: "[]"(_228, or, _229) :- _229 No match for clause. Trying clause: "[]"(_230, "=", iter, "[]"(cons, _230, _231)) No match for clause. Trying clause: "[]"(_232, "=", iter, "[]"(cons, _233, _234)) :- "[]"(_232, "=", iter, _234) No match for clause. Trying clause: "[]"(verify, "[]"(_235, should, be, true)) :- _235 No match for clause. Trying clause: "[]"(_236, "=", smartmul, "()"("[]"(_237, ",", _238))) :- "[]"(_236, "=", intmul, "()"("[]"(_237, ",", _238))) No match for clause. Trying clause: "[]"(_239, "=", smartmul, "()"("[]"(_240, ",", _241))) :- "[]"(_240, "=", intdiv, "()"("[]"(_239, ",", _241))) No match for clause. Trying clause: "[]"(_242, "=", smartmul, "()"("[]"(_243, ",", _244))) :- "[]"(_244, "=", intdiv, "()"("[]"(_242, ",", _243))) No match for clause. Trying clause: "[]"(verify, "[]"(_245, should, be, false)) :- "[]"(not, "()"(_245)) No match for clause. Trying clause: "()"(_246) :- _246 No match for clause. Trying clause: "[]"("\"and\"", is, a, fill, word) No match for clause. Trying clause: "[]"("\",\"", is, a, fill, word) No match for clause. Trying clause: "[]"("[]"(not, "()"(true)), should, be, false) No match for clause. Trying clause: "[]"(mrshutco, is, a, human) No match for clause. Trying clause: "[]"("[]"(not, "()"(false)), should, be, true) No match for clause. Trying clause: "[]"(not, "()"(_247)) :- _247; "!"; false No match for clause. Trying clause: "[]"(not, "()"(_248)) No match for clause. Trying clause: "[]"(_249, and, _250) :- _249; _250 No match for clause. Trying clause: "[]"(_251, is, in, list, _252) :- "[]"(_253, "=", tocons, "()"(_252)); "[]"(_251, "=", iter, _253) No match for clause. Trying clause: "[]"(feet, is, the, plural, of, foot) No match for clause. Trying clause: "[]"(bits, is, the, plural, of, bit) No match for clause. Trying clause: "[]"(lasagna, is, tasty) No match for clause. Trying clause: "[]"(_254, or, _255) :- _255 New goal: true