The mouse is young. The mouse likes the squirrel. The mouse sees the squirrel. The mouse visits the squirrel. The squirrel is kind. The squirrel likes the mouse. The squirrel visits the mouse. If something sees the squirrel and it visits the mouse then the mouse likes the squirrel. If something sees the squirrel then it visits the squirrel. If something likes the mouse then it sees the squirrel. If something likes the squirrel then the squirrel visits the mouse. If something visits the mouse then the mouse visits the squirrel. If the squirrel is cold and the squirrel likes the mouse then the squirrel sees the mouse. If the squirrel sees the mouse then the mouse is big. If something likes the squirrel and the squirrel sees the mouse then it likes the mouse.
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If something sees the squirrel and it visits the mouse then the mouse likes the squirrel.
((("something" "sees" "squirrel" "+") ("something" "visits" "mouse" "+")) -> ("mouse" "likes" "squirrel" "+"))
If something sees the squirrel then it visits the squirrel.
((("something" "sees" "squirrel" "+")) -> ("something" "visits" "squirrel" "+"))
If something likes the mouse then it sees the squirrel.
((("something" "likes" "mouse" "+")) -> ("something" "sees" "squirrel" "+"))
If something likes the squirrel then the squirrel visits the mouse.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "visits" "mouse" "+"))
If something visits the mouse then the mouse visits the squirrel.
((("something" "visits" "mouse" "+")) -> ("mouse" "visits" "squirrel" "+"))
If the squirrel is cold and the squirrel likes the mouse then the squirrel sees the mouse.
((("squirrel" "is" "cold" "+") ("squirrel" "likes" "mouse" "+")) -> ("squirrel" "sees" "mouse" "+"))
If the squirrel sees the mouse then the mouse is big.
((("squirrel" "sees" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If something likes the squirrel and the squirrel sees the mouse then it likes the mouse.
((("something" "likes" "squirrel" "+") ("squirrel" "sees" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
The squirrel visits the mouse.
True
1
proof
[(triple7 OR ((triple2) -> rule4))]
("squirrel" "visits" "mouse" "+")
triple7
((triple2) -> (rule4 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel does not like the mouse.
False
1
inv-proof
[(triple6)]
("squirrel" "likes" "mouse" "-")
triple6
The squirrel sees the squirrel.
True
2
proof
[(((triple6) -> rule3))]
("squirrel" "sees" "squirrel" "+")
((triple6) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not see the squirrel.
False
2
inv-proof
[(((triple6) -> rule3))]
("squirrel" "sees" "squirrel" "-")
((triple6) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel visits the squirrel.
True
3
proof
[(((((triple6) -> rule3)) -> rule2))]
("squirrel" "visits" "squirrel" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel does not visit the squirrel.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule2))]
("squirrel" "visits" "squirrel" "-")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel does not see the mouse.
Unknown
inv-rconc
[@1: The squirrel sees the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "sees" "mouse" "-")
The mouse is big.
Unknown
rconc
[@2: The mouse is big.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("mouse" "is" "big" "+")
The mouse does not like the mouse.
Unknown
inv-rconc
[@2: The mouse likes the mouse.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The mouse is young.[(triple1)] The mouse likes the squirrel.[(triple2 OR ((((triple6) -> rule3) triple7) -> rule1))] The mouse sees the squirrel.[(triple3)] The mouse visits the squirrel.[(triple4 OR ((triple3) -> rule2) OR ((triple7) -> rule5) OR ((((triple2) -> rule4)) -> rule5))] The squirrel is kind.[(triple5)] The squirrel likes the mouse.[(triple6)] The squirrel visits the mouse.[(triple7 OR ((triple2) -> rule4))] @1: The squirrel sees the squirrel.[(((triple6) -> rule3))] @2: The squirrel visits the squirrel.[(((((triple6) -> rule3)) -> rule2))]
The mouse is young.
("mouse" "is" "young" "+")
triple1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple2
((((triple6) -> (rule3 % int2)) triple7) -> (rule1 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple3
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple4
((triple3) -> (rule2 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
((triple7) -> (rule5 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple5
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple6
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple7
((triple2) -> (rule4 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple6) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2