Proof
1
conjecture
\( \forall \mathit{R}\, \forall \mathit{E}\, \left(\mathrm{order}(\mathit{R}, \mathit{E}) \to \forall \mathit{M1}\, \forall \mathit{M2}\, \left(\mathrm{min}(\mathit{M1}, \mathit{R}, \mathit{E}) \land \mathrm{min}(\mathit{M2}, \mathit{R}, \mathit{E}) \land \neg \left(\mathit{M1} = \mathit{M2}\right) \to \neg \exists \mathit{M}\, \mathrm{least}(\mathit{M}, \mathit{R}, \mathit{E})\right)\right) \)
thIV16  |  Problems/SET/SET804+4.p
2
axiom
\( \forall \mathit{R}\, \forall \mathit{E}\, \forall \mathit{M}\, \left(\mathrm{least}(\mathit{M}, \mathit{R}, \mathit{E}) \leftrightarrow \mathrm{member}(\mathit{M}, \mathit{E}) \land \forall \mathit{X}\, \left(\mathrm{member}(\mathit{X}, \mathit{E}) \to \mathrm{apply}(\mathit{R}, \mathit{M}, \mathit{X})\right)\right) \)
least  |  Axioms/SET006+3.ax
3
axiom
\( \forall \mathit{R}\, \forall \mathit{E}\, \forall \mathit{M}\, \left(\mathrm{min}(\mathit{M}, \mathit{R}, \mathit{E}) \leftrightarrow \mathrm{member}(\mathit{M}, \mathit{E}) \land \forall \mathit{X}\, \left(\mathrm{member}(\mathit{X}, \mathit{E}) \land \mathrm{apply}(\mathit{R}, \mathit{X}, \mathit{M}) \to \mathit{M} = \mathit{X}\right)\right) \)
min  |  Axioms/SET006+3.ax
4
negated_conjecture
\( \neg \forall \mathit{R}\, \forall \mathit{E}\, \left(\mathrm{order}(\mathit{R}, \mathit{E}) \to \forall \mathit{M1}\, \forall \mathit{M2}\, \left(\mathrm{min}(\mathit{M1}, \mathit{R}, \mathit{E}) \land \mathrm{min}(\mathit{M2}, \mathit{R}, \mathit{E}) \land \neg \left(\mathit{M1} = \mathit{M2}\right) \to \neg \exists \mathit{M}\, \mathrm{least}(\mathit{M}, \mathit{R}, \mathit{E})\right)\right) \)
negate_conjecture [ 1 ]
5
plain
\( \mathrm{least}(\mathrm{sk21}, \mathrm{sk17}, \mathrm{sk18}) \)
cnf_transformation [ 4 ]
6
plain
\( \neg \mathrm{least}(\mathit{V3}, \mathit{V1}, \mathit{V2}) \lor \neg \mathrm{member}(\mathit{V4}, \mathit{V2}) \lor \mathrm{apply}(\mathit{V1}, \mathit{V3}, \mathit{V4}) \)
cnf_transformation [ 2 ]
7
plain
\( \neg \mathrm{member}(\mathit{V538}, \mathrm{sk18}) \lor \mathrm{apply}(\mathrm{sk17}, \mathrm{sk21}, \mathit{V538}) \)
resolution [ 5, 6 ]
8
plain
\( \mathrm{min}(\mathrm{sk19}, \mathrm{sk17}, \mathrm{sk18}) \)
cnf_transformation [ 4 ]
9
plain
\( \neg \mathrm{min}(\mathit{V3}, \mathit{V1}, \mathit{V2}) \lor \neg \mathrm{member}(\mathit{V4}, \mathit{V2}) \lor \neg \mathrm{apply}(\mathit{V1}, \mathit{V4}, \mathit{V3}) \lor \mathit{V3} = \mathit{V4} \)
cnf_transformation [ 3 ]
10
plain
\( \neg \mathrm{member}(\mathit{V519}, \mathrm{sk18}) \lor \neg \mathrm{apply}(\mathrm{sk17}, \mathit{V519}, \mathrm{sk19}) \lor \mathrm{sk19} = \mathit{V519} \)
resolution [ 8, 9 ]
11
plain
\( \neg \mathrm{member}(\mathrm{sk19}, \mathrm{sk18}) \lor \neg \mathrm{member}(\mathrm{sk21}, \mathrm{sk18}) \lor \mathrm{sk19} = \mathrm{sk21} \)
resolution [ 7, 10 ]
12
plain
\( \neg \mathrm{least}(\mathit{V3}, \mathit{V1}, \mathit{V2}) \lor \mathrm{member}(\mathit{V3}, \mathit{V2}) \)
cnf_transformation [ 2 ]
13
plain
\( \mathrm{member}(\mathrm{sk21}, \mathrm{sk18}) \)
resolution [ 5, 12 ]
14
plain
\( \neg \mathrm{member}(\mathrm{sk19}, \mathrm{sk18}) \lor \mathrm{sk19} = \mathrm{sk21} \)
predicate_unit_simplification [ 11, 13 ]
15
plain
\( \neg \mathrm{min}(\mathit{V3}, \mathit{V1}, \mathit{V2}) \lor \mathrm{member}(\mathit{V3}, \mathit{V2}) \)
cnf_transformation [ 3 ]
16
plain
\( \mathrm{member}(\mathrm{sk19}, \mathrm{sk18}) \)
resolution [ 8, 15 ]
17
plain
\( \mathrm{sk19} = \mathrm{sk21} \)
predicate_unit_simplification [ 14, 16 ]
18
plain
\( \neg \mathrm{member}(\mathit{V538}, \mathrm{sk18}) \lor \mathrm{apply}(\mathrm{sk17}, \mathrm{sk19}, \mathit{V538}) \)
demodulation [ 7, 17 ]
19
plain
\( \mathrm{min}(\mathrm{sk20}, \mathrm{sk17}, \mathrm{sk18}) \)
cnf_transformation [ 4 ]
20
plain
\( \neg \mathrm{member}(\mathit{V520}, \mathrm{sk18}) \lor \neg \mathrm{apply}(\mathrm{sk17}, \mathit{V520}, \mathrm{sk20}) \lor \mathrm{sk20} = \mathit{V520} \)
resolution [ 19, 9 ]
21
plain
\( \neg \mathrm{member}(\mathrm{sk20}, \mathrm{sk18}) \lor \neg \mathrm{member}(\mathrm{sk19}, \mathrm{sk18}) \lor \mathrm{sk20} = \mathrm{sk19} \)
resolution [ 18, 20 ]
22
plain
\( \mathrm{member}(\mathrm{sk20}, \mathrm{sk18}) \)
resolution [ 19, 15 ]
23
plain
\( \neg \mathrm{member}(\mathrm{sk19}, \mathrm{sk18}) \lor \mathrm{sk20} = \mathrm{sk19} \)
predicate_unit_simplification [ 21, 22 ]
24
plain
\( \mathrm{sk20} = \mathrm{sk19} \)
predicate_unit_simplification [ 23, 16 ]
25
plain
\( \neg \left(\mathrm{sk19} = \mathrm{sk20}\right) \)
cnf_transformation [ 4 ]
26
plain
\( \bot \)
negative_simplify-reflect [ 24, 25 ]