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