The cat is nice. The cat sees the dog. The cat visits the dog. The dog is blue. The dog is cold. The dog likes the cat. The dog does not see the cat. If something is red then it likes the dog. If something likes the dog and the dog is nice then the dog visits the cat. If the cat is not cold and the cat is not red then the cat visits the dog. If something is blue and it visits the dog then it does not see the dog. If something visits the dog then it likes the cat. If the dog sees the cat and the dog visits the cat then the dog is blue.
The cat is nice.
("cat" "is" "nice" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog does not see the cat.
("dog" "sees" "cat" "-")
If something is red then it likes the dog.
((("something" "is" "red" "+")) -> ("something" "likes" "dog" "+"))
If something likes the dog and the dog is nice then the dog visits the cat.
((("something" "likes" "dog" "+") ("dog" "is" "nice" "+")) -> ("dog" "visits" "cat" "+"))
If the cat is not cold and the cat is not red then the cat visits the dog.
((("cat" "is" "cold" "~") ("cat" "is" "red" "~")) -> ("cat" "visits" "dog" "+"))
If something is blue and it visits the dog then it does not see the dog.
((("something" "is" "blue" "+") ("something" "visits" "dog" "+")) -> ("something" "sees" "dog" "-"))
If something visits the dog then it likes the cat.
((("something" "visits" "dog" "+")) -> ("something" "likes" "cat" "+"))
If the dog sees the cat and the dog visits the cat then the dog is blue.
((("dog" "sees" "cat" "+") ("dog" "visits" "cat" "+")) -> ("dog" "is" "blue" "+"))
The cat is nice.
True
1
proof
[(triple1)]
("cat" "is" "nice" "+")
triple1
The cat does not see the dog.
False
1
inv-proof
[(triple2)]
("cat" "sees" "dog" "-")
triple2
The cat likes the cat.
True
2
proof
[(((triple3) -> rule5))]
("cat" "likes" "cat" "+")
((triple3) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat does not like the cat.
False
2
inv-proof
[(((triple3) -> rule5))]
("cat" "likes" "cat" "-")
((triple3) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The dog does not visit the cat.
Unknown
inv-rconc
[@1: The dog visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "visits" "cat" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "dog" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The cat is nice.[(triple1)] The cat sees the dog.[(triple2)] The cat visits the dog.[(triple3)] The dog does not see the cat.[(triple7)] The dog is blue.[(triple4)] The dog is cold.[(triple5)] The dog likes the cat.[(triple6)] @1: The cat likes the cat.[(((triple3) -> rule5))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat sees the dog.
("cat" "sees" "dog" "+")
triple2
The cat visits the dog.
("cat" "visits" "dog" "+")
triple3
The dog does not see the cat.
("dog" "sees" "cat" "-")
triple7
The dog is blue.
("dog" "is" "blue" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog likes the cat.
("dog" "likes" "cat" "+")
triple6
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple3) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1