The mouse chases the squirrel. The mouse eats the squirrel. The mouse is not big. The mouse is cold. The mouse is green. The mouse is nice. The mouse does not see the squirrel. The squirrel chases the mouse. The squirrel does not eat the mouse. The squirrel is big. The squirrel is cold. The squirrel is green. The squirrel is nice. The squirrel is rough. The squirrel sees the mouse. If something is nice then it is rough. If something eats the squirrel then it is rough. If the mouse eats the squirrel then the squirrel is green. If the mouse is not nice then the mouse chases the squirrel. If something eats the mouse and it sees the squirrel then the mouse chases the squirrel. If something sees the squirrel then the squirrel does not eat the mouse. If something is nice then it chases the squirrel. If something is rough then it sees the mouse.
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel does not eat the mouse.
("squirrel" "eats" "mouse" "-")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something eats the squirrel then it is rough.
((("something" "eats" "squirrel" "+")) -> ("something" "is" "rough" "+"))
If the mouse eats the squirrel then the squirrel is green.
((("mouse" "eats" "squirrel" "+")) -> ("squirrel" "is" "green" "+"))
If the mouse is not nice then the mouse chases the squirrel.
((("mouse" "is" "nice" "~")) -> ("mouse" "chases" "squirrel" "+"))
If something eats the mouse and it sees the squirrel then the mouse chases the squirrel.
((("something" "eats" "mouse" "+") ("something" "sees" "squirrel" "+")) -> ("mouse" "chases" "squirrel" "+"))
If something sees the squirrel then the squirrel does not eat the mouse.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "eats" "mouse" "-"))
If something is nice then it chases the squirrel.
((("something" "is" "nice" "+")) -> ("something" "chases" "squirrel" "+"))
If something is rough then it sees the mouse.
((("something" "is" "rough" "+")) -> ("something" "sees" "mouse" "+"))
The mouse is green.
True
1
proof
[(triple5)]
("mouse" "is" "green" "+")
triple5
The squirrel is not green.
False
1
inv-proof
[(triple12 OR ((triple2) -> rule3))]
("squirrel" "is" "green" "-")
triple12
((triple2) -> (rule3 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The mouse is rough.
True
2
proof
[(((triple2) -> rule2) OR ((triple6) -> rule1))]
("mouse" "is" "rough" "+")
((triple2) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((triple6) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The squirrel does not chase the squirrel.
False
2
inv-proof
[(((triple13) -> rule7))]
("squirrel" "chases" "squirrel" "-")
((triple13) -> (rule7 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The mouse sees the mouse.
True
3
proof
[(((((triple2) -> rule2)) -> rule8) OR ((((triple6) -> rule1)) -> rule8))]
("mouse" "sees" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not see the mouse.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule8) OR ((((triple6) -> rule1)) -> rule8))]
("mouse" "sees" "mouse" "-")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
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 mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The mouse chases the squirrel.[(triple1 OR ((triple6) -> rule7))] The mouse does not see the squirrel.[(triple7)] The mouse eats the squirrel.[(triple2)] The mouse is cold.[(triple4)] The mouse is green.[(triple5)] The mouse is nice.[(triple6)] The mouse is not big.[(triple3)] The squirrel chases the mouse.[(triple8)] The squirrel does not eat the mouse.[(triple9)] The squirrel is big.[(triple10)] The squirrel is cold.[(triple11)] The squirrel is green.[(triple12 OR ((triple2) -> rule3))] The squirrel is nice.[(triple13)] The squirrel is rough.[(triple14 OR ((triple13) -> rule1))] The squirrel sees the mouse.[(triple15 OR ((triple14) -> rule8) OR ((((triple13) -> rule1)) -> rule8))] @1: The mouse is rough.[(((triple2) -> rule2) OR ((triple6) -> rule1))] The squirrel chases the squirrel.[(((triple13) -> rule7))] @2: The mouse sees the mouse.[(((((triple2) -> rule2)) -> rule8) OR ((((triple6) -> rule1)) -> rule8))]
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple1
((triple6) -> (rule7 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
triple7
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
The mouse is green.
("mouse" "is" "green" "+")
triple5
The mouse is nice.
("mouse" "is" "nice" "+")
triple6
The mouse is not big.
("mouse" "is" "big" "-")
triple3
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple8
The squirrel does not eat the mouse.
("squirrel" "eats" "mouse" "-")
triple9
The squirrel is big.
("squirrel" "is" "big" "+")
triple10
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple11
The squirrel is green.
("squirrel" "is" "green" "+")
triple12
((triple2) -> (rule3 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple13
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple14
((triple13) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple15
((triple14) -> (rule8 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
((((triple13) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
((triple2) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((triple6) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple13) -> (rule7 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2