The mouse eats the squirrel. The squirrel sees the mouse. If the squirrel likes the mouse then the mouse sees the squirrel. If something likes the squirrel and the squirrel sees the mouse then the squirrel likes the mouse. If something eats the squirrel and it is kind then the squirrel sees the mouse. If something sees the mouse then the mouse likes the squirrel. If something eats the squirrel then it is blue. If something likes the squirrel and the squirrel is nice then the squirrel likes the mouse.
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If the squirrel likes the mouse then the mouse sees the squirrel.
((("squirrel" "likes" "mouse" "+")) -> ("mouse" "sees" "squirrel" "+"))
If something likes the squirrel and the squirrel sees the mouse then the squirrel likes the mouse.
((("something" "likes" "squirrel" "+") ("squirrel" "sees" "mouse" "+")) -> ("squirrel" "likes" "mouse" "+"))
If something eats the squirrel and it is kind then the squirrel sees the mouse.
((("something" "eats" "squirrel" "+") ("something" "is" "kind" "+")) -> ("squirrel" "sees" "mouse" "+"))
If something sees the mouse then the mouse likes the squirrel.
((("something" "sees" "mouse" "+")) -> ("mouse" "likes" "squirrel" "+"))
If something eats the squirrel then it is blue.
((("something" "eats" "squirrel" "+")) -> ("something" "is" "blue" "+"))
If something likes the squirrel and the squirrel is nice then the squirrel likes the mouse.
((("something" "likes" "squirrel" "+") ("squirrel" "is" "nice" "+")) -> ("squirrel" "likes" "mouse" "+"))
The squirrel sees the mouse.
True
1
proof
[(triple2)]
("squirrel" "sees" "mouse" "+")
triple2
The squirrel does not see the mouse.
False
1
inv-proof
[(triple2)]
("squirrel" "sees" "mouse" "-")
triple2
The mouse likes the squirrel.
True
2
proof
[(((triple2) -> rule4))]
("mouse" "likes" "squirrel" "+")
((triple2) -> (rule4 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse is not blue.
False
2
inv-proof
[(((triple1) -> rule5))]
("mouse" "is" "blue" "-")
((triple1) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The squirrel likes the mouse.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule2))]
("squirrel" "likes" "mouse" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule2 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The squirrel does not like the mouse.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule2))]
("squirrel" "likes" "mouse" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule2 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse sees the squirrel.
True
5
proof
[(((((((triple2) -> rule4) triple2) -> rule2)) -> rule1))]
("mouse" "sees" "squirrel" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3
The mouse does not see the squirrel.
False
5
inv-proof
[(((((((triple2) -> rule4) triple2) -> rule2)) -> rule1))]
("mouse" "sees" "squirrel" "-")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3
The squirrel is not blue.
Unknown
inv-rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "blue" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
@0: The mouse eats the squirrel.[(triple1)] The squirrel sees the mouse.[(triple2)] @1: The mouse is blue.[(((triple1) -> rule5))] The mouse likes the squirrel.[(((triple2) -> rule4))] @2: The squirrel likes the mouse.[(((((triple2) -> rule4) triple2) -> rule2))] @3: The mouse sees the squirrel.[(((((((triple2) -> rule4) triple2) -> rule2)) -> rule1))]
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
((triple1) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
((triple2) -> (rule4 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule2 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3