The bear is blue. The bear visits the cat. The cat likes the bear. If something likes the bear then it sees the cat.
The bear is blue.
("bear" "is" "blue" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
If something likes the bear then it sees the cat.
((("something" "likes" "bear" "+")) -> ("something" "sees" "cat" "+"))
The bear visits the cat.
True
1
proof
[(triple2)]
("bear" "visits" "cat" "+")
triple2
The cat does not like the bear.
False
1
inv-proof
[(triple3)]
("cat" "likes" "bear" "-")
triple3
The cat sees the cat.
True
2
proof
[(((triple3) -> rule1))]
("cat" "sees" "cat" "+")
((triple3) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "sees" "cat" "-")
((triple3) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The bear does not see the cat.
Unknown
inv-rconc
[@1: The bear sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "cat" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is blue.[(triple1)] The bear visits the cat.[(triple2)] The cat likes the bear.[(triple3)] @1: The cat sees the cat.[(((triple3) -> rule1))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear visits the cat.
("bear" "visits" "cat" "+")
triple2
The cat likes the bear.
("cat" "likes" "bear" "+")
triple3
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple3) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1