Dave is quiet. If someone is rough then they are quiet. If someone is round and furry then they are rough. Round, nice people are big. Nice people are furry. Round, furry people are nice. All quiet, furry people are kind. If Dave is quiet then Dave is round. If Dave is round then Dave is furry.
Dave is quiet.
("Dave" "is" "quiet" "+")
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is round and furry then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Round, nice people are big.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Round, furry people are nice.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All quiet, furry people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If Dave is quiet then Dave is round.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "round" "+"))
If Dave is round then Dave is furry.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "furry" "+"))
Dave is quiet.
True
1
proof
[(triple1)]
("Dave" "is" "quiet" "+")
triple1
Dave is not quiet.
False
1
inv-proof
[(triple1)]
("Dave" "is" "quiet" "-")
triple1
Dave is round.
True
2
proof
[(((triple1) -> rule7))]
("Dave" "is" "round" "+")
((triple1) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple1) -> rule7))]
("Dave" "is" "round" "-")
((triple1) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
True
3
proof
[(((((triple1) -> rule7)) -> rule8))]
("Dave" "is" "furry" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule8))]
("Dave" "is" "furry" "-")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
True
5
proof
[(((triple1 ((((triple1) -> rule7)) -> rule8)) -> rule6))]
("Dave" "is" "kind" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not kind.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule7)) -> rule8)) -> rule6))]
("Dave" "is" "kind" "-")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
@0: Dave is quiet.[(triple1)] @1: Dave is round.[(((triple1) -> rule7))] @2: Dave is furry.[(((((triple1) -> rule7)) -> rule8))] @3: Dave is kind.[(((triple1 ((((triple1) -> rule7)) -> rule8)) -> rule6))] Dave is nice.[(((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule8)) -> rule5))] Dave is rough.[(((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule8)) -> rule2))] @4: Dave is big.[(((((triple1) -> rule7) ((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule8)) -> rule5)) -> rule3))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule7 % int4)) ((((triple1) -> (rule7 % int4)) ((((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4