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