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