Dave is big. Dave is blue. Dave is furry. Dave is quiet. Dave is rough. Dave is white. Dave is young. Harry is big. Harry is blue. Harry is furry. Harry is quiet. Harry is rough. Harry is white. Harry is young. Quiet, furry people are young. All young people are furry. If Dave is furry then Dave is rough.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
Quiet, furry people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
All young people are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If Dave is furry then Dave is rough.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "rough" "+"))
Dave is young.
True
1
proof
[(triple7 OR ((triple4 triple3) -> rule1))]
("Dave" "is" "young" "+")
triple7
((triple4 triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not quiet.
False
1
inv-proof
[(triple4)]
("Dave" "is" "quiet" "-")
triple4
@0: Dave is big.[(triple1)] Dave is blue.[(triple2)] Dave is furry.[(triple3 OR ((triple7) -> rule2))] Dave is quiet.[(triple4)] Dave is rough.[(triple5 OR ((triple3) -> rule3) OR ((((triple7) -> rule2)) -> rule3))] Dave is white.[(triple6)] Dave is young.[(triple7 OR ((triple4 triple3) -> rule1))] Harry is big.[(triple8)] Harry is blue.[(triple9)] Harry is furry.[(triple10 OR ((triple14) -> rule2))] Harry is quiet.[(triple11)] Harry is rough.[(triple12)] Harry is white.[(triple13)] Harry is young.[(triple14 OR ((triple11 triple10) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple7) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple3) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple4 triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
((triple14) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is white.
("Harry" "is" "white" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14
((triple11 triple10) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1