Erin is white. Gary is nice. Harry is white. If Harry is smart then Harry is quiet. Nice things are smart. Round, white things are quiet. Blue, nice things are quiet. Smart, quiet things are nice. If something is round then it is white.
Erin is white.
("Erin" "is" "white" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is smart then Harry is quiet.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "quiet" "+"))
Nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Round, white things are quiet.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Blue, nice things are quiet.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Smart, quiet things are nice.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If something is round then it is white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Erin is white.
True
1
proof
[(triple1)]
("Erin" "is" "white" "+")
triple1
Gary is not nice.
False
1
inv-proof
[(triple2)]
("Gary" "is" "nice" "-")
triple2
Gary is smart.
True
2
proof
[(((triple2) -> rule2))]
("Gary" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple2) -> rule2))]
("Gary" "is" "smart" "-")
((triple2) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is not nice.
Unknown
inv-rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Harry" "is" "nice" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "white" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Erin is white.[(triple1)] Gary is nice.[(triple2)] Harry is white.[(triple3)] @1: Gary is smart.[(((triple2) -> rule2))]
Erin is white.
("Erin" "is" "white" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1