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