Anne is quiet. Anne is not white. Dave is nice. Dave is white. Gary is furry. Harry is furry. Harry is round. If Gary is furry then Gary is rough. Big things are not rough. White things are big.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not white.
("Anne" "is" "white" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
If Gary is furry then Gary is rough.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "rough" "+"))
Big things are not rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "-"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Harry is round.
True
1
proof
[(triple7)]
("Harry" "is" "round" "+")
triple7
Gary is not furry.
False
1
inv-proof
[(triple5)]
("Gary" "is" "furry" "-")
triple5
Dave is big.
True
2
proof
[(((triple4) -> rule3))]
("Dave" "is" "big" "+")
((triple4) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple4) -> rule3))]
("Dave" "is" "big" "-")
((triple4) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "big" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Anne is not white.[(triple2)] Anne is quiet.[(triple1)] Dave is nice.[(triple3)] Dave is white.[(triple4)] Gary is furry.[(triple5)] Harry is furry.[(triple6)] Harry is round.[(triple7)] @1: Dave is big.[(((triple4) -> rule3))] Gary is rough.[(((triple5) -> rule1))] @2: Dave is not rough.[(((((triple4) -> rule3)) -> rule2))]
Anne is not white.
("Anne" "is" "white" "-")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
((triple4) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is not rough.
("Dave" "is" "rough" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2