Anne is blue. Anne is furry. Dave is blue. Dave is quiet. Harry is furry. Harry is round. Harry is not young. If someone is blue then they are quiet. If someone is red and quiet then they are blue. If someone is quiet and red then they are blue. If someone is red and not furry then they are not round. Blue people are young. If someone is quiet and not furry then they are not red. All round, blue people are red. All young, furry people are nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is not young.
("Harry" "is" "young" "-")
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is red and quiet then they are blue.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet and red then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is red and not furry then they are not round.
((("someone" "is" "red" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "round" "-"))
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet and not furry then they are not red.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "red" "-"))
All round, blue people are red.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
All young, furry people are nice.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Dave is blue.
True
1
proof
[(triple3)]
("Dave" "is" "blue" "+")
triple3
Dave is not blue.
False
1
inv-proof
[(triple3)]
("Dave" "is" "blue" "-")
triple3
Dave is young.
True
2
proof
[(((triple3) -> rule5))]
("Dave" "is" "young" "+")
((triple3) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple3) -> rule5))]
("Dave" "is" "young" "-")
((triple3) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Anne is nice.
True
4
proof
[(((((triple1) -> rule5) triple2) -> rule8))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule5 % int2)) triple2) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not nice.
False
4
inv-proof
[(((((triple1) -> rule5) triple2) -> rule8))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule5 % int2)) triple2) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Harry is not quiet.
Unknown
inv-rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "red" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Dave is blue.[(triple3)] Dave is quiet.[(triple4 OR ((triple3) -> rule1))] Harry is furry.[(triple5)] Harry is not young.[(triple7)] Harry is round.[(triple6)] @1: Anne is quiet.[(((triple1) -> rule1))] Anne is young.[(((triple1) -> rule5))] Dave is young.[(((triple3) -> rule5))] @2: Anne is nice.[(((((triple1) -> rule5) triple2) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
((triple3) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple5
Harry is not young.
("Harry" "is" "young" "-")
triple7
Harry is round.
("Harry" "is" "round" "+")
triple6
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule5 % int2)) triple2) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2