The bear does not eat the lion. The bear eats the squirrel. The bear visits the lion. The dog is kind. The lion eats the bear. The lion is blue. The squirrel eats the bear. The squirrel sees the dog. The squirrel sees the lion. The squirrel visits the lion. Big things are not blue. If something sees the bear then the bear eats the squirrel. If something sees the lion and the lion sees the bear then the lion visits the squirrel. If something sees the lion then the lion is blue. If something sees the lion then the lion does not visit the dog. If something eats the bear and it is cold then the bear sees the lion.
The bear does not eat the lion.
("bear" "eats" "lion" "-")
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The dog is kind.
("dog" "is" "kind" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion is blue.
("lion" "is" "blue" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
Big things are not blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "-"))
If something sees the bear then the bear eats the squirrel.
((("something" "sees" "bear" "+")) -> ("bear" "eats" "squirrel" "+"))
If something sees the lion and the lion sees the bear then the lion visits the squirrel.
((("something" "sees" "lion" "+") ("lion" "sees" "bear" "+")) -> ("lion" "visits" "squirrel" "+"))
If something sees the lion then the lion is blue.
((("something" "sees" "lion" "+")) -> ("lion" "is" "blue" "+"))
If something sees the lion then the lion does not visit the dog.
((("something" "sees" "lion" "+")) -> ("lion" "visits" "dog" "-"))
If something eats the bear and it is cold then the bear sees the lion.
((("something" "eats" "bear" "+") ("something" "is" "cold" "+")) -> ("bear" "sees" "lion" "+"))
The squirrel visits the lion.
True
1
proof
[(triple10)]
("squirrel" "visits" "lion" "+")
triple10
The dog is not kind.
False
1
inv-proof
[(triple4)]
("dog" "is" "kind" "-")
triple4
The lion does not visit the dog.
True
2
proof
[(((triple9) -> rule5))]
("lion" "visits" "dog" "-")
((triple9) -> (rule5 % int1))
The lion does not visit the dog.
("lion" "visits" "dog" "-")
int1
The lion visits the dog.
False
2
inv-proof
[(((triple9) -> rule5))]
("lion" "visits" "dog" "+")
((triple9) -> (rule5 % int1))
The lion does not visit the dog.
("lion" "visits" "dog" "-")
int1
The bear does not see the lion.
Unknown
inv-rconc
[@1: The bear sees the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "sees" "lion" "-")
The lion visits the squirrel.
Unknown
rconc
[@1: The lion visits the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "squirrel" "+")
The dog does not see the lion.
Unknown
inv-random
[@0: The dog sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "lion" "-")
The dog eats the lion.
Unknown
random
[@0: The dog eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "lion" "+")
@0: The bear does not eat the lion.[(triple1)] The bear eats the squirrel.[(triple2)] The bear visits the lion.[(triple3)] The dog is kind.[(triple4)] The lion eats the bear.[(triple5)] The lion is blue.[(triple6 OR ((triple9) -> rule4))] The squirrel eats the bear.[(triple7)] The squirrel sees the dog.[(triple8)] The squirrel sees the lion.[(triple9)] The squirrel visits the lion.[(triple10)] @1: The lion does not visit the dog.[(((triple9) -> rule5))]
The bear does not eat the lion.
("bear" "eats" "lion" "-")
triple1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple2
The bear visits the lion.
("bear" "visits" "lion" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The lion eats the bear.
("lion" "eats" "bear" "+")
triple5
The lion is blue.
("lion" "is" "blue" "+")
triple6
((triple9) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple7
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple8
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple9
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple10
The lion does not visit the dog.
("lion" "visits" "dog" "-")
((triple9) -> (rule5 % int1))
The lion does not visit the dog.
("lion" "visits" "dog" "-")
int1