Dave is quiet. Dave is smart. Dave is young. If something is round and quiet then it is furry. Furry, smart things are big. If something is smart then it is round.
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is round and quiet then it is furry.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Furry, smart things are big.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is smart then it is round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Dave is smart.
True
1
proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Dave is not smart.
False
1
inv-proof
[(triple2)]
("Dave" "is" "smart" "-")
triple2
Dave is round.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "round" "+")
((triple2) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "round" "-")
((triple2) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
True
4
proof
[(((((triple2) -> rule3) triple1) -> rule1))]
("Dave" "is" "furry" "+")
((((triple2) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not furry.
False
4
inv-proof
[(((((triple2) -> rule3) triple1) -> rule1))]
("Dave" "is" "furry" "-")
((((triple2) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
True
6
proof
[(((((((triple2) -> rule3) triple1) -> rule1) triple2) -> rule2))]
("Dave" "is" "big" "+")
((((((triple2) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not big.
False
6
inv-proof
[(((((((triple2) -> rule3) triple1) -> rule1) triple2) -> rule2))]
("Dave" "is" "big" "-")
((((((triple2) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
@0: Dave is quiet.[(triple1)] Dave is smart.[(triple2)] Dave is young.[(triple3)] @1: Dave is round.[(((triple2) -> rule3))] @2: Dave is furry.[(((((triple2) -> rule3) triple1) -> rule1))] @3: Dave is big.[(((((((triple2) -> rule3) triple1) -> rule1) triple2) -> rule2))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple2) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple2) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3