%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SYO040^2 : TPTP v9.2.1. Released v4.1.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 09:11:50 AM UTC 2026 % Result : Theorem 0.38s 0.57s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYO040^2 : TPTP v9.2.1. Released v4.1.0. % 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.35 % Computer : n010.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue Jun 2 23:51:55 EDT 2026 % 0.17/0.35 % CPUTime : % 0.28/0.50 %----Proving TH0 % 0.38/0.57 --- 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.38/0.57 % SZS status Theorem % 0.38/0.57 % SZS output start Proof % 0.38/0.57 ( % 0.38/0.57 (declare-sort $$unsorted 0) % 0.38/0.57 (declare-const tptp.h (-> Bool $$unsorted)) % 0.38/0.57 (declare-const tptp.f (-> Bool Bool)) % 0.38/0.57 (declare-const tptp.x Bool) % 0.38/0.57 (define @t1 () (_ tptp.f tptp.x)) % 0.38/0.57 (define @t2 () (_ tptp.f @t1)) % 0.38/0.57 (define @t3 () (_ tptp.f @t2)) % 0.38/0.57 (define @t4 () (= (_ tptp.h @t3) (_ tptp.h @t1))) % 0.38/0.57 (define @t5 () (not @t4)) % 0.38/0.57 (define @t6 () (@purify @t3)) % 0.38/0.57 (define @t7 () (tptp.h @t6)) % 0.38/0.57 (define @t8 () (@purify @t1)) % 0.38/0.57 (define @t9 () (tptp.h @t8)) % 0.38/0.57 (define @t10 () (_ tptp.h @t8)) % 0.38/0.57 (define @t11 () (= @t1 @t8)) % 0.38/0.57 (define @t12 () (_ tptp.h @t6)) % 0.38/0.57 (define @t13 () (= @t3 @t6)) % 0.38/0.57 (define @t14 () (@purify tptp.x)) % 0.38/0.57 (define @t15 () (tptp.f @t14)) % 0.38/0.57 (define @t16 () (_ tptp.f @t14)) % 0.38/0.57 (define @t17 () (not @t8)) % 0.38/0.57 (define @t18 () (= @t9 @t7)) % 0.38/0.57 (define @t19 () (and @t8 @t6)) % 0.38/0.57 (define @t20 () (not @t6)) % 0.38/0.57 (define @t21 () (@purify @t2)) % 0.38/0.57 (define @t22 () (tptp.f @t21)) % 0.38/0.57 (define @t23 () (_ tptp.f @t21)) % 0.38/0.57 (define @t24 () (= @t2 @t21)) % 0.38/0.57 (define @t25 () (tptp.f @t8)) % 0.38/0.57 (define @t26 () (and @t8 @t14 @t15)) % 0.38/0.57 (define @t27 () (not @t14)) % 0.38/0.57 (define @t28 () (not @t15)) % 0.38/0.57 (define @t29 () (_ tptp.f @t8)) % 0.38/0.57 (define @t30 () (not @t21)) % 0.38/0.57 (define @t31 () (not @t22)) % 0.38/0.57 (define @t32 () (not @t31)) % 0.38/0.57 (define @t33 () (= false true)) % 0.38/0.57 (define @t34 () (and @t15 @t14 @t8 @t21 @t31)) % 0.38/0.57 (define @t35 () (not @t25)) % 0.38/0.57 (define @t36 () (and @t8 @t21 @t31)) % 0.38/0.57 (define @t37 () (not @t30)) % 0.38/0.57 (define @t38 () (not @t27)) % 0.38/0.57 (define @t39 () (and @t15 @t27 @t30 @t31)) % 0.38/0.57 (define @t40 () (not @t17)) % 0.38/0.57 (define @t41 () (and @t22 @t17 @t30)) % 0.38/0.57 (define @t42 () (@list true)) % 0.38/0.57 (define @t43 () (not @t28)) % 0.38/0.57 (define @t44 () (and @t28 @t14 @t21 @t22)) % 0.38/0.57 (define @t45 () (and @t25 @t17 @t27 @t28)) % 0.38/0.57 (define @t46 () (and @t17 @t20)) % 0.38/0.57 (assume @p1 @t5) % 0.38/0.57 (assume @p2 true) % 0.38/0.57 (step @p3 :rule eq-symm :args (@t7 @t9)) % 0.38/0.57 (step @p4 :rule refl :args (@t9)) % 0.38/0.57 (step @p5 :rule refl :args (@t10)) % 0.38/0.57 (step @p6 :rule cong :premises (@p5 @p4) :args ((= @t10 @t9))) % 0.38/0.57 (step @p7 :rule symm :premises (@p6)) % 0.38/0.57 (step @p8 :rule eq_resolve :premises (@p5 @p7)) % 0.38/0.57 (step @p9 :rule eq-refl :args (@t1)) % 0.38/0.57 (step @p10 :rule skolem_intro :args (@t8)) % 0.38/0.57 (step @p11 :rule refl :args (@t1)) % 0.38/0.57 (step @p12 :rule cong :premises (@p11 @p10) :args (@t11)) % 0.38/0.57 (step @p13 :rule trans :premises (@p12 @p9)) % 0.38/0.57 (step @p14 :rule true_elim :premises (@p13)) % 0.38/0.57 (step @p15 :rule refl :args (tptp.h)) % 0.38/0.57 (step @p16 :rule ho_cong :premises (@p15 @p14)) % 0.38/0.57 (step @p17 :rule trans :premises (@p16 @p8)) % 0.38/0.57 (step @p18 :rule refl :args (@t7)) % 0.38/0.57 (step @p19 :rule refl :args (@t12)) % 0.38/0.57 (step @p20 :rule cong :premises (@p19 @p18) :args ((= @t12 @t7))) % 0.38/0.57 (step @p21 :rule symm :premises (@p20)) % 0.38/0.57 (step @p22 :rule eq_resolve :premises (@p19 @p21)) % 0.38/0.57 (step @p23 :rule eq-refl :args (@t3)) % 0.38/0.57 (step @p24 :rule skolem_intro :args (@t6)) % 0.38/0.57 (step @p25 :rule refl :args (@t3)) % 0.38/0.57 (step @p26 :rule cong :premises (@p25 @p24) :args (@t13)) % 0.38/0.57 (step @p27 :rule trans :premises (@p26 @p23)) % 0.38/0.57 (step @p28 :rule true_elim :premises (@p27)) % 0.38/0.57 (step @p29 :rule ho_cong :premises (@p15 @p28)) % 0.38/0.57 (step @p30 :rule trans :premises (@p29 @p22)) % 0.38/0.57 (step @p31 :rule cong :premises (@p30 @p17) :args (@t4)) % 0.38/0.57 (step @p32 :rule trans :premises (@p31 @p3)) % 0.38/0.57 (step @p33 :rule cong :premises (@p32) :args (@t5)) % 0.38/0.57 (step @p34 :rule eq_resolve :premises (@p1 @p33)) % 0.38/0.57 (step @p35 :rule eq-symm :args (@t15 @t8)) % 0.38/0.57 (step @p36 :rule refl :args (@t8)) % 0.38/0.57 (step @p37 :rule refl :args (@t15)) % 0.38/0.57 (step @p38 :rule refl :args (@t16)) % 0.38/0.57 (step @p39 :rule cong :premises (@p38 @p37) :args ((= @t16 @t15))) % 0.38/0.57 (step @p40 :rule symm :premises (@p39)) % 0.38/0.57 (step @p41 :rule eq_resolve :premises (@p38 @p40)) % 0.38/0.57 (step @p42 :rule eq-refl :args (tptp.x)) % 0.38/0.57 (step @p43 :rule skolem_intro :args (@t14)) % 0.38/0.57 (step @p44 :rule refl :args (tptp.x)) % 0.38/0.57 (step @p45 :rule cong :premises (@p44 @p43) :args ((= tptp.x @t14))) % 0.38/0.57 (step @p46 :rule trans :premises (@p45 @p42)) % 0.38/0.57 (step @p47 :rule true_elim :premises (@p46)) % 0.38/0.57 (step @p48 :rule refl :args (tptp.f)) % 0.38/0.57 (step @p49 :rule ho_cong :premises (@p48 @p47)) % 0.38/0.57 (step @p50 :rule trans :premises (@p49 @p41)) % 0.38/0.57 (step @p51 :rule cong :premises (@p50 @p36) :args (@t11)) % 0.38/0.57 (step @p52 :rule trans :premises (@p51 @p35)) % 0.38/0.57 (step @p53 :rule eq-symm :args (@t8 @t1)) % 0.38/0.57 (step @p54 :rule trans :premises (@p53 @p52)) % 0.38/0.57 (step @p55 :rule eq_resolve :premises (@p10 @p54)) % 0.38/0.57 (step @p56 :rule equiv_elim1 :premises (@p55)) % 0.38/0.57 (step @p57 :rule reordering :premises (@p56) :args ((or @t15 @t17))) % 0.38/0.57 (assume-push @p402 @t8) % 0.38/0.57 (assume-push @p403 @t6) % 0.38/0.57 (assume-push @p404 @t6) % 0.38/0.57 (assume-push @p405 @t8) % 0.38/0.57 (step @p62 :rule true_intro :premises (@p403)) % 0.38/0.57 (step @p63 :rule symm :premises (@p62)) % 0.38/0.57 (step @p64 :rule true_intro :premises (@p402)) % 0.38/0.57 (step @p65 :rule trans :premises (@p64 @p63)) % 0.38/0.57 (step @p66 :rule cong :premises (@p65) :args (@t9)) % 0.38/0.57 (step-pop @p406 :rule scope :premises (@p66)) % 0.38/0.57 (step-pop @p407 :rule scope :premises (@p406)) % 0.38/0.57 (step @p67 :rule process_scope :premises (@p407) :args (@t18)) % 0.38/0.57 (step @p70 :rule and_intro :premises (@p403 @p402)) % 0.38/0.57 (step @p71 :rule modus_ponens :premises (@p70 @p67)) % 0.38/0.57 (step-pop @p408 :rule scope :premises (@p71)) % 0.38/0.57 (step-pop @p409 :rule scope :premises (@p408)) % 0.38/0.57 (step @p72 :rule process_scope :premises (@p409) :args (@t18)) % 0.38/0.57 (step @p75 :rule implies_elim :premises (@p72)) % 0.38/0.57 (step @p76 :rule cnf_and_neg :args (@t19)) % 0.38/0.57 (step @p77 :rule resolution :premises (@p76 @p75) :args (true @t19)) % 0.38/0.57 (step @p78 :rule reordering :premises (@p77) :args ((or @t18 @t17 @t20))) % 0.38/0.57 (step @p79 :rule eq-symm :args (@t22 @t6)) % 0.38/0.57 (step @p80 :rule refl :args (@t6)) % 0.38/0.57 (step @p81 :rule refl :args (@t22)) % 0.38/0.57 (step @p82 :rule refl :args (@t23)) % 0.38/0.57 (step @p83 :rule cong :premises (@p82 @p81) :args ((= @t23 @t22))) % 0.38/0.57 (step @p84 :rule symm :premises (@p83)) % 0.38/0.57 (step @p85 :rule eq_resolve :premises (@p82 @p84)) % 0.38/0.57 (step @p86 :rule eq-refl :args (@t2)) % 0.38/0.57 (step @p87 :rule skolem_intro :args (@t21)) % 0.38/0.57 (step @p88 :rule refl :args (@t2)) % 0.38/0.57 (step @p89 :rule cong :premises (@p88 @p87) :args (@t24)) % 0.38/0.57 (step @p90 :rule trans :premises (@p89 @p86)) % 0.38/0.57 (step @p91 :rule true_elim :premises (@p90)) % 0.38/0.57 (step @p92 :rule ho_cong :premises (@p48 @p91)) % 0.38/0.57 (step @p93 :rule trans :premises (@p92 @p85)) % 0.38/0.57 (step @p94 :rule cong :premises (@p93 @p80) :args (@t13)) % 0.38/0.57 (step @p95 :rule trans :premises (@p94 @p79)) % 0.38/0.57 (step @p96 :rule eq-symm :args (@t6 @t3)) % 0.38/0.57 (step @p97 :rule trans :premises (@p96 @p95)) % 0.38/0.57 (step @p98 :rule eq_resolve :premises (@p24 @p97)) % 0.38/0.57 (step @p99 :rule equiv_elim2 :premises (@p98)) % 0.38/0.57 (assume-push @p410 @t8) % 0.38/0.57 (assume-push @p411 @t14) % 0.38/0.57 (assume-push @p412 @t15) % 0.38/0.57 (assume-push @p413 @t15) % 0.38/0.57 (assume-push @p414 @t14) % 0.38/0.57 (assume-push @p415 @t8) % 0.38/0.57 (step @p106 :rule true_intro :premises (@p412)) % 0.38/0.57 (step @p107 :rule true_intro :premises (@p411)) % 0.38/0.57 (step @p108 :rule symm :premises (@p107)) % 0.38/0.57 (step @p109 :rule true_intro :premises (@p410)) % 0.38/0.57 (step @p110 :rule trans :premises (@p109 @p108)) % 0.38/0.57 (step @p111 :rule cong :premises (@p110) :args (@t25)) % 0.38/0.57 (step @p112 :rule trans :premises (@p111 @p106)) % 0.38/0.57 (step @p113 :rule true_elim :premises (@p112)) % 0.38/0.57 (step-pop @p416 :rule scope :premises (@p113)) % 0.38/0.57 (step-pop @p417 :rule scope :premises (@p416)) % 0.38/0.57 (step-pop @p418 :rule scope :premises (@p417)) % 0.38/0.57 (step @p114 :rule process_scope :premises (@p418) :args (@t25)) % 0.38/0.57 (step @p118 :rule and_intro :premises (@p412 @p411 @p410)) % 0.38/0.57 (step @p119 :rule modus_ponens :premises (@p118 @p114)) % 0.38/0.57 (step-pop @p419 :rule scope :premises (@p119)) % 0.38/0.57 (step-pop @p420 :rule scope :premises (@p419)) % 0.38/0.57 (step-pop @p421 :rule scope :premises (@p420)) % 0.38/0.57 (step @p120 :rule process_scope :premises (@p421) :args (@t25)) % 0.38/0.57 (step @p124 :rule implies_elim :premises (@p120)) % 0.38/0.57 (step @p125 :rule cnf_and_neg :args (@t26)) % 0.38/0.57 (step @p126 :rule resolution :premises (@p125 @p124) :args (true @t26)) % 0.38/0.57 (step @p127 :rule reordering :premises (@p126) :args ((or @t25 @t17 @t28 @t27))) % 0.38/0.57 (step @p128 :rule eq-symm :args (@t25 @t21)) % 0.38/0.57 (step @p129 :rule refl :args (@t21)) % 0.38/0.57 (step @p130 :rule refl :args (@t25)) % 0.38/0.57 (step @p131 :rule refl :args (@t29)) % 0.38/0.57 (step @p132 :rule cong :premises (@p131 @p130) :args ((= @t29 @t25))) % 0.38/0.57 (step @p133 :rule symm :premises (@p132)) % 0.38/0.57 (step @p134 :rule eq_resolve :premises (@p131 @p133)) % 0.38/0.57 (step @p135 :rule ho_cong :premises (@p48 @p14)) % 0.38/0.57 (step @p136 :rule trans :premises (@p135 @p134)) % 0.38/0.57 (step @p137 :rule cong :premises (@p136 @p129) :args (@t24)) % 0.38/0.57 (step @p138 :rule trans :premises (@p137 @p128)) % 0.38/0.57 (step @p139 :rule eq-symm :args (@t21 @t2)) % 0.38/0.57 (step @p140 :rule trans :premises (@p139 @p138)) % 0.38/0.57 (step @p141 :rule eq_resolve :premises (@p87 @p140)) % 0.38/0.57 (step @p142 :rule equiv_elim2 :premises (@p141)) % 0.38/0.57 (step @p143 :rule bool-double-not-elim :args (@t22)) % 0.38/0.57 (step @p144 :rule refl :args (@t30)) % 0.38/0.57 (step @p145 :rule refl :args (@t28)) % 0.38/0.57 (step @p146 :rule refl :args (@t27)) % 0.38/0.57 (step @p147 :rule refl :args (@t17)) % 0.38/0.57 (step @p148 :rule nary_cong :premises (@p147 @p146 @p145 @p144 @p143) :args ((or @t17 @t27 @t28 @t30 @t32))) % 0.38/0.57 (assume-push @p422 @t15) % 0.38/0.57 (assume-push @p423 @t14) % 0.38/0.57 (assume-push @p424 @t8) % 0.38/0.57 (assume-push @p425 @t21) % 0.38/0.57 (assume-push @p426 @t31) % 0.38/0.57 (step @p154 :rule evaluate :args (@t33)) % 0.38/0.57 (step @p155 :rule true_intro :premises (@p422)) % 0.38/0.57 (step @p156 :rule true_intro :premises (@p423)) % 0.38/0.57 (step @p157 :rule symm :premises (@p156)) % 0.38/0.57 (step @p158 :rule true_intro :premises (@p424)) % 0.38/0.57 (step @p159 :rule trans :premises (@p158 @p157)) % 0.38/0.57 (step @p160 :rule cong :premises (@p159) :args (@t25)) % 0.38/0.57 (step @p161 :rule symm :premises (@p158)) % 0.38/0.57 (step @p162 :rule true_intro :premises (@p425)) % 0.38/0.57 (step @p163 :rule trans :premises (@p162 @p161)) % 0.38/0.57 (step @p164 :rule cong :premises (@p163) :args (@t22)) % 0.38/0.57 (step @p165 :rule false_intro :premises (@p426)) % 0.38/0.57 (step @p166 :rule symm :premises (@p165)) % 0.38/0.57 (step @p167 :rule trans :premises (@p166 @p164 @p160 @p155)) % 0.38/0.57 (step @p168 false :rule eq_resolve :premises (@p167 @p154)) % 0.38/0.57 (step-pop @p427 :rule scope :premises (@p168)) % 0.38/0.57 (step-pop @p428 :rule scope :premises (@p427)) % 0.38/0.57 (step-pop @p429 :rule scope :premises (@p428)) % 0.38/0.57 (step-pop @p430 :rule scope :premises (@p429)) % 0.38/0.57 (step-pop @p431 :rule scope :premises (@p430)) % 0.38/0.57 (step @p169 :rule process_scope :premises (@p431) :args (false)) % 0.38/0.57 (assume-push @p432 @t8) % 0.38/0.57 (assume-push @p433 @t14) % 0.38/0.57 (assume-push @p434 @t15) % 0.38/0.57 (assume-push @p435 @t21) % 0.38/0.57 (assume-push @p436 @t31) % 0.38/0.57 (step @p180 :rule and_intro :premises (@p434 @p433 @p432 @p435 @p436)) % 0.38/0.57 (step-pop @p437 :rule scope :premises (@p180)) % 0.38/0.57 (step-pop @p438 :rule scope :premises (@p437)) % 0.38/0.57 (step-pop @p439 :rule scope :premises (@p438)) % 0.38/0.57 (step-pop @p440 :rule scope :premises (@p439)) % 0.38/0.57 (step-pop @p441 :rule scope :premises (@p440)) % 0.38/0.57 (step @p181 :rule process_scope :premises (@p441) :args (@t34)) % 0.38/0.57 (step @p187 :rule implies_elim :premises (@p181)) % 0.38/0.57 (step @p188 :rule resolution :premises (@p187 @p169) :args (true @t34)) % 0.38/0.57 (step @p189 :rule not_and :premises (@p188)) % 0.38/0.57 (step @p190 :rule eq_resolve :premises (@p189 @p148)) % 0.38/0.57 (step @p191 :rule reordering :premises (@p190) :args ((or @t22 @t17 @t28 @t27 @t30))) % 0.38/0.57 (step @p192 :rule chain_m_resolution :premises (@p191 @p142 @p127 @p57 @p99 @p78 @p34) :args ((or @t17 @t27) (@list false false false true true true) (@list @t21 @t25 @t15 @t22 @t6 @t18))) % 0.38/0.57 (step @p193 :rule equiv_elim1 :premises (@p141)) % 0.38/0.57 (step @p194 :rule reordering :premises (@p193) :args ((or @t25 @t30))) % 0.38/0.57 (step @p195 :rule refl :args (@t35)) % 0.38/0.57 (step @p196 :rule nary_cong :premises (@p147 @p144 @p143 @p195) :args ((or @t17 @t30 @t32 @t35))) % 0.38/0.57 (assume-push @p442 @t8) % 0.38/0.57 (assume-push @p443 @t21) % 0.38/0.57 (assume-push @p444 @t31) % 0.38/0.57 (assume-push @p445 @t31) % 0.38/0.57 (assume-push @p446 @t21) % 0.38/0.57 (assume-push @p447 @t8) % 0.38/0.57 (step @p203 :rule false_intro :premises (@p444)) % 0.38/0.57 (step @p204 :rule true_intro :premises (@p443)) % 0.38/0.57 (step @p205 :rule symm :premises (@p204)) % 0.38/0.57 (step @p206 :rule true_intro :premises (@p442)) % 0.38/0.57 (step @p207 :rule trans :premises (@p206 @p205)) % 0.38/0.57 (step @p208 :rule cong :premises (@p207) :args (@t25)) % 0.38/0.57 (step @p209 :rule trans :premises (@p208 @p203)) % 0.38/0.57 (step @p210 :rule false_elim :premises (@p209)) % 0.38/0.57 (step-pop @p448 :rule scope :premises (@p210)) % 0.38/0.57 (step-pop @p449 :rule scope :premises (@p448)) % 0.38/0.57 (step-pop @p450 :rule scope :premises (@p449)) % 0.38/0.57 (step @p211 :rule process_scope :premises (@p450) :args (@t35)) % 0.38/0.57 (step @p215 :rule and_intro :premises (@p444 @p443 @p442)) % 0.38/0.57 (step @p216 :rule modus_ponens :premises (@p215 @p211)) % 0.38/0.57 (step-pop @p451 :rule scope :premises (@p216)) % 0.38/0.57 (step-pop @p452 :rule scope :premises (@p451)) % 0.38/0.57 (step-pop @p453 :rule scope :premises (@p452)) % 0.38/0.57 (step @p217 :rule process_scope :premises (@p453) :args (@t35)) % 0.38/0.57 (step @p221 :rule implies_elim :premises (@p217)) % 0.38/0.57 (step @p222 :rule cnf_and_neg :args (@t36)) % 0.38/0.57 (step @p223 :rule resolution :premises (@p222 @p221) :args (true @t36)) % 0.38/0.57 (step @p224 :rule eq_resolve :premises (@p223 @p196)) % 0.38/0.57 (step @p225 :rule reordering :premises (@p224) :args ((or @t22 @t17 @t30 @t35))) % 0.38/0.57 (step @p226 :rule chain_m_resolution :premises (@p225 @p194 @p99 @p78 @p34) :args ((or @t17 @t30) (@list false true true true) (@list @t25 @t22 @t6 @t18))) % 0.38/0.57 (step @p227 :rule bool-double-not-elim :args (@t21)) % 0.38/0.57 (step @p228 :rule bool-double-not-elim :args (@t14)) % 0.38/0.57 (step @p229 :rule nary_cong :premises (@p145 @p143 @p228 @p227) :args ((or @t28 @t32 @t38 @t37))) % 0.38/0.57 (assume-push @p454 @t15) % 0.38/0.57 (assume-push @p455 @t27) % 0.38/0.57 (assume-push @p456 @t30) % 0.38/0.57 (assume-push @p457 @t31) % 0.38/0.57 (step @p154 :rule evaluate :args (@t33)) % 0.38/0.57 (step @p234 :rule true_intro :premises (@p454)) % 0.38/0.57 (step @p235 :rule false_intro :premises (@p455)) % 0.38/0.57 (step @p236 :rule symm :premises (@p235)) % 0.38/0.57 (step @p237 :rule false_intro :premises (@p456)) % 0.38/0.57 (step @p238 :rule trans :premises (@p237 @p236)) % 0.38/0.57 (step @p239 :rule cong :premises (@p238) :args (@t22)) % 0.38/0.57 (step @p240 :rule false_intro :premises (@p457)) % 0.38/0.57 (step @p241 :rule symm :premises (@p240)) % 0.38/0.57 (step @p242 :rule trans :premises (@p241 @p239 @p234)) % 0.38/0.57 (step @p243 false :rule eq_resolve :premises (@p242 @p154)) % 0.38/0.57 (step-pop @p458 :rule scope :premises (@p243)) % 0.38/0.57 (step-pop @p459 :rule scope :premises (@p458)) % 0.38/0.57 (step-pop @p460 :rule scope :premises (@p459)) % 0.38/0.57 (step-pop @p461 :rule scope :premises (@p460)) % 0.38/0.57 (step @p244 :rule process_scope :premises (@p461) :args (false)) % 0.38/0.57 (assume-push @p462 @t15) % 0.38/0.57 (assume-push @p463 @t31) % 0.38/0.57 (assume-push @p464 @t27) % 0.38/0.57 (assume-push @p465 @t30) % 0.38/0.57 (step @p253 :rule and_intro :premises (@p462 @p464 @p465 @p463)) % 0.38/0.57 (step-pop @p466 :rule scope :premises (@p253)) % 0.38/0.57 (step-pop @p467 :rule scope :premises (@p466)) % 0.38/0.57 (step-pop @p468 :rule scope :premises (@p467)) % 0.38/0.57 (step-pop @p469 :rule scope :premises (@p468)) % 0.38/0.57 (step @p254 :rule process_scope :premises (@p469) :args (@t39)) % 0.38/0.57 (step @p259 :rule implies_elim :premises (@p254)) % 0.38/0.57 (step @p260 :rule resolution :premises (@p259 @p244) :args (true @t39)) % 0.38/0.57 (step @p261 :rule not_and :premises (@p260)) % 0.38/0.57 (step @p262 :rule eq_resolve :premises (@p261 @p229)) % 0.38/0.57 (step @p263 :rule reordering :premises (@p262) :args ((or @t14 @t21 @t22 @t28))) % 0.38/0.57 (step @p264 :rule chain_m_resolution :premises (@p263 @p226 @p192 @p99 @p78 @p34 @p57) :args (@t17 (@list true true true true true false) (@list @t21 @t14 @t22 @t6 @t18 @t15))) % 0.38/0.57 (step @p265 :rule refl :args (@t25)) % 0.38/0.57 (step @p266 :rule bool-double-not-elim :args (@t8)) % 0.38/0.57 (step @p267 :rule refl :args (@t31)) % 0.38/0.57 (step @p268 :rule nary_cong :premises (@p267 @p266 @p227 @p265) :args ((or @t31 @t40 @t37 @t25))) % 0.38/0.57 (assume-push @p470 @t22) % 0.38/0.57 (assume-push @p471 @t17) % 0.38/0.57 (assume-push @p472 @t30) % 0.38/0.57 (assume-push @p473 @t22) % 0.38/0.57 (assume-push @p474 @t30) % 0.38/0.57 (assume-push @p475 @t17) % 0.38/0.57 (step @p275 :rule true_intro :premises (@p470)) % 0.38/0.57 (step @p276 :rule false_intro :premises (@p472)) % 0.38/0.57 (step @p277 :rule symm :premises (@p276)) % 0.38/0.57 (step @p278 :rule false_intro :premises (@p471)) % 0.38/0.57 (step @p279 :rule trans :premises (@p278 @p277)) % 0.38/0.57 (step @p280 :rule cong :premises (@p279) :args (@t25)) % 0.38/0.57 (step @p281 :rule trans :premises (@p280 @p275)) % 0.38/0.57 (step @p282 :rule true_elim :premises (@p281)) % 0.38/0.57 (step-pop @p476 :rule scope :premises (@p282)) % 0.38/0.57 (step-pop @p477 :rule scope :premises (@p476)) % 0.38/0.57 (step-pop @p478 :rule scope :premises (@p477)) % 0.38/0.57 (step @p283 :rule process_scope :premises (@p478) :args (@t25)) % 0.38/0.57 (step @p287 :rule and_intro :premises (@p470 @p472 @p471)) % 0.38/0.57 (step @p288 :rule modus_ponens :premises (@p287 @p283)) % 0.38/0.57 (step-pop @p479 :rule scope :premises (@p288)) % 0.38/0.57 (step-pop @p480 :rule scope :premises (@p479)) % 0.38/0.57 (step-pop @p481 :rule scope :premises (@p480)) % 0.38/0.57 (step @p289 :rule process_scope :premises (@p481) :args (@t25)) % 0.38/0.57 (step @p293 :rule implies_elim :premises (@p289)) % 0.38/0.57 (step @p294 :rule cnf_and_neg :args (@t41)) % 0.38/0.57 (step @p295 :rule resolution :premises (@p294 @p293) :args (true @t41)) % 0.38/0.57 (step @p296 :rule eq_resolve :premises (@p295 @p268)) % 0.38/0.57 (step @p297 :rule reordering :premises (@p296) :args ((or @t8 @t21 @t25 @t31))) % 0.38/0.57 (step @p298 :rule chain_m_resolution :premises (@p297 @p264 @p142) :args ((or @t21 @t31) (@list true true) (@list @t8 @t25))) % 0.38/0.57 (step @p299 :rule equiv_elim2 :premises (@p55)) % 0.38/0.57 (step @p300 :rule chain_m_resolution :premises (@p299 @p264) :args (@t28 @t42 (@list @t8))) % 0.38/0.57 (step @p301 :rule bool-double-not-elim :args (@t15)) % 0.38/0.57 (step @p302 :rule nary_cong :premises (@p146 @p144 @p267 @p301) :args ((or @t27 @t30 @t31 @t43))) % 0.38/0.57 (assume-push @p482 @t28) % 0.38/0.57 (assume-push @p483 @t14) % 0.38/0.57 (assume-push @p484 @t21) % 0.38/0.57 (assume-push @p485 @t22) % 0.38/0.57 (step @p307 :rule evaluate :args ((= true false))) % 0.38/0.57 (step @p308 :rule false_intro :premises (@p482)) % 0.38/0.57 (step @p309 :rule true_intro :premises (@p483)) % 0.38/0.57 (step @p310 :rule symm :premises (@p309)) % 0.38/0.57 (step @p311 :rule true_intro :premises (@p484)) % 0.38/0.57 (step @p312 :rule trans :premises (@p311 @p310)) % 0.38/0.57 (step @p313 :rule cong :premises (@p312) :args (@t22)) % 0.38/0.57 (step @p314 :rule true_intro :premises (@p485)) % 0.38/0.57 (step @p315 :rule symm :premises (@p314)) % 0.38/0.57 (step @p316 :rule trans :premises (@p315 @p313 @p308)) % 0.38/0.57 (step @p317 false :rule eq_resolve :premises (@p316 @p307)) % 0.38/0.57 (step-pop @p486 :rule scope :premises (@p317)) % 0.38/0.57 (step-pop @p487 :rule scope :premises (@p486)) % 0.38/0.57 (step-pop @p488 :rule scope :premises (@p487)) % 0.38/0.57 (step-pop @p489 :rule scope :premises (@p488)) % 0.38/0.57 (step @p318 :rule process_scope :premises (@p489) :args (false)) % 0.38/0.57 (assume-push @p490 @t14) % 0.38/0.57 (assume-push @p491 @t21) % 0.38/0.57 (assume-push @p492 @t22) % 0.38/0.57 (assume-push @p493 @t28) % 0.38/0.57 (step @p327 :rule and_intro :premises (@p493 @p490 @p491 @p492)) % 0.38/0.57 (step-pop @p494 :rule scope :premises (@p327)) % 0.38/0.57 (step-pop @p495 :rule scope :premises (@p494)) % 0.38/0.57 (step-pop @p496 :rule scope :premises (@p495)) % 0.38/0.57 (step-pop @p497 :rule scope :premises (@p496)) % 0.38/0.57 (step @p328 :rule process_scope :premises (@p497) :args (@t44)) % 0.38/0.57 (step @p333 :rule implies_elim :premises (@p328)) % 0.38/0.57 (step @p334 :rule resolution :premises (@p333 @p318) :args (true @t44)) % 0.38/0.57 (step @p335 :rule not_and :premises (@p334)) % 0.38/0.57 (step @p336 :rule eq_resolve :premises (@p335 @p302)) % 0.38/0.57 (step @p337 :rule reordering :premises (@p336) :args ((or @t15 @t31 @t27 @t30))) % 0.38/0.57 (step @p338 :rule nary_cong :premises (@p195 @p266 @p301 @p228) :args ((or @t35 @t40 @t43 @t38))) % 0.38/0.57 (assume-push @p498 @t25) % 0.38/0.57 (assume-push @p499 @t17) % 0.38/0.57 (assume-push @p500 @t27) % 0.38/0.57 (assume-push @p501 @t28) % 0.38/0.57 (step @p154 :rule evaluate :args (@t33)) % 0.38/0.57 (step @p343 :rule true_intro :premises (@p498)) % 0.38/0.57 (step @p344 :rule false_intro :premises (@p499)) % 0.38/0.57 (step @p345 :rule symm :premises (@p344)) % 0.38/0.57 (step @p346 :rule false_intro :premises (@p500)) % 0.38/0.57 (step @p347 :rule trans :premises (@p346 @p345)) % 0.38/0.57 (step @p348 :rule cong :premises (@p347) :args (@t15)) % 0.38/0.57 (step @p349 :rule false_intro :premises (@p501)) % 0.38/0.57 (step @p350 :rule symm :premises (@p349)) % 0.38/0.57 (step @p351 :rule trans :premises (@p350 @p348 @p343)) % 0.38/0.57 (step @p352 false :rule eq_resolve :premises (@p351 @p154)) % 0.38/0.57 (step-pop @p502 :rule scope :premises (@p352)) % 0.38/0.57 (step-pop @p503 :rule scope :premises (@p502)) % 0.38/0.57 (step-pop @p504 :rule scope :premises (@p503)) % 0.38/0.57 (step-pop @p505 :rule scope :premises (@p504)) % 0.38/0.57 (step @p353 :rule process_scope :premises (@p505) :args (false)) % 0.38/0.57 (assume-push @p506 @t25) % 0.38/0.57 (assume-push @p507 @t17) % 0.38/0.57 (assume-push @p508 @t28) % 0.38/0.57 (assume-push @p509 @t27) % 0.38/0.57 (step @p362 :rule and_intro :premises (@p506 @p507 @p509 @p508)) % 0.38/0.57 (step-pop @p510 :rule scope :premises (@p362)) % 0.38/0.57 (step-pop @p511 :rule scope :premises (@p510)) % 0.38/0.57 (step-pop @p512 :rule scope :premises (@p511)) % 0.38/0.57 (step-pop @p513 :rule scope :premises (@p512)) % 0.38/0.57 (step @p363 :rule process_scope :premises (@p513) :args (@t45)) % 0.38/0.57 (step @p368 :rule implies_elim :premises (@p363)) % 0.38/0.57 (step @p369 :rule resolution :premises (@p368 @p353) :args (true @t45)) % 0.38/0.57 (step @p370 :rule not_and :premises (@p369)) % 0.38/0.57 (step @p371 :rule eq_resolve :premises (@p370 @p338)) % 0.38/0.57 (step @p372 :rule reordering :premises (@p371) :args ((or @t8 @t14 @t15 @t35))) % 0.38/0.57 (step @p373 :rule chain_m_resolution :premises (@p372 @p300 @p264 @p337 @p300 @p194 @p298) :args (@t31 (@list true true true true false false) (@list @t15 @t8 @t14 @t15 @t25 @t21))) % 0.38/0.57 (step @p374 :rule equiv_elim1 :premises (@p98)) % 0.38/0.57 (step @p375 :rule reordering :premises (@p374) :args ((or @t22 @t20))) % 0.38/0.57 (step @p376 :rule chain_m_resolution :premises (@p375 @p373) :args (@t20 @t42 (@list @t22))) % 0.38/0.57 (step @p377 :rule refl :args (@t18)) % 0.38/0.57 (step @p378 :rule bool-double-not-elim :args (@t6)) % 0.38/0.57 (step @p379 :rule nary_cong :premises (@p266 @p378 @p377) :args ((or @t40 (not @t20) @t18))) % 0.38/0.57 (assume-push @p514 @t17) % 0.38/0.58 (assume-push @p515 @t20) % 0.38/0.58 (assume-push @p516 @t20) % 0.38/0.58 (assume-push @p517 @t17) % 0.38/0.58 (step @p384 :rule false_intro :premises (@p515)) % 0.38/0.58 (step @p385 :rule symm :premises (@p384)) % 0.38/0.58 (step @p386 :rule false_intro :premises (@p514)) % 0.38/0.58 (step @p387 :rule trans :premises (@p386 @p385)) % 0.38/0.58 (step @p388 :rule cong :premises (@p387) :args (@t9)) % 0.38/0.58 (step-pop @p518 :rule scope :premises (@p388)) % 0.38/0.58 (step-pop @p519 :rule scope :premises (@p518)) % 0.38/0.58 (step @p389 :rule process_scope :premises (@p519) :args (@t18)) % 0.38/0.58 (step @p392 :rule and_intro :premises (@p515 @p514)) % 0.38/0.58 (step @p393 :rule modus_ponens :premises (@p392 @p389)) % 0.38/0.58 (step-pop @p520 :rule scope :premises (@p393)) % 0.38/0.58 (step-pop @p521 :rule scope :premises (@p520)) % 0.38/0.58 (step @p394 :rule process_scope :premises (@p521) :args (@t18)) % 0.38/0.58 (step @p397 :rule implies_elim :premises (@p394)) % 0.38/0.58 (step @p398 :rule cnf_and_neg :args (@t46)) % 0.38/0.58 (step @p399 :rule resolution :premises (@p398 @p397) :args (true @t46)) % 0.38/0.58 (step @p400 :rule eq_resolve :premises (@p399 @p379)) % 0.38/0.58 (step @p401 false :rule chain_m_resolution :premises (@p400 @p376 @p264 @p34) :args (false (@list true true true) (@list @t6 @t8 @t18))) % 0.38/0.58 ) % 0.38/0.58 % SZS output end Proof % 0.38/0.58 % cvc5 exiting %------------------------------------------------------------------------------