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