The mouse sees the squirrel. The mouse visits the squirrel. The squirrel eats the mouse. If someone sees the mouse then the mouse eats the squirrel. If the mouse eats the squirrel then the squirrel sees the mouse. If someone is red and green then they visit the mouse. If someone sees the squirrel and the squirrel visits the mouse then the squirrel is young. If someone is big then they visit the squirrel. If someone sees the mouse and they are not cold then the mouse sees the squirrel. If someone visits the squirrel then they see the mouse. If someone visits the squirrel and the squirrel does not visit the mouse then the squirrel does not eat the mouse.
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
If someone sees the mouse then the mouse eats the squirrel.
((("someone" "sees" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
If the mouse eats the squirrel then the squirrel sees the mouse.
((("mouse" "eats" "squirrel" "+")) -> ("squirrel" "sees" "mouse" "+"))
If someone is red and green then they visit the mouse.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "visits" "mouse" "+"))
If someone sees the squirrel and the squirrel visits the mouse then the squirrel is young.
((("someone" "sees" "squirrel" "+") ("squirrel" "visits" "mouse" "+")) -> ("squirrel" "is" "young" "+"))
If someone is big then they visit the squirrel.
((("someone" "is" "big" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone sees the mouse and they are not cold then the mouse sees the squirrel.
((("someone" "sees" "mouse" "+") ("someone" "is" "cold" "~")) -> ("mouse" "sees" "squirrel" "+"))
If someone visits the squirrel then they see the mouse.
((("someone" "visits" "squirrel" "+")) -> ("someone" "sees" "mouse" "+"))
If someone visits the squirrel and the squirrel does not visit the mouse then the squirrel does not eat the mouse.
((("someone" "visits" "squirrel" "+") ("squirrel" "visits" "mouse" "~")) -> ("squirrel" "eats" "mouse" "-"))
The mouse sees the squirrel.
True
1
proof
[(triple1)]
("mouse" "sees" "squirrel" "+")
triple1
The squirrel does not eat the mouse.
False
1
inv-proof
[(triple3)]
("squirrel" "eats" "mouse" "-")
triple3
The mouse sees the mouse.
True
2
proof
[(((triple2) -> rule7))]
("mouse" "sees" "mouse" "+")
((triple2) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse does not see the mouse.
False
2
inv-proof
[(((triple2) -> rule7))]
("mouse" "sees" "mouse" "-")
((triple2) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse eats the squirrel.
True
3
proof
[(((((triple2) -> rule7)) -> rule1))]
("mouse" "eats" "squirrel" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse does not eat the squirrel.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule1))]
("mouse" "eats" "squirrel" "-")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The squirrel sees the mouse.
True
4
proof
[(((((((triple2) -> rule7)) -> rule1)) -> rule2))]
("squirrel" "sees" "mouse" "+")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The squirrel does not see the mouse.
False
4
inv-proof
[(((((((triple2) -> rule7)) -> rule1)) -> rule2))]
("squirrel" "sees" "mouse" "-")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The squirrel is not young.
Unknown
inv-rconc
[@2: The squirrel is young.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("squirrel" "is" "young" "-")
The squirrel visits the mouse.
Unknown
rconc
[@1: The squirrel visits the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "visits" "mouse" "+")
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The mouse sees the squirrel.[(triple1)] The mouse visits the squirrel.[(triple2)] The squirrel eats the mouse.[(triple3)] @1: The mouse sees the mouse.[(((triple2) -> rule7))] @2: The mouse eats the squirrel.[(((((triple2) -> rule7)) -> rule1))] @3: The squirrel sees the mouse.[(((((((triple2) -> rule7)) -> rule1)) -> rule2))]
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple2) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3