Anne is quiet. Anne is round. Anne is smart. Anne is not white. Dave is cold. Harry is not quiet. Harry is smart. If something is round then it is big. All nice things are quiet. If something is smart and not round then it is cold.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is not white.
("Anne" "is" "white" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is smart.
("Harry" "is" "smart" "+")
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is smart and not round then it is cold.
((("something" "is" "smart" "+") ("something" "is" "round" "~")) -> ("something" "is" "cold" "+"))
Anne is not white.
True
1
proof
[(triple4)]
("Anne" "is" "white" "-")
triple4
Anne is white.
False
1
inv-proof
[(triple4)]
("Anne" "is" "white" "+")
triple4
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is not white.[(triple4)] Anne is quiet.[(triple1)] Anne is round.[(triple2)] Anne is smart.[(triple3)] Dave is cold.[(triple5)] Harry is not quiet.[(triple6)] Harry is smart.[(triple7)] @1: Anne is big.[(((triple2) -> rule1))]
Anne is not white.
("Anne" "is" "white" "-")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1