Anne is round. Dave is red. Dave is rough. Dave is round. Gary is green. Gary is rough. Harry is rough. If something is nice and green then it is round. If Anne is green then Anne is cold. If Harry is green and Harry is red then Harry is nice. If something is red and young then it is green. All red things are young. All cold things are red.
Anne is round.
("Anne" "is" "round" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If something is nice and green then it is round.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If Anne is green then Anne is cold.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "cold" "+"))
If Harry is green and Harry is red then Harry is nice.
((("Harry" "is" "green" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "nice" "+"))
If something is red and young then it is green.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Harry is rough.
True
1
proof
[(triple7)]
("Harry" "is" "rough" "+")
triple7
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is round.[(triple1)] Dave is red.[(triple2)] Dave is rough.[(triple3)] Dave is round.[(triple4)] Gary is green.[(triple5)] Gary is rough.[(triple6)] Harry is rough.[(triple7)] @1: Dave is young.[(((triple2) -> rule5))] @2: Dave is green.[(((triple2 ((triple2) -> rule5)) -> rule4))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2