Anne is green. Bob is white. Gary is quiet. Harry is green. Green things are red. If something is nice then it is green. All rough, nice things are quiet.
Anne is green.
("Anne" "is" "green" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is green.
("Harry" "is" "green" "+")
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
All rough, nice things are quiet.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Anne is green.
True
1
proof
[(triple1)]
("Anne" "is" "green" "+")
triple1
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Harry is red.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "red" "+")
((triple4) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "red" "-")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "quiet" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Anne is green.[(triple1)] Bob is white.[(triple2)] Gary is quiet.[(triple3)] Harry is green.[(triple4)] @1: Anne is red.[(((triple1) -> rule1))] Harry is red.[(((triple4) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple4) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1