The cat eats the cow. The cat is kind. The cow does not chase the rabbit. The cow is big. The cow needs the rabbit. The rabbit needs the cat. The rabbit needs the cow. If someone eats the cow then they eat the cat. If someone needs the rabbit then the rabbit does not eat the cat. If the cat is kind then the cat is big. If someone eats the cow and they are young then they are round. If someone chases the cat and the cat does not eat the cow then the cat does not need the cow. If the cat eats the cow then the cow does not chase the cat.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cow does not chase the rabbit.
("cow" "chases" "rabbit" "-")
The cow is big.
("cow" "is" "big" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
If someone eats the cow then they eat the cat.
((("someone" "eats" "cow" "+")) -> ("someone" "eats" "cat" "+"))
If someone needs the rabbit then the rabbit does not eat the cat.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "eats" "cat" "-"))
If the cat is kind then the cat is big.
((("cat" "is" "kind" "+")) -> ("cat" "is" "big" "+"))
If someone eats the cow and they are young then they are round.
((("someone" "eats" "cow" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone chases the cat and the cat does not eat the cow then the cat does not need the cow.
((("someone" "chases" "cat" "+") ("cat" "eats" "cow" "~")) -> ("cat" "needs" "cow" "-"))
If the cat eats the cow then the cow does not chase the cat.
((("cat" "eats" "cow" "+")) -> ("cow" "chases" "cat" "-"))
The cat eats the cow.
True
1
proof
[(triple1)]
("cat" "eats" "cow" "+")
triple1
The cat is not kind.
False
1
inv-proof
[(triple2)]
("cat" "is" "kind" "-")
triple2
The cow does not eat the cat.
Unknown
inv-rconc
[@1: The cow eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "cat" "-")
The cat chases the cow.
Unknown
random
[@0: The cat chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cow" "+")
@0: The cat eats the cow.[(triple1)] The cat is kind.[(triple2)] The cow does not chase the rabbit.[(triple3)] The cow is big.[(triple4)] The cow needs the rabbit.[(triple5)] The rabbit needs the cat.[(triple6)] The rabbit needs the cow.[(triple7)] @1: The cat eats the cat.[(((triple1) -> rule1))] The cat is big.[(((triple2) -> rule3))] The cow does not chase the cat.[(((triple1) -> rule6))] The rabbit does not eat the cat.[(((triple5) -> rule2))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cow does not chase the rabbit.
("cow" "chases" "rabbit" "-")
triple3
The cow is big.
("cow" "is" "big" "+")
triple4
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple5
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple6
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple7
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple1) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
((triple2) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cow does not chase the cat.
("cow" "chases" "cat" "-")
((triple1) -> (rule6 % int1))
The cow does not chase the cat.
("cow" "chases" "cat" "-")
int1
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
((triple5) -> (rule2 % int1))
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
int1