The lion chases the mouse. The lion is blue. The mouse chases the lion. The mouse is cold. The mouse is red. The tiger chases the lion. The tiger is green. The tiger is young. The tiger needs the lion. The tiger sees the lion. If someone needs the tiger and the tiger is red then the tiger chases the lion. If someone sees the tiger then they need the mouse. If the mouse needs the lion and the mouse needs the tiger then the lion chases the tiger. If someone needs the tiger and the tiger needs the mouse then the mouse chases the tiger. If the tiger sees the lion and the tiger needs the mouse then the tiger sees the mouse. If someone is green then they are blue. If someone sees the mouse then they are young. If someone chases the lion then they need the tiger.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is blue.
("lion" "is" "blue" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone needs the tiger and the tiger is red then the tiger chases the lion.
((("someone" "needs" "tiger" "+") ("tiger" "is" "red" "+")) -> ("tiger" "chases" "lion" "+"))
If someone sees the tiger then they need the mouse.
((("someone" "sees" "tiger" "+")) -> ("someone" "needs" "mouse" "+"))
If the mouse needs the lion and the mouse needs the tiger then the lion chases the tiger.
((("mouse" "needs" "lion" "+") ("mouse" "needs" "tiger" "+")) -> ("lion" "chases" "tiger" "+"))
If someone needs the tiger and the tiger needs the mouse then the mouse chases the tiger.
((("someone" "needs" "tiger" "+") ("tiger" "needs" "mouse" "+")) -> ("mouse" "chases" "tiger" "+"))
If the tiger sees the lion and the tiger needs the mouse then the tiger sees the mouse.
((("tiger" "sees" "lion" "+") ("tiger" "needs" "mouse" "+")) -> ("tiger" "sees" "mouse" "+"))
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the mouse then they are young.
((("someone" "sees" "mouse" "+")) -> ("someone" "is" "young" "+"))
If someone chases the lion then they need the tiger.
((("someone" "chases" "lion" "+")) -> ("someone" "needs" "tiger" "+"))
The tiger chases the lion.
True
1
proof
[(triple6)]
("tiger" "chases" "lion" "+")
triple6
The tiger is not young.
False
1
inv-proof
[(triple8)]
("tiger" "is" "young" "-")
triple8
The lion does not need the mouse.
Unknown
inv-rconc
[@1: The lion needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The lion chases the mouse.[(triple1)] The lion is blue.[(triple2)] The mouse chases the lion.[(triple3)] The mouse is cold.[(triple4)] The mouse is red.[(triple5)] The tiger chases the lion.[(triple6)] The tiger is green.[(triple7)] The tiger is young.[(triple8)] The tiger needs the lion.[(triple9)] The tiger sees the lion.[(triple10)] @1: The mouse needs the tiger.[(((triple3) -> rule8))] The tiger is blue.[(((triple7) -> rule6))] The tiger needs the tiger.[(((triple6) -> rule8))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple3
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
triple5
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The tiger is young.
("tiger" "is" "young" "+")
triple8
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple9
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple10
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
((triple3) -> (rule8 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple7) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple6) -> (rule8 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1