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