The bear eats the mouse. The bear likes the rabbit. The mouse is blue. The mouse likes the bear. The mouse likes the rabbit. The mouse needs the bear. The rabbit is blue. The rabbit is cold. The rabbit likes the bear. The rabbit likes the mouse. The rabbit needs the bear. The rabbit needs the mouse. If the rabbit likes the bear and the bear likes the rabbit then the bear eats the rabbit.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If the rabbit likes the bear and the bear likes the rabbit then the bear eats the rabbit.
((("rabbit" "likes" "bear" "+") ("bear" "likes" "rabbit" "+")) -> ("bear" "eats" "rabbit" "+"))
The mouse is blue.
True
1
proof
[(triple3)]
("mouse" "is" "blue" "+")
triple3
The rabbit does not need the mouse.
False
1
inv-proof
[(triple12)]
("rabbit" "needs" "mouse" "-")
triple12
The bear eats the rabbit.
True
3
proof
[(((triple9 triple2) -> rule1))]
("bear" "eats" "rabbit" "+")
((triple9 triple2) -> (rule1 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear does not eat the rabbit.
False
3
inv-proof
[(((triple9 triple2) -> rule1))]
("bear" "eats" "rabbit" "-")
((triple9 triple2) -> (rule1 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The mouse needs the rabbit.
Unknown
random
[@0: The mouse needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "rabbit" "+")
@0: The bear eats the mouse.[(triple1)] The bear likes the rabbit.[(triple2)] The mouse is blue.[(triple3)] The mouse likes the bear.[(triple4)] The mouse likes the rabbit.[(triple5)] The mouse needs the bear.[(triple6)] The rabbit is blue.[(triple7)] The rabbit is cold.[(triple8)] The rabbit likes the bear.[(triple9)] The rabbit likes the mouse.[(triple10)] The rabbit needs the bear.[(triple11)] The rabbit needs the mouse.[(triple12)] @1: The bear eats the rabbit.[(((triple9 triple2) -> rule1))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple4
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple5
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple6
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple9
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple10
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple11
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple12
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
((triple9 triple2) -> (rule1 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1