Anne is smart. Erin is nice. Erin is not round. Gary is cold. Gary is quiet. Harry is not rough. Harry is smart. If something is nice and not quiet then it is white. Round, smart things are not white. If something is rough and round then it is white. All cold things are not nice. If something is round and quiet then it is not nice. White things are round.
Anne is smart.
("Anne" "is" "smart" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not round.
("Erin" "is" "round" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is smart.
("Harry" "is" "smart" "+")
If something is nice and not quiet then it is white.
((("something" "is" "nice" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "white" "+"))
Round, smart things are not white.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "-"))
If something is rough and round then it is white.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All cold things are not nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "-"))
If something is round and quiet then it is not nice.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "-"))
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Erin is nice.
True
1
proof
[(triple2)]
("Erin" "is" "nice" "+")
triple2
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Gary is not nice.
True
2
proof
[(((triple4) -> rule4))]
("Gary" "is" "nice" "-")
((triple4) -> (rule4 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is nice.
False
2
inv-proof
[(((triple4) -> rule4))]
("Gary" "is" "nice" "+")
((triple4) -> (rule4 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "white" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is smart.[(triple1)] Erin is nice.[(triple2)] Erin is not round.[(triple3)] Gary is cold.[(triple4)] Gary is quiet.[(triple5)] Harry is not rough.[(triple6)] Harry is smart.[(triple7)] @1: Gary is not nice.[(((triple4) -> rule4))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Erin is not round.
("Erin" "is" "round" "-")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Harry is not rough.
("Harry" "is" "rough" "-")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Gary is not nice.
("Gary" "is" "nice" "-")
((triple4) -> (rule4 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1