Charlie is red. Dave is white. Erin is white. Harry is red. If Dave is rough and Dave is blue then Dave is red. If something is nice then it is quiet. If Erin is nice and Erin is round then Erin is white.
Charlie is red.
("Charlie" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is red.
("Harry" "is" "red" "+")
If Dave is rough and Dave is blue then Dave is red.
((("Dave" "is" "rough" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "red" "+"))
If something is nice then it is quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If Erin is nice and Erin is round then Erin is white.
((("Erin" "is" "nice" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "white" "+"))
Charlie is red.
True
1
proof
[(triple1)]
("Charlie" "is" "red" "+")
triple1
Erin is not white.
False
1
inv-proof
[(triple3)]
("Erin" "is" "white" "-")
triple3
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is red.[(triple1)] Dave is white.[(triple2)] Erin is white.[(triple3)] Harry is red.[(triple4)]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4