%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : SWW748_1 : TPTP v9.2.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n029.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:43 AM UTC 2026 % Result : Satisfiable 11.02s 11.23s % Output : Model 11.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SWW748_1 : TPTP v9.2.1. Released v7.0.0. % 0.12/0.14 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.17/0.35 % Computer : n029.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 22:25:17 EDT 2026 % 0.17/0.35 % CPUTime : % 0.41/0.63 %----Disproving TF0_ARI % 0.41/0.65 --- Run --finite-model-find --decision=internal at 60... % 11.02/11.23 % SZS status Satisfiable % 11.02/11.23 % SZS output start Model % 11.02/11.23 ( % 11.02/11.23 ; cardinality of $$unsorted is 1 % 11.02/11.23 ; rep: (as @$$unsorted_0 $$unsorted) % 11.02/11.23 ; cardinality of tptp.an_Action is 9 % 11.02/11.23 ; rep: (as @tptp.an_Action_0 tptp.an_Action) % 11.02/11.23 ; rep: (as @tptp.an_Action_1 tptp.an_Action) % 11.02/11.23 ; rep: (as @tptp.an_Action_2 tptp.an_Action) % 11.02/11.23 ; rep: (as @tptp.an_Action_3 tptp.an_Action) % 11.02/11.23 ; rep: (as @tptp.an_Action_4 tptp.an_Action) % 11.02/11.23 ; rep: (as @tptp.an_Action_5 tptp.an_Action) % 11.02/11.23 ; rep: (as @tptp.an_Action_6 tptp.an_Action) % 11.02/11.23 ; rep: (as @tptp.an_Action_7 tptp.an_Action) % 11.02/11.23 ; rep: (as @tptp.an_Action_8 tptp.an_Action) % 11.02/11.23 ; cardinality of tptp.a_Role is 6 % 11.02/11.23 ; rep: (as @tptp.a_Role_0 tptp.a_Role) % 11.02/11.23 ; rep: (as @tptp.a_Role_1 tptp.a_Role) % 11.02/11.23 ; rep: (as @tptp.a_Role_2 tptp.a_Role) % 11.02/11.23 ; rep: (as @tptp.a_Role_3 tptp.a_Role) % 11.02/11.23 ; rep: (as @tptp.a_Role_4 tptp.a_Role) % 11.02/11.23 ; rep: (as @tptp.a_Role_5 tptp.a_Role) % 11.02/11.23 ; cardinality of tptp.a_Permission is 6 % 11.02/11.23 ; rep: (as @tptp.a_Permission_0 tptp.a_Permission) % 11.02/11.23 ; rep: (as @tptp.a_Permission_1 tptp.a_Permission) % 11.02/11.23 ; rep: (as @tptp.a_Permission_2 tptp.a_Permission) % 11.02/11.23 ; rep: (as @tptp.a_Permission_3 tptp.a_Permission) % 11.02/11.23 ; rep: (as @tptp.a_Permission_4 tptp.a_Permission) % 11.02/11.23 ; rep: (as @tptp.a_Permission_5 tptp.a_Permission) % 11.02/11.23 ; cardinality of tptp.an_Id is 7 % 11.02/11.23 ; rep: (as @tptp.an_Id_0 tptp.an_Id) % 11.02/11.23 ; rep: (as @tptp.an_Id_1 tptp.an_Id) % 11.02/11.23 ; rep: (as @tptp.an_Id_2 tptp.an_Id) % 11.02/11.23 ; rep: (as @tptp.an_Id_3 tptp.an_Id) % 11.02/11.23 ; rep: (as @tptp.an_Id_4 tptp.an_Id) % 11.02/11.23 ; rep: (as @tptp.an_Id_5 tptp.an_Id) % 11.02/11.23 ; rep: (as @tptp.an_Id_6 tptp.an_Id) % 11.02/11.23 (define-fun tptp.client () tptp.a_Role (as @tptp.a_Role_5 tptp.a_Role)) % 11.02/11.23 (define-fun tptp.finadmin () tptp.a_Role (as @tptp.a_Role_1 tptp.a_Role)) % 11.02/11.23 (define-fun tptp.finclerk () tptp.a_Role (as @tptp.a_Role_2 tptp.a_Role)) % 11.02/11.23 (define-fun tptp.manager () tptp.a_Role (as @tptp.a_Role_0 tptp.a_Role)) % 11.02/11.23 (define-fun tptp.poadmin () tptp.a_Role (as @tptp.a_Role_3 tptp.a_Role)) % 11.02/11.23 (define-fun tptp.poclerk () tptp.a_Role (as @tptp.a_Role_4 tptp.a_Role)) % 11.02/11.23 (define-fun tptp.action2int (($x1 tptp.an_Action)) Int (ite (= (as @tptp.an_Action_0 tptp.an_Action) $x1) 1 (ite (= (as @tptp.an_Action_1 tptp.an_Action) $x1) 2 (ite (= (as @tptp.an_Action_2 tptp.an_Action) $x1) 3 (ite (= (as @tptp.an_Action_3 tptp.an_Action) $x1) 4 (ite (= (as @tptp.an_Action_4 tptp.an_Action) $x1) 5 (ite (= (as @tptp.an_Action_5 tptp.an_Action) $x1) 6 (ite (= (as @tptp.an_Action_6 tptp.an_Action) $x1) 7 (ite (= (as @tptp.an_Action_7 tptp.an_Action) $x1) 8 9))))))))) % 11.02/11.23 (define-fun tptp.id1 () tptp.an_Id (as @tptp.an_Id_5 tptp.an_Id)) % 11.02/11.23 (define-fun tptp.id2 () tptp.an_Id (as @tptp.an_Id_4 tptp.an_Id)) % 11.02/11.23 (define-fun tptp.id2int (($x1 tptp.an_Id)) Int (ite (= (as @tptp.an_Id_5 tptp.an_Id) $x1) 1 (ite (= (as @tptp.an_Id_4 tptp.an_Id) $x1) 2 (ite (= (as @tptp.an_Id_6 tptp.an_Id) $x1) 3 (ite (= (as @tptp.an_Id_1 tptp.an_Id) $x1) 4 (ite (= (as @tptp.an_Id_3 tptp.an_Id) $x1) 5 (ite (= (as @tptp.an_Id_0 tptp.an_Id) $x1) 6 7))))))) % 11.02/11.23 (define-fun tptp.id3 () tptp.an_Id (as @tptp.an_Id_6 tptp.an_Id)) % 11.02/11.23 (define-fun tptp.id4 () tptp.an_Id (as @tptp.an_Id_1 tptp.an_Id)) % 11.02/11.23 (define-fun tptp.id5 () tptp.an_Id (as @tptp.an_Id_3 tptp.an_Id)) % 11.02/11.23 (define-fun tptp.id6 () tptp.an_Id (as @tptp.an_Id_0 tptp.an_Id)) % 11.02/11.23 (define-fun tptp.id7 () tptp.an_Id (as @tptp.an_Id_2 tptp.an_Id)) % 11.02/11.23 (define-fun tptp.p1 () tptp.a_Permission (as @tptp.a_Permission_0 tptp.a_Permission)) % 11.02/11.23 (define-fun tptp.p2 () tptp.a_Permission (as @tptp.a_Permission_1 tptp.a_Permission)) % 11.02/11.23 (define-fun tptp.p3 () tptp.a_Permission (as @tptp.a_Permission_2 tptp.a_Permission)) % 11.02/11.23 (define-fun tptp.p4 () tptp.a_Permission (as @tptp.a_Permission_3 tptp.a_Permission)) % 11.02/11.23 (define-fun tptp.p5 () tptp.a_Permission (as @tptp.a_Permission_4 tptp.a_Permission)) % 11.02/11.23 (define-fun tptp.p6 () tptp.a_Permission (as @tptp.a_Permission_5 tptp.a_Permission)) % 11.02/11.23 (define-fun tptp.permission2int (($x1 tptp.a_Permission)) Int (ite (= (as @tptp.a_Permission_0 tptp.a_Permission) $x1) 1 (ite (= (as @tptp.a_Permission_1 tptp.a_Permission) $x1) 2 (ite (= (as @tptp.a_Permission_2 tptp.a_Permission) $x1) 3 (ite (= (as @tptp.a_Permission_3 tptp.a_Permission) $x1) 4 (ite (= (as @tptp.a_Permission_4 tptp.a_Permission) $x1) 5 6)))))) % 11.02/11.23 (define-fun tptp.role2int (($x1 tptp.a_Role)) Int (ite (= (as @tptp.a_Role_0 tptp.a_Role) $x1) 1 (ite (= (as @tptp.a_Role_1 tptp.a_Role) $x1) 2 (ite (= (as @tptp.a_Role_2 tptp.a_Role) $x1) 3 (ite (= (as @tptp.a_Role_3 tptp.a_Role) $x1) 4 (ite (= (as @tptp.a_Role_4 tptp.a_Role) $x1) 5 6)))))) % 11.02/11.23 (define-fun tptp.role_level (($x1 tptp.a_Role)) Int (ite (= (as @tptp.a_Role_2 tptp.a_Role) $x1) 1 (ite (= (as @tptp.a_Role_4 tptp.a_Role) $x1) 1 (ite (= (as @tptp.a_Role_1 tptp.a_Role) $x1) 2 (ite (= (as @tptp.a_Role_3 tptp.a_Role) $x1) 2 (ite (= (as @tptp.a_Role_0 tptp.a_Role) $x1) 3 0)))))) % 11.02/11.23 (define-fun tptp.t1_receive () tptp.an_Action (as @tptp.an_Action_0 tptp.an_Action)) % 11.02/11.23 (define-fun tptp.t2_invoke () tptp.an_Action (as @tptp.an_Action_1 tptp.an_Action)) % 11.02/11.23 (define-fun tptp.t3_split () tptp.an_Action (as @tptp.an_Action_2 tptp.an_Action)) % 11.02/11.23 (define-fun tptp.t4_join () tptp.an_Action (as @tptp.an_Action_3 tptp.an_Action)) % 11.02/11.23 (define-fun tptp.t5_invoke () tptp.an_Action (as @tptp.an_Action_4 tptp.an_Action)) % 11.02/11.23 (define-fun tptp.t6_invoke () tptp.an_Action (as @tptp.an_Action_5 tptp.an_Action)) % 11.02/11.23 (define-fun tptp.t7_invokeo () tptp.an_Action (as @tptp.an_Action_6 tptp.an_Action)) % 11.02/11.23 (define-fun tptp.t8_invokei () tptp.an_Action (as @tptp.an_Action_7 tptp.an_Action)) % 11.02/11.23 (define-fun tptp.t9_invoke () tptp.an_Action (as @tptp.an_Action_8 tptp.an_Action)) % 11.02/11.23 (define-fun tptp.in_creator_ctrpay_0 () Int 1) % 11.02/11.23 (define-fun tptp.in_creator_ctrpay_1 () Int 1) % 11.02/11.23 (define-fun tptp.in_creator_ctrpay_2 () Int 1) % 11.02/11.23 (define-fun tptp.in_creator_ctrpay_3 () Int 1) % 11.02/11.23 (define-fun tptp.in_creator_ctrpay_4 () Int 1) % 11.02/11.23 (define-fun tptp.in_creator_ctrpay_5 () Int 1) % 11.02/11.23 (define-fun tptp.in_creator_ctrpay_6 () Int 1) % 11.02/11.23 (define-fun tptp.in_creator_ctrpay_7 () Int 0) % 11.02/11.23 (define-fun tptp.in_creator_ctrpay_8 () Int 0) % 11.02/11.23 (define-fun tptp.in_creator_ctrpay_9 () Int 0) % 11.02/11.23 (define-fun tptp.in_customer_crtpo_0 () Int 1) % 11.02/11.23 (define-fun tptp.in_customer_crtpo_1 () Int 0) % 11.02/11.23 (define-fun tptp.in_customer_crtpo_2 () Int 0) % 11.02/11.23 (define-fun tptp.in_customer_crtpo_3 () Int 0) % 11.02/11.23 (define-fun tptp.in_customer_crtpo_4 () Int 0) % 11.02/11.23 (define-fun tptp.in_customer_crtpo_5 () Int 0) % 11.02/11.23 (define-fun tptp.in_customer_crtpo_6 () Int 0) % 11.02/11.23 (define-fun tptp.in_customer_crtpo_7 () Int 0) % 11.02/11.23 (define-fun tptp.in_customer_crtpo_8 () Int 0) % 11.02/11.23 (define-fun tptp.in_customer_crtpo_9 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpopayment_apprpay_0 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpopayment_apprpay_1 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpopayment_apprpay_2 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpopayment_apprpay_3 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpopayment_apprpay_4 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpopayment_apprpay_5 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpopayment_apprpay_6 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpopayment_apprpay_7 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpopayment_apprpay_8 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpopayment_apprpay_9 () Int 1) % 11.02/11.23 (define-fun tptp.out_approverpo_apprpo_0 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpo_apprpo_1 () Int 0) % 11.02/11.23 (define-fun tptp.out_approverpo_apprpo_2 () Int 1) % 11.02/11.23 (define-fun tptp.out_approverpo_apprpo_3 () Int 1) % 11.02/11.23 (define-fun tptp.out_approverpo_apprpo_4 () Int 1) % 11.02/11.23 (define-fun tptp.out_approverpo_apprpo_5 () Int 1) % 11.02/11.23 (define-fun tptp.out_approverpo_apprpo_6 () Int 1) % 11.02/11.23 (define-fun tptp.out_approverpo_apprpo_7 () Int 1) % 11.02/11.23 (define-fun tptp.out_approverpo_apprpo_8 () Int 1) % 11.02/11.23 (define-fun tptp.out_approverpo_apprpo_9 () Int 1) % 11.02/11.23 (define-fun tptp.out_creator_ctrpay_0 () Int 0) % 11.02/11.23 (define-fun tptp.out_creator_ctrpay_1 () Int 0) % 11.02/11.23 (define-fun tptp.out_creator_ctrpay_2 () Int 0) % 11.02/11.23 (define-fun tptp.out_creator_ctrpay_3 () Int 0) % 11.02/11.23 (define-fun tptp.out_creator_ctrpay_4 () Int 0) % 11.02/11.23 (define-fun tptp.out_creator_ctrpay_5 () Int 0) % 11.02/11.23 (define-fun tptp.out_creator_ctrpay_6 () Int 1) % 11.02/11.23 (define-fun tptp.out_creator_ctrpay_7 () Int 1) % 11.02/11.23 (define-fun tptp.out_creator_ctrpay_8 () Int 1) % 11.02/11.23 (define-fun tptp.out_creator_ctrpay_9 () Int 1) % 11.02/11.23 (define-fun tptp.out_signergrn_ctrsigngrn_0 () Int 0) % 11.02/11.23 (define-fun tptp.out_signergrn_ctrsigngrn_1 () Int 0) % 11.02/11.23 (define-fun tptp.out_signergrn_ctrsigngrn_2 () Int 0) % 11.02/11.23 (define-fun tptp.out_signergrn_ctrsigngrn_3 () Int 0) % 11.02/11.23 (define-fun tptp.out_signergrn_ctrsigngrn_4 () Int 0) % 11.02/11.23 (define-fun tptp.out_signergrn_ctrsigngrn_5 () Int 1) % 11.02/11.23 (define-fun tptp.out_signergrn_ctrsigngrn_6 () Int 1) % 11.02/11.23 (define-fun tptp.out_signergrn_ctrsigngrn_7 () Int 1) % 11.02/11.23 (define-fun tptp.out_signergrn_ctrsigngrn_8 () Int 1) % 11.02/11.23 (define-fun tptp.out_signergrn_ctrsigngrn_9 () Int 1) % 11.02/11.23 (define-fun tptp.out_signergrn_signgrn_0 () Int 0) % 11.02/11.23 (define-fun tptp.out_signergrn_signgrn_1 () Int 0) % 11.02/11.23 (define-fun tptp.out_signergrn_signgrn_2 () Int 0) % 11.02/11.23 (define-fun tptp.out_signergrn_signgrn_3 () Int 0) % 11.02/11.23 (define-fun tptp.out_signergrn_signgrn_4 () Int 1) % 11.02/11.23 (define-fun tptp.out_signergrn_signgrn_5 () Int 1) % 11.02/11.23 (define-fun tptp.out_signergrn_signgrn_6 () Int 1) % 11.02/11.23 (define-fun tptp.out_signergrn_signgrn_7 () Int 1) % 11.02/11.23 (define-fun tptp.out_signergrn_signgrn_8 () Int 1) % 11.02/11.23 (define-fun tptp.out_signergrn_signgrn_9 () Int 1) % 11.02/11.23 (define-fun tptp.p10_final_0 () Int 0) % 11.02/11.23 (define-fun tptp.p10_final_1 () Int 1) % 11.02/11.23 (define-fun tptp.p10_final_2 () Int 0) % 11.02/11.23 (define-fun tptp.p10_final_3 () Int 0) % 11.02/11.23 (define-fun tptp.p10_final_4 () Int 0) % 11.02/11.23 (define-fun tptp.p10_final_5 () Int 0) % 11.02/11.23 (define-fun tptp.p10_final_6 () Int 0) % 11.02/11.23 (define-fun tptp.p10_final_7 () Int 0) % 11.02/11.23 (define-fun tptp.p10_final_8 () Int 0) % 11.02/11.23 (define-fun tptp.p10_final_9 () Int 0) % 11.02/11.23 (define-fun tptp.p11_final_0 () Int 0) % 11.02/11.23 (define-fun tptp.p11_final_1 () Int 0) % 11.02/11.23 (define-fun tptp.p11_final_2 () Int 0) % 11.02/11.23 (define-fun tptp.p11_final_3 () Int 0) % 11.02/11.23 (define-fun tptp.p11_final_4 () Int 0) % 11.02/11.23 (define-fun tptp.p11_final_5 () Int 0) % 11.02/11.23 (define-fun tptp.p11_final_6 () Int 0) % 11.02/11.23 (define-fun tptp.p11_final_7 () Int 0) % 11.02/11.23 (define-fun tptp.p11_final_8 () Int 0) % 11.02/11.23 (define-fun tptp.p11_final_9 () Int 1) % 11.02/11.23 (define-fun tptp.p1_final_0 () Int 0) % 11.02/11.23 (define-fun tptp.p1_final_1 () Int 0) % 11.02/11.23 (define-fun tptp.p1_final_2 () Int 1) % 11.02/11.23 (define-fun tptp.p1_final_3 () Int 0) % 11.02/11.23 (define-fun tptp.p1_final_4 () Int 0) % 11.02/11.23 (define-fun tptp.p1_final_5 () Int 0) % 11.02/11.23 (define-fun tptp.p1_final_6 () Int 0) % 11.02/11.23 (define-fun tptp.p1_final_7 () Int 0) % 11.02/11.23 (define-fun tptp.p1_final_8 () Int 0) % 11.02/11.23 (define-fun tptp.p1_final_9 () Int 0) % 11.02/11.23 (define-fun tptp.p2_final_0 () Int 0) % 11.02/11.23 (define-fun tptp.p2_final_1 () Int 0) % 11.02/11.23 (define-fun tptp.p2_final_2 () Int 0) % 11.02/11.23 (define-fun tptp.p2_final_3 () Int 0) % 11.02/11.23 (define-fun tptp.p2_final_4 () Int 0) % 11.02/11.23 (define-fun tptp.p2_final_5 () Int 0) % 11.02/11.23 (define-fun tptp.p2_final_6 () Int 0) % 11.02/11.23 (define-fun tptp.p2_final_7 () Int 0) % 11.02/11.23 (define-fun tptp.p2_final_8 () Int 1) % 11.02/11.23 (define-fun tptp.p2_final_9 () Int 0) % 11.02/11.23 (define-fun tptp.p3_running_0 () Int 0) % 11.02/11.23 (define-fun tptp.p3_running_1 () Int 0) % 11.02/11.23 (define-fun tptp.p3_running_2 () Int 0) % 11.02/11.23 (define-fun tptp.p3_running_3 () Int 0) % 11.02/11.23 (define-fun tptp.p3_running_4 () Int 0) % 11.02/11.23 (define-fun tptp.p3_running_5 () Int 0) % 11.02/11.23 (define-fun tptp.p3_running_6 () Int 1) % 11.02/11.23 (define-fun tptp.p3_running_7 () Int 0) % 11.02/11.23 (define-fun tptp.p3_running_8 () Int 0) % 11.02/11.23 (define-fun tptp.p3_running_9 () Int 0) % 11.02/11.23 (define-fun tptp.p4_final_0 () Int 0) % 11.02/11.23 (define-fun tptp.p4_final_1 () Int 0) % 11.02/11.23 (define-fun tptp.p4_final_2 () Int 0) % 11.02/11.23 (define-fun tptp.p4_final_3 () Int 0) % 11.02/11.23 (define-fun tptp.p4_final_4 () Int 0) % 11.02/11.23 (define-fun tptp.p4_final_5 () Int 1) % 11.02/11.23 (define-fun tptp.p4_final_6 () Int 1) % 11.02/11.23 (define-fun tptp.p4_final_7 () Int 1) % 11.02/11.23 (define-fun tptp.p4_final_8 () Int 0) % 11.02/11.23 (define-fun tptp.p4_final_9 () Int 0) % 11.02/11.23 (define-fun tptp.p5_final_0 () Int 0) % 11.02/11.23 (define-fun tptp.p5_final_1 () Int 0) % 11.02/11.23 (define-fun tptp.p5_final_2 () Int 0) % 11.02/11.23 (define-fun tptp.p5_final_3 () Int 0) % 11.02/11.23 (define-fun tptp.p5_final_4 () Int 0) % 11.02/11.23 (define-fun tptp.p5_final_5 () Int 0) % 11.02/11.23 (define-fun tptp.p5_final_6 () Int 0) % 11.02/11.23 (define-fun tptp.p5_final_7 () Int 1) % 11.02/11.23 (define-fun tptp.p5_final_8 () Int 0) % 11.02/11.23 (define-fun tptp.p5_final_9 () Int 0) % 11.02/11.23 (define-fun tptp.p6_initial_0 () Int 0) % 11.02/11.23 (define-fun tptp.p6_initial_1 () Int 0) % 11.02/11.23 (define-fun tptp.p6_initial_2 () Int 0) % 11.02/11.23 (define-fun tptp.p6_initial_3 () Int 1) % 11.02/11.23 (define-fun tptp.p6_initial_4 () Int 0) % 11.02/11.23 (define-fun tptp.p6_initial_5 () Int 0) % 11.02/11.23 (define-fun tptp.p6_initial_6 () Int 0) % 11.02/11.23 (define-fun tptp.p6_initial_7 () Int 0) % 11.02/11.23 (define-fun tptp.p6_initial_8 () Int 0) % 11.02/11.23 (define-fun tptp.p6_initial_9 () Int 0) % 11.02/11.23 (define-fun tptp.p7_final_0 () Int 0) % 11.02/11.23 (define-fun tptp.p7_final_1 () Int 0) % 11.02/11.23 (define-fun tptp.p7_final_2 () Int 0) % 11.02/11.23 (define-fun tptp.p7_final_3 () Int 0) % 11.02/11.23 (define-fun tptp.p7_final_4 () Int 1) % 11.02/11.23 (define-fun tptp.p7_final_5 () Int 0) % 11.02/11.23 (define-fun tptp.p7_final_6 () Int 0) % 11.02/11.23 (define-fun tptp.p7_final_7 () Int 0) % 11.02/11.23 (define-fun tptp.p7_final_8 () Int 0) % 11.02/11.23 (define-fun tptp.p7_final_9 () Int 0) % 11.02/11.23 (define-fun tptp.p8_initial_0 () Int 0) % 11.02/11.23 (define-fun tptp.p8_initial_1 () Int 0) % 11.02/11.23 (define-fun tptp.p8_initial_2 () Int 0) % 11.02/11.23 (define-fun tptp.p8_initial_3 () Int 1) % 11.02/11.23 (define-fun tptp.p8_initial_4 () Int 1) % 11.02/11.23 (define-fun tptp.p8_initial_5 () Int 1) % 11.02/11.23 (define-fun tptp.p8_initial_6 () Int 0) % 11.02/11.23 (define-fun tptp.p8_initial_7 () Int 0) % 11.02/11.23 (define-fun tptp.p8_initial_8 () Int 0) % 11.02/11.23 (define-fun tptp.p8_initial_9 () Int 0) % 11.02/11.23 (define-fun tptp.p9_initial_0 () Int 1) % 11.02/11.23 (define-fun tptp.p9_initial_1 () Int 0) % 11.02/11.23 (define-fun tptp.p9_initial_2 () Int 0) % 11.02/11.23 (define-fun tptp.p9_initial_3 () Int 0) % 11.02/11.23 (define-fun tptp.p9_initial_4 () Int 0) % 11.02/11.23 (define-fun tptp.p9_initial_5 () Int 0) % 11.02/11.23 (define-fun tptp.p9_initial_6 () Int 0) % 11.02/11.23 (define-fun tptp.p9_initial_7 () Int 0) % 11.02/11.23 (define-fun tptp.p9_initial_8 () Int 0) % 11.02/11.23 (define-fun tptp.p9_initial_9 () Int 0) % 11.02/11.23 (define-fun tptp.has_permission (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_8 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_8 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_8 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.permission (($x1 tptp.a_Permission) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.a_Permission_1 tptp.a_Permission) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.a_Permission_2 tptp.a_Permission) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.a_Permission_3 tptp.a_Permission) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.a_Permission_3 tptp.a_Permission) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.a_Permission_4 tptp.a_Permission) $x1) (= (as @tptp.an_Action_8 tptp.an_Action) $x2)) (and (= (as @tptp.a_Permission_5 tptp.a_Permission) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.a_Permission_0 tptp.a_Permission) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.role ((_arg_1 tptp.a_Role)) Bool false) % 11.02/11.23 (define-fun tptp.role_le (($x1 tptp.a_Role) ($x2 tptp.a_Role)) Bool (or (and (= (as @tptp.a_Role_5 tptp.a_Role) $x1) (= (as @tptp.a_Role_4 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_2 tptp.a_Role) $x1) (= (as @tptp.a_Role_1 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_3 tptp.a_Role) $x1) (= (as @tptp.a_Role_0 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_1 tptp.a_Role) $x1) (= (as @tptp.a_Role_0 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_4 tptp.a_Role) $x1) (= (as @tptp.a_Role_0 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_4 tptp.a_Role) $x1) (= (as @tptp.a_Role_3 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_4 tptp.a_Role) $x1) (= (as @tptp.a_Role_1 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_2 tptp.a_Role) $x1) (= (as @tptp.a_Role_0 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_5 tptp.a_Role) $x1) (= (as @tptp.a_Role_2 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_2 tptp.a_Role) $x1) (= (as @tptp.a_Role_3 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_5 tptp.a_Role) $x1) (= (as @tptp.a_Role_1 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_5 tptp.a_Role) $x1) (= (as @tptp.a_Role_3 tptp.a_Role) $x2)) (and (= (as @tptp.a_Role_5 tptp.a_Role) $x1) (= (as @tptp.a_Role_0 tptp.a_Role) $x2)))) % 11.02/11.23 (define-fun tptp.role_permission_assign (($x1 tptp.a_Role) ($x2 tptp.a_Permission)) Bool (or (and (= (as @tptp.a_Role_0 tptp.a_Role) $x1) (= (as @tptp.a_Permission_3 tptp.a_Permission) $x2)) (and (= (as @tptp.a_Role_4 tptp.a_Role) $x1) (= (as @tptp.a_Permission_2 tptp.a_Permission) $x2)) (and (= (as @tptp.a_Role_2 tptp.a_Role) $x1) (= (as @tptp.a_Permission_3 tptp.a_Permission) $x2)) (and (= (as @tptp.a_Role_3 tptp.a_Role) $x1) (= (as @tptp.a_Permission_0 tptp.a_Permission) $x2)) (and (= (as @tptp.a_Role_3 tptp.a_Role) $x1) (= (as @tptp.a_Permission_2 tptp.a_Permission) $x2)) (and (= (as @tptp.a_Role_1 tptp.a_Role) $x1) (= (as @tptp.a_Permission_4 tptp.a_Permission) $x2)) (and (= (as @tptp.a_Role_1 tptp.a_Role) $x1) (= (as @tptp.a_Permission_3 tptp.a_Permission) $x2)) (and (= (as @tptp.a_Role_0 tptp.a_Role) $x1) (= (as @tptp.a_Permission_0 tptp.a_Permission) $x2)) (and (= (as @tptp.a_Role_0 tptp.a_Role) $x1) (= (as @tptp.a_Permission_2 tptp.a_Permission) $x2)) (and (= (as @tptp.a_Role_5 tptp.a_Role) $x1) (= (as @tptp.a_Permission_5 tptp.a_Permission) $x2)) (and (= (as @tptp.a_Role_0 tptp.a_Role) $x1) (= (as @tptp.a_Permission_4 tptp.a_Permission) $x2)) (and (= (as @tptp.a_Role_5 tptp.a_Role) $x1) (= (as @tptp.a_Permission_1 tptp.a_Permission) $x2)))) % 11.02/11.23 (define-fun tptp.user ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.user_role_assign (($x1 tptp.an_Id) ($x2 tptp.a_Role)) Bool (or (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.a_Role_1 tptp.a_Role) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.a_Role_3 tptp.a_Role) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.a_Role_4 tptp.a_Role) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.a_Role_0 tptp.a_Role) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.a_Role_0 tptp.a_Role) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.a_Role_2 tptp.a_Role) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.a_Role_5 tptp.a_Role) $x2)))) % 11.02/11.23 (define-fun tptp.can_exec_0 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.can_exec_1 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.can_exec_2 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.can_exec_3 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.can_exec_4 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.can_exec_5 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.can_exec_6 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.can_exec_7 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_8 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_8 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.can_exec_8 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_8 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_8 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.can_exec_9 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_6 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_8 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_8 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.executed_0 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool false) % 11.02/11.23 (define-fun tptp.executed_1 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2))) % 11.02/11.23 (define-fun tptp.executed_2 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.executed_3 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_2 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.executed_4 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_2 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.executed_5 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_2 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.executed_6 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_2 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.executed_7 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_2 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.executed_8 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_2 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_3 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.executed_9 (($x1 tptp.an_Id) ($x2 tptp.an_Action)) Bool (or (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_0 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_6 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_4 tptp.an_Id) $x1) (= (as @tptp.an_Action_7 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_0 tptp.an_Id) $x1) (= (as @tptp.an_Action_4 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_3 tptp.an_Id) $x1) (= (as @tptp.an_Action_5 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_2 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_5 tptp.an_Id) $x1) (= (as @tptp.an_Action_8 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_2 tptp.an_Id) $x1) (= (as @tptp.an_Action_3 tptp.an_Action) $x2)) (and (= (as @tptp.an_Id_1 tptp.an_Id) $x1) (= (as @tptp.an_Action_1 tptp.an_Action) $x2)))) % 11.02/11.23 (define-fun tptp.initial_pm_0 () Bool true) % 11.02/11.23 (define-fun tptp.initial_wf_0 () Bool true) % 11.02/11.23 (define-fun tptp.t1_receive_0_1 (($x1 tptp.an_Id)) Bool (= (as @tptp.an_Id_0 tptp.an_Id) $x1)) % 11.02/11.23 (define-fun tptp.t1_receive_1_2 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t1_receive_2_3 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t1_receive_3_4 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t1_receive_4_5 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t1_receive_5_6 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t1_receive_6_7 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t1_receive_7_8 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t1_receive_8_9 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t2_invoke_0_1 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t2_invoke_1_2 (($x1 tptp.an_Id)) Bool (= (as @tptp.an_Id_1 tptp.an_Id) $x1)) % 11.02/11.23 (define-fun tptp.t2_invoke_2_3 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t2_invoke_3_4 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t2_invoke_4_5 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t2_invoke_5_6 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t2_invoke_6_7 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t2_invoke_7_8 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t2_invoke_8_9 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t3_split_0_1 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t3_split_1_2 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t3_split_2_3 (($x1 tptp.an_Id)) Bool (= (as @tptp.an_Id_2 tptp.an_Id) $x1)) % 11.02/11.23 (define-fun tptp.t3_split_3_4 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t3_split_4_5 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t3_split_5_6 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t3_split_6_7 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t3_split_7_8 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t3_split_8_9 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t4_join_0_1 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t4_join_1_2 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t4_join_2_3 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t4_join_3_4 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t4_join_4_5 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t4_join_5_6 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t4_join_6_7 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t4_join_7_8 (($x1 tptp.an_Id)) Bool (= (as @tptp.an_Id_2 tptp.an_Id) $x1)) % 11.02/11.23 (define-fun tptp.t4_join_8_9 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t5_invoke_0_1 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t5_invoke_1_2 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t5_invoke_2_3 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t5_invoke_3_4 (($x1 tptp.an_Id)) Bool (= (as @tptp.an_Id_0 tptp.an_Id) $x1)) % 11.02/11.23 (define-fun tptp.t5_invoke_4_5 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t5_invoke_5_6 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t5_invoke_6_7 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t5_invoke_7_8 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t5_invoke_8_9 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t6_invoke_0_1 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t6_invoke_1_2 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t6_invoke_2_3 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t6_invoke_3_4 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t6_invoke_4_5 (($x1 tptp.an_Id)) Bool (= (as @tptp.an_Id_3 tptp.an_Id) $x1)) % 11.02/11.23 (define-fun tptp.t6_invoke_5_6 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t6_invoke_6_7 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t6_invoke_7_8 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t6_invoke_8_9 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t7_invokeo_0_1 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t7_invokeo_1_2 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t7_invokeo_2_3 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t7_invokeo_3_4 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t7_invokeo_4_5 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t7_invokeo_5_6 (($x1 tptp.an_Id)) Bool (= (as @tptp.an_Id_4 tptp.an_Id) $x1)) % 11.02/11.23 (define-fun tptp.t7_invokeo_6_7 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t7_invokeo_7_8 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t7_invokeo_8_9 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t8_invokei_0_1 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t8_invokei_1_2 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t8_invokei_2_3 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t8_invokei_3_4 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t8_invokei_4_5 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t8_invokei_5_6 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t8_invokei_6_7 (($x1 tptp.an_Id)) Bool (= (as @tptp.an_Id_4 tptp.an_Id) $x1)) % 11.02/11.23 (define-fun tptp.t8_invokei_7_8 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t8_invokei_8_9 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t9_invoke_0_1 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t9_invoke_1_2 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t9_invoke_2_3 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t9_invoke_3_4 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t9_invoke_4_5 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t9_invoke_5_6 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t9_invoke_6_7 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t9_invoke_7_8 ((_arg_1 tptp.an_Id)) Bool false) % 11.02/11.23 (define-fun tptp.t9_invoke_8_9 (($x1 tptp.an_Id)) Bool (= (as @tptp.an_Id_5 tptp.an_Id) $x1)) % 11.02/11.23 ) % 11.02/11.24 % SZS output end Model % 11.02/11.24 % cvc5 exiting %------------------------------------------------------------------------------