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