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