Anne is blue. Anne is rough. Charlie is red. Dave is not blue. Dave is not smart. Harry is green. Harry is rough. Red, blue things are not rough. If something is red and not green then it is rough. Smart things are not round. If something is round and not blue then it is smart. All round things are red. All round, smart things are cold. If something is blue then it is not cold. If something is green and not rough then it is cold.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is not smart.
("Dave" "is" "smart" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Red, blue things are not rough.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "-"))
If something is red and not green then it is rough.
((("something" "is" "red" "+") ("something" "is" "green" "~")) -> ("something" "is" "rough" "+"))
Smart things are not round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "-"))
If something is round and not blue then it is smart.
((("something" "is" "round" "+") ("something" "is" "blue" "~")) -> ("something" "is" "smart" "+"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All round, smart things are cold.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If something is blue then it is not cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "-"))
If something is green and not rough then it is cold.
((("something" "is" "green" "+") ("something" "is" "rough" "~")) -> ("something" "is" "cold" "+"))
Harry is rough.
True
1
proof
[(triple7)]
("Harry" "is" "rough" "+")
triple7
Harry is not rough.
False
1
inv-proof
[(triple7)]
("Harry" "is" "rough" "-")
triple7
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "red" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is blue.[(triple1)] Anne is rough.[(triple2)] Charlie is red.[(triple3)] Dave is not blue.[(triple4)] Dave is not smart.[(triple5)] Harry is green.[(triple6)] Harry is rough.[(triple7)] @1: Anne is not cold.[(((triple1) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Dave is not blue.
("Dave" "is" "blue" "-")
triple4
Dave is not smart.
("Dave" "is" "smart" "-")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Anne is not cold.
("Anne" "is" "cold" "-")
((triple1) -> (rule7 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1