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