The lion chases the rabbit. The lion is big. The lion is green. The lion is not nice. The lion is rough. The lion is young. The lion does not see the rabbit. The lion visits the rabbit. The rabbit chases the lion. The rabbit is big. The rabbit is green. The rabbit is not nice. The rabbit is rough. The rabbit sees the lion. The rabbit visits the lion. If someone sees the lion and they see the rabbit then the lion chases the rabbit. If someone sees the lion and the lion sees the rabbit then the lion does not chase the rabbit. If the rabbit visits the lion and the lion is rough then the rabbit is young.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is not nice.
("lion" "is" "nice" "-")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "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 sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone sees the lion and they see the rabbit then the lion chases the rabbit.
((("someone" "sees" "lion" "+") ("someone" "sees" "rabbit" "+")) -> ("lion" "chases" "rabbit" "+"))
If someone sees the lion and the lion sees the rabbit then the lion does not chase the rabbit.
((("someone" "sees" "lion" "+") ("lion" "sees" "rabbit" "+")) -> ("lion" "chases" "rabbit" "-"))
If the rabbit visits the lion and the lion is rough then the rabbit is young.
((("rabbit" "visits" "lion" "+") ("lion" "is" "rough" "+")) -> ("rabbit" "is" "young" "+"))
The rabbit is rough.
True
1
proof
[(triple13)]
("rabbit" "is" "rough" "+")
triple13
The lion is not young.
False
1
inv-proof
[(triple6)]
("lion" "is" "young" "-")
triple6
The rabbit is young.
True
3
proof
[(((triple15 triple5) -> rule3))]
("rabbit" "is" "young" "+")
((triple15 triple5) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is not young.
False
3
inv-proof
[(((triple15 triple5) -> rule3))]
("rabbit" "is" "young" "-")
((triple15 triple5) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
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 visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "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 does not see the rabbit.[(triple7)] The lion is big.[(triple2)] The lion is green.[(triple3)] The lion is not nice.[(triple4)] The lion is rough.[(triple5)] The lion is young.[(triple6)] The lion visits the rabbit.[(triple8)] The rabbit chases the lion.[(triple9)] The rabbit is big.[(triple10)] The rabbit is green.[(triple11)] The rabbit is not nice.[(triple12)] The rabbit is rough.[(triple13)] The rabbit sees the lion.[(triple14)] The rabbit visits the lion.[(triple15)] @1: The rabbit is young.[(((triple15 triple5) -> rule3))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
triple7
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is not nice.
("lion" "is" "nice" "-")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple8
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple9
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
The rabbit is green.
("rabbit" "is" "green" "+")
triple11
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple12
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple13
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple14
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple15
The rabbit is young.
("rabbit" "is" "young" "+")
((triple15 triple5) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1