The bear eats the dog. The bear is nice. The bear sees the dog. The dog eats the lion. The dog is cold. The dog is young. The dog likes the bear. The dog likes the lion. The lion eats the bear. The lion eats the dog. The lion is cold. The lion is nice. The lion is young. The lion sees the bear. The lion sees the dog. If something sees the dog then the dog sees the bear. If something sees the bear then it eats the bear.
The bear eats the dog.
("bear" "eats" "dog" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
If something sees the dog then the dog sees the bear.
((("something" "sees" "dog" "+")) -> ("dog" "sees" "bear" "+"))
If something sees the bear then it eats the bear.
((("something" "sees" "bear" "+")) -> ("something" "eats" "bear" "+"))
The dog is cold.
True
1
proof
[(triple5)]
("dog" "is" "cold" "+")
triple5
The lion does not see the bear.
False
1
inv-proof
[(triple14)]
("lion" "sees" "bear" "-")
triple14
The dog sees the bear.
True
2
proof
[(((triple15) -> rule1) OR ((triple3) -> rule1))]
("dog" "sees" "bear" "+")
((triple15) -> (rule1 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
((triple3) -> (rule1 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog does not see the bear.
False
2
inv-proof
[(((triple15) -> rule1) OR ((triple3) -> rule1))]
("dog" "sees" "bear" "-")
((triple15) -> (rule1 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
((triple3) -> (rule1 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog eats the bear.
True
3
proof
[(((((triple15) -> rule1)) -> rule2) OR ((((triple3) -> rule1)) -> rule2))]
("dog" "eats" "bear" "+")
((((triple15) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog sees the bear.
("dog" "sees" "bear" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog sees the bear.
("dog" "sees" "bear" "+")
int2
The dog does not eat the bear.
False
3
inv-proof
[(((((triple15) -> rule1)) -> rule2) OR ((((triple3) -> rule1)) -> rule2))]
("dog" "eats" "bear" "-")
((((triple15) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog sees the bear.
("dog" "sees" "bear" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog sees the bear.
("dog" "sees" "bear" "+")
int2
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "bear" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
@0: The bear eats the dog.[(triple1)] The bear is nice.[(triple2)] The bear sees the dog.[(triple3)] The dog eats the lion.[(triple4)] The dog is cold.[(triple5)] The dog is young.[(triple6)] The dog likes the bear.[(triple7)] The dog likes the lion.[(triple8)] The lion eats the bear.[(triple9 OR ((triple14) -> rule2))] The lion eats the dog.[(triple10)] The lion is cold.[(triple11)] The lion is nice.[(triple12)] The lion is young.[(triple13)] The lion sees the bear.[(triple14)] The lion sees the dog.[(triple15)] @1: The dog sees the bear.[(((triple15) -> rule1) OR ((triple3) -> rule1))] @2: The dog eats the bear.[(((((triple15) -> rule1)) -> rule2) OR ((((triple3) -> rule1)) -> rule2))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear sees the dog.
("bear" "sees" "dog" "+")
triple3
The dog eats the lion.
("dog" "eats" "lion" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
The dog likes the bear.
("dog" "likes" "bear" "+")
triple7
The dog likes the lion.
("dog" "likes" "lion" "+")
triple8
The lion eats the bear.
("lion" "eats" "bear" "+")
triple9
((triple14) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion eats the dog.
("lion" "eats" "dog" "+")
triple10
The lion is cold.
("lion" "is" "cold" "+")
triple11
The lion is nice.
("lion" "is" "nice" "+")
triple12
The lion is young.
("lion" "is" "young" "+")
triple13
The lion sees the bear.
("lion" "sees" "bear" "+")
triple14
The lion sees the dog.
("lion" "sees" "dog" "+")
triple15
The dog sees the bear.
("dog" "sees" "bear" "+")
((triple15) -> (rule1 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
((triple3) -> (rule1 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
((((triple15) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog sees the bear.
("dog" "sees" "bear" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog sees the bear.
("dog" "sees" "bear" "+")
int2