%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP107^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:25:04 AM UTC 2026 % Result : Theorem 0.44s 0.89s % Output : Proof 0.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP107^1 : TPTP v9.2.1. Released v7.5.0. % 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n010.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 04:14:10 EDT 2026 % 0.16/0.34 % CPUTime : % 0.37/0.60 %----Proving TH0 % 0.44/0.89 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.44/0.89 % SZS status Theorem % 0.44/0.89 % SZS output start Proof % 0.44/0.89 ( % 0.44/0.89 (declare-sort tptp.set_a 0) % 0.44/0.89 (declare-sort tptp.set_set_a 0) % 0.44/0.89 (declare-sort tptp.set_Product_prod_a_a 0) % 0.44/0.89 (declare-sort tptp.set_se1596668135od_a_a 0) % 0.44/0.89 (declare-sort tptp.product_prod_a_a 0) % 0.44/0.89 (declare-sort tptp.partia1833973666xt_a_b 0) % 0.44/0.89 (declare-sort tptp.partia539144763t_unit 0) % 0.44/0.89 (declare-sort tptp.a 0) % 0.44/0.89 (declare-sort tptp.partia96731725t_unit 0) % 0.44/0.89 (declare-sort tptp.partia1993116613t_unit 0) % 0.44/0.89 (declare-sort tptp.nat 0) % 0.44/0.89 (declare-sort tptp.int 0) % 0.44/0.89 (declare-const tptp.locali425460998xt_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a Bool)) % 0.44/0.89 (declare-const tptp.ring_a_b (-> tptp.partia1833973666xt_a_b Bool)) % 0.44/0.89 (declare-const tptp.one_se1488596747t_unit (-> tptp.partia539144763t_unit tptp.set_Product_prod_a_a)) % 0.44/0.89 (declare-const tptp.mult_s977248631t_unit (-> tptp.partia539144763t_unit tptp.set_Product_prod_a_a tptp.set_Product_prod_a_a tptp.set_Product_prod_a_a)) % 0.44/0.89 (declare-const tptp.member1838126896od_a_a (-> tptp.set_Product_prod_a_a tptp.set_se1596668135od_a_a Bool)) % 0.44/0.89 (declare-const tptp.partia616129906t_unit (-> tptp.partia539144763t_unit tptp.set_se1596668135od_a_a)) % 0.44/0.89 (declare-const tptp.one_a_ring_ext_a_b (-> tptp.partia1833973666xt_a_b tptp.a)) % 0.44/0.89 (declare-const tptp.mult_a_ring_ext_a_b (-> tptp.partia1833973666xt_a_b tptp.a tptp.a tptp.a)) % 0.44/0.89 (declare-const tptp.member_a (-> tptp.a tptp.set_a Bool)) % 0.44/0.89 (declare-const tptp.partia1066395285xt_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a)) % 0.44/0.89 (declare-const tptp.member449909584od_a_a (-> tptp.product_prod_a_a tptp.set_Product_prod_a_a Bool)) % 0.44/0.89 (declare-const tptp.member_set_a (-> tptp.set_a tptp.set_set_a Bool)) % 0.44/0.89 (declare-const tptp.pow_a (-> tptp.set_a tptp.set_set_a)) % 0.44/0.89 (declare-const tptp.collect_set_a (-> (-> tptp.set_a Bool) tptp.set_set_a)) % 0.44/0.89 (declare-const tptp.mult_a_Product_unit (-> tptp.partia96731725t_unit tptp.a tptp.a tptp.a)) % 0.44/0.89 (declare-const tptp.collect_a (-> (-> tptp.a Bool) tptp.set_a)) % 0.44/0.89 (declare-const tptp.abelian_monoid_a_b (-> tptp.partia1833973666xt_a_b Bool)) % 0.44/0.89 (declare-const tptp.product_Pair_a_a (-> tptp.a tptp.a tptp.product_prod_a_a)) % 0.44/0.89 (declare-const tptp.partia1955795460t_unit (-> tptp.partia96731725t_unit tptp.set_a)) % 0.44/0.89 (declare-const tptp.partia206007992t_unit (-> tptp.partia1993116613t_unit tptp.set_Product_prod_a_a)) % 0.44/0.89 (declare-const tptp.equiva2136214035t_unit (-> tptp.partia1993116613t_unit Bool)) % 0.44/0.89 (declare-const tptp.r2 tptp.a) % 0.44/0.89 (declare-const tptp.locali1538946157t_unit (-> tptp.partia1993116613t_unit tptp.set_se1596668135od_a_a)) % 0.44/0.89 (declare-const tptp.field_a_b (-> tptp.partia1833973666xt_a_b Bool)) % 0.44/0.89 (declare-const tptp.locali1648887798ac_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a Bool)) % 0.44/0.89 (declare-const tptp.locali1488796916t_unit (-> tptp.partia539144763t_unit tptp.set_se1596668135od_a_a Bool)) % 0.44/0.89 (declare-const tptp.rel tptp.partia1993116613t_unit) % 0.44/0.89 (declare-const tptp.r3 tptp.a) % 0.44/0.89 (declare-const tptp.a_RCOSETS_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a tptp.set_set_a)) % 0.44/0.89 (declare-const tptp.units_a_ring_ext_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a)) % 0.44/0.89 (declare-const tptp.add_pow_a_b_nat (-> tptp.partia1833973666xt_a_b tptp.nat tptp.a tptp.a)) % 0.44/0.89 (declare-const tptp.locali1170246543t_unit (-> tptp.partia1993116613t_unit tptp.a tptp.a tptp.set_Product_prod_a_a)) % 0.44/0.89 (declare-const tptp.bot_bo2131659635od_a_a tptp.set_Product_prod_a_a) % 0.44/0.89 (declare-const tptp.s3 tptp.a) % 0.44/0.89 (declare-const tptp.s2 tptp.a) % 0.44/0.89 (declare-const tptp.a_l_coset_a_b (-> tptp.partia1833973666xt_a_b tptp.a tptp.set_a tptp.set_a)) % 0.44/0.89 (declare-const tptp.semiring_a_b (-> tptp.partia1833973666xt_a_b Bool)) % 0.44/0.89 (declare-const tptp.group_a_Product_unit (-> tptp.partia96731725t_unit Bool)) % 0.44/0.89 (declare-const tptp.locali807230110ng_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a Bool)) % 0.44/0.89 (declare-const tptp.r tptp.partia1833973666xt_a_b) % 0.44/0.89 (declare-const tptp.collec645855634od_a_a (-> (-> tptp.product_prod_a_a Bool) tptp.set_Product_prod_a_a)) % 0.44/0.89 (declare-const tptp.s tptp.set_a) % 0.44/0.89 (declare-const tptp.collec183727474od_a_a (-> (-> tptp.set_Product_prod_a_a Bool) tptp.set_se1596668135od_a_a)) % 0.44/0.89 (declare-const tptp.zero_a_b (-> tptp.partia1833973666xt_a_b tptp.a)) % 0.44/0.89 (declare-const tptp.locali1944243560ac_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a tptp.partia539144763t_unit)) % 0.44/0.89 (declare-const tptp.units_1734235042t_unit (-> tptp.partia539144763t_unit tptp.set_se1596668135od_a_a)) % 0.44/0.89 (declare-const tptp.add_pow_a_b_int (-> tptp.partia1833973666xt_a_b tptp.int tptp.a tptp.a)) % 0.44/0.89 (declare-const tptp.bot_bo1424703315od_a_a tptp.set_se1596668135od_a_a) % 0.44/0.89 (declare-const tptp.a_r_coset_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a tptp.a tptp.set_a)) % 0.44/0.89 (declare-const tptp.bot_bot_set_a tptp.set_a) % 0.44/0.89 (declare-const tptp.additi2104487374up_a_b (-> tptp.set_a tptp.partia1833973666xt_a_b Bool)) % 0.44/0.89 (declare-const tptp.group_a_ring_ext_a_b (-> tptp.partia1833973666xt_a_b Bool)) % 0.44/0.89 (declare-const tptp.units_a_Product_unit (-> tptp.partia96731725t_unit tptp.set_a)) % 0.44/0.89 (declare-const tptp.monoid1447254976t_unit (-> tptp.partia96731725t_unit Bool)) % 0.44/0.89 (declare-const tptp.group_52730354t_unit (-> tptp.partia539144763t_unit Bool)) % 0.44/0.89 (declare-const tptp.one_a_Product_unit (-> tptp.partia96731725t_unit tptp.a)) % 0.44/0.89 (declare-const tptp.set_add_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a tptp.set_a tptp.set_a)) % 0.44/0.89 (declare-const tptp.bot_bot_set_set_a tptp.set_set_a) % 0.44/0.89 (declare-const tptp.units_1411277569xt_a_b (-> tptp.partia1833973666xt_a_b tptp.partia96731725t_unit)) % 0.44/0.89 (declare-const tptp.units_390215097t_unit (-> tptp.partia539144763t_unit tptp.partia539144763t_unit)) % 0.44/0.89 (declare-const tptp.insert_a (-> tptp.a tptp.set_a tptp.set_a)) % 0.44/0.89 (declare-const tptp.insert1116662519od_a_a (-> tptp.product_prod_a_a tptp.set_Product_prod_a_a tptp.set_Product_prod_a_a)) % 0.44/0.89 (declare-const tptp.insert1738756823od_a_a (-> tptp.set_Product_prod_a_a tptp.set_se1596668135od_a_a tptp.set_se1596668135od_a_a)) % 0.44/0.89 (declare-const tptp.insert_set_a (-> tptp.set_a tptp.set_set_a tptp.set_set_a)) % 0.44/0.89 (declare-const tptp.minus_minus_set_a (-> tptp.set_a tptp.set_a tptp.set_a)) % 0.44/0.89 (define tptp.locali880295127ng_a_b () (let ((_let_1 (@var "S4" tptp.set_a))) (let ((_let_2 (@var "R4" tptp.partia1833973666xt_a_b))) (lambda (@list _let_2 _let_1) (and (_ tptp.ring_a_b _let_2) (_ (_ tptp.locali425460998xt_a_b _let_2) _let_1)))))) % 0.44/0.89 (define tptp.monoid1242292471t_unit () (let ((_let_1 (@var "X3" tptp.set_Product_prod_a_a))) (let ((_let_2 (@var "G2" tptp.partia539144763t_unit))) (let ((_let_3 (_ tptp.one_se1488596747t_unit _let_2))) (let ((_let_4 (_ tptp.mult_s977248631t_unit _let_2))) (let ((_let_5 (_ _let_4 _let_1))) (let ((_let_6 (_ tptp.partia616129906t_unit _let_2))) (let ((_let_7 (_ (_ tptp.member1838126896od_a_a _let_1) _let_6))) (let ((_let_8 (@list _let_1))) (let ((_let_9 (@var "Z3" tptp.set_Product_prod_a_a))) (let ((_let_10 (@var "Y4" tptp.set_Product_prod_a_a))) (let ((_let_11 (_ _let_5 _let_10))) (let ((_let_12 (_ (_ tptp.member1838126896od_a_a _let_10) _let_6))) (lambda (@list _let_2) (and (forall (@list _let_1 _let_10) (=> _let_7 (=> _let_12 (_ (_ tptp.member1838126896od_a_a _let_11) _let_6)))) (forall (@list _let_1 _let_10 _let_9) (=> _let_7 (=> _let_12 (=> (_ (_ tptp.member1838126896od_a_a _let_9) _let_6) (= (_ (_ _let_4 _let_11) _let_9) (_ _let_5 (_ (_ _let_4 _let_10) _let_9))))))) (_ (_ tptp.member1838126896od_a_a _let_3) _let_6) (forall _let_8 (=> _let_7 (= (_ (_ _let_4 _let_3) _let_1) _let_1))) (forall _let_8 (=> _let_7 (= (_ _let_5 _let_3) _let_1)))))))))))))))))) % 0.44/0.89 (define tptp.monoid1022105667xt_a_b () (let ((_let_1 (@var "X3" tptp.a))) (let ((_let_2 (@var "G2" tptp.partia1833973666xt_a_b))) (let ((_let_3 (_ tptp.one_a_ring_ext_a_b _let_2))) (let ((_let_4 (_ tptp.mult_a_ring_ext_a_b _let_2))) (let ((_let_5 (_ _let_4 _let_1))) (let ((_let_6 (_ tptp.partia1066395285xt_a_b _let_2))) (let ((_let_7 (_ (_ tptp.member_a _let_1) _let_6))) (let ((_let_8 (@list _let_1))) (let ((_let_9 (@var "Z3" tptp.a))) (let ((_let_10 (@var "Y4" tptp.a))) (let ((_let_11 (_ _let_5 _let_10))) (let ((_let_12 (_ (_ tptp.member_a _let_10) _let_6))) (lambda (@list _let_2) (and (forall (@list _let_1 _let_10) (=> _let_7 (=> _let_12 (_ (_ tptp.member_a _let_11) _let_6)))) (forall (@list _let_1 _let_10 _let_9) (=> _let_7 (=> _let_12 (=> (_ (_ tptp.member_a _let_9) _let_6) (= (_ (_ _let_4 _let_11) _let_9) (_ _let_5 (_ (_ _let_4 _let_10) _let_9))))))) (_ (_ tptp.member_a _let_3) _let_6) (forall _let_8 (=> _let_7 (= (_ (_ _let_4 _let_3) _let_1) _let_1))) (forall _let_8 (=> _let_7 (= (_ _let_5 _let_3) _let_1)))))))))))))))))) % 0.44/0.89 (define tptp.ord_le1824328871od_a_a () (let ((_let_1 (@var "B5" tptp.set_Product_prod_a_a))) (let ((_let_2 (@var "X3" tptp.product_prod_a_a))) (let ((_let_3 (_ tptp.member449909584od_a_a _let_2))) (let ((_let_4 (@var "A5" tptp.set_Product_prod_a_a))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.44/0.89 (define tptp.ord_le391835783od_a_a () (let ((_let_1 (@var "B5" tptp.set_se1596668135od_a_a))) (let ((_let_2 (@var "X3" tptp.set_Product_prod_a_a))) (let ((_let_3 (_ tptp.member1838126896od_a_a _let_2))) (let ((_let_4 (@var "A5" tptp.set_se1596668135od_a_a))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.44/0.89 (define tptp.ord_less_eq_set_a () (let ((_let_1 (@var "B5" tptp.set_a))) (let ((_let_2 (@var "X3" tptp.a))) (let ((_let_3 (_ tptp.member_a _let_2))) (let ((_let_4 (@var "A5" tptp.set_a))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.44/0.89 (define tptp.ord_le318720350_set_a () (let ((_let_1 (@var "B5" tptp.set_set_a))) (let ((_let_2 (@var "X3" tptp.set_a))) (let ((_let_3 (_ tptp.member_set_a _let_2))) (let ((_let_4 (@var "A5" tptp.set_set_a))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.44/0.89 (define @t1 () (_ tptp.mult_a_ring_ext_a_b tptp.r)) % 0.44/0.89 (define @t2 () (_ (_ @t1 tptp.r3) tptp.r2)) % 0.44/0.89 (define @t3 () (_ (_ @t1 tptp.r2) tptp.r3)) % 0.44/0.89 (define @t4 () (= @t3 @t2)) % 0.44/0.89 (define @t5 () (_ (_ @t1 tptp.s3) tptp.s2)) % 0.44/0.89 (define @t6 () (_ (_ @t1 tptp.s2) tptp.s3)) % 0.44/0.89 (define @t7 () (= @t6 @t5)) % 0.44/0.89 (define @t8 () (_ tptp.locali1170246543t_unit tptp.rel)) % 0.44/0.89 (define @t9 () (_ (_ @t8 @t3) @t6)) % 0.44/0.89 (define @t10 () (_ (_ @t8 tptp.r3) tptp.s3)) % 0.44/0.89 (define @t11 () (_ (_ @t8 tptp.r2) tptp.s2)) % 0.44/0.89 (define @t12 () (_ (_ tptp.locali1944243560ac_a_b tptp.r) tptp.s)) % 0.44/0.89 (define @t13 () (_ tptp.mult_s977248631t_unit @t12)) % 0.44/0.89 (define @t14 () (_ (_ @t13 @t11) @t10)) % 0.44/0.89 (define @t15 () (= @t14 @t9)) % 0.44/0.89 (define @t16 () (_ (_ @t8 @t2) @t5)) % 0.44/0.89 (define @t17 () (_ (_ @t13 @t10) @t11)) % 0.44/0.89 (define @t18 () (= @t17 @t16)) % 0.44/0.89 (define @t19 () (@var "Y" tptp.a)) % 0.44/0.89 (define @t20 () (@var "X" tptp.a)) % 0.44/0.89 (define @t21 () (_ @t1 @t20)) % 0.44/0.89 (define @t22 () (_ @t21 @t19)) % 0.44/0.89 (define @t23 () (_ tptp.member_a @t22)) % 0.44/0.89 (define @t24 () (_ tptp.member_a @t19)) % 0.44/0.89 (define @t25 () (_ tptp.member_a @t20)) % 0.44/0.89 (define @t26 () (@list @t20 @t19)) % 0.44/0.89 (define @t27 () (_ tptp.one_a_ring_ext_a_b tptp.r)) % 0.44/0.89 (define @t28 () (_ tptp.member_a @t27)) % 0.44/0.89 (define @t29 () (_ tptp.partia206007992t_unit tptp.rel)) % 0.44/0.89 (define @t30 () (@var "W" tptp.a)) % 0.44/0.89 (define @t31 () (@var "V" tptp.a)) % 0.44/0.89 (define @t32 () (_ (_ @t8 @t31) @t30)) % 0.44/0.89 (define @t33 () (@var "U" tptp.a)) % 0.44/0.89 (define @t34 () (@var "T" tptp.a)) % 0.44/0.89 (define @t35 () (_ (_ @t8 @t34) @t33)) % 0.44/0.89 (define @t36 () (@var "S" tptp.a)) % 0.44/0.89 (define @t37 () (@var "R" tptp.a)) % 0.44/0.89 (define @t38 () (_ (_ @t8 @t37) @t36)) % 0.44/0.89 (define @t39 () (_ @t13 @t38)) % 0.44/0.89 (define @t40 () (_ @t39 @t35)) % 0.44/0.89 (define @t41 () (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a @t34) @t33)) @t29)) % 0.44/0.89 (define @t42 () (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a @t37) @t36)) @t29)) % 0.44/0.89 (define @t43 () (@var "S2" tptp.a)) % 0.44/0.89 (define @t44 () (@var "R2" tptp.a)) % 0.44/0.89 (define @t45 () (_ (_ @t8 @t44) @t43)) % 0.44/0.89 (define @t46 () (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a @t44) @t43)) @t29)) % 0.44/0.89 (define @t47 () (@list @t37 @t36 @t44 @t43)) % 0.44/0.89 (define @t48 () (@var "M" tptp.partia539144763t_unit)) % 0.44/0.89 (define @t49 () (@var "S3" tptp.set_se1596668135od_a_a)) % 0.44/0.89 (define @t50 () (_ (_ tptp.locali1488796916t_unit @t48) @t49)) % 0.44/0.89 (define @t51 () (@list @t48 @t49)) % 0.44/0.89 (define @t52 () (@var "M" tptp.partia1833973666xt_a_b)) % 0.44/0.89 (define @t53 () (@var "S3" tptp.set_a)) % 0.44/0.89 (define @t54 () (_ (_ tptp.locali425460998xt_a_b @t52) @t53)) % 0.44/0.89 (define @t55 () (@list @t52 @t53)) % 0.44/0.89 (define @t56 () (@var "R3" tptp.partia1833973666xt_a_b)) % 0.44/0.89 (define @t57 () (_ (_ tptp.locali807230110ng_a_b @t56) @t53)) % 0.44/0.89 (define @t58 () (_ (_ tptp.locali1648887798ac_a_b @t56) @t53)) % 0.44/0.89 (define @t59 () (@list @t56 @t53)) % 0.44/0.89 (define @t60 () (_ (_ tptp.locali425460998xt_a_b @t56) @t53)) % 0.44/0.89 (define @t61 () (_ (_ tptp.locali880295127ng_a_b @t56) @t53)) % 0.44/0.89 (define @t62 () (_ tptp.ring_a_b @t56)) % 0.44/0.89 (define @t63 () (@var "Y" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t64 () (@var "X" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t65 () (_ tptp.member1838126896od_a_a @t63)) % 0.44/0.89 (define @t66 () (_ tptp.member1838126896od_a_a @t64)) % 0.44/0.89 (define @t67 () (_ tptp.one_se1488596747t_unit @t12)) % 0.44/0.89 (define @t68 () (@list @t37 @t36)) % 0.44/0.89 (define @t69 () (_ tptp.zero_a_b tptp.r)) % 0.44/0.89 (define @t70 () (_ tptp.member_a @t69)) % 0.44/0.89 (define @t71 () (@var "X2" tptp.a)) % 0.44/0.89 (define @t72 () (_ tptp.partia1066395285xt_a_b tptp.r)) % 0.44/0.89 (define @t73 () (_ tptp.member_a @t71)) % 0.44/0.89 (define @t74 () (_ @t73 @t72)) % 0.44/0.89 (define @t75 () (@list @t71)) % 0.44/0.89 (define @t76 () (_ tptp.member_a @t33)) % 0.44/0.89 (define @t77 () (@var "Y2" tptp.a)) % 0.44/0.89 (define @t78 () (= @t19 @t77)) % 0.44/0.89 (define @t79 () (_ tptp.member_a @t77)) % 0.44/0.89 (define @t80 () (_ @t24 @t72)) % 0.44/0.89 (define @t81 () (_ @t25 @t72)) % 0.44/0.89 (define @t82 () (_ @t1 @t19)) % 0.44/0.89 (define @t83 () (_ @t82 @t20)) % 0.44/0.89 (define @t84 () (= @t83 @t27)) % 0.44/0.89 (define @t85 () (_ tptp.units_a_ring_ext_a_b tptp.r)) % 0.44/0.89 (define @t86 () (_ @t24 @t85)) % 0.44/0.89 (define @t87 () (_ @t25 @t85)) % 0.44/0.89 (define @t88 () (@var "Y22" tptp.a)) % 0.44/0.89 (define @t89 () (@var "X22" tptp.a)) % 0.44/0.89 (define @t90 () (@var "Y1" tptp.a)) % 0.44/0.89 (define @t91 () (@var "X1" tptp.a)) % 0.44/0.89 (define @t92 () (@var "B2" tptp.a)) % 0.44/0.89 (define @t93 () (@var "B" tptp.a)) % 0.44/0.89 (define @t94 () (= @t93 @t92)) % 0.44/0.89 (define @t95 () (@var "A2" tptp.a)) % 0.44/0.89 (define @t96 () (@var "A" tptp.a)) % 0.44/0.89 (define @t97 () (= @t96 @t95)) % 0.44/0.89 (define @t98 () (= (_ (_ tptp.product_Pair_a_a @t96) @t93) (_ (_ tptp.product_Pair_a_a @t95) @t92))) % 0.44/0.89 (define @t99 () (@list @t96 @t93 @t95 @t92)) % 0.44/0.89 (define @t100 () (_ tptp.abelian_monoid_a_b @t56)) % 0.44/0.89 (define @t101 () (_ tptp.semiring_a_b @t56)) % 0.44/0.89 (define @t102 () (@list @t56)) % 0.44/0.89 (define @t103 () (@var "Z" tptp.a)) % 0.44/0.89 (define @t104 () (_ @t21 (_ @t82 @t103))) % 0.44/0.89 (define @t105 () (_ tptp.member_a @t103)) % 0.44/0.89 (define @t106 () (_ @t105 @t72)) % 0.44/0.89 (define @t107 () (@list @t20 @t19 @t103)) % 0.44/0.89 (define @t108 () (@var "P" (-> tptp.a Bool))) % 0.44/0.89 (define @t109 () (_ tptp.collect_a @t108)) % 0.44/0.89 (define @t110 () (_ tptp.member_a @t96)) % 0.44/0.89 (define @t111 () (@var "A" tptp.product_prod_a_a)) % 0.44/0.89 (define @t112 () (@var "P" (-> tptp.product_prod_a_a Bool))) % 0.44/0.89 (define @t113 () (_ tptp.collec645855634od_a_a @t112)) % 0.44/0.89 (define @t114 () (_ tptp.member449909584od_a_a @t111)) % 0.44/0.89 (define @t115 () (@var "A" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t116 () (@var "P" (-> tptp.set_Product_prod_a_a Bool))) % 0.44/0.89 (define @t117 () (_ tptp.member1838126896od_a_a @t115)) % 0.44/0.89 (define @t118 () (@var "A" tptp.set_a)) % 0.44/0.89 (define @t119 () (@var "P" (-> tptp.set_a Bool))) % 0.44/0.89 (define @t120 () (_ tptp.collect_set_a @t119)) % 0.44/0.89 (define @t121 () (_ tptp.member_set_a @t118)) % 0.44/0.89 (define @t122 () (@var "A3" tptp.set_a)) % 0.44/0.89 (define @t123 () (@var "X3" tptp.a)) % 0.44/0.89 (define @t124 () (_ tptp.member_a @t123)) % 0.44/0.89 (define @t125 () (_ @t124 @t122)) % 0.44/0.89 (define @t126 () (@list @t123)) % 0.44/0.89 (define @t127 () (@list @t122)) % 0.44/0.89 (define @t128 () (@var "A3" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t129 () (@var "X3" tptp.product_prod_a_a)) % 0.44/0.89 (define @t130 () (_ tptp.member449909584od_a_a @t129)) % 0.44/0.89 (define @t131 () (_ @t130 @t128)) % 0.44/0.89 (define @t132 () (@list @t129)) % 0.44/0.89 (define @t133 () (@list @t128)) % 0.44/0.89 (define @t134 () (@var "A3" tptp.set_se1596668135od_a_a)) % 0.44/0.89 (define @t135 () (@var "X3" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t136 () (_ tptp.member1838126896od_a_a @t135)) % 0.44/0.89 (define @t137 () (_ @t136 @t134)) % 0.44/0.89 (define @t138 () (@list @t135)) % 0.44/0.89 (define @t139 () (@list @t134)) % 0.44/0.89 (define @t140 () (@var "A3" tptp.set_set_a)) % 0.44/0.89 (define @t141 () (@var "X3" tptp.set_a)) % 0.44/0.89 (define @t142 () (_ tptp.member_set_a @t141)) % 0.44/0.89 (define @t143 () (_ @t142 @t140)) % 0.44/0.89 (define @t144 () (@list @t141)) % 0.44/0.89 (define @t145 () (@list @t140)) % 0.44/0.89 (define @t146 () (_ @t21 @t103)) % 0.44/0.89 (define @t147 () (@list @t20)) % 0.44/0.89 (define @t148 () (= @t19 @t103)) % 0.44/0.89 (define @t149 () (_ tptp.partia1066395285xt_a_b @t56)) % 0.44/0.89 (define @t150 () (_ tptp.zero_a_b @t56)) % 0.44/0.89 (define @t151 () (_ (_ tptp.member_a @t150) @t149)) % 0.44/0.89 (define @t152 () (@var "G" tptp.partia1833973666xt_a_b)) % 0.44/0.89 (define @t153 () (_ tptp.partia1066395285xt_a_b @t152)) % 0.44/0.89 (define @t154 () (@list @t152)) % 0.44/0.89 (define @t155 () (_ tptp.monoid1022105667xt_a_b @t56)) % 0.44/0.89 (define @t156 () (_ tptp.mult_a_ring_ext_a_b @t56)) % 0.44/0.89 (define @t157 () (_ @t25 @t149)) % 0.44/0.89 (define @t158 () (=> @t157 (= (_ (_ @t156 @t150) @t20) @t150))) % 0.44/0.89 (define @t159 () (@list @t56 @t20)) % 0.44/0.89 (define @t160 () (_ @t156 @t20)) % 0.44/0.89 (define @t161 () (=> @t157 (= (_ @t160 @t150) @t150))) % 0.44/0.89 (define @t162 () (_ @t160 @t19)) % 0.44/0.89 (define @t163 () (_ @t24 @t149)) % 0.44/0.89 (define @t164 () (=> @t157 (=> @t163 (_ (_ tptp.member_a @t162) @t149)))) % 0.44/0.89 (define @t165 () (@list @t56 @t20 @t19)) % 0.44/0.89 (define @t166 () (=> @t157 (=> @t163 (=> (_ @t105 @t149) (= (_ (_ @t156 @t162) @t103) (_ @t160 (_ (_ @t156 @t19) @t103))))))) % 0.44/0.89 (define @t167 () (@list @t56 @t20 @t19 @t103)) % 0.44/0.89 (define @t168 () (_ tptp.one_a_ring_ext_a_b @t56)) % 0.44/0.89 (define @t169 () (_ (_ tptp.member_a @t168) @t149)) % 0.44/0.89 (define @t170 () (=> @t157 (= (_ (_ @t156 @t168) @t20) @t20))) % 0.44/0.89 (define @t171 () (@var "Prod" tptp.product_prod_a_a)) % 0.44/0.89 (define @t172 () (@var "B3" tptp.a)) % 0.44/0.89 (define @t173 () (@var "A4" tptp.a)) % 0.44/0.89 (define @t174 () (_ (_ tptp.product_Pair_a_a @t173) @t172)) % 0.44/0.89 (define @t175 () (@list @t173 @t172)) % 0.44/0.89 (define @t176 () (forall @t175 (_ @t112 @t174))) % 0.44/0.89 (define @t177 () (@var "Y" tptp.product_prod_a_a)) % 0.44/0.89 (define @t178 () (@var "P2" tptp.product_prod_a_a)) % 0.44/0.89 (define @t179 () (@var "Y3" tptp.a)) % 0.44/0.89 (define @t180 () (@list @t71 @t179)) % 0.44/0.89 (define @t181 () (_ tptp.field_a_b tptp.r)) % 0.44/0.89 (define @t182 () (@var "X4" tptp.a)) % 0.44/0.89 (define @t183 () (not (= @t69 @t27))) % 0.44/0.89 (define @t184 () (@var "G" tptp.partia539144763t_unit)) % 0.44/0.89 (define @t185 () (_ tptp.one_se1488596747t_unit @t184)) % 0.44/0.89 (define @t186 () (_ tptp.mult_s977248631t_unit @t184)) % 0.44/0.89 (define @t187 () (_ @t186 @t64)) % 0.44/0.89 (define @t188 () (_ tptp.partia616129906t_unit @t184)) % 0.44/0.89 (define @t189 () (_ @t66 @t188)) % 0.44/0.89 (define @t190 () (_ tptp.monoid1242292471t_unit @t184)) % 0.44/0.89 (define @t191 () (@list @t184 @t64)) % 0.44/0.89 (define @t192 () (_ tptp.one_a_ring_ext_a_b @t152)) % 0.44/0.89 (define @t193 () (_ tptp.mult_a_ring_ext_a_b @t152)) % 0.44/0.89 (define @t194 () (_ @t193 @t20)) % 0.44/0.89 (define @t195 () (_ @t25 @t153)) % 0.44/0.89 (define @t196 () (_ tptp.monoid1022105667xt_a_b @t152)) % 0.44/0.89 (define @t197 () (@list @t152 @t20)) % 0.44/0.89 (define @t198 () (_ @t186 @t185)) % 0.44/0.89 (define @t199 () (_ @t193 @t192)) % 0.44/0.89 (define @t200 () (_ tptp.member1838126896od_a_a @t185)) % 0.44/0.89 (define @t201 () (_ @t200 @t188)) % 0.44/0.89 (define @t202 () (@list @t184)) % 0.44/0.89 (define @t203 () (_ tptp.member_a @t192)) % 0.44/0.89 (define @t204 () (_ @t203 @t153)) % 0.44/0.89 (define @t205 () (@var "X2" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t206 () (_ tptp.member1838126896od_a_a @t205)) % 0.44/0.89 (define @t207 () (_ @t206 @t188)) % 0.44/0.89 (define @t208 () (@list @t205)) % 0.44/0.89 (define @t209 () (exists @t208 (and @t207 (= (_ @t187 @t205) @t185)))) % 0.44/0.89 (define @t210 () (_ tptp.units_1734235042t_unit @t184)) % 0.44/0.89 (define @t211 () (_ @t66 @t210)) % 0.44/0.89 (define @t212 () (_ @t73 @t153)) % 0.44/0.89 (define @t213 () (exists @t75 (and @t212 (= (_ @t194 @t71) @t192)))) % 0.44/0.89 (define @t214 () (_ tptp.units_a_ring_ext_a_b @t152)) % 0.44/0.89 (define @t215 () (_ @t25 @t214)) % 0.44/0.89 (define @t216 () (_ @t186 @t205)) % 0.44/0.89 (define @t217 () (exists @t208 (and @t207 (= (_ @t216 @t64) @t185)))) % 0.44/0.89 (define @t218 () (_ @t193 @t71)) % 0.44/0.89 (define @t219 () (exists @t75 (and @t212 (= (_ @t218 @t20) @t192)))) % 0.44/0.89 (define @t220 () (_ @t186 @t63)) % 0.44/0.89 (define @t221 () (_ @t220 @t64)) % 0.44/0.89 (define @t222 () (= @t221 @t185)) % 0.44/0.89 (define @t223 () (_ @t65 @t210)) % 0.44/0.89 (define @t224 () (_ @t187 @t63)) % 0.44/0.89 (define @t225 () (= @t224 @t185)) % 0.44/0.89 (define @t226 () (@list @t184 @t64 @t63)) % 0.44/0.89 (define @t227 () (_ @t193 @t19)) % 0.44/0.89 (define @t228 () (_ @t227 @t20)) % 0.44/0.89 (define @t229 () (= @t228 @t192)) % 0.44/0.89 (define @t230 () (_ @t24 @t214)) % 0.44/0.89 (define @t231 () (_ @t194 @t19)) % 0.44/0.89 (define @t232 () (= @t231 @t192)) % 0.44/0.89 (define @t233 () (@list @t152 @t20 @t19)) % 0.44/0.89 (define @t234 () (_ @t1 @t96)) % 0.44/0.89 (define @t235 () (_ @t234 @t93)) % 0.44/0.89 (define @t236 () (@var "K" tptp.int)) % 0.44/0.89 (define @t237 () (_ tptp.add_pow_a_b_int tptp.r)) % 0.44/0.89 (define @t238 () (_ @t237 @t236)) % 0.44/0.89 (define @t239 () (_ @t238 @t235)) % 0.44/0.89 (define @t240 () (_ tptp.member_a @t93)) % 0.44/0.89 (define @t241 () (_ @t240 @t72)) % 0.44/0.89 (define @t242 () (_ @t110 @t72)) % 0.44/0.89 (define @t243 () (@list @t96 @t93 @t236)) % 0.44/0.89 (define @t244 () (@var "I" tptp.int)) % 0.44/0.89 (define @t245 () (@var "Z" tptp.int)) % 0.44/0.89 (define @t246 () (_ tptp.field_a_b @t56)) % 0.44/0.89 (define @t247 () (_ @t240 @t149)) % 0.44/0.89 (define @t248 () (_ @t110 @t149)) % 0.44/0.89 (define @t249 () (_ @t156 @t96)) % 0.44/0.89 (define @t250 () (_ @t249 @t93)) % 0.44/0.89 (define @t251 () (_ (_ tptp.add_pow_a_b_int @t56) @t236)) % 0.44/0.89 (define @t252 () (_ @t251 @t250)) % 0.44/0.89 (define @t253 () (@list @t56 @t96 @t93 @t236)) % 0.44/0.89 (define @t254 () (@var "Z" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t255 () (_ (_ tptp.member1838126896od_a_a @t254) @t188)) % 0.44/0.89 (define @t256 () (_ @t65 @t188)) % 0.44/0.89 (define @t257 () (@list @t184 @t64 @t63 @t254)) % 0.44/0.89 (define @t258 () (_ @t105 @t153)) % 0.44/0.89 (define @t259 () (_ @t24 @t153)) % 0.44/0.89 (define @t260 () (@list @t152 @t20 @t19 @t103)) % 0.44/0.89 (define @t261 () (_ tptp.member1838126896od_a_a @t224)) % 0.44/0.89 (define @t262 () (_ tptp.member_a @t231)) % 0.44/0.89 (define @t263 () (forall @t208 (=> @t207 (= (_ @t198 @t205) @t205)))) % 0.44/0.89 (define @t264 () (=> @t263 (=> (forall @t208 (=> @t207 (= (_ @t216 @t185) @t205))) @t190))) % 0.44/0.89 (define @t265 () (@var "Z2" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t266 () (@var "Y3" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t267 () (_ @t216 @t266)) % 0.44/0.89 (define @t268 () (=> (_ (_ tptp.member1838126896od_a_a @t265) @t188) (= (_ (_ @t186 @t267) @t265) (_ @t216 (_ (_ @t186 @t266) @t265))))) % 0.44/0.89 (define @t269 () (_ tptp.member1838126896od_a_a @t266)) % 0.44/0.89 (define @t270 () (_ @t269 @t188)) % 0.44/0.89 (define @t271 () (forall (@list @t205 @t266 @t265) (=> @t207 (=> @t270 @t268)))) % 0.44/0.89 (define @t272 () (=> @t270 (_ (_ tptp.member1838126896od_a_a @t267) @t188))) % 0.44/0.89 (define @t273 () (forall (@list @t205 @t266) (=> @t207 @t272))) % 0.44/0.89 (define @t274 () (forall @t75 (=> @t212 (= (_ @t199 @t71) @t71)))) % 0.44/0.89 (define @t275 () (=> @t274 (=> (forall @t75 (=> @t212 (= (_ @t218 @t192) @t71))) @t196))) % 0.44/0.89 (define @t276 () (@var "Z2" tptp.a)) % 0.44/0.89 (define @t277 () (_ @t218 @t179)) % 0.44/0.89 (define @t278 () (_ tptp.member_a @t276)) % 0.44/0.89 (define @t279 () (=> (_ @t278 @t153) (= (_ (_ @t193 @t277) @t276) (_ @t218 (_ (_ @t193 @t179) @t276))))) % 0.44/0.89 (define @t280 () (_ tptp.member_a @t179)) % 0.44/0.89 (define @t281 () (_ @t280 @t153)) % 0.44/0.89 (define @t282 () (forall (@list @t71 @t179 @t276) (=> @t212 (=> @t281 @t279)))) % 0.44/0.89 (define @t283 () (=> @t281 (_ (_ tptp.member_a @t277) @t153))) % 0.44/0.89 (define @t284 () (forall @t180 (=> @t212 @t283))) % 0.44/0.89 (define @t285 () (@var "Y2" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t286 () (@var "U" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t287 () (= @t63 @t254)) % 0.44/0.89 (define @t288 () (@var "K" tptp.nat)) % 0.44/0.89 (define @t289 () (_ tptp.add_pow_a_b_nat tptp.r)) % 0.44/0.89 (define @t290 () (_ @t289 @t288)) % 0.44/0.89 (define @t291 () (_ @t290 @t235)) % 0.44/0.89 (define @t292 () (@list @t96 @t93 @t288)) % 0.44/0.89 (define @t293 () (@var "Xa" tptp.a)) % 0.44/0.89 (define @t294 () (_ tptp.member_a @t293)) % 0.44/0.89 (define @t295 () (@list @t293)) % 0.44/0.89 (define @t296 () (@var "N" tptp.nat)) % 0.44/0.89 (define @t297 () (_ @t289 @t296)) % 0.44/0.89 (define @t298 () (_ tptp.group_a_ring_ext_a_b @t152)) % 0.44/0.89 (define @t299 () (@var "G" tptp.partia96731725t_unit)) % 0.44/0.89 (define @t300 () (_ tptp.group_a_Product_unit @t299)) % 0.44/0.89 (define @t301 () (@list @t299)) % 0.44/0.89 (define @t302 () (_ tptp.units_a_Product_unit @t299)) % 0.44/0.89 (define @t303 () (_ tptp.partia1955795460t_unit @t299)) % 0.44/0.89 (define @t304 () (_ tptp.monoid1447254976t_unit @t299)) % 0.44/0.89 (define @t305 () (_ tptp.group_52730354t_unit @t184)) % 0.44/0.89 (define @t306 () (_ tptp.mult_a_Product_unit @t299)) % 0.44/0.89 (define @t307 () (_ (_ @t306 @t19) @t20)) % 0.44/0.89 (define @t308 () (_ @t24 @t303)) % 0.44/0.89 (define @t309 () (_ @t25 @t303)) % 0.44/0.89 (define @t310 () (_ tptp.one_a_Product_unit @t299)) % 0.44/0.89 (define @t311 () (= @t96 @t310)) % 0.44/0.89 (define @t312 () (_ (_ @t306 @t96) @t20)) % 0.44/0.89 (define @t313 () (_ @t110 @t303)) % 0.44/0.89 (define @t314 () (@list @t299 @t20 @t96)) % 0.44/0.89 (define @t315 () (= @t115 @t185)) % 0.44/0.89 (define @t316 () (_ (_ @t186 @t115) @t64)) % 0.44/0.89 (define @t317 () (_ @t117 @t188)) % 0.44/0.89 (define @t318 () (@list @t184 @t64 @t115)) % 0.44/0.89 (define @t319 () (= @t96 @t192)) % 0.44/0.89 (define @t320 () (_ (_ @t193 @t96) @t20)) % 0.44/0.89 (define @t321 () (_ @t110 @t153)) % 0.44/0.89 (define @t322 () (@list @t152 @t20 @t96)) % 0.44/0.89 (define @t323 () (_ @t306 @t20)) % 0.44/0.89 (define @t324 () (_ @t323 @t96)) % 0.44/0.89 (define @t325 () (_ @t187 @t115)) % 0.44/0.89 (define @t326 () (_ @t194 @t96)) % 0.44/0.89 (define @t327 () (_ @t73 @t303)) % 0.44/0.89 (define @t328 () (@list @t299 @t20)) % 0.44/0.89 (define @t329 () (_ @t306 @t71)) % 0.44/0.89 (define @t330 () (=> (forall @t75 (=> @t327 (exists @t295 (and (_ @t294 @t303) (= (_ (_ @t306 @t293) @t71) @t310))))) @t300)) % 0.44/0.89 (define @t331 () (_ @t329 @t179)) % 0.44/0.89 (define @t332 () (@list @t276)) % 0.44/0.89 (define @t333 () (_ @t280 @t303)) % 0.44/0.89 (define @t334 () (@list @t179)) % 0.44/0.89 (define @t335 () (@var "Xa" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t336 () (=> (forall @t208 (=> @t207 (exists (@list @t335) (and (_ (_ tptp.member1838126896od_a_a @t335) @t188) (= (_ (_ @t186 @t335) @t205) @t185))))) @t305)) % 0.44/0.89 (define @t337 () (@list @t266)) % 0.44/0.89 (define @t338 () (=> (forall @t75 (=> @t212 (exists @t295 (and (_ @t294 @t153) (= (_ (_ @t193 @t293) @t71) @t192))))) @t298)) % 0.44/0.89 (define @t339 () (_ (_ tptp.add_pow_a_b_nat @t56) @t288)) % 0.44/0.89 (define @t340 () (_ @t339 @t250)) % 0.44/0.89 (define @t341 () (@list @t56 @t96 @t93 @t288)) % 0.44/0.89 (define @t342 () (@var "M" tptp.set_a)) % 0.44/0.89 (define @t343 () (_ tptp.a_l_coset_a_b tptp.r)) % 0.44/0.89 (define @t344 () (_ (_ tptp.ord_less_eq_set_a @t342) @t72)) % 0.44/0.89 (define @t345 () (@list @t342)) % 0.44/0.89 (define @t346 () (@var "B4" tptp.set_a)) % 0.44/0.89 (define @t347 () (_ tptp.set_add_a_b tptp.r)) % 0.44/0.89 (define @t348 () (_ tptp.ord_less_eq_set_a @t346)) % 0.44/0.89 (define @t349 () (_ tptp.ord_less_eq_set_a @t122)) % 0.44/0.89 (define @t350 () (@list @t122 @t346)) % 0.44/0.89 (define @t351 () (@var "K2" tptp.set_a)) % 0.44/0.89 (define @t352 () (@var "H" tptp.set_a)) % 0.44/0.89 (define @t353 () (_ @t347 @t352)) % 0.44/0.89 (define @t354 () (_ @t353 @t351)) % 0.44/0.89 (define @t355 () (_ (_ tptp.ord_less_eq_set_a @t351) @t72)) % 0.44/0.89 (define @t356 () (_ (_ tptp.ord_less_eq_set_a @t352) @t72)) % 0.44/0.89 (define @t357 () (@list @t352 @t351)) % 0.44/0.89 (define @t358 () (= @t128 tptp.bot_bo2131659635od_a_a)) % 0.44/0.89 (define @t359 () (_ tptp.ord_le1824328871od_a_a @t128)) % 0.44/0.89 (define @t360 () (= @t122 tptp.bot_bot_set_a)) % 0.44/0.89 (define @t361 () (= @t140 tptp.bot_bot_set_set_a)) % 0.44/0.89 (define @t362 () (_ tptp.ord_le318720350_set_a @t140)) % 0.44/0.89 (define @t363 () (@var "C" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t364 () (_ tptp.member1838126896od_a_a @t363)) % 0.44/0.89 (define @t365 () (@var "C" tptp.set_a)) % 0.44/0.89 (define @t366 () (_ tptp.member_set_a @t365)) % 0.44/0.89 (define @t367 () (@var "C" tptp.product_prod_a_a)) % 0.44/0.89 (define @t368 () (_ tptp.member449909584od_a_a @t367)) % 0.44/0.89 (define @t369 () (@var "C" tptp.a)) % 0.44/0.89 (define @t370 () (_ tptp.member_a @t369)) % 0.44/0.89 (define @t371 () (= @t134 tptp.bot_bo1424703315od_a_a)) % 0.44/0.89 (define @t372 () (forall @t132 (not (_ @t112 @t129)))) % 0.44/0.89 (define @t373 () (@list @t112)) % 0.44/0.89 (define @t374 () (_ @t108 @t123)) % 0.44/0.89 (define @t375 () (forall @t126 (not @t374))) % 0.44/0.89 (define @t376 () (@list @t108)) % 0.44/0.89 (define @t377 () (@var "B4" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t378 () (_ @t359 @t377)) % 0.44/0.89 (define @t379 () (@var "X2" tptp.product_prod_a_a)) % 0.44/0.89 (define @t380 () (_ tptp.member449909584od_a_a @t379)) % 0.44/0.89 (define @t381 () (@var "B4" tptp.set_se1596668135od_a_a)) % 0.44/0.89 (define @t382 () (_ (_ tptp.ord_le391835783od_a_a @t134) @t381)) % 0.44/0.89 (define @t383 () (_ @t349 @t346)) % 0.44/0.89 (define @t384 () (@var "B4" tptp.set_set_a)) % 0.44/0.89 (define @t385 () (_ @t362 @t384)) % 0.44/0.89 (define @t386 () (@var "X2" tptp.set_a)) % 0.44/0.89 (define @t387 () (_ tptp.member_set_a @t386)) % 0.44/0.89 (define @t388 () (@list @t386)) % 0.44/0.89 (define @t389 () (@list @t140 @t384)) % 0.44/0.89 (define @t390 () (= @t122 @t346)) % 0.44/0.89 (define @t391 () (_ @t348 @t122)) % 0.44/0.89 (define @t392 () (= @t140 @t384)) % 0.44/0.89 (define @t393 () (_ tptp.ord_le318720350_set_a @t384)) % 0.44/0.89 (define @t394 () (_ @t393 @t140)) % 0.44/0.89 (define @t395 () (_ @t343 @t20)) % 0.44/0.89 (define @t396 () (@list @t352 @t20)) % 0.44/0.89 (define @t397 () (@list @t115)) % 0.44/0.89 (define @t398 () (@list @t118)) % 0.44/0.89 (define @t399 () (@list @t111)) % 0.44/0.89 (define @t400 () (@list @t96)) % 0.44/0.89 (define @t401 () (_ @t117 @t134)) % 0.44/0.89 (define @t402 () (not @t401)) % 0.44/0.89 (define @t403 () (_ @t121 @t140)) % 0.44/0.89 (define @t404 () (not @t403)) % 0.44/0.89 (define @t405 () (_ @t114 @t128)) % 0.44/0.89 (define @t406 () (not @t405)) % 0.44/0.89 (define @t407 () (_ @t110 @t122)) % 0.44/0.89 (define @t408 () (not @t407)) % 0.44/0.89 (define @t409 () (@var "Y3" tptp.set_a)) % 0.44/0.89 (define @t410 () (@var "Y3" tptp.product_prod_a_a)) % 0.44/0.89 (define @t411 () (@var "X" tptp.product_prod_a_a)) % 0.44/0.89 (define @t412 () (_ tptp.member449909584od_a_a @t411)) % 0.44/0.89 (define @t413 () (_ @t412 @t377)) % 0.44/0.89 (define @t414 () (_ @t412 @t128)) % 0.44/0.89 (define @t415 () (_ @t66 @t381)) % 0.44/0.89 (define @t416 () (_ @t66 @t134)) % 0.44/0.89 (define @t417 () (_ @t25 @t346)) % 0.44/0.89 (define @t418 () (_ @t25 @t122)) % 0.44/0.89 (define @t419 () (@var "X" tptp.set_a)) % 0.44/0.89 (define @t420 () (_ tptp.member_set_a @t419)) % 0.44/0.89 (define @t421 () (_ @t420 @t384)) % 0.44/0.89 (define @t422 () (_ @t420 @t140)) % 0.44/0.89 (define @t423 () (@var "B5" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t424 () (@var "T2" tptp.product_prod_a_a)) % 0.44/0.89 (define @t425 () (_ tptp.member449909584od_a_a @t424)) % 0.44/0.89 (define @t426 () (@var "A5" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t427 () (@list @t426 @t423)) % 0.44/0.89 (define @t428 () (@var "B5" tptp.set_se1596668135od_a_a)) % 0.44/0.89 (define @t429 () (@var "T2" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t430 () (_ tptp.member1838126896od_a_a @t429)) % 0.44/0.89 (define @t431 () (@var "A5" tptp.set_se1596668135od_a_a)) % 0.44/0.89 (define @t432 () (@list @t431 @t428)) % 0.44/0.89 (define @t433 () (@var "B5" tptp.set_a)) % 0.44/0.89 (define @t434 () (@var "T2" tptp.a)) % 0.44/0.89 (define @t435 () (_ tptp.member_a @t434)) % 0.44/0.89 (define @t436 () (@var "A5" tptp.set_a)) % 0.44/0.89 (define @t437 () (@list @t436 @t433)) % 0.44/0.89 (define @t438 () (@var "B5" tptp.set_set_a)) % 0.44/0.89 (define @t439 () (@var "T2" tptp.set_a)) % 0.44/0.89 (define @t440 () (_ tptp.member_set_a @t439)) % 0.44/0.89 (define @t441 () (@var "A5" tptp.set_set_a)) % 0.44/0.89 (define @t442 () (@list @t441 @t438)) % 0.44/0.89 (define @t443 () (@var "Q" (-> tptp.a Bool))) % 0.44/0.89 (define @t444 () (_ (_ tptp.ord_less_eq_set_a @t109) (_ tptp.collect_a @t443))) % 0.44/0.89 (define @t445 () (@list @t108 @t443)) % 0.44/0.89 (define @t446 () (@var "Q" (-> tptp.set_a Bool))) % 0.44/0.89 (define @t447 () (_ (_ tptp.ord_le318720350_set_a @t120) (_ tptp.collect_set_a @t446))) % 0.44/0.89 (define @t448 () (@list @t119 @t446)) % 0.44/0.89 (define @t449 () (@var "C2" tptp.set_a)) % 0.44/0.89 (define @t450 () (@var "C2" tptp.set_set_a)) % 0.44/0.89 (define @t451 () (@var "Z4" tptp.set_a)) % 0.44/0.89 (define @t452 () (@var "Y5" tptp.set_a)) % 0.44/0.89 (define @t453 () (@var "Z4" tptp.set_set_a)) % 0.44/0.89 (define @t454 () (@var "Y5" tptp.set_set_a)) % 0.44/0.89 (define @t455 () (_ (_ tptp.additi2104487374up_a_b @t352) tptp.r)) % 0.44/0.89 (define @t456 () (_ tptp.a_r_coset_a_b tptp.r)) % 0.44/0.89 (define @t457 () (_ (_ @t456 @t352) @t20)) % 0.44/0.89 (define @t458 () (@list @t352 @t351 @t20)) % 0.44/0.89 (define @t459 () (_ tptp.units_1411277569xt_a_b @t152)) % 0.44/0.89 (define @t460 () (_ tptp.units_390215097t_unit @t184)) % 0.44/0.89 (define @t461 () (_ (_ tptp.a_RCOSETS_a_b tptp.r) @t352)) % 0.44/0.89 (define @t462 () (= @t27 @t69)) % 0.44/0.89 (define @t463 () (_ (_ tptp.insert_a @t69) tptp.bot_bot_set_a)) % 0.44/0.89 (define @t464 () (= @t72 @t463)) % 0.44/0.89 (define @t465 () (_ tptp.insert_a @t20)) % 0.44/0.89 (define @t466 () (_ @t465 @t122)) % 0.44/0.89 (define @t467 () (@list @t20 @t122)) % 0.44/0.89 (define @t468 () (= @t96 @t93)) % 0.44/0.89 (define @t469 () (_ tptp.insert_a @t93)) % 0.44/0.89 (define @t470 () (_ @t110 (_ @t469 @t122))) % 0.44/0.89 (define @t471 () (@list @t96 @t93 @t122)) % 0.44/0.89 (define @t472 () (@var "B" tptp.product_prod_a_a)) % 0.44/0.89 (define @t473 () (= @t111 @t472)) % 0.44/0.89 (define @t474 () (_ tptp.insert1116662519od_a_a @t472)) % 0.44/0.89 (define @t475 () (_ @t114 (_ @t474 @t128))) % 0.44/0.89 (define @t476 () (@list @t111 @t472 @t128)) % 0.44/0.89 (define @t477 () (@var "B" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t478 () (= @t115 @t477)) % 0.44/0.89 (define @t479 () (_ tptp.insert1738756823od_a_a @t477)) % 0.44/0.89 (define @t480 () (_ @t117 (_ @t479 @t134))) % 0.44/0.89 (define @t481 () (@list @t115 @t477 @t134)) % 0.44/0.89 (define @t482 () (@var "B" tptp.set_a)) % 0.44/0.89 (define @t483 () (= @t118 @t482)) % 0.44/0.89 (define @t484 () (_ tptp.insert_set_a @t482)) % 0.44/0.89 (define @t485 () (_ @t121 (_ @t484 @t140))) % 0.44/0.89 (define @t486 () (@list @t118 @t482 @t140)) % 0.44/0.89 (define @t487 () (_ @t469 @t346)) % 0.44/0.89 (define @t488 () (_ @t110 @t487)) % 0.44/0.89 (define @t489 () (_ @t110 @t346)) % 0.44/0.89 (define @t490 () (@list @t96 @t346 @t93)) % 0.44/0.89 (define @t491 () (_ @t474 @t377)) % 0.44/0.89 (define @t492 () (_ @t114 @t491)) % 0.44/0.89 (define @t493 () (_ @t114 @t377)) % 0.44/0.89 (define @t494 () (@list @t111 @t377 @t472)) % 0.44/0.89 (define @t495 () (_ @t479 @t381)) % 0.44/0.89 (define @t496 () (_ @t117 @t495)) % 0.44/0.89 (define @t497 () (_ @t117 @t381)) % 0.44/0.89 (define @t498 () (@list @t115 @t381 @t477)) % 0.44/0.89 (define @t499 () (_ @t484 @t384)) % 0.44/0.89 (define @t500 () (_ @t121 @t499)) % 0.44/0.89 (define @t501 () (_ @t121 @t384)) % 0.44/0.89 (define @t502 () (@list @t118 @t384 @t482)) % 0.44/0.89 (define @t503 () (_ tptp.insert1738756823od_a_a @t115)) % 0.44/0.89 (define @t504 () (_ tptp.insert_set_a @t118)) % 0.44/0.89 (define @t505 () (_ @t504 tptp.bot_bot_set_set_a)) % 0.44/0.89 (define @t506 () (_ tptp.insert1116662519od_a_a @t111)) % 0.44/0.89 (define @t507 () (_ @t506 tptp.bot_bo2131659635od_a_a)) % 0.44/0.89 (define @t508 () (_ tptp.insert_a @t96)) % 0.44/0.89 (define @t509 () (_ @t508 tptp.bot_bot_set_a)) % 0.44/0.89 (define @t510 () (_ tptp.insert1116662519od_a_a @t411)) % 0.44/0.89 (define @t511 () (_ @t510 @t128)) % 0.44/0.89 (define @t512 () (@list @t411 @t128 @t377)) % 0.44/0.89 (define @t513 () (_ tptp.insert1738756823od_a_a @t64)) % 0.44/0.89 (define @t514 () (_ @t513 @t134)) % 0.44/0.89 (define @t515 () (@list @t64 @t134 @t381)) % 0.44/0.89 (define @t516 () (@list @t20 @t122 @t346)) % 0.44/0.89 (define @t517 () (_ tptp.insert_set_a @t419)) % 0.44/0.89 (define @t518 () (_ @t517 @t140)) % 0.44/0.89 (define @t519 () (@list @t419 @t140 @t384)) % 0.44/0.89 (define @t520 () (_ @t474 tptp.bot_bo2131659635od_a_a)) % 0.44/0.89 (define @t521 () (and @t473 (_ @t359 @t520))) % 0.44/0.89 (define @t522 () (_ @t506 @t128)) % 0.44/0.89 (define @t523 () (_ @t469 tptp.bot_bot_set_a)) % 0.44/0.89 (define @t524 () (and @t468 (_ @t349 @t523))) % 0.44/0.89 (define @t525 () (_ @t508 @t122)) % 0.44/0.89 (define @t526 () (_ @t484 tptp.bot_bot_set_set_a)) % 0.44/0.89 (define @t527 () (and @t483 (_ @t362 @t526))) % 0.44/0.89 (define @t528 () (_ @t504 @t140)) % 0.44/0.89 (define @t529 () (@var "X5" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t530 () (@var "X5" tptp.set_a)) % 0.44/0.89 (define @t531 () (@var "X5" tptp.set_set_a)) % 0.44/0.89 (define @t532 () (_ @t510 tptp.bot_bo2131659635od_a_a)) % 0.44/0.89 (define @t533 () (_ @t465 tptp.bot_bot_set_a)) % 0.44/0.89 (define @t534 () (_ @t517 tptp.bot_bot_set_set_a)) % 0.44/0.89 (define @t535 () (@var "B6" tptp.set_a)) % 0.44/0.89 (define @t536 () (@list @t535)) % 0.44/0.89 (define @t537 () (@list @t96 @t122)) % 0.44/0.89 (define @t538 () (@var "B6" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t539 () (@list @t538)) % 0.44/0.89 (define @t540 () (@list @t111 @t128)) % 0.44/0.89 (define @t541 () (@var "B6" tptp.set_se1596668135od_a_a)) % 0.44/0.89 (define @t542 () (@list @t541)) % 0.44/0.89 (define @t543 () (@list @t115 @t134)) % 0.44/0.89 (define @t544 () (@var "B6" tptp.set_set_a)) % 0.44/0.89 (define @t545 () (@list @t544)) % 0.44/0.89 (define @t546 () (@list @t118 @t140)) % 0.44/0.89 (define @t547 () (_ tptp.insert_a @t19)) % 0.44/0.89 (define @t548 () (@var "C3" tptp.set_a)) % 0.44/0.89 (define @t549 () (not @t468)) % 0.44/0.89 (define @t550 () (@var "C3" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t551 () (_ tptp.member449909584od_a_a @t472)) % 0.44/0.89 (define @t552 () (not @t473)) % 0.44/0.89 (define @t553 () (= @t128 @t377)) % 0.44/0.89 (define @t554 () (@var "C3" tptp.set_se1596668135od_a_a)) % 0.44/0.89 (define @t555 () (_ tptp.member1838126896od_a_a @t477)) % 0.44/0.89 (define @t556 () (not @t478)) % 0.44/0.89 (define @t557 () (= @t134 @t381)) % 0.44/0.89 (define @t558 () (_ @t503 @t134)) % 0.44/0.89 (define @t559 () (@var "C3" tptp.set_set_a)) % 0.44/0.89 (define @t560 () (_ tptp.member_set_a @t482)) % 0.44/0.89 (define @t561 () (not @t483)) % 0.44/0.89 (define @t562 () (@var "D" tptp.product_prod_a_a)) % 0.44/0.89 (define @t563 () (@var "D" tptp.a)) % 0.44/0.89 (define @t564 () (_ (_ tptp.minus_minus_set_a @t72) @t463)) % 0.44/0.89 (define @t565 () (= @t14 @t17)) % 0.44/0.89 (define @t566 () (not @t565)) % 0.44/0.89 (define @t567 () (@var "S4" tptp.set_a)) % 0.44/0.89 (define @t568 () (@var "R4" tptp.partia1833973666xt_a_b)) % 0.44/0.89 (define @t569 () (lambda (@list @t568 @t567) (and (_ tptp.ring_a_b @t568) (_ (_ tptp.locali425460998xt_a_b @t568) @t567)))) % 0.44/0.89 (define @t570 () (@var "G2" tptp.partia539144763t_unit)) % 0.44/0.89 (define @t571 () (_ tptp.one_se1488596747t_unit @t570)) % 0.44/0.89 (define @t572 () (_ tptp.mult_s977248631t_unit @t570)) % 0.44/0.89 (define @t573 () (_ @t572 @t135)) % 0.44/0.89 (define @t574 () (_ tptp.partia616129906t_unit @t570)) % 0.44/0.89 (define @t575 () (_ @t136 @t574)) % 0.44/0.89 (define @t576 () (@var "Z3" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t577 () (@var "Y4" tptp.set_Product_prod_a_a)) % 0.44/0.89 (define @t578 () (_ @t573 @t577)) % 0.44/0.89 (define @t579 () (_ (_ tptp.member1838126896od_a_a @t577) @t574)) % 0.44/0.89 (define @t580 () (lambda (@list @t570) (and (forall (@list @t135 @t577) (=> @t575 (=> @t579 (_ (_ tptp.member1838126896od_a_a @t578) @t574)))) (forall (@list @t135 @t577 @t576) (=> @t575 (=> @t579 (=> (_ (_ tptp.member1838126896od_a_a @t576) @t574) (= (_ (_ @t572 @t578) @t576) (_ @t573 (_ (_ @t572 @t577) @t576))))))) (_ (_ tptp.member1838126896od_a_a @t571) @t574) (forall @t138 (=> @t575 (= (_ (_ @t572 @t571) @t135) @t135))) (forall @t138 (=> @t575 (= (_ @t573 @t571) @t135)))))) % 0.44/0.89 (define @t581 () (@var "G2" tptp.partia1833973666xt_a_b)) % 0.44/0.89 (define @t582 () (_ tptp.one_a_ring_ext_a_b @t581)) % 0.44/0.89 (define @t583 () (_ tptp.mult_a_ring_ext_a_b @t581)) % 0.44/0.89 (define @t584 () (_ @t583 @t123)) % 0.44/0.89 (define @t585 () (_ tptp.partia1066395285xt_a_b @t581)) % 0.44/0.89 (define @t586 () (_ @t124 @t585)) % 0.44/0.89 (define @t587 () (@var "Z3" tptp.a)) % 0.44/0.89 (define @t588 () (@var "Y4" tptp.a)) % 0.44/0.89 (define @t589 () (_ @t584 @t588)) % 0.44/0.89 (define @t590 () (_ (_ tptp.member_a @t588) @t585)) % 0.44/0.89 (define @t591 () (lambda (@list @t581) (and (forall (@list @t123 @t588) (=> @t586 (=> @t590 (_ (_ tptp.member_a @t589) @t585)))) (forall (@list @t123 @t588 @t587) (=> @t586 (=> @t590 (=> (_ (_ tptp.member_a @t587) @t585) (= (_ (_ @t583 @t589) @t587) (_ @t584 (_ (_ @t583 @t588) @t587))))))) (_ (_ tptp.member_a @t582) @t585) (forall @t126 (=> @t586 (= (_ (_ @t583 @t582) @t123) @t123))) (forall @t126 (=> @t586 (= (_ @t584 @t582) @t123)))))) % 0.44/0.89 (define @t592 () (lambda @t427 (forall @t132 (=> (_ @t130 @t426) (_ @t130 @t423))))) % 0.44/0.89 (define @t593 () (lambda @t432 (forall @t138 (=> (_ @t136 @t431) (_ @t136 @t428))))) % 0.44/0.89 (define @t594 () (lambda @t437 (forall @t126 (=> (_ @t124 @t436) (_ @t124 @t433))))) % 0.44/0.89 (define @t595 () (lambda @t442 (forall @t144 (=> (_ @t142 @t441) (_ @t142 @t438))))) % 0.44/0.89 (define @t596 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.r2 tptp.r3)) % 0.44/0.89 (define @t597 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.r3 tptp.r2)) % 0.44/0.89 (define @t598 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.s2 tptp.s3)) % 0.44/0.89 (define @t599 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.s3 tptp.s2)) % 0.44/0.89 (define @t600 () (tptp.locali1170246543t_unit tptp.rel tptp.r3 tptp.s3)) % 0.44/0.89 (define @t601 () (tptp.locali1170246543t_unit tptp.rel tptp.r2 tptp.s2)) % 0.44/0.89 (define @t602 () (tptp.locali1944243560ac_a_b tptp.r tptp.s)) % 0.44/0.89 (define @t603 () (tptp.mult_s977248631t_unit @t602 @t601 @t600)) % 0.44/0.89 (define @t604 () (tptp.locali1170246543t_unit tptp.rel @t596 @t598)) % 0.44/0.89 (define @t605 () (_ tptp.mult_s977248631t_unit @t602)) % 0.44/0.89 (define @t606 () (tptp.mult_s977248631t_unit @t602 @t600 @t601)) % 0.44/0.89 (define @t607 () (tptp.locali1170246543t_unit tptp.rel @t597 @t599)) % 0.44/0.89 (define @t608 () (= @t597 @t596)) % 0.44/0.89 (define @t609 () (= @t599 @t598)) % 0.44/0.89 (define @t610 () (= @t604 @t603)) % 0.44/0.89 (define @t611 () (= @t607 @t606)) % 0.44/0.89 (define @t612 () (= @t603 @t606)) % 0.44/0.89 (define @t613 () (and @t608 @t609 @t610 @t611)) % 0.44/0.89 (assume @p1 @t4) % 0.44/0.89 (assume @p2 @t7) % 0.44/0.89 (assume @p3 (_ (_ tptp.locali1648887798ac_a_b tptp.r) tptp.s)) % 0.44/0.89 (assume @p4 @t15) % 0.44/0.89 (assume @p5 @t18) % 0.44/0.89 (assume @p6 (_ (_ tptp.locali807230110ng_a_b tptp.r) tptp.s)) % 0.44/0.89 (assume @p7 (_ (_ tptp.locali880295127ng_a_b tptp.r) tptp.s)) % 0.44/0.89 (assume @p8 (= tptp.locali1944243560ac_a_b tptp.locali1944243560ac_a_b)) % 0.44/0.89 (assume @p9 (_ (_ tptp.locali425460998xt_a_b tptp.r) tptp.s)) % 0.44/0.89 (assume @p10 (forall @t26 (=> (_ @t25 tptp.s) (=> (_ @t24 tptp.s) (_ @t23 tptp.s))))) % 0.44/0.89 (assume @p11 (_ tptp.monoid1242292471t_unit @t12)) % 0.44/0.89 (assume @p12 (_ tptp.semiring_a_b tptp.r)) % 0.44/0.89 (assume @p13 (_ @t28 tptp.s)) % 0.44/0.89 (assume @p14 (_ tptp.equiva2136214035t_unit tptp.rel)) % 0.44/0.89 (assume @p15 (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a tptp.r3) tptp.s3)) @t29)) % 0.44/0.89 (assume @p16 (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a tptp.r2) tptp.s2)) @t29)) % 0.44/0.89 (assume @p17 (forall (@list @t37 @t36 @t34 @t33 @t31 @t30) (=> @t42 (=> @t41 (=> (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a @t31) @t30)) @t29) (= (_ (_ @t13 @t40) @t32) (_ @t39 (_ (_ @t13 @t35) @t32)))))))) % 0.44/0.89 (assume @p18 (_ tptp.abelian_monoid_a_b tptp.r)) % 0.44/0.89 (assume @p19 (forall @t47 (=> @t42 (=> @t46 (= (_ @t39 @t45) (_ (_ @t8 (_ (_ @t1 @t37) @t44)) (_ (_ @t1 @t36) @t43))))))) % 0.44/0.89 (assume @p20 (_ tptp.ring_a_b tptp.r)) % 0.44/0.89 (assume @p21 (forall (@list @t37 @t36 @t34 @t33) (=> @t42 (=> @t41 (_ (_ tptp.member1838126896od_a_a @t40) (_ tptp.locali1538946157t_unit tptp.rel)))))) % 0.44/0.89 (assume @p22 (forall @t51 (=> @t50 (_ tptp.monoid1242292471t_unit @t48)))) % 0.44/0.89 (assume @p23 (forall @t55 (=> @t54 (_ tptp.monoid1022105667xt_a_b @t52)))) % 0.44/0.89 (assume @p24 (forall @t59 (=> @t58 @t57))) % 0.44/0.89 (assume @p25 (forall @t59 (=> @t61 @t60))) % 0.44/0.89 (assume @p26 (forall @t59 (=> @t61 @t62))) % 0.44/0.89 (assume @p27 (forall @t59 (=> @t57 @t61))) % 0.44/0.89 (assume @p28 (forall @t51 (=> @t50 (_ (_ tptp.member1838126896od_a_a (_ tptp.one_se1488596747t_unit @t48)) @t49)))) % 0.44/0.89 (assume @p29 (forall @t55 (=> @t54 (_ (_ tptp.member_a (_ tptp.one_a_ring_ext_a_b @t52)) @t53)))) % 0.44/0.89 (assume @p30 (forall @t59 (=> @t62 (=> @t60 @t61)))) % 0.44/0.89 (assume @p31 (forall @t55 (=> @t54 @t54))) % 0.44/0.89 (assume @p32 (forall @t59 (=> @t58 (_ tptp.monoid1242292471t_unit (_ (_ tptp.locali1944243560ac_a_b @t56) @t53))))) % 0.44/0.89 (assume @p33 (forall (@list @t48 @t49 @t64 @t63) (=> @t50 (=> (_ @t66 @t49) (=> (_ @t65 @t49) (_ (_ tptp.member1838126896od_a_a (_ (_ (_ tptp.mult_s977248631t_unit @t48) @t64) @t63)) @t49)))))) % 0.44/0.89 (assume @p34 (forall (@list @t52 @t53 @t20 @t19) (=> @t54 (=> (_ @t25 @t53) (=> (_ @t24 @t53) (_ (_ tptp.member_a (_ (_ (_ tptp.mult_a_ring_ext_a_b @t52) @t20) @t19)) @t53)))))) % 0.44/0.89 (assume @p35 (forall @t68 (=> @t42 (= (_ @t39 @t67) @t38)))) % 0.44/0.89 (assume @p36 (forall @t68 (=> @t42 (= (_ (_ @t13 @t67) @t38) @t38)))) % 0.44/0.89 (assume @p37 (forall @t47 (=> (_ @t70 tptp.s) (=> @t42 (=> @t46 (= @t38 @t45)))))) % 0.44/0.89 (assume @p38 (forall @t68 (=> @t42 (not (= @t38 tptp.bot_bo2131659635od_a_a))))) % 0.44/0.89 (assume @p39 (forall (@list @t33) (=> (_ @t76 @t72) (=> (forall @t75 (=> @t74 (= (_ (_ @t1 @t33) @t71) @t71))) (= @t33 @t27))))) % 0.44/0.89 (assume @p40 (forall (@list @t19 @t20 @t77) (=> @t84 (=> (= (_ @t21 @t77) @t27) (=> @t81 (=> @t80 (=> (_ @t79 @t72) @t78))))))) % 0.44/0.89 (assume @p41 (forall @t26 (=> (= @t22 @t27) (=> @t87 (=> @t86 @t84))))) % 0.44/0.89 (assume @p42 (forall (@list @t91 @t89 @t90 @t88) (= (= (_ (_ tptp.product_Pair_a_a @t91) @t89) (_ (_ tptp.product_Pair_a_a @t90) @t88)) (and (= @t91 @t90) (= @t89 @t88))))) % 0.44/0.89 (assume @p43 (forall @t99 (= @t98 (and @t97 @t94)))) % 0.44/0.89 (assume @p44 (forall @t102 (=> @t101 @t100))) % 0.44/0.89 (assume @p45 (_ tptp.monoid1022105667xt_a_b tptp.r)) % 0.44/0.89 (assume @p46 (forall @t107 (=> @t81 (=> @t80 (=> @t106 (= (_ (_ @t1 @t22) @t103) @t104)))))) % 0.44/0.89 (assume @p47 (forall @t26 (=> @t81 (=> @t80 (= @t22 @t83))))) % 0.44/0.89 (assume @p48 (forall (@list @t96 @t108) (= (_ @t110 @t109) (_ @t108 @t96)))) % 0.44/0.89 (assume @p49 (forall (@list @t111 @t112) (= (_ @t114 @t113) (_ @t112 @t111)))) % 0.44/0.89 (assume @p50 (forall (@list @t115 @t116) (= (_ @t117 (_ tptp.collec183727474od_a_a @t116)) (_ @t116 @t115)))) % 0.44/0.89 (assume @p51 (forall (@list @t118 @t119) (= (_ @t121 @t120) (_ @t119 @t118)))) % 0.44/0.89 (assume @p52 (forall @t127 (= (_ tptp.collect_a (lambda @t126 @t125)) @t122))) % 0.44/0.89 (assume @p53 (forall @t133 (= (_ tptp.collec645855634od_a_a (lambda @t132 @t131)) @t128))) % 0.44/0.89 (assume @p54 (forall @t139 (= (_ tptp.collec183727474od_a_a (lambda @t138 @t137)) @t134))) % 0.44/0.89 (assume @p55 (forall @t145 (= (_ tptp.collect_set_a (lambda @t144 @t143)) @t140))) % 0.44/0.89 (assume @p56 (forall @t107 (=> @t81 (=> @t80 (=> @t106 (= @t104 (_ @t82 @t146))))))) % 0.44/0.89 (assume @p57 (forall @t147 (=> @t87 @t81))) % 0.44/0.89 (assume @p58 (forall @t147 (=> @t87 (exists @t75 (and @t74 (= (_ (_ @t1 @t71) @t20) @t27)))))) % 0.44/0.89 (assume @p59 (forall @t147 (=> @t87 (exists @t75 (and @t74 (= (_ @t21 @t71) @t27)))))) % 0.44/0.89 (assume @p60 (_ @t70 @t72)) % 0.44/0.89 (assume @p61 (forall @t26 (=> @t81 (=> @t80 (_ @t23 @t72))))) % 0.44/0.89 (assume @p62 (_ @t28 @t72)) % 0.44/0.89 (assume @p63 (forall @t26 (=> @t87 (=> @t86 (_ @t23 @t85))))) % 0.44/0.89 (assume @p64 (_ @t28 @t85)) % 0.44/0.89 (assume @p65 (forall @t147 (=> @t81 (= (_ (_ @t1 @t69) @t20) @t69)))) % 0.44/0.89 (assume @p66 (forall @t147 (=> @t81 (= (_ @t21 @t69) @t69)))) % 0.44/0.89 (assume @p67 (forall @t147 (=> @t81 (= (_ (_ @t1 @t27) @t20) @t20)))) % 0.44/0.89 (assume @p68 (forall @t147 (=> @t81 (= (_ @t21 @t27) @t20)))) % 0.44/0.89 (assume @p69 (forall @t107 (=> @t87 (=> @t80 (=> @t106 (= (= @t22 @t146) @t148)))))) % 0.44/0.89 (assume @p70 (forall @t102 (=> @t100 @t151))) % 0.44/0.89 (assume @p71 (forall @t102 (=> @t62 @t151))) % 0.44/0.89 (assume @p72 (forall @t102 (=> @t101 @t151))) % 0.44/0.89 (assume @p73 (forall @t154 (=> (_ tptp.abelian_monoid_a_b @t152) (_ (_ tptp.member_a (_ tptp.zero_a_b @t152)) @t153)))) % 0.44/0.89 (assume @p74 (forall @t102 (=> @t62 @t155))) % 0.44/0.89 (assume @p75 (forall @t102 (=> @t101 @t155))) % 0.44/0.89 (assume @p76 (forall @t159 (=> @t62 @t158))) % 0.44/0.89 (assume @p77 (forall @t159 (=> @t62 @t161))) % 0.44/0.89 (assume @p78 (forall @t159 (=> @t101 @t161))) % 0.44/0.89 (assume @p79 (forall @t159 (=> @t101 @t158))) % 0.44/0.89 (assume @p80 (forall @t165 (=> @t62 @t164))) % 0.44/0.89 (assume @p81 (forall @t167 (=> @t62 @t166))) % 0.44/0.89 (assume @p82 (forall @t165 (=> @t101 @t164))) % 0.44/0.89 (assume @p83 (forall @t167 (=> @t101 @t166))) % 0.44/0.89 (assume @p84 (forall @t102 (=> @t62 @t169))) % 0.44/0.89 (assume @p85 (forall @t102 (=> @t101 @t169))) % 0.44/0.89 (assume @p86 (forall @t159 (=> @t62 @t170))) % 0.44/0.89 (assume @p87 (forall @t159 (=> @t101 @t170))) % 0.44/0.89 (assume @p88 (forall (@list @t112 @t171) (=> @t176 (_ @t112 @t171)))) % 0.44/0.89 (assume @p89 (forall (@list @t177) (not (forall @t175 (not (= @t177 @t174)))))) % 0.44/0.89 (assume @p90 (forall @t99 (=> @t98 (not (=> @t97 (not @t94)))))) % 0.44/0.89 (assume @p91 (forall (@list @t112 @t178) (=> @t176 (_ @t112 @t178)))) % 0.44/0.89 (assume @p92 (forall (@list @t178) (exists @t180 (= @t178 (_ (_ tptp.product_Pair_a_a @t71) @t179))))) % 0.44/0.89 (assume @p93 (forall @t102 (=> @t62 @t62))) % 0.44/0.89 (assume @p94 (=> @t183 (=> (forall (@list @t173) (=> (_ (_ tptp.member_a @t173) @t72) (=> (not (= @t173 @t69)) (exists (@list @t182) (and (_ (_ tptp.member_a @t182) @t72) (= (_ (_ @t1 @t173) @t182) @t27)))))) @t181))) % 0.44/0.89 (assume @p95 (forall @t191 (=> @t190 (=> @t189 (= (_ @t187 @t185) @t64))))) % 0.44/0.89 (assume @p96 (forall @t197 (=> @t196 (=> @t195 (= (_ @t194 @t192) @t20))))) % 0.44/0.89 (assume @p97 (forall @t191 (=> @t190 (=> @t189 (= (_ @t198 @t64) @t64))))) % 0.44/0.89 (assume @p98 (forall @t197 (=> @t196 (=> @t195 (= (_ @t199 @t20) @t20))))) % 0.44/0.89 (assume @p99 (forall @t202 (=> @t190 @t201))) % 0.44/0.89 (assume @p100 (forall @t154 (=> @t196 @t204))) % 0.44/0.89 (assume @p101 (forall @t191 (=> @t190 (=> @t211 @t209)))) % 0.44/0.89 (assume @p102 (forall @t197 (=> @t196 (=> @t215 @t213)))) % 0.44/0.89 (assume @p103 (forall @t191 (=> @t190 (=> @t211 @t217)))) % 0.44/0.89 (assume @p104 (forall @t197 (=> @t196 (=> @t215 @t219)))) % 0.44/0.89 (assume @p105 (forall @t226 (=> @t190 (=> @t225 (=> @t211 (=> @t223 @t222)))))) % 0.44/0.89 (assume @p106 (forall @t233 (=> @t196 (=> @t232 (=> @t215 (=> @t230 @t229)))))) % 0.44/0.89 (assume @p107 (forall @t243 (=> @t242 (=> @t241 (= (_ (_ @t1 (_ @t238 @t96)) @t93) @t239))))) % 0.44/0.89 (assume @p108 (forall @t243 (=> @t242 (=> @t241 (= (_ @t234 (_ @t238 @t93)) @t239))))) % 0.44/0.89 (assume @p109 (forall (@list @t20 @t244) (=> @t81 (_ (_ tptp.member_a (_ (_ @t237 @t244) @t20)) @t72)))) % 0.44/0.89 (assume @p110 (forall (@list @t245) (= (_ (_ @t237 @t245) @t69) @t69))) % 0.44/0.89 (assume @p111 (forall @t102 (=> @t246 @t62))) % 0.44/0.89 (assume @p112 (forall @t102 (=> @t246 (not (= @t168 @t150))))) % 0.44/0.89 (assume @p113 (forall (@list @t56 @t96 @t93) (=> @t246 (=> (= @t250 @t150) (=> @t248 (=> @t247 (or (= @t96 @t150) (= @t93 @t150)))))))) % 0.44/0.89 (assume @p114 (forall @t253 (=> @t62 (=> @t248 (=> @t247 (= (_ (_ @t156 (_ @t251 @t96)) @t93) @t252)))))) % 0.44/0.89 (assume @p115 (forall @t253 (=> @t62 (=> @t248 (=> @t247 (= (_ @t249 (_ @t251 @t93)) @t252)))))) % 0.44/0.89 (assume @p116 (forall @t202 (=> @t190 (not (= @t188 tptp.bot_bo1424703315od_a_a))))) % 0.44/0.89 (assume @p117 (forall @t154 (=> @t196 (not (= @t153 tptp.bot_bot_set_a))))) % 0.44/0.89 (assume @p118 (forall @t257 (=> @t190 (=> @t189 (=> @t256 (=> @t255 (= (_ (_ @t186 @t224) @t254) (_ @t187 (_ @t220 @t254))))))))) % 0.44/0.89 (assume @p119 (forall @t260 (=> @t196 (=> @t195 (=> @t259 (=> @t258 (= (_ (_ @t193 @t231) @t103) (_ @t194 (_ @t227 @t103))))))))) % 0.44/0.89 (assume @p120 (forall @t226 (=> @t190 (=> @t189 (=> @t256 (_ @t261 @t188)))))) % 0.44/0.89 (assume @p121 (forall @t233 (=> @t196 (=> @t195 (=> @t259 (_ @t262 @t153)))))) % 0.44/0.89 (assume @p122 (forall @t191 (=> @t190 (=> @t211 @t189)))) % 0.44/0.89 (assume @p123 (forall @t197 (=> @t196 (=> @t215 @t195)))) % 0.44/0.89 (assume @p124 (forall @t226 (=> @t190 (=> @t211 (=> @t223 (_ @t261 @t210)))))) % 0.44/0.89 (assume @p125 (forall @t233 (=> @t196 (=> @t215 (=> @t230 (_ @t262 @t214)))))) % 0.44/0.89 (assume @p126 (forall @t154 (=> @t196 (_ @t203 @t214)))) % 0.44/0.89 (assume @p127 (forall @t202 (=> @t190 (_ @t200 @t210)))) % 0.44/0.89 (assume @p128 (forall @t202 (=> @t273 (=> @t201 (=> @t271 @t264))))) % 0.44/0.89 (assume @p129 (forall @t154 (=> @t284 (=> @t204 (=> @t282 @t275))))) % 0.44/0.89 (assume @p130 (forall @t202 (=> @t273 (=> @t271 (=> @t201 @t264))))) % 0.44/0.89 (assume @p131 (forall @t154 (=> @t284 (=> @t282 (=> @t204 @t275))))) % 0.44/0.89 (assume @p132 (forall (@list @t184 @t63 @t64 @t285) (=> @t190 (=> @t222 (=> (= (_ @t187 @t285) @t185) (=> @t189 (=> @t256 (=> (_ (_ tptp.member1838126896od_a_a @t285) @t188) (= @t63 @t285))))))))) % 0.44/0.89 (assume @p133 (forall (@list @t152 @t19 @t20 @t77) (=> @t196 (=> @t229 (=> (= (_ @t194 @t77) @t192) (=> @t195 (=> @t259 (=> (_ @t79 @t153) @t78)))))))) % 0.44/0.89 (assume @p134 (forall (@list @t184 @t286) (=> @t190 (=> (_ (_ tptp.member1838126896od_a_a @t286) @t188) (=> (forall @t208 (=> @t207 (= (_ (_ @t186 @t286) @t205) @t205))) (= @t286 @t185)))))) % 0.44/0.89 (assume @p135 (forall (@list @t152 @t33) (=> @t196 (=> (_ @t76 @t153) (=> (forall @t75 (=> @t212 (= (_ (_ @t193 @t33) @t71) @t71))) (= @t33 @t192)))))) % 0.44/0.89 (assume @p136 (forall @t257 (=> @t190 (=> @t211 (=> @t256 (=> @t255 (= (= @t224 (_ @t187 @t254)) @t287))))))) % 0.44/0.89 (assume @p137 (forall @t260 (=> @t196 (=> @t215 (=> @t259 (=> @t258 (= (= @t231 (_ @t194 @t103)) @t148))))))) % 0.44/0.89 (assume @p138 (_ (_ tptp.ord_less_eq_set_a tptp.s) @t72)) % 0.44/0.89 (assume @p139 (forall @t292 (=> @t242 (=> @t241 (= (_ @t234 (_ @t290 @t93)) @t291))))) % 0.44/0.89 (assume @p140 (forall @t292 (=> @t242 (=> @t241 (= (_ (_ @t1 (_ @t290 @t96)) @t93) @t291))))) % 0.44/0.89 (assume @p141 (=> (forall @t75 (=> @t74 (exists @t295 (and (_ @t294 @t72) (= (_ (_ @t1 @t293) @t71) @t27))))) (_ tptp.group_a_ring_ext_a_b tptp.r))) % 0.44/0.89 (assume @p142 (not (= @t72 tptp.bot_bot_set_a))) % 0.44/0.89 (assume @p143 (forall (@list @t20 @t296) (=> @t81 (_ (_ tptp.member_a (_ @t297 @t20)) @t72)))) % 0.44/0.89 (assume @p144 (forall (@list @t296) (= (_ @t297 @t69) @t69))) % 0.44/0.89 (assume @p145 (forall @t154 (=> @t298 @t298))) % 0.44/0.89 (assume @p146 (forall @t301 (=> @t300 @t300))) % 0.44/0.89 (assume @p147 (forall @t301 (=> @t300 (_ (_ tptp.ord_less_eq_set_a @t303) @t302)))) % 0.44/0.89 (assume @p148 (forall @t154 (=> @t298 (_ (_ tptp.ord_less_eq_set_a @t153) @t214)))) % 0.44/0.89 (assume @p149 (forall @t301 (=> @t300 @t304))) % 0.44/0.89 (assume @p150 (forall @t202 (=> @t305 @t190))) % 0.44/0.89 (assume @p151 (forall @t154 (=> @t298 @t196))) % 0.44/0.89 (assume @p152 (forall (@list @t299 @t20 @t19 @t103) (=> @t300 (=> @t309 (=> @t308 (=> (_ @t105 @t303) (= (= @t307 (_ (_ @t306 @t103) @t20)) @t148))))))) % 0.44/0.89 (assume @p153 (forall @t257 (=> @t305 (=> @t189 (=> @t256 (=> @t255 (= (= @t221 (_ (_ @t186 @t254) @t64)) @t287))))))) % 0.44/0.89 (assume @p154 (forall @t260 (=> @t298 (=> @t195 (=> @t259 (=> @t258 (= (= @t228 (_ (_ @t193 @t103) @t20)) @t148))))))) % 0.44/0.89 (assume @p155 (forall @t301 (=> @t300 (= @t302 @t303)))) % 0.44/0.89 (assume @p156 (forall @t154 (=> @t298 (= @t214 @t153)))) % 0.44/0.89 (assume @p157 (forall @t55 (=> @t54 (_ (_ tptp.ord_less_eq_set_a @t53) (_ tptp.partia1066395285xt_a_b @t52))))) % 0.44/0.89 (assume @p158 (forall @t314 (=> @t300 (=> @t309 (=> @t313 (= (= @t20 @t312) @t311)))))) % 0.44/0.89 (assume @p159 (forall @t318 (=> @t305 (=> @t189 (=> @t317 (= (= @t64 @t316) @t315)))))) % 0.44/0.89 (assume @p160 (forall @t322 (=> @t298 (=> @t195 (=> @t321 (= (= @t20 @t320) @t319)))))) % 0.44/0.89 (assume @p161 (forall @t314 (=> @t300 (=> @t309 (=> @t313 (= (= @t20 @t324) @t311)))))) % 0.44/0.89 (assume @p162 (forall @t318 (=> @t305 (=> @t189 (=> @t317 (= (= @t64 @t325) @t315)))))) % 0.44/0.89 (assume @p163 (forall @t322 (=> @t298 (=> @t195 (=> @t321 (= (= @t20 @t326) @t319)))))) % 0.44/0.89 (assume @p164 (forall @t314 (=> @t300 (=> @t309 (=> @t313 (= (= @t312 @t20) @t311)))))) % 0.44/0.89 (assume @p165 (forall @t318 (=> @t305 (=> @t189 (=> @t317 (= (= @t316 @t64) @t315)))))) % 0.44/0.89 (assume @p166 (forall @t322 (=> @t298 (=> @t195 (=> @t321 (= (= @t320 @t20) @t319)))))) % 0.44/0.89 (assume @p167 (forall @t314 (=> @t300 (=> @t309 (=> @t313 (= (= @t324 @t20) @t311)))))) % 0.44/0.89 (assume @p168 (forall @t318 (=> @t305 (=> @t189 (=> @t317 (= (= @t325 @t64) @t315)))))) % 0.44/0.89 (assume @p169 (forall @t322 (=> @t298 (=> @t195 (=> @t321 (= (= @t326 @t20) @t319)))))) % 0.44/0.89 (assume @p170 (forall @t328 (=> @t300 (=> @t309 (exists @t75 (and @t327 (= (_ @t323 @t71) @t310))))))) % 0.44/0.89 (assume @p171 (forall @t191 (=> @t305 (=> @t189 @t209)))) % 0.44/0.89 (assume @p172 (forall @t197 (=> @t298 (=> @t195 @t213)))) % 0.44/0.89 (assume @p173 (forall @t328 (=> @t300 (=> @t309 (exists @t75 (and @t327 (= (_ @t329 @t20) @t310))))))) % 0.44/0.89 (assume @p174 (forall @t191 (=> @t305 (=> @t189 @t217)))) % 0.44/0.89 (assume @p175 (forall @t197 (=> @t298 (=> @t195 @t219)))) % 0.44/0.89 (assume @p176 (forall (@list @t299 @t20 @t19) (=> @t300 (=> (= (_ @t323 @t19) @t310) (=> @t309 (=> @t308 (= @t307 @t310))))))) % 0.44/0.89 (assume @p177 (forall @t226 (=> @t305 (=> @t225 (=> @t189 (=> @t256 @t222)))))) % 0.44/0.89 (assume @p178 (forall @t233 (=> @t298 (=> @t232 (=> @t195 (=> @t259 @t229)))))) % 0.44/0.89 (assume @p179 (forall @t301 (=> (forall @t75 (=> @t327 (forall @t334 (=> @t333 (_ (_ tptp.member_a @t331) @t303))))) (=> (_ (_ tptp.member_a @t310) @t303) (=> (forall @t75 (=> @t327 (forall @t334 (=> @t333 (forall @t332 (=> (_ @t278 @t303) (= (_ (_ @t306 @t331) @t276) (_ @t329 (_ (_ @t306 @t179) @t276))))))))) (=> (forall @t75 (=> @t327 (= (_ (_ @t306 @t310) @t71) @t71))) @t330)))))) % 0.44/0.89 (assume @p180 (forall @t202 (=> (forall @t208 (=> @t207 (forall @t337 @t272))) (=> @t201 (=> (forall @t208 (=> @t207 (forall @t337 (=> @t270 (forall (@list @t265) @t268))))) (=> @t263 @t336)))))) % 0.44/0.89 (assume @p181 (forall @t154 (=> (forall @t75 (=> @t212 (forall @t334 @t283))) (=> @t204 (=> (forall @t75 (=> @t212 (forall @t334 (=> @t281 (forall @t332 @t279))))) (=> @t274 @t338)))))) % 0.44/0.89 (assume @p182 (forall @t301 (=> @t304 @t330))) % 0.44/0.89 (assume @p183 (forall @t202 (=> @t190 @t336))) % 0.44/0.89 (assume @p184 (forall @t154 (=> @t196 @t338))) % 0.44/0.89 (assume @p185 (forall @t341 (=> @t101 (=> @t248 (=> @t247 (= (_ @t249 (_ @t339 @t93)) @t340)))))) % 0.44/0.89 (assume @p186 (forall @t341 (=> @t101 (=> @t248 (=> @t247 (= (_ (_ @t156 (_ @t339 @t96)) @t93) @t340)))))) % 0.44/0.89 (assume @p187 (forall @t345 (=> @t344 (= (_ (_ @t343 @t69) @t342) @t342)))) % 0.44/0.89 (assume @p188 (forall @t350 (=> (_ @t349 @t72) (=> (_ @t348 @t72) (_ (_ tptp.ord_less_eq_set_a (_ (_ @t347 @t122) @t346)) @t72))))) % 0.44/0.89 (assume @p189 (forall @t357 (=> @t356 (=> @t355 (_ (_ tptp.ord_less_eq_set_a @t354) @t72))))) % 0.44/0.89 (assume @p190 (forall @t133 (= (_ @t359 tptp.bot_bo2131659635od_a_a) @t358))) % 0.44/0.89 (assume @p191 (forall @t127 (= (_ @t349 tptp.bot_bot_set_a) @t360))) % 0.44/0.89 (assume @p192 (forall @t145 (= (_ @t362 tptp.bot_bot_set_set_a) @t361))) % 0.44/0.89 (assume @p193 (forall (@list @t363) (not (_ @t364 tptp.bot_bo1424703315od_a_a)))) % 0.44/0.89 (assume @p194 (forall (@list @t365) (not (_ @t366 tptp.bot_bot_set_set_a)))) % 0.44/0.89 (assume @p195 (forall (@list @t367) (not (_ @t368 tptp.bot_bo2131659635od_a_a)))) % 0.44/0.89 (assume @p196 (forall (@list @t369) (not (_ @t370 tptp.bot_bot_set_a)))) % 0.44/0.89 (assume @p197 (forall @t139 (= (forall @t138 (not @t137)) @t371))) % 0.44/0.89 (assume @p198 (forall @t145 (= (forall @t144 (not @t143)) @t361))) % 0.44/0.89 (assume @p199 (forall @t133 (= (forall @t132 (not @t131)) @t358))) % 0.44/0.89 (assume @p200 (forall @t127 (= (forall @t126 (not @t125)) @t360))) % 0.44/0.89 (assume @p201 (forall @t373 (= (= @t113 tptp.bot_bo2131659635od_a_a) @t372))) % 0.44/0.89 (assume @p202 (forall @t376 (= (= @t109 tptp.bot_bot_set_a) @t375))) % 0.44/0.89 (assume @p203 (forall @t373 (= (= tptp.bot_bo2131659635od_a_a @t113) @t372))) % 0.44/0.89 (assume @p204 (forall @t376 (= (= tptp.bot_bot_set_a @t109) @t375))) % 0.44/0.89 (assume @p205 (forall (@list @t128 @t377) (=> (forall (@list @t379) (=> (_ @t380 @t128) (_ @t380 @t377))) @t378))) % 0.44/0.89 (assume @p206 (forall (@list @t134 @t381) (=> (forall @t208 (=> (_ @t206 @t134) (_ @t206 @t381))) @t382))) % 0.44/0.89 (assume @p207 (forall @t350 (=> (forall @t75 (=> (_ @t73 @t122) (_ @t73 @t346))) @t383))) % 0.44/0.89 (assume @p208 (forall @t389 (=> (forall @t388 (=> (_ @t387 @t140) (_ @t387 @t384))) @t385))) % 0.44/0.89 (assume @p209 (forall @t350 (=> @t383 (=> @t391 @t390)))) % 0.44/0.89 (assume @p210 (forall @t389 (=> @t385 (=> @t394 @t392)))) % 0.44/0.89 (assume @p211 (forall @t396 (=> @t356 (=> @t81 (_ (_ tptp.ord_less_eq_set_a (_ @t395 @t352)) @t72))))) % 0.44/0.89 (assume @p212 (forall @t133 (_ (_ tptp.ord_le1824328871od_a_a tptp.bot_bo2131659635od_a_a) @t128))) % 0.44/0.89 (assume @p213 (forall @t127 (_ (_ tptp.ord_less_eq_set_a tptp.bot_bot_set_a) @t122))) % 0.44/0.89 (assume @p214 (forall @t145 (_ (_ tptp.ord_le318720350_set_a tptp.bot_bot_set_set_a) @t140))) % 0.44/0.89 (assume @p215 (forall @t397 (not (_ @t117 tptp.bot_bo1424703315od_a_a)))) % 0.44/0.89 (assume @p216 (forall @t398 (not (_ @t121 tptp.bot_bot_set_set_a)))) % 0.44/0.89 (assume @p217 (forall @t399 (not (_ @t114 tptp.bot_bo2131659635od_a_a)))) % 0.44/0.89 (assume @p218 (forall @t400 (not (_ @t110 tptp.bot_bot_set_a)))) % 0.44/0.89 (assume @p219 (forall (@list @t134 @t115) (=> @t371 @t402))) % 0.44/0.89 (assume @p220 (forall (@list @t140 @t118) (=> @t361 @t404))) % 0.44/0.89 (assume @p221 (forall (@list @t128 @t111) (=> @t358 @t406))) % 0.44/0.89 (assume @p222 (forall (@list @t122 @t96) (=> @t360 @t408))) % 0.44/0.89 (assume @p223 (forall @t139 (=> (forall @t337 (not (_ @t269 @t134))) @t371))) % 0.44/0.89 (assume @p224 (forall @t145 (=> (forall (@list @t409) (not (_ (_ tptp.member_set_a @t409) @t140))) @t361))) % 0.44/0.89 (assume @p225 (forall @t133 (=> (forall (@list @t410) (not (_ (_ tptp.member449909584od_a_a @t410) @t128))) @t358))) % 0.44/0.89 (assume @p226 (forall @t127 (=> (forall @t334 (not (_ @t280 @t122))) @t360))) % 0.44/0.89 (assume @p227 (forall @t139 (= (exists @t138 @t137) (not @t371)))) % 0.44/0.89 (assume @p228 (forall @t145 (= (exists @t144 @t143) (not @t361)))) % 0.44/0.89 (assume @p229 (forall @t133 (= (exists @t132 @t131) (not @t358)))) % 0.44/0.89 (assume @p230 (forall @t127 (= (exists @t126 @t125) (not @t360)))) % 0.44/0.89 (assume @p231 (forall (@list @t128 @t377 @t411) (=> @t378 (=> @t414 @t413)))) % 0.44/0.89 (assume @p232 (forall (@list @t134 @t381 @t64) (=> @t382 (=> @t416 @t415)))) % 0.44/0.89 (assume @p233 (forall (@list @t122 @t346 @t20) (=> @t383 (=> @t418 @t417)))) % 0.44/0.89 (assume @p234 (forall (@list @t140 @t384 @t419) (=> @t385 (=> @t422 @t421)))) % 0.44/0.89 (assume @p235 (forall (@list @t128 @t377 @t367) (=> @t378 (=> (_ @t368 @t128) (_ @t368 @t377))))) % 0.44/0.89 (assume @p236 (forall (@list @t134 @t381 @t363) (=> @t382 (=> (_ @t364 @t134) (_ @t364 @t381))))) % 0.44/0.89 (assume @p237 (forall (@list @t122 @t346 @t369) (=> @t383 (=> (_ @t370 @t122) (_ @t370 @t346))))) % 0.44/0.89 (assume @p238 (forall (@list @t140 @t384 @t365) (=> @t385 (=> (_ @t366 @t140) (_ @t366 @t384))))) % 0.44/0.89 (assume @p239 (forall @t350 (=> @t390 (not (=> @t383 (not @t391)))))) % 0.44/0.89 (assume @p240 (forall @t389 (=> @t392 (not (=> @t385 (not @t394)))))) % 0.44/0.89 (assume @p241 (forall @t350 (=> @t390 @t383))) % 0.44/0.89 (assume @p242 (forall @t389 (=> @t392 @t385))) % 0.44/0.89 (assume @p243 (forall @t350 (=> @t390 @t391))) % 0.44/0.89 (assume @p244 (forall @t389 (=> @t392 @t394))) % 0.44/0.89 (assume @p245 (= tptp.ord_le1824328871od_a_a (lambda @t427 (forall (@list @t424) (=> (_ @t425 @t426) (_ @t425 @t423)))))) % 0.44/0.89 (assume @p246 (= tptp.ord_le391835783od_a_a (lambda @t432 (forall (@list @t429) (=> (_ @t430 @t431) (_ @t430 @t428)))))) % 0.44/0.89 (assume @p247 (= tptp.ord_less_eq_set_a (lambda @t437 (forall (@list @t434) (=> (_ @t435 @t436) (_ @t435 @t433)))))) % 0.44/0.89 (assume @p248 (= tptp.ord_le318720350_set_a (lambda @t442 (forall (@list @t439) (=> (_ @t440 @t441) (_ @t440 @t438)))))) % 0.44/0.89 (assume @p249 (forall @t127 (_ @t349 @t122))) % 0.44/0.89 (assume @p250 (forall @t145 (_ @t362 @t140))) % 0.44/0.89 (assume @p251 (forall @t445 (=> (forall @t75 (=> (_ @t108 @t71) (_ @t443 @t71))) @t444))) % 0.44/0.89 (assume @p252 (forall @t448 (=> (forall @t388 (=> (_ @t119 @t386) (_ @t446 @t386))) @t447))) % 0.44/0.89 (assume @p253 (forall (@list @t122 @t346 @t449) (=> @t383 (=> (_ @t348 @t449) (_ @t349 @t449))))) % 0.44/0.89 (assume @p254 (forall (@list @t140 @t384 @t450) (=> @t385 (=> (_ @t393 @t450) (_ @t362 @t450))))) % 0.44/0.89 (assume @p255 (= (lambda (@list @t452 @t451) (= @t452 @t451)) (lambda @t437 (and (_ (_ tptp.ord_less_eq_set_a @t436) @t433) (_ (_ tptp.ord_less_eq_set_a @t433) @t436))))) % 0.44/0.89 (assume @p256 (= (lambda (@list @t454 @t453) (= @t454 @t453)) (lambda @t442 (and (_ (_ tptp.ord_le318720350_set_a @t441) @t438) (_ (_ tptp.ord_le318720350_set_a @t438) @t441))))) % 0.44/0.89 (assume @p257 (forall @t445 (= @t444 (forall @t126 (=> @t374 (_ @t443 @t123)))))) % 0.44/0.89 (assume @p258 (forall @t448 (= @t447 (forall @t144 (=> (_ @t119 @t141) (_ @t446 @t141)))))) % 0.44/0.89 (assume @p259 (_ tptp.group_a_Product_unit (_ tptp.units_1411277569xt_a_b tptp.r))) % 0.44/0.89 (assume @p260 (forall @t357 (=> @t455 (=> (_ (_ tptp.additi2104487374up_a_b @t351) tptp.r) (_ (_ tptp.additi2104487374up_a_b @t354) tptp.r))))) % 0.44/0.89 (assume @p261 (forall @t458 (=> @t356 (=> @t355 (=> @t81 (= (_ (_ @t347 @t457) @t351) (_ @t353 (_ @t395 @t351)))))))) % 0.44/0.89 (assume @p262 (forall @t396 (=> @t356 (=> @t81 (_ (_ tptp.ord_less_eq_set_a @t457) @t72))))) % 0.44/0.89 (assume @p263 (forall @t458 (=> @t356 (=> @t355 (=> @t81 (= (_ @t353 (_ (_ @t456 @t351) @t20)) (_ (_ @t456 @t354) @t20))))))) % 0.44/0.89 (assume @p264 (forall @t154 (= (_ tptp.units_a_Product_unit @t459) @t214))) % 0.44/0.89 (assume @p265 (forall @t345 (=> @t344 (= (_ (_ @t456 @t342) @t69) @t342)))) % 0.44/0.89 (assume @p266 (forall @t154 (= (_ tptp.partia1955795460t_unit @t459) @t214))) % 0.44/0.89 (assume @p267 (forall @t202 (=> @t190 (_ tptp.group_52730354t_unit @t460)))) % 0.44/0.89 (assume @p268 (forall @t154 (=> @t196 (_ tptp.group_a_Product_unit @t459)))) % 0.44/0.89 (assume @p269 (forall @t154 (= (_ tptp.mult_a_Product_unit @t459) @t193))) % 0.44/0.89 (assume @p270 (forall @t202 (= (_ tptp.mult_s977248631t_unit @t460) @t186))) % 0.44/0.89 (assume @p271 (forall @t154 (= (_ tptp.one_a_Product_unit @t459) @t192))) % 0.44/0.89 (assume @p272 (forall @t202 (= (_ tptp.one_se1488596747t_unit @t460) @t185))) % 0.44/0.89 (assume @p273 (forall @t396 (=> @t356 (=> @t81 (_ (_ tptp.member_set_a @t457) @t461))))) % 0.44/0.89 (assume @p274 (=> @t464 @t462)) % 0.44/0.89 (assume @p275 (=> @t462 @t464)) % 0.44/0.89 (assume @p276 (forall @t467 (= (_ @t465 @t466) @t466))) % 0.44/0.89 (assume @p277 (forall @t471 (= @t470 (or @t468 @t407)))) % 0.44/0.89 (assume @p278 (forall @t476 (= @t475 (or @t473 @t405)))) % 0.44/0.89 (assume @p279 (forall @t481 (= @t480 (or @t478 @t401)))) % 0.44/0.89 (assume @p280 (forall @t486 (= @t485 (or @t483 @t403)))) % 0.44/0.89 (assume @p281 (forall @t490 (=> (=> (not @t489) @t468) @t488))) % 0.44/0.89 (assume @p282 (forall @t494 (=> (=> (not @t493) @t473) @t492))) % 0.44/0.89 (assume @p283 (forall @t498 (=> (=> (not @t497) @t478) @t496))) % 0.44/0.89 (assume @p284 (forall @t502 (=> (=> (not @t501) @t483) @t500))) % 0.44/0.89 (assume @p285 (= (not @t464) (not @t462))) % 0.44/0.89 (assume @p286 (= @t464 @t462)) % 0.44/0.89 (assume @p287 (forall @t397 (_ @t117 (_ @t503 tptp.bot_bo1424703315od_a_a)))) % 0.44/0.89 (assume @p288 (forall @t398 (_ @t121 @t505))) % 0.44/0.89 (assume @p289 (forall @t399 (_ @t114 @t507))) % 0.44/0.89 (assume @p290 (forall @t400 (_ @t110 @t509))) % 0.44/0.89 (assume @p291 (forall @t512 (= (_ (_ tptp.ord_le1824328871od_a_a @t511) @t377) (and @t413 @t378)))) % 0.44/0.89 (assume @p292 (forall @t515 (= (_ (_ tptp.ord_le391835783od_a_a @t514) @t381) (and @t415 @t382)))) % 0.44/0.89 (assume @p293 (forall @t516 (= (_ (_ tptp.ord_less_eq_set_a @t466) @t346) (and @t417 @t383)))) % 0.44/0.89 (assume @p294 (forall @t519 (= (_ (_ tptp.ord_le318720350_set_a @t518) @t384) (and @t421 @t385)))) % 0.44/0.89 (assume @p295 (forall (@list @t111 @t128 @t472) (= (= @t522 @t520) @t521))) % 0.44/0.89 (assume @p296 (forall (@list @t96 @t122 @t93) (= (= @t525 @t523) @t524))) % 0.44/0.89 (assume @p297 (forall (@list @t118 @t140 @t482) (= (= @t528 @t526) @t527))) % 0.44/0.89 (assume @p298 (forall (@list @t472 @t111 @t128) (= (= @t520 @t522) @t521))) % 0.44/0.89 (assume @p299 (forall (@list @t93 @t96 @t122) (= (= @t523 @t525) @t524))) % 0.44/0.89 (assume @p300 (forall (@list @t482 @t118 @t140) (= (= @t526 @t528) @t527))) % 0.44/0.89 (assume @p301 (forall (@list @t529 @t111) (= (_ (_ tptp.ord_le1824328871od_a_a @t529) @t507) (or (= @t529 tptp.bot_bo2131659635od_a_a) (= @t529 @t507))))) % 0.44/0.89 (assume @p302 (forall (@list @t530 @t96) (= (_ (_ tptp.ord_less_eq_set_a @t530) @t509) (or (= @t530 tptp.bot_bot_set_a) (= @t530 @t509))))) % 0.44/0.89 (assume @p303 (forall (@list @t531 @t118) (= (_ (_ tptp.ord_le318720350_set_a @t531) @t505) (or (= @t531 tptp.bot_bot_set_set_a) (= @t531 @t505))))) % 0.44/0.89 (assume @p304 (forall (@list @t128 @t411) (=> (_ @t359 @t532) (or @t358 (= @t128 @t532))))) % 0.44/0.89 (assume @p305 (forall (@list @t122 @t20) (=> (_ @t349 @t533) (or @t360 (= @t122 @t533))))) % 0.44/0.89 (assume @p306 (forall (@list @t140 @t419) (=> (_ @t362 @t534) (or @t361 (= @t140 @t534))))) % 0.44/0.89 (assume @p307 (forall @t537 (=> @t407 (exists @t536 (and (= @t122 (_ @t508 @t535)) (not (_ @t110 @t535))))))) % 0.44/0.89 (assume @p308 (forall @t540 (=> @t405 (exists @t539 (and (= @t128 (_ @t506 @t538)) (not (_ @t114 @t538))))))) % 0.44/0.89 (assume @p309 (forall @t543 (=> @t401 (exists @t542 (and (= @t134 (_ @t503 @t541)) (not (_ @t117 @t541))))))) % 0.44/0.89 (assume @p310 (forall @t546 (=> @t403 (exists @t545 (and (= @t140 (_ @t504 @t544)) (not (_ @t121 @t544))))))) % 0.44/0.89 (assume @p311 (forall (@list @t20 @t19 @t122) (= (_ @t465 (_ @t547 @t122)) (_ @t547 @t466)))) % 0.44/0.89 (assume @p312 (forall (@list @t96 @t122 @t93 @t346) (=> @t408 (=> (not (_ @t240 @t346)) (= (= @t525 @t487) (and (=> @t468 @t390) (=> @t549 (exists (@list @t548) (and (= @t122 (_ @t469 @t548)) (not (_ @t240 @t548)) (= @t346 (_ @t508 @t548)) (not (_ @t110 @t548))))))))))) % 0.44/0.89 (assume @p313 (forall (@list @t111 @t128 @t472 @t377) (=> @t406 (=> (not (_ @t551 @t377)) (= (= @t522 @t491) (and (=> @t473 @t553) (=> @t552 (exists (@list @t550) (and (= @t128 (_ @t474 @t550)) (not (_ @t551 @t550)) (= @t377 (_ @t506 @t550)) (not (_ @t114 @t550))))))))))) % 0.44/0.89 (assume @p314 (forall (@list @t115 @t134 @t477 @t381) (=> @t402 (=> (not (_ @t555 @t381)) (= (= @t558 @t495) (and (=> @t478 @t557) (=> @t556 (exists (@list @t554) (and (= @t134 (_ @t479 @t554)) (not (_ @t555 @t554)) (= @t381 (_ @t503 @t554)) (not (_ @t117 @t554))))))))))) % 0.44/0.89 (assume @p315 (forall (@list @t118 @t140 @t482 @t384) (=> @t404 (=> (not (_ @t560 @t384)) (= (= @t528 @t499) (and (=> @t483 @t392) (=> @t561 (exists (@list @t559) (and (= @t140 (_ @t484 @t559)) (not (_ @t560 @t559)) (= @t384 (_ @t504 @t559)) (not (_ @t121 @t559))))))))))) % 0.44/0.89 (assume @p316 (forall @t537 (=> @t407 (= @t525 @t122)))) % 0.44/0.89 (assume @p317 (forall @t540 (=> @t405 (= @t522 @t128)))) % 0.44/0.89 (assume @p318 (forall @t543 (=> @t401 (= @t558 @t134)))) % 0.44/0.89 (assume @p319 (forall @t546 (=> @t403 (= @t528 @t140)))) % 0.44/0.89 (assume @p320 (forall @t516 (=> (not @t418) (=> (not @t417) (= (= @t466 (_ @t465 @t346)) @t390))))) % 0.44/0.89 (assume @p321 (forall @t512 (=> (not @t414) (=> (not @t413) (= (= @t511 (_ @t510 @t377)) @t553))))) % 0.44/0.89 (assume @p322 (forall @t515 (=> (not @t416) (=> (not @t415) (= (= @t514 (_ @t513 @t381)) @t557))))) % 0.44/0.89 (assume @p323 (forall @t519 (=> (not @t422) (=> (not @t421) (= (= @t518 (_ @t517 @t384)) @t392))))) % 0.44/0.89 (assume @p324 (forall @t467 (=> @t418 (not (forall @t536 (=> (= @t122 (_ @t465 @t535)) (_ @t25 @t535))))))) % 0.44/0.89 (assume @p325 (forall (@list @t411 @t128) (=> @t414 (not (forall @t539 (=> (= @t128 (_ @t510 @t538)) (_ @t412 @t538))))))) % 0.44/0.89 (assume @p326 (forall (@list @t64 @t134) (=> @t416 (not (forall @t542 (=> (= @t134 (_ @t513 @t541)) (_ @t66 @t541))))))) % 0.44/0.89 (assume @p327 (forall (@list @t419 @t140) (=> @t422 (not (forall @t545 (=> (= @t140 (_ @t517 @t544)) (_ @t420 @t544))))))) % 0.44/0.89 (assume @p328 (forall @t490 (=> @t489 @t488))) % 0.44/0.89 (assume @p329 (forall @t494 (=> @t493 @t492))) % 0.44/0.89 (assume @p330 (forall @t498 (=> @t497 @t496))) % 0.44/0.89 (assume @p331 (forall @t502 (=> @t501 @t500))) % 0.44/0.89 (assume @p332 (forall (@list @t96 @t346) (_ @t110 (_ @t508 @t346)))) % 0.44/0.89 (assume @p333 (forall (@list @t111 @t377) (_ @t114 (_ @t506 @t377)))) % 0.44/0.89 (assume @p334 (forall (@list @t115 @t381) (_ @t117 (_ @t503 @t381)))) % 0.44/0.89 (assume @p335 (forall (@list @t118 @t384) (_ @t121 (_ @t504 @t384)))) % 0.44/0.89 (assume @p336 (forall @t471 (=> @t470 (=> @t549 @t407)))) % 0.44/0.89 (assume @p337 (forall @t476 (=> @t475 (=> @t552 @t405)))) % 0.44/0.89 (assume @p338 (forall @t481 (=> @t480 (=> @t556 @t401)))) % 0.44/0.89 (assume @p339 (forall @t486 (=> @t485 (=> @t561 @t403)))) % 0.44/0.89 (assume @p340 (forall (@list @t111 @t472) (=> (= @t507 @t520) @t473))) % 0.44/0.89 (assume @p341 (forall (@list @t96 @t93) (=> (= @t509 @t523) @t468))) % 0.44/0.89 (assume @p342 (forall @t540 (not (= @t522 tptp.bot_bo2131659635od_a_a)))) % 0.44/0.89 (assume @p343 (forall @t537 (not (= @t525 tptp.bot_bot_set_a)))) % 0.44/0.89 (assume @p344 (forall (@list @t111 @t472 @t367 @t562) (= (= (_ @t506 @t520) (_ (_ tptp.insert1116662519od_a_a @t367) (_ (_ tptp.insert1116662519od_a_a @t562) tptp.bot_bo2131659635od_a_a))) (or (and (= @t111 @t367) (= @t472 @t562)) (and (= @t111 @t562) (= @t472 @t367)))))) % 0.44/0.89 (assume @p345 (forall (@list @t96 @t93 @t369 @t563) (= (= (_ @t508 @t523) (_ (_ tptp.insert_a @t369) (_ (_ tptp.insert_a @t563) tptp.bot_bot_set_a))) (or (and (= @t96 @t369) (= @t93 @t563)) (and (= @t96 @t563) (= @t93 @t369)))))) % 0.44/0.89 (assume @p346 (=> @t183 (=> (forall @t75 (=> (_ @t73 @t564) (_ @t73 @t85))) @t181))) % 0.44/0.89 (assume @p347 (=> (= @t85 @t564) @t181)) % 0.44/0.89 (assume @p348 (forall (@list @t352) (=> @t455 (_ (_ tptp.ord_le318720350_set_a @t461) (_ tptp.pow_a @t72))))) % 0.44/0.89 (assume @p349 @t566) % 0.44/0.89 (assume @p350 true) % 0.44/0.89 (step @p351 (= tptp.locali880295127ng_a_b @t569) :rule refl :args (@t569)) % 0.44/0.89 (step @p352 (= tptp.monoid1242292471t_unit @t580) :rule refl :args (@t580)) % 0.44/0.89 (step @p353 (= tptp.monoid1022105667xt_a_b @t591) :rule refl :args (@t591)) % 0.44/0.89 (step @p354 (= tptp.ord_le1824328871od_a_a @t592) :rule refl :args (@t592)) % 0.44/0.89 (step @p355 (= tptp.ord_le391835783od_a_a @t593) :rule refl :args (@t593)) % 0.44/0.89 (step @p356 (= tptp.ord_less_eq_set_a @t594) :rule refl :args (@t594)) % 0.44/0.89 (step @p357 (= tptp.ord_le318720350_set_a @t595) :rule refl :args (@t595)) % 0.44/0.89 (step @p358 :rule eq-symm :args (@t596 @t597)) % 0.44/0.89 (step @p359 :rule refl :args (@t597)) % 0.44/0.89 (step @p360 :rule refl :args (@t2)) % 0.44/0.89 (step @p361 :rule cong :premises (@p360 @p359) :args ((= @t2 @t597))) % 0.44/0.89 (step @p362 :rule symm :premises (@p361)) % 0.44/0.89 (step @p363 :rule eq_resolve :premises (@p360 @p362)) % 0.44/0.89 (step @p364 :rule refl :args (@t596)) % 0.44/0.89 (step @p365 :rule refl :args (@t3)) % 0.44/0.89 (step @p366 :rule cong :premises (@p365 @p364) :args ((= @t3 @t596))) % 0.44/0.89 (step @p367 :rule symm :premises (@p366)) % 0.44/0.89 (step @p368 :rule eq_resolve :premises (@p365 @p367)) % 0.44/0.89 (step @p369 :rule cong :premises (@p368 @p363) :args (@t4)) % 0.44/0.89 (step @p370 :rule trans :premises (@p369 @p358)) % 0.44/0.89 (step @p371 :rule eq_resolve :premises (@p1 @p370)) % 0.44/0.89 (step @p372 :rule eq-symm :args (@t598 @t599)) % 0.44/0.89 (step @p373 :rule refl :args (@t599)) % 0.44/0.89 (step @p374 :rule refl :args (@t5)) % 0.44/0.89 (step @p375 :rule cong :premises (@p374 @p373) :args ((= @t5 @t599))) % 0.44/0.89 (step @p376 :rule symm :premises (@p375)) % 0.44/0.89 (step @p377 :rule eq_resolve :premises (@p374 @p376)) % 0.44/0.89 (step @p378 :rule refl :args (@t598)) % 0.44/0.89 (step @p379 :rule refl :args (@t6)) % 0.44/0.89 (step @p380 :rule cong :premises (@p379 @p378) :args ((= @t6 @t598))) % 0.44/0.89 (step @p381 :rule symm :premises (@p380)) % 0.44/0.89 (step @p382 :rule eq_resolve :premises (@p379 @p381)) % 0.44/0.89 (step @p383 :rule cong :premises (@p382 @p377) :args (@t7)) % 0.44/0.89 (step @p384 :rule trans :premises (@p383 @p372)) % 0.44/0.89 (step @p385 :rule eq_resolve :premises (@p2 @p384)) % 0.44/0.89 (step @p386 :rule eq-symm :args (@t603 @t604)) % 0.44/0.89 (step @p387 :rule refl :args ((tptp.locali1170246543t_unit tptp.rel @t3 @t6))) % 0.44/0.89 (step @p388 :rule refl :args (tptp.rel)) % 0.44/0.89 (step @p389 :rule cong :premises (@p388 @p364 @p378) :args (@t604)) % 0.44/0.89 (step @p390 :rule trans :premises (@p389 @p387)) % 0.44/0.89 (step @p391 :rule refl :args (@t8)) % 0.44/0.89 (step @p392 :rule ho_cong :premises (@p391 @p364)) % 0.44/0.89 (step @p393 :rule ho_cong :premises (@p392 @p378)) % 0.44/0.89 (step @p394 :rule cong :premises (@p393 @p390) :args ((= (_ (_ @t8 @t596) @t598) @t604))) % 0.44/0.89 (step @p395 :rule symm :premises (@p394)) % 0.44/0.89 (step @p396 :rule refl :args (@t9)) % 0.44/0.89 (step @p397 :rule eq_resolve :premises (@p396 @p395)) % 0.44/0.89 (step @p398 :rule refl :args (@t8)) % 0.44/0.89 (step @p399 :rule ho_cong :premises (@p398 @p368)) % 0.44/0.89 (step @p400 :rule ho_cong :premises (@p399 @p382)) % 0.44/0.89 (step @p401 :rule trans :premises (@p400 @p397)) % 0.44/0.89 (step @p402 :rule refl :args ((tptp.mult_s977248631t_unit @t12 @t11 @t10))) % 0.44/0.89 (step @p403 :rule refl :args (@t600)) % 0.44/0.89 (step @p404 :rule refl :args (@t601)) % 0.44/0.89 (step @p405 :rule refl :args (@t602)) % 0.44/0.89 (step @p406 :rule cong :premises (@p405 @p404 @p403) :args (@t603)) % 0.44/0.89 (step @p407 :rule trans :premises (@p406 @p402)) % 0.44/0.89 (step @p408 :rule refl :args (tptp.mult_s977248631t_unit)) % 0.44/0.89 (step @p409 :rule ho_cong :premises (@p408 @p405)) % 0.44/0.89 (step @p410 :rule ho_cong :premises (@p409 @p404)) % 0.44/0.89 (step @p411 :rule ho_cong :premises (@p410 @p403)) % 0.44/0.89 (step @p412 :rule cong :premises (@p411 @p407) :args ((= (_ (_ @t605 @t601) @t600) @t603))) % 0.44/0.89 (step @p413 :rule symm :premises (@p412)) % 0.44/0.89 (step @p414 :rule refl :args (@t14)) % 0.44/0.89 (step @p415 :rule eq_resolve :premises (@p414 @p413)) % 0.44/0.89 (step @p416 :rule refl :args (@t10)) % 0.44/0.89 (step @p417 :rule cong :premises (@p416 @p403) :args ((= @t10 @t600))) % 0.44/0.89 (step @p418 :rule symm :premises (@p417)) % 0.44/0.89 (step @p419 :rule eq_resolve :premises (@p416 @p418)) % 0.44/0.89 (step @p420 :rule refl :args (@t11)) % 0.44/0.89 (step @p421 :rule cong :premises (@p420 @p404) :args ((= @t11 @t601))) % 0.44/0.89 (step @p422 :rule symm :premises (@p421)) % 0.44/0.89 (step @p423 :rule eq_resolve :premises (@p420 @p422)) % 0.44/0.89 (step @p424 :rule refl :args (@t12)) % 0.44/0.89 (step @p425 :rule cong :premises (@p424 @p405) :args ((= @t12 @t602))) % 0.44/0.89 (step @p426 :rule symm :premises (@p425)) % 0.44/0.89 (step @p427 :rule eq_resolve :premises (@p424 @p426)) % 0.44/0.89 (step @p428 :rule refl :args (tptp.mult_s977248631t_unit)) % 0.44/0.89 (step @p429 :rule ho_cong :premises (@p428 @p427)) % 0.44/0.89 (step @p430 :rule ho_cong :premises (@p429 @p423)) % 0.44/0.89 (step @p431 :rule ho_cong :premises (@p430 @p419)) % 0.44/0.89 (step @p432 :rule trans :premises (@p431 @p415)) % 0.44/0.89 (step @p433 :rule cong :premises (@p432 @p401) :args (@t15)) % 0.44/0.89 (step @p434 :rule trans :premises (@p433 @p386)) % 0.44/0.89 (step @p435 :rule eq_resolve :premises (@p4 @p434)) % 0.44/0.89 (step @p436 :rule eq-symm :args (@t606 @t607)) % 0.44/0.89 (step @p437 :rule refl :args ((tptp.locali1170246543t_unit tptp.rel @t2 @t5))) % 0.44/0.89 (step @p438 :rule cong :premises (@p388 @p359 @p373) :args (@t607)) % 0.44/0.89 (step @p439 :rule trans :premises (@p438 @p437)) % 0.44/0.89 (step @p440 :rule ho_cong :premises (@p391 @p359)) % 0.44/0.89 (step @p441 :rule ho_cong :premises (@p440 @p373)) % 0.44/0.89 (step @p442 :rule cong :premises (@p441 @p439) :args ((= (_ (_ @t8 @t597) @t599) @t607))) % 0.44/0.89 (step @p443 :rule symm :premises (@p442)) % 0.44/0.89 (step @p444 :rule refl :args (@t16)) % 0.44/0.89 (step @p445 :rule eq_resolve :premises (@p444 @p443)) % 0.44/0.89 (step @p446 :rule ho_cong :premises (@p398 @p363)) % 0.44/0.89 (step @p447 :rule ho_cong :premises (@p446 @p377)) % 0.44/0.89 (step @p448 :rule trans :premises (@p447 @p445)) % 0.44/0.89 (step @p449 :rule refl :args ((tptp.mult_s977248631t_unit @t12 @t10 @t11))) % 0.44/0.89 (step @p450 :rule cong :premises (@p405 @p403 @p404) :args (@t606)) % 0.44/0.89 (step @p451 :rule trans :premises (@p450 @p449)) % 0.44/0.89 (step @p452 :rule ho_cong :premises (@p409 @p403)) % 0.44/0.89 (step @p453 :rule ho_cong :premises (@p452 @p404)) % 0.44/0.89 (step @p454 :rule cong :premises (@p453 @p451) :args ((= (_ (_ @t605 @t600) @t601) @t606))) % 0.44/0.89 (step @p455 :rule symm :premises (@p454)) % 0.44/0.89 (step @p456 :rule refl :args (@t17)) % 0.44/0.89 (step @p457 :rule eq_resolve :premises (@p456 @p455)) % 0.44/0.89 (step @p458 :rule ho_cong :premises (@p429 @p419)) % 0.44/0.89 (step @p459 :rule ho_cong :premises (@p458 @p423)) % 0.44/0.89 (step @p460 :rule trans :premises (@p459 @p457)) % 0.44/0.89 (step @p461 :rule cong :premises (@p460 @p448) :args (@t18)) % 0.44/0.89 (step @p462 :rule trans :premises (@p461 @p436)) % 0.44/0.89 (step @p463 :rule eq_resolve :premises (@p5 @p462)) % 0.44/0.89 (step @p464 :rule cong :premises (@p432 @p460) :args (@t565)) % 0.44/0.89 (step @p465 :rule cong :premises (@p464) :args (@t566)) % 0.44/0.89 (step @p466 :rule eq_resolve :premises (@p349 @p465)) % 0.44/0.89 (assume-push @p487 @t608) % 0.44/0.89 (assume-push @p488 @t609) % 0.44/0.89 (assume-push @p489 @t610) % 0.44/0.89 (assume-push @p490 @t611) % 0.44/0.89 (step @p471 :rule symm :premises (@p385)) % 0.44/0.89 (step @p472 :rule symm :premises (@p371)) % 0.44/0.89 (step @p473 :rule refl :args (tptp.rel)) % 0.44/0.89 (step @p474 :rule cong :premises (@p473 @p472 @p471) :args (@t604)) % 0.44/0.89 (step @p475 :rule symm :premises (@p435)) % 0.44/0.89 (step @p476 :rule trans :premises (@p475 @p474 @p463)) % 0.44/0.89 (step-pop @p491 :rule scope :premises (@p476)) % 0.44/0.89 (step-pop @p492 :rule scope :premises (@p491)) % 0.44/0.89 (step-pop @p493 :rule scope :premises (@p492)) % 0.44/0.89 (step-pop @p494 :rule scope :premises (@p493)) % 0.44/0.89 (step @p477 :rule process_scope :premises (@p494) :args (@t612)) % 0.44/0.89 (step @p482 :rule implies_elim :premises (@p477)) % 0.44/0.89 (step @p483 :rule cnf_and_neg :args (@t613)) % 0.44/0.89 (step @p484 :rule resolution :premises (@p483 @p482) :args (true @t613)) % 0.44/0.89 (step @p485 :rule reordering :premises (@p484) :args ((or @t612 (not @t608) (not @t609) (not @t610) (not @t611)))) % 0.44/0.89 (step @p486 false :rule chain_m_resolution :premises (@p485 @p466 @p463 @p435 @p385 @p371) :args (false (@list true false false false false) (@list @t612 @t611 @t610 @t609 @t608))) % 0.44/0.89 ) % 0.44/0.89 % SZS output end Proof % 0.44/0.89 % cvc5 exiting %------------------------------------------------------------------------------