Anne is furry. Erin is quiet. Gary is quiet. Harry is furry. All furry things are smart. If Anne is white and Anne is quiet then Anne is rough. All furry, smart things are kind.
Anne is furry.
("Anne" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Anne is white and Anne is quiet then Anne is rough.
((("Anne" "is" "white" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "rough" "+"))
All furry, smart things are kind.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Harry is furry.
True
1
proof
[(triple4)]
("Harry" "is" "furry" "+")
triple4
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Harry is smart.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "kind" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is furry.[(triple1)] Erin is quiet.[(triple2)] Gary is quiet.[(triple3)] Harry is furry.[(triple4)] @1: Anne is smart.[(((triple1) -> rule1))] Harry is smart.[(((triple4) -> rule1))] @2: Anne is kind.[(((triple1 ((triple1) -> rule1)) -> rule3))] Harry is kind.[(((triple4 ((triple4) -> rule1)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2