The bear is nice. The cat eats the bear. The dog is kind. If something chases the dog then the dog is not nice. Red things are kind. If something is kind then it does not chase the cat. If something chases the cat then it chases the dog. If the bear is nice then the bear is red. If the cat is red and the cat does not chase the dog then the dog chases the bear.
The bear is nice.
("bear" "is" "nice" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The dog is kind.
("dog" "is" "kind" "+")
If something chases the dog then the dog is not nice.
((("something" "chases" "dog" "+")) -> ("dog" "is" "nice" "-"))
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it does not chase the cat.
((("something" "is" "kind" "+")) -> ("something" "chases" "cat" "-"))
If something chases the cat then it chases the dog.
((("something" "chases" "cat" "+")) -> ("something" "chases" "dog" "+"))
If the bear is nice then the bear is red.
((("bear" "is" "nice" "+")) -> ("bear" "is" "red" "+"))
If the cat is red and the cat does not chase the dog then the dog chases the bear.
((("cat" "is" "red" "+") ("cat" "chases" "dog" "~")) -> ("dog" "chases" "bear" "+"))
The bear is nice.
True
1
proof
[(triple1)]
("bear" "is" "nice" "+")
triple1
The bear is not nice.
False
1
inv-proof
[(triple1)]
("bear" "is" "nice" "-")
triple1
The dog does not chase the cat.
True
2
proof
[(((triple3) -> rule3))]
("dog" "chases" "cat" "-")
((triple3) -> (rule3 % int1))
The dog does not chase the cat.
("dog" "chases" "cat" "-")
int1
The dog chases the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("dog" "chases" "cat" "+")
((triple3) -> (rule3 % int1))
The dog does not chase the cat.
("dog" "chases" "cat" "-")
int1
The bear is kind.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("bear" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is not kind.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("bear" "is" "kind" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear does not chase the cat.
True
4
proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule3))]
("bear" "chases" "cat" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear does not chase the cat.
("bear" "chases" "cat" "-")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear chases the cat.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule3))]
("bear" "chases" "cat" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear does not chase the cat.
("bear" "chases" "cat" "-")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The dog does not chase the bear.
Unknown
inv-rconc
[@1: The dog chases the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "chases" "bear" "-")
The cat chases the dog.
Unknown
rconc
[@1: The cat chases the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "chases" "dog" "+")
The cat is not kind.
Unknown
inv-rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "kind" "-")
The dog chases the dog.
Unknown
rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "chases" "dog" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The dog needs the bear.
Unknown
random
[@0: The dog needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "bear" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The bear eats the cat.
Unknown
random
[@0: The bear eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cat" "+")
@0: The bear is nice.[(triple1)] The cat eats the bear.[(triple2)] The dog is kind.[(triple3)] @1: The bear is red.[(((triple1) -> rule5))] The dog does not chase the cat.[(((triple3) -> rule3))] @2: The bear is kind.[(((((triple1) -> rule5)) -> rule2))] @3: The bear does not chase the cat.[(((((((triple1) -> rule5)) -> rule2)) -> rule3))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The cat eats the bear.
("cat" "eats" "bear" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The bear is red.
("bear" "is" "red" "+")
((triple1) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The dog does not chase the cat.
("dog" "chases" "cat" "-")
((triple3) -> (rule3 % int1))
The dog does not chase the cat.
("dog" "chases" "cat" "-")
int1
The bear is kind.
("bear" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear does not chase the cat.
("bear" "chases" "cat" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear does not chase the cat.
("bear" "chases" "cat" "-")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3