The bear is blue. The dog chases the bear. The dog chases the mouse. The dog eats the mouse. The mouse eats the dog. The mouse is blue. The mouse visits the bear. If someone is blue then they eat the bear. If someone visits the bear and the bear eats the mouse then the bear chases the mouse. If someone eats the bear then the bear eats the mouse.
The bear is blue.
("bear" "is" "blue" "+")
The dog chases the bear.
("dog" "chases" "bear" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If someone is blue then they eat the bear.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "bear" "+"))
If someone visits the bear and the bear eats the mouse then the bear chases the mouse.
((("someone" "visits" "bear" "+") ("bear" "eats" "mouse" "+")) -> ("bear" "chases" "mouse" "+"))
If someone eats the bear then the bear eats the mouse.
((("someone" "eats" "bear" "+")) -> ("bear" "eats" "mouse" "+"))
The dog chases the mouse.
True
1
proof
[(triple3)]
("dog" "chases" "mouse" "+")
triple3
The bear is not blue.
False
1
inv-proof
[(triple1)]
("bear" "is" "blue" "-")
triple1
The bear eats the bear.
True
2
proof
[(((triple1) -> rule1))]
("bear" "eats" "bear" "+")
((triple1) -> (rule1 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear does not eat the bear.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "eats" "bear" "-")
((triple1) -> (rule1 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear eats the mouse.
True
3
proof
[(((((triple1) -> rule1)) -> rule3) OR ((((triple6) -> rule1)) -> rule3))]
("bear" "eats" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int2
The bear does not eat the mouse.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3) OR ((((triple6) -> rule1)) -> rule3))]
("bear" "eats" "mouse" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int2
The bear chases the mouse.
True
5
proof
[(((triple7 ((((triple1) -> rule1)) -> rule3)) -> rule2) OR ((triple7 ((((triple6) -> rule1)) -> rule3)) -> rule2))]
("bear" "chases" "mouse" "+")
((triple7 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
((triple7 ((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int3
The bear does not chase the mouse.
False
5
inv-proof
[(((triple7 ((((triple1) -> rule1)) -> rule3)) -> rule2) OR ((triple7 ((((triple6) -> rule1)) -> rule3)) -> rule2))]
("bear" "chases" "mouse" "-")
((triple7 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
((triple7 ((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int3
The dog does not eat the bear.
Unknown
inv-rconc
[@1: The dog eats the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "bear" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The mouse visits the dog.
Unknown
random
[@0: The mouse visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "dog" "+")
@0: The bear is blue.[(triple1)] The dog chases the bear.[(triple2)] The dog chases the mouse.[(triple3)] The dog eats the mouse.[(triple4)] The mouse eats the dog.[(triple5)] The mouse is blue.[(triple6)] The mouse visits the bear.[(triple7)] @1: The bear eats the bear.[(((triple1) -> rule1))] The mouse eats the bear.[(((triple6) -> rule1))] @2: The bear eats the mouse.[(((((triple1) -> rule1)) -> rule3) OR ((((triple6) -> rule1)) -> rule3))] @3: The bear chases the mouse.[(((triple7 ((((triple1) -> rule1)) -> rule3)) -> rule2) OR ((triple7 ((((triple6) -> rule1)) -> rule3)) -> rule2))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The dog chases the bear.
("dog" "chases" "bear" "+")
triple2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple3
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple4
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple7
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple1) -> (rule1 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
((triple6) -> (rule1 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
((triple7 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
((triple7 ((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int3