The cow chases the dog. The cow eats the dog. The cow is kind. The cow is red. The cow is young. The cow does not need the dog. The dog chases the cow. The dog eats the cow. The dog is big. The dog is red. The dog is young. The dog needs the cow. If someone is blue then they chase the cow. If someone needs the dog and the dog does not eat the cow then they chase the dog. If someone chases the cow then they do not chase the dog. If someone is big and they need the cow then they are red. If the dog eats the cow and the cow eats the dog then the cow is kind. If the cow needs the dog then the dog chases the cow. If someone eats the cow and the cow is big then the cow does not chase the dog. If someone chases the cow and the cow needs the dog then the dog does not need the cow.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
The cow does not need the dog.
("cow" "needs" "dog" "-")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
If someone is blue then they chase the cow.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "cow" "+"))
If someone needs the dog and the dog does not eat the cow then they chase the dog.
((("someone" "needs" "dog" "+") ("dog" "eats" "cow" "~")) -> ("someone" "chases" "dog" "+"))
If someone chases the cow then they do not chase the dog.
((("someone" "chases" "cow" "+")) -> ("someone" "chases" "dog" "-"))
If someone is big and they need the cow then they are red.
((("someone" "is" "big" "+") ("someone" "needs" "cow" "+")) -> ("someone" "is" "red" "+"))
If the dog eats the cow and the cow eats the dog then the cow is kind.
((("dog" "eats" "cow" "+") ("cow" "eats" "dog" "+")) -> ("cow" "is" "kind" "+"))
If the cow needs the dog then the dog chases the cow.
((("cow" "needs" "dog" "+")) -> ("dog" "chases" "cow" "+"))
If someone eats the cow and the cow is big then the cow does not chase the dog.
((("someone" "eats" "cow" "+") ("cow" "is" "big" "+")) -> ("cow" "chases" "dog" "-"))
If someone chases the cow and the cow needs the dog then the dog does not need the cow.
((("someone" "chases" "cow" "+") ("cow" "needs" "dog" "+")) -> ("dog" "needs" "cow" "-"))
The dog is red.
True
1
proof
[(triple10 OR ((triple9 triple12) -> rule4))]
("dog" "is" "red" "+")
triple10
((triple9 triple12) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is not young.
False
1
inv-proof
[(triple11)]
("dog" "is" "young" "-")
triple11
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "cow" "-")
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 chases the dog.[(triple1)] The cow does not need the dog.[(triple6)] The cow eats the dog.[(triple2)] The cow is kind.[(triple3 OR ((triple8 triple2) -> rule5))] The cow is red.[(triple4)] The cow is young.[(triple5)] The dog chases the cow.[(triple7)] The dog eats the cow.[(triple8)] The dog is big.[(triple9)] The dog is red.[(triple10 OR ((triple9 triple12) -> rule4))] The dog is young.[(triple11)] The dog needs the cow.[(triple12)] @1: The dog does not chase the dog.[(((triple7) -> rule3))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow does not need the dog.
("cow" "needs" "dog" "-")
triple6
The cow eats the dog.
("cow" "eats" "dog" "+")
triple2
The cow is kind.
("cow" "is" "kind" "+")
triple3
((triple8 triple2) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The dog chases the cow.
("dog" "chases" "cow" "+")
triple7
The dog eats the cow.
("dog" "eats" "cow" "+")
triple8
The dog is big.
("dog" "is" "big" "+")
triple9
The dog is red.
("dog" "is" "red" "+")
triple10
((triple9 triple12) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
triple11
The dog needs the cow.
("dog" "needs" "cow" "+")
triple12
The dog does not chase the dog.
("dog" "chases" "dog" "-")
((triple7) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1