%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LCL636+1.005 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:32:29 PM UTC 2026 % Result : Theorem 83.13s 83.47s % Output : Proof 83.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : LCL636+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.02 % Command : run_zenon %s %d % 0.03/0.29 % Computer : n012.cluster.edu % 0.03/0.29 % Model : x86_64 x86_64 % 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.03/0.29 % Memory : 8046.5625MB % 0.03/0.29 % OS : Linux 6.8.0-71-generic % 0.03/0.29 % CPULimit : 300 % 0.03/0.29 % WCLimit : 300 % 0.03/0.29 % DateTime : Sat Sep 5 16:10:12 UTC 2026 % 0.03/0.29 % CPUTime : % 83.13/83.47 (* PROOF-FOUND *) % 83.13/83.47 % SZS status Theorem % 83.13/83.47 (* BEGIN-PROOF *) % 83.13/83.47 % SZS output start Proof % 83.13/83.47 Theorem main : (~(exists X : zenon_U, (~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y)))))))))))))))))))))))))))))/\((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X)))))))))))))))))))))))))))/\((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y)))))))))))))))))))))))))/\((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X)))))))))))))))))))))))/\((forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y)))))))))))))))))))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\(((p100 X)\/(~(p101 X)))/\((~(p101 X))/\(p100 X))))))))))))))))))))))))))))). % 83.13/83.47 Proof. % 83.13/83.47 assert (zenon_L1_ : forall (zenon_TX_e : zenon_U) (zenon_TX_f : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_f Y))\/(p3 Y))) -> (r1 zenon_TX_f zenon_TX_e) -> (~(p3 zenon_TX_e)) -> False). % 83.13/83.47 do 2 intro. intros zenon_H1 zenon_H2 zenon_H3. % 83.13/83.47 generalize (zenon_H1 zenon_TX_e). zenon_intro zenon_H6. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H6); [ zenon_intro zenon_H8 | zenon_intro zenon_H7 ]. % 83.13/83.47 exact (zenon_H8 zenon_H2). % 83.13/83.47 exact (zenon_H3 zenon_H7). % 83.13/83.47 (* end of lemma zenon_L1_ *) % 83.13/83.47 assert (zenon_L2_ : forall (zenon_TX_e : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))) -> (r1 zenon_TX_l zenon_TX_f) -> (r1 zenon_TX_f zenon_TX_e) -> (~(p3 zenon_TX_e)) -> False). % 83.13/83.47 do 3 intro. intros zenon_H9 zenon_Ha zenon_H2 zenon_H3. % 83.13/83.47 generalize (zenon_H9 zenon_TX_f). zenon_intro zenon_Hc. % 83.13/83.47 apply (zenon_or_s _ _ zenon_Hc); [ zenon_intro zenon_Hd | zenon_intro zenon_H1 ]. % 83.13/83.47 exact (zenon_Hd zenon_Ha). % 83.13/83.47 apply (zenon_L1_ zenon_TX_e zenon_TX_f); trivial. % 83.13/83.47 (* end of lemma zenon_L2_ *) % 83.13/83.47 assert (zenon_L3_ : forall (zenon_TX_e : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_q Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_f) -> (r1 zenon_TX_f zenon_TX_e) -> (~(p3 zenon_TX_e)) -> False). % 83.13/83.47 do 4 intro. intros zenon_He zenon_Hf zenon_Ha zenon_H2 zenon_H3. % 83.13/83.47 generalize (zenon_He zenon_TX_l). zenon_intro zenon_H11. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H11); [ zenon_intro zenon_H12 | zenon_intro zenon_H9 ]. % 83.13/83.47 exact (zenon_H12 zenon_Hf). % 83.13/83.47 apply (zenon_L2_ zenon_TX_e zenon_TX_f zenon_TX_l); trivial. % 83.13/83.47 (* end of lemma zenon_L3_ *) % 83.13/83.47 assert (zenon_L4_ : forall (zenon_TX_e : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U) (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_f) -> (r1 zenon_TX_f zenon_TX_e) -> (~(p3 zenon_TX_e)) -> False). % 83.13/83.47 do 6 intro. intros zenon_H13 zenon_H14 zenon_H15 zenon_Hf zenon_Ha zenon_H2 zenon_H3. % 83.13/83.47 generalize (zenon_H13 zenon_TY_w). zenon_intro zenon_H18. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H18); [ zenon_intro zenon_H1a | zenon_intro zenon_H19 ]. % 83.13/83.47 exact (zenon_H1a zenon_H14). % 83.13/83.47 generalize (zenon_H19 zenon_TX_q). zenon_intro zenon_H1b. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H1b); [ zenon_intro zenon_H1c | zenon_intro zenon_He ]. % 83.13/83.47 exact (zenon_H1c zenon_H15). % 83.13/83.47 apply (zenon_L3_ zenon_TX_e zenon_TX_f zenon_TX_l zenon_TX_q); trivial. % 83.13/83.47 (* end of lemma zenon_L4_ *) % 83.13/83.47 assert (zenon_L5_ : forall (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U) (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_e : zenon_U) (zenon_TX_f : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p3 X))\/(~(p102 X))))) -> (r1 zenon_TX_f zenon_TX_e) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_f) -> (p102 zenon_TX_e) -> False). % 83.13/83.47 do 6 intro. intros zenon_H1d zenon_H2 zenon_H13 zenon_H14 zenon_H15 zenon_Hf zenon_Ha zenon_H1e. % 83.13/83.47 generalize (zenon_H1d zenon_TX_e). zenon_intro zenon_H1f. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H1f); [ zenon_intro zenon_H8 | zenon_intro zenon_H20 ]. % 83.13/83.47 exact (zenon_H8 zenon_H2). % 83.13/83.47 apply (zenon_or_s _ _ zenon_H20); [ zenon_intro zenon_H3 | zenon_intro zenon_H21 ]. % 83.13/83.47 apply (zenon_L4_ zenon_TX_e zenon_TX_f zenon_TX_l zenon_TX_q zenon_TY_w zenon_TX_x); trivial. % 83.13/83.47 exact (zenon_H21 zenon_H1e). % 83.13/83.47 (* end of lemma zenon_L5_ *) % 83.13/83.47 assert (zenon_L6_ : forall (zenon_TX_x : zenon_U) (zenon_TY_w : zenon_U) (zenon_TX_q : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_e : zenon_U), ((p102 zenon_TX_e)\/(~(p103 zenon_TX_e))) -> (p103 zenon_TX_e) -> (r1 zenon_TX_l zenon_TX_f) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_x zenon_TY_w) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_f zenon_TX_e) -> (forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p3 X))\/(~(p102 X))))) -> False). % 83.13/83.47 do 6 intro. intros zenon_H22 zenon_H23 zenon_Ha zenon_Hf zenon_H15 zenon_H14 zenon_H13 zenon_H2 zenon_H1d. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H22); [ zenon_intro zenon_H1e | zenon_intro zenon_H24 ]. % 83.13/83.47 apply (zenon_L5_ zenon_TX_l zenon_TX_q zenon_TY_w zenon_TX_x zenon_TX_e zenon_TX_f); trivial. % 83.13/83.47 exact (zenon_H24 zenon_H23). % 83.13/83.47 (* end of lemma zenon_L6_ *) % 83.13/83.47 assert (zenon_L7_ : forall (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U) (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_e : zenon_U), ((p103 zenon_TX_e)\/(~(p104 zenon_TX_e))) -> (p104 zenon_TX_e) -> (forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p3 X))\/(~(p102 X))))) -> (r1 zenon_TX_f zenon_TX_e) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_f) -> ((p102 zenon_TX_e)\/(~(p103 zenon_TX_e))) -> False). % 83.13/83.47 do 6 intro. intros zenon_H25 zenon_H26 zenon_H1d zenon_H2 zenon_H13 zenon_H14 zenon_H15 zenon_Hf zenon_Ha zenon_H22. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H25); [ zenon_intro zenon_H23 | zenon_intro zenon_H27 ]. % 83.13/83.47 apply (zenon_L6_ zenon_TX_x zenon_TY_w zenon_TX_q zenon_TX_f zenon_TX_l zenon_TX_e); trivial. % 83.13/83.47 exact (zenon_H27 zenon_H26). % 83.13/83.47 (* end of lemma zenon_L7_ *) % 83.13/83.47 assert (zenon_L8_ : forall (zenon_TX_x : zenon_U) (zenon_TY_w : zenon_U) (zenon_TX_q : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_e : zenon_U), ((((~(forall X : zenon_U, ((~(r1 zenon_TX_e X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_e X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 zenon_TX_e))/\(p104 zenon_TX_e))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_e X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_e X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 zenon_TX_e))/\(p103 zenon_TX_e))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_e X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_e X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 zenon_TX_e))/\(p102 zenon_TX_e))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_e X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_e X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 zenon_TX_e))/\(p101 zenon_TX_e))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_e X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_e X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 zenon_TX_e))/\(p100 zenon_TX_e))))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 zenon_TX_e))/\((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 zenon_TX_e))))\/(~(p105 zenon_TX_e)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 zenon_TX_e))/\((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 zenon_TX_e))))\/(~(p104 zenon_TX_e)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 zenon_TX_e))/\((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 zenon_TX_e))))\/(~(p103 zenon_TX_e)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 zenon_TX_e))/\((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 zenon_TX_e))))\/(~(p102 zenon_TX_e)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 zenon_TX_e))/\((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 zenon_TX_e))))\/(~(p101 zenon_TX_e)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 zenon_TX_e))/\((forall X : zenon_U, ((~(r1 zenon_TX_e X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 zenon_TX_e))))\/(~(p100 zenon_TX_e)))/\(((p105 zenon_TX_e)\/(~(p106 zenon_TX_e)))/\(((p104 zenon_TX_e)\/(~(p105 zenon_TX_e)))/\(((p103 zenon_TX_e)\/(~(p104 zenon_TX_e)))/\(((p102 zenon_TX_e)\/(~(p103 zenon_TX_e)))/\(((p101 zenon_TX_e)\/(~(p102 zenon_TX_e)))/\((p100 zenon_TX_e)\/(~(p101 zenon_TX_e))))))))))))))))))) -> (p105 zenon_TX_e) -> (r1 zenon_TX_l zenon_TX_f) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_x zenon_TY_w) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_f zenon_TX_e) -> (forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p3 X))\/(~(p102 X))))) -> False). % 83.13/83.47 do 6 intro. intros zenon_H28 zenon_H29 zenon_Ha zenon_Hf zenon_H15 zenon_H14 zenon_H13 zenon_H2 zenon_H1d. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H28). zenon_intro zenon_H2b. zenon_intro zenon_H2a. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H2a). zenon_intro zenon_H2d. zenon_intro zenon_H2c. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H2c). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H31. zenon_intro zenon_H30. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H30). zenon_intro zenon_H33. zenon_intro zenon_H32. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H32). zenon_intro zenon_H35. zenon_intro zenon_H34. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H34). zenon_intro zenon_H37. zenon_intro zenon_H36. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H39. zenon_intro zenon_H38. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H38). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H3a). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H3c). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H40). zenon_intro zenon_H43. zenon_intro zenon_H42. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H42). zenon_intro zenon_H25. zenon_intro zenon_H44. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H44). zenon_intro zenon_H22. zenon_intro zenon_H45. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H43); [ zenon_intro zenon_H26 | zenon_intro zenon_H46 ]. % 83.13/83.47 apply (zenon_L7_ zenon_TX_l zenon_TX_q zenon_TY_w zenon_TX_x zenon_TX_f zenon_TX_e); trivial. % 83.13/83.47 exact (zenon_H46 zenon_H29). % 83.13/83.47 (* end of lemma zenon_L8_ *) % 83.13/83.47 assert (zenon_L9_ : forall (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U) (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_e : zenon_U) (zenon_TX_f : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X))))))))))))))))))))) -> (r1 zenon_TX_f zenon_TX_e) -> (forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p3 X))\/(~(p102 X))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_f) -> (p105 zenon_TX_e) -> False). % 83.13/83.47 do 6 intro. intros zenon_H47 zenon_H2 zenon_H1d zenon_H13 zenon_H14 zenon_H15 zenon_Hf zenon_Ha zenon_H29. % 83.13/83.47 generalize (zenon_H47 zenon_TX_e). zenon_intro zenon_H48. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H48); [ zenon_intro zenon_H8 | zenon_intro zenon_H28 ]. % 83.13/83.47 exact (zenon_H8 zenon_H2). % 83.13/83.47 apply (zenon_L8_ zenon_TX_x zenon_TY_w zenon_TX_q zenon_TX_f zenon_TX_l zenon_TX_e); trivial. % 83.13/83.47 (* end of lemma zenon_L9_ *) % 83.13/83.47 assert (zenon_L10_ : forall (zenon_TX_q : zenon_U) (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_e : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))) -> (r1 zenon_TX_l zenon_TX_f) -> (r1 zenon_TX_f zenon_TX_e) -> (forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p3 X))\/(~(p102 X))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_q zenon_TX_l) -> (p105 zenon_TX_e) -> False). % 83.13/83.47 do 6 intro. intros zenon_H49 zenon_Ha zenon_H2 zenon_H1d zenon_H13 zenon_H14 zenon_H15 zenon_Hf zenon_H29. % 83.13/83.47 generalize (zenon_H49 zenon_TX_f). zenon_intro zenon_H4a. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H4a); [ zenon_intro zenon_Hd | zenon_intro zenon_H47 ]. % 83.13/83.47 exact (zenon_Hd zenon_Ha). % 83.13/83.47 apply (zenon_L9_ zenon_TX_l zenon_TX_q zenon_TY_w zenon_TX_x zenon_TX_e zenon_TX_f); trivial. % 83.13/83.47 (* end of lemma zenon_L10_ *) % 83.13/83.47 assert (zenon_L11_ : forall (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_e : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X))))))))))))))))))))))))) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_f) -> (r1 zenon_TX_f zenon_TX_e) -> (forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p3 X))\/(~(p102 X))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (r1 zenon_TY_w zenon_TX_q) -> (p105 zenon_TX_e) -> False). % 83.13/83.47 do 6 intro. intros zenon_H4b zenon_Hf zenon_Ha zenon_H2 zenon_H1d zenon_H13 zenon_H14 zenon_H15 zenon_H29. % 83.13/83.47 generalize (zenon_H4b zenon_TX_l). zenon_intro zenon_H4c. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H4c); [ zenon_intro zenon_H12 | zenon_intro zenon_H49 ]. % 83.13/83.47 exact (zenon_H12 zenon_Hf). % 83.13/83.47 apply (zenon_L10_ zenon_TX_q zenon_TY_w zenon_TX_x zenon_TX_e zenon_TX_f zenon_TX_l); trivial. % 83.13/83.47 (* end of lemma zenon_L11_ *) % 83.13/83.47 assert (zenon_L12_ : forall (zenon_TX_e : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U) (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_f) -> (r1 zenon_TX_f zenon_TX_e) -> (forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p3 X))\/(~(p102 X))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (p105 zenon_TX_e) -> False). % 83.13/83.47 do 6 intro. intros zenon_H4d zenon_H14 zenon_H15 zenon_Hf zenon_Ha zenon_H2 zenon_H1d zenon_H13 zenon_H29. % 83.13/83.47 generalize (zenon_H4d zenon_TY_w). zenon_intro zenon_H4e. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H4e); [ zenon_intro zenon_H1a | zenon_intro zenon_H4f ]. % 83.13/83.47 exact (zenon_H1a zenon_H14). % 83.13/83.47 generalize (zenon_H4f zenon_TX_q). zenon_intro zenon_H50. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H50); [ zenon_intro zenon_H1c | zenon_intro zenon_H4b ]. % 83.13/83.47 exact (zenon_H1c zenon_H15). % 83.13/83.47 apply (zenon_L11_ zenon_TY_w zenon_TX_x zenon_TX_e zenon_TX_f zenon_TX_l zenon_TX_q); trivial. % 83.13/83.47 (* end of lemma zenon_L12_ *) % 83.13/83.47 assert (zenon_L13_ : forall (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p3 X))\/(~(p102 X))))) -> (r1 zenon_TX_l zenon_TX_f) -> (p3 zenon_TX_f) -> (p102 zenon_TX_f) -> False). % 83.13/83.47 do 2 intro. intros zenon_H51 zenon_Ha zenon_H52 zenon_H53. % 83.13/83.47 generalize (zenon_H51 zenon_TX_f). zenon_intro zenon_H54. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H54); [ zenon_intro zenon_Hd | zenon_intro zenon_H55 ]. % 83.13/83.47 exact (zenon_Hd zenon_Ha). % 83.13/83.47 apply (zenon_or_s _ _ zenon_H55); [ zenon_intro zenon_H57 | zenon_intro zenon_H56 ]. % 83.13/83.47 exact (zenon_H57 zenon_H52). % 83.13/83.47 exact (zenon_H56 zenon_H53). % 83.13/83.47 (* end of lemma zenon_L13_ *) % 83.13/83.47 assert (zenon_L14_ : forall (zenon_TY_w : zenon_U) (zenon_TX_q : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_e : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_f : zenon_U), ((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 zenon_TX_f)) -> (forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p3 X))\/(~(p102 X))))) -> (p103 zenon_TX_f) -> ((p102 zenon_TX_f)\/(~(p103 zenon_TX_f))) -> (p105 zenon_TX_e) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_f zenon_TX_e) -> (r1 zenon_TX_l zenon_TX_f) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_x zenon_TY_w) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> False). % 83.13/83.47 do 6 intro. intros zenon_H58 zenon_H51 zenon_H59 zenon_H5a zenon_H29 zenon_H13 zenon_H2 zenon_Ha zenon_Hf zenon_H15 zenon_H14 zenon_H4d. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H58); [ zenon_intro zenon_H1d | zenon_intro zenon_H52 ]. % 83.13/83.47 apply (zenon_L12_ zenon_TX_e zenon_TX_f zenon_TX_l zenon_TX_q zenon_TY_w zenon_TX_x); trivial. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H5a); [ zenon_intro zenon_H53 | zenon_intro zenon_H5b ]. % 83.13/83.47 apply (zenon_L13_ zenon_TX_f zenon_TX_l); trivial. % 83.13/83.47 exact (zenon_H5b zenon_H59). % 83.13/83.47 (* end of lemma zenon_L14_ *) % 83.13/83.47 assert (zenon_L15_ : forall (zenon_TX_f : zenon_U), ((p102 zenon_TX_f)\/(~(p103 zenon_TX_f))) -> (p103 zenon_TX_f) -> (~(p102 zenon_TX_f)) -> False). % 83.13/83.47 do 1 intro. intros zenon_H5a zenon_H59 zenon_H56. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H5a); [ zenon_intro zenon_H53 | zenon_intro zenon_H5b ]. % 83.13/83.47 exact (zenon_H56 zenon_H53). % 83.13/83.47 exact (zenon_H5b zenon_H59). % 83.13/83.47 (* end of lemma zenon_L15_ *) % 83.13/83.47 assert (zenon_L16_ : forall (zenon_TX_f : zenon_U), ((p103 zenon_TX_f)\/(~(p104 zenon_TX_f))) -> (p104 zenon_TX_f) -> (~(p102 zenon_TX_f)) -> ((p102 zenon_TX_f)\/(~(p103 zenon_TX_f))) -> False). % 83.13/83.47 do 1 intro. intros zenon_H5c zenon_H5d zenon_H56 zenon_H5a. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H5c); [ zenon_intro zenon_H59 | zenon_intro zenon_H5e ]. % 83.13/83.47 apply (zenon_L15_ zenon_TX_f); trivial. % 83.13/83.47 exact (zenon_H5e zenon_H5d). % 83.13/83.47 (* end of lemma zenon_L16_ *) % 83.13/83.47 assert (zenon_L17_ : forall (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U) (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_f : zenon_U), ((((~(forall X : zenon_U, ((~(r1 zenon_TX_f X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_f X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 zenon_TX_f))/\(p104 zenon_TX_f))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_f X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_f X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 zenon_TX_f))/\(p103 zenon_TX_f))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_f X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_f X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 zenon_TX_f))/\(p102 zenon_TX_f))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_f X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_f X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 zenon_TX_f))/\(p101 zenon_TX_f))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_f X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_f X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 zenon_TX_f))/\(p100 zenon_TX_f))))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 zenon_TX_f))/\((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 zenon_TX_f))))\/(~(p105 zenon_TX_f)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 zenon_TX_f))/\((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 zenon_TX_f))))\/(~(p104 zenon_TX_f)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 zenon_TX_f))/\((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 zenon_TX_f))))\/(~(p103 zenon_TX_f)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 zenon_TX_f))/\((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 zenon_TX_f))))\/(~(p102 zenon_TX_f)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 zenon_TX_f))/\((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 zenon_TX_f))))\/(~(p101 zenon_TX_f)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 zenon_TX_f))/\((forall X : zenon_U, ((~(r1 zenon_TX_f X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 zenon_TX_f))))\/(~(p100 zenon_TX_f)))/\(((p105 zenon_TX_f)\/(~(p106 zenon_TX_f)))/\(((p104 zenon_TX_f)\/(~(p105 zenon_TX_f)))/\(((p103 zenon_TX_f)\/(~(p104 zenon_TX_f)))/\(((p102 zenon_TX_f)\/(~(p103 zenon_TX_f)))/\(((p101 zenon_TX_f)\/(~(p102 zenon_TX_f)))/\((p100 zenon_TX_f)\/(~(p101 zenon_TX_f))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_f) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p3 X))\/(~(p102 X))))) -> (~(p105 zenon_TX_f)) -> (p104 zenon_TX_f) -> False). % 83.13/83.47 do 5 intro. intros zenon_H5f zenon_H4d zenon_H14 zenon_H15 zenon_Hf zenon_Ha zenon_H13 zenon_H51 zenon_H60 zenon_H5d. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H5f). zenon_intro zenon_H62. zenon_intro zenon_H61. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H61). zenon_intro zenon_H64. zenon_intro zenon_H63. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H63). zenon_intro zenon_H66. zenon_intro zenon_H65. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H68. zenon_intro zenon_H67. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H67). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H69). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H6b). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H6f). zenon_intro zenon_H72. zenon_intro zenon_H71. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H74. zenon_intro zenon_H73. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H73). zenon_intro zenon_H76. zenon_intro zenon_H75. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H75). zenon_intro zenon_H78. zenon_intro zenon_H77. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H77). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H79). zenon_intro zenon_H5c. zenon_intro zenon_H7b. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H7b). zenon_intro zenon_H5a. zenon_intro zenon_H7c. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H62); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H7e). zenon_intro zenon_H80. zenon_intro zenon_H7f. % 83.13/83.47 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_f X))\/(~((p6 X)/\((~(p106 X))/\(p105 X)))))) zenon_H7f); [ zenon_intro zenon_H81; idtac ]. % 83.13/83.47 elim zenon_H81. zenon_intro zenon_TX_e. zenon_intro zenon_H82. % 83.13/83.47 apply (zenon_notor_s _ _ zenon_H82). zenon_intro zenon_H84. zenon_intro zenon_H83. % 83.13/83.47 apply zenon_H83. zenon_intro zenon_H85. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H85). zenon_intro zenon_H87. zenon_intro zenon_H86. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H86). zenon_intro zenon_H88. zenon_intro zenon_H29. % 83.13/83.47 apply zenon_H84. zenon_intro zenon_H2. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H72); [ zenon_intro zenon_H89 | zenon_intro zenon_H56 ]. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H89). zenon_intro zenon_H58. zenon_intro zenon_H8a. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H5c); [ zenon_intro zenon_H59 | zenon_intro zenon_H5e ]. % 83.13/83.47 apply (zenon_L14_ zenon_TY_w zenon_TX_q zenon_TX_x zenon_TX_e zenon_TX_l zenon_TX_f); trivial. % 83.13/83.47 exact (zenon_H5e zenon_H5d). % 83.13/83.47 apply (zenon_L16_ zenon_TX_f); trivial. % 83.13/83.47 apply (zenon_notand_s _ _ zenon_H7d); [ zenon_intro zenon_H8b | zenon_intro zenon_H5e ]. % 83.13/83.47 exact (zenon_H8b zenon_H60). % 83.13/83.47 exact (zenon_H5e zenon_H5d). % 83.13/83.47 (* end of lemma zenon_L17_ *) % 83.13/83.47 assert (zenon_L18_ : forall (zenon_TY_w : zenon_U) (zenon_TX_q : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X))))))))))))))))))))) -> (r1 zenon_TX_l zenon_TX_f) -> (forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p3 X))\/(~(p102 X))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_x zenon_TY_w) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (p104 zenon_TX_f) -> (~(p105 zenon_TX_f)) -> False). % 83.13/83.47 do 5 intro. intros zenon_H8c zenon_Ha zenon_H51 zenon_H13 zenon_Hf zenon_H15 zenon_H14 zenon_H4d zenon_H5d zenon_H60. % 83.13/83.47 generalize (zenon_H8c zenon_TX_f). zenon_intro zenon_H8d. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H8d); [ zenon_intro zenon_Hd | zenon_intro zenon_H5f ]. % 83.13/83.47 exact (zenon_Hd zenon_Ha). % 83.13/83.47 apply (zenon_L17_ zenon_TX_l zenon_TX_q zenon_TY_w zenon_TX_x zenon_TX_f); trivial. % 83.13/83.47 (* end of lemma zenon_L18_ *) % 83.13/83.47 assert (zenon_L19_ : forall (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_f) -> (forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p3 X))\/(~(p102 X))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_x zenon_TY_w) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (p104 zenon_TX_f) -> (~(p105 zenon_TX_f)) -> False). % 83.13/83.47 do 5 intro. intros zenon_H8e zenon_Hf zenon_Ha zenon_H51 zenon_H13 zenon_H15 zenon_H14 zenon_H4d zenon_H5d zenon_H60. % 83.13/83.47 generalize (zenon_H8e zenon_TX_l). zenon_intro zenon_H8f. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H8f); [ zenon_intro zenon_H12 | zenon_intro zenon_H8c ]. % 83.13/83.47 exact (zenon_H12 zenon_Hf). % 83.13/83.47 apply (zenon_L18_ zenon_TY_w zenon_TX_q zenon_TX_x zenon_TX_f zenon_TX_l); trivial. % 83.13/83.47 (* end of lemma zenon_L19_ *) % 83.13/83.47 assert (zenon_L20_ : forall (zenon_TX_x : zenon_U) (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U) (zenon_TY_w : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TY_w Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_f) -> (forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p3 X))\/(~(p102 X))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (p104 zenon_TX_f) -> (~(p105 zenon_TX_f)) -> False). % 83.13/83.47 do 5 intro. intros zenon_H90 zenon_H15 zenon_Hf zenon_Ha zenon_H51 zenon_H13 zenon_H14 zenon_H4d zenon_H5d zenon_H60. % 83.13/83.47 generalize (zenon_H90 zenon_TX_q). zenon_intro zenon_H91. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H91); [ zenon_intro zenon_H1c | zenon_intro zenon_H8e ]. % 83.13/83.47 exact (zenon_H1c zenon_H15). % 83.13/83.47 apply (zenon_L19_ zenon_TY_w zenon_TX_x zenon_TX_f zenon_TX_l zenon_TX_q); trivial. % 83.13/83.47 (* end of lemma zenon_L20_ *) % 83.13/83.47 assert (zenon_L21_ : forall (zenon_TX_f : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U) (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X))))))))))))))))))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_f) -> (forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p3 X))\/(~(p102 X))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (p104 zenon_TX_f) -> (~(p105 zenon_TX_f)) -> False). % 83.13/83.47 do 5 intro. intros zenon_H92 zenon_H14 zenon_H15 zenon_Hf zenon_Ha zenon_H51 zenon_H13 zenon_H4d zenon_H5d zenon_H60. % 83.13/83.47 generalize (zenon_H92 zenon_TY_w). zenon_intro zenon_H93. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H93); [ zenon_intro zenon_H1a | zenon_intro zenon_H90 ]. % 83.13/83.47 exact (zenon_H1a zenon_H14). % 83.13/83.47 apply (zenon_L20_ zenon_TX_x zenon_TX_f zenon_TX_l zenon_TX_q zenon_TY_w); trivial. % 83.13/83.47 (* end of lemma zenon_L21_ *) % 83.13/83.47 assert (zenon_L22_ : forall (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p3 X))\/(~(p102 X))))) -> (r1 zenon_TX_q zenon_TX_l) -> (p3 zenon_TX_l) -> (p102 zenon_TX_l) -> False). % 83.13/83.47 do 2 intro. intros zenon_H94 zenon_Hf zenon_H95 zenon_H96. % 83.13/83.47 generalize (zenon_H94 zenon_TX_l). zenon_intro zenon_H97. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H97); [ zenon_intro zenon_H12 | zenon_intro zenon_H98 ]. % 83.13/83.47 exact (zenon_H12 zenon_Hf). % 83.13/83.47 apply (zenon_or_s _ _ zenon_H98); [ zenon_intro zenon_H9a | zenon_intro zenon_H99 ]. % 83.13/83.47 exact (zenon_H9a zenon_H95). % 83.13/83.47 exact (zenon_H99 zenon_H96). % 83.13/83.47 (* end of lemma zenon_L22_ *) % 83.13/83.47 assert (zenon_L23_ : forall (zenon_TX_l : zenon_U), ((p102 zenon_TX_l)\/(~(p103 zenon_TX_l))) -> (p103 zenon_TX_l) -> (~(p102 zenon_TX_l)) -> False). % 83.13/83.47 do 1 intro. intros zenon_H9b zenon_H9c zenon_H99. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H9b); [ zenon_intro zenon_H96 | zenon_intro zenon_H9d ]. % 83.13/83.47 exact (zenon_H99 zenon_H96). % 83.13/83.47 exact (zenon_H9d zenon_H9c). % 83.13/83.47 (* end of lemma zenon_L23_ *) % 83.13/83.47 assert (zenon_L24_ : forall (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_q : zenon_U) (zenon_TX_l : zenon_U), ((((~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 zenon_TX_l))/\(p104 zenon_TX_l))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 zenon_TX_l))/\(p103 zenon_TX_l))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 zenon_TX_l))/\(p102 zenon_TX_l))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 zenon_TX_l))/\(p101 zenon_TX_l))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 zenon_TX_l))/\(p100 zenon_TX_l))))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 zenon_TX_l))))\/(~(p105 zenon_TX_l)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 zenon_TX_l))))\/(~(p104 zenon_TX_l)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 zenon_TX_l))))\/(~(p103 zenon_TX_l)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 zenon_TX_l))))\/(~(p102 zenon_TX_l)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 zenon_TX_l))))\/(~(p101 zenon_TX_l)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 zenon_TX_l))))\/(~(p100 zenon_TX_l)))/\(((p105 zenon_TX_l)\/(~(p106 zenon_TX_l)))/\(((p104 zenon_TX_l)\/(~(p105 zenon_TX_l)))/\(((p103 zenon_TX_l)\/(~(p104 zenon_TX_l)))/\(((p102 zenon_TX_l)\/(~(p103 zenon_TX_l)))/\(((p101 zenon_TX_l)\/(~(p102 zenon_TX_l)))/\((p100 zenon_TX_l)\/(~(p101 zenon_TX_l))))))))))))))))))) -> (forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p3 X))\/(~(p102 X))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_x zenon_TY_w) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X))))))))))))))))))))))))))) -> (~(p104 zenon_TX_l)) -> (p103 zenon_TX_l) -> False). % 83.13/83.47 do 4 intro. intros zenon_H9e zenon_H94 zenon_H4d zenon_H13 zenon_Hf zenon_H15 zenon_H14 zenon_H92 zenon_H9f zenon_H9c. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H9e). zenon_intro zenon_Ha1. zenon_intro zenon_Ha0. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Ha0). zenon_intro zenon_Ha3. zenon_intro zenon_Ha2. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Ha2). zenon_intro zenon_Ha5. zenon_intro zenon_Ha4. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Ha4). zenon_intro zenon_Ha7. zenon_intro zenon_Ha6. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Ha6). zenon_intro zenon_Ha9. zenon_intro zenon_Ha8. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Ha8). zenon_intro zenon_Hab. zenon_intro zenon_Haa. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Haa). zenon_intro zenon_Had. zenon_intro zenon_Hac. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hac). zenon_intro zenon_Haf. zenon_intro zenon_Hae. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hae). zenon_intro zenon_Hb1. zenon_intro zenon_Hb0. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hb0). zenon_intro zenon_Hb3. zenon_intro zenon_Hb2. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hb2). zenon_intro zenon_Hb5. zenon_intro zenon_Hb4. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hb4). zenon_intro zenon_Hb7. zenon_intro zenon_Hb6. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hb6). zenon_intro zenon_Hb9. zenon_intro zenon_Hb8. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hb8). zenon_intro zenon_Hbb. zenon_intro zenon_Hba. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hba). zenon_intro zenon_H9b. zenon_intro zenon_Hbc. % 83.13/83.47 apply (zenon_or_s _ _ zenon_Ha3); [ zenon_intro zenon_Hbe | zenon_intro zenon_Hbd ]. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hbe). zenon_intro zenon_Hc0. zenon_intro zenon_Hbf. % 83.13/83.47 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_l X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))) zenon_Hc0); [ zenon_intro zenon_Hc1; idtac ]. % 83.13/83.47 elim zenon_Hc1. zenon_intro zenon_TX_f. zenon_intro zenon_Hc2. % 83.13/83.47 apply (zenon_notor_s _ _ zenon_Hc2). zenon_intro zenon_Hc4. zenon_intro zenon_Hc3. % 83.13/83.47 apply zenon_Hc3. zenon_intro zenon_Hc5. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hc5). zenon_intro zenon_Hc7. zenon_intro zenon_Hc6. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hc6). zenon_intro zenon_H60. zenon_intro zenon_H5d. % 83.13/83.47 apply zenon_Hc4. zenon_intro zenon_Ha. % 83.13/83.47 apply (zenon_or_s _ _ zenon_Hb1); [ zenon_intro zenon_Hc8 | zenon_intro zenon_H99 ]. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hc8). zenon_intro zenon_Hca. zenon_intro zenon_Hc9. % 83.13/83.47 apply (zenon_or_s _ _ zenon_Hca); [ zenon_intro zenon_H51 | zenon_intro zenon_H95 ]. % 83.13/83.47 apply (zenon_L21_ zenon_TX_f zenon_TX_l zenon_TX_q zenon_TY_w zenon_TX_x); trivial. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H9b); [ zenon_intro zenon_H96 | zenon_intro zenon_H9d ]. % 83.13/83.47 apply (zenon_L22_ zenon_TX_l zenon_TX_q); trivial. % 83.13/83.47 exact (zenon_H9d zenon_H9c). % 83.13/83.47 apply (zenon_L23_ zenon_TX_l); trivial. % 83.13/83.47 apply (zenon_notand_s _ _ zenon_Hbd); [ zenon_intro zenon_Hcb | zenon_intro zenon_H9d ]. % 83.13/83.47 exact (zenon_Hcb zenon_H9f). % 83.13/83.47 exact (zenon_H9d zenon_H9c). % 83.13/83.47 (* end of lemma zenon_L24_ *) % 83.13/83.47 assert (zenon_L25_ : forall (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X))))))))))))))))))))) -> (r1 zenon_TX_q zenon_TX_l) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X))))))))))))))))))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (r1 zenon_TY_w zenon_TX_q) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (p103 zenon_TX_l) -> (forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p3 X))\/(~(p102 X))))) -> (~(p104 zenon_TX_l)) -> False). % 83.13/83.47 do 4 intro. intros zenon_Hcc zenon_Hf zenon_H92 zenon_H14 zenon_H15 zenon_H13 zenon_H4d zenon_H9c zenon_H94 zenon_H9f. % 83.13/83.47 generalize (zenon_Hcc zenon_TX_l). zenon_intro zenon_Hcd. % 83.13/83.47 apply (zenon_or_s _ _ zenon_Hcd); [ zenon_intro zenon_H12 | zenon_intro zenon_H9e ]. % 83.13/83.47 exact (zenon_H12 zenon_Hf). % 83.13/83.47 apply (zenon_L24_ zenon_TY_w zenon_TX_x zenon_TX_q zenon_TX_l); trivial. % 83.13/83.47 (* end of lemma zenon_L25_ *) % 83.13/83.47 assert (zenon_L26_ : forall (zenon_TY_w : zenon_U) (zenon_TX_x : zenon_U) (zenon_TX_q : zenon_U), ((((~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 zenon_TX_q))/\(p104 zenon_TX_q))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 zenon_TX_q))/\(p103 zenon_TX_q))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 zenon_TX_q))/\(p102 zenon_TX_q))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 zenon_TX_q))/\(p101 zenon_TX_q))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 zenon_TX_q))/\(p100 zenon_TX_q))))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 zenon_TX_q))))\/(~(p105 zenon_TX_q)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 zenon_TX_q))))\/(~(p104 zenon_TX_q)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 zenon_TX_q))))\/(~(p103 zenon_TX_q)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 zenon_TX_q))))\/(~(p102 zenon_TX_q)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 zenon_TX_q))))\/(~(p101 zenon_TX_q)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 zenon_TX_q))))\/(~(p100 zenon_TX_q)))/\(((p105 zenon_TX_q)\/(~(p106 zenon_TX_q)))/\(((p104 zenon_TX_q)\/(~(p105 zenon_TX_q)))/\(((p103 zenon_TX_q)\/(~(p104 zenon_TX_q)))/\(((p102 zenon_TX_q)\/(~(p103 zenon_TX_q)))/\(((p101 zenon_TX_q)\/(~(p102 zenon_TX_q)))/\((p100 zenon_TX_q)\/(~(p101 zenon_TX_q))))))))))))))))))) -> (~(p3 zenon_TX_q)) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X))))))))))))))))))))))))))) -> (r1 zenon_TY_w zenon_TX_q) -> (r1 zenon_TX_x zenon_TY_w) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))) -> (~(p103 zenon_TX_q)) -> (p102 zenon_TX_q) -> False). % 83.13/83.47 do 3 intro. intros zenon_Hce zenon_Hcf zenon_H4d zenon_H13 zenon_H92 zenon_H15 zenon_H14 zenon_Hd0 zenon_Hd1 zenon_Hd2. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hce). zenon_intro zenon_Hd4. zenon_intro zenon_Hd3. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hd3). zenon_intro zenon_Hd6. zenon_intro zenon_Hd5. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hd5). zenon_intro zenon_Hd8. zenon_intro zenon_Hd7. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hd7). zenon_intro zenon_Hda. zenon_intro zenon_Hd9. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hd9). zenon_intro zenon_Hdc. zenon_intro zenon_Hdb. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hdb). zenon_intro zenon_Hde. zenon_intro zenon_Hdd. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hdd). zenon_intro zenon_He0. zenon_intro zenon_Hdf. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hdf). zenon_intro zenon_He2. zenon_intro zenon_He1. % 83.13/83.47 apply (zenon_and_s _ _ zenon_He1). zenon_intro zenon_He4. zenon_intro zenon_He3. % 83.13/83.47 apply (zenon_or_s _ _ zenon_Hd8); [ zenon_intro zenon_He6 | zenon_intro zenon_He5 ]. % 83.13/83.47 apply (zenon_and_s _ _ zenon_He6). zenon_intro zenon_He8. zenon_intro zenon_He7. % 83.13/83.47 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_q X))\/(~((p4 X)/\((~(p104 X))/\(p103 X)))))) zenon_He7); [ zenon_intro zenon_He9; idtac ]. % 83.13/83.47 elim zenon_He9. zenon_intro zenon_TX_l. zenon_intro zenon_Hea. % 83.13/83.47 apply (zenon_notor_s _ _ zenon_Hea). zenon_intro zenon_Hec. zenon_intro zenon_Heb. % 83.13/83.47 apply zenon_Heb. zenon_intro zenon_Hed. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hed). zenon_intro zenon_Hef. zenon_intro zenon_Hee. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hee). zenon_intro zenon_H9f. zenon_intro zenon_H9c. % 83.13/83.47 apply zenon_Hec. zenon_intro zenon_Hf. % 83.13/83.47 apply (zenon_or_s _ _ zenon_He4); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hf0 ]. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hf1). zenon_intro zenon_Hf3. zenon_intro zenon_Hf2. % 83.13/83.47 apply (zenon_or_s _ _ zenon_Hf3); [ zenon_intro zenon_H94 | zenon_intro zenon_Hf4 ]. % 83.13/83.47 generalize (zenon_Hd0 zenon_TY_w). zenon_intro zenon_Hf5. % 83.13/83.47 apply (zenon_or_s _ _ zenon_Hf5); [ zenon_intro zenon_H1a | zenon_intro zenon_Hf6 ]. % 83.13/83.47 exact (zenon_H1a zenon_H14). % 83.13/83.47 generalize (zenon_Hf6 zenon_TX_q). zenon_intro zenon_Hf7. % 83.13/83.47 apply (zenon_or_s _ _ zenon_Hf7); [ zenon_intro zenon_H1c | zenon_intro zenon_Hcc ]. % 83.13/83.47 exact (zenon_H1c zenon_H15). % 83.13/83.47 apply (zenon_L25_ zenon_TY_w zenon_TX_x zenon_TX_l zenon_TX_q); trivial. % 83.13/83.47 exact (zenon_Hcf zenon_Hf4). % 83.13/83.47 exact (zenon_Hf0 zenon_Hd2). % 83.13/83.47 apply (zenon_notand_s _ _ zenon_He5); [ zenon_intro zenon_Hf8 | zenon_intro zenon_Hf0 ]. % 83.13/83.47 exact (zenon_Hf8 zenon_Hd1). % 83.13/83.47 exact (zenon_Hf0 zenon_Hd2). % 83.13/83.47 (* end of lemma zenon_L26_ *) % 83.13/83.47 assert (zenon_L27_ : forall (zenon_TX_x : zenon_U) (zenon_TY_w : zenon_U), ((((~(forall X : zenon_U, ((~(r1 zenon_TY_w X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TY_w X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 zenon_TY_w))/\(p104 zenon_TY_w))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TY_w X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TY_w X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 zenon_TY_w))/\(p103 zenon_TY_w))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TY_w X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TY_w X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 zenon_TY_w))/\(p102 zenon_TY_w))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TY_w X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TY_w X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 zenon_TY_w))/\(p101 zenon_TY_w))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TY_w X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TY_w X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 zenon_TY_w))/\(p100 zenon_TY_w))))/\(((((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 zenon_TY_w))/\((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 zenon_TY_w))))\/(~(p105 zenon_TY_w)))/\(((((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 zenon_TY_w))/\((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 zenon_TY_w))))\/(~(p104 zenon_TY_w)))/\(((((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 zenon_TY_w))/\((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 zenon_TY_w))))\/(~(p103 zenon_TY_w)))/\(((((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 zenon_TY_w))/\((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 zenon_TY_w))))\/(~(p102 zenon_TY_w)))/\(((((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 zenon_TY_w))/\((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 zenon_TY_w))))\/(~(p101 zenon_TY_w)))/\(((((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 zenon_TY_w))/\((forall X : zenon_U, ((~(r1 zenon_TY_w X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 zenon_TY_w))))\/(~(p100 zenon_TY_w)))/\(((p105 zenon_TY_w)\/(~(p106 zenon_TY_w)))/\(((p104 zenon_TY_w)\/(~(p105 zenon_TY_w)))/\(((p103 zenon_TY_w)\/(~(p104 zenon_TY_w)))/\(((p102 zenon_TY_w)\/(~(p103 zenon_TY_w)))/\(((p101 zenon_TY_w)\/(~(p102 zenon_TY_w)))/\((p100 zenon_TY_w)\/(~(p101 zenon_TY_w))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X))))))))))))))))))))))) -> (r1 zenon_TX_x zenon_TY_w) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p6 Y))/\((~(p106 Y))/\(p105 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p6 Y)/\((~(p106 Y))/\(p105 Y))))))))\/(~((~(p105 X))/\(p104 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p5 Y))/\((~(p105 Y))/\(p104 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p5 Y)/\((~(p105 Y))/\(p104 Y))))))))\/(~((~(p104 X))/\(p103 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p4 Y))/\((~(p104 Y))/\(p103 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p4 Y)/\((~(p104 Y))/\(p103 Y))))))))\/(~((~(p103 X))/\(p102 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p3 Y))/\((~(p103 Y))/\(p102 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p3 Y)/\((~(p103 Y))/\(p102 Y))))))))\/(~((~(p102 X))/\(p101 X))))/\((((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))))/\(~(forall Y : zenon_U, ((~(r1 X Y))\/(~((p2 Y)/\((~(p102 Y))/\(p101 Y))))))))\/(~((~(p101 X))/\(p100 X))))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p6 Y))\/(~(p105 Y)))))\/(p6 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p6 Y)\/(~(p105 Y)))))\/(~(p6 X))))\/(~(p105 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p5 Y))\/(~(p104 Y)))))\/(p5 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p5 Y)\/(~(p104 Y)))))\/(~(p5 X))))\/(~(p104 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p4 Y))\/(~(p103 Y)))))\/(p4 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(p103 Y)))))\/(~(p4 X))))\/(~(p103 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p3 Y))\/(~(p102 Y)))))\/(p3 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(p102 Y)))))\/(~(p3 X))))\/(~(p102 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p2 Y))\/(~(p101 Y)))))\/(p2 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(p101 Y)))))\/(~(p2 X))))\/(~(p101 X)))/\(((((forall Y : zenon_U, ((~(r1 X Y))\/((~(p1 Y))\/(~(p100 Y)))))\/(p1 X))/\((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(p100 Y)))))\/(~(p1 X))))\/(~(p100 X)))/\(((p105 X)\/(~(p106 X)))/\(((p104 X)\/(~(p105 X)))/\(((p103 X)\/(~(p104 X)))/\(((p102 X)\/(~(p103 X)))/\(((p101 X)\/(~(p102 X)))/\((p100 X)\/(~(p101 X))))))))))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_x Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (~(p102 zenon_TY_w)) -> (p101 zenon_TY_w) -> False). % 83.13/83.47 do 2 intro. intros zenon_Hf9 zenon_Hfa zenon_H14 zenon_Hd0 zenon_H92 zenon_H13 zenon_H4d zenon_Hfb zenon_Hfc. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hf9). zenon_intro zenon_Hfe. zenon_intro zenon_Hfd. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hfd). zenon_intro zenon_H100. zenon_intro zenon_Hff. % 83.13/83.47 apply (zenon_and_s _ _ zenon_Hff). zenon_intro zenon_H102. zenon_intro zenon_H101. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H101). zenon_intro zenon_H104. zenon_intro zenon_H103. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H104); [ zenon_intro zenon_H106 | zenon_intro zenon_H105 ]. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H106). zenon_intro zenon_H108. zenon_intro zenon_H107. % 83.13/83.47 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TY_w X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))) zenon_H108); [ zenon_intro zenon_H109; idtac ]. % 83.13/83.47 elim zenon_H109. zenon_intro zenon_TX_q. zenon_intro zenon_H10a. % 83.13/83.47 apply (zenon_notor_s _ _ zenon_H10a). zenon_intro zenon_H10c. zenon_intro zenon_H10b. % 83.13/83.47 apply zenon_H10b. zenon_intro zenon_H10d. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H10d). zenon_intro zenon_Hcf. zenon_intro zenon_H10e. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H10e). zenon_intro zenon_Hd1. zenon_intro zenon_Hd2. % 83.13/83.47 apply zenon_H10c. zenon_intro zenon_H15. % 83.13/83.47 generalize (zenon_Hfa zenon_TY_w). zenon_intro zenon_H10f. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H10f); [ zenon_intro zenon_H1a | zenon_intro zenon_H110 ]. % 83.13/83.47 exact (zenon_H1a zenon_H14). % 83.13/83.47 generalize (zenon_H110 zenon_TX_q). zenon_intro zenon_H111. % 83.13/83.47 apply (zenon_or_s _ _ zenon_H111); [ zenon_intro zenon_H1c | zenon_intro zenon_Hce ]. % 83.13/83.47 exact (zenon_H1c zenon_H15). % 83.13/83.47 apply (zenon_L26_ zenon_TY_w zenon_TX_x zenon_TX_q); trivial. % 83.13/83.47 apply (zenon_notand_s _ _ zenon_H105); [ zenon_intro zenon_H113 | zenon_intro zenon_H112 ]. % 83.13/83.47 exact (zenon_H113 zenon_Hfb). % 83.13/83.47 exact (zenon_H112 zenon_Hfc). % 83.13/83.47 (* end of lemma zenon_L27_ *) % 83.13/83.47 apply NNPP. intro zenon_G. % 83.13/83.47 apply zenon_G. zenon_intro zenon_H114. % 83.13/83.47 elim zenon_H114. zenon_intro zenon_TX_x. zenon_intro zenon_H115. % 83.13/83.47 apply (zenon_notor_s _ _ zenon_H115). zenon_intro zenon_H117. zenon_intro zenon_H116. % 83.13/83.47 apply zenon_H116. zenon_intro zenon_H118. % 83.13/83.47 apply (zenon_and_s _ _ zenon_H118). zenon_intro zenon_H4d. zenon_intro zenon_H119. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H119). zenon_intro zenon_H92. zenon_intro zenon_H11a. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H11a). zenon_intro zenon_Hd0. zenon_intro zenon_H11b. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H11b). zenon_intro zenon_Hfa. zenon_intro zenon_H11c. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H11c). zenon_intro zenon_H11e. zenon_intro zenon_H11d. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H11d). zenon_intro zenon_H120. zenon_intro zenon_H11f. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H11f). zenon_intro zenon_H122. zenon_intro zenon_H121. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H121). zenon_intro zenon_H124. zenon_intro zenon_H123. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H123). zenon_intro zenon_H126. zenon_intro zenon_H125. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H125). zenon_intro zenon_H128. zenon_intro zenon_H127. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H127). zenon_intro zenon_H12a. zenon_intro zenon_H129. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H129). zenon_intro zenon_H12c. zenon_intro zenon_H12b. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H12b). zenon_intro zenon_H12e. zenon_intro zenon_H12d. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H12d). zenon_intro zenon_H130. zenon_intro zenon_H12f. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H12f). zenon_intro zenon_H132. zenon_intro zenon_H131. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H131). zenon_intro zenon_H134. zenon_intro zenon_H133. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H133). zenon_intro zenon_H136. zenon_intro zenon_H135. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H135). zenon_intro zenon_H138. zenon_intro zenon_H137. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H137). zenon_intro zenon_H13a. zenon_intro zenon_H139. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H139). zenon_intro zenon_H13c. zenon_intro zenon_H13b. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H13b). zenon_intro zenon_H13e. zenon_intro zenon_H13d. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H13d). zenon_intro zenon_H140. zenon_intro zenon_H13f. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H13f). zenon_intro zenon_H142. zenon_intro zenon_H141. % 83.13/83.48 apply zenon_H117. zenon_intro zenon_H13. % 83.13/83.48 apply (zenon_or_s _ _ zenon_H128); [ zenon_intro zenon_H144 | zenon_intro zenon_H143 ]. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H144). zenon_intro zenon_H146. zenon_intro zenon_H145. % 83.13/83.48 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_x Y))\/(~((~(p2 Y))/\((~(p102 Y))/\(p101 Y)))))) zenon_H146); [ zenon_intro zenon_H147; idtac ]. % 83.13/83.48 elim zenon_H147. zenon_intro zenon_TY_w. zenon_intro zenon_H148. % 83.13/83.48 apply (zenon_notor_s _ _ zenon_H148). zenon_intro zenon_H14a. zenon_intro zenon_H149. % 83.13/83.48 apply zenon_H149. zenon_intro zenon_H14b. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H14b). zenon_intro zenon_H14d. zenon_intro zenon_H14c. % 83.13/83.48 apply (zenon_and_s _ _ zenon_H14c). zenon_intro zenon_Hfb. zenon_intro zenon_Hfc. % 83.13/83.48 apply zenon_H14a. zenon_intro zenon_H14. % 83.13/83.48 generalize (zenon_H11e zenon_TY_w). zenon_intro zenon_H14e. % 83.13/83.48 apply (zenon_or_s _ _ zenon_H14e); [ zenon_intro zenon_H1a | zenon_intro zenon_Hf9 ]. % 83.13/83.48 exact (zenon_H1a zenon_H14). % 83.13/83.48 apply (zenon_L27_ zenon_TX_x zenon_TY_w); trivial. % 83.13/83.48 apply (zenon_notand_s _ _ zenon_H143); [ zenon_intro zenon_H150 | zenon_intro zenon_H14f ]. % 83.13/83.48 exact (zenon_H150 zenon_H142). % 83.13/83.48 exact (zenon_H14f zenon_H141). % 83.13/83.48 Qed. % 83.13/83.48 % SZS output end Proof % 83.13/83.48 (* END-PROOF *) % 83.13/83.48 nodes searched: 3197229 % 83.13/83.48 max branch formulas: 45496 % 83.13/83.48 proof nodes created: 345751 % 83.13/83.48 formulas created: 5189424 % 83.13/83.48 %------------------------------------------------------------------------------