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