Dave is quiet. Dave is round. Harry is green. If someone is kind then they are not nice. If Dave is round then Dave is kind. If someone is quiet and nice then they are not kind. All nice people are green. If someone is round and kind then they are green. All nice people are green. If Harry is green then Harry is nice. All kind people are furry.
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is green.
("Harry" "is" "green" "+")
If someone is kind then they are not nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "-"))
If Dave is round then Dave is kind.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "kind" "+"))
If someone is quiet and nice then they are not kind.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "-"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is round and kind then they are green.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Harry is green then Harry is nice.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "nice" "+"))
All kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Dave is quiet.
True
1
proof
[(triple1)]
("Dave" "is" "quiet" "+")
triple1
Harry is not green.
False
1
inv-proof
[(triple3)]
("Harry" "is" "green" "-")
triple3
Dave is kind.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple3) -> rule7))]
("Harry" "is" "nice" "-")
((triple3) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Dave is furry.
True
3
proof
[(((((triple2) -> rule2)) -> rule8))]
("Dave" "is" "furry" "+")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not green.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule5))]
("Dave" "is" "green" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is quiet.[(triple1)] Dave is round.[(triple2)] Harry is green.[(triple3)] @1: Dave is kind.[(((triple2) -> rule2))] Harry is nice.[(((triple3) -> rule7))] @2: Dave is furry.[(((((triple2) -> rule2)) -> rule8))] Dave is green.[(((triple2 ((triple2) -> rule2)) -> rule5))] Dave is not nice.[(((((triple2) -> rule2)) -> rule1))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple3) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2