The mouse is not kind. If the mouse is green and the mouse is nice then the mouse is not cold. Green things are big. Kind things are big. If something is green and cold then it is kind. Green things are cold. If something is green then it is not cold. If something is nice then it is cold. Kind things are green.
The mouse is not kind.
("mouse" "is" "kind" "-")
If the mouse is green and the mouse is nice then the mouse is not cold.
((("mouse" "is" "green" "+") ("mouse" "is" "nice" "+")) -> ("mouse" "is" "cold" "-"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
Kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is green and cold then it is kind.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is not cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "-"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
The mouse is not kind.
True
1
proof
[(triple1)]
("mouse" "is" "kind" "-")
triple1
The mouse is kind.
False
1
inv-proof
[(triple1)]
("mouse" "is" "kind" "+")
triple1
The mouse is not big.
Unknown
inv-rconc
[@2: The mouse is big.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("mouse" "is" "big" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The mouse is not kind.[(triple1)]
The mouse is not kind.
("mouse" "is" "kind" "-")
triple1