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