The cat chases the lion. The cat is big. The cat is blue. The cat is nice. The cat is young. The cat likes the lion. The cat sees the lion. The lion chases the cat. The lion is cold. The lion is nice. The lion does not like the cat. The lion sees the cat. If the lion does not chase the cat then the cat is young. If the lion is not blue then the lion is nice. If something is big then it chases the lion. If the cat is not young then the cat chases the lion. If something chases the lion then the lion sees the cat. If the cat chases the lion and the lion sees the cat then the lion is big.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion does not like the cat.
("lion" "likes" "cat" "-")
The lion sees the cat.
("lion" "sees" "cat" "+")
If the lion does not chase the cat then the cat is young.
((("lion" "chases" "cat" "~")) -> ("cat" "is" "young" "+"))
If the lion is not blue then the lion is nice.
((("lion" "is" "blue" "~")) -> ("lion" "is" "nice" "+"))
If something is big then it chases the lion.
((("something" "is" "big" "+")) -> ("something" "chases" "lion" "+"))
If the cat is not young then the cat chases the lion.
((("cat" "is" "young" "~")) -> ("cat" "chases" "lion" "+"))
If something chases the lion then the lion sees the cat.
((("something" "chases" "lion" "+")) -> ("lion" "sees" "cat" "+"))
If the cat chases the lion and the lion sees the cat then the lion is big.
((("cat" "chases" "lion" "+") ("lion" "sees" "cat" "+")) -> ("lion" "is" "big" "+"))
The lion is cold.
True
1
proof
[(triple9)]
("lion" "is" "cold" "+")
triple9
The cat does not chase the lion.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule3))]
("cat" "chases" "lion" "-")
triple1
((triple2) -> (rule3 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The lion is big.
True
3
proof
[(((triple1 triple12) -> rule6) OR ((triple1 ((triple1) -> rule5)) -> rule6) OR ((((triple2) -> rule3) triple12) -> rule6) OR ((((triple2) -> rule3) ((triple1) -> rule5)) -> rule6) OR ((triple1 ((((triple2) -> rule3)) -> rule5)) -> rule6) OR ((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule6))]
("lion" "is" "big" "+")
((triple1 triple12) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
((((triple2) -> (rule3 % int2)) triple12) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
((((triple2) -> (rule3 % int3)) ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
((triple1 ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
The lion is not big.
False
3
inv-proof
[(((triple1 triple12) -> rule6) OR ((triple1 ((triple1) -> rule5)) -> rule6) OR ((((triple2) -> rule3) triple12) -> rule6) OR ((((triple2) -> rule3) ((triple1) -> rule5)) -> rule6) OR ((triple1 ((((triple2) -> rule3)) -> rule5)) -> rule6) OR ((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule6))]
("lion" "is" "big" "-")
((triple1 triple12) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
((((triple2) -> (rule3 % int2)) triple12) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
((((triple2) -> (rule3 % int3)) ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
((triple1 ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
The lion chases the lion.
True
4
proof
[(((((triple1 triple12) -> rule6)) -> rule3) OR ((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule3) OR ((((((triple2) -> rule3) triple12) -> rule6)) -> rule3) OR ((((((triple2) -> rule3) ((triple1) -> rule5)) -> rule6)) -> rule3) OR ((((triple1 ((((triple2) -> rule3)) -> rule5)) -> rule6)) -> rule3) OR ((((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule6)) -> rule3))]
("lion" "chases" "lion" "+")
((((triple1 triple12) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
((((((triple2) -> (rule3 % int3)) triple12) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
((((((triple2) -> (rule3 % int4)) ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat chases the lion.
("cat" "chases" "lion" "+")
int4
((((triple1 ((((triple2) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat chases the lion.
("cat" "chases" "lion" "+")
int4
((((((triple2) -> (rule3 % int4)) ((((triple2) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat chases the lion.
("cat" "chases" "lion" "+")
int4
The lion does not chase the lion.
False
4
inv-proof
[(((((triple1 triple12) -> rule6)) -> rule3) OR ((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule3) OR ((((((triple2) -> rule3) triple12) -> rule6)) -> rule3) OR ((((((triple2) -> rule3) ((triple1) -> rule5)) -> rule6)) -> rule3) OR ((((triple1 ((((triple2) -> rule3)) -> rule5)) -> rule6)) -> rule3) OR ((((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule6)) -> rule3))]
("lion" "chases" "lion" "-")
((((triple1 triple12) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
((((((triple2) -> (rule3 % int3)) triple12) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
((((((triple2) -> (rule3 % int4)) ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat chases the lion.
("cat" "chases" "lion" "+")
int4
((((triple1 ((((triple2) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat chases the lion.
("cat" "chases" "lion" "+")
int4
((((((triple2) -> (rule3 % int4)) ((((triple2) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat chases the lion.
("cat" "chases" "lion" "+")
int4
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat chases the lion.[(triple1 OR ((triple2) -> rule3))] The cat is big.[(triple2)] The cat is blue.[(triple3)] The cat is nice.[(triple4)] The cat is young.[(triple5)] The cat likes the lion.[(triple6)] The cat sees the lion.[(triple7)] The lion chases the cat.[(triple8)] The lion does not like the cat.[(triple11)] The lion is cold.[(triple9)] The lion is nice.[(triple10)] The lion sees the cat.[(triple12 OR ((triple1) -> rule5) OR ((((triple2) -> rule3)) -> rule5))] @1: The lion is big.[(((triple1 triple12) -> rule6) OR ((triple1 ((triple1) -> rule5)) -> rule6) OR ((((triple2) -> rule3) triple12) -> rule6) OR ((((triple2) -> rule3) ((triple1) -> rule5)) -> rule6) OR ((triple1 ((((triple2) -> rule3)) -> rule5)) -> rule6) OR ((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule6))] @2: The lion chases the lion.[(((((triple1 triple12) -> rule6)) -> rule3) OR ((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule3) OR ((((((triple2) -> rule3) triple12) -> rule6)) -> rule3) OR ((((((triple2) -> rule3) ((triple1) -> rule5)) -> rule6)) -> rule3) OR ((((triple1 ((((triple2) -> rule3)) -> rule5)) -> rule6)) -> rule3) OR ((((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule6)) -> rule3))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
((triple2) -> (rule3 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat likes the lion.
("cat" "likes" "lion" "+")
triple6
The cat sees the lion.
("cat" "sees" "lion" "+")
triple7
The lion chases the cat.
("lion" "chases" "cat" "+")
triple8
The lion does not like the cat.
("lion" "likes" "cat" "-")
triple11
The lion is cold.
("lion" "is" "cold" "+")
triple9
The lion is nice.
("lion" "is" "nice" "+")
triple10
The lion sees the cat.
("lion" "sees" "cat" "+")
triple12
((triple1) -> (rule5 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The lion is big.
("lion" "is" "big" "+")
((triple1 triple12) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
((((triple2) -> (rule3 % int2)) triple12) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
((((triple2) -> (rule3 % int3)) ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
((triple1 ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple1 triple12) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
((((((triple2) -> (rule3 % int3)) triple12) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
((((((triple2) -> (rule3 % int4)) ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat chases the lion.
("cat" "chases" "lion" "+")
int4
((((triple1 ((((triple2) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat chases the lion.
("cat" "chases" "lion" "+")
int4
((((((triple2) -> (rule3 % int4)) ((((triple2) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat chases the lion.
("cat" "chases" "lion" "+")
int4