Dave is blue. Dave is not young. Harry is blue. Harry is not kind. Harry is nice. Harry is not quiet. Harry is round. All young people are not cold. If someone is kind and not young then they are cold. If Dave is quiet and Dave is young then Dave is nice. If someone is nice and not cold then they are blue. Cold people are not round. All blue people are round.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not young.
("Dave" "is" "young" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is round.
("Harry" "is" "round" "+")
All young people are not cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "-"))
If someone is kind and not young then they are cold.
((("someone" "is" "kind" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "cold" "+"))
If Dave is quiet and Dave is young then Dave is nice.
((("Dave" "is" "quiet" "+") ("Dave" "is" "young" "+")) -> ("Dave" "is" "nice" "+"))
If someone is nice and not cold then they are blue.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "blue" "+"))
Cold people are not round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "-"))
All blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Dave is not young.
True
1
proof
[(triple2)]
("Dave" "is" "young" "-")
triple2
Harry is quiet.
False
1
inv-proof
[(triple6)]
("Harry" "is" "quiet" "+")
triple6
Dave is round.
True
2
proof
[(((triple1) -> rule6))]
("Dave" "is" "round" "+")
((triple1) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple1) -> rule6))]
("Dave" "is" "round" "-")
((triple1) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Dave is blue.[(triple1)] Dave is not young.[(triple2)] Harry is blue.[(triple3)] Harry is nice.[(triple5)] Harry is not kind.[(triple4)] Harry is not quiet.[(triple6)] Harry is round.[(triple7 OR ((triple3) -> rule6))] @1: Dave is round.[(((triple1) -> rule6))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is not young.
("Dave" "is" "young" "-")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is not kind.
("Harry" "is" "kind" "-")
triple4
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
((triple3) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1