The mouse likes the squirrel. The squirrel is kind. The tiger is rough. If someone is blue and they see the mouse then they do not like the mouse. If someone is blue and they see the tiger then the tiger does not see the squirrel. Kind people are blue. If someone is nice then they like the squirrel. If someone visits the mouse and the mouse visits the tiger then the mouse does not like the tiger. If the squirrel is blue then the squirrel visits the mouse.
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If someone is blue and they see the mouse then they do not like the mouse.
((("someone" "is" "blue" "+") ("someone" "sees" "mouse" "+")) -> ("someone" "likes" "mouse" "-"))
If someone is blue and they see the tiger then the tiger does not see the squirrel.
((("someone" "is" "blue" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "squirrel" "-"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice then they like the squirrel.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone visits the mouse and the mouse visits the tiger then the mouse does not like the tiger.
((("someone" "visits" "mouse" "+") ("mouse" "visits" "tiger" "+")) -> ("mouse" "likes" "tiger" "-"))
If the squirrel is blue then the squirrel visits the mouse.
((("squirrel" "is" "blue" "+")) -> ("squirrel" "visits" "mouse" "+"))
The squirrel is kind.
True
1
proof
[(triple2)]
("squirrel" "is" "kind" "+")
triple2
The squirrel is not kind.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "kind" "-")
triple2
The squirrel is blue.
True
2
proof
[(((triple2) -> rule3))]
("squirrel" "is" "blue" "+")
((triple2) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is not blue.
False
2
inv-proof
[(((triple2) -> rule3))]
("squirrel" "is" "blue" "-")
((triple2) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the mouse.
True
3
proof
[(((((triple2) -> rule3)) -> rule6))]
("squirrel" "visits" "mouse" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel does not visit the mouse.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6))]
("squirrel" "visits" "mouse" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "blue" "-")
The squirrel likes the squirrel.
Unknown
rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "likes" "squirrel" "+")
The tiger does not like the squirrel.
Unknown
inv-rconc
[@1: The tiger likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "likes" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The mouse does not like the tiger.
Unknown
inv-random
[@0: The mouse likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "tiger" "-")
The tiger sees the mouse.
Unknown
random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "mouse" "+")
@0: The mouse likes the squirrel.[(triple1)] The squirrel is kind.[(triple2)] The tiger is rough.[(triple3)] @1: The squirrel is blue.[(((triple2) -> rule3))] @2: The squirrel visits the mouse.[(((((triple2) -> rule3)) -> rule6))]
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple1
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple2
The tiger is rough.
("tiger" "is" "rough" "+")
triple3
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple2) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2