The lion is blue. The lion is cold. The lion is not green. The lion is kind. The lion is rough. The lion likes the rabbit. The lion sees the rabbit. The lion visits the rabbit. The rabbit is blue. The rabbit is not cold. The rabbit is green. The rabbit is kind. The rabbit is not rough. The rabbit likes the lion. The rabbit sees the lion. The rabbit visits the lion. If someone is kind then they see the lion. If someone is blue and they like the lion then they see the lion. If someone visits the lion and the lion is blue then the lion sees the rabbit. If someone sees the lion and they do not visit the lion then they are rough. If someone likes the lion and they are not rough then they visit the rabbit. If someone visits the lion and they do not see the lion then they do not visit the rabbit.
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is not green.
("lion" "is" "green" "-")
The lion is kind.
("lion" "is" "kind" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
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 not rough.
("rabbit" "is" "rough" "-")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone is kind then they see the lion.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "lion" "+"))
If someone is blue and they like the lion then they see the lion.
((("someone" "is" "blue" "+") ("someone" "likes" "lion" "+")) -> ("someone" "sees" "lion" "+"))
If someone visits the lion and the lion is blue then the lion sees the rabbit.
((("someone" "visits" "lion" "+") ("lion" "is" "blue" "+")) -> ("lion" "sees" "rabbit" "+"))
If someone sees the lion and they do not visit the lion then they are rough.
((("someone" "sees" "lion" "+") ("someone" "visits" "lion" "~")) -> ("someone" "is" "rough" "+"))
If someone likes the lion and they are not rough then they visit the rabbit.
((("someone" "likes" "lion" "+") ("someone" "is" "rough" "~")) -> ("someone" "visits" "rabbit" "+"))
If someone visits the lion and they do not see the lion then they do not visit the rabbit.
((("someone" "visits" "lion" "+") ("someone" "sees" "lion" "~")) -> ("someone" "visits" "rabbit" "-"))
The rabbit sees the lion.
True
1
proof
[(triple15 OR ((triple12) -> rule1) OR ((triple9 triple14) -> rule2))]
("rabbit" "sees" "lion" "+")
triple15
((triple12) -> (rule1 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
((triple9 triple14) -> (rule2 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit does not visit the lion.
False
1
inv-proof
[(triple16)]
("rabbit" "visits" "lion" "-")
triple16
The rabbit visits the rabbit.
True
3
proof
[(((triple14 triple13) -> rule5))]
("rabbit" "visits" "rabbit" "+")
((triple14 triple13) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The lion does not see the lion.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "sees" "lion" "-")
((triple4) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The lion is blue.[(triple1)] The lion is cold.[(triple2)] The lion is kind.[(triple4)] The lion is not green.[(triple3)] The lion is rough.[(triple5)] The lion likes the rabbit.[(triple6)] The lion sees the rabbit.[(triple7 OR ((triple16 triple1) -> rule3))] The lion visits the rabbit.[(triple8)] The rabbit is blue.[(triple9)] The rabbit is green.[(triple11)] The rabbit is kind.[(triple12)] The rabbit is not cold.[(triple10)] The rabbit is not rough.[(triple13)] The rabbit likes the lion.[(triple14)] The rabbit sees the lion.[(triple15 OR ((triple12) -> rule1) OR ((triple9 triple14) -> rule2))] The rabbit visits the lion.[(triple16)] @1: The lion sees the lion.[(((triple4) -> rule1))] The rabbit visits the rabbit.[(((triple14 triple13) -> rule5))]
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple4
The lion is not green.
("lion" "is" "green" "-")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple6
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple7
((triple16 triple1) -> (rule3 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit is green.
("rabbit" "is" "green" "+")
triple11
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple12
The rabbit is not cold.
("rabbit" "is" "cold" "-")
triple10
The rabbit is not rough.
("rabbit" "is" "rough" "-")
triple13
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple14
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple15
((triple12) -> (rule1 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
((triple9 triple14) -> (rule2 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple16
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple4) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple14 triple13) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1