Anne is cold. Dave is rough. Gary is cold. Harry is nice. Cold, rough things are big. All young things are red. If something is nice then it is cold. Big, green things are red. If Anne is young then Anne is big. If something is cold and red then it is big.
Anne is cold.
("Anne" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Cold, rough things are big.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Big, green things are red.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Anne is young then Anne is big.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "big" "+"))
If something is cold and red then it is big.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Harry is not nice.
False
1
inv-proof
[(triple4)]
("Harry" "is" "nice" "-")
triple4
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "red" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Dave is rough.[(triple2)] Gary is cold.[(triple3)] Harry is nice.[(triple4)] @1: Harry is cold.[(((triple4) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1