The cow likes the rabbit. The rabbit likes the cow. The rabbit visits the cow. If something is cold and it visits the cow then it eats the cow. If something is young and it visits the cow then the cow eats the rabbit. If something eats the cow then the cow is big. If the rabbit likes the cow and the cow likes the rabbit then the rabbit eats the cow. If something visits the cow then it eats the cow. If something is cold and it eats the rabbit then the rabbit likes the cow.
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If something is cold and it visits the cow then it eats the cow.
((("something" "is" "cold" "+") ("something" "visits" "cow" "+")) -> ("something" "eats" "cow" "+"))
If something is young and it visits the cow then the cow eats the rabbit.
((("something" "is" "young" "+") ("something" "visits" "cow" "+")) -> ("cow" "eats" "rabbit" "+"))
If something eats the cow then the cow is big.
((("something" "eats" "cow" "+")) -> ("cow" "is" "big" "+"))
If the rabbit likes the cow and the cow likes the rabbit then the rabbit eats the cow.
((("rabbit" "likes" "cow" "+") ("cow" "likes" "rabbit" "+")) -> ("rabbit" "eats" "cow" "+"))
If something visits the cow then it eats the cow.
((("something" "visits" "cow" "+")) -> ("something" "eats" "cow" "+"))
If something is cold and it eats the rabbit then the rabbit likes the cow.
((("something" "is" "cold" "+") ("something" "eats" "rabbit" "+")) -> ("rabbit" "likes" "cow" "+"))
The rabbit visits the cow.
True
1
proof
[(triple3)]
("rabbit" "visits" "cow" "+")
triple3
The rabbit does not like the cow.
False
1
inv-proof
[(triple2)]
("rabbit" "likes" "cow" "-")
triple2
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "cow" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The cow likes the rabbit.[(triple1)] The rabbit likes the cow.[(triple2)] The rabbit visits the cow.[(triple3)] @1: The rabbit eats the cow.[(((triple3) -> rule5) OR ((triple2 triple1) -> rule4))] @2: The cow is big.[(((((triple3) -> rule5)) -> rule3) OR ((((triple2 triple1) -> rule4)) -> rule3))]
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple1
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple3
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
((triple3) -> (rule5 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
((triple2 triple1) -> (rule4 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
((((triple2 triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2