Beginning of Section Random3
Variable r : set → set → prop
Variable g : set → set → set
Variable q : set → prop
Variable p : set → prop
Variable f : set → set
Variable z y x : set
Theorem. (conj_Random3_TMEtp1VLyohnxRuiPH7w63QqjFycGR1pE99)
∃X8 : set, (((g y x = g (f X8) (g (f (f y)) y)) ∧ p (g (g (g y y) (f X8)) (g z (f (f y))))) ∧ (∃X9 : set, (¬ p z)))
In Proofgold the corresponding term root is 7a65f2... and proposition id is ee2847...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMa6U1phXgeiBqPe9iK1tj8z5ktabkEBdBS)
((∃X8 : set, ((((∃X9 : set, ∃X10 : set, ((y = X8) ∧ (X8 = g X10 X10))) ∧ (∃X9 : set, ((y = y) ∧ (z = z)))) ∧ (∀X9 : set, (X8 = X9))) ∧ (y = g X8 X8))) ∧ (∃X8 : set, p (g x (g (g X8 (g (f (f (f z))) (g x (g x y)))) x))))
In Proofgold the corresponding term root is e5603d... and proposition id is c9566b...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMJWwFyh5h8KoFa5YgsGd1KydNMbusMTCE2)
((∀X8 : set, (¬ p (g y z)) → (∃X9 : set, (r (g (g x (f z)) (g x X8)) (f (g y X8)) ∧ p x))) ∧ (∃X8 : set, ∃X9 : set, (q (f (g y z)) ∧ (x = X8))))
In Proofgold the corresponding term root is 5e2324... and proposition id is f7b2cd...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMJ8ZUQ7pMunaUnp4TUhQpZXjMnErNUnrD2)
∃X8 : set, (((∀X9 : set, (∃X10 : set, ((∀X11 : set, ((X11 = X9) ∧ (∃X12 : set, p X11))) ∧ ((¬ p X10) → (g (f X8) x = g X10 y)))) → (x = y)) → (∀X9 : set, (¬ p (g z (f x))))) ∧ (f z = g (f X8) x))
In Proofgold the corresponding term root is 601af4... and proposition id is 7d4e20...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMYL2s7h3gQZ7uPF7PzmQMJXT6Kt2jocTu6)
((∃X8 : set, ((z = f X8) ∧ (∃X9 : set, ((∃X10 : set, ((X9 = X9) ∧ (∀X11 : set, (X9 = X10)))) ∧ ((y = f y) ∧ (∃X10 : set, (x = X9))))))) ∧ ((∃X8 : set, p (f z)) ∧ (¬ r (g (f (f (f x))) x) (f z))))
In Proofgold the corresponding term root is f21911... and proposition id is 1e5772...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMcnbGNrki6kckhfZddLRRizKCdkD4nACLR)
(¬ p (f (g (g y (g (f (g y (f (g y (g (g (f x) x) (g z (g (g (g (f (g x (g (f z) x))) x) (f (g (g x (g y (f (g (f (g z y)) (g (g y (f y)) (g y (f (g x (g (f (g (g x (f (g (g (g (g x (g z z)) y) (g (g (g (g z (g y z)) (g y x)) (g (g z x) x)) (f y))) z))) (g (g (f (g z (g z x))) (f (g (f (g y (g (g (g x (g (g x x) x)) x) z))) (f z)))) (g z (f (g (g (g z (f x)) (g (f x) (g x (g x (g z y))))) (f (g x (g (f y) x))))))))) (g z (g y z))))))))))) (f x)))) x))))))) z)) z))) → r y x
In Proofgold the corresponding term root is c296ea... and proposition id is c618c2...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMPE8oug9tcfYtLwYtbQdk7NeUVqa48do5t)
∃X8 : set, p (g (g x (g x y)) (f (f (g (g (f (g (f (g (g x z) (g (f x) z))) (g y (g z (f y))))) (g y (g z X8))) (f (f x))))))
In Proofgold the corresponding term root is be0a84... and proposition id is cc8959...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMZZmtQ7wu6S8sYc2unMArQRQ272oLocB8Y)
∀X8 : set, (¬ q X8) → (∀X9 : set, (∃X10 : set, ((∀X11 : set, (∀X12 : set, (¬ r X8 (f y)) → (∀X13 : set, p x → (∃X14 : set, (f X13 = X14)))) → (∀X12 : set, (X11 = f y))) ∧ (¬ p y))) → (∀X10 : set, q z → (∀X11 : set, (∃X12 : set, (y = X8)) → (∀X12 : set, p X10))))
In Proofgold the corresponding term root is 2b4040... and proposition id is bfe0d1...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMSDaUtNXxuUd7PRxpdFwQFPPgvvi1s6Y3U)
∃X8 : set, (((X8 = x) → (∀X9 : set, ∀X10 : set, (∀X11 : set, (¬ r X10 X8) → (∃X12 : set, ∃X13 : set, p X8)) → (∀X11 : set, ∀X12 : set, (X10 = X11)))) ∧ ((∃X9 : set, (f z = f (f z))) ∧ (¬ r y X8)))
In Proofgold the corresponding term root is a9d289... and proposition id is 7cc66f...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMNXJS9dMpZjpkEiiFjn1j3Mbo5GP1L8p4Y)
(g (g (g y (f x)) x) x = g (g y (g y (g (f (g x (f (g y y)))) x))) (g (g (g (g x z) (g y (f x))) (g (g z (f y)) z)) (g (f z) (f x))))
In Proofgold the corresponding term root is 10e36b... and proposition id is d91be8...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMEpAzBopztXyV1qjgxBVVuSRHroAKgyYgo)
(¬ r z (g (g z (g (g (f (g x x)) x) (g (g (g (f x) x) x) (g z (g (g x (g x (g (g z x) (g x (g (g (g (g z (g y x)) (g y y)) y) (g z (g (f x) y))))))) y))))) x))
In Proofgold the corresponding term root is 886127... and proposition id is f595f0...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMN6jz5U6xAwrnfFDxpeYhRTwv9NN4ZkSfM)
∃X8 : set, ((g (g (g (g x (g y (f (f (g (f z) (g (g (f (g z X8)) x) X8)))))) (g X8 x)) z) z = f (g (g (g y y) (f y)) (f (f (g (g y (g y y)) x))))) ∧ (∃X9 : set, p z))
In Proofgold the corresponding term root is 371bcb... and proposition id is 6d3860...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMbjYSHeJ5Y6qCdLrPaUX7hLz2u8zJWZhyz)
(¬ p z) → (∀X8 : set, (g y (g (f (g (f (g (g (g (g (g y z) (f y)) (f (g (g x (g X8 z)) y))) (g (g x (g y x)) X8)) y)) (f (g x (g (f (g (g (f z) (g (g x z) (f (g (f x) (g (f (g (f y) X8)) y))))) (f (f z)))) (g (g x x) (f X8))))))) x) = g (g (f x) (f x)) y))
In Proofgold the corresponding term root is 06cf05... and proposition id is 5e6c81...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMdBrwQbYrtDWfJByTQUhbfd7AXLurf7pEj)
(x = g (g (g (f (g (g (g (g x (g (g z (g (f (g (g (g x y) x) x)) y)) y)) x) (g z (g (g (g (g y y) z) (g (f x) (g (g (g (g x x) z) x) (g z y)))) (g (g z (g (g x z) (f (g y (g (g z (g (g (g x (g (g z y) (f y))) (g x x)) z)) x))))) z)))) x)) (g y (f (g z (g z (g (g (g (g (g (g (g y (f x)) (f (g (g (f (g z z)) z) (g (g x (g x (f (g x (f (g x x)))))) (g y y))))) x) (f y)) x) y) x)))))) y) (g (g (g (g y z) (g (g z (g (g (g (g z y) (g x x)) (f (g y (g z x)))) y)) y)) (f (g (g z z) y))) x))
In Proofgold the corresponding term root is 8c8b97... and proposition id is 064368...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMGhyoUTArnaR6tphsTN1TYRyaZuozAVkGT)
∃X8 : set, ((f (f (g (g y (g X8 (g z y))) (f (g z (g z (f (g (g (g (g x (g x (f z))) (g x (f (g y y)))) z) x))))))) = f X8) ∧ ((∀X9 : set, (¬ q z)) → p X8))
In Proofgold the corresponding term root is 1886f1... and proposition id is 34a10f...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMTeVHF2tVDGmurSGa7uQc2UQ5ESU1Jf4X3)
(((∃X8 : set, ((∀X9 : set, p y) ∧ (∃X9 : set, p y))) → (∀X8 : set, ∀X9 : set, (¬ r z X9))) ∧ (∃X8 : set, ((∀X9 : set, ∀X10 : set, ((∀X11 : set, (z = g X9 X8)) → (z = x)) → (f y = x)) ∧ (f z = g X8 y))))
In Proofgold the corresponding term root is 960496... and proposition id is 695ec3...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMHd7jJSY7yc4ARGe2HU1GjTTYyhHQTv6MG)
(((¬ q (g (f y) (g (g (g x z) x) x))) → r (f y) y) ∧ (∀X8 : set, ∃X9 : set, ((g x (f (f X8)) = g x y) ∧ ((¬ p (f X8)) ∧ (X8 = g (f (f z)) z)))))
In Proofgold the corresponding term root is bf37ea... and proposition id is cc43c3...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMZvbB92gisLoEQS4hfG4DJE8zvNAxvRcZC)
(g (g (g y (g (g z (f (g (g x (g (g z x) x)) z))) (g (f x) (g (g (f y) (g z (g (g (g (g y z) x) (g y x)) (f (g (g x (g y y)) x))))) (f z))))) (g (g (g (g y (f x)) x) (g y x)) z)) y = y)
In Proofgold the corresponding term root is 608265... and proposition id is 95e740...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMFpkPiiGtNTvSkwkqZRXrNKYBx8VERfqiD)
(∀X8 : set, p (g (g X8 (g (f (f (f X8))) (f (g (f x) (f z))))) z)) → ((∀X8 : set, ∀X9 : set, ((∀X10 : set, (X8 = X8)) → (¬ r y X8)) → (∃X10 : set, ∃X11 : set, ((¬ r y X9) ∧ (x = X11)))) ∧ (g x (g (g (g z y) y) (f y)) = g (g z (g x y)) x))
In Proofgold the corresponding term root is 779ec8... and proposition id is 3910a3...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMS6oUhuPXaQfr4KnPhWtt5rc2J3bxEqgQy)
p (g x (g (f (g (g z (g (g (g (g (g y (f (f (g y (g z (g z (g z (f (g (g y (g y (g (f (g x (g (g x x) (g (f x) (g (g z (g (g z z) y)) (g y x)))))) (g (g z (g z (g (g (g x (g (f x) (g (g (g (g (g (g x y) (g x (f y))) z) (f (f (g y z)))) y) (g (f (f x)) (g x y))))) (g y (g y x))) (f (g (f z) y))))) y)))) y))))))))) x) (g x y)) x) y)) y)) y)) → (∃X8 : set, (X8 = X8) → (∃X9 : set, ((∃X10 : set, ((∀X11 : set, (g z X9 = X11) → q (g (g X10 X11) X11)) ∧ (g z X8 = y))) ∧ (x = x))))
In Proofgold the corresponding term root is 49f006... and proposition id is 50be8b...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMKygq7bLv7vXb4qz3c7Ds7zyWYD4RFoLvn)
(g (g (g (g (g (g (g z (g (g (g y z) z) (f (g (g (g (g y y) (f x)) (g (f (g (g (g (g (g (g x (g z (f (g (f (g y (g x z))) (f (g y y)))))) (g (g (g y (g x (g (f z) z))) (g z (g z x))) (g (g z z) (g (g (f x) y) (f (f x)))))) (g z (g (g x (f (g (f x) x))) (g z (g z (g y y)))))) z) (g (f z) z)) (g (g (g x (g x (g x (g (f z) (g (f (g y z)) (g (g y (g (f (g (f (g (g (g x (g (g y (g (g (g (g (g (g (f z) (g x (g (g (f y) y) y))) (g y (g (f (g z (f (g (f x) (g (g z y) z))))) (g (g (g y y) (f (g (g (g x (g x (g (g z (g (f (g (g (g (g (f z) x) y) (g z y)) y)) (g y (g (g (g (g (g z (g (g y (f (g y y))) (g (f (g (g y x) x)) (f (g (g (f (g (g y x) z)) (g (g z y) (g (g (g y (f y)) (g (g (g (f (g (g (g z (f x)) x) (g (f (g z (f x))) x))) (g (g (g (g y (g z (g (g (g (g (g x z) x) z) y) (g (g (g z (g x (g x (f x)))) (f (g z (g (f x) z)))) x)))) (f (f x))) x) (g (g (f x) y) z))) (g (g (g (g (g (f x) (g (g (g (g z (g (f (g (f y) (g x (g (g y y) (g (g (g (g y x) (f z)) z) y))))) z)) (g (g (g z (f y)) z) (g x (g x (g z x))))) (g (f y) x)) y)) z) (g (g (g (g (g x z) y) (g x x)) x) x)) (f z)) (f (g (f (g (f y) (g (g (g y y) (f y)) (g (g x (g y x)) z)))) z)))) (f (f (f (f x)))))) z))) x))))) (f y)) y) (g (g (g x z) x) (g (g (g z (g (g (g (g (g (g x (g (g y x) x)) (f (g (f z) (g (f (g x x)) y)))) (g (g y (f (g (g (g (g (f z) x) (g (g (g (g x x) (g (f x) z)) z) (g z (f (g (g (g z z) (f (f x))) z))))) z) x))) z)) (g (g (g (g (g (f (f y)) z) z) z) z) (g x (g (g x x) x)))) y) y)) z) z))) z)))) (g (f x) y)))) y) (g z (f (f z)))))) z)))) z) (g (f x) y)) y) (g (f z) z))) (g (g (g (g (g (f (f x)) (f z)) y) y) y) (g (f x) x)))) (f y)) (g (g (g z (f (g (g x x) x))) (g (g (g (g (g x y) (g (g (g z (g (g (g (g (g z (g (g (f (f (g (g x (g y y)) y))) y) (g (f y) y))) (g (f z) (g x (g x (g (g y x) y))))) (g y y)) y) z)) y) (g z y))) (g z x)) (g z (g y y))) (g (g y (g (g y x) (g z (f (g z (g (g (g (f (g (f z) (g (g y (g (g x (f (g (g (g (g z (g (g (g y y) (g (g (g (f (f (g (g (g (g (g (g (f (g y (f (f x)))) x) y) x) (g y z)) y) (g (g (f (g y x)) y) (f z))))) z) (g z (f (f (g x (f x)))))) (f (g (f (g (f y) x)) z)))) y)) (g z (g (g z (g y x)) (g y z)))) z) x))) z)) z))) y) y) (f (g x y)))))))) z))) z))) x)) (g z y))) (f y))))))) (g z (f x))) y))) (g x (f (f (g x (g (g (g (g x z) (g z (f x))) (f x)) y))))))) (g z x))))) (g x z)) (g z z)) y) z) (g (f x) (g (f x) (g y (g y (g (g x (g x (g x x))) (g (g y z) x))))))) y = g (f (g (g (g y (g (g z (g y y)) x)) (g (g (g y z) (g x z)) (f (f (f (g (g (g z z) z) (g (f y) z))))))) y)) z)
In Proofgold the corresponding term root is db394d... and proposition id is 4f5036...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMSjxA34VFr7MyeetZC3ta1mX1oEqVGErVi)
(p (g (g z x) x) ∧ (q x ∧ (∀X8 : set, ((∃X9 : set, p z) ∧ ((∃X9 : set, ∀X10 : set, (g (f x) X10 = z)) → (∃X9 : set, ((X8 = g z x) ∧ (z = X8))))))))
In Proofgold the corresponding term root is 5660cc... and proposition id is 052a68...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMG9avq1D9bwPBkS4EVvye4oKCLTHf1rB4y)
∃X8 : set, ((∃X9 : set, ((∃X10 : set, (((((∀X11 : set, (∃X12 : set, ∀X13 : set, (z = z) → (X9 = X13)) → (¬ p (g X11 (g (g y X10) z)))) ∧ (X10 = X10)) → p X9) ∧ ((∃X11 : set, ((∃X12 : set, (X12 = f X12)) ∧ ((∃X12 : set, ∃X13 : set, (X9 = X9)) → p X9))) → (∀X11 : set, q X10))) ∧ ((∀X11 : set, (¬ q y) → (∃X12 : set, (X11 = X10))) ∧ (∀X11 : set, (g (g z (g (g X8 y) (g X8 X8))) X10 = g X11 (f X8)) → (∃X12 : set, ∃X13 : set, ((x = X13) ∧ (∃X14 : set, r X11 X10))))))) ∧ (∀X10 : set, ∃X11 : set, ∀X12 : set, (∀X13 : set, ∀X14 : set, (∃X15 : set, ∃X16 : set, ((¬ p X14) ∧ (∀X17 : set, ∃X18 : set, ∀X19 : set, (X19 = g X16 X13) → p X17))) → ((X12 = z) ∧ (x = X12))) → (X11 = x)))) ∧ p X8)
In Proofgold the corresponding term root is a08aec... and proposition id is efc143...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMXy5q4i2By4zoZuWZRKtzAQpXNaqfMcN6B)
∀X8 : set, (∃X9 : set, ((∃X10 : set, (q (g X10 X10) ∧ (¬ q X9))) ∧ ((z = X9) → (∀X10 : set, p X9) → p X9))) → ((∀X9 : set, (X9 = g (g (f z) z) y)) ∧ (z = z))
In Proofgold the corresponding term root is 946f6e... and proposition id is 71cb17...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMZeV4brMBitny5Fed6CW92EZpTmu3vm1er)
(g z (g y (f (g (g (g y (g x (g z z))) (g (g (f (g (g (f (g (g (f (g (g z z) (g (f y) (f (f (f (g y (g (f (f (g (f (g y z)) (f (g z (g z (g (f (g (g x x) y)) x))))))) y)))))))) z) y)) (g x y)) x)) z) z)) z))) = f z)
In Proofgold the corresponding term root is 7fe4e2... and proposition id is 5dd2cd...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMGNhMxnmLV7JQRp3Xzuui47LpxPqXb78Lx)
∀X8 : set, r (g (g (g y x) (f X8)) (f z)) y → (∃X9 : set, ((∀X10 : set, (r X8 X8 ∧ (z = g x z))) ∧ p X9) → (¬ p y))
In Proofgold the corresponding term root is f9b251... and proposition id is bdada8...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMZg8zv1z3PDU9eatZec54dva9ip3pXvQLq)
(g (g (g x z) (g (g (g (g x (g (g (g z (f x)) (g (g x z) (g (g z x) z))) (g x z))) (g (g y (f x)) y)) y) z)) y = g x (g (g (g x (g (g (g z z) y) (g (f x) (g (f (f y)) (g (g (f y) x) y))))) (f (f x))) x))
In Proofgold the corresponding term root is 4be20f... and proposition id is 284fa8...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMQSshG5bFcr7hHdxH3kKGNcLyavvJXXRVb)
(∃X8 : set, ((f (f (f z)) = f X8) ∧ (((∃X9 : set, q X8) → ((∃X9 : set, ∀X10 : set, ∀X11 : set, (X10 = x)) ∧ ((z = f (f (f X8))) ∧ (∀X9 : set, (∃X10 : set, (X9 = z)) → (∃X10 : set, ∃X11 : set, (((∃X12 : set, (X9 = X11)) → (∃X12 : set, (¬ p (f X8)))) → (∀X12 : set, q (f X12) → ((∀X13 : set, ∃X14 : set, (((∀X15 : set, r (f X15) X10) → (X10 = X11)) ∧ (X13 = X12))) ∧ r (f (g X8 (f (f z)))) X11))) → (∀X12 : set, p X8 → (r (g (g (f (f (g X10 X11))) X12) X9) X12 ∧ (¬ p (f X11))))))))) ∧ (¬ p z)))) → (∃X8 : set, ∃X9 : set, ((¬ r z (g X9 (g x x))) ∧ (¬ r X9 (f z))))
In Proofgold the corresponding term root is 4b7d81... and proposition id is c8ed3f...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMHW9ua2hM8KncpauUcnc4o97jBQjYjxWHK)
∀X8 : set, (∃X9 : set, (¬ p z)) → ((∃X9 : set, ((g (f (f (g X8 X8))) X8 = x) ∧ (∀X10 : set, ∀X11 : set, ∃X12 : set, (y = y) → p (g y z)))) ∧ (g (g x (f z)) x = z))
In Proofgold the corresponding term root is 970886... and proposition id is f9a04c...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMc1vFsBW2q2tkgZpoQPvvbYGKCnRFwJuSj)
(y = g (g z (g (g x (g y (g x x))) (g (g (g y z) (f (g z x))) y))) (g (g y (g z (g y (g (g x x) (g y (f (f (g x x)))))))) y))
In Proofgold the corresponding term root is 3c6fab... and proposition id is af1aeb...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMW9aCVNpMoijkzmBu8fV77B9DR4HfkezNP)
((∃X8 : set, ∀X9 : set, (f y = z) → (∀X10 : set, ∀X11 : set, (∀X12 : set, (X11 = g X10 X12)) → (∃X12 : set, ((X9 = f X11) ∧ (f (g X12 X8) = f x))))) ∧ (¬ p z)) → p (g x z)
In Proofgold the corresponding term root is ab532d... and proposition id is 21e5e4...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMZd5bJzozKeWUzxvDSmNoRFyxdxoBpetNT)
∀X8 : set, ∀X9 : set, ∀X10 : set, (∀X11 : set, (∀X12 : set, (z = f y) → p (f (f X9))) → (¬ p (g (g (g X10 (g X8 X10)) X8) X9))) → (∃X11 : set, q y)
In Proofgold the corresponding term root is 4a5307... and proposition id is c4753c...
Proof:
The rest of this subproof is missing.
∎
Theorem. (conj_Random3_TMRhMmLVnJANDQLiXyjrRh7bfYmqnMkBKRE)
∃X8 : set, (((∃X9 : set, ∀X10 : set, (∃X11 : set, ((∀X12 : set, (p X9 ∧ (∃X13 : set, (¬ q X10))) → p (g X11 X9)) ∧ p X11)) → (∃X11 : set, ((∀X12 : set, ∃X13 : set, ∃X14 : set, ((∀X15 : set, ((∃X16 : set, ∀X17 : set, (z = X14)) ∧ (¬ p y)) → (¬ r X10 (f X12)) → (X15 = X14)) ∧ (∃X15 : set, ((∀X16 : set, (∃X17 : set, (((X16 = X15) → (¬ q X8)) ∧ (X14 = X14))) → (∀X17 : set, (∃X18 : set, ∃X19 : set, ((∀X20 : set, (X10 = X19) → (∃X21 : set, q X11)) ∧ (∃X20 : set, (X16 = x) → p X17 → (∃X21 : set, (X20 = X15) → (∀X22 : set, ∀X23 : set, ((X22 = X23) ∧ (∃X24 : set, ((X21 = X23) ∧ ((¬ p X24) ∧ (∃X25 : set, (r X18 X14 ∧ (X18 = X22))))))) → (∀X24 : set, (¬ r X21 X23))))))) → q X17)) ∧ (X14 = X8))))) ∧ (X8 = z)))) → (p (f (f y)) ∧ (g x (g y (f z)) = f x))) ∧ (∃X9 : set, (¬ p y)))
In Proofgold the corresponding term root is 437232... and proposition id is 4955ed...
Proof:
The rest of this subproof is missing.
∎
End of Section Random3