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