The cow eats the dog. The dog eats the cow. If someone likes the dog and the dog likes the cow then they eat the dog. If the dog likes the cow and the cow does not need the dog then the dog eats the cow. If the cow does not need the dog then the dog likes the cow. If someone eats the cow then they do not like the dog. If someone eats the dog and the dog eats the cow then they like the dog. If someone is red then they are not round.
The cow eats the dog.
("cow" "eats" "dog" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
If someone likes the dog and the dog likes the cow then they eat the dog.
((("someone" "likes" "dog" "+") ("dog" "likes" "cow" "+")) -> ("someone" "eats" "dog" "+"))
If the dog likes the cow and the cow does not need the dog then the dog eats the cow.
((("dog" "likes" "cow" "+") ("cow" "needs" "dog" "~")) -> ("dog" "eats" "cow" "+"))
If the cow does not need the dog then the dog likes the cow.
((("cow" "needs" "dog" "~")) -> ("dog" "likes" "cow" "+"))
If someone eats the cow then they do not like the dog.
((("someone" "eats" "cow" "+")) -> ("someone" "likes" "dog" "-"))
If someone eats the dog and the dog eats the cow then they like the dog.
((("someone" "eats" "dog" "+") ("dog" "eats" "cow" "+")) -> ("someone" "likes" "dog" "+"))
If someone is red then they are not round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "-"))
The cow eats the dog.
True
1
proof
[(triple1)]
("cow" "eats" "dog" "+")
triple1
The cow does not eat the dog.
False
1
inv-proof
[(triple1)]
("cow" "eats" "dog" "-")
triple1
The cow likes the dog.
True
3
proof
[(((triple1 triple2) -> rule5))]
("cow" "likes" "dog" "+")
((triple1 triple2) -> (rule5 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The dog likes the dog.
False
2
inv-proof
[(((triple2) -> rule4))]
("dog" "likes" "dog" "+")
((triple2) -> (rule4 % int1))
The dog does not like the dog.
("dog" "likes" "dog" "-")
int1
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "dog" "-")
The dog likes the cow.
Unknown
rconc
[@1: The dog likes the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "likes" "cow" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The cow eats the dog.[(triple1)] The dog eats the cow.[(triple2)] @1: The cow likes the dog.[(((triple1 triple2) -> rule5))] The dog does not like the dog.[(((triple2) -> rule4))]
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The dog eats the cow.
("dog" "eats" "cow" "+")
triple2
The cow likes the dog.
("cow" "likes" "dog" "+")
((triple1 triple2) -> (rule5 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The dog does not like the dog.
("dog" "likes" "dog" "-")
((triple2) -> (rule4 % int1))
The dog does not like the dog.
("dog" "likes" "dog" "-")
int1