Charlie is not cold. Dave is nice. Harry is cold. All white things are smart. If something is white and not cold then it is smart. If Harry is cold then Harry is not white. Red things are nice. Cold, big things are not white. If Harry is cold then Harry is nice. If something is nice and smart then it is not red. If Dave is red and Dave is not cold then Dave is smart.
Charlie is not cold.
("Charlie" "is" "cold" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All white things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If something is white and not cold then it is smart.
((("something" "is" "white" "+") ("something" "is" "cold" "~")) -> ("something" "is" "smart" "+"))
If Harry is cold then Harry is not white.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "white" "-"))
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Cold, big things are not white.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "-"))
If Harry is cold then Harry is nice.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "nice" "+"))
If something is nice and smart then it is not red.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "-"))
If Dave is red and Dave is not cold then Dave is smart.
((("Dave" "is" "red" "+") ("Dave" "is" "cold" "~")) -> ("Dave" "is" "smart" "+"))
Harry is cold.
True
1
proof
[(triple3)]
("Harry" "is" "cold" "+")
triple3
Charlie is cold.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Harry is not white.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "white" "-")
((triple3) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is not nice.
False
2
inv-proof
[(((triple3) -> rule6))]
("Harry" "is" "nice" "-")
((triple3) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Charlie is not cold.[(triple1)] Dave is nice.[(triple2)] Harry is cold.[(triple3)] @1: Harry is nice.[(((triple3) -> rule6))] Harry is not white.[(((triple3) -> rule3))]
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
((triple3) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1