The bear is nice. The cat is not green. The lion visits the cat. If someone eats the bear and the bear is cold then they do not visit the cat. If the cat chases the lion then the lion does not chase the bear. If someone is blue then they eat the bear. If the bear eats the lion and the lion is green then the lion does not visit the bear. If someone visits the cat then the cat does not eat the bear. If someone eats the bear then the bear chases the cat.
The bear is nice.
("bear" "is" "nice" "+")
The cat is not green.
("cat" "is" "green" "-")
The lion visits the cat.
("lion" "visits" "cat" "+")
If someone eats the bear and the bear is cold then they do not visit the cat.
((("someone" "eats" "bear" "+") ("bear" "is" "cold" "+")) -> ("someone" "visits" "cat" "-"))
If the cat chases the lion then the lion does not chase the bear.
((("cat" "chases" "lion" "+")) -> ("lion" "chases" "bear" "-"))
If someone is blue then they eat the bear.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "bear" "+"))
If the bear eats the lion and the lion is green then the lion does not visit the bear.
((("bear" "eats" "lion" "+") ("lion" "is" "green" "+")) -> ("lion" "visits" "bear" "-"))
If someone visits the cat then the cat does not eat the bear.
((("someone" "visits" "cat" "+")) -> ("cat" "eats" "bear" "-"))
If someone eats the bear then the bear chases the cat.
((("someone" "eats" "bear" "+")) -> ("bear" "chases" "cat" "+"))
The bear is nice.
True
1
proof
[(triple1)]
("bear" "is" "nice" "+")
triple1
The cat is green.
False
1
inv-proof
[(triple2)]
("cat" "is" "green" "+")
triple2
The cat does not eat the bear.
True
2
proof
[(((triple3) -> rule5))]
("cat" "eats" "bear" "-")
((triple3) -> (rule5 % int1))
The cat does not eat the bear.
("cat" "eats" "bear" "-")
int1
The cat eats the bear.
False
2
inv-proof
[(((triple3) -> rule5))]
("cat" "eats" "bear" "+")
((triple3) -> (rule5 % int1))
The cat does not eat the bear.
("cat" "eats" "bear" "-")
int1
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "eats" "bear" "-")
The bear chases the cat.
Unknown
rconc
[@2: The bear chases the cat.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("bear" "chases" "cat" "+")
The cat does not visit the lion.
Unknown
inv-random
[@0: The cat visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "lion" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The bear is nice.[(triple1)] The cat is not green.[(triple2)] The lion visits the cat.[(triple3)] @1: The cat does not eat the bear.[(((triple3) -> rule5))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The cat is not green.
("cat" "is" "green" "-")
triple2
The lion visits the cat.
("lion" "visits" "cat" "+")
triple3
The cat does not eat the bear.
("cat" "eats" "bear" "-")
((triple3) -> (rule5 % int1))
The cat does not eat the bear.
("cat" "eats" "bear" "-")
int1