The bear is kind. The cat is rough. The squirrel is kind. If something likes the cat and the cat needs the squirrel then the cat is kind. If something likes the squirrel then it visits the bear. If something needs the bear then the bear needs the cat. If something is rough then it needs the cat. If something likes the squirrel then it visits the cat. If something needs the cat then it likes the squirrel. If something likes the bear then the bear needs the squirrel. If the cat needs the squirrel and the squirrel is rough then the squirrel needs the cat.
The bear is kind.
("bear" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If something likes the cat and the cat needs the squirrel then the cat is kind.
((("something" "likes" "cat" "+") ("cat" "needs" "squirrel" "+")) -> ("cat" "is" "kind" "+"))
If something likes the squirrel then it visits the bear.
((("something" "likes" "squirrel" "+")) -> ("something" "visits" "bear" "+"))
If something needs the bear then the bear needs the cat.
((("something" "needs" "bear" "+")) -> ("bear" "needs" "cat" "+"))
If something is rough then it needs the cat.
((("something" "is" "rough" "+")) -> ("something" "needs" "cat" "+"))
If something likes the squirrel then it visits the cat.
((("something" "likes" "squirrel" "+")) -> ("something" "visits" "cat" "+"))
If something needs the cat then it likes the squirrel.
((("something" "needs" "cat" "+")) -> ("something" "likes" "squirrel" "+"))
If something likes the bear then the bear needs the squirrel.
((("something" "likes" "bear" "+")) -> ("bear" "needs" "squirrel" "+"))
If the cat needs the squirrel and the squirrel is rough then the squirrel needs the cat.
((("cat" "needs" "squirrel" "+") ("squirrel" "is" "rough" "+")) -> ("squirrel" "needs" "cat" "+"))
The bear is kind.
True
1
proof
[(triple1)]
("bear" "is" "kind" "+")
triple1
The squirrel is not kind.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "kind" "-")
triple3
The cat needs the cat.
True
2
proof
[(((triple2) -> rule4))]
("cat" "needs" "cat" "+")
((triple2) -> (rule4 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple2) -> rule4))]
("cat" "needs" "cat" "-")
((triple2) -> (rule4 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat likes the squirrel.
True
3
proof
[(((((triple2) -> rule4)) -> rule6))]
("cat" "likes" "squirrel" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat does not like the squirrel.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6))]
("cat" "likes" "squirrel" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat visits the cat.
True
4
proof
[(((((((triple2) -> rule4)) -> rule6)) -> rule5))]
("cat" "visits" "cat" "+")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The cat does not visit the cat.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule6)) -> rule5))]
("cat" "visits" "cat" "-")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The bear does not visit the cat.
Unknown
inv-rconc
[@3: The bear visits the cat.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule3 <- FAIL)]]
("bear" "visits" "cat" "-")
The cat is kind.
Unknown
rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "kind" "+")
The bear does not need the squirrel.
Unknown
inv-rconc
[@1: The bear needs the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "needs" "squirrel" "-")
The squirrel visits the cat.
Unknown
rconc
[@3: The squirrel visits the cat.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule4 <- FAIL)]]
("squirrel" "visits" "cat" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
The squirrel does not like the bear.
Unknown
inv-random
[@0: The squirrel likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "bear" "-")
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 is kind.[(triple1)] The cat is rough.[(triple2)] The squirrel is kind.[(triple3)] @1: The cat needs the cat.[(((triple2) -> rule4))] @2: The cat likes the squirrel.[(((((triple2) -> rule4)) -> rule6))] @3: The cat visits the bear.[(((((((triple2) -> rule4)) -> rule6)) -> rule2))] The cat visits the cat.[(((((((triple2) -> rule4)) -> rule6)) -> rule5))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple2) -> (rule4 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat visits the bear.
("cat" "visits" "bear" "+")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The cat visits the cat.
("cat" "visits" "cat" "+")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3