Bob is kind. Kind things are blue. If Bob is kind then Bob is round. All green things are cold. All blue things are white. All blue, green things are rough. If something is blue and not green then it is rough. If Bob is cold then Bob is blue. If Bob is round and Bob is not cold then Bob is blue.
Bob is kind.
("Bob" "is" "kind" "+")
Kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If Bob is kind then Bob is round.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "round" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All blue, green things are rough.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something is blue and not green then it is rough.
((("something" "is" "blue" "+") ("something" "is" "green" "~")) -> ("something" "is" "rough" "+"))
If Bob is cold then Bob is blue.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "blue" "+"))
If Bob is round and Bob is not cold then Bob is blue.
((("Bob" "is" "round" "+") ("Bob" "is" "cold" "~")) -> ("Bob" "is" "blue" "+"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Bob is not kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "-")
triple1
Bob is blue.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "round" "-")
((triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Bob" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Bob" "is" "white" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is kind.[(triple1)] @1: Bob is blue.[(((triple1) -> rule1))] Bob is round.[(((triple1) -> rule2))] @2: Bob is white.[(((((triple1) -> rule1)) -> rule4))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2