Proof
1
negated_conjecture
\( \neg \left(\mathrm{d}(\mathit{Y}, \mathrm{x}) = \mathrm{mul}(\mathrm{exp}(\mathrm{mul}(\mathrm{x}, \mathrm{ln}(\mathrm{x}))), \mathrm{add}(\mathrm{ln}(\mathrm{x}), \mathtt{1}))\right) \lor \mathrm{ans}(\mathit{Y}) \)
query  |  AnsTasks/zad16d.p
2
axiom
\( \mathrm{mul}(\mathit{X}, \mathrm{div}(\mathtt{1}, \mathit{X})) = \mathtt{1} \)
mul_inv  |  AnsTasks/zad16d.p
3
axiom
\( \mathrm{d}(\mathrm{ln}(\mathit{X}), \mathit{X}) = \mathrm{div}(\mathtt{1}, \mathit{X}) \)
diff_ln  |  AnsTasks/zad16d.p
4
axiom
\( \mathrm{d}(\mathit{X}, \mathit{X}) = \mathtt{1} \)
diff_var  |  AnsTasks/zad16d.p
5
axiom
\( \mathrm{d}(\mathrm{mul}(\mathit{U}, \mathit{V}), \mathit{X}) = \mathrm{add}(\mathrm{mul}(\mathrm{d}(\mathit{U}, \mathit{X}), \mathit{V}), \mathrm{mul}(\mathit{U}, \mathrm{d}(\mathit{V}, \mathit{X}))) \)
diff_mul  |  AnsTasks/zad16d.p
6
axiom
\( \mathrm{mul}(\mathtt{1}, \mathit{X}) = \mathit{X} \)
mul_1_l  |  AnsTasks/zad16d.p
7
axiom
\( \mathrm{d}(\mathrm{exp}(\mathit{U}), \mathit{X}) = \mathrm{mul}(\mathrm{exp}(\mathit{U}), \mathrm{d}(\mathit{U}, \mathit{X})) \)
diff_exp_chain  |  AnsTasks/zad16d.p
8
plain
\( \neg \left(\mathrm{d}(\mathit{Y}, \mathrm{x}) = \mathrm{mul}(\mathrm{exp}(\mathrm{mul}(\mathrm{x}, \mathrm{ln}(\mathrm{x}))), \mathrm{add}(\mathrm{ln}(\mathrm{x}), \mathtt{1}))\right) \lor \mathrm{ans}(\mathit{Y}) \)
cnf_transformation [ 1 ]
9
plain
\( \mathrm{mul}(\mathit{X}, \mathrm{div}(\mathtt{1}, \mathit{X})) = \mathtt{1} \)
cnf_transformation [ 2 ]
10
plain
\( \mathrm{d}(\mathrm{ln}(\mathit{X}), \mathit{X}) = \mathrm{div}(\mathtt{1}, \mathit{X}) \)
cnf_transformation [ 3 ]
11
plain
\( \mathrm{mul}(\mathit{V9}, \mathrm{d}(\mathrm{ln}(\mathit{V9}), \mathit{V9})) = \mathtt{1} \)
demodulation [ 9, 10 ]
12
plain
\( \mathrm{d}(\mathit{X}, \mathit{X}) = \mathtt{1} \)
cnf_transformation [ 4 ]
13
plain
\( \mathrm{d}(\mathrm{mul}(\mathit{U}, \mathit{V}), \mathit{X}) = \mathrm{add}(\mathrm{mul}(\mathrm{d}(\mathit{U}, \mathit{X}), \mathit{V}), \mathrm{mul}(\mathit{U}, \mathrm{d}(\mathit{V}, \mathit{X}))) \)
cnf_transformation [ 5 ]
14
plain
\( \mathrm{d}(\mathrm{mul}(\mathit{V17}, \mathit{V18}), \mathit{V17}) = \mathrm{add}(\mathrm{mul}(\mathtt{1}, \mathit{V18}), \mathrm{mul}(\mathit{V17}, \mathrm{d}(\mathit{V18}, \mathit{V17}))) \)
superposition [ 12, 13 ]
15
plain
\( \mathrm{mul}(\mathtt{1}, \mathit{X}) = \mathit{X} \)
cnf_transformation [ 6 ]
16
plain
\( \mathrm{d}(\mathrm{mul}(\mathit{V17}, \mathit{V18}), \mathit{V17}) = \mathrm{add}(\mathit{V18}, \mathrm{mul}(\mathit{V17}, \mathrm{d}(\mathit{V18}, \mathit{V17}))) \)
demodulation [ 14, 15 ]
17
plain
\( \mathrm{d}(\mathrm{mul}(\mathit{V35}, \mathrm{ln}(\mathit{V35})), \mathit{V35}) = \mathrm{add}(\mathrm{ln}(\mathit{V35}), \mathtt{1}) \)
superposition [ 11, 16 ]
18
plain
\( \mathrm{d}(\mathrm{exp}(\mathit{U}), \mathit{X}) = \mathrm{mul}(\mathrm{exp}(\mathit{U}), \mathrm{d}(\mathit{U}, \mathit{X})) \)
cnf_transformation [ 7 ]
19
plain
\( \mathrm{d}(\mathrm{exp}(\mathrm{mul}(\mathit{V39}, \mathrm{ln}(\mathit{V39}))), \mathit{V39}) = \mathrm{mul}(\mathrm{exp}(\mathrm{mul}(\mathit{V39}, \mathrm{ln}(\mathit{V39}))), \mathrm{add}(\mathrm{ln}(\mathit{V39}), \mathtt{1})) \)
superposition [ 17, 18 ]
20
plain
\( \neg \left(\mathrm{d}(\mathit{V131}, \mathrm{x}) = \mathrm{d}(\mathrm{exp}(\mathrm{mul}(\mathrm{x}, \mathrm{ln}(\mathrm{x}))), \mathrm{x})\right) \lor \mathrm{ans}(\mathit{V131}) \)
demodulation [ 8, 19 ]
21
plain
\( \mathrm{ans}(\mathrm{exp}(\mathrm{mul}(\mathrm{x}, \mathrm{ln}(\mathrm{x})))) \)
equality_resolution [ 20 ]