Dave is rough. All green, rough people are round. All round people are white. Rough people are young. All rough people are furry. If Dave is rough then Dave is red. If Dave is furry then Dave is green.
Dave is rough.
("Dave" "is" "rough" "+")
All green, rough people are round.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
All rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If Dave is rough then Dave is red.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "red" "+"))
If Dave is furry then Dave is green.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "green" "+"))
Dave is rough.
True
1
proof
[(triple1)]
("Dave" "is" "rough" "+")
triple1
Dave is not rough.
False
1
inv-proof
[(triple1)]
("Dave" "is" "rough" "-")
triple1
Dave is furry.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple1) -> rule5))]
("Dave" "is" "red" "-")
((triple1) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("Dave" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("Dave" "is" "green" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
True
5
proof
[(((((((triple1) -> rule4)) -> rule6) triple1) -> rule1))]
("Dave" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not round.
False
5
inv-proof
[(((((((triple1) -> rule4)) -> rule6) triple1) -> rule1))]
("Dave" "is" "round" "-")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
@0: Dave is rough.[(triple1)] @1: Dave is furry.[(((triple1) -> rule4))] Dave is red.[(((triple1) -> rule5))] Dave is young.[(((triple1) -> rule3))] @2: Dave is green.[(((((triple1) -> rule4)) -> rule6))] @3: Dave is round.[(((((((triple1) -> rule4)) -> rule6) triple1) -> rule1))] @4: Dave is white.[(((((((((triple1) -> rule4)) -> rule6) triple1) -> rule1)) -> rule2))]
Dave is rough.
("Dave" "is" "rough" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule6 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4