Bob is big. Bob is nice. Bob is round. Dave is nice. Harry is blue. Harry is nice. Harry is young. If someone is blue and young then they are not furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is blue and young then they are not furry.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "-"))
Bob is round.
True
1
proof
[(triple3)]
("Bob" "is" "round" "+")
triple3
Harry is not nice.
False
1
inv-proof
[(triple6)]
("Harry" "is" "nice" "-")
triple6
Harry is not furry.
True
3
proof
[(((triple5 triple7) -> rule1))]
("Harry" "is" "furry" "-")
((triple5 triple7) -> (rule1 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is furry.
False
3
inv-proof
[(((triple5 triple7) -> rule1))]
("Harry" "is" "furry" "+")
((triple5 triple7) -> (rule1 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is nice.[(triple2)] Bob is round.[(triple3)] Dave is nice.[(triple4)] Harry is blue.[(triple5)] Harry is nice.[(triple6)] Harry is young.[(triple7)] @1: Harry is not furry.[(((triple5 triple7) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Harry is not furry.
("Harry" "is" "furry" "-")
((triple5 triple7) -> (rule1 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1