The bear chases the squirrel. The bear is blue. The mouse chases the bear. The mouse is blue. The mouse visits the bear. The mouse visits the squirrel. The squirrel chases the bear. The squirrel is blue. The squirrel is not cold. The squirrel needs the mouse. The squirrel visits the bear. The squirrel visits the mouse. If someone needs the mouse then the mouse chases the bear. If someone is nice and cold then they need the squirrel. If someone needs the bear then the bear visits the mouse. If someone visits the mouse then they are not kind. If someone visits the bear then they chase the bear. If someone visits the squirrel then they are blue. If someone visits the squirrel then they need the bear. If someone is nice then they visit the squirrel.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear is blue.
("bear" "is" "blue" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is not cold.
("squirrel" "is" "cold" "-")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If someone needs the mouse then the mouse chases the bear.
((("someone" "needs" "mouse" "+")) -> ("mouse" "chases" "bear" "+"))
If someone is nice and cold then they need the squirrel.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone needs the bear then the bear visits the mouse.
((("someone" "needs" "bear" "+")) -> ("bear" "visits" "mouse" "+"))
If someone visits the mouse then they are not kind.
((("someone" "visits" "mouse" "+")) -> ("someone" "is" "kind" "-"))
If someone visits the bear then they chase the bear.
((("someone" "visits" "bear" "+")) -> ("someone" "chases" "bear" "+"))
If someone visits the squirrel then they are blue.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "blue" "+"))
If someone visits the squirrel then they need the bear.
((("someone" "visits" "squirrel" "+")) -> ("someone" "needs" "bear" "+"))
If someone is nice then they visit the squirrel.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "squirrel" "+"))
The mouse is blue.
True
1
proof
[(triple4 OR ((triple6) -> rule6))]
("mouse" "is" "blue" "+")
triple4
((triple6) -> (rule6 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The squirrel is not blue.
False
1
inv-proof
[(triple8)]
("squirrel" "is" "blue" "-")
triple8
The mouse needs the bear.
True
2
proof
[(((triple6) -> rule7))]
("mouse" "needs" "bear" "+")
((triple6) -> (rule7 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse does not need the bear.
False
2
inv-proof
[(((triple6) -> rule7))]
("mouse" "needs" "bear" "-")
((triple6) -> (rule7 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The bear visits the mouse.
True
3
proof
[(((((triple6) -> rule7)) -> rule3))]
("bear" "visits" "mouse" "+")
((((triple6) -> (rule7 % int2))) -> (rule3 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The bear does not visit the mouse.
False
3
inv-proof
[(((((triple6) -> rule7)) -> rule3))]
("bear" "visits" "mouse" "-")
((((triple6) -> (rule7 % int2))) -> (rule3 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The bear is not kind.
True
4
proof
[(((((((triple6) -> rule7)) -> rule3)) -> rule4))]
("bear" "is" "kind" "-")
((((((triple6) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear is not kind.
("bear" "is" "kind" "-")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The bear is kind.
False
4
inv-proof
[(((((((triple6) -> rule7)) -> rule3)) -> rule4))]
("bear" "is" "kind" "+")
((((((triple6) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear is not kind.
("bear" "is" "kind" "-")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The bear does not need the bear.
Unknown
inv-rconc
[@2: The bear needs the bear.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("bear" "needs" "bear" "-")
The bear visits the squirrel.
Unknown
rconc
[@1: The bear visits the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "visits" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "squirrel" "+")
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 squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
@0: The bear chases the squirrel.[(triple1)] The bear is blue.[(triple2)] The mouse chases the bear.[(triple3 OR ((triple10) -> rule1) OR ((triple5) -> rule5))] The mouse is blue.[(triple4 OR ((triple6) -> rule6))] The mouse visits the bear.[(triple5)] The mouse visits the squirrel.[(triple6)] The squirrel chases the bear.[(triple7 OR ((triple11) -> rule5))] The squirrel is blue.[(triple8)] The squirrel is not cold.[(triple9)] The squirrel needs the mouse.[(triple10)] The squirrel visits the bear.[(triple11)] The squirrel visits the mouse.[(triple12)] @1: The mouse needs the bear.[(((triple6) -> rule7))] The squirrel is not kind.[(((triple12) -> rule4))] @2: The bear visits the mouse.[(((((triple6) -> rule7)) -> rule3))] @3: The bear is not kind.[(((((((triple6) -> rule7)) -> rule3)) -> rule4))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple3
((triple10) -> (rule1 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
((triple5) -> (rule5 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
triple4
((triple6) -> (rule6 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple5
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple6
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple7
((triple11) -> (rule5 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple8
The squirrel is not cold.
("squirrel" "is" "cold" "-")
triple9
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple10
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple11
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple12
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple6) -> (rule7 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The squirrel is not kind.
("squirrel" "is" "kind" "-")
((triple12) -> (rule4 % int1))
The squirrel is not kind.
("squirrel" "is" "kind" "-")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
((((triple6) -> (rule7 % int2))) -> (rule3 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The bear is not kind.
("bear" "is" "kind" "-")
((((((triple6) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear is not kind.
("bear" "is" "kind" "-")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3