The bear eats the dog. The bear is big. The bear is blue. The bear is green. The bear is red. The bear is rough. The bear sees the dog. The bear visits the dog. The dog is big. The dog is blue. The dog is green. The dog is red. The dog is rough. The dog sees the bear. The dog visits the bear. If someone is blue then they see the dog. Rough people are blue. If someone sees the dog then the dog is blue. If the dog eats the bear then the bear visits the dog. If someone eats the dog and the dog eats the bear then they are red. If the bear visits the dog and the bear sees the dog then the bear is rough.
The bear eats the dog.
("bear" "eats" "dog" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
If someone is blue then they see the dog.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "dog" "+"))
Rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the dog then the dog is blue.
((("someone" "sees" "dog" "+")) -> ("dog" "is" "blue" "+"))
If the dog eats the bear then the bear visits the dog.
((("dog" "eats" "bear" "+")) -> ("bear" "visits" "dog" "+"))
If someone eats the dog and the dog eats the bear then they are red.
((("someone" "eats" "dog" "+") ("dog" "eats" "bear" "+")) -> ("someone" "is" "red" "+"))
If the bear visits the dog and the bear sees the dog then the bear is rough.
((("bear" "visits" "dog" "+") ("bear" "sees" "dog" "+")) -> ("bear" "is" "rough" "+"))
The dog is red.
True
1
proof
[(triple12)]
("dog" "is" "red" "+")
triple12
The dog is not big.
False
1
inv-proof
[(triple9)]
("dog" "is" "big" "-")
triple9
The dog sees the dog.
True
2
proof
[(((triple10) -> rule1) OR ((((triple13) -> rule2)) -> rule1) OR ((((triple7) -> rule3)) -> rule1) OR ((((((triple3) -> rule1)) -> rule3)) -> rule1) OR ((((((((triple6) -> rule2)) -> rule1)) -> rule3)) -> rule1))]
("dog" "sees" "dog" "+")
((triple10) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The bear sees the dog.
("bear" "sees" "dog" "+")
int3
((((((((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The bear sees the dog.
("bear" "sees" "dog" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
The dog does not see the dog.
False
2
inv-proof
[(((triple10) -> rule1) OR ((((triple13) -> rule2)) -> rule1) OR ((((triple7) -> rule3)) -> rule1) OR ((((((triple3) -> rule1)) -> rule3)) -> rule1) OR ((((((((triple6) -> rule2)) -> rule1)) -> rule3)) -> rule1))]
("dog" "sees" "dog" "-")
((triple10) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The bear sees the dog.
("bear" "sees" "dog" "+")
int3
((((((((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The bear sees the dog.
("bear" "sees" "dog" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The bear eats the dog.[(triple1)] The bear is big.[(triple2)] The bear is blue.[(triple3 OR ((triple6) -> rule2) OR ((((triple8 triple7) -> rule6)) -> rule2))] The bear is green.[(triple4)] The bear is red.[(triple5)] The bear is rough.[(triple6 OR ((triple8 triple7) -> rule6) OR ((triple8 ((triple3) -> rule1)) -> rule6))] The bear sees the dog.[(triple7 OR ((triple3) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] The bear visits the dog.[(triple8)] The dog is big.[(triple9)] The dog is blue.[(triple10 OR ((triple13) -> rule2) OR ((triple7) -> rule3) OR ((((triple3) -> rule1)) -> rule3) OR ((((((triple6) -> rule2)) -> rule1)) -> rule3))] The dog is green.[(triple11)] The dog is red.[(triple12)] The dog is rough.[(triple13)] The dog sees the bear.[(triple14)] The dog visits the bear.[(triple15)] @1: The dog sees the dog.[(((triple10) -> rule1) OR ((((triple13) -> rule2)) -> rule1) OR ((((triple7) -> rule3)) -> rule1) OR ((((((triple3) -> rule1)) -> rule3)) -> rule1) OR ((((((((triple6) -> rule2)) -> rule1)) -> rule3)) -> rule1))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is blue.
("bear" "is" "blue" "+")
triple3
((triple6) -> (rule2 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((((triple8 triple7) -> (rule6 % int2))) -> (rule2 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear is green.
("bear" "is" "green" "+")
triple4
The bear is red.
("bear" "is" "red" "+")
triple5
The bear is rough.
("bear" "is" "rough" "+")
triple6
((triple8 triple7) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
((triple8 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
The bear sees the dog.
("bear" "sees" "dog" "+")
triple7
((triple3) -> (rule1 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear visits the dog.
("bear" "visits" "dog" "+")
triple8
The dog is big.
("dog" "is" "big" "+")
triple9
The dog is blue.
("dog" "is" "blue" "+")
triple10
((triple13) -> (rule2 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((triple7) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The dog is green.
("dog" "is" "green" "+")
triple11
The dog is red.
("dog" "is" "red" "+")
triple12
The dog is rough.
("dog" "is" "rough" "+")
triple13
The dog sees the bear.
("dog" "sees" "bear" "+")
triple14
The dog visits the bear.
("dog" "visits" "bear" "+")
triple15
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple10) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The bear sees the dog.
("bear" "sees" "dog" "+")
int3
((((((((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The bear sees the dog.
("bear" "sees" "dog" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4