Charlie is not smart. Gary is round. Harry is smart. If something is smart then it is blue. Young things are not blue. If Harry is not smart then Harry is not cold. If something is round and cold then it is nice. If something is big and not blue then it is nice. Nice things are cold.
Charlie is not smart.
("Charlie" "is" "smart" "-")
Gary is round.
("Gary" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is smart then it is blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Young things are not blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "-"))
If Harry is not smart then Harry is not cold.
((("Harry" "is" "smart" "~")) -> ("Harry" "is" "cold" "-"))
If something is round and cold then it is nice.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is big and not blue then it is nice.
((("something" "is" "big" "+") ("something" "is" "blue" "~")) -> ("something" "is" "nice" "+"))
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Harry is smart.
True
1
proof
[(triple3)]
("Harry" "is" "smart" "+")
triple3
Charlie is smart.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "smart" "+")
triple1
Harry is blue.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Harry" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is not smart.[(triple1)] Gary is round.[(triple2)] Harry is smart.[(triple3)] @1: Harry is blue.[(((triple3) -> rule1))]
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple1
Gary is round.
("Gary" "is" "round" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1