The cat does not chase the mouse. The cat eats the mouse. The cat is big. The cat is kind. The cat sees the mouse. The mouse chases the cat. The mouse is young. If someone eats the mouse then they do not see the cat. If the mouse is young then the mouse is big. If the cat eats the mouse and the cat chases the mouse then the mouse does not see the cat.
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is young.
("mouse" "is" "young" "+")
If someone eats the mouse then they do not see the cat.
((("someone" "eats" "mouse" "+")) -> ("someone" "sees" "cat" "-"))
If the mouse is young then the mouse is big.
((("mouse" "is" "young" "+")) -> ("mouse" "is" "big" "+"))
If the cat eats the mouse and the cat chases the mouse then the mouse does not see the cat.
((("cat" "eats" "mouse" "+") ("cat" "chases" "mouse" "+")) -> ("mouse" "sees" "cat" "-"))
The cat does not chase the mouse.
True
1
proof
[(triple1)]
("cat" "chases" "mouse" "-")
triple1
The cat chases the mouse.
False
1
inv-proof
[(triple1)]
("cat" "chases" "mouse" "+")
triple1
The mouse is big.
True
2
proof
[(((triple7) -> rule2))]
("mouse" "is" "big" "+")
((triple7) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is not big.
False
2
inv-proof
[(((triple7) -> rule2))]
("mouse" "is" "big" "-")
((triple7) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The mouse eats the cat.
Unknown
random
[@0: The mouse eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cat" "+")
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" "+")
@0: The cat does not chase the mouse.[(triple1)] The cat eats the mouse.[(triple2)] The cat is big.[(triple3)] The cat is kind.[(triple4)] The cat sees the mouse.[(triple5)] The mouse chases the cat.[(triple6)] The mouse is young.[(triple7)] @1: The cat does not see the cat.[(((triple2) -> rule1))] The mouse is big.[(((triple7) -> rule2))]
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple6
The mouse is young.
("mouse" "is" "young" "+")
triple7
The cat does not see the cat.
("cat" "sees" "cat" "-")
((triple2) -> (rule1 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1
The mouse is big.
("mouse" "is" "big" "+")
((triple7) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1