The bear does not like the cat. The cat needs the squirrel. The lion does not see the cat. The lion does not see the squirrel. The squirrel needs the bear. The squirrel does not need the cat. The squirrel sees the cat. If something is kind then it needs the bear. If something is blue and green then it sees the bear. If the squirrel likes the bear then the squirrel is kind. If something needs the bear then the bear likes the lion. If something is kind then it sees the cat. If the lion sees the squirrel then the lion is green. If something likes the cat then it needs the lion. If something likes the lion then the lion likes the cat.
The bear does not like the cat.
("bear" "likes" "cat" "-")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The lion does not see the cat.
("lion" "sees" "cat" "-")
The lion does not see the squirrel.
("lion" "sees" "squirrel" "-")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If something is kind then it needs the bear.
((("something" "is" "kind" "+")) -> ("something" "needs" "bear" "+"))
If something is blue and green then it sees the bear.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "sees" "bear" "+"))
If the squirrel likes the bear then the squirrel is kind.
((("squirrel" "likes" "bear" "+")) -> ("squirrel" "is" "kind" "+"))
If something needs the bear then the bear likes the lion.
((("something" "needs" "bear" "+")) -> ("bear" "likes" "lion" "+"))
If something is kind then it sees the cat.
((("something" "is" "kind" "+")) -> ("something" "sees" "cat" "+"))
If the lion sees the squirrel then the lion is green.
((("lion" "sees" "squirrel" "+")) -> ("lion" "is" "green" "+"))
If something likes the cat then it needs the lion.
((("something" "likes" "cat" "+")) -> ("something" "needs" "lion" "+"))
If something likes the lion then the lion likes the cat.
((("something" "likes" "lion" "+")) -> ("lion" "likes" "cat" "+"))
The lion does not see the squirrel.
True
1
proof
[(triple4)]
("lion" "sees" "squirrel" "-")
triple4
The squirrel needs the cat.
False
1
inv-proof
[(triple6)]
("squirrel" "needs" "cat" "+")
triple6
The bear likes the lion.
True
2
proof
[(((triple5) -> rule4))]
("bear" "likes" "lion" "+")
((triple5) -> (rule4 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The bear does not like the lion.
False
2
inv-proof
[(((triple5) -> rule4))]
("bear" "likes" "lion" "-")
((triple5) -> (rule4 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The lion likes the cat.
True
3
proof
[(((((triple5) -> rule4)) -> rule8))]
("lion" "likes" "cat" "+")
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The bear likes the lion.
("bear" "likes" "lion" "+")
int2
The lion does not like the cat.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule8))]
("lion" "likes" "cat" "-")
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The bear likes the lion.
("bear" "likes" "lion" "+")
int2
The lion needs the lion.
True
4
proof
[(((((((triple5) -> rule4)) -> rule8)) -> rule7))]
("lion" "needs" "lion" "+")
((((((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The bear likes the lion.
("bear" "likes" "lion" "+")
int3
The lion does not need the lion.
False
4
inv-proof
[(((((((triple5) -> rule4)) -> rule8)) -> rule7))]
("lion" "needs" "lion" "-")
((((((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The bear likes the lion.
("bear" "likes" "lion" "+")
int3
The cat does not need the bear.
Unknown
inv-rconc
[@1: The cat needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "bear" "-")
The squirrel needs the lion.
Unknown
rconc
[@1: The squirrel needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "needs" "lion" "+")
The squirrel is not kind.
Unknown
inv-rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "kind" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "bear" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The bear does not see the squirrel.
Unknown
inv-random
[@0: The bear sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "squirrel" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear does not like the cat.[(triple1)] The cat needs the squirrel.[(triple2)] The lion does not see the cat.[(triple3)] The lion does not see the squirrel.[(triple4)] The squirrel does not need the cat.[(triple6)] The squirrel needs the bear.[(triple5)] The squirrel sees the cat.[(triple7)] @1: The bear likes the lion.[(((triple5) -> rule4))] @2: The lion likes the cat.[(((((triple5) -> rule4)) -> rule8))] @3: The lion needs the lion.[(((((((triple5) -> rule4)) -> rule8)) -> rule7))]
The bear does not like the cat.
("bear" "likes" "cat" "-")
triple1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple2
The lion does not see the cat.
("lion" "sees" "cat" "-")
triple3
The lion does not see the squirrel.
("lion" "sees" "squirrel" "-")
triple4
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
triple6
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple5
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple7
The bear likes the lion.
("bear" "likes" "lion" "+")
((triple5) -> (rule4 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The bear likes the lion.
("bear" "likes" "lion" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
((((((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The bear likes the lion.
("bear" "likes" "lion" "+")
int3