Dave is blue. Dave is red. Dave is round. If someone is blue and not red then they are not white. All round people are quiet. If someone is red then they are blue.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
If someone is blue and not red then they are not white.
((("someone" "is" "blue" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "white" "-"))
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is red then they are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Dave is blue.
True
1
proof
[(triple1 OR ((triple2) -> rule3))]
("Dave" "is" "blue" "+")
triple1
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not round.
False
1
inv-proof
[(triple3)]
("Dave" "is" "round" "-")
triple3
Dave is quiet.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "quiet" "-")
((triple3) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is blue.[(triple1 OR ((triple2) -> rule3))] Dave is red.[(triple2)] Dave is round.[(triple3)] @1: Dave is quiet.[(((triple3) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1