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