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