The lion chases the rabbit. The lion is big. The lion is blue. The lion is not cold. The lion is nice. The lion is rough. The lion likes the rabbit. The lion does not visit the rabbit. The rabbit chases the lion. The rabbit is big. The rabbit is blue. The rabbit is cold. The rabbit is nice. The rabbit does not like the lion. The rabbit visits the lion. If someone chases the rabbit then they visit the lion. If someone visits the lion then they chase the lion.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is not cold.
("lion" "is" "cold" "-")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone chases the rabbit then they visit the lion.
((("someone" "chases" "rabbit" "+")) -> ("someone" "visits" "lion" "+"))
If someone visits the lion then they chase the lion.
((("someone" "visits" "lion" "+")) -> ("someone" "chases" "lion" "+"))
The lion chases the rabbit.
True
1
proof
[(triple1)]
("lion" "chases" "rabbit" "+")
triple1
The lion is cold.
False
1
inv-proof
[(triple4)]
("lion" "is" "cold" "+")
triple4
The lion visits the lion.
True
2
proof
[(((triple1) -> rule1))]
("lion" "visits" "lion" "+")
((triple1) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion does not visit the lion.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "visits" "lion" "-")
((triple1) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion chases the lion.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("lion" "chases" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion does not chase the lion.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("lion" "chases" "lion" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The lion chases the rabbit.[(triple1)] The lion does not visit the rabbit.[(triple8)] The lion is big.[(triple2)] The lion is blue.[(triple3)] The lion is nice.[(triple5)] The lion is not cold.[(triple4)] The lion is rough.[(triple6)] The lion likes the rabbit.[(triple7)] The rabbit chases the lion.[(triple9 OR ((triple15) -> rule2))] The rabbit does not like the lion.[(triple14)] The rabbit is big.[(triple10)] The rabbit is blue.[(triple11)] The rabbit is cold.[(triple12)] The rabbit is nice.[(triple13)] The rabbit visits the lion.[(triple15)] @1: The lion visits the lion.[(((triple1) -> rule1))] @2: The lion chases the lion.[(((((triple1) -> rule1)) -> rule2))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
triple8
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple5
The lion is not cold.
("lion" "is" "cold" "-")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple6
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple7
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple9
((triple15) -> (rule2 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
triple14
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple11
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple12
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple13
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple15
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple1) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2