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