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