The bear eats the dog. The bear is blue. The bear is rough. The dog needs the lion. The lion eats the dog. The lion is blue. The lion is nice. The lion is rough. The lion is round. The lion needs the bear. The lion needs the dog. The lion sees the dog. If someone is rough then they need the lion. If someone needs the lion then the lion needs the dog.
The bear eats the dog.
("bear" "eats" "dog" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is rough.
("bear" "is" "rough" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
If someone is rough then they need the lion.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the lion then the lion needs the dog.
((("someone" "needs" "lion" "+")) -> ("lion" "needs" "dog" "+"))
The lion is rough.
True
1
proof
[(triple8)]
("lion" "is" "rough" "+")
triple8
The lion does not need the bear.
False
1
inv-proof
[(triple10)]
("lion" "needs" "bear" "-")
triple10
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear eats the dog.[(triple1)] The bear is blue.[(triple2)] The bear is rough.[(triple3)] The dog needs the lion.[(triple4)] The lion eats the dog.[(triple5)] The lion is blue.[(triple6)] The lion is nice.[(triple7)] The lion is rough.[(triple8)] The lion is round.[(triple9)] The lion needs the bear.[(triple10)] The lion needs the dog.[(triple11 OR ((triple4) -> rule2) OR ((((triple3) -> rule1)) -> rule2) OR ((((triple8) -> rule1)) -> rule2))] The lion sees the dog.[(triple12)] @1: The bear needs the lion.[(((triple3) -> rule1))] The lion needs the lion.[(((triple8) -> rule1))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The dog needs the lion.
("dog" "needs" "lion" "+")
triple4
The lion eats the dog.
("lion" "eats" "dog" "+")
triple5
The lion is blue.
("lion" "is" "blue" "+")
triple6
The lion is nice.
("lion" "is" "nice" "+")
triple7
The lion is rough.
("lion" "is" "rough" "+")
triple8
The lion is round.
("lion" "is" "round" "+")
triple9
The lion needs the bear.
("lion" "needs" "bear" "+")
triple10
The lion needs the dog.
("lion" "needs" "dog" "+")
triple11
((triple4) -> (rule2 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
triple12
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple3) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple8) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1