Bob is quiet. Charlie is not blue. Gary is nice. If Gary is quiet then Gary is furry. All red people are nice. Nice people are kind. If someone is furry then they are not cold. If someone is cold then they are red. If someone is nice then they are quiet.
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Gary is nice.
("Gary" "is" "nice" "+")
If Gary is quiet then Gary is furry.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "furry" "+"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is furry then they are not cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "-"))
If someone is cold then they are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Bob is not quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "-")
triple1
Gary is quiet.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "quiet" "+")
((triple3) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "kind" "-")
((triple3) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("Gary" "is" "furry" "+")
((((triple3) -> (rule6 % 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
[(((((triple3) -> rule6)) -> rule1))]
("Gary" "is" "furry" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not cold.
True
4
proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule4))]
("Gary" "is" "cold" "-")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is cold.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule4))]
("Gary" "is" "cold" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Charlie is not kind.
Unknown
inv-rconc
[@3: Charlie is kind.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "kind" "-")
Bob is kind.
Unknown
rconc
[@3: Bob is kind.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule5 <- FAIL)]]
("Bob" "is" "kind" "+")
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "red" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "red" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Bob is quiet.[(triple1)] Charlie is not blue.[(triple2)] Gary is nice.[(triple3)] @1: Gary is kind.[(((triple3) -> rule3))] Gary is quiet.[(((triple3) -> rule6))] @2: Gary is furry.[(((((triple3) -> rule6)) -> rule1))] @3: Gary is not cold.[(((((((triple3) -> rule6)) -> rule1)) -> rule4))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not cold.
("Gary" "is" "cold" "-")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3