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