The bear chases the squirrel. The dog eats the bear. The dog eats the squirrel. The dog does not see the mouse. The mouse chases the squirrel. The mouse eats the bear. The mouse does not eat the squirrel. The squirrel does not eat the dog. The squirrel is red. The squirrel is round. The squirrel sees the bear. The squirrel sees the mouse. If the bear is kind and the bear chases the mouse then the mouse chases the dog. If the mouse sees the squirrel and the squirrel does not eat the mouse then the squirrel eats the dog. If someone chases the squirrel then they see the dog. If someone sees the dog then they are red. If someone sees the mouse and the mouse is red then they eat the squirrel. If someone sees the dog and they are not red then they see the bear.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The dog eats the bear.
("dog" "eats" "bear" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse does not eat the squirrel.
("mouse" "eats" "squirrel" "-")
The squirrel does not eat the dog.
("squirrel" "eats" "dog" "-")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If the bear is kind and the bear chases the mouse then the mouse chases the dog.
((("bear" "is" "kind" "+") ("bear" "chases" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
If the mouse sees the squirrel and the squirrel does not eat the mouse then the squirrel eats the dog.
((("mouse" "sees" "squirrel" "+") ("squirrel" "eats" "mouse" "~")) -> ("squirrel" "eats" "dog" "+"))
If someone chases the squirrel then they see the dog.
((("someone" "chases" "squirrel" "+")) -> ("someone" "sees" "dog" "+"))
If someone sees the dog then they are red.
((("someone" "sees" "dog" "+")) -> ("someone" "is" "red" "+"))
If someone sees the mouse and the mouse is red then they eat the squirrel.
((("someone" "sees" "mouse" "+") ("mouse" "is" "red" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone sees the dog and they are not red then they see the bear.
((("someone" "sees" "dog" "+") ("someone" "is" "red" "~")) -> ("someone" "sees" "bear" "+"))
The dog does not see the mouse.
True
1
proof
[(triple4)]
("dog" "sees" "mouse" "-")
triple4
The mouse eats the squirrel.
False
1
inv-proof
[(triple7)]
("mouse" "eats" "squirrel" "+")
triple7
The bear sees the dog.
True
2
proof
[(((triple1) -> rule3))]
("bear" "sees" "dog" "+")
((triple1) -> (rule3 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
The bear does not see the dog.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "sees" "dog" "-")
((triple1) -> (rule3 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
The mouse is red.
True
3
proof
[(((((triple5) -> rule3)) -> rule4))]
("mouse" "is" "red" "+")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The bear is not red.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("bear" "is" "red" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
The squirrel eats the squirrel.
True
5
proof
[(((triple12 ((((triple5) -> rule3)) -> rule4)) -> rule5))]
("squirrel" "eats" "squirrel" "+")
((triple12 ((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The squirrel does not eat the squirrel.
False
5
inv-proof
[(((triple12 ((((triple5) -> rule3)) -> rule4)) -> rule5))]
("squirrel" "eats" "squirrel" "-")
((triple12 ((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The squirrel does not see the dog.
Unknown
inv-rconc
[@1: The squirrel sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "dog" "-")
The dog sees the bear.
Unknown
rconc
[@1: The dog sees the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "sees" "bear" "+")
The bear does not see the bear.
Unknown
inv-rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "sees" "bear" "-")
The bear eats the squirrel.
Unknown
rconc
[@1: The bear eats the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "squirrel" "+")
The bear does not see the squirrel.
Unknown
inv-random
[@0: The bear sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "squirrel" "-")
The dog chases the mouse.
Unknown
random
[@0: The dog chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "mouse" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The squirrel eats the mouse.
Unknown
random
[@0: The squirrel eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "mouse" "+")
@0: The bear chases the squirrel.[(triple1)] The dog does not see the mouse.[(triple4)] The dog eats the bear.[(triple2)] The dog eats the squirrel.[(triple3)] The mouse chases the squirrel.[(triple5)] The mouse does not eat the squirrel.[(triple7)] The mouse eats the bear.[(triple6)] The squirrel does not eat the dog.[(triple8)] The squirrel is red.[(triple9)] The squirrel is round.[(triple10)] The squirrel sees the bear.[(triple11)] The squirrel sees the mouse.[(triple12)] @1: The bear sees the dog.[(((triple1) -> rule3))] The mouse sees the dog.[(((triple5) -> rule3))] @2: The bear is red.[(((((triple1) -> rule3)) -> rule4))] The mouse is red.[(((((triple5) -> rule3)) -> rule4))] @3: The squirrel eats the squirrel.[(((triple12 ((((triple5) -> rule3)) -> rule4)) -> rule5))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
triple4
The dog eats the bear.
("dog" "eats" "bear" "+")
triple2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple3
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple5
The mouse does not eat the squirrel.
("mouse" "eats" "squirrel" "-")
triple7
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple6
The squirrel does not eat the dog.
("squirrel" "eats" "dog" "-")
triple8
The squirrel is red.
("squirrel" "is" "red" "+")
triple9
The squirrel is round.
("squirrel" "is" "round" "+")
triple10
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple11
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple12
The bear sees the dog.
("bear" "sees" "dog" "+")
((triple1) -> (rule3 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
((triple5) -> (rule3 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The bear is red.
("bear" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple12 ((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3