Charlie is round. Dave is red. Gary is smart. Harry is round. Smart things are red. If something is rough and kind then it is round. Kind, young things are cold. All young, cold things are smart. Kind things are cold. If something is round and cold then it is smart. If Gary is round and Gary is kind then Gary is cold. All cold things are red.
Charlie is round.
("Charlie" "is" "round" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is round.
("Harry" "is" "round" "+")
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is rough and kind then it is round.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Kind, young things are cold.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All young, cold things are smart.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is round and cold then it is smart.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If Gary is round and Gary is kind then Gary is cold.
((("Gary" "is" "round" "+") ("Gary" "is" "kind" "+")) -> ("Gary" "is" "cold" "+"))
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Gary is smart.
True
1
proof
[(triple3)]
("Gary" "is" "smart" "+")
triple3
Gary is not smart.
False
1
inv-proof
[(triple3)]
("Gary" "is" "smart" "-")
triple3
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "cold" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Charlie is round.[(triple1)] Dave is red.[(triple2)] Gary is smart.[(triple3)] Harry is round.[(triple4)] @1: Gary is red.[(((triple3) -> rule1))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1