Anne is not nice. Anne is not red. Charlie is quiet. Charlie is not red. Harry is blue. Harry is red. Harry is not rough. All red, nice people are quiet. If Anne is blue and Anne is not furry then Anne is rough. If someone is blue then they are nice. If someone is kind and not nice then they are rough. If someone is rough and not quiet then they are kind. Quiet people are not kind.
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is not red.
("Anne" "is" "red" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
All red, nice people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is blue and Anne is not furry then Anne is rough.
((("Anne" "is" "blue" "+") ("Anne" "is" "furry" "~")) -> ("Anne" "is" "rough" "+"))
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind and not nice then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "rough" "+"))
If someone is rough and not quiet then they are kind.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "kind" "+"))
Quiet people are not kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "-"))
Charlie is not red.
True
1
proof
[(triple4)]
("Charlie" "is" "red" "-")
triple4
Anne is nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Harry is nice.
True
2
proof
[(((triple5) -> rule3))]
("Harry" "is" "nice" "+")
((triple5) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Charlie is kind.
False
2
inv-proof
[(((triple3) -> rule6))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Harry is quiet.
True
4
proof
[(((triple6 ((triple5) -> rule3)) -> rule1))]
("Harry" "is" "quiet" "+")
((triple6 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not quiet.
False
4
inv-proof
[(((triple6 ((triple5) -> rule3)) -> rule1))]
("Harry" "is" "quiet" "-")
((triple6 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not kind.
True
5
proof
[(((((triple6 ((triple5) -> rule3)) -> rule1)) -> rule6))]
("Harry" "is" "kind" "-")
((((triple6 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is kind.
False
5
inv-proof
[(((((triple6 ((triple5) -> rule3)) -> rule1)) -> rule6))]
("Harry" "is" "kind" "+")
((((triple6 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "nice" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "kind" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is not nice.[(triple1)] Anne is not red.[(triple2)] Charlie is not red.[(triple4)] Charlie is quiet.[(triple3)] Harry is blue.[(triple5)] Harry is not rough.[(triple7)] Harry is red.[(triple6)] @1: Charlie is not kind.[(((triple3) -> rule6))] Harry is nice.[(((triple5) -> rule3))] @2: Harry is quiet.[(((triple6 ((triple5) -> rule3)) -> rule1))] @3: Harry is not kind.[(((((triple6 ((triple5) -> rule3)) -> rule1)) -> rule6))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Anne is not red.
("Anne" "is" "red" "-")
triple2
Charlie is not red.
("Charlie" "is" "red" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is not rough.
("Harry" "is" "rough" "-")
triple7
Harry is red.
("Harry" "is" "red" "+")
triple6
Charlie is not kind.
("Charlie" "is" "kind" "-")
((triple3) -> (rule6 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple5) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple6 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not kind.
("Harry" "is" "kind" "-")
((((triple6 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3