The bear needs the rabbit. The rabbit is big. The rabbit is nice. The rabbit likes the bear. The rabbit likes the squirrel. The rabbit needs the bear. The rabbit visits the squirrel. The squirrel is big. The squirrel is cold. The squirrel is nice. The squirrel is rough. The squirrel likes the rabbit. The squirrel needs the bear. The squirrel needs the rabbit. The squirrel visits the bear. If someone needs the bear then the bear needs the squirrel. If someone needs the squirrel then they like the squirrel. If someone likes the squirrel then they do not visit the rabbit.
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If someone needs the bear then the bear needs the squirrel.
((("someone" "needs" "bear" "+")) -> ("bear" "needs" "squirrel" "+"))
If someone needs the squirrel then they like the squirrel.
((("someone" "needs" "squirrel" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone likes the squirrel then they do not visit the rabbit.
((("someone" "likes" "squirrel" "+")) -> ("someone" "visits" "rabbit" "-"))
The bear needs the rabbit.
True
1
proof
[(triple1)]
("bear" "needs" "rabbit" "+")
triple1
The rabbit does not visit the squirrel.
False
1
inv-proof
[(triple7)]
("rabbit" "visits" "squirrel" "-")
triple7
The bear needs the squirrel.
True
2
proof
[(((triple13) -> rule1) OR ((triple6) -> rule1))]
("bear" "needs" "squirrel" "+")
((triple13) -> (rule1 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
((triple6) -> (rule1 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear does not need the squirrel.
False
2
inv-proof
[(((triple13) -> rule1) OR ((triple6) -> rule1))]
("bear" "needs" "squirrel" "-")
((triple13) -> (rule1 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
((triple6) -> (rule1 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear likes the squirrel.
True
3
proof
[(((((triple13) -> rule1)) -> rule2) OR ((((triple6) -> rule1)) -> rule2))]
("bear" "likes" "squirrel" "+")
((((triple13) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The bear does not like the squirrel.
False
3
inv-proof
[(((((triple13) -> rule1)) -> rule2) OR ((((triple6) -> rule1)) -> rule2))]
("bear" "likes" "squirrel" "-")
((((triple13) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The bear does not visit the rabbit.
True
4
proof
[(((((((triple13) -> rule1)) -> rule2)) -> rule3) OR ((((((triple6) -> rule1)) -> rule2)) -> rule3))]
("bear" "visits" "rabbit" "-")
((((((triple13) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The bear visits the rabbit.
False
4
inv-proof
[(((((((triple13) -> rule1)) -> rule2)) -> rule3) OR ((((((triple6) -> rule1)) -> rule2)) -> rule3))]
("bear" "visits" "rabbit" "+")
((((((triple13) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
The bear does not visit the squirrel.
Unknown
inv-random
[@0: The bear visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The bear likes the rabbit.
Unknown
random
[@0: The bear likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "rabbit" "+")
@0: The bear needs the rabbit.[(triple1)] The rabbit is big.[(triple2)] The rabbit is nice.[(triple3)] The rabbit likes the bear.[(triple4)] The rabbit likes the squirrel.[(triple5)] The rabbit needs the bear.[(triple6)] The rabbit visits the squirrel.[(triple7)] The squirrel is big.[(triple8)] The squirrel is cold.[(triple9)] The squirrel is nice.[(triple10)] The squirrel is rough.[(triple11)] The squirrel likes the rabbit.[(triple12)] The squirrel needs the bear.[(triple13)] The squirrel needs the rabbit.[(triple14)] The squirrel visits the bear.[(triple15)] @1: The bear needs the squirrel.[(((triple13) -> rule1) OR ((triple6) -> rule1))] The rabbit does not visit the rabbit.[(((triple5) -> rule3))] @2: The bear likes the squirrel.[(((((triple13) -> rule1)) -> rule2) OR ((((triple6) -> rule1)) -> rule2))] @3: The bear does not visit the rabbit.[(((((((triple13) -> rule1)) -> rule2)) -> rule3) OR ((((((triple6) -> rule1)) -> rule2)) -> rule3))]
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
triple2
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple3
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple4
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple5
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple6
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple11
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple12
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple13
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple14
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple15
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((triple13) -> (rule1 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
((triple6) -> (rule1 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
((triple5) -> (rule3 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
((((triple13) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
((((((triple13) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3