Dave is furry. If something is furry then it is quiet. Big, smart things are green. If something is smart and green then it is big. If something is quiet and green then it is round. If Dave is quiet then Dave is kind. If Dave is furry then Dave is green. If something is round then it is quiet. If Dave is furry and Dave is round then Dave is big.
Dave is furry.
("Dave" "is" "furry" "+")
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Big, smart things are green.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is smart and green then it is big.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is quiet and green then it is round.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If Dave is quiet then Dave is kind.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "kind" "+"))
If Dave is furry then Dave is green.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "green" "+"))
If something is round then it is quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If Dave is furry and Dave is round then Dave is big.
((("Dave" "is" "furry" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "big" "+"))
Dave is furry.
True
1
proof
[(triple1)]
("Dave" "is" "furry" "+")
triple1
Dave is not furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
Dave is green.
True
2
proof
[(((triple1) -> rule6))]
("Dave" "is" "green" "+")
((triple1) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple1) -> rule6))]
("Dave" "is" "green" "-")
((triple1) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Dave" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not round.
False
5
inv-proof
[(((((triple1) -> rule1) ((triple1) -> rule6)) -> rule4))]
("Dave" "is" "round" "-")
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is big.
True
7
proof
[(((triple1 ((((triple1) -> rule1) ((triple1) -> rule6)) -> rule4)) -> rule8))]
("Dave" "is" "big" "+")
((triple1 ((((triple1) -> (rule1 % int4)) ((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is not big.
False
7
inv-proof
[(((triple1 ((((triple1) -> rule1) ((triple1) -> rule6)) -> rule4)) -> rule8))]
("Dave" "is" "big" "-")
((triple1 ((((triple1) -> (rule1 % int4)) ((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
@0: Dave is furry.[(triple1)] @1: Dave is green.[(((triple1) -> rule6))] Dave is quiet.[(((triple1) -> rule1))] @2: Dave is kind.[(((((triple1) -> rule1)) -> rule5))] Dave is round.[(((((triple1) -> rule1) ((triple1) -> rule6)) -> rule4))] @3: Dave is big.[(((triple1 ((((triple1) -> rule1) ((triple1) -> rule6)) -> rule4)) -> rule8))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((triple1 ((((triple1) -> (rule1 % int4)) ((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4