Bob is cold. Bob is green. Bob is kind. If someone is white then they are blue. All white, cold people are kind. If someone is green then they are kind. All cold people are white. Green, rough people are white. If someone is rough then they are not white. If Bob is not green then Bob is kind. All quiet people are rough.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
If someone is white then they are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
All white, cold people are kind.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Green, rough people are white.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is rough then they are not white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "-"))
If Bob is not green then Bob is kind.
((("Bob" "is" "green" "~")) -> ("Bob" "is" "kind" "+"))
All quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Bob is not cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
Bob is white.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "white" "+")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "white" "-")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("Bob" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule1))]
("Bob" "is" "blue" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3 OR ((triple2) -> rule3) OR ((((triple1) -> rule4) triple1) -> rule2))] @1: Bob is white.[(((triple1) -> rule4))] @2: Bob is blue.[(((((triple1) -> rule4)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2