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