Dave is furry. Dave is green. Dave is kind. Dave is quiet. Dave is rough. Dave is smart. Dave is not white. Erin is kind. Erin is rough. Gary is quiet. Gary is smart. Harry is furry. Harry is green. Harry is kind. Harry is not rough. Harry is smart. All smart, quiet people are not white. If Harry is furry and Harry is quiet then Harry is kind. If Harry is not white then Harry is not rough.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is not white.
("Dave" "is" "white" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is smart.
("Harry" "is" "smart" "+")
All smart, quiet people are not white.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "-"))
If Harry is furry and Harry is quiet then Harry is kind.
((("Harry" "is" "furry" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "kind" "+"))
If Harry is not white then Harry is not rough.
((("Harry" "is" "white" "~")) -> ("Harry" "is" "rough" "-"))
Dave is furry.
True
1
proof
[(triple1)]
("Dave" "is" "furry" "+")
triple1
Dave is not rough.
False
1
inv-proof
[(triple5)]
("Dave" "is" "rough" "-")
triple5
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Dave is furry.[(triple1)] Dave is green.[(triple2)] Dave is kind.[(triple3)] Dave is not white.[(triple7 OR ((triple6 triple4) -> rule1))] Dave is quiet.[(triple4)] Dave is rough.[(triple5)] Dave is smart.[(triple6)] Erin is kind.[(triple8)] Erin is rough.[(triple9)] Gary is quiet.[(triple10)] Gary is smart.[(triple11)] Harry is furry.[(triple12)] Harry is green.[(triple13)] Harry is kind.[(triple14)] Harry is not rough.[(triple15)] Harry is smart.[(triple16)] @1: Gary is not white.[(((triple11 triple10) -> rule1))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is not white.
("Dave" "is" "white" "-")
triple7
((triple6 triple4) -> (rule1 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is not rough.
("Harry" "is" "rough" "-")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16
Gary is not white.
("Gary" "is" "white" "-")
((triple11 triple10) -> (rule1 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1