Bob is white. Fiona is nice. Gary is green. Harry is blue. Nice things are not blue. Smart, white things are green. All smart things are quiet.
Bob is white.
("Bob" "is" "white" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Nice things are not blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "-"))
Smart, white things are green.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Bob is white.
True
1
proof
[(triple1)]
("Bob" "is" "white" "+")
triple1
Harry is not blue.
False
1
inv-proof
[(triple4)]
("Harry" "is" "blue" "-")
triple4
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Bob is white.[(triple1)] Fiona is nice.[(triple2)] Gary is green.[(triple3)] Harry is blue.[(triple4)] @1: Fiona is not blue.[(((triple2) -> rule1))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Fiona is not blue.
("Fiona" "is" "blue" "-")
((triple2) -> (rule1 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1