The bear chases the squirrel. The cat chases the bear. The cat is cold. The lion chases the cat. The squirrel is cold. The squirrel needs the cat. The squirrel sees the cat. If someone sees the bear then the bear sees the squirrel. If someone sees the cat then the cat is kind. If someone needs the cat and they are big then the cat needs the squirrel. If someone is cold then they see the lion. If someone chases the squirrel then they are cold. If someone needs the bear then the bear is big.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat is cold.
("cat" "is" "cold" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If someone sees the bear then the bear sees the squirrel.
((("someone" "sees" "bear" "+")) -> ("bear" "sees" "squirrel" "+"))
If someone sees the cat then the cat is kind.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "kind" "+"))
If someone needs the cat and they are big then the cat needs the squirrel.
((("someone" "needs" "cat" "+") ("someone" "is" "big" "+")) -> ("cat" "needs" "squirrel" "+"))
If someone is cold then they see the lion.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "lion" "+"))
If someone chases the squirrel then they are cold.
((("someone" "chases" "squirrel" "+")) -> ("someone" "is" "cold" "+"))
If someone needs the bear then the bear is big.
((("someone" "needs" "bear" "+")) -> ("bear" "is" "big" "+"))
The squirrel is cold.
True
1
proof
[(triple5)]
("squirrel" "is" "cold" "+")
triple5
The squirrel does not see the cat.
False
1
inv-proof
[(triple7)]
("squirrel" "sees" "cat" "-")
triple7
The bear is cold.
True
2
proof
[(((triple1) -> rule5))]
("bear" "is" "cold" "+")
((triple1) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The cat is not kind.
False
2
inv-proof
[(((triple7) -> rule2))]
("cat" "is" "kind" "-")
((triple7) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The bear sees the lion.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("bear" "sees" "lion" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear does not see the lion.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("bear" "sees" "lion" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The cat does not need the squirrel.
Unknown
inv-rconc
[@1: The cat needs the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "needs" "squirrel" "-")
The bear sees the squirrel.
Unknown
rconc
[@1: The bear sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "squirrel" "+")
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "big" "-")
The lion chases the squirrel.
Unknown
random
[@0: The lion chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "squirrel" "+")
The lion does not see the cat.
Unknown
inv-random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "-")
The cat sees the squirrel.
Unknown
random
[@0: The cat sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "squirrel" "+")
@0: The bear chases the squirrel.[(triple1)] The cat chases the bear.[(triple2)] The cat is cold.[(triple3)] The lion chases the cat.[(triple4)] The squirrel is cold.[(triple5)] The squirrel needs the cat.[(triple6)] The squirrel sees the cat.[(triple7)] @1: The bear is cold.[(((triple1) -> rule5))] The cat is kind.[(((triple7) -> rule2))] The cat sees the lion.[(((triple3) -> rule4))] The squirrel sees the lion.[(((triple5) -> rule4))] @2: The bear sees the lion.[(((((triple1) -> rule5)) -> rule4))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The cat chases the bear.
("cat" "chases" "bear" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The lion chases the cat.
("lion" "chases" "cat" "+")
triple4
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple5
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple6
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple7
The bear is cold.
("bear" "is" "cold" "+")
((triple1) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
((triple7) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
((triple3) -> (rule4 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((triple5) -> (rule4 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2