Anne is quiet. Charlie is big. Harry is kind. White things are furry. If Harry is kind then Harry is white. If something is white then it is not quiet. If something is furry and kind then it is big. If something is kind and not furry then it is young. If Harry is not young then Harry is quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
White things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If Harry is kind then Harry is white.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "white" "+"))
If something is white then it is not quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "-"))
If something is furry and kind then it is big.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is kind and not furry then it is young.
((("something" "is" "kind" "+") ("something" "is" "furry" "~")) -> ("something" "is" "young" "+"))
If Harry is not young then Harry is quiet.
((("Harry" "is" "young" "~")) -> ("Harry" "is" "quiet" "+"))
Harry is kind.
True
1
proof
[(triple3)]
("Harry" "is" "kind" "+")
triple3
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Harry is white.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "white" "+")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "white" "-")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not quiet.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Harry" "is" "quiet" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Harry" "is" "quiet" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is big.
True
5
proof
[(((((((triple3) -> rule2)) -> rule1) triple3) -> rule4))]
("Harry" "is" "big" "+")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not big.
False
5
inv-proof
[(((((((triple3) -> rule2)) -> rule1) triple3) -> rule4))]
("Harry" "is" "big" "-")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "young" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "big" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "furry" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is quiet.[(triple1)] Charlie is big.[(triple2)] Harry is kind.[(triple3)] @1: Harry is white.[(((triple3) -> rule2))] @2: Harry is furry.[(((((triple3) -> rule2)) -> rule1))] Harry is not quiet.[(((((triple3) -> rule2)) -> rule3))] @3: Harry is big.[(((((((triple3) -> rule2)) -> rule1) triple3) -> rule4))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3