The cat does not chase the mouse. The cat is blue. The cat is kind. The cat is nice. The cat is red. The cat is rough. The cat needs the mouse. The cat does not see the mouse. The mouse chases the cat. The mouse is blue. The mouse is kind. The mouse is nice. The mouse is red. The mouse is not rough. The mouse needs the cat. The mouse sees the cat. If someone is red and they do not need the mouse then the mouse chases the cat. If someone is red then they see the cat.
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
The cat is blue.
("cat" "is" "blue" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone is red and they do not need the mouse then the mouse chases the cat.
((("someone" "is" "red" "+") ("someone" "needs" "mouse" "~")) -> ("mouse" "chases" "cat" "+"))
If someone is red then they see the cat.
((("someone" "is" "red" "+")) -> ("someone" "sees" "cat" "+"))
The cat is blue.
True
1
proof
[(triple2)]
("cat" "is" "blue" "+")
triple2
The cat does not need the mouse.
False
1
inv-proof
[(triple7)]
("cat" "needs" "mouse" "-")
triple7
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 cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat does not chase the mouse.[(triple1)] The cat does not see the mouse.[(triple8)] The cat is blue.[(triple2)] The cat is kind.[(triple3)] The cat is nice.[(triple4)] The cat is red.[(triple5)] The cat is rough.[(triple6)] The cat needs the mouse.[(triple7)] The mouse chases the cat.[(triple9)] The mouse is blue.[(triple10)] The mouse is kind.[(triple11)] The mouse is nice.[(triple12)] The mouse is not rough.[(triple14)] The mouse is red.[(triple13)] The mouse needs the cat.[(triple15)] The mouse sees the cat.[(triple16 OR ((triple13) -> rule2))] @1: The cat sees the cat.[(((triple5) -> rule2))]
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
triple1
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
triple8
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple7
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple11
The mouse is nice.
("mouse" "is" "nice" "+")
triple12
The mouse is not rough.
("mouse" "is" "rough" "-")
triple14
The mouse is red.
("mouse" "is" "red" "+")
triple13
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple15
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple16
((triple13) -> (rule2 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple5) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1