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