Anne is nice. Charlie is furry. Harry is nice. If Anne is nice then Anne is kind. All nice people are cold. If someone is kind then they are cold. If Anne is kind then Anne is not furry. If Anne is nice then Anne is not green. If Charlie is young then Charlie is not nice. If someone is smart then they are not kind. If Charlie is green then Charlie is young.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If Anne is nice then Anne is kind.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "kind" "+"))
All nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If Anne is kind then Anne is not furry.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "furry" "-"))
If Anne is nice then Anne is not green.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "green" "-"))
If Charlie is young then Charlie is not nice.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "nice" "-"))
If someone is smart then they are not kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "-"))
If Charlie is green then Charlie is young.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "young" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Harry is not nice.
False
1
inv-proof
[(triple3)]
("Harry" "is" "nice" "-")
triple3
Harry is cold.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not furry.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "cold" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Anne is nice.[(triple1)] Charlie is furry.[(triple2)] Harry is nice.[(triple3)] @1: Anne is cold.[(((triple1) -> rule2) OR ((((triple1) -> rule1)) -> rule3))] Anne is kind.[(((triple1) -> rule1))] Anne is not green.[(((triple1) -> rule5))] Harry is cold.[(((triple3) -> rule2))] @2: Anne is not furry.[(((((triple1) -> rule1)) -> rule4))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not green.
("Anne" "is" "green" "-")
((triple1) -> (rule5 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is not furry.
("Anne" "is" "furry" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2