The lion chases the rabbit. The lion is big. The lion is cold. The lion is green. The lion is kind. The lion is not young. The lion needs the rabbit. The lion sees the rabbit. The rabbit does not chase the lion. The rabbit is big. The rabbit is not cold. The rabbit is green. The rabbit is kind. The rabbit is young. The rabbit needs the lion. The rabbit sees the lion. If something sees the lion and it is young then it chases the rabbit. If the rabbit chases the lion and the lion sees the rabbit then the lion is cold.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is not young.
("lion" "is" "young" "-")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is not cold.
("rabbit" "is" "cold" "-")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If something sees the lion and it is young then it chases the rabbit.
((("something" "sees" "lion" "+") ("something" "is" "young" "+")) -> ("something" "chases" "rabbit" "+"))
If the rabbit chases the lion and the lion sees the rabbit then the lion is cold.
((("rabbit" "chases" "lion" "+") ("lion" "sees" "rabbit" "+")) -> ("lion" "is" "cold" "+"))
The rabbit is young.
True
1
proof
[(triple14)]
("rabbit" "is" "young" "+")
triple14
The rabbit chases the lion.
False
1
inv-proof
[(triple9)]
("rabbit" "chases" "lion" "+")
triple9
The rabbit chases the rabbit.
True
3
proof
[(((triple16 triple14) -> rule1))]
("rabbit" "chases" "rabbit" "+")
((triple16 triple14) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit does not chase the rabbit.
False
3
inv-proof
[(((triple16 triple14) -> rule1))]
("rabbit" "chases" "rabbit" "-")
((triple16 triple14) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The lion chases the rabbit.[(triple1)] The lion is big.[(triple2)] The lion is cold.[(triple3)] The lion is green.[(triple4)] The lion is kind.[(triple5)] The lion is not young.[(triple6)] The lion needs the rabbit.[(triple7)] The lion sees the rabbit.[(triple8)] The rabbit does not chase the lion.[(triple9)] The rabbit is big.[(triple10)] The rabbit is green.[(triple12)] The rabbit is kind.[(triple13)] The rabbit is not cold.[(triple11)] The rabbit is young.[(triple14)] The rabbit needs the lion.[(triple15)] The rabbit sees the lion.[(triple16)] @1: The rabbit chases the rabbit.[(((triple16 triple14) -> rule1))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
triple4
The lion is kind.
("lion" "is" "kind" "+")
triple5
The lion is not young.
("lion" "is" "young" "-")
triple6
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple7
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple8
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
triple9
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
The rabbit is green.
("rabbit" "is" "green" "+")
triple12
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple13
The rabbit is not cold.
("rabbit" "is" "cold" "-")
triple11
The rabbit is young.
("rabbit" "is" "young" "+")
triple14
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple15
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple16
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple16 triple14) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1