Dave is furry. Dave is green. Dave is white. Furry, white people are young. All furry people are smart. If someone is smart then they are round.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is white.
("Dave" "is" "white" "+")
Furry, white people are young.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
All furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Dave is white.
True
1
proof
[(triple3)]
("Dave" "is" "white" "+")
triple3
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Dave is smart.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Dave" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not round.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Dave" "is" "round" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
@0: Dave is furry.[(triple1)] Dave is green.[(triple2)] Dave is white.[(triple3)] @1: Dave is smart.[(((triple1) -> rule2))] Dave is young.[(((triple1 triple3) -> rule1))] @2: Dave is round.[(((((triple1) -> rule2)) -> rule3))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple1 triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2