Dave is big. Dave is furry. Dave is nice. Dave is quiet. Dave is round. Dave is smart. Dave is young. If Dave is smart and Dave is furry then Dave is nice. All round things are nice. If Dave is nice and Dave is quiet then Dave is young. All round, furry things are nice. If something is smart then it is round. If Dave is furry then Dave is young.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
If Dave is smart and Dave is furry then Dave is nice.
((("Dave" "is" "smart" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "nice" "+"))
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If Dave is nice and Dave is quiet then Dave is young.
((("Dave" "is" "nice" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "young" "+"))
All round, furry things are nice.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is smart then it is round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If Dave is furry then Dave is young.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "young" "+"))
Dave is round.
True
1
proof
[(triple5 OR ((triple6) -> rule5))]
("Dave" "is" "round" "+")
triple5
((triple6) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not smart.
False
1
inv-proof
[(triple6)]
("Dave" "is" "smart" "-")
triple6
@0: Dave is big.[(triple1)] Dave is furry.[(triple2)] Dave is nice.[(triple3 OR ((triple5) -> rule2) OR ((triple5 triple2) -> rule4) OR ((triple6 triple2) -> rule1) OR ((((triple6) -> rule5)) -> rule2) OR ((((triple6) -> rule5) triple2) -> rule4))] Dave is quiet.[(triple4)] Dave is round.[(triple5 OR ((triple6) -> rule5))] Dave is smart.[(triple6)] Dave is young.[(triple7 OR ((triple2) -> rule6) OR ((triple3 triple4) -> rule3) OR ((((triple5) -> rule2) triple4) -> rule3) OR ((((triple5 triple2) -> rule4) triple4) -> rule3) OR ((((triple6 triple2) -> rule1) triple4) -> rule3) OR ((((((triple6) -> rule5)) -> rule2) triple4) -> rule3) OR ((((((triple6) -> rule5) triple2) -> rule4) triple4) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple5) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple5 triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple6 triple2) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple6) -> (rule5 % int2)) triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple6) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple2) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple3 triple4) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple5) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple5 triple2) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple6 triple2) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple6) -> (rule5 % int3)) triple2) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3