The bear does not like the lion. The bear does not need the rabbit. The bear does not see the rabbit. The lion is big. The lion is blue. The lion is not red. The lion does not need the bear. The lion sees the rabbit. The rabbit is rough. The rabbit needs the bear. The rabbit needs the lion. The rabbit sees the bear. If something needs the lion then the lion sees the bear.
The bear does not like the lion.
("bear" "likes" "lion" "-")
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is not red.
("lion" "is" "red" "-")
The lion does not need the bear.
("lion" "needs" "bear" "-")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
If something needs the lion then the lion sees the bear.
((("something" "needs" "lion" "+")) -> ("lion" "sees" "bear" "+"))
The lion does not need the bear.
True
1
proof
[(triple7)]
("lion" "needs" "bear" "-")
triple7
The rabbit is not rough.
False
1
inv-proof
[(triple9)]
("rabbit" "is" "rough" "-")
triple9
The lion sees the bear.
True
2
proof
[(((triple11) -> rule1))]
("lion" "sees" "bear" "+")
((triple11) -> (rule1 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The lion does not see the bear.
False
2
inv-proof
[(((triple11) -> rule1))]
("lion" "sees" "bear" "-")
((triple11) -> (rule1 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The rabbit does not see the lion.
Unknown
inv-random
[@0: The rabbit sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "lion" "-")
The lion likes the rabbit.
Unknown
random
[@0: The lion likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "rabbit" "+")
@0: The bear does not like the lion.[(triple1)] The bear does not need the rabbit.[(triple2)] The bear does not see the rabbit.[(triple3)] The lion does not need the bear.[(triple7)] The lion is big.[(triple4)] The lion is blue.[(triple5)] The lion is not red.[(triple6)] The lion sees the rabbit.[(triple8)] The rabbit is rough.[(triple9)] The rabbit needs the bear.[(triple10)] The rabbit needs the lion.[(triple11)] The rabbit sees the bear.[(triple12)] @1: The lion sees the bear.[(((triple11) -> rule1))]
The bear does not like the lion.
("bear" "likes" "lion" "-")
triple1
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
triple2
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
triple3
The lion does not need the bear.
("lion" "needs" "bear" "-")
triple7
The lion is big.
("lion" "is" "big" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion is not red.
("lion" "is" "red" "-")
triple6
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple8
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple9
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple10
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple11
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple12
The lion sees the bear.
("lion" "sees" "bear" "+")
((triple11) -> (rule1 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1