Gary is furry. Harry is round. If something is furry then it is not quiet. If something is round then it is furry. All kind things are not big. If Harry is big then Harry is not round. Quiet things are not kind. If something is round and kind then it is rough. If something is big and not kind then it is cold. All round, big things are not cold.
Gary is furry.
("Gary" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is furry then it is not quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "-"))
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All kind things are not big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "-"))
If Harry is big then Harry is not round.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "round" "-"))
Quiet things are not kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "-"))
If something is round and kind then it is rough.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is big and not kind then it is cold.
((("something" "is" "big" "+") ("something" "is" "kind" "~")) -> ("something" "is" "cold" "+"))
All round, big things are not cold.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "-"))
Gary is furry.
True
1
proof
[(triple1)]
("Gary" "is" "furry" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple2)]
("Harry" "is" "round" "-")
triple2
Harry is furry.
True
2
proof
[(((triple2) -> rule2))]
("Harry" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple2) -> rule2))]
("Harry" "is" "furry" "-")
((triple2) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not quiet.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Harry" "is" "quiet" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Harry" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "rough" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "cold" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Gary is furry.[(triple1)] Harry is round.[(triple2)] @1: Gary is not quiet.[(((triple1) -> rule1))] Harry is furry.[(((triple2) -> rule2))] @2: Harry is not quiet.[(((((triple2) -> rule2)) -> rule1))]
Gary is furry.
("Gary" "is" "furry" "+")
triple1
Harry is round.
("Harry" "is" "round" "+")
triple2
Gary is not quiet.
("Gary" "is" "quiet" "-")
((triple1) -> (rule1 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2