The lion chases the rabbit. The lion eats the rabbit. The lion is big. The lion is green. The lion is rough. The lion is not round. The lion likes the rabbit. The rabbit chases the lion. The rabbit does not eat the lion. The rabbit is big. The rabbit is green. The rabbit is not nice. The rabbit is rough. The rabbit is round. The rabbit likes the lion. All round things are green. If the rabbit is not big and the rabbit is not rough then the rabbit eats the lion. If something is round then it chases the rabbit. If something chases the rabbit and it chases the lion then it eats the rabbit. If something likes the lion then it chases the lion. If something eats the lion and it is not green then the lion is nice. If something eats the lion then the lion likes the rabbit. If something is nice then it does not eat the lion.
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 green.
("lion" "is" "green" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is not round.
("lion" "is" "round" "-")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit does not eat the lion.
("rabbit" "eats" "lion" "-")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If the rabbit is not big and the rabbit is not rough then the rabbit eats the lion.
((("rabbit" "is" "big" "~") ("rabbit" "is" "rough" "~")) -> ("rabbit" "eats" "lion" "+"))
If something is round then it chases the rabbit.
((("something" "is" "round" "+")) -> ("something" "chases" "rabbit" "+"))
If something chases the rabbit and it chases the lion then it eats the rabbit.
((("something" "chases" "rabbit" "+") ("something" "chases" "lion" "+")) -> ("something" "eats" "rabbit" "+"))
If something likes the lion then it chases the lion.
((("something" "likes" "lion" "+")) -> ("something" "chases" "lion" "+"))
If something eats the lion and it is not green then the lion is nice.
((("something" "eats" "lion" "+") ("something" "is" "green" "~")) -> ("lion" "is" "nice" "+"))
If something eats the lion then the lion likes the rabbit.
((("something" "eats" "lion" "+")) -> ("lion" "likes" "rabbit" "+"))
If something is nice then it does not eat the lion.
((("something" "is" "nice" "+")) -> ("something" "eats" "lion" "-"))
The lion is not round.
True
1
proof
[(triple6)]
("lion" "is" "round" "-")
triple6
The rabbit is not green.
False
1
inv-proof
[(triple11 OR ((triple14) -> rule1))]
("rabbit" "is" "green" "-")
triple11
((triple14) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the rabbit.
True
2
proof
[(((triple14) -> rule3))]
("rabbit" "chases" "rabbit" "+")
((triple14) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit does not chase the rabbit.
False
2
inv-proof
[(((triple14) -> rule3))]
("rabbit" "chases" "rabbit" "-")
((triple14) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit eats the rabbit.
True
4
proof
[(((((triple14) -> rule3) triple8) -> rule4) OR ((((triple14) -> rule3) ((triple15) -> rule5)) -> rule4))]
("rabbit" "eats" "rabbit" "+")
((((triple14) -> (rule3 % int2)) triple8) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
((((triple14) -> (rule3 % int3)) ((triple15) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The rabbit does not eat the rabbit.
False
4
inv-proof
[(((((triple14) -> rule3) triple8) -> rule4) OR ((((triple14) -> rule3) ((triple15) -> rule5)) -> rule4))]
("rabbit" "eats" "rabbit" "-")
((((triple14) -> (rule3 % int2)) triple8) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
((((triple14) -> (rule3 % int3)) ((triple15) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "nice" "-")
The lion chases the lion.
Unknown
rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "chases" "lion" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
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 eats the rabbit.[(triple2)] The lion is big.[(triple3)] The lion is green.[(triple4)] The lion is not round.[(triple6)] The lion is rough.[(triple5)] The lion likes the rabbit.[(triple7)] The rabbit chases the lion.[(triple8 OR ((triple15) -> rule5))] The rabbit does not eat the lion.[(triple9)] The rabbit is big.[(triple10)] The rabbit is green.[(triple11 OR ((triple14) -> rule1))] The rabbit is not nice.[(triple12)] The rabbit is rough.[(triple13)] The rabbit is round.[(triple14)] The rabbit likes the lion.[(triple15)] @1: The rabbit chases the rabbit.[(((triple14) -> rule3))] @2: The rabbit eats the rabbit.[(((((triple14) -> rule3) triple8) -> rule4) OR ((((triple14) -> rule3) ((triple15) -> rule5)) -> rule4))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple2
The lion is big.
("lion" "is" "big" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
triple4
The lion is not round.
("lion" "is" "round" "-")
triple6
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple7
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple8
((triple15) -> (rule5 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit does not eat the lion.
("rabbit" "eats" "lion" "-")
triple9
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
The rabbit is green.
("rabbit" "is" "green" "+")
triple11
((triple14) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple12
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple13
The rabbit is round.
("rabbit" "is" "round" "+")
triple14
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple15
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple14) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple14) -> (rule3 % int2)) triple8) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
((((triple14) -> (rule3 % int3)) ((triple15) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3