The bear needs the squirrel. The bear sees the squirrel. The bear visits the squirrel. The squirrel is cold. The squirrel is green. The squirrel sees the bear. The squirrel visits the bear. If the squirrel visits the bear and the squirrel is not nice then the squirrel does not need the bear. If something is kind and it needs the bear then the bear needs the squirrel. If something sees the squirrel and the squirrel needs the bear then it is cold. If something needs the bear and it is nice then it is not kind. All blue things are kind. If something is kind then it sees the bear.
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If the squirrel visits the bear and the squirrel is not nice then the squirrel does not need the bear.
((("squirrel" "visits" "bear" "+") ("squirrel" "is" "nice" "~")) -> ("squirrel" "needs" "bear" "-"))
If something is kind and it needs the bear then the bear needs the squirrel.
((("something" "is" "kind" "+") ("something" "needs" "bear" "+")) -> ("bear" "needs" "squirrel" "+"))
If something sees the squirrel and the squirrel needs the bear then it is cold.
((("something" "sees" "squirrel" "+") ("squirrel" "needs" "bear" "+")) -> ("something" "is" "cold" "+"))
If something needs the bear and it is nice then it is not kind.
((("something" "needs" "bear" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "-"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it sees the bear.
((("something" "is" "kind" "+")) -> ("something" "sees" "bear" "+"))
The bear needs the squirrel.
True
1
proof
[(triple1)]
("bear" "needs" "squirrel" "+")
triple1
The squirrel is not green.
False
1
inv-proof
[(triple5)]
("squirrel" "is" "green" "-")
triple5
The bear does not see the bear.
Unknown
inv-rconc
[@2: The bear sees the bear.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("bear" "sees" "bear" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
@0: The bear needs the squirrel.[(triple1)] The bear sees the squirrel.[(triple2)] The bear visits the squirrel.[(triple3)] The squirrel is cold.[(triple4)] The squirrel is green.[(triple5)] The squirrel sees the bear.[(triple6)] The squirrel visits the bear.[(triple7)]
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple4
The squirrel is green.
("squirrel" "is" "green" "+")
triple5
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple6
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple7