The lion eats the rabbit. The lion is young. The rabbit chases the lion. The rabbit chases the tiger. The rabbit eats the tiger. The rabbit is cold. The rabbit is kind. The rabbit likes the lion. The rabbit likes the tiger. The tiger chases the lion. The tiger chases the rabbit. The tiger eats the rabbit. The tiger is not big. The tiger is green. The tiger is not kind. The tiger likes the lion. If someone likes the lion then they chase the rabbit. If the lion does not like the rabbit then the rabbit is big. If someone likes the rabbit then they are kind. If someone chases the lion then they chase the tiger. If someone is green and they eat the tiger then they are young. If someone eats the tiger and the tiger is green then they chase the lion. If someone chases the lion and they are not big then the lion eats the tiger. If someone eats the rabbit and they do not chase the tiger then the tiger is kind.
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is young.
("lion" "is" "young" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is not kind.
("tiger" "is" "kind" "-")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If someone likes the lion then they chase the rabbit.
((("someone" "likes" "lion" "+")) -> ("someone" "chases" "rabbit" "+"))
If the lion does not like the rabbit then the rabbit is big.
((("lion" "likes" "rabbit" "~")) -> ("rabbit" "is" "big" "+"))
If someone likes the rabbit then they are kind.
((("someone" "likes" "rabbit" "+")) -> ("someone" "is" "kind" "+"))
If someone chases the lion then they chase the tiger.
((("someone" "chases" "lion" "+")) -> ("someone" "chases" "tiger" "+"))
If someone is green and they eat the tiger then they are young.
((("someone" "is" "green" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "is" "young" "+"))
If someone eats the tiger and the tiger is green then they chase the lion.
((("someone" "eats" "tiger" "+") ("tiger" "is" "green" "+")) -> ("someone" "chases" "lion" "+"))
If someone chases the lion and they are not big then the lion eats the tiger.
((("someone" "chases" "lion" "+") ("someone" "is" "big" "~")) -> ("lion" "eats" "tiger" "+"))
If someone eats the rabbit and they do not chase the tiger then the tiger is kind.
((("someone" "eats" "rabbit" "+") ("someone" "chases" "tiger" "~")) -> ("tiger" "is" "kind" "+"))
The tiger chases the lion.
True
1
proof
[(triple10)]
("tiger" "chases" "lion" "+")
triple10
The tiger does not chase the lion.
False
1
inv-proof
[(triple10)]
("tiger" "chases" "lion" "-")
triple10
The rabbit chases the rabbit.
True
2
proof
[(((triple8) -> rule1))]
("rabbit" "chases" "rabbit" "+")
((triple8) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The lion does not eat the tiger.
False
3
inv-proof
[(((triple10 triple13) -> rule7))]
("lion" "eats" "tiger" "-")
((triple10 triple13) -> (rule7 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion chases the lion.
True
5
proof
[(((((triple10 triple13) -> rule7) triple14) -> rule6))]
("lion" "chases" "lion" "+")
((((triple10 triple13) -> (rule7 % int2)) triple14) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion does not chase the lion.
False
5
inv-proof
[(((((triple10 triple13) -> rule7) triple14) -> rule6))]
("lion" "chases" "lion" "-")
((((triple10 triple13) -> (rule7 % int2)) triple14) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion chases the tiger.
True
6
proof
[(((((((triple10 triple13) -> rule7) triple14) -> rule6)) -> rule4))]
("lion" "chases" "tiger" "+")
((((((triple10 triple13) -> (rule7 % int3)) triple14) -> (rule6 % int2))) -> (rule4 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3
The lion does not chase the tiger.
False
6
inv-proof
[(((((((triple10 triple13) -> rule7) triple14) -> rule6)) -> rule4))]
("lion" "chases" "tiger" "-")
((((((triple10 triple13) -> (rule7 % int3)) triple14) -> (rule6 % int2))) -> (rule4 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "kind" "-")
The tiger is young.
Unknown
rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "young" "+")
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "young" "-")
The rabbit is big.
Unknown
rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "big" "+")
The rabbit does not eat the lion.
Unknown
inv-random
[@0: The rabbit eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "lion" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
The lion does not like the rabbit.
Unknown
inv-random
[@0: The lion likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "rabbit" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The lion eats the rabbit.[(triple1)] The lion is young.[(triple2)] The rabbit chases the lion.[(triple3 OR ((triple5 triple14) -> rule6))] The rabbit chases the tiger.[(triple4 OR ((triple3) -> rule4) OR ((((triple5 triple14) -> rule6)) -> rule4))] The rabbit eats the tiger.[(triple5)] The rabbit is cold.[(triple6)] The rabbit is kind.[(triple7)] The rabbit likes the lion.[(triple8)] The rabbit likes the tiger.[(triple9)] The tiger chases the lion.[(triple10)] The tiger chases the rabbit.[(triple11 OR ((triple16) -> rule1))] The tiger eats the rabbit.[(triple12)] The tiger is green.[(triple14)] The tiger is not big.[(triple13)] The tiger is not kind.[(triple15)] The tiger likes the lion.[(triple16)] @1: The lion eats the tiger.[(((triple10 triple13) -> rule7))] The rabbit chases the rabbit.[(((triple8) -> rule1))] The tiger chases the tiger.[(((triple10) -> rule4))] @2: The lion chases the lion.[(((((triple10 triple13) -> rule7) triple14) -> rule6))] @3: The lion chases the tiger.[(((((((triple10 triple13) -> rule7) triple14) -> rule6)) -> rule4))]
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple1
The lion is young.
("lion" "is" "young" "+")
triple2
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple3
((triple5 triple14) -> (rule6 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple4
((triple3) -> (rule4 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
((((triple5 triple14) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple5
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple6
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple7
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple8
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple9
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple10
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple11
((triple16) -> (rule1 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple12
The tiger is green.
("tiger" "is" "green" "+")
triple14
The tiger is not big.
("tiger" "is" "big" "-")
triple13
The tiger is not kind.
("tiger" "is" "kind" "-")
triple15
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple16
The lion eats the tiger.
("lion" "eats" "tiger" "+")
((triple10 triple13) -> (rule7 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple8) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple10) -> (rule4 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple10 triple13) -> (rule7 % int2)) triple14) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((((((triple10 triple13) -> (rule7 % int3)) triple14) -> (rule6 % int2))) -> (rule4 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3