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