The bear visits the cat. The cat chases the bear. The cat is nice. If something is red then it likes the bear. If something chases the cat and it visits the cat then it likes the cat. If something chases the bear then it visits the cat.
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat is nice.
("cat" "is" "nice" "+")
If something is red then it likes the bear.
((("something" "is" "red" "+")) -> ("something" "likes" "bear" "+"))
If something chases the cat and it visits the cat then it likes the cat.
((("something" "chases" "cat" "+") ("something" "visits" "cat" "+")) -> ("something" "likes" "cat" "+"))
If something chases the bear then it visits the cat.
((("something" "chases" "bear" "+")) -> ("something" "visits" "cat" "+"))
The cat is nice.
True
1
proof
[(triple3)]
("cat" "is" "nice" "+")
triple3
The cat is not nice.
False
1
inv-proof
[(triple3)]
("cat" "is" "nice" "-")
triple3
The cat visits the cat.
True
2
proof
[(((triple2) -> rule3))]
("cat" "visits" "cat" "+")
((triple2) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple2) -> rule3))]
("cat" "visits" "cat" "-")
((triple2) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not like the bear.
Unknown
inv-rconc
[@1: The cat likes the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "bear" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "cat" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The bear visits the cat.[(triple1)] The cat chases the bear.[(triple2)] The cat is nice.[(triple3)] @1: The cat visits the cat.[(((triple2) -> rule3))]
The bear visits the cat.
("bear" "visits" "cat" "+")
triple1
The cat chases the bear.
("cat" "chases" "bear" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple2) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1