Anne is blue. Bob is red. Charlie is red. Dave is red. If Dave is furry then Dave is blue. If someone is big then they are blue. If someone is red then they are not blue.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is red.
("Dave" "is" "red" "+")
If Dave is furry then Dave is blue.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "blue" "+"))
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is red then they are not blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "-"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Bob is not blue.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "blue" "-")
((triple2) -> (rule3 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Charlie is blue.
False
2
inv-proof
[(((triple3) -> rule3))]
("Charlie" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is blue.[(triple1)] Bob is red.[(triple2)] Charlie is red.[(triple3)] Dave is red.[(triple4)] @1: Bob is not blue.[(((triple2) -> rule3))] Charlie is not blue.[(((triple3) -> rule3))] Dave is not blue.[(((triple4) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Bob is not blue.
("Bob" "is" "blue" "-")
((triple2) -> (rule3 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Charlie is not blue.
("Charlie" "is" "blue" "-")
((triple3) -> (rule3 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
((triple4) -> (rule3 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1