Anne is kind. Dave is kind. Harry is nice. If Dave is big then Dave is not young. Kind people are not green. If someone is nice then they are green. Cold, quiet people are kind. If someone is big then they are not kind. If Harry is green and Harry is nice then Harry is cold. Young people are not big. If Harry is nice and Harry is quiet then Harry is green.
Anne is kind.
("Anne" "is" "kind" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If Dave is big then Dave is not young.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "young" "-"))
Kind people are not green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "-"))
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Cold, quiet people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is big then they are not kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "-"))
If Harry is green and Harry is nice then Harry is cold.
((("Harry" "is" "green" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "cold" "+"))
Young people are not big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "-"))
If Harry is nice and Harry is quiet then Harry is green.
((("Harry" "is" "nice" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "green" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Dave is not green.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "green" "-")
((triple2) -> (rule2 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Harry is not green.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "green" "-")
((triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule6))]
("Harry" "is" "cold" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not cold.
False
4
inv-proof
[(((((triple3) -> rule3) triple3) -> rule6))]
("Harry" "is" "cold" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is kind.[(triple1)] Dave is kind.[(triple2)] Harry is nice.[(triple3)] @1: Anne is not green.[(((triple1) -> rule2))] Dave is not green.[(((triple2) -> rule2))] Harry is green.[(((triple3) -> rule3))] @2: Harry is cold.[(((((triple3) -> rule3) triple3) -> rule6))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Anne is not green.
("Anne" "is" "green" "-")
((triple1) -> (rule2 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Dave is not green.
("Dave" "is" "green" "-")
((triple2) -> (rule2 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2