The cat is blue. The cat needs the dog. The cat does not see the dog. The cow does not chase the dog. The cow is big. The cow is kind. The cow needs the cat. The cow needs the dog. The cow sees the cat. The cow sees the dog. The dog is blue. The dog is young. The dog needs the cow. The dog sees the cat. The dog sees the cow. If the cow is kind then the cow is blue. If the cow sees the dog then the dog needs the cat. If someone sees the dog then the dog does not chase the cow. If the dog needs the cow then the dog chases the cat. If someone is big then they do not need the cow. If someone is kind and they do not chase the cat then the cat does not see the cow.
The cat is blue.
("cat" "is" "blue" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat does not see the dog.
("cat" "sees" "dog" "-")
The cow does not chase the dog.
("cow" "chases" "dog" "-")
The cow is big.
("cow" "is" "big" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
If the cow is kind then the cow is blue.
((("cow" "is" "kind" "+")) -> ("cow" "is" "blue" "+"))
If the cow sees the dog then the dog needs the cat.
((("cow" "sees" "dog" "+")) -> ("dog" "needs" "cat" "+"))
If someone sees the dog then the dog does not chase the cow.
((("someone" "sees" "dog" "+")) -> ("dog" "chases" "cow" "-"))
If the dog needs the cow then the dog chases the cat.
((("dog" "needs" "cow" "+")) -> ("dog" "chases" "cat" "+"))
If someone is big then they do not need the cow.
((("someone" "is" "big" "+")) -> ("someone" "needs" "cow" "-"))
If someone is kind and they do not chase the cat then the cat does not see the cow.
((("someone" "is" "kind" "+") ("someone" "chases" "cat" "~")) -> ("cat" "sees" "cow" "-"))
The dog sees the cat.
True
1
proof
[(triple14)]
("dog" "sees" "cat" "+")
triple14
The cow does not see the cat.
False
1
inv-proof
[(triple9)]
("cow" "sees" "cat" "-")
triple9
The cow is blue.
True
2
proof
[(((triple6) -> rule1))]
("cow" "is" "blue" "+")
((triple6) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is not blue.
False
2
inv-proof
[(((triple6) -> rule1))]
("cow" "is" "blue" "-")
((triple6) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The cat does not see the dog.[(triple3)] The cat is blue.[(triple1)] The cat needs the dog.[(triple2)] The cow does not chase the dog.[(triple4)] The cow is big.[(triple5)] The cow is kind.[(triple6)] The cow needs the cat.[(triple7)] The cow needs the dog.[(triple8)] The cow sees the cat.[(triple9)] The cow sees the dog.[(triple10)] The dog is blue.[(triple11)] The dog is young.[(triple12)] The dog needs the cow.[(triple13)] The dog sees the cat.[(triple14)] The dog sees the cow.[(triple15)] @1: The cow does not need the cow.[(((triple5) -> rule5))] The cow is blue.[(((triple6) -> rule1))] The dog chases the cat.[(((triple13) -> rule4))] The dog does not chase the cow.[(((triple10) -> rule3))] The dog needs the cat.[(((triple10) -> rule2))]
The cat does not see the dog.
("cat" "sees" "dog" "-")
triple3
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple2
The cow does not chase the dog.
("cow" "chases" "dog" "-")
triple4
The cow is big.
("cow" "is" "big" "+")
triple5
The cow is kind.
("cow" "is" "kind" "+")
triple6
The cow needs the cat.
("cow" "needs" "cat" "+")
triple7
The cow needs the dog.
("cow" "needs" "dog" "+")
triple8
The cow sees the cat.
("cow" "sees" "cat" "+")
triple9
The cow sees the dog.
("cow" "sees" "dog" "+")
triple10
The dog is blue.
("dog" "is" "blue" "+")
triple11
The dog is young.
("dog" "is" "young" "+")
triple12
The dog needs the cow.
("dog" "needs" "cow" "+")
triple13
The dog sees the cat.
("dog" "sees" "cat" "+")
triple14
The dog sees the cow.
("dog" "sees" "cow" "+")
triple15
The cow does not need the cow.
("cow" "needs" "cow" "-")
((triple5) -> (rule5 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The cow is blue.
("cow" "is" "blue" "+")
((triple6) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
((triple13) -> (rule4 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog does not chase the cow.
("dog" "chases" "cow" "-")
((triple10) -> (rule3 % int1))
The dog does not chase the cow.
("dog" "chases" "cow" "-")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
((triple10) -> (rule2 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1