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