The bear does not see the cat. The cat needs the squirrel. The squirrel needs the bear. If someone is blue then they do not chase the squirrel. If someone needs the cat then they chase the squirrel. If someone sees the squirrel and they see the bear then the squirrel is not cold. All red people are blue. If someone sees the cat then they do not need the bear. If someone sees the cat and they need the bear then the cat is cold. All kind people are young. If someone needs the squirrel then the squirrel is red.
The bear does not see the cat.
("bear" "sees" "cat" "-")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
If someone is blue then they do not chase the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "squirrel" "-"))
If someone needs the cat then they chase the squirrel.
((("someone" "needs" "cat" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone sees the squirrel and they see the bear then the squirrel is not cold.
((("someone" "sees" "squirrel" "+") ("someone" "sees" "bear" "+")) -> ("squirrel" "is" "cold" "-"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the cat then they do not need the bear.
((("someone" "sees" "cat" "+")) -> ("someone" "needs" "bear" "-"))
If someone sees the cat and they need the bear then the cat is cold.
((("someone" "sees" "cat" "+") ("someone" "needs" "bear" "+")) -> ("cat" "is" "cold" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone needs the squirrel then the squirrel is red.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
The squirrel needs the bear.
True
1
proof
[(triple3)]
("squirrel" "needs" "bear" "+")
triple3
The bear sees the cat.
False
1
inv-proof
[(triple1)]
("bear" "sees" "cat" "+")
triple1
The squirrel is red.
True
2
proof
[(((triple2) -> rule8))]
("squirrel" "is" "red" "+")
((triple2) -> (rule8 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is not red.
False
2
inv-proof
[(((triple2) -> rule8))]
("squirrel" "is" "red" "-")
((triple2) -> (rule8 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is blue.
True
3
proof
[(((((triple2) -> rule8)) -> rule4))]
("squirrel" "is" "blue" "+")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is not blue.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule4))]
("squirrel" "is" "blue" "-")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel does not chase the squirrel.
True
4
proof
[(((((((triple2) -> rule8)) -> rule4)) -> rule1))]
("squirrel" "chases" "squirrel" "-")
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel chases the squirrel.
False
4
inv-proof
[(((((((triple2) -> rule8)) -> rule4)) -> rule1))]
("squirrel" "chases" "squirrel" "+")
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The bear does not chase the squirrel.
Unknown
inv-rconc
[@1: The bear chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "chases" "squirrel" "-")
The bear is blue.
Unknown
rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "blue" "+")
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "young" "-")
The bear is young.
Unknown
rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "is" "young" "+")
The squirrel does not chase the cat.
Unknown
inv-random
[@0: The squirrel chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "cat" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The squirrel does not need the cat.
Unknown
inv-random
[@0: The squirrel needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cat" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The bear does not see the cat.[(triple1)] The cat needs the squirrel.[(triple2)] The squirrel needs the bear.[(triple3)] @1: The squirrel is red.[(((triple2) -> rule8))] @2: The squirrel is blue.[(((((triple2) -> rule8)) -> rule4))] @3: The squirrel does not chase the squirrel.[(((((((triple2) -> rule8)) -> rule4)) -> rule1))]
The bear does not see the cat.
("bear" "sees" "cat" "-")
triple1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple3
The squirrel is red.
("squirrel" "is" "red" "+")
((triple2) -> (rule8 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3