The lion is blue. The lion is nice. The lion is red. The lion is young. The lion likes the rabbit. The lion needs the rabbit. The lion sees the rabbit. The rabbit is big. The rabbit is blue. The rabbit is not nice. The rabbit is not red. The rabbit is not young. The rabbit likes the lion. The rabbit needs the lion. The rabbit sees the lion. If the lion does not see the rabbit then the rabbit does not need the lion. If something likes the rabbit then the rabbit sees the lion. If the rabbit needs the lion then the lion likes the rabbit. If something is red and it sees the lion then the lion likes the rabbit. If the rabbit sees the lion then the rabbit is not young. If something sees the lion then the lion needs the rabbit. If something is red and it does not need the lion then the lion is not young. If the rabbit is red and the rabbit does not see the lion then the rabbit is not blue.
The lion is blue.
("lion" "is" "blue" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit is not red.
("rabbit" "is" "red" "-")
The rabbit is not young.
("rabbit" "is" "young" "-")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If the lion does not see the rabbit then the rabbit does not need the lion.
((("lion" "sees" "rabbit" "~")) -> ("rabbit" "needs" "lion" "-"))
If something likes the rabbit then the rabbit sees the lion.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
If the rabbit needs the lion then the lion likes the rabbit.
((("rabbit" "needs" "lion" "+")) -> ("lion" "likes" "rabbit" "+"))
If something is red and it sees the lion then the lion likes the rabbit.
((("something" "is" "red" "+") ("something" "sees" "lion" "+")) -> ("lion" "likes" "rabbit" "+"))
If the rabbit sees the lion then the rabbit is not young.
((("rabbit" "sees" "lion" "+")) -> ("rabbit" "is" "young" "-"))
If something sees the lion then the lion needs the rabbit.
((("something" "sees" "lion" "+")) -> ("lion" "needs" "rabbit" "+"))
If something is red and it does not need the lion then the lion is not young.
((("something" "is" "red" "+") ("something" "needs" "lion" "~")) -> ("lion" "is" "young" "-"))
If the rabbit is red and the rabbit does not see the lion then the rabbit is not blue.
((("rabbit" "is" "red" "+") ("rabbit" "sees" "lion" "~")) -> ("rabbit" "is" "blue" "-"))
The rabbit needs the lion.
True
1
proof
[(triple14)]
("rabbit" "needs" "lion" "+")
triple14
The rabbit does not see the lion.
False
1
inv-proof
[(triple15 OR ((triple5) -> rule2) OR ((((triple14) -> rule3)) -> rule2))]
("rabbit" "sees" "lion" "-")
triple15
((triple5) -> (rule2 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
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 is blue.[(triple1)] The lion is nice.[(triple2)] The lion is red.[(triple3)] The lion is young.[(triple4)] The lion likes the rabbit.[(triple5 OR ((triple14) -> rule3))] The lion needs the rabbit.[(triple6 OR ((triple15) -> rule6) OR ((((triple5) -> rule2)) -> rule6) OR ((((((triple14) -> rule3)) -> rule2)) -> rule6))] The lion sees the rabbit.[(triple7)] The rabbit is big.[(triple8)] The rabbit is blue.[(triple9)] The rabbit is not nice.[(triple10)] The rabbit is not red.[(triple11)] The rabbit is not young.[(triple12 OR ((triple15) -> rule5) OR ((((triple5) -> rule2)) -> rule5) OR ((((((triple14) -> rule3)) -> rule2)) -> rule5))] The rabbit likes the lion.[(triple13)] The rabbit needs the lion.[(triple14)] The rabbit sees the lion.[(triple15 OR ((triple5) -> rule2) OR ((((triple14) -> rule3)) -> rule2))]
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The lion is young.
("lion" "is" "young" "+")
triple4
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple5
((triple14) -> (rule3 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple6
((triple15) -> (rule6 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule6 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
((((((triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple7
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple10
The rabbit is not red.
("rabbit" "is" "red" "-")
triple11
The rabbit is not young.
("rabbit" "is" "young" "-")
triple12
((triple15) -> (rule5 % int1))
The rabbit is not young.
("rabbit" "is" "young" "-")
int1
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is not young.
("rabbit" "is" "young" "-")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
((((((triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is not young.
("rabbit" "is" "young" "-")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int3
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple13
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple14
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple15
((triple5) -> (rule2 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2