Bob is furry. Gary is nice. Harry is kind. If Bob is red and Bob is not kind then Bob is not furry. If Harry is kind then Harry is furry. White things are nice. If something is kind then it is white. If Harry is furry and Harry is nice then Harry is not quiet. White things are round.
Bob is furry.
("Bob" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If Bob is red and Bob is not kind then Bob is not furry.
((("Bob" "is" "red" "+") ("Bob" "is" "kind" "~")) -> ("Bob" "is" "furry" "-"))
If Harry is kind then Harry is furry.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "furry" "+"))
White things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is kind then it is white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If Harry is furry and Harry is nice then Harry is not quiet.
((("Harry" "is" "furry" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "quiet" "-"))
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Gary is not nice.
False
1
inv-proof
[(triple2)]
("Gary" "is" "nice" "-")
triple2
Harry is white.
True
2
proof
[(((triple3) -> rule4))]
("Harry" "is" "white" "+")
((triple3) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple3) -> rule4))]
("Harry" "is" "white" "-")
((triple3) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
True
3
proof
[(((((triple3) -> rule4)) -> rule3))]
("Harry" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule6))]
("Harry" "is" "round" "-")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not quiet.
True
6
proof
[(((((triple3) -> rule2) ((((triple3) -> rule4)) -> rule3)) -> rule5))]
("Harry" "is" "quiet" "-")
((((triple3) -> (rule2 % int4)) ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is quiet.
False
6
inv-proof
[(((((triple3) -> rule2) ((((triple3) -> rule4)) -> rule3)) -> rule5))]
("Harry" "is" "quiet" "+")
((((triple3) -> (rule2 % int4)) ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Gary" "is" "round" "-")
Bob is round.
Unknown
rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "white" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "white" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is furry.[(triple1)] Gary is nice.[(triple2)] Harry is kind.[(triple3)] @1: Harry is furry.[(((triple3) -> rule2))] Harry is white.[(((triple3) -> rule4))] @2: Harry is nice.[(((((triple3) -> rule4)) -> rule3))] Harry is round.[(((((triple3) -> rule4)) -> rule6))] @3: Harry is not quiet.[(((((triple3) -> rule2) ((((triple3) -> rule4)) -> rule3)) -> rule5))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((triple3) -> (rule2 % int4)) ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4