Dave is not green. Gary is green. Harry is big. Green people are quiet. All quiet people are not furry. If someone is green and not big then they are not furry.
Dave is not green.
("Dave" "is" "green" "-")
Gary is green.
("Gary" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are not furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "-"))
If someone is green and not big then they are not furry.
((("someone" "is" "green" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "furry" "-"))
Harry is big.
True
1
proof
[(triple3)]
("Harry" "is" "big" "+")
triple3
Dave is green.
False
1
inv-proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Gary is quiet.
True
2
proof
[(((triple2) -> rule1))]
("Gary" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple2) -> rule1))]
("Gary" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not furry.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("Gary" "is" "furry" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Gary" "is" "furry" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "quiet" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Dave is not green.[(triple1)] Gary is green.[(triple2)] Harry is big.[(triple3)] @1: Gary is quiet.[(((triple2) -> rule1))] @2: Gary is not furry.[(((((triple2) -> rule1)) -> rule2))]
Dave is not green.
("Dave" "is" "green" "-")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2