The bear chases the rabbit. The bear is blue. The bear is round. The bear is young. The bear needs the mouse. The bear does not need the rabbit. The bear sees the mouse. The mouse is not big. The mouse is round. The mouse needs the bear. The mouse sees the rabbit. The rabbit is big. The rabbit is blue. The rabbit is red. The rabbit needs the bear. The rabbit sees the mouse. If the rabbit needs the bear then the bear sees the rabbit.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is round.
("bear" "is" "round" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If the rabbit needs the bear then the bear sees the rabbit.
((("rabbit" "needs" "bear" "+")) -> ("bear" "sees" "rabbit" "+"))
The rabbit is big.
True
1
proof
[(triple12)]
("rabbit" "is" "big" "+")
triple12
The rabbit is not red.
False
1
inv-proof
[(triple14)]
("rabbit" "is" "red" "-")
triple14
The bear sees the rabbit.
True
2
proof
[(((triple15) -> rule1))]
("bear" "sees" "rabbit" "+")
((triple15) -> (rule1 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The bear does not see the rabbit.
False
2
inv-proof
[(((triple15) -> rule1))]
("bear" "sees" "rabbit" "-")
((triple15) -> (rule1 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
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 mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The rabbit does not chase the mouse.
Unknown
inv-random
[@0: The rabbit chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "mouse" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
@0: The bear chases the rabbit.[(triple1)] The bear does not need the rabbit.[(triple6)] The bear is blue.[(triple2)] The bear is round.[(triple3)] The bear is young.[(triple4)] The bear needs the mouse.[(triple5)] The bear sees the mouse.[(triple7)] The mouse is not big.[(triple8)] The mouse is round.[(triple9)] The mouse needs the bear.[(triple10)] The mouse sees the rabbit.[(triple11)] The rabbit is big.[(triple12)] The rabbit is blue.[(triple13)] The rabbit is red.[(triple14)] The rabbit needs the bear.[(triple15)] The rabbit sees the mouse.[(triple16)] @1: The bear sees the rabbit.[(((triple15) -> rule1))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
triple6
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear is young.
("bear" "is" "young" "+")
triple4
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple5
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple7
The mouse is not big.
("mouse" "is" "big" "-")
triple8
The mouse is round.
("mouse" "is" "round" "+")
triple9
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple10
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple11
The rabbit is big.
("rabbit" "is" "big" "+")
triple12
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple13
The rabbit is red.
("rabbit" "is" "red" "+")
triple14
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple15
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple16
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
((triple15) -> (rule1 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1