The rabbit is kind. The squirrel eats the rabbit. The squirrel likes the rabbit. If someone eats the squirrel then they visit the squirrel. If someone likes the rabbit then the rabbit visits the squirrel. If someone likes the rabbit and the rabbit visits the squirrel then the rabbit likes the squirrel.
The rabbit is kind.
("rabbit" "is" "kind" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
If someone eats the squirrel then they visit the squirrel.
((("someone" "eats" "squirrel" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone likes the rabbit then the rabbit visits the squirrel.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "visits" "squirrel" "+"))
If someone likes the rabbit and the rabbit visits the squirrel then the rabbit likes the squirrel.
((("someone" "likes" "rabbit" "+") ("rabbit" "visits" "squirrel" "+")) -> ("rabbit" "likes" "squirrel" "+"))
The squirrel eats the rabbit.
True
1
proof
[(triple2)]
("squirrel" "eats" "rabbit" "+")
triple2
The rabbit is not kind.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "kind" "-")
triple1
The rabbit visits the squirrel.
True
2
proof
[(((triple3) -> rule2))]
("rabbit" "visits" "squirrel" "+")
((triple3) -> (rule2 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit does not visit the squirrel.
False
2
inv-proof
[(((triple3) -> rule2))]
("rabbit" "visits" "squirrel" "-")
((triple3) -> (rule2 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The rabbit is kind.[(triple1)] The squirrel eats the rabbit.[(triple2)] The squirrel likes the rabbit.[(triple3)] @1: The rabbit visits the squirrel.[(((triple3) -> rule2))] @2: The rabbit likes the squirrel.[(((triple3 ((triple3) -> rule2)) -> rule3))]
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple3
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
((triple3) -> (rule2 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2