Anne is blue. Anne is furry. Anne is quiet. Anne is smart. Dave is furry. Dave is kind. Dave is smart. Dave is white. Erin is blue. Erin is smart. All quiet people are kind. Kind, blue people are white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is smart.
("Erin" "is" "smart" "+")
All quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Kind, blue people are white.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Anne is quiet.
True
1
proof
[(triple3)]
("Anne" "is" "quiet" "+")
triple3
Dave is not white.
False
1
inv-proof
[(triple8)]
("Dave" "is" "white" "-")
triple8
Anne is kind.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "kind" "-")
((triple3) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
True
4
proof
[(((((triple3) -> rule1) triple1) -> rule2))]
("Anne" "is" "white" "+")
((((triple3) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not white.
False
4
inv-proof
[(((((triple3) -> rule1) triple1) -> rule2))]
("Anne" "is" "white" "-")
((((triple3) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Erin is not white.
Unknown
inv-rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "kind" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is quiet.[(triple3)] Anne is smart.[(triple4)] Dave is furry.[(triple5)] Dave is kind.[(triple6)] Dave is smart.[(triple7)] Dave is white.[(triple8)] Erin is blue.[(triple9)] Erin is smart.[(triple10)] @1: Anne is kind.[(((triple3) -> rule1))] @2: Anne is white.[(((((triple3) -> rule1) triple1) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
Erin is blue.
("Erin" "is" "blue" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Anne is kind.
("Anne" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple3) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2