The bear eats the cat. The cat is not red. The squirrel is nice. If someone eats the squirrel and they are nice then the squirrel is not blue. If someone eats the bear and they are red then they like the cat. If someone needs the bear then they do not like the cat. If someone is red and not nice then they eat the cat. If someone likes the bear then the bear likes the squirrel. If someone needs the squirrel then they are rough. If someone likes the bear and the bear eats the cat then the bear needs the squirrel. If someone eats the cat then the cat likes the bear.
The bear eats the cat.
("bear" "eats" "cat" "+")
The cat is not red.
("cat" "is" "red" "-")
The squirrel is nice.
("squirrel" "is" "nice" "+")
If someone eats the squirrel and they are nice then the squirrel is not blue.
((("someone" "eats" "squirrel" "+") ("someone" "is" "nice" "+")) -> ("squirrel" "is" "blue" "-"))
If someone eats the bear and they are red then they like the cat.
((("someone" "eats" "bear" "+") ("someone" "is" "red" "+")) -> ("someone" "likes" "cat" "+"))
If someone needs the bear then they do not like the cat.
((("someone" "needs" "bear" "+")) -> ("someone" "likes" "cat" "-"))
If someone is red and not nice then they eat the cat.
((("someone" "is" "red" "+") ("someone" "is" "nice" "~")) -> ("someone" "eats" "cat" "+"))
If someone likes the bear then the bear likes the squirrel.
((("someone" "likes" "bear" "+")) -> ("bear" "likes" "squirrel" "+"))
If someone needs the squirrel then they are rough.
((("someone" "needs" "squirrel" "+")) -> ("someone" "is" "rough" "+"))
If someone likes the bear and the bear eats the cat then the bear needs the squirrel.
((("someone" "likes" "bear" "+") ("bear" "eats" "cat" "+")) -> ("bear" "needs" "squirrel" "+"))
If someone eats the cat then the cat likes the bear.
((("someone" "eats" "cat" "+")) -> ("cat" "likes" "bear" "+"))
The bear eats the cat.
True
1
proof
[(triple1)]
("bear" "eats" "cat" "+")
triple1
The cat is red.
False
1
inv-proof
[(triple2)]
("cat" "is" "red" "+")
triple2
The cat likes the bear.
True
2
proof
[(((triple1) -> rule8))]
("cat" "likes" "bear" "+")
((triple1) -> (rule8 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The cat does not like the bear.
False
2
inv-proof
[(((triple1) -> rule8))]
("cat" "likes" "bear" "-")
((triple1) -> (rule8 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear needs the squirrel.
True
4
proof
[(((((triple1) -> rule8) triple1) -> rule7))]
("bear" "needs" "squirrel" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule7 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear does not like the squirrel.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule5))]
("bear" "likes" "squirrel" "-")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear is rough.
True
5
proof
[(((((((triple1) -> rule8) triple1) -> rule7)) -> rule6))]
("bear" "is" "rough" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The cat likes the bear.
("cat" "likes" "bear" "+")
int3
The bear is not rough.
False
5
inv-proof
[(((((((triple1) -> rule8) triple1) -> rule7)) -> rule6))]
("bear" "is" "rough" "-")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The cat likes the bear.
("cat" "likes" "bear" "+")
int3
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "rough" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "rough" "+")
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "cat" "-")
The cat eats the cat.
Unknown
rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "cat" "+")
The cat does not eat the bear.
Unknown
inv-random
[@0: The cat eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bear" "-")
The squirrel needs the bear.
Unknown
random
[@0: The squirrel needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "bear" "+")
The cat does not like the squirrel.
Unknown
inv-random
[@0: The cat likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "squirrel" "-")
The squirrel eats the bear.
Unknown
random
[@0: The squirrel eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "bear" "+")
@0: The bear eats the cat.[(triple1)] The cat is not red.[(triple2)] The squirrel is nice.[(triple3)] @1: The cat likes the bear.[(((triple1) -> rule8))] @2: The bear likes the squirrel.[(((((triple1) -> rule8)) -> rule5))] The bear needs the squirrel.[(((((triple1) -> rule8) triple1) -> rule7))] @3: The bear is rough.[(((((((triple1) -> rule8) triple1) -> rule7)) -> rule6))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The cat is not red.
("cat" "is" "red" "-")
triple2
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple3
The cat likes the bear.
("cat" "likes" "bear" "+")
((triple1) -> (rule8 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule7 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The cat likes the bear.
("cat" "likes" "bear" "+")
int3