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