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