Anne is kind. Dave is kind. Gary is nice. If something is kind and nice then it is blue. All quiet things are blue. If Anne is kind then Anne is quiet. If something is round and kind then it is blue. Blue things are round. If something is quiet and red then it is blue. If Gary is red then Gary is round. If something is red and kind then it is round.
Anne is kind.
("Anne" "is" "kind" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
If something is kind and nice then it is blue.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Anne is kind then Anne is quiet.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "quiet" "+"))
If something is round and kind then it is blue.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is quiet and red then it is blue.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If Gary is red then Gary is round.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "round" "+"))
If something is red and kind then it is round.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Anne is quiet.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is round.
True
4
proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("Anne" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not round.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("Anne" "is" "round" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Dave is not blue.
Unknown
inv-rconc
[@3: Dave is blue.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule1 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is round.
Unknown
rconc
[@3: Dave is round.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule8 <- FAIL)]]
("Dave" "is" "round" "+")
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is round.
Unknown
rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is kind.[(triple1)] Dave is kind.[(triple2)] Gary is nice.[(triple3)] @1: Anne is quiet.[(((triple1) -> rule3))] @2: Anne is blue.[(((((triple1) -> rule3)) -> rule2))] @3: Anne is round.[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3