Hill Climbing

Algorithm

Choose initial Target with largest C_sw^Inferred
Repeatedly ...
- Try do a self-combining step, best-first
- Otherwise try to do a non-self-combining step
- Minimize C_sw^Leaves, then C_sw^Inferred, then C_sw^Inferences, hill climbing

Is the Combined Proof Different?

Proof		C_sw^Leaves	C_sw^Inferred	C_sw^Inferences
Original A		1.0000	0.8483	0.5616
Original B		1.0000	0.8483	0.5616
Combined 1		1.0000	0.8736	0.5616
Combined 2		0.6250	0.6405	0.4235