Bob is cold. Erin is not white. Gary is kind. If something is cold then it is kind. If Erin is cold and Erin is not rough then Erin is not red. If Gary is quiet then Gary is red. If something is white and not kind then it is quiet. All kind things are quiet. If something is white and not quiet then it is not red.
Bob is cold.
("Bob" "is" "cold" "+")
Erin is not white.
("Erin" "is" "white" "-")
Gary is kind.
("Gary" "is" "kind" "+")
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If Erin is cold and Erin is not rough then Erin is not red.
((("Erin" "is" "cold" "+") ("Erin" "is" "rough" "~")) -> ("Erin" "is" "red" "-"))
If Gary is quiet then Gary is red.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "red" "+"))
If something is white and not kind then it is quiet.
((("something" "is" "white" "+") ("something" "is" "kind" "~")) -> ("something" "is" "quiet" "+"))
All kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is white and not quiet then it is not red.
((("something" "is" "white" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "red" "-"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Erin is white.
False
1
inv-proof
[(triple2)]
("Erin" "is" "white" "+")
triple2
Bob is kind.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "kind" "-")
Erin is quiet.
Unknown
rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Erin" "is" "quiet" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Bob is cold.[(triple1)] Erin is not white.[(triple2)] Gary is kind.[(triple3)] @1: Bob is kind.[(((triple1) -> rule1))] Gary is quiet.[(((triple3) -> rule5))] @2: Bob is quiet.[(((((triple1) -> rule1)) -> rule5))] Gary is red.[(((((triple3) -> rule5)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Erin is not white.
("Erin" "is" "white" "-")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2