The bear does not chase the dog. The bear does not eat the tiger. The bear does not see the dog. The bear sees the tiger. The dog does not chase the tiger. The dog is young. The tiger sees the dog. If the bear sees the dog then the bear is not kind. If something sees the dog then it sees the tiger. If something is red and it does not see the tiger then the tiger eats the dog.
The bear does not chase the dog.
("bear" "chases" "dog" "-")
The bear does not eat the tiger.
("bear" "eats" "tiger" "-")
The bear does not see the dog.
("bear" "sees" "dog" "-")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
The dog is young.
("dog" "is" "young" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If the bear sees the dog then the bear is not kind.
((("bear" "sees" "dog" "+")) -> ("bear" "is" "kind" "-"))
If something sees the dog then it sees the tiger.
((("something" "sees" "dog" "+")) -> ("something" "sees" "tiger" "+"))
If something is red and it does not see the tiger then the tiger eats the dog.
((("something" "is" "red" "+") ("something" "sees" "tiger" "~")) -> ("tiger" "eats" "dog" "+"))
The dog is young.
True
1
proof
[(triple6)]
("dog" "is" "young" "+")
triple6
The bear chases the dog.
False
1
inv-proof
[(triple1)]
("bear" "chases" "dog" "+")
triple1
The tiger sees the tiger.
True
2
proof
[(((triple7) -> rule2))]
("tiger" "sees" "tiger" "+")
((triple7) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not see the tiger.
False
2
inv-proof
[(((triple7) -> rule2))]
("tiger" "sees" "tiger" "-")
((triple7) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not eat the dog.
Unknown
inv-rconc
[@1: The tiger eats the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "eats" "dog" "-")
The dog sees the tiger.
Unknown
rconc
[@1: The dog sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "tiger" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog eats the bear.
Unknown
random
[@0: The dog eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "bear" "+")
@0: The bear does not chase the dog.[(triple1)] The bear does not eat the tiger.[(triple2)] The bear does not see the dog.[(triple3)] The bear sees the tiger.[(triple4)] The dog does not chase the tiger.[(triple5)] The dog is young.[(triple6)] The tiger sees the dog.[(triple7)] @1: The tiger sees the tiger.[(((triple7) -> rule2))]
The bear does not chase the dog.
("bear" "chases" "dog" "-")
triple1
The bear does not eat the tiger.
("bear" "eats" "tiger" "-")
triple2
The bear does not see the dog.
("bear" "sees" "dog" "-")
triple3
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple4
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple7
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple7) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1