%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : SWW471_1 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n008.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:06:21 AM UTC 2026 % Result : CounterSatisfiable 138.14s 138.41s % Output : Model 138.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW471_1 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.16/0.34 % Computer : n008.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 22:03:33 EDT 2026 % 0.16/0.35 % CPUTime : % 0.39/0.57 %----Disproving TF0_NAR % 138.14/138.41 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 138.14/138.41 --- Run --mbqi at 45... % 138.14/138.41 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 138.14/138.41 --- Run --full-saturate-quant at 45... % 138.14/138.41 --- Run --finite-model-find --fmf-bound --macros-quant at 60... % 138.14/138.41 % SZS status CounterSatisfiable % 138.14/138.41 % SZS output start Model % 138.14/138.41 ( % 138.14/138.41 ; cardinality of $$unsorted is 1 % 138.14/138.41 ; rep: (as @$$unsorted_0 $$unsorted) % 138.14/138.41 ; cardinality of tptp.com is 1 % 138.14/138.41 ; rep: (as @tptp.com_0 tptp.com) % 138.14/138.41 ; cardinality of tptp.pname is 1 % 138.14/138.41 ; rep: (as @tptp.pname_0 tptp.pname) % 138.14/138.41 ; cardinality of tptp.state is 1 % 138.14/138.41 ; rep: (as @tptp.state_0 tptp.state) % 138.14/138.41 ; cardinality of tptp.bool is 2 % 138.14/138.41 ; rep: (as @tptp.bool_0 tptp.bool) % 138.14/138.41 ; rep: (as @tptp.bool_1 tptp.bool) % 138.14/138.41 ; cardinality of tptp.hoare_1927711152iple_a is 1 % 138.14/138.41 ; rep: (as @tptp.hoare_1927711152iple_a_0 tptp.hoare_1927711152iple_a) % 138.14/138.41 ; cardinality of tptp.nat is 2 % 138.14/138.41 ; rep: (as @tptp.nat_0 tptp.nat) % 138.14/138.41 ; rep: (as @tptp.nat_1 tptp.nat) % 138.14/138.41 ; cardinality of tptp.option_com is 1 % 138.14/138.41 ; rep: (as @tptp.option_com_0 tptp.option_com) % 138.14/138.41 ; cardinality of tptp.fun_a_fun_state_bool is 1 % 138.14/138.41 ; rep: (as @tptp.fun_a_fun_state_bool_0 tptp.fun_a_fun_state_bool) % 138.14/138.41 ; cardinality of tptp.fun_co1155576772iple_a is 1 % 138.14/138.41 ; rep: (as @tptp.fun_co1155576772iple_a_0 tptp.fun_co1155576772iple_a) % 138.14/138.41 ; cardinality of tptp.fun_pname_com is 1 % 138.14/138.41 ; rep: (as @tptp.fun_pname_com_0 tptp.fun_pname_com) % 138.14/138.41 ; cardinality of tptp.fun_pname_pname is 1 % 138.14/138.41 ; rep: (as @tptp.fun_pname_pname_0 tptp.fun_pname_pname) % 138.14/138.41 ; cardinality of tptp.fun_pname_bool is 2 % 138.14/138.41 ; rep: (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) % 138.14/138.41 ; rep: (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool) % 138.14/138.41 ; cardinality of tptp.fun_pn708290217iple_a is 1 % 138.14/138.41 ; rep: (as @tptp.fun_pn708290217iple_a_0 tptp.fun_pn708290217iple_a) % 138.14/138.41 ; cardinality of tptp.fun_pname_option_com is 1 % 138.14/138.41 ; rep: (as @tptp.fun_pname_option_com_0 tptp.fun_pname_option_com) % 138.14/138.41 ; cardinality of tptp.fun_pn1683930517e_bool is 1 % 138.14/138.41 ; rep: (as @tptp.fun_pn1683930517e_bool_0 tptp.fun_pn1683930517e_bool) % 138.14/138.41 ; cardinality of tptp.fun_pn308211645iple_a is 1 % 138.14/138.41 ; rep: (as @tptp.fun_pn308211645iple_a_0 tptp.fun_pn308211645iple_a) % 138.14/138.41 ; cardinality of tptp.fun_pn800050071e_bool is 1 % 138.14/138.41 ; rep: (as @tptp.fun_pn800050071e_bool_0 tptp.fun_pn800050071e_bool) % 138.14/138.41 ; cardinality of tptp.fun_pn250273176l_bool is 3 % 138.14/138.41 ; rep: (as @tptp.fun_pn250273176l_bool_0 tptp.fun_pn250273176l_bool) % 138.14/138.41 ; rep: (as @tptp.fun_pn250273176l_bool_1 tptp.fun_pn250273176l_bool) % 138.14/138.41 ; rep: (as @tptp.fun_pn250273176l_bool_2 tptp.fun_pn250273176l_bool) % 138.14/138.41 ; cardinality of tptp.fun_pn579076298iple_a is 1 % 138.14/138.41 ; rep: (as @tptp.fun_pn579076298iple_a_0 tptp.fun_pn579076298iple_a) % 138.14/138.41 ; cardinality of tptp.fun_pn422929397l_bool is 1 % 138.14/138.41 ; rep: (as @tptp.fun_pn422929397l_bool_0 tptp.fun_pn422929397l_bool) % 138.14/138.41 ; cardinality of tptp.fun_bool_bool is 4 % 138.14/138.41 ; rep: (as @tptp.fun_bool_bool_0 tptp.fun_bool_bool) % 138.14/138.41 ; rep: (as @tptp.fun_bool_bool_1 tptp.fun_bool_bool) % 138.14/138.41 ; rep: (as @tptp.fun_bool_bool_2 tptp.fun_bool_bool) % 138.14/138.41 ; rep: (as @tptp.fun_bool_bool_3 tptp.fun_bool_bool) % 138.14/138.41 ; cardinality of tptp.fun_bo1549164019l_bool is 3 % 138.14/138.41 ; rep: (as @tptp.fun_bo1549164019l_bool_0 tptp.fun_bo1549164019l_bool) % 138.14/138.41 ; rep: (as @tptp.fun_bo1549164019l_bool_1 tptp.fun_bo1549164019l_bool) % 138.14/138.41 ; rep: (as @tptp.fun_bo1549164019l_bool_2 tptp.fun_bo1549164019l_bool) % 138.14/138.41 ; cardinality of tptp.fun_Ho842746065_pname is 1 % 138.14/138.41 ; rep: (as @tptp.fun_Ho842746065_pname_0 tptp.fun_Ho842746065_pname) % 138.14/138.41 ; cardinality of tptp.fun_Ho1877127206a_bool is 2 % 138.14/138.41 ; rep: (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) % 138.14/138.41 ; rep: (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) % 138.14/138.41 ; cardinality of tptp.fun_Ho843200573iple_a is 1 % 138.14/138.41 ; rep: (as @tptp.fun_Ho843200573iple_a_0 tptp.fun_Ho843200573iple_a) % 138.14/138.41 ; cardinality of tptp.fun_Ho957066028l_bool is 3 % 138.14/138.41 ; rep: (as @tptp.fun_Ho957066028l_bool_0 tptp.fun_Ho957066028l_bool) % 138.14/138.41 ; rep: (as @tptp.fun_Ho957066028l_bool_1 tptp.fun_Ho957066028l_bool) % 138.14/138.41 ; rep: (as @tptp.fun_Ho957066028l_bool_2 tptp.fun_Ho957066028l_bool) % 138.14/138.41 ; cardinality of tptp.fun_Ho440810351a_bool is 1 % 138.14/138.41 ; rep: (as @tptp.fun_Ho440810351a_bool_0 tptp.fun_Ho440810351a_bool) % 138.14/138.41 ; cardinality of tptp.fun_Ho525994229l_bool is 1 % 138.14/138.41 ; rep: (as @tptp.fun_Ho525994229l_bool_0 tptp.fun_Ho525994229l_bool) % 138.14/138.41 ; cardinality of tptp.fun_option_com_com is 1 % 138.14/138.41 ; rep: (as @tptp.fun_option_com_com_0 tptp.fun_option_com_com) % 138.14/138.41 ; cardinality of tptp.fun_fu1344872529iple_a is 1 % 138.14/138.41 ; rep: (as @tptp.fun_fu1344872529iple_a_0 tptp.fun_fu1344872529iple_a) % 138.14/138.41 ; cardinality of tptp.fun_fu90068325iple_a is 1 % 138.14/138.41 ; rep: (as @tptp.fun_fu90068325iple_a_0 tptp.fun_fu90068325iple_a) % 138.14/138.41 ; cardinality of tptp.fun_fu1430349052l_bool is 1 % 138.14/138.41 ; rep: (as @tptp.fun_fu1430349052l_bool_0 tptp.fun_fu1430349052l_bool) % 138.14/138.41 ; cardinality of tptp.fun_fu832487784l_bool is 1 % 138.14/138.41 ; rep: (as @tptp.fun_fu832487784l_bool_0 tptp.fun_fu832487784l_bool) % 138.14/138.41 (define-fun tptp.cOMBB_1110279240iple_a (($x1 tptp.fun_pn708290217iple_a) ($x2 tptp.fun_Ho842746065_pname)) tptp.fun_Ho843200573iple_a (as @tptp.fun_Ho843200573iple_a_0 tptp.fun_Ho843200573iple_a)) % 138.14/138.41 (define-fun tptp.cOMBB_647938656_pname (($x1 tptp.fun_bool_bool) ($x2 tptp.fun_pname_bool)) tptp.fun_pname_bool (ite (and (= (as @tptp.fun_bool_bool_1 tptp.fun_bool_bool) $x1) (= (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (and (= (as @tptp.fun_bool_bool_0 tptp.fun_bool_bool) $x1) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (and (= (as @tptp.fun_bool_bool_3 tptp.fun_bool_bool) $x1) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (and (= (as @tptp.fun_bool_bool_3 tptp.fun_bool_bool) $x1) (= (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool)))))) % 138.14/138.41 (define-fun tptp.cOMBB_213049548iple_a (($x1 tptp.fun_bool_bool) ($x2 tptp.fun_Ho1877127206a_bool)) tptp.fun_Ho1877127206a_bool (ite (and (= (as @tptp.fun_bool_bool_1 tptp.fun_bool_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (and (= (as @tptp.fun_bool_bool_0 tptp.fun_bool_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (and (= (as @tptp.fun_bool_bool_3 tptp.fun_bool_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (and (= (as @tptp.fun_bool_bool_3 tptp.fun_bool_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool)))))) % 138.14/138.41 (define-fun tptp.cOMBB_675860798_pname (($x1 tptp.fun_bo1549164019l_bool) ($x2 tptp.fun_pname_bool)) tptp.fun_pn250273176l_bool (ite (and (= (as @tptp.fun_bo1549164019l_bool_1 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pn250273176l_bool_0 tptp.fun_pn250273176l_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_0 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pn250273176l_bool_0 tptp.fun_pn250273176l_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_2 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pn250273176l_bool_0 tptp.fun_pn250273176l_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_0 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pn250273176l_bool_1 tptp.fun_pn250273176l_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_1 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pn250273176l_bool_1 tptp.fun_pn250273176l_bool) (as @tptp.fun_pn250273176l_bool_2 tptp.fun_pn250273176l_bool))))))) % 138.14/138.41 (define-fun tptp.cOMBB_196465322iple_a (($x1 tptp.fun_bo1549164019l_bool) ($x2 tptp.fun_Ho1877127206a_bool)) tptp.fun_Ho957066028l_bool (ite (and (= (as @tptp.fun_bo1549164019l_bool_2 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho957066028l_bool_0 tptp.fun_Ho957066028l_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_1 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho957066028l_bool_0 tptp.fun_Ho957066028l_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_0 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho957066028l_bool_0 tptp.fun_Ho957066028l_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_0 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho957066028l_bool_1 tptp.fun_Ho957066028l_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_1 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho957066028l_bool_1 tptp.fun_Ho957066028l_bool) (as @tptp.fun_Ho957066028l_bool_2 tptp.fun_Ho957066028l_bool))))))) % 138.14/138.41 (define-fun tptp.cOMBB_1433562676_pname (($x1 tptp.fun_Ho842746065_pname) ($x2 tptp.fun_pn708290217iple_a)) tptp.fun_pname_pname (as @tptp.fun_pname_pname_0 tptp.fun_pname_pname)) % 138.14/138.41 (define-fun tptp.cOMBB_923936821_pname (($x1 tptp.fun_option_com_com) ($x2 tptp.fun_pname_option_com)) tptp.fun_pname_com (as @tptp.fun_pname_com_0 tptp.fun_pname_com)) % 138.14/138.41 (define-fun tptp.cOMBB_1515136928_pname (($x1 tptp.fun_fu90068325iple_a) ($x2 tptp.fun_pn1683930517e_bool)) tptp.fun_pn308211645iple_a (as @tptp.fun_pn308211645iple_a_0 tptp.fun_pn308211645iple_a)) % 138.14/138.41 (define-fun tptp.cOMBC_1149511130e_bool (($x1 tptp.fun_pn800050071e_bool) ($x2 tptp.pname)) tptp.fun_pname_bool (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool)) % 138.14/138.41 (define-fun tptp.cOMBC_1058051404l_bool (($x1 tptp.fun_pn422929397l_bool) ($x2 tptp.fun_pname_bool)) tptp.fun_pname_bool (ite (and (= (as @tptp.fun_pn422929397l_bool_0 tptp.fun_pn422929397l_bool) $x1) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) % 138.14/138.41 (define-fun tptp.cOMBC_671859290a_bool (($x1 tptp.fun_Ho440810351a_bool) ($x2 tptp.hoare_1927711152iple_a)) tptp.fun_Ho1877127206a_bool (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool)) % 138.14/138.41 (define-fun tptp.cOMBC_862840740l_bool (($x1 tptp.fun_Ho525994229l_bool) ($x2 tptp.fun_Ho1877127206a_bool)) tptp.fun_Ho1877127206a_bool (ite (and (= (as @tptp.fun_Ho525994229l_bool_0 tptp.fun_Ho525994229l_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) % 138.14/138.41 (define-fun tptp.cOMBK_pname_pname (($x1 tptp.pname)) tptp.fun_pname_pname (as @tptp.fun_pname_pname_0 tptp.fun_pname_pname)) % 138.14/138.41 (define-fun tptp.cOMBK_1495131898iple_a (($x1 tptp.pname)) tptp.fun_Ho842746065_pname (as @tptp.fun_Ho842746065_pname_0 tptp.fun_Ho842746065_pname)) % 138.14/138.41 (define-fun tptp.cOMBK_bool_pname (($x1 tptp.bool)) tptp.fun_pname_bool (ite (= (as @tptp.bool_0 tptp.bool) $x1) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) % 138.14/138.41 (define-fun tptp.cOMBK_712844119iple_a (($x1 tptp.bool)) tptp.fun_Ho1877127206a_bool (ite (= (as @tptp.bool_0 tptp.bool) $x1) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) % 138.14/138.41 (define-fun tptp.cOMBK_669226658_pname (($x1 tptp.hoare_1927711152iple_a)) tptp.fun_pn708290217iple_a (as @tptp.fun_pn708290217iple_a_0 tptp.fun_pn708290217iple_a)) % 138.14/138.41 (define-fun tptp.cOMBK_2109678094iple_a (($x1 tptp.hoare_1927711152iple_a)) tptp.fun_Ho843200573iple_a (as @tptp.fun_Ho843200573iple_a_0 tptp.fun_Ho843200573iple_a)) % 138.14/138.41 (define-fun tptp.cOMBS_1125763966iple_a (($x1 tptp.fun_pn308211645iple_a) ($x2 tptp.fun_pname_com)) tptp.fun_pn579076298iple_a (as @tptp.fun_pn579076298iple_a_0 tptp.fun_pn579076298iple_a)) % 138.14/138.41 (define-fun tptp.cOMBS_568398431l_bool (($x1 tptp.fun_pn250273176l_bool) ($x2 tptp.fun_pname_bool)) tptp.fun_pname_bool (ite (and (= (as @tptp.fun_pn250273176l_bool_2 tptp.fun_pn250273176l_bool) $x1) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (and (= (as @tptp.fun_pn250273176l_bool_0 tptp.fun_pn250273176l_bool) $x1) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (and (= (as @tptp.fun_pn250273176l_bool_2 tptp.fun_pn250273176l_bool) $x1) (= (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))))) % 138.14/138.41 (define-fun tptp.cOMBS_821474699iple_a (($x1 tptp.fun_pn579076298iple_a) ($x2 tptp.fun_pn1683930517e_bool)) tptp.fun_pn708290217iple_a (as @tptp.fun_pn708290217iple_a_0 tptp.fun_pn708290217iple_a)) % 138.14/138.41 (define-fun tptp.cOMBS_2061548107l_bool (($x1 tptp.fun_Ho957066028l_bool) ($x2 tptp.fun_Ho1877127206a_bool)) tptp.fun_Ho1877127206a_bool (ite (and (= (as @tptp.fun_Ho957066028l_bool_0 tptp.fun_Ho957066028l_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (and (= (as @tptp.fun_Ho957066028l_bool_2 tptp.fun_Ho957066028l_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (and (= (as @tptp.fun_Ho957066028l_bool_2 tptp.fun_Ho957066028l_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))))) % 138.14/138.41 (define-fun tptp.body_1 () tptp.fun_pname_option_com (as @tptp.fun_pname_option_com_0 tptp.fun_pname_option_com)) % 138.14/138.41 (define-fun tptp.body () tptp.fun_pname_com (as @tptp.fun_pname_com_0 tptp.fun_pname_com)) % 138.14/138.41 (define-fun tptp.zero_zero_nat () tptp.nat (as @tptp.nat_1 tptp.nat)) % 138.14/138.41 (define-fun tptp.hoare_1617968510rivs_a (($x1 tptp.fun_Ho1877127206a_bool) ($x2 tptp.fun_Ho1877127206a_bool)) tptp.bool (as @tptp.bool_0 tptp.bool)) % 138.14/138.41 (define-fun tptp.hoare_1955801856lids_a (($x1 tptp.fun_Ho1877127206a_bool) ($x2 tptp.fun_Ho1877127206a_bool)) tptp.bool (ite (and (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.bool_0 tptp.bool) (as @tptp.bool_1 tptp.bool))) % 138.14/138.41 (define-fun tptp.hoare_1652181356iple_a () tptp.fun_fu90068325iple_a (as @tptp.fun_fu90068325iple_a_0 tptp.fun_fu90068325iple_a)) % 138.14/138.41 (define-fun tptp.hoare_1572001082alid_a (($x1 tptp.nat)) tptp.fun_Ho1877127206a_bool (ite (= (as @tptp.nat_0 tptp.nat) $x1) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) % 138.14/138.41 (define-fun tptp.semila1168014441p_bool (($x1 tptp.bool) ($x2 tptp.bool)) tptp.bool (ite (and (= (as @tptp.bool_0 tptp.bool) $x1) (= (as @tptp.bool_0 tptp.bool) $x2)) (as @tptp.bool_0 tptp.bool) (as @tptp.bool_1 tptp.bool))) % 138.14/138.41 (define-fun tptp.semila278973382e_bool ((BOUND_VARIABLE_3099 tptp.fun_pname_bool) (BOUND_VARIABLE_3100 tptp.fun_pname_bool)) tptp.fun_pname_bool (ite (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (and (= (as @tptp.fun_pn250273176l_bool_2 tptp.fun_pn250273176l_bool) (ite (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (= BOUND_VARIABLE_3099 (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) (as @tptp.fun_pn250273176l_bool_0 tptp.fun_pn250273176l_bool) (ite (= (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool) (ite (= BOUND_VARIABLE_3099 (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) (as @tptp.fun_pn250273176l_bool_1 tptp.fun_pn250273176l_bool) (as @tptp.fun_pn250273176l_bool_2 tptp.fun_pn250273176l_bool)))) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (= BOUND_VARIABLE_3100 (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool)))) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (and (= (as @tptp.fun_pn250273176l_bool_0 tptp.fun_pn250273176l_bool) (ite (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (= BOUND_VARIABLE_3099 (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) (as @tptp.fun_pn250273176l_bool_0 tptp.fun_pn250273176l_bool) (ite (= (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool) (ite (= BOUND_VARIABLE_3099 (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) (as @tptp.fun_pn250273176l_bool_1 tptp.fun_pn250273176l_bool) (as @tptp.fun_pn250273176l_bool_2 tptp.fun_pn250273176l_bool)))) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (= BOUND_VARIABLE_3100 (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool)))) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (and (= (as @tptp.fun_pn250273176l_bool_2 tptp.fun_pn250273176l_bool) (ite (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (ite (= BOUND_VARIABLE_3099 (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) (as @tptp.fun_pn250273176l_bool_0 tptp.fun_pn250273176l_bool) (ite (= (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool) (ite (= BOUND_VARIABLE_3099 (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) (as @tptp.fun_pn250273176l_bool_1 tptp.fun_pn250273176l_bool) (as @tptp.fun_pn250273176l_bool_2 tptp.fun_pn250273176l_bool)))) (= (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool) (ite (= BOUND_VARIABLE_3100 (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool)))) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))))) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) % 138.14/138.41 (define-fun tptp.semila1525949746a_bool ((BOUND_VARIABLE_3082 tptp.fun_Ho1877127206a_bool) (BOUND_VARIABLE_3083 tptp.fun_Ho1877127206a_bool)) tptp.fun_Ho1877127206a_bool (ite (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (and (= (as @tptp.fun_Ho957066028l_bool_0 tptp.fun_Ho957066028l_bool) (ite (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (= BOUND_VARIABLE_3082 (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) (as @tptp.fun_Ho957066028l_bool_0 tptp.fun_Ho957066028l_bool) (ite (= (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) (ite (= BOUND_VARIABLE_3082 (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) (as @tptp.fun_Ho957066028l_bool_1 tptp.fun_Ho957066028l_bool) (as @tptp.fun_Ho957066028l_bool_2 tptp.fun_Ho957066028l_bool)))) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (= BOUND_VARIABLE_3083 (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool)))) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (and (= (as @tptp.fun_Ho957066028l_bool_2 tptp.fun_Ho957066028l_bool) (ite (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (= BOUND_VARIABLE_3082 (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) (as @tptp.fun_Ho957066028l_bool_0 tptp.fun_Ho957066028l_bool) (ite (= (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) (ite (= BOUND_VARIABLE_3082 (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) (as @tptp.fun_Ho957066028l_bool_1 tptp.fun_Ho957066028l_bool) (as @tptp.fun_Ho957066028l_bool_2 tptp.fun_Ho957066028l_bool)))) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (= BOUND_VARIABLE_3083 (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool)))) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (and (= (as @tptp.fun_Ho957066028l_bool_2 tptp.fun_Ho957066028l_bool) (ite (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (ite (= BOUND_VARIABLE_3082 (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) (as @tptp.fun_Ho957066028l_bool_0 tptp.fun_Ho957066028l_bool) (ite (= (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) (ite (= BOUND_VARIABLE_3082 (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) (as @tptp.fun_Ho957066028l_bool_1 tptp.fun_Ho957066028l_bool) (as @tptp.fun_Ho957066028l_bool_2 tptp.fun_Ho957066028l_bool)))) (= (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool) (ite (= BOUND_VARIABLE_3083 (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool)))) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))))) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) % 138.14/138.41 (define-fun tptp.suc (($x1 tptp.nat)) tptp.nat (ite (= (as @tptp.nat_0 tptp.nat) $x1) (as @tptp.nat_0 tptp.nat) (as @tptp.nat_1 tptp.nat))) % 138.14/138.41 (define-fun tptp.evalc (($x1 tptp.com) ($x2 tptp.state) ($x3 tptp.state)) tptp.bool (as @tptp.bool_0 tptp.bool)) % 138.14/138.41 (define-fun tptp.the_com () tptp.fun_option_com_com (as @tptp.fun_option_com_com_0 tptp.fun_option_com_com)) % 138.14/138.41 (define-fun tptp.bot_bo844097828e_bool () tptp.fun_pname_bool (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool)) % 138.14/138.41 (define-fun tptp.bot_bo1208640912a_bool () tptp.fun_Ho1877127206a_bool (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool)) % 138.14/138.41 (define-fun tptp.collect_pname (($x1 tptp.fun_pname_bool)) tptp.fun_pname_bool (ite (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x1) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) % 138.14/138.41 (define-fun tptp.collec829051333iple_a (($x1 tptp.fun_Ho1877127206a_bool)) tptp.fun_Ho1877127206a_bool (ite (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x1) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) % 138.14/138.41 (define-fun tptp.image_pname_pname (($x1 tptp.fun_pname_pname) ($x2 tptp.fun_pname_bool)) tptp.fun_pname_bool (ite (and (= (as @tptp.fun_pname_pname_0 tptp.fun_pname_pname) $x1) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x2)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) % 138.14/138.41 (define-fun tptp.image_68284913iple_a (($x1 tptp.fun_pn708290217iple_a) ($x2 tptp.fun_pname_bool)) tptp.fun_Ho1877127206a_bool (ite (and (= (as @tptp.fun_pn708290217iple_a_0 tptp.fun_pn708290217iple_a) $x1) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x2)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) % 138.14/138.41 (define-fun tptp.image_1389863321_pname (($x1 tptp.fun_Ho842746065_pname) ($x2 tptp.fun_Ho1877127206a_bool)) tptp.fun_pname_bool (ite (and (= (as @tptp.fun_Ho842746065_pname_0 tptp.fun_Ho842746065_pname) $x1) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool))) % 138.14/138.41 (define-fun tptp.image_590713477iple_a (($x1 tptp.fun_Ho843200573iple_a) ($x2 tptp.fun_Ho1877127206a_bool)) tptp.fun_Ho1877127206a_bool (ite (and (= (as @tptp.fun_Ho843200573iple_a_0 tptp.fun_Ho843200573iple_a) $x1) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool))) % 138.14/138.41 (define-fun tptp.insert_pname ((BOUND_VARIABLE_29415 tptp.pname) (BOUND_VARIABLE_29417 tptp.fun_pname_bool)) tptp.fun_pname_bool (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool)) % 138.14/138.41 (define-fun tptp.insert1434104874iple_a ((BOUND_VARIABLE_29470 tptp.hoare_1927711152iple_a) (BOUND_VARIABLE_29472 tptp.fun_Ho1877127206a_bool)) tptp.fun_Ho1877127206a_bool (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool)) % 138.14/138.41 (define-fun tptp.fFalse () tptp.bool (as @tptp.bool_0 tptp.bool)) % 138.14/138.41 (define-fun tptp.fNot () tptp.fun_bool_bool (as @tptp.fun_bool_bool_1 tptp.fun_bool_bool)) % 138.14/138.41 (define-fun tptp.fTrue () tptp.bool (as @tptp.bool_1 tptp.bool)) % 138.14/138.41 (define-fun tptp.fconj () tptp.fun_bo1549164019l_bool (as @tptp.fun_bo1549164019l_bool_2 tptp.fun_bo1549164019l_bool)) % 138.14/138.41 (define-fun tptp.fdisj () tptp.fun_bo1549164019l_bool (as @tptp.fun_bo1549164019l_bool_1 tptp.fun_bo1549164019l_bool)) % 138.14/138.41 (define-fun tptp.fequal_pname () tptp.fun_pn800050071e_bool (as @tptp.fun_pn800050071e_bool_0 tptp.fun_pn800050071e_bool)) % 138.14/138.41 (define-fun tptp.fequal1440857775iple_a () tptp.fun_Ho440810351a_bool (as @tptp.fun_Ho440810351a_bool_0 tptp.fun_Ho440810351a_bool)) % 138.14/138.41 (define-fun tptp.fimplies () tptp.fun_bo1549164019l_bool (as @tptp.fun_bo1549164019l_bool_0 tptp.fun_bo1549164019l_bool)) % 138.14/138.41 (define-fun tptp.hAPP_c429049308iple_a (($x1 tptp.fun_co1155576772iple_a) ($x2 tptp.com)) tptp.fun_fu1344872529iple_a (as @tptp.fun_fu1344872529iple_a_0 tptp.fun_fu1344872529iple_a)) % 138.14/138.41 (define-fun tptp.hAPP_pname_com (($x1 tptp.fun_pname_com) ($x2 tptp.pname)) tptp.com (as @tptp.com_0 tptp.com)) % 138.14/138.41 (define-fun tptp.hAPP_pname_pname (($x1 tptp.fun_pname_pname) ($x2 tptp.pname)) tptp.pname (as @tptp.pname_0 tptp.pname)) % 138.14/138.41 (define-fun tptp.hAPP_pname_bool (($x1 tptp.fun_pname_bool) ($x2 tptp.pname)) tptp.bool (ite (and (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x1) (= (as @tptp.pname_0 tptp.pname) $x2)) (as @tptp.bool_0 tptp.bool) (as @tptp.bool_1 tptp.bool))) % 138.14/138.41 (define-fun tptp.hAPP_p824302401iple_a (($x1 tptp.fun_pn708290217iple_a) ($x2 tptp.pname)) tptp.hoare_1927711152iple_a (as @tptp.hoare_1927711152iple_a_0 tptp.hoare_1927711152iple_a)) % 138.14/138.41 (define-fun tptp.hAPP_p799580910on_com (($x1 tptp.fun_pname_option_com) ($x2 tptp.pname)) tptp.option_com (as @tptp.option_com_0 tptp.option_com)) % 138.14/138.41 (define-fun tptp.hAPP_p635540397e_bool (($x1 tptp.fun_pn1683930517e_bool) ($x2 tptp.pname)) tptp.fun_a_fun_state_bool (as @tptp.fun_a_fun_state_bool_0 tptp.fun_a_fun_state_bool)) % 138.14/138.41 (define-fun tptp.hAPP_p1788720341iple_a (($x1 tptp.fun_pn308211645iple_a) ($x2 tptp.pname)) tptp.fun_co1155576772iple_a (as @tptp.fun_co1155576772iple_a_0 tptp.fun_co1155576772iple_a)) % 138.14/138.41 (define-fun tptp.hAPP_p61793385e_bool (($x1 tptp.fun_pn800050071e_bool) ($x2 tptp.pname)) tptp.fun_pname_bool (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool)) % 138.14/138.41 (define-fun tptp.hAPP_p393069232l_bool (($x1 tptp.fun_pn250273176l_bool) ($x2 tptp.pname)) tptp.fun_bool_bool (ite (and (= (as @tptp.fun_pn250273176l_bool_0 tptp.fun_pn250273176l_bool) $x1) (= (as @tptp.pname_0 tptp.pname) $x2)) (as @tptp.fun_bool_bool_0 tptp.fun_bool_bool) (ite (and (= (as @tptp.fun_pn250273176l_bool_1 tptp.fun_pn250273176l_bool) $x1) (= (as @tptp.pname_0 tptp.pname) $x2)) (as @tptp.fun_bool_bool_2 tptp.fun_bool_bool) (as @tptp.fun_bool_bool_3 tptp.fun_bool_bool)))) % 138.14/138.41 (define-fun tptp.hAPP_p1513881570iple_a (($x1 tptp.fun_pn579076298iple_a) ($x2 tptp.pname)) tptp.fun_fu1344872529iple_a (as @tptp.fun_fu1344872529iple_a_0 tptp.fun_fu1344872529iple_a)) % 138.14/138.41 (define-fun tptp.hAPP_p338031245l_bool (($x1 tptp.fun_pn422929397l_bool) ($x2 tptp.pname)) tptp.fun_fu1430349052l_bool (as @tptp.fun_fu1430349052l_bool_0 tptp.fun_fu1430349052l_bool)) % 138.14/138.41 (define-fun tptp.hAPP_bool_bool (($x1 tptp.fun_bool_bool) ($x2 tptp.bool)) tptp.bool (ite (and (= (as @tptp.fun_bool_bool_3 tptp.fun_bool_bool) $x1) (= (as @tptp.bool_0 tptp.bool) $x2)) (as @tptp.bool_0 tptp.bool) (ite (and (= (as @tptp.fun_bool_bool_3 tptp.fun_bool_bool) $x1) (= (as @tptp.bool_1 tptp.bool) $x2)) (as @tptp.bool_0 tptp.bool) (ite (and (= (as @tptp.fun_bool_bool_1 tptp.fun_bool_bool) $x1) (= (as @tptp.bool_1 tptp.bool) $x2)) (as @tptp.bool_0 tptp.bool) (ite (and (= (as @tptp.fun_bool_bool_0 tptp.fun_bool_bool) $x1) (= (as @tptp.bool_0 tptp.bool) $x2)) (as @tptp.bool_0 tptp.bool) (as @tptp.bool_1 tptp.bool)))))) % 138.14/138.41 (define-fun tptp.hAPP_b589554111l_bool (($x1 tptp.fun_bo1549164019l_bool) ($x2 tptp.bool)) tptp.fun_bool_bool (ite (and (= (as @tptp.fun_bo1549164019l_bool_2 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.bool_1 tptp.bool) $x2)) (as @tptp.fun_bool_bool_0 tptp.fun_bool_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_0 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.bool_1 tptp.bool) $x2)) (as @tptp.fun_bool_bool_0 tptp.fun_bool_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_1 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.bool_0 tptp.bool) $x2)) (as @tptp.fun_bool_bool_0 tptp.fun_bool_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_0 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.bool_0 tptp.bool) $x2)) (as @tptp.fun_bool_bool_2 tptp.fun_bool_bool) (ite (and (= (as @tptp.fun_bo1549164019l_bool_1 tptp.fun_bo1549164019l_bool) $x1) (= (as @tptp.bool_1 tptp.bool) $x2)) (as @tptp.fun_bool_bool_2 tptp.fun_bool_bool) (as @tptp.fun_bool_bool_3 tptp.fun_bool_bool))))))) % 138.14/138.41 (define-fun tptp.hAPP_H2145880809_pname (($x1 tptp.fun_Ho842746065_pname) ($x2 tptp.hoare_1927711152iple_a)) tptp.pname (as @tptp.pname_0 tptp.pname)) % 138.14/138.41 (define-fun tptp.hAPP_H1448631928a_bool (($x1 tptp.fun_Ho1877127206a_bool) ($x2 tptp.hoare_1927711152iple_a)) tptp.bool (ite (and (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x1) (= (as @tptp.hoare_1927711152iple_a_0 tptp.hoare_1927711152iple_a) $x2)) (as @tptp.bool_0 tptp.bool) (as @tptp.bool_1 tptp.bool))) % 138.14/138.41 (define-fun tptp.hAPP_H963118037iple_a (($x1 tptp.fun_Ho843200573iple_a) ($x2 tptp.hoare_1927711152iple_a)) tptp.hoare_1927711152iple_a (as @tptp.hoare_1927711152iple_a_0 tptp.hoare_1927711152iple_a)) % 138.14/138.41 (define-fun tptp.hAPP_H1487873860l_bool (($x1 tptp.fun_Ho957066028l_bool) ($x2 tptp.hoare_1927711152iple_a)) tptp.fun_bool_bool (ite (and (= (as @tptp.fun_Ho957066028l_bool_0 tptp.fun_Ho957066028l_bool) $x1) (= (as @tptp.hoare_1927711152iple_a_0 tptp.hoare_1927711152iple_a) $x2)) (as @tptp.fun_bool_bool_0 tptp.fun_bool_bool) (ite (and (= (as @tptp.fun_Ho957066028l_bool_1 tptp.fun_Ho957066028l_bool) $x1) (= (as @tptp.hoare_1927711152iple_a_0 tptp.hoare_1927711152iple_a) $x2)) (as @tptp.fun_bool_bool_2 tptp.fun_bool_bool) (as @tptp.fun_bool_bool_3 tptp.fun_bool_bool)))) % 138.14/138.41 (define-fun tptp.hAPP_H1027145665a_bool (($x1 tptp.fun_Ho440810351a_bool) ($x2 tptp.hoare_1927711152iple_a)) tptp.fun_Ho1877127206a_bool (as @tptp.fun_Ho1877127206a_bool_1 tptp.fun_Ho1877127206a_bool)) % 138.14/138.41 (define-fun tptp.hAPP_H694056973l_bool (($x1 tptp.fun_Ho525994229l_bool) ($x2 tptp.hoare_1927711152iple_a)) tptp.fun_fu832487784l_bool (as @tptp.fun_fu832487784l_bool_0 tptp.fun_fu832487784l_bool)) % 138.14/138.41 (define-fun tptp.hAPP_option_com_com (($x1 tptp.fun_option_com_com) ($x2 tptp.option_com)) tptp.com (as @tptp.com_0 tptp.com)) % 138.14/138.41 (define-fun tptp.hAPP_f711275241iple_a (($x1 tptp.fun_fu1344872529iple_a) ($x2 tptp.fun_a_fun_state_bool)) tptp.hoare_1927711152iple_a (as @tptp.hoare_1927711152iple_a_0 tptp.hoare_1927711152iple_a)) % 138.14/138.41 (define-fun tptp.hAPP_f185596029iple_a (($x1 tptp.fun_fu90068325iple_a) ($x2 tptp.fun_a_fun_state_bool)) tptp.fun_co1155576772iple_a (as @tptp.fun_co1155576772iple_a_0 tptp.fun_co1155576772iple_a)) % 138.14/138.42 (define-fun tptp.hAPP_f1664156314l_bool (($x1 tptp.fun_fu1430349052l_bool) ($x2 tptp.fun_pname_bool)) tptp.bool (ite (and (= (as @tptp.fun_fu1430349052l_bool_0 tptp.fun_fu1430349052l_bool) $x1) (= (as @tptp.fun_pname_bool_0 tptp.fun_pname_bool) $x2)) (as @tptp.bool_0 tptp.bool) (as @tptp.bool_1 tptp.bool))) % 138.14/138.42 (define-fun tptp.hAPP_f1454306822l_bool (($x1 tptp.fun_fu832487784l_bool) ($x2 tptp.fun_Ho1877127206a_bool)) tptp.bool (ite (and (= (as @tptp.fun_fu832487784l_bool_0 tptp.fun_fu832487784l_bool) $x1) (= (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool) $x2)) (as @tptp.bool_0 tptp.bool) (as @tptp.bool_1 tptp.bool))) % 138.14/138.42 (define-fun tptp.hBOOL (($x1 tptp.bool)) Bool (= (as @tptp.bool_1 tptp.bool) $x1)) % 138.14/138.42 (define-fun tptp.member_pname () tptp.fun_pn422929397l_bool (as @tptp.fun_pn422929397l_bool_0 tptp.fun_pn422929397l_bool)) % 138.14/138.42 (define-fun tptp.member127332739iple_a () tptp.fun_Ho525994229l_bool (as @tptp.fun_Ho525994229l_bool_0 tptp.fun_Ho525994229l_bool)) % 138.14/138.42 (define-fun tptp.g () tptp.fun_Ho1877127206a_bool (as @tptp.fun_Ho1877127206a_bool_0 tptp.fun_Ho1877127206a_bool)) % 138.14/138.42 (define-fun tptp.p () tptp.fun_pn1683930517e_bool (as @tptp.fun_pn1683930517e_bool_0 tptp.fun_pn1683930517e_bool)) % 138.14/138.42 (define-fun tptp.procs () tptp.fun_pname_bool (as @tptp.fun_pname_bool_1 tptp.fun_pname_bool)) % 138.14/138.42 (define-fun tptp.q () tptp.fun_pn1683930517e_bool (as @tptp.fun_pn1683930517e_bool_0 tptp.fun_pn1683930517e_bool)) % 138.14/138.42 (define-fun tptp.n () tptp.nat (as @tptp.nat_0 tptp.nat)) % 138.14/138.42 ) % 138.14/138.42 % SZS output end Model % 138.14/138.42 % cvc5 exiting %------------------------------------------------------------------------------