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