The lion chases the tiger. The lion is red. The lion is round. The lion sees the tiger. The rabbit chases the lion. The rabbit is not nice. The rabbit does not like the lion. The rabbit sees the lion. The tiger is not red. The tiger sees the rabbit. If the tiger is nice then the tiger sees the lion. If someone sees the rabbit then the rabbit is round.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The tiger is not red.
("tiger" "is" "red" "-")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If the tiger is nice then the tiger sees the lion.
((("tiger" "is" "nice" "+")) -> ("tiger" "sees" "lion" "+"))
If someone sees the rabbit then the rabbit is round.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
The tiger sees the rabbit.
True
1
proof
[(triple10)]
("tiger" "sees" "rabbit" "+")
triple10
The rabbit does not see the lion.
False
1
inv-proof
[(triple8)]
("rabbit" "sees" "lion" "-")
triple8
The rabbit is round.
True
2
proof
[(((triple10) -> rule2))]
("rabbit" "is" "round" "+")
((triple10) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple10) -> rule2))]
("rabbit" "is" "round" "-")
((triple10) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The tiger does not see the lion.
Unknown
inv-rconc
[@1: The tiger sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "lion" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The tiger likes the rabbit.
Unknown
random
[@0: The tiger likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "rabbit" "+")
@0: The lion chases the tiger.[(triple1)] The lion is red.[(triple2)] The lion is round.[(triple3)] The lion sees the tiger.[(triple4)] The rabbit chases the lion.[(triple5)] The rabbit does not like the lion.[(triple7)] The rabbit is not nice.[(triple6)] The rabbit sees the lion.[(triple8)] The tiger is not red.[(triple9)] The tiger sees the rabbit.[(triple10)] @1: The rabbit is round.[(((triple10) -> rule2))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple4
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple5
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
triple7
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple6
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple8
The tiger is not red.
("tiger" "is" "red" "-")
triple9
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
((triple10) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1