The bear visits the mouse. The mouse visits the bear. If someone likes the bear then they do not visit the bear. If someone likes the mouse then the mouse does not see the bear. If the mouse is blue and the mouse visits the bear then the bear likes the mouse. If someone visits the bear then they are blue. If someone is cold and they do not visit the bear then they visit the mouse. If someone is round then they do not visit the mouse. If someone visits the mouse and the mouse is nice then they do not see the bear. If someone likes the mouse and the mouse is not nice then they see the bear.
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If someone likes the bear then they do not visit the bear.
((("someone" "likes" "bear" "+")) -> ("someone" "visits" "bear" "-"))
If someone likes the mouse then the mouse does not see the bear.
((("someone" "likes" "mouse" "+")) -> ("mouse" "sees" "bear" "-"))
If the mouse is blue and the mouse visits the bear then the bear likes the mouse.
((("mouse" "is" "blue" "+") ("mouse" "visits" "bear" "+")) -> ("bear" "likes" "mouse" "+"))
If someone visits the bear then they are blue.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold and they do not visit the bear then they visit the mouse.
((("someone" "is" "cold" "+") ("someone" "visits" "bear" "~")) -> ("someone" "visits" "mouse" "+"))
If someone is round then they do not visit the mouse.
((("someone" "is" "round" "+")) -> ("someone" "visits" "mouse" "-"))
If someone visits the mouse and the mouse is nice then they do not see the bear.
((("someone" "visits" "mouse" "+") ("mouse" "is" "nice" "+")) -> ("someone" "sees" "bear" "-"))
If someone likes the mouse and the mouse is not nice then they see the bear.
((("someone" "likes" "mouse" "+") ("mouse" "is" "nice" "~")) -> ("someone" "sees" "bear" "+"))
The mouse visits the bear.
True
1
proof
[(triple2)]
("mouse" "visits" "bear" "+")
triple2
The bear does not visit the mouse.
False
1
inv-proof
[(triple1)]
("bear" "visits" "mouse" "-")
triple1
The mouse is blue.
True
2
proof
[(((triple2) -> rule4))]
("mouse" "is" "blue" "+")
((triple2) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is not blue.
False
2
inv-proof
[(((triple2) -> rule4))]
("mouse" "is" "blue" "-")
((triple2) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The bear likes the mouse.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule3))]
("bear" "likes" "mouse" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The bear does not like the mouse.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule3))]
("bear" "likes" "mouse" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse does not see the bear.
True
5
proof
[(((((((triple2) -> rule4) triple2) -> rule3)) -> rule2))]
("mouse" "sees" "bear" "-")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse sees the bear.
False
5
inv-proof
[(((((((triple2) -> rule4) triple2) -> rule3)) -> rule2))]
("mouse" "sees" "bear" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "sees" "bear" "+")
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "blue" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The bear does not see the mouse.
Unknown
inv-random
[@0: The bear sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "mouse" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
@0: The bear visits the mouse.[(triple1)] The mouse visits the bear.[(triple2)] @1: The mouse is blue.[(((triple2) -> rule4))] @2: The bear likes the mouse.[(((((triple2) -> rule4) triple2) -> rule3))] @3: The mouse does not see the bear.[(((((((triple2) -> rule4) triple2) -> rule3)) -> rule2))]
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
((triple2) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3