Harry is round. If Harry is not cold then Harry is not furry. If something is round then it is young. If Harry is quiet and Harry is not young then Harry is big.
Harry is round.
("Harry" "is" "round" "+")
If Harry is not cold then Harry is not furry.
((("Harry" "is" "cold" "~")) -> ("Harry" "is" "furry" "-"))
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If Harry is quiet and Harry is not young then Harry is big.
((("Harry" "is" "quiet" "+") ("Harry" "is" "young" "~")) -> ("Harry" "is" "big" "+"))
Harry is round.
True
1
proof
[(triple1)]
("Harry" "is" "round" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple1)]
("Harry" "is" "round" "-")
triple1
Harry is young.
True
2
proof
[(((triple1) -> rule2))]
("Harry" "is" "young" "+")
((triple1) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple1) -> rule2))]
("Harry" "is" "young" "-")
((triple1) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Harry is round.[(triple1)] @1: Harry is young.[(((triple1) -> rule2))]
Harry is round.
("Harry" "is" "round" "+")
triple1
Harry is young.
("Harry" "is" "young" "+")
((triple1) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1