The bear eats the lion. The bear is not blue. The bear needs the squirrel. The cat is round. The cat visits the lion. The lion needs the bear. The lion does not need the cat. The squirrel eats the lion. The squirrel is cold. The squirrel is nice. The squirrel needs the bear. The squirrel visits the bear. If someone is nice then they eat the bear. If someone visits the cat and they are not green then they are nice. If someone is nice then they are blue. If someone visits the lion then the lion does not visit the squirrel. If someone eats the bear then they do not visit the lion. If the bear eats the lion then the bear needs the lion.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear is not blue.
("bear" "is" "blue" "-")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The cat is round.
("cat" "is" "round" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion does not need the cat.
("lion" "needs" "cat" "-")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If someone is nice then they eat the bear.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "bear" "+"))
If someone visits the cat and they are not green then they are nice.
((("someone" "visits" "cat" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone visits the lion then the lion does not visit the squirrel.
((("someone" "visits" "lion" "+")) -> ("lion" "visits" "squirrel" "-"))
If someone eats the bear then they do not visit the lion.
((("someone" "eats" "bear" "+")) -> ("someone" "visits" "lion" "-"))
If the bear eats the lion then the bear needs the lion.
((("bear" "eats" "lion" "+")) -> ("bear" "needs" "lion" "+"))
The cat visits the lion.
True
1
proof
[(triple5)]
("cat" "visits" "lion" "+")
triple5
The squirrel does not visit the bear.
False
1
inv-proof
[(triple12)]
("squirrel" "visits" "bear" "-")
triple12
The lion does not visit the squirrel.
True
2
proof
[(((triple5) -> rule4))]
("lion" "visits" "squirrel" "-")
((triple5) -> (rule4 % int1))
The lion does not visit the squirrel.
("lion" "visits" "squirrel" "-")
int1
The bear does not need the lion.
False
2
inv-proof
[(((triple1) -> rule6))]
("bear" "needs" "lion" "-")
((triple1) -> (rule6 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The squirrel does not visit the lion.
True
3
proof
[(((((triple10) -> rule1)) -> rule5))]
("squirrel" "visits" "lion" "-")
((((triple10) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel does not visit the lion.
("squirrel" "visits" "lion" "-")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The squirrel visits the lion.
False
3
inv-proof
[(((((triple10) -> rule1)) -> rule5))]
("squirrel" "visits" "lion" "+")
((((triple10) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel does not visit the lion.
("squirrel" "visits" "lion" "-")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The lion does not eat the bear.
Unknown
inv-rconc
[@2: The lion eats the bear.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("lion" "eats" "bear" "-")
The cat is blue.
Unknown
rconc
[@2: The cat is blue.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("cat" "is" "blue" "+")
The cat does not eat the bear.
Unknown
inv-rconc
[@2: The cat eats the bear.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("cat" "eats" "bear" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
The lion does not visit the cat.
Unknown
inv-random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The bear eats the lion.[(triple1)] The bear is not blue.[(triple2)] The bear needs the squirrel.[(triple3)] The cat is round.[(triple4)] The cat visits the lion.[(triple5)] The lion does not need the cat.[(triple7)] The lion needs the bear.[(triple6)] The squirrel eats the lion.[(triple8)] The squirrel is cold.[(triple9)] The squirrel is nice.[(triple10)] The squirrel needs the bear.[(triple11)] The squirrel visits the bear.[(triple12)] @1: The bear needs the lion.[(((triple1) -> rule6))] The lion does not visit the squirrel.[(((triple5) -> rule4))] The squirrel eats the bear.[(((triple10) -> rule1))] The squirrel is blue.[(((triple10) -> rule3))] @2: The squirrel does not visit the lion.[(((((triple10) -> rule1)) -> rule5))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear is not blue.
("bear" "is" "blue" "-")
triple2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat visits the lion.
("cat" "visits" "lion" "+")
triple5
The lion does not need the cat.
("lion" "needs" "cat" "-")
triple7
The lion needs the bear.
("lion" "needs" "bear" "+")
triple6
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple10
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple11
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple12
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple1) -> (rule6 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The lion does not visit the squirrel.
("lion" "visits" "squirrel" "-")
((triple5) -> (rule4 % int1))
The lion does not visit the squirrel.
("lion" "visits" "squirrel" "-")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
((triple10) -> (rule1 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple10) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel does not visit the lion.
("squirrel" "visits" "lion" "-")
((((triple10) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel does not visit the lion.
("squirrel" "visits" "lion" "-")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2