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