The bear is blue. The bear is not green. The bear likes the mouse. The mouse is blue. The mouse is green. The mouse is nice. The mouse is round. The mouse likes the bear. The mouse needs the bear. The mouse sees the bear. If the mouse is round and the mouse sees the bear then the bear sees the mouse. If someone likes the bear then they need the bear. If someone sees the mouse then they do not see the bear. If someone is blue and they do not see the bear then the bear needs the mouse. If someone likes the bear and they need the bear then the bear likes the mouse. If the bear does not see the mouse then the bear likes the mouse.
The bear is blue.
("bear" "is" "blue" "+")
The bear is not green.
("bear" "is" "green" "-")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
If the mouse is round and the mouse sees the bear then the bear sees the mouse.
((("mouse" "is" "round" "+") ("mouse" "sees" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
If someone likes the bear then they need the bear.
((("someone" "likes" "bear" "+")) -> ("someone" "needs" "bear" "+"))
If someone sees the mouse then they do not see the bear.
((("someone" "sees" "mouse" "+")) -> ("someone" "sees" "bear" "-"))
If someone is blue and they do not see the bear then the bear needs the mouse.
((("someone" "is" "blue" "+") ("someone" "sees" "bear" "~")) -> ("bear" "needs" "mouse" "+"))
If someone likes the bear and they need the bear then the bear likes the mouse.
((("someone" "likes" "bear" "+") ("someone" "needs" "bear" "+")) -> ("bear" "likes" "mouse" "+"))
If the bear does not see the mouse then the bear likes the mouse.
((("bear" "sees" "mouse" "~")) -> ("bear" "likes" "mouse" "+"))
The bear is not green.
True
1
proof
[(triple2)]
("bear" "is" "green" "-")
triple2
The mouse is not round.
False
1
inv-proof
[(triple7)]
("mouse" "is" "round" "-")
triple7
The bear sees the mouse.
True
3
proof
[(((triple7 triple10) -> rule1))]
("bear" "sees" "mouse" "+")
((triple7 triple10) -> (rule1 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear does not see the mouse.
False
3
inv-proof
[(((triple7 triple10) -> rule1))]
("bear" "sees" "mouse" "-")
((triple7 triple10) -> (rule1 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear does not see the bear.
True
4
proof
[(((((triple7 triple10) -> rule1)) -> rule3))]
("bear" "sees" "bear" "-")
((((triple7 triple10) -> (rule1 % int2))) -> (rule3 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear sees the bear.
False
4
inv-proof
[(((((triple7 triple10) -> rule1)) -> rule3))]
("bear" "sees" "bear" "+")
((((triple7 triple10) -> (rule1 % int2))) -> (rule3 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear needs the mouse.
True
6
proof
[(((triple1 ((((triple7 triple10) -> rule1)) -> rule3)) -> rule4))]
("bear" "needs" "mouse" "+")
((triple1 ((((triple7 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3
The bear does not need the mouse.
False
6
inv-proof
[(((triple1 ((((triple7 triple10) -> rule1)) -> rule3)) -> rule4))]
("bear" "needs" "mouse" "-")
((triple1 ((((triple7 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "needs" "bear" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
@0: The bear is blue.[(triple1)] The bear is not green.[(triple2)] The bear likes the mouse.[(triple3 OR ((triple8 triple9) -> rule5) OR ((triple8 ((triple8) -> rule2)) -> rule5))] The mouse is blue.[(triple4)] The mouse is green.[(triple5)] The mouse is nice.[(triple6)] The mouse is round.[(triple7)] The mouse likes the bear.[(triple8)] The mouse needs the bear.[(triple9 OR ((triple8) -> rule2))] The mouse sees the bear.[(triple10)] @1: The bear sees the mouse.[(((triple7 triple10) -> rule1))] @2: The bear does not see the bear.[(((((triple7 triple10) -> rule1)) -> rule3))] @3: The bear needs the mouse.[(((triple1 ((((triple7 triple10) -> rule1)) -> rule3)) -> rule4))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is not green.
("bear" "is" "green" "-")
triple2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple3
((triple8 triple9) -> (rule5 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
((triple8 ((triple8) -> (rule2 % int2))) -> (rule5 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
triple4
The mouse is green.
("mouse" "is" "green" "+")
triple5
The mouse is nice.
("mouse" "is" "nice" "+")
triple6
The mouse is round.
("mouse" "is" "round" "+")
triple7
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple8
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple9
((triple8) -> (rule2 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple10
The bear sees the mouse.
("bear" "sees" "mouse" "+")
((triple7 triple10) -> (rule1 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
((((triple7 triple10) -> (rule1 % int2))) -> (rule3 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((triple1 ((((triple7 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3