Anne is quiet. Dave is quiet. Erin is red. Harry is white. If Dave is nice and Dave is red then Dave is white. White, smart things are nice. If something is red then it is green. If something is smart and green then it is red. All quiet, big things are red. If something is quiet and green then it is white. Quiet things are white. If Dave is smart and Dave is nice then Dave is big.
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
If Dave is nice and Dave is red then Dave is white.
((("Dave" "is" "nice" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "white" "+"))
White, smart things are nice.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is smart and green then it is red.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All quiet, big things are red.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is quiet and green then it is white.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If Dave is smart and Dave is nice then Dave is big.
((("Dave" "is" "smart" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "big" "+"))
Erin is red.
True
1
proof
[(triple3)]
("Erin" "is" "red" "+")
triple3
Dave is not quiet.
False
1
inv-proof
[(triple2)]
("Dave" "is" "quiet" "-")
triple2
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "nice" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Anne is quiet.[(triple1)] Dave is quiet.[(triple2)] Erin is red.[(triple3)] Harry is white.[(triple4)] @1: Anne is white.[(((triple1) -> rule7))] Dave is white.[(((triple2) -> rule7))] Erin is green.[(((triple3) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1