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