Bob is smart. Charlie is kind. Gary is blue. All furry people are nice. If someone is smart and round then they are nice. All smart people are cold. All kind, nice people are cold. If Charlie is kind then Charlie is cold. If someone is round then they are nice. If Gary is nice then Gary is smart. If Gary is nice then Gary is cold.
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Gary is blue.
("Gary" "is" "blue" "+")
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart and round then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
All kind, nice people are cold.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is kind then Charlie is cold.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "cold" "+"))
If someone is round then they are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If Gary is nice then Gary is smart.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "smart" "+"))
If Gary is nice then Gary is cold.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "cold" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Charlie is not kind.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "kind" "-")
triple2
Bob is cold.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "cold" "-")
((triple2) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is cold.
Unknown
rconc
[@3: Gary is cold.[CWA. Example of deepest failure = (rule3 <- rule7 <- rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is smart.[(triple1)] Charlie is kind.[(triple2)] Gary is blue.[(triple3)] @1: Bob is cold.[(((triple1) -> rule3))] Charlie is cold.[(((triple2) -> rule5))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1