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