Bob is not green. Gary is kind. Harry is kind. If someone is quiet then they are furry. If someone is young then they are furry. All furry people are nice. If someone is nice and not big then they are quiet. If someone is kind then they are quiet. All furry, young people are not kind. If someone is furry then they are not green. If someone is nice and not big then they are green.
Bob is not green.
("Bob" "is" "green" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If someone is quiet then they are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If someone is young then they are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and not big then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
All furry, young people are not kind.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "-"))
If someone is furry then they are not green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "-"))
If someone is nice and not big then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "green" "+"))
Harry is kind.
True
1
proof
[(triple3)]
("Harry" "is" "kind" "+")
triple3
Gary is not kind.
False
1
inv-proof
[(triple2)]
("Gary" "is" "kind" "-")
triple2
Gary is quiet.
True
2
proof
[(((triple2) -> rule5))]
("Gary" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple3) -> rule5))]
("Harry" "is" "quiet" "-")
((triple3) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Gary is furry.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("Gary" "is" "furry" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("Gary" "is" "furry" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Harry is nice.
True
4
proof
[(((((((triple3) -> rule5)) -> rule1)) -> rule3))]
("Harry" "is" "nice" "+")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not nice.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule1)) -> rule3))]
("Harry" "is" "nice" "-")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is nice.
Unknown
rconc
[@3: Bob is nice.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule4 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not furry.
Unknown
inv-rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Bob" "is" "furry" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Bob is not green.[(triple1)] Gary is kind.[(triple2)] Harry is kind.[(triple3)] @1: Gary is quiet.[(((triple2) -> rule5))] Harry is quiet.[(((triple3) -> rule5))] @2: Gary is furry.[(((((triple2) -> rule5)) -> rule1))] Harry is furry.[(((((triple3) -> rule5)) -> rule1))] @3: Gary is nice.[(((((((triple2) -> rule5)) -> rule1)) -> rule3))] Gary is not green.[(((((((triple2) -> rule5)) -> rule1)) -> rule7))] Harry is nice.[(((((((triple3) -> rule5)) -> rule1)) -> rule3))] Harry is not green.[(((((((triple3) -> rule5)) -> rule1)) -> rule7))]
Bob is not green.
("Bob" "is" "green" "-")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not green.
("Gary" "is" "green" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not green.
("Harry" "is" "green" "-")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3