%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWV547-1.007 : TPTP v9.2.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n021.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 09:01:54 AM UTC 2026 % Result : Unsatisfiable 0.39s 0.57s % Output : Proof 0.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV547-1.007 : TPTP v9.2.1. Released v4.0.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n021.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 20:43:05 EDT 2026 % 0.16/0.34 % CPUTime : % 0.32/0.50 %----Proving TF0_NAR, FOF, or CNF % 0.32/0.51 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.39/0.57 % SZS status Unsatisfiable % 0.39/0.57 % SZS output start Proof % 0.39/0.58 ( % 0.39/0.58 (declare-sort $$unsorted 0) % 0.39/0.58 (declare-const tptp.a_851 $$unsorted) % 0.39/0.58 (declare-const tptp.e_883 $$unsorted) % 0.39/0.58 (declare-const tptp.a_844 $$unsorted) % 0.39/0.58 (declare-const tptp.i5 $$unsorted) % 0.39/0.58 (declare-const tptp.a_871 $$unsorted) % 0.39/0.58 (declare-const tptp.e_843 $$unsorted) % 0.39/0.58 (declare-const tptp.a_842 $$unsorted) % 0.39/0.58 (declare-const tptp.i0 $$unsorted) % 0.39/0.58 (declare-const tptp.e_868 $$unsorted) % 0.39/0.58 (declare-const tptp.e_841 $$unsorted) % 0.39/0.58 (declare-const tptp.a_869 $$unsorted) % 0.39/0.58 (declare-const tptp.a_840 $$unsorted) % 0.39/0.58 (declare-const tptp.a_867 $$unsorted) % 0.39/0.58 (declare-const tptp.i1 $$unsorted) % 0.39/0.58 (declare-const tptp.e_839 $$unsorted) % 0.39/0.58 (declare-const tptp.e_866 $$unsorted) % 0.39/0.58 (declare-const tptp.e_849 $$unsorted) % 0.39/0.58 (declare-const tptp.e_852 $$unsorted) % 0.39/0.58 (declare-const tptp.select (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.58 (declare-const tptp.a_865 $$unsorted) % 0.39/0.58 (declare-const tptp.e_847 $$unsorted) % 0.39/0.58 (declare-const tptp.i3 $$unsorted) % 0.39/0.58 (declare-const tptp.a_861 $$unsorted) % 0.39/0.58 (declare-const tptp.sk (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.58 (declare-const tptp.e_845 $$unsorted) % 0.39/0.58 (declare-const tptp.e_833 $$unsorted) % 0.39/0.58 (declare-const tptp.i4 $$unsorted) % 0.39/0.58 (declare-const tptp.a1 $$unsorted) % 0.39/0.58 (declare-const tptp.a_859 $$unsorted) % 0.39/0.58 (declare-const tptp.a_838 $$unsorted) % 0.39/0.58 (declare-const tptp.e_864 $$unsorted) % 0.39/0.58 (declare-const tptp.a_846 $$unsorted) % 0.39/0.58 (declare-const tptp.e_873 $$unsorted) % 0.39/0.58 (declare-const tptp.a_834 $$unsorted) % 0.39/0.58 (declare-const tptp.a_860 $$unsorted) % 0.39/0.58 (declare-const tptp.a_848 $$unsorted) % 0.39/0.58 (declare-const tptp.e_875 $$unsorted) % 0.39/0.58 (declare-const tptp.e_835 $$unsorted) % 0.39/0.58 (declare-const tptp.store (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.39/0.58 (declare-const tptp.e_837 $$unsorted) % 0.39/0.58 (declare-const tptp.a_836 $$unsorted) % 0.39/0.58 (declare-const tptp.a_850 $$unsorted) % 0.39/0.58 (declare-const tptp.e_877 $$unsorted) % 0.39/0.58 (declare-const tptp.i2 $$unsorted) % 0.39/0.58 (declare-const tptp.a_853 $$unsorted) % 0.39/0.58 (declare-const tptp.e_854 $$unsorted) % 0.39/0.58 (declare-const tptp.a_855 $$unsorted) % 0.39/0.58 (declare-const tptp.e_856 $$unsorted) % 0.39/0.58 (declare-const tptp.a_857 $$unsorted) % 0.39/0.58 (declare-const tptp.e_858 $$unsorted) % 0.39/0.58 (declare-const tptp.e_862 $$unsorted) % 0.39/0.58 (declare-const tptp.a_863 $$unsorted) % 0.39/0.58 (declare-const tptp.e_870 $$unsorted) % 0.39/0.58 (declare-const tptp.a_872 $$unsorted) % 0.39/0.58 (declare-const tptp.a_874 $$unsorted) % 0.39/0.58 (declare-const tptp.i_881 $$unsorted) % 0.39/0.58 (declare-const tptp.a_876 $$unsorted) % 0.39/0.58 (declare-const tptp.a_878 $$unsorted) % 0.39/0.58 (declare-const tptp.e_879 $$unsorted) % 0.39/0.58 (declare-const tptp.a_880 $$unsorted) % 0.39/0.58 (declare-const tptp.e_882 $$unsorted) % 0.39/0.58 (define @t1 () (@var "E" $$unsorted)) % 0.39/0.58 (define @t2 () (@var "I" $$unsorted)) % 0.39/0.58 (define @t3 () (@var "A" $$unsorted)) % 0.39/0.58 (define @t4 () (tptp.store @t3 @t2 @t1)) % 0.39/0.58 (define @t5 () (tptp.select @t4 @t2)) % 0.39/0.58 (define @t6 () (forall (@list @t3 @t2 @t1) (= @t5 @t1))) % 0.39/0.58 (define @t7 () (@var "J" $$unsorted)) % 0.39/0.58 (define @t8 () (tptp.select @t3 @t7)) % 0.39/0.58 (define @t9 () (tptp.select @t3 @t2)) % 0.39/0.58 (define @t10 () (tptp.store tptp.a_836 tptp.i2 tptp.e_837)) % 0.39/0.58 (define @t11 () (= tptp.a_838 @t10)) % 0.39/0.58 (define @t12 () (tptp.store tptp.a_838 tptp.i1 tptp.e_839)) % 0.39/0.58 (define @t13 () (= tptp.a_840 @t12)) % 0.39/0.58 (define @t14 () (tptp.store tptp.a_840 tptp.i0 tptp.e_841)) % 0.39/0.58 (define @t15 () (= tptp.a_842 @t14)) % 0.39/0.58 (define @t16 () (tptp.store tptp.a_842 tptp.i5 tptp.e_843)) % 0.39/0.58 (define @t17 () (= tptp.a_844 @t16)) % 0.39/0.58 (define @t18 () (tptp.store tptp.a_844 tptp.i2 tptp.e_845)) % 0.39/0.58 (define @t19 () (= tptp.a_846 @t18)) % 0.39/0.58 (define @t20 () (tptp.store tptp.a_846 tptp.i5 tptp.e_847)) % 0.39/0.58 (define @t21 () (= tptp.a_848 @t20)) % 0.39/0.58 (define @t22 () (tptp.store tptp.a_848 tptp.i1 tptp.e_849)) % 0.39/0.58 (define @t23 () (= tptp.a_850 @t22)) % 0.39/0.58 (define @t24 () (tptp.store tptp.a_850 tptp.i1 tptp.e_849)) % 0.39/0.58 (define @t25 () (= tptp.a_851 @t24)) % 0.39/0.58 (define @t26 () (tptp.store tptp.a_851 tptp.i5 tptp.e_852)) % 0.39/0.58 (define @t27 () (= tptp.a_853 @t26)) % 0.39/0.58 (define @t28 () (tptp.store tptp.a_853 tptp.i2 tptp.e_854)) % 0.39/0.58 (define @t29 () (= tptp.a_855 @t28)) % 0.39/0.58 (define @t30 () (tptp.store tptp.a_855 tptp.i5 tptp.e_856)) % 0.39/0.58 (define @t31 () (= tptp.a_857 @t30)) % 0.39/0.58 (define @t32 () (tptp.store tptp.a_857 tptp.i2 tptp.e_858)) % 0.39/0.58 (define @t33 () (= tptp.a_859 @t32)) % 0.39/0.58 (define @t34 () (= tptp.a_860 (tptp.store tptp.a_836 tptp.i1 tptp.e_839))) % 0.39/0.58 (define @t35 () (= tptp.a_861 (tptp.store tptp.a_860 tptp.i2 tptp.e_837))) % 0.39/0.58 (define @t36 () (= tptp.a_863 (tptp.store tptp.a_861 tptp.i5 tptp.e_862))) % 0.39/0.58 (define @t37 () (= tptp.a_865 (tptp.store tptp.a_863 tptp.i0 tptp.e_864))) % 0.39/0.58 (define @t38 () (= tptp.a_867 (tptp.store tptp.a_865 tptp.i5 tptp.e_866))) % 0.39/0.58 (define @t39 () (= tptp.a_869 (tptp.store tptp.a_867 tptp.i2 tptp.e_868))) % 0.39/0.58 (define @t40 () (= tptp.a_871 (tptp.store tptp.a_869 tptp.i1 tptp.e_870))) % 0.39/0.58 (define @t41 () (= tptp.a_872 (tptp.store tptp.a_871 tptp.i1 tptp.e_870))) % 0.39/0.58 (define @t42 () (= tptp.a_874 (tptp.store tptp.a_872 tptp.i5 tptp.e_873))) % 0.39/0.58 (define @t43 () (tptp.store tptp.a_874 tptp.i2 tptp.e_875)) % 0.39/0.58 (define @t44 () (= tptp.a_876 @t43)) % 0.39/0.58 (define @t45 () (= tptp.a_878 (tptp.store tptp.a_876 tptp.i5 tptp.e_877))) % 0.39/0.58 (define @t46 () (= tptp.a_880 (tptp.store tptp.a_878 tptp.i2 tptp.e_879))) % 0.39/0.58 (define @t47 () (tptp.select tptp.a_836 tptp.i1)) % 0.39/0.58 (define @t48 () (= tptp.e_837 @t47)) % 0.39/0.58 (define @t49 () (tptp.select tptp.a_836 tptp.i2)) % 0.39/0.58 (define @t50 () (= tptp.e_839 @t49)) % 0.39/0.58 (define @t51 () (tptp.select tptp.a_840 tptp.i5)) % 0.39/0.58 (define @t52 () (= tptp.e_841 @t51)) % 0.39/0.58 (define @t53 () (tptp.select tptp.a_840 tptp.i0)) % 0.39/0.58 (define @t54 () (= tptp.e_843 @t53)) % 0.39/0.58 (define @t55 () (tptp.select tptp.a_844 tptp.i5)) % 0.39/0.58 (define @t56 () (= tptp.e_845 @t55)) % 0.39/0.58 (define @t57 () (tptp.select tptp.a_844 tptp.i2)) % 0.39/0.58 (define @t58 () (= tptp.e_847 @t57)) % 0.39/0.58 (define @t59 () (tptp.select tptp.a_848 tptp.i1)) % 0.39/0.58 (define @t60 () (= tptp.e_849 @t59)) % 0.39/0.58 (define @t61 () (tptp.select tptp.a_851 tptp.i2)) % 0.39/0.58 (define @t62 () (= tptp.e_852 @t61)) % 0.39/0.58 (define @t63 () (tptp.select tptp.a_851 tptp.i5)) % 0.39/0.58 (define @t64 () (= tptp.e_854 @t63)) % 0.39/0.58 (define @t65 () (tptp.select tptp.a_855 tptp.i2)) % 0.39/0.58 (define @t66 () (= tptp.e_856 @t65)) % 0.39/0.58 (define @t67 () (tptp.select tptp.a_855 tptp.i5)) % 0.39/0.58 (define @t68 () (= tptp.e_858 @t67)) % 0.39/0.58 (define @t69 () (= tptp.e_862 (tptp.select tptp.a_861 tptp.i0))) % 0.39/0.58 (define @t70 () (= tptp.e_864 (tptp.select tptp.a_861 tptp.i5))) % 0.39/0.58 (define @t71 () (= tptp.e_866 (tptp.select tptp.a_865 tptp.i2))) % 0.39/0.58 (define @t72 () (= tptp.e_868 (tptp.select tptp.a_865 tptp.i5))) % 0.39/0.58 (define @t73 () (= tptp.e_870 (tptp.select tptp.a_869 tptp.i1))) % 0.39/0.58 (define @t74 () (= tptp.e_873 (tptp.select tptp.a_872 tptp.i2))) % 0.39/0.58 (define @t75 () (= tptp.e_875 (tptp.select tptp.a_872 tptp.i5))) % 0.39/0.58 (define @t76 () (tptp.select tptp.a_876 tptp.i2)) % 0.39/0.58 (define @t77 () (= tptp.e_877 @t76)) % 0.39/0.58 (define @t78 () (= tptp.e_879 (tptp.select tptp.a_876 tptp.i5))) % 0.39/0.58 (define @t79 () (tptp.select tptp.a_859 tptp.i_881)) % 0.39/0.58 (define @t80 () (= tptp.e_882 @t79)) % 0.39/0.58 (define @t81 () (= tptp.e_883 (tptp.select tptp.a_880 tptp.i_881))) % 0.39/0.58 (define @t82 () (= tptp.e_882 tptp.e_883)) % 0.39/0.58 (define @t83 () (= tptp.e_854 (tptp.select @t28 tptp.i2))) % 0.39/0.58 (define @t84 () (tptp.select @t43 tptp.i2)) % 0.39/0.58 (define @t85 () (= tptp.e_875 @t84)) % 0.39/0.58 (define @t86 () (tptp.store tptp.a_836 tptp.i1 @t49)) % 0.39/0.58 (define @t87 () (tptp.store @t86 tptp.i2 @t47)) % 0.39/0.58 (define @t88 () (= (tptp.store (tptp.store tptp.a_836 tptp.i2 @t47) tptp.i1 @t49) @t87)) % 0.39/0.58 (define @t89 () (tptp.store tptp.a_840 tptp.i5 @t53)) % 0.39/0.58 (define @t90 () (tptp.store @t89 tptp.i0 @t51)) % 0.39/0.58 (define @t91 () (= (tptp.store (tptp.store tptp.a_840 tptp.i0 @t51) tptp.i5 @t53) @t90)) % 0.39/0.58 (define @t92 () (tptp.store tptp.a_844 tptp.i5 @t57)) % 0.39/0.58 (define @t93 () (tptp.store @t92 tptp.i2 @t55)) % 0.39/0.58 (define @t94 () (= (tptp.store (tptp.store tptp.a_844 tptp.i2 @t55) tptp.i5 @t57) @t93)) % 0.39/0.58 (define @t95 () (and @t11 @t13 @t15 @t17 @t19 @t21 @t23 @t25 @t27 @t29 @t31 @t33 @t34 @t35 @t36 @t37 @t38 @t39 @t40 @t41 @t42 @t44 @t45 @t46 @t48 @t50 @t52 @t54 @t56 @t58 @t60 @t62 @t64 @t66 @t68 @t69 @t70 @t71 @t72 @t73 @t74 @t75 @t77 @t78 @t80 @t81 @t83 @t85 @t88 @t91 @t94)) % 0.39/0.58 (assume @p1 @t6) % 0.39/0.58 (assume @p2 (forall (@list @t2 @t7 @t3 @t1) (or (= @t2 @t7) (= (tptp.select @t4 @t7) @t8)))) % 0.39/0.58 (assume @p3 (forall (@list @t3 @t2 @t7) (= (tptp.store (tptp.store @t3 @t2 @t8) @t7 @t9) (tptp.store (tptp.store @t3 @t7 @t9) @t2 @t8)))) % 0.39/0.58 (assume @p4 (= tptp.a_834 (tptp.store tptp.a1 tptp.i4 tptp.e_833))) % 0.39/0.58 (assume @p5 (= tptp.a_836 (tptp.store tptp.a_834 tptp.i3 tptp.e_835))) % 0.39/0.58 (assume @p6 @t11) % 0.39/0.58 (assume @p7 @t13) % 0.39/0.58 (assume @p8 @t15) % 0.39/0.58 (assume @p9 @t17) % 0.39/0.58 (assume @p10 @t19) % 0.39/0.58 (assume @p11 @t21) % 0.39/0.58 (assume @p12 @t23) % 0.39/0.58 (assume @p13 @t25) % 0.39/0.58 (assume @p14 @t27) % 0.39/0.58 (assume @p15 @t29) % 0.39/0.58 (assume @p16 @t31) % 0.39/0.58 (assume @p17 @t33) % 0.39/0.58 (assume @p18 @t34) % 0.39/0.58 (assume @p19 @t35) % 0.39/0.58 (assume @p20 @t36) % 0.39/0.58 (assume @p21 @t37) % 0.39/0.58 (assume @p22 @t38) % 0.39/0.58 (assume @p23 @t39) % 0.39/0.58 (assume @p24 @t40) % 0.39/0.58 (assume @p25 @t41) % 0.39/0.58 (assume @p26 @t42) % 0.39/0.58 (assume @p27 @t44) % 0.39/0.58 (assume @p28 @t45) % 0.39/0.58 (assume @p29 @t46) % 0.39/0.58 (assume @p30 (= tptp.e_833 (tptp.select tptp.a1 tptp.i3))) % 0.39/0.58 (assume @p31 (= tptp.e_835 (tptp.select tptp.a1 tptp.i4))) % 0.39/0.58 (assume @p32 @t48) % 0.39/0.58 (assume @p33 @t50) % 0.39/0.58 (assume @p34 @t52) % 0.39/0.58 (assume @p35 @t54) % 0.39/0.58 (assume @p36 @t56) % 0.39/0.58 (assume @p37 @t58) % 0.39/0.58 (assume @p38 @t60) % 0.39/0.58 (assume @p39 @t62) % 0.39/0.58 (assume @p40 @t64) % 0.39/0.58 (assume @p41 @t66) % 0.39/0.58 (assume @p42 @t68) % 0.39/0.58 (assume @p43 @t69) % 0.39/0.58 (assume @p44 @t70) % 0.39/0.58 (assume @p45 @t71) % 0.39/0.58 (assume @p46 @t72) % 0.39/0.58 (assume @p47 @t73) % 0.39/0.58 (assume @p48 @t74) % 0.39/0.58 (assume @p49 @t75) % 0.39/0.58 (assume @p50 @t77) % 0.39/0.58 (assume @p51 @t78) % 0.39/0.58 (assume @p52 @t80) % 0.39/0.58 (assume @p53 @t81) % 0.39/0.58 (assume @p54 (= tptp.i_881 (tptp.sk tptp.a_859 tptp.a_880))) % 0.39/0.58 (assume @p55 (not @t82)) % 0.39/0.58 (step @p56 :rule eq-symm :args (@t5 @t1)) % 0.39/0.58 (step @p57 :rule cong :premises (@p56) :args (@t6)) % 0.39/0.58 (step @p58 :rule eq_resolve :premises (@p1 @p57)) % 0.39/0.58 (step @p59 :rule instantiate :premises (@p58) :args ((@list tptp.a_853 tptp.i2 tptp.e_854))) % 0.39/0.58 (step @p60 :rule instantiate :premises (@p58) :args ((@list tptp.a_874 tptp.i2 tptp.e_875))) % 0.39/0.58 (step @p61 :rule instantiate :premises (@p3) :args ((@list tptp.a_836 tptp.i2 tptp.i1))) % 0.39/0.58 (step @p62 :rule instantiate :premises (@p3) :args ((@list tptp.a_840 tptp.i0 tptp.i5))) % 0.39/0.58 (step @p63 :rule instantiate :premises (@p3) :args ((@list tptp.a_844 tptp.i2 tptp.i5))) % 0.39/0.58 (assume-push @p278 @t11) % 0.39/0.58 (assume-push @p279 @t13) % 0.39/0.58 (assume-push @p280 @t15) % 0.39/0.58 (assume-push @p281 @t17) % 0.39/0.58 (assume-push @p282 @t19) % 0.39/0.58 (assume-push @p283 @t21) % 0.39/0.58 (assume-push @p284 @t23) % 0.39/0.58 (assume-push @p285 @t25) % 0.39/0.58 (assume-push @p286 @t27) % 0.39/0.58 (assume-push @p287 @t29) % 0.39/0.58 (assume-push @p288 @t31) % 0.39/0.58 (assume-push @p289 @t33) % 0.39/0.58 (assume-push @p290 @t34) % 0.39/0.58 (assume-push @p291 @t35) % 0.39/0.58 (assume-push @p292 @t36) % 0.39/0.58 (assume-push @p293 @t37) % 0.39/0.58 (assume-push @p294 @t38) % 0.39/0.58 (assume-push @p295 @t39) % 0.39/0.58 (assume-push @p296 @t40) % 0.39/0.58 (assume-push @p297 @t41) % 0.39/0.58 (assume-push @p298 @t42) % 0.39/0.58 (assume-push @p299 @t44) % 0.39/0.58 (assume-push @p300 @t45) % 0.39/0.58 (assume-push @p301 @t46) % 0.39/0.58 (assume-push @p302 @t48) % 0.39/0.58 (assume-push @p303 @t50) % 0.39/0.58 (assume-push @p304 @t52) % 0.39/0.58 (assume-push @p305 @t54) % 0.39/0.58 (assume-push @p306 @t56) % 0.39/0.58 (assume-push @p307 @t58) % 0.39/0.58 (assume-push @p308 @t60) % 0.39/0.58 (assume-push @p309 @t62) % 0.39/0.58 (assume-push @p310 @t64) % 0.39/0.58 (assume-push @p311 @t66) % 0.39/0.58 (assume-push @p312 @t68) % 0.39/0.58 (assume-push @p313 @t69) % 0.39/0.58 (assume-push @p314 @t70) % 0.39/0.58 (assume-push @p315 @t71) % 0.39/0.58 (assume-push @p316 @t72) % 0.39/0.58 (assume-push @p317 @t73) % 0.39/0.58 (assume-push @p318 @t74) % 0.39/0.58 (assume-push @p319 @t75) % 0.39/0.58 (assume-push @p320 @t77) % 0.39/0.58 (assume-push @p321 @t78) % 0.39/0.58 (assume-push @p322 @t80) % 0.39/0.58 (assume-push @p323 @t81) % 0.39/0.58 (assume-push @p324 @t83) % 0.39/0.58 (assume-push @p325 @t85) % 0.39/0.58 (assume-push @p326 @t88) % 0.39/0.58 (assume-push @p327 @t91) % 0.39/0.58 (assume-push @p328 @t94) % 0.39/0.58 (step @p115 :rule symm :premises (@p53)) % 0.39/0.58 (step @p116 :rule refl :args (tptp.i_881)) % 0.39/0.58 (step @p117 :rule symm :premises (@p29)) % 0.39/0.58 (step @p118 :rule symm :premises (@p51)) % 0.39/0.58 (step @p119 :rule refl :args (tptp.i5)) % 0.39/0.58 (step @p120 :rule symm :premises (@p27)) % 0.39/0.58 (step @p121 :rule symm :premises (@p49)) % 0.39/0.58 (step @p122 :rule symm :premises (@p25)) % 0.39/0.58 (step @p123 :rule symm :premises (@p47)) % 0.39/0.58 (step @p124 :rule refl :args (tptp.i1)) % 0.39/0.58 (step @p125 :rule symm :premises (@p23)) % 0.39/0.58 (step @p126 :rule symm :premises (@p46)) % 0.39/0.58 (step @p127 :rule symm :premises (@p21)) % 0.39/0.58 (step @p128 :rule symm :premises (@p44)) % 0.39/0.58 (step @p129 :rule symm :premises (@p19)) % 0.39/0.58 (step @p130 :rule symm :premises (@p32)) % 0.39/0.58 (step @p131 :rule refl :args (tptp.i2)) % 0.39/0.58 (step @p132 :rule symm :premises (@p18)) % 0.39/0.58 (step @p133 :rule symm :premises (@p33)) % 0.39/0.58 (step @p134 :rule refl :args (tptp.a_836)) % 0.39/0.58 (step @p135 :rule cong :premises (@p134 @p124 @p133) :args (@t86)) % 0.39/0.58 (step @p136 :rule trans :premises (@p135 @p132)) % 0.39/0.58 (step @p137 :rule cong :premises (@p136 @p131 @p130) :args (@t87)) % 0.39/0.58 (step @p138 :rule cong :premises (@p134 @p131 @p32) :args (@t10)) % 0.39/0.58 (step @p139 :rule trans :premises (@p6 @p138)) % 0.39/0.58 (step @p140 :rule cong :premises (@p139 @p124 @p33) :args (@t12)) % 0.39/0.58 (step @p141 :rule trans :premises (@p7 @p140 @p61 @p137 @p129)) % 0.39/0.58 (step @p142 :rule symm :premises (@p7)) % 0.39/0.58 (step @p143 :rule trans :premises (@p142 @p141)) % 0.39/0.58 (step @p144 :rule cong :premises (@p143 @p119) :args ((tptp.select @t12 tptp.i5))) % 0.39/0.58 (step @p145 :rule cong :premises (@p7 @p119) :args (@t51)) % 0.39/0.58 (step @p146 :rule trans :premises (@p145 @p144 @p128)) % 0.39/0.58 (step @p147 :rule refl :args (tptp.i0)) % 0.39/0.58 (step @p148 :rule symm :premises (@p20)) % 0.39/0.58 (step @p149 :rule symm :premises (@p43)) % 0.39/0.58 (step @p150 :rule cong :premises (@p141 @p147) :args (@t53)) % 0.39/0.58 (step @p151 :rule trans :premises (@p150 @p149)) % 0.39/0.58 (step @p152 :rule cong :premises (@p141 @p119 @p151) :args (@t89)) % 0.39/0.58 (step @p153 :rule trans :premises (@p152 @p148)) % 0.39/0.58 (step @p154 :rule cong :premises (@p153 @p147 @p146) :args (@t90)) % 0.39/0.58 (step @p155 :rule refl :args (tptp.a_840)) % 0.39/0.58 (step @p156 :rule cong :premises (@p155 @p147 @p34) :args (@t14)) % 0.39/0.58 (step @p157 :rule trans :premises (@p8 @p156)) % 0.39/0.58 (step @p158 :rule cong :premises (@p157 @p119 @p35) :args (@t16)) % 0.39/0.58 (step @p159 :rule trans :premises (@p9 @p158 @p62 @p154 @p127)) % 0.39/0.58 (step @p160 :rule symm :premises (@p9)) % 0.39/0.58 (step @p161 :rule trans :premises (@p160 @p159)) % 0.39/0.58 (step @p162 :rule cong :premises (@p161 @p119) :args ((tptp.select @t16 tptp.i5))) % 0.39/0.58 (step @p163 :rule cong :premises (@p9 @p119) :args (@t55)) % 0.39/0.58 (step @p164 :rule trans :premises (@p163 @p162 @p126)) % 0.39/0.58 (step @p165 :rule symm :premises (@p22)) % 0.39/0.58 (step @p166 :rule symm :premises (@p45)) % 0.39/0.58 (step @p167 :rule cong :premises (@p159 @p131) :args (@t57)) % 0.39/0.58 (step @p168 :rule trans :premises (@p167 @p166)) % 0.39/0.58 (step @p169 :rule cong :premises (@p159 @p119 @p168) :args (@t92)) % 0.39/0.58 (step @p170 :rule trans :premises (@p169 @p165)) % 0.39/0.58 (step @p171 :rule cong :premises (@p170 @p131 @p164) :args (@t93)) % 0.39/0.58 (step @p172 :rule refl :args (tptp.a_844)) % 0.39/0.58 (step @p173 :rule cong :premises (@p172 @p131 @p36) :args (@t18)) % 0.39/0.58 (step @p174 :rule trans :premises (@p10 @p173)) % 0.39/0.58 (step @p175 :rule cong :premises (@p174 @p119 @p37) :args (@t20)) % 0.39/0.58 (step @p176 :rule trans :premises (@p11 @p175 @p63 @p171 @p125)) % 0.39/0.58 (step @p177 :rule symm :premises (@p11)) % 0.39/0.58 (step @p178 :rule trans :premises (@p177 @p176)) % 0.39/0.58 (step @p179 :rule cong :premises (@p178 @p124) :args ((tptp.select @t20 tptp.i1))) % 0.39/0.58 (step @p180 :rule cong :premises (@p11 @p124) :args (@t59)) % 0.39/0.58 (step @p181 :rule trans :premises (@p38 @p180 @p179 @p123)) % 0.39/0.58 (step @p182 :rule symm :premises (@p24)) % 0.39/0.58 (step @p183 :rule cong :premises (@p176 @p124 @p181) :args (@t22)) % 0.39/0.58 (step @p184 :rule trans :premises (@p12 @p183 @p182)) % 0.39/0.58 (step @p185 :rule cong :premises (@p184 @p124 @p181) :args (@t24)) % 0.39/0.58 (step @p186 :rule trans :premises (@p13 @p185 @p122)) % 0.39/0.58 (step @p187 :rule cong :premises (@p186 @p119) :args (@t63)) % 0.39/0.58 (step @p188 :rule trans :premises (@p40 @p187 @p121)) % 0.39/0.58 (step @p189 :rule symm :premises (@p26)) % 0.39/0.58 (step @p190 :rule symm :premises (@p48)) % 0.39/0.58 (step @p191 :rule symm :premises (@p13)) % 0.39/0.58 (step @p192 :rule trans :premises (@p191 @p186)) % 0.39/0.58 (step @p193 :rule cong :premises (@p192 @p131) :args ((tptp.select @t24 tptp.i2))) % 0.39/0.58 (step @p194 :rule cong :premises (@p13 @p131) :args (@t61)) % 0.39/0.58 (step @p195 :rule trans :premises (@p194 @p193 @p190)) % 0.39/0.58 (step @p196 :rule cong :premises (@p186 @p119 @p195) :args ((tptp.store tptp.a_851 tptp.i5 @t61))) % 0.39/0.58 (step @p197 :rule refl :args (tptp.a_851)) % 0.39/0.58 (step @p198 :rule cong :premises (@p197 @p119 @p39) :args (@t26)) % 0.39/0.58 (step @p199 :rule trans :premises (@p14 @p198 @p196 @p189)) % 0.39/0.58 (step @p200 :rule cong :premises (@p199 @p131 @p188) :args (@t28)) % 0.39/0.58 (step @p201 :rule trans :premises (@p15 @p200 @p120)) % 0.39/0.58 (step @p202 :rule cong :premises (@p201 @p119) :args (@t67)) % 0.39/0.58 (step @p203 :rule trans :premises (@p42 @p202 @p118)) % 0.39/0.58 (step @p204 :rule symm :premises (@p28)) % 0.39/0.58 (step @p205 :rule symm :premises (@p50)) % 0.39/0.58 (step @p206 :rule refl :args (tptp.a_876)) % 0.39/0.58 (step @p207 :rule cong :premises (@p206 @p119 @p205) :args ((tptp.store tptp.a_876 tptp.i5 @t76))) % 0.39/0.58 (step @p208 :rule cong :premises (@p120 @p131) :args (@t84)) % 0.39/0.58 (step @p209 :rule symm :premises (@p59)) % 0.39/0.58 (step @p210 :rule cong :premises (@p15 @p131) :args (@t65)) % 0.39/0.58 (step @p211 :rule trans :premises (@p41 @p210 @p209 @p40 @p187 @p121 @p60 @p208)) % 0.39/0.58 (step @p212 :rule cong :premises (@p201 @p119 @p211) :args (@t30)) % 0.39/0.58 (step @p213 :rule trans :premises (@p16 @p212 @p207 @p204)) % 0.39/0.58 (step @p214 :rule cong :premises (@p213 @p131 @p203) :args (@t32)) % 0.39/0.58 (step @p215 :rule trans :premises (@p17 @p214 @p117)) % 0.39/0.58 (step @p216 :rule symm :premises (@p17)) % 0.39/0.58 (step @p217 :rule trans :premises (@p216 @p215)) % 0.39/0.58 (step @p218 :rule cong :premises (@p217 @p116) :args ((tptp.select @t32 tptp.i_881))) % 0.39/0.58 (step @p219 :rule cong :premises (@p17 @p116) :args (@t79)) % 0.39/0.58 (step @p220 :rule trans :premises (@p52 @p219 @p218 @p115)) % 0.39/0.58 (step-pop @p329 :rule scope :premises (@p220)) % 0.39/0.58 (step-pop @p330 :rule scope :premises (@p329)) % 0.39/0.58 (step-pop @p331 :rule scope :premises (@p330)) % 0.39/0.58 (step-pop @p332 :rule scope :premises (@p331)) % 0.39/0.58 (step-pop @p333 :rule scope :premises (@p332)) % 0.39/0.58 (step-pop @p334 :rule scope :premises (@p333)) % 0.39/0.58 (step-pop @p335 :rule scope :premises (@p334)) % 0.39/0.58 (step-pop @p336 :rule scope :premises (@p335)) % 0.39/0.58 (step-pop @p337 :rule scope :premises (@p336)) % 0.39/0.58 (step-pop @p338 :rule scope :premises (@p337)) % 0.39/0.58 (step-pop @p339 :rule scope :premises (@p338)) % 0.39/0.58 (step-pop @p340 :rule scope :premises (@p339)) % 0.39/0.58 (step-pop @p341 :rule scope :premises (@p340)) % 0.39/0.58 (step-pop @p342 :rule scope :premises (@p341)) % 0.39/0.58 (step-pop @p343 :rule scope :premises (@p342)) % 0.39/0.58 (step-pop @p344 :rule scope :premises (@p343)) % 0.39/0.58 (step-pop @p345 :rule scope :premises (@p344)) % 0.39/0.58 (step-pop @p346 :rule scope :premises (@p345)) % 0.39/0.58 (step-pop @p347 :rule scope :premises (@p346)) % 0.39/0.58 (step-pop @p348 :rule scope :premises (@p347)) % 0.39/0.58 (step-pop @p349 :rule scope :premises (@p348)) % 0.39/0.58 (step-pop @p350 :rule scope :premises (@p349)) % 0.39/0.58 (step-pop @p351 :rule scope :premises (@p350)) % 0.39/0.58 (step-pop @p352 :rule scope :premises (@p351)) % 0.39/0.58 (step-pop @p353 :rule scope :premises (@p352)) % 0.39/0.58 (step-pop @p354 :rule scope :premises (@p353)) % 0.39/0.58 (step-pop @p355 :rule scope :premises (@p354)) % 0.39/0.58 (step-pop @p356 :rule scope :premises (@p355)) % 0.39/0.58 (step-pop @p357 :rule scope :premises (@p356)) % 0.39/0.58 (step-pop @p358 :rule scope :premises (@p357)) % 0.39/0.58 (step-pop @p359 :rule scope :premises (@p358)) % 0.39/0.58 (step-pop @p360 :rule scope :premises (@p359)) % 0.39/0.58 (step-pop @p361 :rule scope :premises (@p360)) % 0.39/0.58 (step-pop @p362 :rule scope :premises (@p361)) % 0.39/0.58 (step-pop @p363 :rule scope :premises (@p362)) % 0.39/0.58 (step-pop @p364 :rule scope :premises (@p363)) % 0.39/0.58 (step-pop @p365 :rule scope :premises (@p364)) % 0.39/0.58 (step-pop @p366 :rule scope :premises (@p365)) % 0.39/0.58 (step-pop @p367 :rule scope :premises (@p366)) % 0.39/0.58 (step-pop @p368 :rule scope :premises (@p367)) % 0.39/0.58 (step-pop @p369 :rule scope :premises (@p368)) % 0.39/0.58 (step-pop @p370 :rule scope :premises (@p369)) % 0.39/0.58 (step-pop @p371 :rule scope :premises (@p370)) % 0.39/0.58 (step-pop @p372 :rule scope :premises (@p371)) % 0.39/0.58 (step-pop @p373 :rule scope :premises (@p372)) % 0.39/0.58 (step-pop @p374 :rule scope :premises (@p373)) % 0.39/0.58 (step-pop @p375 :rule scope :premises (@p374)) % 0.39/0.58 (step-pop @p376 :rule scope :premises (@p375)) % 0.39/0.58 (step-pop @p377 :rule scope :premises (@p376)) % 0.39/0.58 (step-pop @p378 :rule scope :premises (@p377)) % 0.39/0.58 (step-pop @p379 :rule scope :premises (@p378)) % 0.39/0.58 (step @p221 :rule process_scope :premises (@p379) :args (@t82)) % 0.39/0.58 (step @p273 :rule implies_elim :premises (@p221)) % 0.39/0.58 (step @p274 :rule cnf_and_neg :args (@t95)) % 0.39/0.58 (step @p275 :rule resolution :premises (@p274 @p273) :args (true @t95)) % 0.39/0.58 (step @p276 :rule reordering :premises (@p275) :args ((or @t82 (not @t11) (not @t13) (not @t15) (not @t17) (not @t19) (not @t21) (not @t23) (not @t25) (not @t27) (not @t29) (not @t31) (not @t33) (not @t34) (not @t35) (not @t36) (not @t37) (not @t38) (not @t39) (not @t40) (not @t41) (not @t42) (not @t44) (not @t45) (not @t46) (not @t48) (not @t50) (not @t52) (not @t54) (not @t56) (not @t58) (not @t60) (not @t62) (not @t64) (not @t66) (not @t68) (not @t69) (not @t70) (not @t71) (not @t72) (not @t73) (not @t74) (not @t75) (not @t77) (not @t78) (not @t80) (not @t81) (not @t83) (not @t85) (not @t88) (not @t91) (not @t94)))) % 0.39/0.58 (step @p277 false :rule chain_m_resolution :premises (@p276 @p63 @p62 @p61 @p60 @p59 @p55 @p53 @p52 @p51 @p50 @p49 @p48 @p47 @p46 @p45 @p44 @p43 @p42 @p41 @p40 @p39 @p38 @p37 @p36 @p35 @p34 @p33 @p32 @p29 @p28 @p27 @p26 @p25 @p24 @p23 @p22 @p21 @p20 @p19 @p18 @p17 @p16 @p15 @p14 @p13 @p12 @p11 @p10 @p9 @p8 @p7 @p6) :args (false (@list false false false false false true false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false) (@list @t94 @t91 @t88 @t85 @t83 @t82 @t81 @t80 @t78 @t77 @t75 @t74 @t73 @t72 @t71 @t70 @t69 @t68 @t66 @t64 @t62 @t60 @t58 @t56 @t54 @t52 @t50 @t48 @t46 @t45 @t44 @t42 @t41 @t40 @t39 @t38 @t37 @t36 @t35 @t34 @t33 @t31 @t29 @t27 @t25 @t23 @t21 @t19 @t17 @t15 @t13 @t11))) % 0.39/0.58 ) % 0.39/0.58 % SZS output end Proof % 0.39/0.58 % cvc5 exiting %------------------------------------------------------------------------------