Anne is nice. Bob is furry. Bob is green. Bob is nice. Bob is not quiet. Bob is not smart. Dave is blue. Dave is furry. Dave is not green. Dave is nice. Dave is quiet. Dave is rough. Dave is smart. Harry is blue. Harry is furry. Harry is rough. If Anne is smart then Anne is not green. If Anne is furry then Anne is blue. If something is green then it is furry. If Harry is smart then Harry is rough. Rough, furry things are smart. If Anne is not furry then Anne is nice.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is not smart.
("Bob" "is" "smart" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Anne is smart then Anne is not green.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "green" "-"))
If Anne is furry then Anne is blue.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "blue" "+"))
If something is green then it is furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If Harry is smart then Harry is rough.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "rough" "+"))
Rough, furry things are smart.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Anne is not furry then Anne is nice.
((("Anne" "is" "furry" "~")) -> ("Anne" "is" "nice" "+"))
Bob is not smart.
True
1
proof
[(triple6)]
("Bob" "is" "smart" "-")
triple6
Dave is not quiet.
False
1
inv-proof
[(triple11)]
("Dave" "is" "quiet" "-")
triple11
Harry is smart.
True
3
proof
[(((triple16 triple15) -> rule5))]
("Harry" "is" "smart" "+")
((triple16 triple15) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
3
inv-proof
[(((triple16 triple15) -> rule5))]
("Harry" "is" "smart" "-")
((triple16 triple15) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "smart" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is nice.[(triple1)] Bob is furry.[(triple2 OR ((triple3) -> rule3))] Bob is green.[(triple3)] Bob is nice.[(triple4)] Bob is not quiet.[(triple5)] Bob is not smart.[(triple6)] Dave is blue.[(triple7)] Dave is furry.[(triple8)] Dave is nice.[(triple10)] Dave is not green.[(triple9)] Dave is quiet.[(triple11)] Dave is rough.[(triple12)] Dave is smart.[(triple13 OR ((triple12 triple8) -> rule5))] Harry is blue.[(triple14)] Harry is furry.[(triple15)] Harry is rough.[(triple16)] @1: Harry is smart.[(((triple16 triple15) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple3) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple5
Bob is not smart.
("Bob" "is" "smart" "-")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple10
Dave is not green.
("Dave" "is" "green" "-")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
Dave is rough.
("Dave" "is" "rough" "+")
triple12
Dave is smart.
("Dave" "is" "smart" "+")
triple13
((triple12 triple8) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple14
Harry is furry.
("Harry" "is" "furry" "+")
triple15
Harry is rough.
("Harry" "is" "rough" "+")
triple16
Harry is smart.
("Harry" "is" "smart" "+")
((triple16 triple15) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1