The mouse is red. All young things are big. If the mouse is red and the mouse is rough then the mouse is young. All young, rough things are red. If something is big and rough then it is red. If something is nice and red then it is rough. All nice, young things are big.
The mouse is red.
("mouse" "is" "red" "+")
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If the mouse is red and the mouse is rough then the mouse is young.
((("mouse" "is" "red" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "is" "young" "+"))
All young, rough things are red.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is big and rough then it is red.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is nice and red then it is rough.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All nice, young things are big.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
The mouse is red.
True
1
proof
[(triple1)]
("mouse" "is" "red" "+")
triple1
The mouse is not red.
False
1
inv-proof
[(triple1)]
("mouse" "is" "red" "-")
triple1
The mouse is not big.
Unknown
inv-rconc
[@3: The mouse is big.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule5 <- FAIL)]]
("mouse" "is" "big" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The mouse is red.[(triple1)]
The mouse is red.
("mouse" "is" "red" "+")
triple1