The lion is rough. The lion likes the mouse. The lion needs the squirrel. The lion visits the mouse. The mouse needs the lion. The rabbit needs the mouse. The rabbit visits the lion. The rabbit visits the squirrel. The squirrel is cold. The squirrel needs the lion. The squirrel visits the lion. The squirrel visits the rabbit. If someone is kind then they need the mouse. If the rabbit is young and the rabbit visits the lion then the lion likes the rabbit. If someone is cold then they are kind. If the rabbit is rough and the rabbit visits the lion then the rabbit is round. If someone likes the mouse and the mouse needs the squirrel then they need the squirrel. If someone needs the rabbit and they visit the lion then the rabbit visits the lion. If someone likes the squirrel then the squirrel likes the rabbit. If someone is round then they visit the lion.
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If someone is kind then they need the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "mouse" "+"))
If the rabbit is young and the rabbit visits the lion then the lion likes the rabbit.
((("rabbit" "is" "young" "+") ("rabbit" "visits" "lion" "+")) -> ("lion" "likes" "rabbit" "+"))
If someone is cold then they are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If the rabbit is rough and the rabbit visits the lion then the rabbit is round.
((("rabbit" "is" "rough" "+") ("rabbit" "visits" "lion" "+")) -> ("rabbit" "is" "round" "+"))
If someone likes the mouse and the mouse needs the squirrel then they need the squirrel.
((("someone" "likes" "mouse" "+") ("mouse" "needs" "squirrel" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone needs the rabbit and they visit the lion then the rabbit visits the lion.
((("someone" "needs" "rabbit" "+") ("someone" "visits" "lion" "+")) -> ("rabbit" "visits" "lion" "+"))
If someone likes the squirrel then the squirrel likes the rabbit.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "likes" "rabbit" "+"))
If someone is round then they visit the lion.
((("someone" "is" "round" "+")) -> ("someone" "visits" "lion" "+"))
The squirrel visits the lion.
True
1
proof
[(triple11)]
("squirrel" "visits" "lion" "+")
triple11
The lion does not visit the mouse.
False
1
inv-proof
[(triple4)]
("lion" "visits" "mouse" "-")
triple4
The squirrel is kind.
True
2
proof
[(((triple9) -> rule3))]
("squirrel" "is" "kind" "+")
((triple9) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is not kind.
False
2
inv-proof
[(((triple9) -> rule3))]
("squirrel" "is" "kind" "-")
((triple9) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel needs the mouse.
True
3
proof
[(((((triple9) -> rule3)) -> rule1))]
("squirrel" "needs" "mouse" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel does not need the mouse.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule1))]
("squirrel" "needs" "mouse" "-")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The rabbit is not round.
Unknown
inv-rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "round" "-")
The squirrel likes the rabbit.
Unknown
rconc
[@1: The squirrel likes the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "likes" "rabbit" "+")
The rabbit is not kind.
Unknown
inv-rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "kind" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The lion is rough.[(triple1)] The lion likes the mouse.[(triple2)] The lion needs the squirrel.[(triple3)] The lion visits the mouse.[(triple4)] The mouse needs the lion.[(triple5)] The rabbit needs the mouse.[(triple6)] The rabbit visits the lion.[(triple7)] The rabbit visits the squirrel.[(triple8)] The squirrel is cold.[(triple9)] The squirrel needs the lion.[(triple10)] The squirrel visits the lion.[(triple11)] The squirrel visits the rabbit.[(triple12)] @1: The squirrel is kind.[(((triple9) -> rule3))] @2: The squirrel needs the mouse.[(((((triple9) -> rule3)) -> rule1))]
The lion is rough.
("lion" "is" "rough" "+")
triple1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple3
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple4
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple5
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple6
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple7
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple10
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple11
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple12
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple9) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2