The bear likes the rabbit. The cat eats the rabbit. The rabbit needs the cat. If the rabbit needs the bear then the rabbit likes the cat. If something likes the rabbit then the rabbit needs the bear.
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If the rabbit needs the bear then the rabbit likes the cat.
((("rabbit" "needs" "bear" "+")) -> ("rabbit" "likes" "cat" "+"))
If something likes the rabbit then the rabbit needs the bear.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "needs" "bear" "+"))
The rabbit needs the cat.
True
1
proof
[(triple3)]
("rabbit" "needs" "cat" "+")
triple3
The cat does not eat the rabbit.
False
1
inv-proof
[(triple2)]
("cat" "eats" "rabbit" "-")
triple2
The rabbit needs the bear.
True
2
proof
[(((triple1) -> rule2))]
("rabbit" "needs" "bear" "+")
((triple1) -> (rule2 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit does not need the bear.
False
2
inv-proof
[(((triple1) -> rule2))]
("rabbit" "needs" "bear" "-")
((triple1) -> (rule2 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit likes the cat.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("rabbit" "likes" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int2
The rabbit does not like the cat.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("rabbit" "likes" "cat" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int2
The bear does not eat the cat.
Unknown
inv-random
[@0: The bear eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cat" "-")
The bear eats the rabbit.
Unknown
random
[@0: The bear eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "rabbit" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The bear needs the cat.
Unknown
random
[@0: The bear needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cat" "+")
The bear does not need the rabbit.
Unknown
inv-random
[@0: The bear needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "rabbit" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The bear likes the rabbit.[(triple1)] The cat eats the rabbit.[(triple2)] The rabbit needs the cat.[(triple3)] @1: The rabbit needs the bear.[(((triple1) -> rule2))] @2: The rabbit likes the cat.[(((((triple1) -> rule2)) -> rule1))]
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple3
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
((triple1) -> (rule2 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int2