Bob is blue. Bob is furry. Bob is kind. Bob is nice. Gary is blue. Gary is kind. Gary is quiet. If Gary is nice then Gary is kind. If someone is quiet then they are kind. If someone is green then they are furry. If someone is nice and blue then they are quiet. Kind, quiet people are rough. If someone is furry then they are kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If Gary is nice then Gary is kind.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "kind" "+"))
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is green then they are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If someone is nice and blue then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
Kind, quiet people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry then they are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Bob is nice.
True
1
proof
[(triple4)]
("Bob" "is" "nice" "+")
triple4
Bob is not kind.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule6) OR ((((triple4 triple1) -> rule4)) -> rule2))]
("Bob" "is" "kind" "-")
triple3
((triple2) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple4 triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is quiet.
True
3
proof
[(((triple4 triple1) -> rule4))]
("Bob" "is" "quiet" "+")
((triple4 triple1) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
3
inv-proof
[(((triple4 triple1) -> rule4))]
("Bob" "is" "quiet" "-")
((triple4 triple1) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
True
5
proof
[(((triple3 ((triple4 triple1) -> rule4)) -> rule5) OR ((((triple2) -> rule6) ((triple4 triple1) -> rule4)) -> rule5) OR ((((((triple4 triple1) -> rule4)) -> rule2) ((triple4 triple1) -> rule4)) -> rule5))]
("Bob" "is" "rough" "+")
((triple3 ((triple4 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple2) -> (rule6 % int3)) ((triple4 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple4 triple1) -> (rule4 % int3))) -> (rule2 % int2)) ((triple4 triple1) -> (rule4 % int3))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not rough.
False
5
inv-proof
[(((triple3 ((triple4 triple1) -> rule4)) -> rule5) OR ((((triple2) -> rule6) ((triple4 triple1) -> rule4)) -> rule5) OR ((((((triple4 triple1) -> rule4)) -> rule2) ((triple4 triple1) -> rule4)) -> rule5))]
("Bob" "is" "rough" "-")
((triple3 ((triple4 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple2) -> (rule6 % int3)) ((triple4 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple4 triple1) -> (rule4 % int3))) -> (rule2 % int2)) ((triple4 triple1) -> (rule4 % int3))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is kind.[(triple3 OR ((triple2) -> rule6) OR ((((triple4 triple1) -> rule4)) -> rule2))] Bob is nice.[(triple4)] Gary is blue.[(triple5)] Gary is kind.[(triple6 OR ((triple7) -> rule2))] Gary is quiet.[(triple7)] @1: Bob is quiet.[(((triple4 triple1) -> rule4))] Gary is rough.[(((triple6 triple7) -> rule5) OR ((((triple7) -> rule2) triple7) -> rule5))] @2: Bob is rough.[(((triple3 ((triple4 triple1) -> rule4)) -> rule5) OR ((((triple2) -> rule6) ((triple4 triple1) -> rule4)) -> rule5) OR ((((((triple4 triple1) -> rule4)) -> rule2) ((triple4 triple1) -> rule4)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple2) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple4 triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
((triple7) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple4 triple1) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple6 triple7) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple7) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((triple3 ((triple4 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple2) -> (rule6 % int3)) ((triple4 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple4 triple1) -> (rule4 % int3))) -> (rule2 % int2)) ((triple4 triple1) -> (rule4 % int3))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3