The bear likes the cat. The bear needs the rabbit. The bear sees the squirrel. The cat is rough. The cat likes the bear. The cat likes the rabbit. The cat likes the squirrel. The cat sees the bear. The cat sees the squirrel. The rabbit likes the bear. The rabbit needs the bear. The rabbit needs the cat. The rabbit sees the cat. The squirrel is rough. The squirrel needs the bear. The squirrel needs the rabbit. If something is big then it sees the cat. All big things are nice. If something likes the rabbit then it is big. If something is nice then it needs the squirrel. If something needs the bear and it needs the cat then it likes the squirrel. If something is red and it needs the rabbit then the rabbit is rough.
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If something is big then it sees the cat.
((("something" "is" "big" "+")) -> ("something" "sees" "cat" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something likes the rabbit then it is big.
((("something" "likes" "rabbit" "+")) -> ("something" "is" "big" "+"))
If something is nice then it needs the squirrel.
((("something" "is" "nice" "+")) -> ("something" "needs" "squirrel" "+"))
If something needs the bear and it needs the cat then it likes the squirrel.
((("something" "needs" "bear" "+") ("something" "needs" "cat" "+")) -> ("something" "likes" "squirrel" "+"))
If something is red and it needs the rabbit then the rabbit is rough.
((("something" "is" "red" "+") ("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
The squirrel needs the bear.
True
1
proof
[(triple15)]
("squirrel" "needs" "bear" "+")
triple15
The squirrel is not rough.
False
1
inv-proof
[(triple14)]
("squirrel" "is" "rough" "-")
triple14
The cat is big.
True
2
proof
[(((triple6) -> rule3))]
("cat" "is" "big" "+")
((triple6) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The rabbit does not like the squirrel.
False
3
inv-proof
[(((triple11 triple12) -> rule5))]
("rabbit" "likes" "squirrel" "-")
((triple11 triple12) -> (rule5 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The cat is nice.
True
3
proof
[(((((triple6) -> rule3)) -> rule2))]
("cat" "is" "nice" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is not nice.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule2))]
("cat" "is" "nice" "-")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat needs the squirrel.
True
4
proof
[(((((((triple6) -> rule3)) -> rule2)) -> rule4))]
("cat" "needs" "squirrel" "+")
((((((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The cat does not need the squirrel.
False
4
inv-proof
[(((((((triple6) -> rule3)) -> rule2)) -> rule4))]
("cat" "needs" "squirrel" "-")
((((((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The squirrel is not nice.
Unknown
inv-rconc
[@2: The squirrel is nice.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("squirrel" "is" "nice" "-")
The bear sees the cat.
Unknown
rconc
[@2: The bear sees the cat.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("bear" "sees" "cat" "+")
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "big" "-")
The squirrel likes the squirrel.
Unknown
rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "squirrel" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The squirrel likes the bear.
Unknown
random
[@0: The squirrel likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "bear" "+")
The rabbit does not see the bear.
Unknown
inv-random
[@0: The rabbit sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bear" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The bear likes the cat.[(triple1)] The bear needs the rabbit.[(triple2)] The bear sees the squirrel.[(triple3)] The cat is rough.[(triple4)] The cat likes the bear.[(triple5)] The cat likes the rabbit.[(triple6)] The cat likes the squirrel.[(triple7)] The cat sees the bear.[(triple8)] The cat sees the squirrel.[(triple9)] The rabbit likes the bear.[(triple10)] The rabbit needs the bear.[(triple11)] The rabbit needs the cat.[(triple12)] The rabbit sees the cat.[(triple13)] The squirrel is rough.[(triple14)] The squirrel needs the bear.[(triple15)] The squirrel needs the rabbit.[(triple16)] @1: The cat is big.[(((triple6) -> rule3))] The rabbit likes the squirrel.[(((triple11 triple12) -> rule5))] @2: The cat is nice.[(((((triple6) -> rule3)) -> rule2))] The cat sees the cat.[(((((triple6) -> rule3)) -> rule1))] @3: The cat needs the squirrel.[(((((((triple6) -> rule3)) -> rule2)) -> rule4))]
The bear likes the cat.
("bear" "likes" "cat" "+")
triple1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat likes the bear.
("cat" "likes" "bear" "+")
triple5
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple6
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple7
The cat sees the bear.
("cat" "sees" "bear" "+")
triple8
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple9
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple10
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple11
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple12
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple13
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple14
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple15
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple16
The cat is big.
("cat" "is" "big" "+")
((triple6) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
((triple11 triple12) -> (rule5 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
((((((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3