The bear is big. The bear is green. The bear is nice. The bear is red. The bear is rough. The bear likes the dog. The bear needs the dog. The bear visits the dog. The dog is big. The dog is green. The dog is nice. The dog is red. The dog is rough. The dog likes the bear. The dog needs the bear. The dog visits the bear. If the dog is nice and the dog needs the bear then the bear likes the dog. If the bear needs the dog then the bear likes the dog. If something visits the bear and the bear needs the dog then the dog visits the bear. If something needs the dog and the dog visits the bear then the bear is red. If the dog is red then the dog visits the bear. If something visits the bear and the bear likes the dog then it visits the dog.
The bear is big.
("bear" "is" "big" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
If the dog is nice and the dog needs the bear then the bear likes the dog.
((("dog" "is" "nice" "+") ("dog" "needs" "bear" "+")) -> ("bear" "likes" "dog" "+"))
If the bear needs the dog then the bear likes the dog.
((("bear" "needs" "dog" "+")) -> ("bear" "likes" "dog" "+"))
If something visits the bear and the bear needs the dog then the dog visits the bear.
((("something" "visits" "bear" "+") ("bear" "needs" "dog" "+")) -> ("dog" "visits" "bear" "+"))
If something needs the dog and the dog visits the bear then the bear is red.
((("something" "needs" "dog" "+") ("dog" "visits" "bear" "+")) -> ("bear" "is" "red" "+"))
If the dog is red then the dog visits the bear.
((("dog" "is" "red" "+")) -> ("dog" "visits" "bear" "+"))
If something visits the bear and the bear likes the dog then it visits the dog.
((("something" "visits" "bear" "+") ("bear" "likes" "dog" "+")) -> ("something" "visits" "dog" "+"))
The dog needs the bear.
True
1
proof
[(triple15)]
("dog" "needs" "bear" "+")
triple15
The dog does not need the bear.
False
1
inv-proof
[(triple15)]
("dog" "needs" "bear" "-")
triple15
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The bear is big.[(triple1)] The bear is green.[(triple2)] The bear is nice.[(triple3)] The bear is red.[(triple4 OR ((triple7 triple16) -> rule4) OR ((triple7 ((triple12) -> rule5)) -> rule4))] The bear is rough.[(triple5)] The bear likes the dog.[(triple6 OR ((triple7) -> rule2) OR ((triple11 triple15) -> rule1))] The bear needs the dog.[(triple7)] The bear visits the dog.[(triple8)] The dog is big.[(triple9)] The dog is green.[(triple10)] The dog is nice.[(triple11)] The dog is red.[(triple12)] The dog is rough.[(triple13)] The dog likes the bear.[(triple14)] The dog needs the bear.[(triple15)] The dog visits the bear.[(triple16 OR ((triple12) -> rule5))] @1: The dog visits the dog.[(((triple16 triple6) -> rule6) OR ((triple16 ((triple7) -> rule2)) -> rule6) OR ((triple16 ((triple11 triple15) -> rule1)) -> rule6) OR ((((triple12) -> rule5) triple6) -> rule6) OR ((((triple12) -> rule5) ((triple7) -> rule2)) -> rule6) OR ((((triple12) -> rule5) ((triple11 triple15) -> rule1)) -> rule6))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
The bear is red.
("bear" "is" "red" "+")
triple4
((triple7 triple16) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
((triple7 ((triple12) -> (rule5 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
triple5
The bear likes the dog.
("bear" "likes" "dog" "+")
triple6
((triple7) -> (rule2 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
((triple11 triple15) -> (rule1 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
triple7
The bear visits the dog.
("bear" "visits" "dog" "+")
triple8
The dog is big.
("dog" "is" "big" "+")
triple9
The dog is green.
("dog" "is" "green" "+")
triple10
The dog is nice.
("dog" "is" "nice" "+")
triple11
The dog is red.
("dog" "is" "red" "+")
triple12
The dog is rough.
("dog" "is" "rough" "+")
triple13
The dog likes the bear.
("dog" "likes" "bear" "+")
triple14
The dog needs the bear.
("dog" "needs" "bear" "+")
triple15
The dog visits the bear.
("dog" "visits" "bear" "+")
triple16
((triple12) -> (rule5 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple16 triple6) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((triple16 ((triple7) -> (rule2 % int2))) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
((triple16 ((triple11 triple15) -> (rule1 % int2))) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
((((triple12) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
int2
((((triple12) -> (rule5 % int3)) ((triple7) -> (rule2 % int2))) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
int3
((((triple12) -> (rule5 % int3)) ((triple11 triple15) -> (rule1 % int2))) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
int3