Anne is kind. Anne is quiet. Anne is white. Dave is nice. Erin is young. Harry is cold. Harry is white. All furry things are white. If Erin is nice then Erin is cold. If something is young then it is furry. If Erin is white and Erin is kind then Erin is quiet. Quiet things are cold. If something is quiet and not white then it is cold.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is white.
("Harry" "is" "white" "+")
All furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If Erin is nice then Erin is cold.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "cold" "+"))
If something is young then it is furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If Erin is white and Erin is kind then Erin is quiet.
((("Erin" "is" "white" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "quiet" "+"))
Quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is quiet and not white then it is cold.
((("something" "is" "quiet" "+") ("something" "is" "white" "~")) -> ("something" "is" "cold" "+"))
Harry is cold.
True
1
proof
[(triple6)]
("Harry" "is" "cold" "+")
triple6
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Erin is furry.
True
2
proof
[(((triple5) -> rule3))]
("Erin" "is" "furry" "+")
((triple5) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple5) -> rule3))]
("Erin" "is" "furry" "-")
((triple5) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
True
3
proof
[(((((triple5) -> rule3)) -> rule1))]
("Erin" "is" "white" "+")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule1))]
("Erin" "is" "white" "-")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is white.
Unknown
rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "white" "+")
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "quiet" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is kind.[(triple1)] Anne is quiet.[(triple2)] Anne is white.[(triple3)] Dave is nice.[(triple4)] Erin is young.[(triple5)] Harry is cold.[(triple6)] Harry is white.[(triple7)] @1: Anne is cold.[(((triple2) -> rule5))] Erin is furry.[(((triple5) -> rule3))] @2: Erin is white.[(((((triple5) -> rule3)) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Anne is cold.
("Anne" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple5) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2