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