Anne is green. Dave is furry. Harry is nice. If Harry is white then Harry is furry. All cold things are furry. All cold, young things are kind. If something is cold and kind then it is white. All young things are green. If something is green then it is cold. If something is white and cold then it is kind. If something is furry then it is nice.
Anne is green.
("Anne" "is" "green" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If Harry is white then Harry is furry.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "furry" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
All cold, young things are kind.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is cold and kind then it is white.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
All young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is white and cold then it is kind.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is furry then it is nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Harry is nice.
True
1
proof
[(triple3)]
("Harry" "is" "nice" "+")
triple3
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Anne is cold.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple2) -> rule8))]
("Dave" "is" "nice" "-")
((triple2) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Anne is furry.
True
3
proof
[(((((triple1) -> rule6)) -> rule2))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
True
4
proof
[(((((((triple1) -> rule6)) -> rule2)) -> rule8))]
("Anne" "is" "nice" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not nice.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule2)) -> rule8))]
("Anne" "is" "nice" "-")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@3: Anne is kind.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule3 <- FAIL)]]
("Anne" "is" "kind" "-")
Harry is cold.
Unknown
rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Harry" "is" "cold" "+")
Dave is not kind.
Unknown
inv-rconc
[@3: Dave is kind.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule3 <- FAIL)]]
("Dave" "is" "kind" "-")
Harry is kind.
Unknown
rconc
[@3: Harry is kind.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule3 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is green.[(triple1)] Dave is furry.[(triple2)] Harry is nice.[(triple3)] @1: Anne is cold.[(((triple1) -> rule6))] Dave is nice.[(((triple2) -> rule8))] @2: Anne is furry.[(((((triple1) -> rule6)) -> rule2))] @3: Anne is nice.[(((((((triple1) -> rule6)) -> rule2)) -> rule8))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3