Anne is smart. Bob is young. Dave is quiet. Harry is kind. All blue people are nice. If Anne is kind and Anne is nice then Anne is blue. Quiet, furry people are kind. If Harry is kind then Harry is blue. All smart, nice people are quiet. Nice people are young. Nice, furry people are quiet. If someone is nice then they are furry.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Anne is kind and Anne is nice then Anne is blue.
((("Anne" "is" "kind" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "blue" "+"))
Quiet, furry people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If Harry is kind then Harry is blue.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "blue" "+"))
All smart, nice people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Nice, furry people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is nice then they are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Harry is not kind.
False
1
inv-proof
[(triple4)]
("Harry" "is" "kind" "-")
triple4
Harry is blue.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple4) -> rule4))]
("Harry" "is" "blue" "-")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
True
3
proof
[(((((triple4) -> rule4)) -> rule1))]
("Harry" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule1))]
("Harry" "is" "nice" "-")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Dave is kind.
Unknown
rconc
[@3: Dave is kind.[CWA. Example of deepest failure = (rule3 <- rule8 <- rule1 <- FAIL)]]
("Dave" "is" "kind" "+")
Anne is not young.
Unknown
inv-rconc
[@3: Anne is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule2 <- FAIL)]]
("Anne" "is" "young" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is smart.[(triple1)] Bob is young.[(triple2)] Dave is quiet.[(triple3)] Harry is kind.[(triple4)] @1: Harry is blue.[(((triple4) -> rule4))] @2: Harry is nice.[(((((triple4) -> rule4)) -> rule1))] @3: Harry is furry.[(((((((triple4) -> rule4)) -> rule1)) -> rule8))] Harry is young.[(((((((triple4) -> rule4)) -> rule1)) -> rule6))] @4: Harry is quiet.[(((((((triple4) -> rule4)) -> rule1) ((((((triple4) -> rule4)) -> rule1)) -> rule8)) -> rule7))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((triple4) -> (rule4 % int4))) -> (rule1 % int3)) ((((((triple4) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4