Erin is furry. Gary is round. Harry is blue. All blue things are smart. If Harry is blue and Harry is cold then Harry is furry. Furry things are not white. Smart things are white. If something is cold and not smart then it is not furry. If something is furry and not white then it is rough.
Erin is furry.
("Erin" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If Harry is blue and Harry is cold then Harry is furry.
((("Harry" "is" "blue" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "furry" "+"))
Furry things are not white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "-"))
Smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is cold and not smart then it is not furry.
((("something" "is" "cold" "+") ("something" "is" "smart" "~")) -> ("something" "is" "furry" "-"))
If something is furry and not white then it is rough.
((("something" "is" "furry" "+") ("something" "is" "white" "~")) -> ("something" "is" "rough" "+"))
Erin is furry.
True
1
proof
[(triple1)]
("Erin" "is" "furry" "+")
triple1
Harry is not blue.
False
1
inv-proof
[(triple3)]
("Harry" "is" "blue" "-")
triple3
Erin is not white.
True
2
proof
[(((triple1) -> rule3))]
("Erin" "is" "white" "-")
((triple1) -> (rule3 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Harry is not smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Gary is not white.
Unknown
inv-rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Erin is furry.[(triple1)] Gary is round.[(triple2)] Harry is blue.[(triple3)] @1: Erin is not white.[(((triple1) -> rule3))] Harry is smart.[(((triple3) -> rule1))] @2: Erin is rough.[(((triple1 ((triple1) -> rule3)) -> rule6))] Harry is white.[(((((triple3) -> rule1)) -> rule4))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
Gary is round.
("Gary" "is" "round" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Erin is not white.
("Erin" "is" "white" "-")
((triple1) -> (rule3 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not white.
("Erin" "is" "white" "-")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2