The cat chases the lion. The cat chases the tiger. The cat is red. The cat is young. The cat likes the lion. The lion does not chase the tiger. The lion is young. The tiger is kind. The tiger likes the lion. The tiger visits the cat. If someone likes the lion then the lion likes the tiger. If the tiger likes the lion and the tiger chases the lion then the lion is not big. If someone likes the tiger then the tiger chases the lion.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
The lion is young.
("lion" "is" "young" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone likes the lion then the lion likes the tiger.
((("someone" "likes" "lion" "+")) -> ("lion" "likes" "tiger" "+"))
If the tiger likes the lion and the tiger chases the lion then the lion is not big.
((("tiger" "likes" "lion" "+") ("tiger" "chases" "lion" "+")) -> ("lion" "is" "big" "-"))
If someone likes the tiger then the tiger chases the lion.
((("someone" "likes" "tiger" "+")) -> ("tiger" "chases" "lion" "+"))
The lion does not chase the tiger.
True
1
proof
[(triple6)]
("lion" "chases" "tiger" "-")
triple6
The lion is not young.
False
1
inv-proof
[(triple7)]
("lion" "is" "young" "-")
triple7
The lion likes the tiger.
True
2
proof
[(((triple5) -> rule1) OR ((triple9) -> rule1))]
("lion" "likes" "tiger" "+")
((triple5) -> (rule1 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
((triple9) -> (rule1 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The lion does not like the tiger.
False
2
inv-proof
[(((triple5) -> rule1) OR ((triple9) -> rule1))]
("lion" "likes" "tiger" "-")
((triple5) -> (rule1 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
((triple9) -> (rule1 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The tiger chases the lion.
True
3
proof
[(((((triple5) -> rule1)) -> rule3) OR ((((triple9) -> rule1)) -> rule3))]
("tiger" "chases" "lion" "+")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
The tiger does not chase the lion.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule3) OR ((((triple9) -> rule1)) -> rule3))]
("tiger" "chases" "lion" "-")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
The lion is not big.
True
5
proof
[(((triple9 ((((triple5) -> rule1)) -> rule3)) -> rule2) OR ((triple9 ((((triple9) -> rule1)) -> rule3)) -> rule2))]
("lion" "is" "big" "-")
((triple9 ((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int3
((triple9 ((((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int3
The lion is big.
False
5
inv-proof
[(((triple9 ((((triple5) -> rule1)) -> rule3)) -> rule2) OR ((triple9 ((((triple9) -> rule1)) -> rule3)) -> rule2))]
("lion" "is" "big" "+")
((triple9 ((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int3
((triple9 ((((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int3
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 lion visits the tiger.
Unknown
random
[@0: The lion visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "tiger" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The lion chases the cat.
Unknown
random
[@0: The lion chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cat" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The lion likes the cat.
Unknown
random
[@0: The lion likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cat" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The cat chases the lion.[(triple1)] The cat chases the tiger.[(triple2)] The cat is red.[(triple3)] The cat is young.[(triple4)] The cat likes the lion.[(triple5)] The lion does not chase the tiger.[(triple6)] The lion is young.[(triple7)] The tiger is kind.[(triple8)] The tiger likes the lion.[(triple9)] The tiger visits the cat.[(triple10)] @1: The lion likes the tiger.[(((triple5) -> rule1) OR ((triple9) -> rule1))] @2: The tiger chases the lion.[(((((triple5) -> rule1)) -> rule3) OR ((((triple9) -> rule1)) -> rule3))] @3: The lion is not big.[(((triple9 ((((triple5) -> rule1)) -> rule3)) -> rule2) OR ((triple9 ((((triple9) -> rule1)) -> rule3)) -> rule2))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
triple4
The cat likes the lion.
("cat" "likes" "lion" "+")
triple5
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
triple6
The lion is young.
("lion" "is" "young" "+")
triple7
The tiger is kind.
("tiger" "is" "kind" "+")
triple8
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple9
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple10
The lion likes the tiger.
("lion" "likes" "tiger" "+")
((triple5) -> (rule1 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
((triple9) -> (rule1 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
The lion is not big.
("lion" "is" "big" "-")
((triple9 ((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int3
((triple9 ((((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int3