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