Charlie is furry. Charlie is kind. Charlie is quiet. Dave is furry. Dave is round. Dave is young. Harry is nice. Young people are quiet. If Dave is furry and Dave is quiet then Dave is kind. If Charlie is furry and Charlie is white then Charlie is nice. All furry, kind people are nice. If Charlie is young then Charlie is quiet. All kind, white people are furry.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is furry and Dave is quiet then Dave is kind.
((("Dave" "is" "furry" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "kind" "+"))
If Charlie is furry and Charlie is white then Charlie is nice.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "nice" "+"))
All furry, kind people are nice.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is young then Charlie is quiet.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "quiet" "+"))
All kind, white people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Dave is furry.
True
1
proof
[(triple4)]
("Dave" "is" "furry" "+")
triple4
Dave is not furry.
False
1
inv-proof
[(triple4)]
("Dave" "is" "furry" "-")
triple4
Charlie is nice.
True
3
proof
[(((triple1 triple2) -> rule4))]
("Charlie" "is" "nice" "+")
((triple1 triple2) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
3
inv-proof
[(((triple1 triple2) -> rule4))]
("Charlie" "is" "nice" "-")
((triple1 triple2) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is kind.
True
4
proof
[(((triple4 ((triple6) -> rule1)) -> rule2))]
("Dave" "is" "kind" "+")
((triple4 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not kind.
False
4
inv-proof
[(((triple4 ((triple6) -> rule1)) -> rule2))]
("Dave" "is" "kind" "-")
((triple4 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
True
6
proof
[(((triple4 ((triple4 ((triple6) -> rule1)) -> rule2)) -> rule4))]
("Dave" "is" "nice" "+")
((triple4 ((triple4 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not nice.
False
6
inv-proof
[(((triple4 ((triple4 ((triple6) -> rule1)) -> rule2)) -> rule4))]
("Dave" "is" "nice" "-")
((triple4 ((triple4 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is furry.
Unknown
rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "furry" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is furry.[(triple1)] Charlie is kind.[(triple2)] Charlie is quiet.[(triple3)] Dave is furry.[(triple4)] Dave is round.[(triple5)] Dave is young.[(triple6)] Harry is nice.[(triple7)] @1: Charlie is nice.[(((triple1 triple2) -> rule4))] Dave is quiet.[(((triple6) -> rule1))] @2: Dave is kind.[(((triple4 ((triple6) -> rule1)) -> rule2))] @3: Dave is nice.[(((triple4 ((triple4 ((triple6) -> rule1)) -> rule2)) -> rule4))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1 triple2) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple6) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple4 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple4 ((triple4 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3