The bald eagle needs the bear. The bear is cold. The mouse is round. The rabbit sees the mouse. If someone sees the rabbit then they like the rabbit. If someone likes the rabbit then the rabbit needs the mouse. If someone is kind and they see the bear then the bear needs the rabbit. If someone sees the bald eagle then they are young. If someone is cold then they like the mouse. If someone likes the mouse then they like the rabbit. If someone is young then they see the mouse. If someone likes the rabbit and the rabbit likes the bear then they like the bear.
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
The bear is cold.
("bear" "is" "cold" "+")
The mouse is round.
("mouse" "is" "round" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If someone sees the rabbit then they like the rabbit.
((("someone" "sees" "rabbit" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone likes the rabbit then the rabbit needs the mouse.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If someone is kind and they see the bear then the bear needs the rabbit.
((("someone" "is" "kind" "+") ("someone" "sees" "bear" "+")) -> ("bear" "needs" "rabbit" "+"))
If someone sees the bald eagle then they are young.
((("someone" "sees" "bald eagle" "+")) -> ("someone" "is" "young" "+"))
If someone is cold then they like the mouse.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "mouse" "+"))
If someone likes the mouse then they like the rabbit.
((("someone" "likes" "mouse" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone is young then they see the mouse.
((("someone" "is" "young" "+")) -> ("someone" "sees" "mouse" "+"))
If someone likes the rabbit and the rabbit likes the bear then they like the bear.
((("someone" "likes" "rabbit" "+") ("rabbit" "likes" "bear" "+")) -> ("someone" "likes" "bear" "+"))
The rabbit sees the mouse.
True
1
proof
[(triple4)]
("rabbit" "sees" "mouse" "+")
triple4
The rabbit does not see the mouse.
False
1
inv-proof
[(triple4)]
("rabbit" "sees" "mouse" "-")
triple4
The bear likes the mouse.
True
2
proof
[(((triple2) -> rule5))]
("bear" "likes" "mouse" "+")
((triple2) -> (rule5 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The bear does not like the mouse.
False
2
inv-proof
[(((triple2) -> rule5))]
("bear" "likes" "mouse" "-")
((triple2) -> (rule5 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The bear likes the rabbit.
True
3
proof
[(((((triple2) -> rule5)) -> rule6))]
("bear" "likes" "rabbit" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The bear does not like the rabbit.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6))]
("bear" "likes" "rabbit" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The rabbit needs the mouse.
True
4
proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule2))]
("rabbit" "needs" "mouse" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The rabbit does not need the mouse.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule2))]
("rabbit" "needs" "mouse" "-")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The bald eagle does not like the rabbit.
Unknown
inv-rconc
[@2: The bald eagle likes the rabbit.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("bald eagle" "likes" "rabbit" "-")
The rabbit is young.
Unknown
rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "young" "+")
The bald eagle does not like the bear.
Unknown
inv-rconc
[@1: The bald eagle likes the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bald eagle" "likes" "bear" "-")
The rabbit likes the mouse.
Unknown
rconc
[@1: The rabbit likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "likes" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The bear needs the mouse.
Unknown
random
[@0: The bear needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "mouse" "+")
The bear does not see the bald eagle.
Unknown
inv-random
[@0: The bear sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bald eagle" "-")
The mouse needs the bear.
Unknown
random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "+")
@0: The bald eagle needs the bear.[(triple1)] The bear is cold.[(triple2)] The mouse is round.[(triple3)] The rabbit sees the mouse.[(triple4)] @1: The bear likes the mouse.[(((triple2) -> rule5))] @2: The bear likes the rabbit.[(((((triple2) -> rule5)) -> rule6))] @3: The rabbit needs the mouse.[(((((((triple2) -> rule5)) -> rule6)) -> rule2))]
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The mouse is round.
("mouse" "is" "round" "+")
triple3
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple4
The bear likes the mouse.
("bear" "likes" "mouse" "+")
((triple2) -> (rule5 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3