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