The dog is rough. If something is rough then it is green. Blue, red things are green. If something is blue and red then it is not green. If the dog is blue then the dog is not young. Rough, blue things are red. If the dog is not red then the dog is green.
The dog is rough.
("dog" "is" "rough" "+")
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Blue, red things are green.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is blue and red then it is not green.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "-"))
If the dog is blue then the dog is not young.
((("dog" "is" "blue" "+")) -> ("dog" "is" "young" "-"))
Rough, blue things are red.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If the dog is not red then the dog is green.
((("dog" "is" "red" "~")) -> ("dog" "is" "green" "+"))
The dog is rough.
True
1
proof
[(triple1)]
("dog" "is" "rough" "+")
triple1
The dog is not rough.
False
1
inv-proof
[(triple1)]
("dog" "is" "rough" "-")
triple1
The dog is not red.
Unknown
inv-rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "red" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The dog is rough.[(triple1)] @1: The dog is green.[(((triple1) -> rule1))]
The dog is rough.
("dog" "is" "rough" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
((triple1) -> (rule1 % int1))
The dog is green.
("dog" "is" "green" "+")
int1