The bear chases the mouse. The bear is kind. The bear is red. The bear sees the mouse. The bear sees the squirrel. The bear visits the squirrel. The mouse chases the bear. The mouse chases the squirrel. The mouse is blue. The mouse is kind. The mouse is rough. The mouse sees the bear. The mouse sees the squirrel. The mouse visits the squirrel. The squirrel chases the bear. The squirrel is kind. If something visits the bear then it sees the mouse. If something visits the mouse then the mouse sees the bear. If something chases the bear and the bear visits the mouse then the bear sees the squirrel. If something is red then it chases the squirrel. If something visits the squirrel and the squirrel sees the mouse then the mouse visits the squirrel. If something visits the squirrel then the squirrel is red.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is red.
("bear" "is" "red" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If something visits the bear then it sees the mouse.
((("something" "visits" "bear" "+")) -> ("something" "sees" "mouse" "+"))
If something visits the mouse then the mouse sees the bear.
((("something" "visits" "mouse" "+")) -> ("mouse" "sees" "bear" "+"))
If something chases the bear and the bear visits the mouse then the bear sees the squirrel.
((("something" "chases" "bear" "+") ("bear" "visits" "mouse" "+")) -> ("bear" "sees" "squirrel" "+"))
If something is red then it chases the squirrel.
((("something" "is" "red" "+")) -> ("something" "chases" "squirrel" "+"))
If something visits the squirrel and the squirrel sees the mouse then the mouse visits the squirrel.
((("something" "visits" "squirrel" "+") ("squirrel" "sees" "mouse" "+")) -> ("mouse" "visits" "squirrel" "+"))
If something visits the squirrel then the squirrel is red.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
The mouse is blue.
True
1
proof
[(triple9)]
("mouse" "is" "blue" "+")
triple9
The bear does not see the mouse.
False
1
inv-proof
[(triple4)]
("bear" "sees" "mouse" "-")
triple4
The squirrel is red.
True
2
proof
[(((triple14) -> rule6) OR ((triple6) -> rule6))]
("squirrel" "is" "red" "+")
((triple14) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
((triple6) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is not red.
False
2
inv-proof
[(((triple14) -> rule6) OR ((triple6) -> rule6))]
("squirrel" "is" "red" "-")
((triple14) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
((triple6) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel chases the squirrel.
True
3
proof
[(((((triple14) -> rule6)) -> rule4) OR ((((triple6) -> rule6)) -> rule4))]
("squirrel" "chases" "squirrel" "+")
((((triple14) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel does not chase the squirrel.
False
3
inv-proof
[(((((triple14) -> rule6)) -> rule4) OR ((((triple6) -> rule6)) -> rule4))]
("squirrel" "chases" "squirrel" "-")
((((triple14) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel does not see the mouse.
Unknown
inv-rconc
[@1: The squirrel sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "mouse" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The bear chases the mouse.[(triple1)] The bear is kind.[(triple2)] The bear is red.[(triple3)] The bear sees the mouse.[(triple4)] The bear sees the squirrel.[(triple5)] The bear visits the squirrel.[(triple6)] The mouse chases the bear.[(triple7)] The mouse chases the squirrel.[(triple8)] The mouse is blue.[(triple9)] The mouse is kind.[(triple10)] The mouse is rough.[(triple11)] The mouse sees the bear.[(triple12)] The mouse sees the squirrel.[(triple13)] The mouse visits the squirrel.[(triple14)] The squirrel chases the bear.[(triple15)] The squirrel is kind.[(triple16)] @1: The bear chases the squirrel.[(((triple3) -> rule4))] The squirrel is red.[(((triple14) -> rule6) OR ((triple6) -> rule6))] @2: The squirrel chases the squirrel.[(((((triple14) -> rule6)) -> rule4) OR ((((triple6) -> rule6)) -> rule4))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple4
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple5
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple6
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple7
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple8
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
The mouse is kind.
("mouse" "is" "kind" "+")
triple10
The mouse is rough.
("mouse" "is" "rough" "+")
triple11
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple12
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple13
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple14
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple15
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple16
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
((triple3) -> (rule4 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((triple14) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
((triple6) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((((triple14) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2