Anne is furry. Charlie is blue. Erin is nice. Harry is nice. If something is kind and not rough then it is blue. If Charlie is big then Charlie is nice. All rough things are young. If something is nice and not blue then it is young. Furry things are young. If something is young and not kind then it is not big.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is kind and not rough then it is blue.
((("something" "is" "kind" "+") ("something" "is" "rough" "~")) -> ("something" "is" "blue" "+"))
If Charlie is big then Charlie is nice.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "nice" "+"))
All rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is nice and not blue then it is young.
((("something" "is" "nice" "+") ("something" "is" "blue" "~")) -> ("something" "is" "young" "+"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is young and not kind then it is not big.
((("something" "is" "young" "+") ("something" "is" "kind" "~")) -> ("something" "is" "big" "-"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Erin is not nice.
False
1
inv-proof
[(triple3)]
("Erin" "is" "nice" "-")
triple3
Anne is young.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "young" "+")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "young" "-")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "young" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "blue" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is furry.[(triple1)] Charlie is blue.[(triple2)] Erin is nice.[(triple3)] Harry is nice.[(triple4)] @1: Anne is young.[(((triple1) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1