Dave is big. Dave is furry. Dave is smart. If Dave is nice and Dave is furry then Dave is blue. Young people are blue. All big people are nice. All white, nice people are young. Blue people are white. All blue people are furry. Young people are white. If Dave is nice and Dave is white then Dave is big.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If Dave is nice and Dave is furry then Dave is blue.
((("Dave" "is" "nice" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "blue" "+"))
Young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
All white, nice people are young.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
All blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If Dave is nice and Dave is white then Dave is big.
((("Dave" "is" "nice" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "big" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not smart.
False
1
inv-proof
[(triple3)]
("Dave" "is" "smart" "-")
triple3
Dave is nice.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
True
4
proof
[(((((triple1) -> rule3) triple2) -> rule1))]
("Dave" "is" "blue" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not blue.
False
4
inv-proof
[(((((triple1) -> rule3) triple2) -> rule1))]
("Dave" "is" "blue" "-")
((((triple1) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
True
5
proof
[(((((((triple1) -> rule3) triple2) -> rule1)) -> rule5))]
("Dave" "is" "white" "+")
((((((triple1) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not white.
False
5
inv-proof
[(((((((triple1) -> rule3) triple2) -> rule1)) -> rule5))]
("Dave" "is" "white" "-")
((((((triple1) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
@0: Dave is big.[(triple1)] Dave is furry.[(triple2)] Dave is smart.[(triple3)] @1: Dave is nice.[(((triple1) -> rule3))] @2: Dave is blue.[(((((triple1) -> rule3) triple2) -> rule1))] @3: Dave is white.[(((((((triple1) -> rule3) triple2) -> rule1)) -> rule5))] @4: Dave is young.[(((((((((triple1) -> rule3) triple2) -> rule1)) -> rule5) ((triple1) -> rule3)) -> rule4))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((((triple1) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((((((((triple1) -> (rule3 % int4)) triple2) -> (rule1 % int3))) -> (rule5 % int2)) ((triple1) -> (rule3 % int4))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4