The lion chases the rabbit. The lion eats the rabbit. The lion is big. The lion is blue. The lion is green. The lion is rough. The lion is round. The lion sees the rabbit. The rabbit chases the lion. The rabbit eats the lion. The rabbit is big. The rabbit is blue. The rabbit is green. The rabbit is round. The rabbit sees the lion. If the rabbit is big and the rabbit eats the lion then the lion sees the rabbit. If someone eats the lion and they eat the rabbit then the rabbit sees the lion. If someone is round and rough then they eat the rabbit.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If the rabbit is big and the rabbit eats the lion then the lion sees the rabbit.
((("rabbit" "is" "big" "+") ("rabbit" "eats" "lion" "+")) -> ("lion" "sees" "rabbit" "+"))
If someone eats the lion and they eat the rabbit then the rabbit sees the lion.
((("someone" "eats" "lion" "+") ("someone" "eats" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
If someone is round and rough then they eat the rabbit.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "eats" "rabbit" "+"))
The rabbit chases the lion.
True
1
proof
[(triple9)]
("rabbit" "chases" "lion" "+")
triple9
The rabbit is not round.
False
1
inv-proof
[(triple14)]
("rabbit" "is" "round" "-")
triple14
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The lion chases the rabbit.[(triple1)] The lion eats the rabbit.[(triple2 OR ((triple7 triple6) -> rule3))] The lion is big.[(triple3)] The lion is blue.[(triple4)] The lion is green.[(triple5)] The lion is rough.[(triple6)] The lion is round.[(triple7)] The lion sees the rabbit.[(triple8 OR ((triple11 triple10) -> rule1))] The rabbit chases the lion.[(triple9)] The rabbit eats the lion.[(triple10)] The rabbit is big.[(triple11)] The rabbit is blue.[(triple12)] The rabbit is green.[(triple13)] The rabbit is round.[(triple14)] The rabbit sees the lion.[(triple15)]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple2
((triple7 triple6) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion is big.
("lion" "is" "big" "+")
triple3
The lion is blue.
("lion" "is" "blue" "+")
triple4
The lion is green.
("lion" "is" "green" "+")
triple5
The lion is rough.
("lion" "is" "rough" "+")
triple6
The lion is round.
("lion" "is" "round" "+")
triple7
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple8
((triple11 triple10) -> (rule1 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple9
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple10
The rabbit is big.
("rabbit" "is" "big" "+")
triple11
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple12
The rabbit is green.
("rabbit" "is" "green" "+")
triple13
The rabbit is round.
("rabbit" "is" "round" "+")
triple14
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple15