The lion chases the rabbit. The lion is blue. The lion is cold. The lion is red. The lion is young. The lion likes the rabbit. The lion visits the rabbit. The rabbit chases the lion. The rabbit is blue. The rabbit is cold. The rabbit is red. The rabbit is rough. The rabbit is young. The rabbit does not like the lion. The rabbit visits the lion. If something likes the lion then it visits the rabbit. If something is young and it does not like the lion then it visits the rabbit.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If something likes the lion then it visits the rabbit.
((("something" "likes" "lion" "+")) -> ("something" "visits" "rabbit" "+"))
If something is young and it does not like the lion then it visits the rabbit.
((("something" "is" "young" "+") ("something" "likes" "lion" "~")) -> ("something" "visits" "rabbit" "+"))
The rabbit is rough.
True
1
proof
[(triple12)]
("rabbit" "is" "rough" "+")
triple12
The lion does not like the rabbit.
False
1
inv-proof
[(triple6)]
("lion" "likes" "rabbit" "-")
triple6
The rabbit visits the rabbit.
True
3
proof
[(((triple13 triple14) -> rule2))]
("rabbit" "visits" "rabbit" "+")
((triple13 triple14) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit does not visit the rabbit.
False
3
inv-proof
[(((triple13 triple14) -> rule2))]
("rabbit" "visits" "rabbit" "-")
((triple13 triple14) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
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 likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The lion chases the rabbit.[(triple1)] The lion is blue.[(triple2)] The lion is cold.[(triple3)] The lion is red.[(triple4)] The lion is young.[(triple5)] The lion likes the rabbit.[(triple6)] The lion visits the rabbit.[(triple7)] The rabbit chases the lion.[(triple8)] The rabbit does not like the lion.[(triple14)] The rabbit is blue.[(triple9)] The rabbit is cold.[(triple10)] The rabbit is red.[(triple11)] The rabbit is rough.[(triple12)] The rabbit is young.[(triple13)] The rabbit visits the lion.[(triple15)] @1: The rabbit visits the rabbit.[(((triple13 triple14) -> rule2))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion is red.
("lion" "is" "red" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple6
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple7
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple8
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
triple14
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple10
The rabbit is red.
("rabbit" "is" "red" "+")
triple11
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple12
The rabbit is young.
("rabbit" "is" "young" "+")
triple13
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple15
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple13 triple14) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1