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