The cat chases the mouse. The cat is kind. The cat is nice. The cat is rough. The cat is young. The cat likes the mouse. The cat needs the mouse. The mouse chases the cat. The mouse is kind. The mouse is nice. The mouse is rough. The mouse is round. The mouse is young. The mouse likes the cat. The mouse needs the cat. If someone chases the mouse and the mouse likes the cat then the mouse chases the cat. If someone is rough and they like the mouse then they need the cat. If someone needs the cat then they like the mouse. If someone needs the cat and the cat likes the mouse then the cat is nice. If someone likes the cat and they like the mouse then the cat needs the mouse. If someone is round and they need the cat then the cat needs the mouse.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If someone chases the mouse and the mouse likes the cat then the mouse chases the cat.
((("someone" "chases" "mouse" "+") ("mouse" "likes" "cat" "+")) -> ("mouse" "chases" "cat" "+"))
If someone is rough and they like the mouse then they need the cat.
((("someone" "is" "rough" "+") ("someone" "likes" "mouse" "+")) -> ("someone" "needs" "cat" "+"))
If someone needs the cat then they like the mouse.
((("someone" "needs" "cat" "+")) -> ("someone" "likes" "mouse" "+"))
If someone needs the cat and the cat likes the mouse then the cat is nice.
((("someone" "needs" "cat" "+") ("cat" "likes" "mouse" "+")) -> ("cat" "is" "nice" "+"))
If someone likes the cat and they like the mouse then the cat needs the mouse.
((("someone" "likes" "cat" "+") ("someone" "likes" "mouse" "+")) -> ("cat" "needs" "mouse" "+"))
If someone is round and they need the cat then the cat needs the mouse.
((("someone" "is" "round" "+") ("someone" "needs" "cat" "+")) -> ("cat" "needs" "mouse" "+"))
The mouse is young.
True
1
proof
[(triple13)]
("mouse" "is" "young" "+")
triple13
The mouse does not need the cat.
False
1
inv-proof
[(triple15)]
("mouse" "needs" "cat" "-")
triple15
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 cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat chases the mouse.[(triple1)] The cat is kind.[(triple2)] The cat is nice.[(triple3 OR ((triple15 triple6) -> rule4) OR ((((triple4 triple6) -> rule2) triple6) -> rule4))] The cat is rough.[(triple4)] The cat is young.[(triple5)] The cat likes the mouse.[(triple6)] The cat needs the mouse.[(triple7 OR ((triple12 triple15) -> rule6) OR ((triple14 ((triple15) -> rule3)) -> rule5))] The mouse chases the cat.[(triple8 OR ((triple1 triple14) -> rule1))] The mouse is kind.[(triple9)] The mouse is nice.[(triple10)] The mouse is rough.[(triple11)] The mouse is round.[(triple12)] The mouse is young.[(triple13)] The mouse likes the cat.[(triple14)] The mouse needs the cat.[(triple15)] @1: The cat needs the cat.[(((triple4 triple6) -> rule2))] The mouse likes the mouse.[(((triple15) -> rule3))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
((triple15 triple6) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((((triple4 triple6) -> (rule2 % int2)) triple6) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple6
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple7
((triple12 triple15) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
((triple14 ((triple15) -> (rule3 % int2))) -> (rule5 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple8
((triple1 triple14) -> (rule1 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
triple9
The mouse is nice.
("mouse" "is" "nice" "+")
triple10
The mouse is rough.
("mouse" "is" "rough" "+")
triple11
The mouse is round.
("mouse" "is" "round" "+")
triple12
The mouse is young.
("mouse" "is" "young" "+")
triple13
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple14
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple15
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple4 triple6) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple15) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1