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