The lion is round. The lion sees the rabbit. The mouse needs the squirrel. The rabbit is cold. The rabbit sees the squirrel. The squirrel likes the mouse. The squirrel needs the rabbit. If someone likes the squirrel then they like the rabbit. If someone sees the rabbit and the rabbit likes the squirrel then the rabbit needs the squirrel. If someone sees the lion then the lion is cold. If someone needs the lion and the lion sees the mouse then the lion is rough. If someone sees the rabbit then the rabbit likes the mouse. If someone likes the mouse and they like the squirrel then the mouse sees the squirrel. If someone sees the rabbit then they need the lion. If someone is cold then they like the squirrel.
The lion is round.
("lion" "is" "round" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If someone likes the squirrel then they like the rabbit.
((("someone" "likes" "squirrel" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone sees the rabbit and the rabbit likes the squirrel then the rabbit needs the squirrel.
((("someone" "sees" "rabbit" "+") ("rabbit" "likes" "squirrel" "+")) -> ("rabbit" "needs" "squirrel" "+"))
If someone sees the lion then the lion is cold.
((("someone" "sees" "lion" "+")) -> ("lion" "is" "cold" "+"))
If someone needs the lion and the lion sees the mouse then the lion is rough.
((("someone" "needs" "lion" "+") ("lion" "sees" "mouse" "+")) -> ("lion" "is" "rough" "+"))
If someone sees the rabbit then the rabbit likes the mouse.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "likes" "mouse" "+"))
If someone likes the mouse and they like the squirrel then the mouse sees the squirrel.
((("someone" "likes" "mouse" "+") ("someone" "likes" "squirrel" "+")) -> ("mouse" "sees" "squirrel" "+"))
If someone sees the rabbit then they need the lion.
((("someone" "sees" "rabbit" "+")) -> ("someone" "needs" "lion" "+"))
If someone is cold then they like the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "squirrel" "+"))
The lion is round.
True
1
proof
[(triple1)]
("lion" "is" "round" "+")
triple1
The mouse does not need the squirrel.
False
1
inv-proof
[(triple3)]
("mouse" "needs" "squirrel" "-")
triple3
The lion needs the lion.
True
2
proof
[(((triple2) -> rule7))]
("lion" "needs" "lion" "+")
((triple2) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The rabbit does not like the squirrel.
False
2
inv-proof
[(((triple4) -> rule8))]
("rabbit" "likes" "squirrel" "-")
((triple4) -> (rule8 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The mouse sees the squirrel.
True
5
proof
[(((((triple2) -> rule5) ((triple4) -> rule8)) -> rule6))]
("mouse" "sees" "squirrel" "+")
((((triple2) -> (rule5 % int3)) ((triple4) -> (rule8 % int2))) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int3
The rabbit does not like the rabbit.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule1))]
("rabbit" "likes" "rabbit" "-")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The mouse does not like the squirrel.
Unknown
inv-rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "likes" "squirrel" "-")
The squirrel needs the lion.
Unknown
rconc
[@1: The squirrel needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "needs" "lion" "+")
The mouse does not like the rabbit.
Unknown
inv-rconc
[@2: The mouse likes the rabbit.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("mouse" "likes" "rabbit" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The rabbit likes the lion.
Unknown
random
[@0: The rabbit likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "lion" "+")
@0: The lion is round.[(triple1)] The lion sees the rabbit.[(triple2)] The mouse needs the squirrel.[(triple3)] The rabbit is cold.[(triple4)] The rabbit sees the squirrel.[(triple5)] The squirrel likes the mouse.[(triple6)] The squirrel needs the rabbit.[(triple7)] @1: The lion needs the lion.[(((triple2) -> rule7))] The rabbit likes the mouse.[(((triple2) -> rule5))] The rabbit likes the squirrel.[(((triple4) -> rule8))] @2: The mouse sees the squirrel.[(((((triple2) -> rule5) ((triple4) -> rule8)) -> rule6))] The rabbit likes the rabbit.[(((((triple4) -> rule8)) -> rule1))] The rabbit needs the squirrel.[(((triple2 ((triple4) -> rule8)) -> rule2))]
The lion is round.
("lion" "is" "round" "+")
triple1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple3
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple5
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple6
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple7
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple2) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((triple2) -> (rule5 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
((triple4) -> (rule8 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((((triple2) -> (rule5 % int3)) ((triple4) -> (rule8 % int2))) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int3
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
((triple2 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2