The cat eats the rabbit. The cow is big. The rabbit eats the cow. The rabbit is kind. The rabbit does not like the cat. The rabbit likes the cow. The rabbit sees the cow. If the cat is kind then the cat is not round. If someone likes the cow then the cow sees the rabbit. If the cat is nice then the cat eats the rabbit. If someone likes the cat then the cat eats the rabbit. If the cat is round then the cat does not like the cow. If someone eats the cow then they see the rabbit. If the rabbit sees the cow then the cow is nice. If the cow is not nice then the cow is not kind.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cow is big.
("cow" "is" "big" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit does not like the cat.
("rabbit" "likes" "cat" "-")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If the cat is kind then the cat is not round.
((("cat" "is" "kind" "+")) -> ("cat" "is" "round" "-"))
If someone likes the cow then the cow sees the rabbit.
((("someone" "likes" "cow" "+")) -> ("cow" "sees" "rabbit" "+"))
If the cat is nice then the cat eats the rabbit.
((("cat" "is" "nice" "+")) -> ("cat" "eats" "rabbit" "+"))
If someone likes the cat then the cat eats the rabbit.
((("someone" "likes" "cat" "+")) -> ("cat" "eats" "rabbit" "+"))
If the cat is round then the cat does not like the cow.
((("cat" "is" "round" "+")) -> ("cat" "likes" "cow" "-"))
If someone eats the cow then they see the rabbit.
((("someone" "eats" "cow" "+")) -> ("someone" "sees" "rabbit" "+"))
If the rabbit sees the cow then the cow is nice.
((("rabbit" "sees" "cow" "+")) -> ("cow" "is" "nice" "+"))
If the cow is not nice then the cow is not kind.
((("cow" "is" "nice" "~")) -> ("cow" "is" "kind" "-"))
The rabbit is kind.
True
1
proof
[(triple4)]
("rabbit" "is" "kind" "+")
triple4
The cat does not eat the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "eats" "rabbit" "-")
triple1
The cat does not see the rabbit.
Unknown
inv-rconc
[@1: The cat sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "rabbit" "-")
The cow eats the cat.
Unknown
random
[@0: The cow eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cat" "+")
@0: The cat eats the rabbit.[(triple1)] The cow is big.[(triple2)] The rabbit does not like the cat.[(triple5)] The rabbit eats the cow.[(triple3)] The rabbit is kind.[(triple4)] The rabbit likes the cow.[(triple6)] The rabbit sees the cow.[(triple7)] @1: The cow is nice.[(((triple7) -> rule7))] The cow sees the rabbit.[(((triple6) -> rule2))] The rabbit sees the rabbit.[(((triple3) -> rule6))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The rabbit does not like the cat.
("rabbit" "likes" "cat" "-")
triple5
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple6
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple7
The cow is nice.
("cow" "is" "nice" "+")
((triple7) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
((triple6) -> (rule2 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple3) -> (rule6 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1