Dave is big. Dave is cold. Dave is quiet. Dave is red. Dave is round. Dave is smart. Dave is young. Big things are young.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Dave is quiet.
True
1
proof
[(triple3)]
("Dave" "is" "quiet" "+")
triple3
Dave is not red.
False
1
inv-proof
[(triple4)]
("Dave" "is" "red" "-")
triple4
@0: Dave is big.[(triple1)] Dave is cold.[(triple2)] Dave is quiet.[(triple3)] Dave is red.[(triple4)] Dave is round.[(triple5)] Dave is smart.[(triple6)] Dave is young.[(triple7 OR ((triple1) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple1) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1