The bear sees the dog. The dog sees the rabbit. The rabbit sees the bear. If something eats the dog and it is cold then the dog chases the rabbit. If something chases the bear then the bear chases the rabbit. If something sees the bear then it eats the dog. If something is cold and it chases the bear then the bear eats the dog. If the bear chases the rabbit then the rabbit is young. If the dog sees the rabbit then the dog chases the bear.
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
If something eats the dog and it is cold then the dog chases the rabbit.
((("something" "eats" "dog" "+") ("something" "is" "cold" "+")) -> ("dog" "chases" "rabbit" "+"))
If something chases the bear then the bear chases the rabbit.
((("something" "chases" "bear" "+")) -> ("bear" "chases" "rabbit" "+"))
If something sees the bear then it eats the dog.
((("something" "sees" "bear" "+")) -> ("something" "eats" "dog" "+"))
If something is cold and it chases the bear then the bear eats the dog.
((("something" "is" "cold" "+") ("something" "chases" "bear" "+")) -> ("bear" "eats" "dog" "+"))
If the bear chases the rabbit then the rabbit is young.
((("bear" "chases" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If the dog sees the rabbit then the dog chases the bear.
((("dog" "sees" "rabbit" "+")) -> ("dog" "chases" "bear" "+"))
The dog sees the rabbit.
True
1
proof
[(triple2)]
("dog" "sees" "rabbit" "+")
triple2
The dog does not see the rabbit.
False
1
inv-proof
[(triple2)]
("dog" "sees" "rabbit" "-")
triple2
The dog chases the bear.
True
2
proof
[(((triple2) -> rule6))]
("dog" "chases" "bear" "+")
((triple2) -> (rule6 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The rabbit does not eat the dog.
False
2
inv-proof
[(((triple3) -> rule3))]
("rabbit" "eats" "dog" "-")
((triple3) -> (rule3 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The bear chases the rabbit.
True
3
proof
[(((((triple2) -> rule6)) -> rule2))]
("bear" "chases" "rabbit" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The bear does not chase the rabbit.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("bear" "chases" "rabbit" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The bear does not eat the dog.
Unknown
inv-rconc
[@1: The bear eats the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "eats" "dog" "-")
The dog chases the rabbit.
Unknown
rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "rabbit" "+")
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "eats" "dog" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear sees the dog.[(triple1)] The dog sees the rabbit.[(triple2)] The rabbit sees the bear.[(triple3)] @1: The dog chases the bear.[(((triple2) -> rule6))] The rabbit eats the dog.[(((triple3) -> rule3))] @2: The bear chases the rabbit.[(((((triple2) -> rule6)) -> rule2))] @3: The rabbit is young.[(((((((triple2) -> rule6)) -> rule2)) -> rule5))]
The bear sees the dog.
("bear" "sees" "dog" "+")
triple1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple2
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple3
The dog chases the bear.
("dog" "chases" "bear" "+")
((triple2) -> (rule6 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
((triple3) -> (rule3 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int2
The dog chases the bear.
("dog" "chases" "bear" "+")
int3