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