The cat does not chase the dog. The cat is not big. The cat is not rough. The cat sees the dog. The dog chases the cat. The dog is cold. The dog is not green. The dog is rough. The dog likes the cat. The dog sees the cat. If someone is cold and not rough then they see the cat. If someone sees the dog then they do not see the cat. If the cat sees the dog and the cat is big then the cat does not like the dog.
The cat does not chase the dog.
("cat" "chases" "dog" "-")
The cat is not big.
("cat" "is" "big" "-")
The cat is not rough.
("cat" "is" "rough" "-")
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is not green.
("dog" "is" "green" "-")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
If someone is cold and not rough then they see the cat.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "~")) -> ("someone" "sees" "cat" "+"))
If someone sees the dog then they do not see the cat.
((("someone" "sees" "dog" "+")) -> ("someone" "sees" "cat" "-"))
If the cat sees the dog and the cat is big then the cat does not like the dog.
((("cat" "sees" "dog" "+") ("cat" "is" "big" "+")) -> ("cat" "likes" "dog" "-"))
The cat is not big.
True
1
proof
[(triple2)]
("cat" "is" "big" "-")
triple2
The dog does not chase the cat.
False
1
inv-proof
[(triple5)]
("dog" "chases" "cat" "-")
triple5
The cat does not see the cat.
True
2
proof
[(((triple4) -> rule2))]
("cat" "sees" "cat" "-")
((triple4) -> (rule2 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1
The cat sees the cat.
False
2
inv-proof
[(((triple4) -> rule2))]
("cat" "sees" "cat" "+")
((triple4) -> (rule2 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The cat does not chase the dog.[(triple1)] The cat is not big.[(triple2)] The cat is not rough.[(triple3)] The cat sees the dog.[(triple4)] The dog chases the cat.[(triple5)] The dog is cold.[(triple6)] The dog is not green.[(triple7)] The dog is rough.[(triple8)] The dog likes the cat.[(triple9)] The dog sees the cat.[(triple10)] @1: The cat does not see the cat.[(((triple4) -> rule2))]
The cat does not chase the dog.
("cat" "chases" "dog" "-")
triple1
The cat is not big.
("cat" "is" "big" "-")
triple2
The cat is not rough.
("cat" "is" "rough" "-")
triple3
The cat sees the dog.
("cat" "sees" "dog" "+")
triple4
The dog chases the cat.
("dog" "chases" "cat" "+")
triple5
The dog is cold.
("dog" "is" "cold" "+")
triple6
The dog is not green.
("dog" "is" "green" "-")
triple7
The dog is rough.
("dog" "is" "rough" "+")
triple8
The dog likes the cat.
("dog" "likes" "cat" "+")
triple9
The dog sees the cat.
("dog" "sees" "cat" "+")
triple10
The cat does not see the cat.
("cat" "sees" "cat" "-")
((triple4) -> (rule2 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1