The lion is blue. The lion needs the rabbit. The lion sees the rabbit. The lion visits the rabbit. The rabbit is kind. The rabbit is red. The rabbit is rough. The rabbit sees the lion. The rabbit visits the squirrel. The squirrel is blue. The squirrel needs the rabbit. The squirrel visits the lion. If the lion needs the squirrel then the lion is blue. If something is round then it visits the squirrel. If something sees the rabbit then it visits the lion.
The lion is blue.
("lion" "is" "blue" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If the lion needs the squirrel then the lion is blue.
((("lion" "needs" "squirrel" "+")) -> ("lion" "is" "blue" "+"))
If something is round then it visits the squirrel.
((("something" "is" "round" "+")) -> ("something" "visits" "squirrel" "+"))
If something sees the rabbit then it visits the lion.
((("something" "sees" "rabbit" "+")) -> ("something" "visits" "lion" "+"))
The rabbit is kind.
True
1
proof
[(triple5)]
("rabbit" "is" "kind" "+")
triple5
The rabbit is not kind.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "kind" "-")
triple5
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
@0: The lion is blue.[(triple1)] The lion needs the rabbit.[(triple2)] The lion sees the rabbit.[(triple3)] The lion visits the rabbit.[(triple4)] The rabbit is kind.[(triple5)] The rabbit is red.[(triple6)] The rabbit is rough.[(triple7)] The rabbit sees the lion.[(triple8)] The rabbit visits the squirrel.[(triple9)] The squirrel is blue.[(triple10)] The squirrel needs the rabbit.[(triple11)] The squirrel visits the lion.[(triple12)] @1: The lion visits the lion.[(((triple3) -> rule3))]
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple3
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple4
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple5
The rabbit is red.
("rabbit" "is" "red" "+")
triple6
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple7
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple8
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple11
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple12
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple3) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1