%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : ITP006_2 : TPTP v8.1.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n026.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 : 600s % DateTime : Sun Jul 17 00:39:41 EDT 2022 % Result : Theorem 40.70s 23.78s % Output : Refutation 40.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ITP006_2 : TPTP v8.1.0. Bugfixed v7.5.0. % 0.03/0.12 % Command : spasst-tptp-script %s %d % 0.13/0.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sat Jun 4 02:58:43 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.47 % Using EUF theory % 40.70/23.78 % 40.70/23.78 % 40.70/23.78 % SZS status Theorem for /tmp/SPASST_16300_n026.cluster.edu % 40.70/23.78 % 40.70/23.78 SPASS V 2.2.22 in combination with yices. % 40.70/23.78 SPASS beiseite: Proof found by SPASS. % 40.70/23.78 Problem: /tmp/SPASST_16300_n026.cluster.edu % 40.70/23.78 SPASS derived 41361 clauses, backtracked 9547 clauses and kept 15228 clauses. % 40.70/23.78 SPASS backtracked 28 times (0 times due to theory inconsistency). % 40.70/23.78 SPASS allocated 66779 KBytes. % 40.70/23.78 SPASS spent 0:00:22.25 on the problem. % 40.70/23.78 0:00:00.00 for the input. % 40.70/23.78 0:00:00.22 for the FLOTTER CNF translation. % 40.70/23.78 0:00:00.32 for inferences. % 40.70/23.78 0:00:00.80 for the backtracking. % 40.70/23.78 0:00:18.72 for the reduction. % 40.70/23.78 0:00:00.67 for interacting with the SMT procedure. % 40.70/23.78 % 40.70/23.78 % 40.70/23.78 % SZS output start CNFRefutation for /tmp/SPASST_16300_n026.cluster.edu % 40.70/23.78 % 40.70/23.78 % Here is a proof with depth 13, length 628 : % 40.70/23.78 21[0:Inp] || -> p(c_2Ebool_2ET)*. % 40.70/23.78 22[0:Inp] || -> tp__o(fo__c_2Ebool_2EF)*. % 40.70/23.78 23[0:Inp] || -> tp__o(fo__c_2Ebool_2ET)*. % 40.70/23.78 26[0:Inp] || -> del(bool)*. % 40.70/23.78 28[0:Inp] || -> del(skc8)*. % 40.70/23.78 29[0:Inp] || -> del(skc7)*. % 40.70/23.78 30[0:Inp] || p(c_2Ebool_2EF)* -> . % 40.70/23.78 31[0:Inp] || -> mem(c_2Ebool_2EF,bool)*. % 40.70/23.78 32[0:Inp] || -> mem(c_2Ebool_2ET,bool)*. % 40.70/23.78 33[0:Inp] || -> tp__o(surj__o(U))*. % 40.70/23.78 34[0:Inp] || -> equal(inj__o(fo__c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 35[0:Inp] || -> equal(inj__o(fo__c_2Ebool_2ET),c_2Ebool_2ET)**. % 40.70/23.78 36[0:Inp] || -> mem(c_2Ebool_2E_7E,arr(bool,bool))*. % 40.70/23.78 37[0:Inp] || -> mem(skc11,arr(skc8,bool))*. % 40.70/23.78 38[0:Inp] || -> mem(skc10,arr(skc8,bool))*. % 40.70/23.78 39[0:Inp] || -> mem(skc9,arr(skc7,skc8))*. % 40.70/23.78 42[0:Inp] || tp__o(U) -> tp__o(fo__c_2Ebool_2E_7E(U))*. % 40.70/23.78 50[0:Inp] || tp__o(U) -> mem(inj__o(U),bool)*. % 40.70/23.78 55[0:Inp] || tp__o(U) -> equal(surj__o(inj__o(U)),U)**. % 40.70/23.78 56[0:Inp] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),skc10))*. % 40.70/23.78 59[0:Inp] || mem(U,bool) -> equal(inj__o(surj__o(U)),U)**. % 40.70/23.78 60[0:Inp] || p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),skc11))* -> . % 40.70/23.78 65[0:Inp] || mem(U,bool) -> p(U) p(ap(c_2Ebool_2E_7E,U))*. % 40.70/23.78 66[0:Inp] || tp__o(U) tp__o(V) -> tp__o(fo__c_2Emin_2E_3D_3D_3E(U,V))*. % 40.70/23.78 67[0:Inp] || tp__o(U) tp__o(V) -> tp__o(fo__c_2Ebool_2E_2F_5C(U,V))*. % 40.70/23.78 68[0:Inp] || tp__o(U) tp__o(V) -> tp__o(fo__c_2Ebool_2E_5C_2F(U,V))*. % 40.70/23.78 69[0:Inp] || del(U) del(V) -> del(arr(U,V))*. % 40.70/23.78 79[0:Inp] || tp__o(U) -> equal(ap(c_2Ebool_2E_7E,inj__o(U)),inj__o(fo__c_2Ebool_2E_7E(U)))**. % 40.70/23.78 81[0:Inp] || del(U) -> mem(c_2Ebool_2E_3F(U),arr(arr(U,bool),bool))*. % 40.70/23.78 93[0:Inp] || p(U) p(ap(c_2Ebool_2E_7E,U))* mem(U,bool) -> . % 40.70/23.78 97[0:Inp] || p(ap(skc11,U))* mem(U,skc8) -> p(ap(skc10,U)). % 40.70/23.78 102[0:Inp] || mem(U,bool)*+ mem(V,bool)* -> p(U) p(V) equal(U,V)*. % 40.70/23.78 105[0:Inp] || mem(U,bool) mem(V,bool) -> p(U) p(ap(ap(c_2Emin_2E_3D_3D_3E,U),V))*. % 40.70/23.78 109(e)[0:Inp] || p(U) mem(V,bool) mem(U,bool) -> p(ap(ap(c_2Emin_2E_3D_3D_3E,V),U))*. % 40.70/23.78 112[0:Inp] || p(U) mem(V,bool) mem(U,bool) -> p(ap(ap(c_2Ebool_2E_5C_2F,V),U))*. % 40.70/23.78 114(e)[0:Inp] || p(U) p(V) mem(U,bool)*+ mem(V,bool)* -> equal(U,V)*. % 40.70/23.78 120[0:Inp] || tp__o(U) tp__o(V) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),inj__o(V)),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)))**. % 40.70/23.78 122[0:Inp] || tp__o(U) tp__o(V) -> equal(ap(ap(c_2Ebool_2E_5C_2F,inj__o(U)),inj__o(V)),inj__o(fo__c_2Ebool_2E_5C_2F(U,V)))**. % 40.70/23.78 123[0:Inp] || del(U) mem(V,arr(U,bool))+ -> p(ap(c_2Ebool_2E_21(U),V))* mem(skf15(V,U),U)*. % 40.70/23.78 131[0:Inp] || del(U) p(ap(c_2Ebool_2E_3F(U),V))*+ mem(V,arr(U,bool)) -> mem(skf14(V,U),U)*. % 40.70/23.78 133(e)[0:Inp] || p(U) p(ap(ap(c_2Emin_2E_3D_3D_3E,U),V))* mem(U,bool) mem(V,bool) -> p(V). % 40.70/23.78 135[0:Inp] || del(U) del(V) mem(W,U)* mem(X,arr(U,V))*+ -> mem(ap(X,W),V)*. % 40.70/23.78 136[0:Inp] || del(U) p(ap(c_2Ebool_2E_3F(U),V))*+ mem(V,arr(U,bool)) -> p(ap(V,skf14(V,W)))*. % 40.70/23.78 137[0:Inp] || del(U) p(ap(V,skf15(V,W)))*+ mem(V,arr(U,bool)) -> p(ap(c_2Ebool_2E_21(U),V))*. % 40.70/23.78 141[0:Inp] || del(U) p(ap(V,W))* mem(W,U)* mem(V,arr(U,bool))+ -> p(ap(c_2Ebool_2E_3F(U),V))*. % 40.70/23.78 142[0:Inp] || del(U) p(ap(c_2Ebool_2E_21(U),V))*+ mem(W,U)* mem(V,arr(U,bool)) -> p(ap(V,W))*. % 40.70/23.78 147[0:Inp] || del(U) del(V) mem(W,arr(U,V))*+ mem(X,arr(U,V))* -> equal(W,X)* mem(skf13(U,Y,Z),U)*. % 40.70/23.78 154[0:Inp] || del(U) del(V) mem(W,arr(U,V))+ mem(X,arr(V,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(U,V),W),X))* mem(skf21(U,Y,Z),U)*. % 40.70/23.78 156[0:Inp] || del(U) del(V) mem(W,arr(U,V))+ mem(X,arr(V,bool)) -> p(ap(X,skf17(X,Y)))* p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(U,V),W),X))*. % 40.70/23.78 157[0:Inp] || del(U) del(V) mem(W,arr(U,V))+ mem(X,arr(V,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(U,V),W),X))* mem(skf27(X,V,Y,Z),V)*. % 40.70/23.78 158[0:Inp] || del(U) del(V) mem(W,arr(U,V))+ mem(X,arr(V,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(U,V),W),X))* mem(skf24(X,V,Y,Z),V)*. % 40.70/23.78 164[0:Inp] || del(U) del(V) mem(W,arr(U,V))+ mem(X,arr(V,bool)) -> p(ap(X,ap(W,skf21(U,W,X))))* p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(U,V),W),X))*. % 40.70/23.78 169[0:Inp] || del(U) del(V) p(ap(W,ap(X,Y)))* p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(U,V),X),W))*+ mem(Y,U)* mem(X,arr(U,V)) mem(W,arr(V,bool)) -> . % 40.70/23.78 172[0:Inp] || del(U) del(V) p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(U,V),W),X))*+ mem(Y,V)* mem(W,arr(U,V)) mem(X,arr(V,bool)) -> p(ap(X,Y))* mem(skf25(U,Z,X1),U)*. % 40.70/23.78 174[0:Inp] || del(U) del(V) p(ap(W,X))* p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(U,V),Y),W))*+ mem(X,V)* mem(Y,arr(U,V)) mem(W,arr(V,bool)) -> mem(skf22(U,Z,X1),U)*. % 40.70/23.78 175[0:Inp] || del(U) del(V) p(ap(W,X))* p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(U,V),Y),W))*+ mem(X,V)* mem(Y,arr(U,V)) mem(W,arr(V,bool)) -> mem(skf16(U,Z,X1),U)*. % 40.70/23.78 176[0:Inp] || del(U) del(V) p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(U,V),W),X))*+ mem(Y,V)* mem(W,arr(U,V)) mem(X,arr(V,bool)) -> p(ap(X,Y))* equal(ap(W,skf25(U,W,Y)),Y)**. % 40.70/23.78 177[0:Inp] || del(U) del(V) p(ap(W,X))* p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(U,V),Y),W))*+ mem(X,V)* mem(Y,arr(U,V)) mem(W,arr(V,bool)) -> equal(ap(Y,skf22(U,Y,X)),X)**. % 40.70/23.78 179[0:Inp] || del(U) del(V) p(ap(W,X))* p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(U,V),Y),W))*+ mem(X,V)* mem(Y,arr(U,V)) mem(W,arr(V,bool)) -> p(ap(W,ap(Y,skf16(U,Y,W))))*. % 40.70/23.78 299[0:Res:28.0,137.0] || p(ap(U,skf15(U,V)))* mem(U,arr(skc8,bool)) -> p(ap(c_2Ebool_2E_21(skc8),U)). % 40.70/23.78 300[0:Res:28.0,136.0] || p(ap(c_2Ebool_2E_3F(skc8),U)) mem(U,arr(skc8,bool)) -> p(ap(U,skf14(U,V)))*. % 40.70/23.78 315[0:Res:28.0,81.0] || -> mem(c_2Ebool_2E_3F(skc8),arr(arr(skc8,bool),bool))*. % 40.70/23.78 352[0:Res:28.0,69.1] || del(U) -> del(arr(skc8,U))*. % 40.70/23.78 359[0:SpR:35.0,55.1] || tp__o(fo__c_2Ebool_2ET) -> equal(surj__o(c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 40.70/23.78 360[0:SpR:34.0,55.1] || tp__o(fo__c_2Ebool_2EF) -> equal(surj__o(c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 40.70/23.78 361[0:MRR:359.0,23.0] || -> equal(surj__o(c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 40.70/23.78 362[0:MRR:360.0,22.0] || -> equal(surj__o(c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 40.70/23.78 377[0:SpR:79.1,65.2] || tp__o(U) mem(inj__o(U),bool) -> p(inj__o(U)) p(inj__o(fo__c_2Ebool_2E_7E(U)))*. % 40.70/23.78 379[0:SpR:35.0,79.1] || tp__o(fo__c_2Ebool_2ET) -> equal(inj__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET)),ap(c_2Ebool_2E_7E,c_2Ebool_2ET))**. % 40.70/23.78 380[0:SpR:34.0,79.1] || tp__o(fo__c_2Ebool_2EF) -> equal(inj__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF)),ap(c_2Ebool_2E_7E,c_2Ebool_2EF))**. % 40.70/23.78 381[0:SpR:59.1,79.1] || mem(U,bool) tp__o(surj__o(U)) -> equal(inj__o(fo__c_2Ebool_2E_7E(surj__o(U))),ap(c_2Ebool_2E_7E,U))**. % 40.70/23.78 382[0:MRR:379.0,23.0] || -> equal(inj__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET)),ap(c_2Ebool_2E_7E,c_2Ebool_2ET))**. % 40.70/23.78 383[0:MRR:380.0,22.0] || -> equal(inj__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF)),ap(c_2Ebool_2E_7E,c_2Ebool_2EF))**. % 40.70/23.78 384[0:MRR:377.1,50.1] || tp__o(U) -> p(inj__o(U)) p(inj__o(fo__c_2Ebool_2E_7E(U)))*. % 40.70/23.78 385[0:MRR:381.1,33.0] || mem(U,bool) -> equal(inj__o(fo__c_2Ebool_2E_7E(surj__o(U))),ap(c_2Ebool_2E_7E,U))**. % 40.70/23.78 386[0:SpR:382.0,50.1] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET)) -> mem(ap(c_2Ebool_2E_7E,c_2Ebool_2ET),bool)*. % 40.70/23.78 387[0:SpR:382.0,55.1] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET)) -> equal(surj__o(ap(c_2Ebool_2E_7E,c_2Ebool_2ET)),fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET))**. % 40.70/23.78 395[0:SpR:383.0,384.2] || tp__o(fo__c_2Ebool_2EF) -> p(inj__o(fo__c_2Ebool_2EF)) p(ap(c_2Ebool_2E_7E,c_2Ebool_2EF))*. % 40.70/23.78 397[0:Rew:34.0,395.1] || tp__o(fo__c_2Ebool_2EF) -> p(c_2Ebool_2EF) p(ap(c_2Ebool_2E_7E,c_2Ebool_2EF))*. % 40.70/23.78 398(e)[0:MRR:397.0,397.1,22.0,30.0] || -> p(ap(c_2Ebool_2E_7E,c_2Ebool_2EF))*. % 40.70/23.78 416[0:SpL:79.1,93.1] || tp__o(U) p(inj__o(U)) p(inj__o(fo__c_2Ebool_2E_7E(U)))* mem(inj__o(U),bool) -> . % 40.70/23.78 419[0:MRR:416.3,50.1] || tp__o(U) p(inj__o(U)) p(inj__o(fo__c_2Ebool_2E_7E(U)))* -> . % 40.70/23.78 431[0:SpL:382.0,419.2] || tp__o(fo__c_2Ebool_2ET) p(inj__o(fo__c_2Ebool_2ET)) p(ap(c_2Ebool_2E_7E,c_2Ebool_2ET))* -> . % 40.70/23.78 435[0:Rew:35.0,431.1] || tp__o(fo__c_2Ebool_2ET) p(c_2Ebool_2ET) p(ap(c_2Ebool_2E_7E,c_2Ebool_2ET))* -> . % 40.70/23.78 436[0:MRR:435.0,435.1,23.0,21.0] || p(ap(c_2Ebool_2E_7E,c_2Ebool_2ET))* -> . % 40.70/23.78 487[0:Res:31.0,102.0] || mem(U,bool)* -> p(c_2Ebool_2EF) p(U) equal(c_2Ebool_2EF,U). % 40.70/23.78 492(e)[0:MRR:487.1,30.0] || mem(U,bool)* -> p(U) equal(c_2Ebool_2EF,U). % 40.70/23.78 499[0:Res:50.1,492.0] || tp__o(U) -> p(inj__o(U))* equal(inj__o(U),c_2Ebool_2EF). % 40.70/23.78 500[0:Res:386.1,492.0] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET)) -> p(ap(c_2Ebool_2E_7E,c_2Ebool_2ET))* equal(ap(c_2Ebool_2E_7E,c_2Ebool_2ET),c_2Ebool_2EF). % 40.70/23.78 504[0:MRR:500.1,436.0] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET)) -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2ET),c_2Ebool_2EF)**. % 40.70/23.78 506[0:Rew:504.1,387.1] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET))* -> equal(surj__o(c_2Ebool_2EF),fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET)). % 40.70/23.78 509[0:Rew:362.0,506.1] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET))* -> equal(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET),fo__c_2Ebool_2EF). % 40.70/23.78 514[0:Res:42.1,509.0] || tp__o(fo__c_2Ebool_2ET) -> equal(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET),fo__c_2Ebool_2EF)**. % 40.70/23.78 515[0:MRR:514.0,23.0] || -> equal(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2ET),fo__c_2Ebool_2EF)**. % 40.70/23.78 516[0:Rew:515.0,382.0] || -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2ET),inj__o(fo__c_2Ebool_2EF))**. % 40.70/23.78 518[0:Rew:34.0,516.0] || -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2ET),c_2Ebool_2EF)**. % 40.70/23.78 535[0:Res:499.1,419.2] || tp__o(fo__c_2Ebool_2E_7E(U)) tp__o(U) p(inj__o(U)) -> equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2EF)**. % 40.70/23.78 541[0:MRR:535.0,42.1] || tp__o(U) p(inj__o(U)) -> equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2EF)**. % 40.70/23.78 572[0:SpR:541.2,55.1] || tp__o(U) p(inj__o(U))* tp__o(fo__c_2Ebool_2E_7E(U)) -> equal(surj__o(c_2Ebool_2EF),fo__c_2Ebool_2E_7E(U)). % 40.70/23.78 577[0:SpR:541.2,385.1] || tp__o(surj__o(U)) p(inj__o(surj__o(U)))* mem(U,bool) -> equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2EF). % 40.70/23.78 581[0:Rew:362.0,572.3] || tp__o(U) p(inj__o(U))* tp__o(fo__c_2Ebool_2E_7E(U)) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF). % 40.70/23.78 582[0:MRR:581.2,42.1] || tp__o(U) p(inj__o(U))* -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF). % 40.70/23.78 586[0:Rew:59.1,577.1] || tp__o(surj__o(U)) p(U) mem(U,bool) -> equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2EF)**. % 40.70/23.78 587(e)[0:MRR:586.0,33.0] || p(U) mem(U,bool) -> equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2EF)**. % 40.70/23.78 592[0:SpL:59.1,582.1] || mem(U,bool) tp__o(surj__o(U)) p(U) -> equal(fo__c_2Ebool_2E_7E(surj__o(U)),fo__c_2Ebool_2EF)**. % 40.70/23.78 595[0:Res:499.1,582.1] || tp__o(U) tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF). % 40.70/23.78 597(e)[0:Obv:595.0] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF). % 40.70/23.78 600[0:MRR:592.1,33.0] || mem(U,bool) p(U) -> equal(fo__c_2Ebool_2E_7E(surj__o(U)),fo__c_2Ebool_2EF)**. % 40.70/23.78 605[0:SpR:597.1,55.1] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)** equal(surj__o(c_2Ebool_2EF),U)*. % 40.70/23.78 606[0:SpR:597.1,79.1] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF) equal(inj__o(fo__c_2Ebool_2E_7E(U)),ap(c_2Ebool_2E_7E,c_2Ebool_2EF))**. % 40.70/23.78 608[0:SpR:597.1,59.1] || tp__o(surj__o(U)) mem(U,bool) -> equal(fo__c_2Ebool_2E_7E(surj__o(U)),fo__c_2Ebool_2EF)** equal(c_2Ebool_2EF,U). % 40.70/23.78 613[0:Obv:605.0] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)** equal(surj__o(c_2Ebool_2EF),U)*. % 40.70/23.78 614(e)[0:Rew:362.0,613.2] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)** equal(fo__c_2Ebool_2EF,U). % 40.70/23.78 616[0:MRR:608.0,33.0] || mem(U,bool) -> equal(fo__c_2Ebool_2E_7E(surj__o(U)),fo__c_2Ebool_2EF)** equal(c_2Ebool_2EF,U). % 40.70/23.78 617[0:Obv:606.0] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF) equal(inj__o(fo__c_2Ebool_2E_7E(U)),ap(c_2Ebool_2E_7E,c_2Ebool_2EF))**. % 40.70/23.78 620[0:SpR:614.1,384.2] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2EF,U) p(inj__o(U))* p(inj__o(fo__c_2Ebool_2EF))*. % 40.70/23.78 628[0:Obv:620.0] || tp__o(U) -> equal(fo__c_2Ebool_2EF,U) p(inj__o(U))* p(inj__o(fo__c_2Ebool_2EF))*. % 40.70/23.78 629[0:Rew:34.0,628.3] || tp__o(U) -> equal(fo__c_2Ebool_2EF,U) p(inj__o(U))* p(c_2Ebool_2EF). % 40.70/23.78 630[0:MRR:629.3,30.0] || tp__o(U) -> equal(fo__c_2Ebool_2EF,U) p(inj__o(U))*. % 40.70/23.78 642[0:SpR:59.1,630.2] || mem(U,bool)* tp__o(surj__o(U)) -> equal(surj__o(U),fo__c_2Ebool_2EF) p(U). % 40.70/23.78 645(e)[0:MRR:642.1,33.0] || mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2EF) p(U). % 40.70/23.78 669[0:SpR:587.2,79.1] || p(inj__o(U)) mem(inj__o(U),bool)* tp__o(U) -> equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2EF). % 40.70/23.78 676[0:MRR:669.1,50.1] || p(inj__o(U)) tp__o(U) -> equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2EF)**. % 40.70/23.78 697[0:SpR:616.1,385.1] || mem(U,bool) mem(U,bool) -> equal(c_2Ebool_2EF,U) equal(ap(c_2Ebool_2E_7E,U),inj__o(fo__c_2Ebool_2EF))**. % 40.70/23.78 704[0:Obv:697.0] || mem(U,bool) -> equal(c_2Ebool_2EF,U) equal(ap(c_2Ebool_2E_7E,U),inj__o(fo__c_2Ebool_2EF))**. % 40.70/23.78 705(e)[0:Rew:34.0,704.2] || mem(U,bool) -> equal(c_2Ebool_2EF,U) equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2EF)**. % 40.70/23.78 712[0:SpR:676.2,79.1] || p(inj__o(U)) tp__o(U) tp__o(fo__c_2Ebool_2E_7E(U)) -> equal(inj__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2E_7E(U))),ap(c_2Ebool_2E_7E,c_2Ebool_2EF))**. % 40.70/23.78 731[0:MRR:712.2,42.1] || p(inj__o(U)) tp__o(U) -> equal(inj__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2E_7E(U))),ap(c_2Ebool_2E_7E,c_2Ebool_2EF))**. % 40.70/23.78 922(e)[0:SpR:731.2,597.1] || p(inj__o(U)) tp__o(U) tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2E_7E(U))) -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2EF) equal(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2E_7E(U))),fo__c_2Ebool_2EF)**. % 40.70/23.78 951(e)[1:Spt:922.3] || -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 953[1:Rew:951.0,398.0] || -> p(c_2Ebool_2EF)*. % 40.70/23.78 965(e)[1:MRR:953.0,30.0] || -> . % 40.70/23.78 998(e)[1:Spt:965.0,922.3,951.0] || equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2EF)** -> . % 40.70/23.78 999(e)[1:Spt:965.0,922.0,922.1,922.2,922.4] || p(inj__o(U)) tp__o(U) tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2E_7E(U))) -> equal(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2E_7E(U))),fo__c_2Ebool_2EF)**. % 40.70/23.78 1254[0:Res:32.0,114.2] || p(c_2Ebool_2ET) p(U) mem(U,bool)* -> equal(c_2Ebool_2ET,U). % 40.70/23.78 1259[0:MRR:1254.0,21.0] || p(U) mem(U,bool)* -> equal(c_2Ebool_2ET,U). % 40.70/23.78 1263[0:Res:50.1,1259.1] || tp__o(U) p(inj__o(U))* -> equal(inj__o(U),c_2Ebool_2ET). % 40.70/23.78 1384[0:Res:499.1,1263.1] || tp__o(U) tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF) equal(inj__o(U),c_2Ebool_2ET)**. % 40.70/23.78 1385[0:Res:630.2,1263.1] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2EF,U) equal(inj__o(U),c_2Ebool_2ET)**. % 40.70/23.78 1386[0:Res:384.2,1263.1] || tp__o(U) tp__o(fo__c_2Ebool_2E_7E(U)) -> p(inj__o(U)) equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2ET)**. % 40.70/23.78 1387[0:Obv:1385.0] || tp__o(U) -> equal(fo__c_2Ebool_2EF,U) equal(inj__o(U),c_2Ebool_2ET)**. % 40.70/23.78 1389[0:Obv:1384.0] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF) equal(inj__o(U),c_2Ebool_2ET)**. % 40.70/23.78 1392[0:MRR:1386.1,42.1] || tp__o(U) -> p(inj__o(U)) equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2ET)**. % 40.70/23.78 1400[0:SpR:1387.2,55.1] || tp__o(U)* tp__o(U)* -> equal(fo__c_2Ebool_2EF,U) equal(surj__o(c_2Ebool_2ET),U)*. % 40.70/23.78 1404[0:SpR:1387.2,59.1] || tp__o(surj__o(U)) mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2EF) equal(c_2Ebool_2ET,U). % 40.70/23.78 1408[0:Obv:1400.0] || tp__o(U)* -> equal(fo__c_2Ebool_2EF,U) equal(surj__o(c_2Ebool_2ET),U)*. % 40.70/23.78 1409[0:Rew:361.0,1408.2] || tp__o(U)* -> equal(fo__c_2Ebool_2EF,U) equal(fo__c_2Ebool_2ET,U). % 40.70/23.78 1410[0:MRR:1404.0,33.0] || mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2EF) equal(c_2Ebool_2ET,U). % 40.70/23.78 1418[0:Res:33.0,1409.0] || -> equal(surj__o(U),fo__c_2Ebool_2EF) equal(surj__o(U),fo__c_2Ebool_2ET)**. % 40.70/23.78 1419(e)[0:Res:42.1,1409.0] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF) equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET)**. % 40.70/23.78 1420[0:Res:68.2,1409.0] || tp__o(U) tp__o(V) -> equal(fo__c_2Ebool_2E_5C_2F(U,V),fo__c_2Ebool_2EF) equal(fo__c_2Ebool_2E_5C_2F(U,V),fo__c_2Ebool_2ET)**. % 40.70/23.78 1422[0:Res:66.2,1409.0] || tp__o(U) tp__o(V) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,V),fo__c_2Ebool_2EF) equal(fo__c_2Emin_2E_3D_3D_3E(U,V),fo__c_2Ebool_2ET)**. % 40.70/23.78 1432[0:EqF:1418.1,1418.0] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF) -> equal(surj__o(U),fo__c_2Ebool_2EF)**. % 40.70/23.78 1467[0:SpR:1389.2,55.1] || tp__o(U) tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(surj__o(c_2Ebool_2ET),U). % 40.70/23.78 1472[0:SpR:1389.2,59.1] || tp__o(surj__o(U)) mem(U,bool) -> equal(inj__o(surj__o(U)),c_2Ebool_2EF)** equal(c_2Ebool_2ET,U). % 40.70/23.78 1476[0:Obv:1467.0] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(surj__o(c_2Ebool_2ET),U). % 40.70/23.78 1477[0:Rew:361.0,1476.2] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(fo__c_2Ebool_2ET,U). % 40.70/23.78 1478[0:Rew:59.1,1472.2] || tp__o(surj__o(U)) mem(U,bool)* -> equal(U,c_2Ebool_2EF) equal(c_2Ebool_2ET,U). % 40.70/23.78 1479[0:Rew:1410.1,1478.0] || tp__o(fo__c_2Ebool_2EF) mem(U,bool)* -> equal(U,c_2Ebool_2EF) equal(c_2Ebool_2ET,U). % 40.70/23.78 1480[0:MRR:1479.0,22.0] || mem(U,bool)* -> equal(U,c_2Ebool_2EF) equal(c_2Ebool_2ET,U). % 40.70/23.78 1512[0:SpR:122.2,112.3] || tp__o(U) tp__o(V) p(inj__o(V)) mem(inj__o(U),bool) mem(inj__o(V),bool) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(U,V)))*. % 40.70/23.78 1515[0:SpR:35.0,122.2] || tp__o(U) tp__o(fo__c_2Ebool_2ET) -> equal(ap(ap(c_2Ebool_2E_5C_2F,inj__o(U)),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2E_5C_2F(U,fo__c_2Ebool_2ET)))**. % 40.70/23.78 1525[0:SpR:34.0,122.2] || tp__o(fo__c_2Ebool_2EF) tp__o(U) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),inj__o(U)),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)))**. % 40.70/23.78 1533[0:MRR:1515.1,23.0] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_5C_2F,inj__o(U)),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2E_5C_2F(U,fo__c_2Ebool_2ET)))**. % 40.70/23.78 1536[0:MRR:1525.0,22.0] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),inj__o(U)),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)))**. % 40.70/23.78 1556[0:MRR:1512.3,1512.4,50.1,50.1] || tp__o(U) tp__o(V) p(inj__o(V)) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(U,V)))*. % 40.70/23.78 1566[0:SpR:1392.2,55.1] || tp__o(U) tp__o(fo__c_2Ebool_2E_7E(U)) -> p(inj__o(U))* equal(surj__o(c_2Ebool_2ET),fo__c_2Ebool_2E_7E(U)). % 40.70/23.78 1574[0:SpR:1392.2,385.1] || tp__o(surj__o(U)) mem(U,bool) -> p(inj__o(surj__o(U)))* equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2ET). % 40.70/23.78 1584[0:Rew:361.0,1566.3] || tp__o(U) tp__o(fo__c_2Ebool_2E_7E(U)) -> p(inj__o(U))* equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET). % 40.70/23.78 1591[0:Rew:59.1,1574.2] || tp__o(surj__o(U)) mem(U,bool) -> p(U) equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2ET)**. % 40.70/23.78 1592[0:Rew:645.1,1591.0] || tp__o(fo__c_2Ebool_2EF) mem(U,bool) -> p(U) equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2ET)**. % 40.70/23.78 1593[0:MRR:1592.0,22.0] || mem(U,bool) -> p(U) equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2ET)**. % 40.70/23.78 1726[0:SpR:120.2,105.3] || tp__o(U) tp__o(V) mem(inj__o(U),bool) mem(inj__o(V),bool) -> p(inj__o(U)) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)))*. % 40.70/23.78 1728[0:SpR:35.0,120.2] || tp__o(U) tp__o(fo__c_2Ebool_2ET) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2ET),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET)))**. % 40.70/23.78 1729[0:SpR:34.0,120.2] || tp__o(U) tp__o(fo__c_2Ebool_2EF) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)))**. % 40.70/23.78 1734[0:SpR:59.1,120.2] || mem(U,bool) tp__o(V) tp__o(surj__o(U)) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(V)),U),inj__o(fo__c_2Emin_2E_3D_3D_3E(V,surj__o(U))))**. % 40.70/23.78 1737[0:SpR:35.0,120.2] || tp__o(fo__c_2Ebool_2ET) tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),inj__o(U)),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U)))**. % 40.70/23.78 1743[0:SpR:59.1,120.2] || mem(U,bool) tp__o(surj__o(U)) tp__o(V) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),inj__o(V)),inj__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),V)))**. % 40.70/23.78 1746[0:MRR:1728.1,23.0] || tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2ET),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET)))**. % 40.70/23.78 1747[0:MRR:1729.1,22.0] || tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)))**. % 40.70/23.78 1748[0:MRR:1737.0,23.0] || tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),inj__o(U)),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U)))**. % 40.70/23.78 1750[0:MRR:1743.1,33.0] || mem(U,bool) tp__o(V) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),inj__o(V)),inj__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),V)))**. % 40.70/23.78 1755[0:MRR:1734.2,33.0] || mem(U,bool) tp__o(V) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(V)),U),inj__o(fo__c_2Emin_2E_3D_3D_3E(V,surj__o(U))))**. % 40.70/23.78 1768[0:MRR:1726.2,1726.3,50.1,50.1] || tp__o(U) tp__o(V) -> p(inj__o(U)) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)))*. % 40.70/23.78 1870[0:SpR:34.0,1533.1] || tp__o(fo__c_2Ebool_2EF) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET)))**. % 40.70/23.78 1880[0:MRR:1870.0,22.0] || -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET)))**. % 40.70/23.78 1914[0:SpR:1880.0,112.3] || p(c_2Ebool_2ET) mem(c_2Ebool_2EF,bool) mem(c_2Ebool_2ET,bool) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET)))*. % 40.70/23.78 1916[0:MRR:1914.0,1914.1,1914.2,21.0,31.0,32.0] || -> p(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET)))*. % 40.70/23.78 1919[0:SpR:1477.1,1916.0] || tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET))* -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET) p(c_2Ebool_2EF). % 40.70/23.78 1921[0:MRR:1919.2,30.0] || tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET))* -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET). % 40.70/23.78 1942[0:Res:68.2,1921.0] || tp__o(fo__c_2Ebool_2EF) tp__o(fo__c_2Ebool_2ET) -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 40.70/23.78 1943[0:MRR:1942.0,1942.1,22.0,23.0] || -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 40.70/23.78 2791[0:Res:38.0,123.1] || del(skc8) -> p(ap(c_2Ebool_2E_21(skc8),skc10))* mem(skf15(skc10,skc8),skc8). % 40.70/23.78 2792[0:Res:37.0,123.1] || del(skc8) -> p(ap(c_2Ebool_2E_21(skc8),skc11))* mem(skf15(skc11,skc8),skc8). % 40.70/23.78 2793[0:Res:36.0,123.1] || del(bool) -> p(ap(c_2Ebool_2E_21(bool),c_2Ebool_2E_7E))* mem(skf15(c_2Ebool_2E_7E,bool),bool). % 40.70/23.78 2800[0:MRR:2791.0,28.0] || -> p(ap(c_2Ebool_2E_21(skc8),skc10))* mem(skf15(skc10,skc8),skc8). % 40.70/23.78 2801[0:MRR:2792.0,28.0] || -> p(ap(c_2Ebool_2E_21(skc8),skc11))* mem(skf15(skc11,skc8),skc8). % 40.70/23.78 2802(e)[0:MRR:2793.0,26.0] || -> p(ap(c_2Ebool_2E_21(bool),c_2Ebool_2E_7E))* mem(skf15(c_2Ebool_2E_7E,bool),bool). % 40.70/23.78 2805[2:Spt:2802.0] || -> p(ap(c_2Ebool_2E_21(bool),c_2Ebool_2E_7E))*. % 40.70/23.78 2864[0:SpR:59.1,1536.1] || mem(U,bool) tp__o(surj__o(U)) -> equal(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,surj__o(U))),ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U))**. % 40.70/23.78 2881[0:MRR:2864.1,33.0] || mem(U,bool) -> equal(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,surj__o(U))),ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U))**. % 40.70/23.78 3680[0:Res:39.0,135.3] || del(skc7) del(skc8) mem(U,skc7) -> mem(ap(skc9,U),skc8)*. % 40.70/23.78 3681[0:Res:38.0,135.3] || del(skc8) del(bool) mem(U,skc8) -> mem(ap(skc10,U),bool)*. % 40.70/23.78 3682[0:Res:37.0,135.3] || del(skc8) del(bool) mem(U,skc8) -> mem(ap(skc11,U),bool)*. % 40.70/23.78 3683[0:Res:36.0,135.3] || del(bool) del(bool) mem(U,bool) -> mem(ap(c_2Ebool_2E_7E,U),bool)*. % 40.70/23.78 3687[0:Res:315.0,135.3] || del(arr(skc8,bool)) del(bool) mem(U,arr(skc8,bool)) -> mem(ap(c_2Ebool_2E_3F(skc8),U),bool)*. % 40.70/23.78 3702(e)[0:MRR:3680.0,3680.1,29.0,28.0] || mem(U,skc7) -> mem(ap(skc9,U),skc8)*. % 40.70/23.78 3703[0:MRR:3681.0,3681.1,28.0,26.0] || mem(U,skc8) -> mem(ap(skc10,U),bool)*. % 40.70/23.78 3704[0:MRR:3682.0,3682.1,28.0,26.0] || mem(U,skc8) -> mem(ap(skc11,U),bool)*. % 40.70/23.78 3705[0:Obv:3683.0] || del(bool) mem(U,bool) -> mem(ap(c_2Ebool_2E_7E,U),bool)*. % 40.70/23.78 3706[0:MRR:3705.0,26.0] || mem(U,bool) -> mem(ap(c_2Ebool_2E_7E,U),bool)*. % 40.70/23.78 3712[0:MRR:3687.0,3687.1,352.1,26.0] || mem(U,arr(skc8,bool)) -> mem(ap(c_2Ebool_2E_3F(skc8),U),bool)*. % 40.70/23.78 3736[0:Res:3703.1,1480.0] || mem(U,skc8) -> equal(ap(skc10,U),c_2Ebool_2EF) equal(ap(skc10,U),c_2Ebool_2ET)**. % 40.70/23.78 3753[0:Res:3704.1,1480.0] || mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF) equal(ap(skc11,U),c_2Ebool_2ET)**. % 40.70/23.78 3772[0:SpR:79.1,3706.1] || tp__o(U) mem(inj__o(U),bool) -> mem(inj__o(fo__c_2Ebool_2E_7E(U)),bool)*. % 40.70/23.78 3787[0:MRR:3772.1,50.1] || tp__o(U) -> mem(inj__o(fo__c_2Ebool_2E_7E(U)),bool)*. % 40.70/23.78 3867[0:Res:3712.1,1480.0] || mem(U,arr(skc8,bool))* -> equal(ap(c_2Ebool_2E_3F(skc8),U),c_2Ebool_2EF) equal(ap(c_2Ebool_2E_3F(skc8),U),c_2Ebool_2ET). % 40.70/23.78 3913[0:Res:38.0,141.3] || del(skc8) p(ap(skc10,U))* mem(U,skc8) -> p(ap(c_2Ebool_2E_3F(skc8),skc10))*. % 40.70/23.78 3914[0:Res:37.0,141.3] || del(skc8) p(ap(skc11,U))* mem(U,skc8) -> p(ap(c_2Ebool_2E_3F(skc8),skc11))*. % 40.70/23.78 3922[0:MRR:3913.0,28.0] || p(ap(skc10,U))*+ mem(U,skc8) -> p(ap(c_2Ebool_2E_3F(skc8),skc10))*. % 40.70/23.78 3923[0:MRR:3914.0,28.0] || p(ap(skc11,U))*+ mem(U,skc8) -> p(ap(c_2Ebool_2E_3F(skc8),skc11))*. % 40.70/23.78 4069[2:Res:2805.0,142.1] || del(bool) mem(U,bool) mem(c_2Ebool_2E_7E,arr(bool,bool))* -> p(ap(c_2Ebool_2E_7E,U))*. % 40.70/23.78 4078[2:MRR:4069.0,4069.2,26.0,36.0] || mem(U,bool) -> p(ap(c_2Ebool_2E_7E,U))*. % 40.70/23.78 4112[2:SpR:518.0,4078.1] || mem(c_2Ebool_2ET,bool)* -> p(c_2Ebool_2EF). % 40.70/23.78 4116(e)[2:MRR:4112.0,4112.1,32.0,30.0] || -> . % 40.70/23.78 4225[2:Spt:4116.0,2802.0,2805.0] || p(ap(c_2Ebool_2E_21(bool),c_2Ebool_2E_7E))* -> . % 40.70/23.78 4226[2:Spt:4116.0,2802.1] || -> mem(skf15(c_2Ebool_2E_7E,bool),bool)*. % 40.70/23.78 4232[0:Rew:1419.2,617.2] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)** equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),inj__o(fo__c_2Ebool_2ET))**. % 40.70/23.78 4233(e)[0:Rew:35.0,4232.2] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)** equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2ET)**. % 40.70/23.78 4241[0:Rew:1419.1,1584.1] || tp__o(U) tp__o(fo__c_2Ebool_2EF) -> p(inj__o(U))* equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET). % 40.70/23.78 4242[0:MRR:4241.1,22.0] || tp__o(U) -> p(inj__o(U))* equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET). % 40.70/23.78 4306[3:Spt:4233.2] || -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2ET)**. % 40.70/23.78 4308[3:Rew:4306.0,998.0] || equal(c_2Ebool_2ET,c_2Ebool_2EF)** -> . % 40.70/23.78 4412[0:SpR:1432.1,59.1] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF) mem(U,bool)* -> equal(inj__o(fo__c_2Ebool_2EF),U). % 40.70/23.78 4416(e)[0:Rew:34.0,4412.2] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF) mem(U,bool)* -> equal(c_2Ebool_2EF,U). % 40.70/23.78 4426(e)[2:Res:4226.0,492.0] || -> p(skf15(c_2Ebool_2E_7E,bool))* equal(skf15(c_2Ebool_2E_7E,bool),c_2Ebool_2EF). % 40.70/23.78 4443[4:Spt:4426.1] || -> equal(skf15(c_2Ebool_2E_7E,bool),c_2Ebool_2EF)**. % 40.70/23.78 4448[4:SpL:4443.0,137.1] || del(U) p(ap(c_2Ebool_2E_7E,c_2Ebool_2EF)) mem(c_2Ebool_2E_7E,arr(U,bool)) -> p(ap(c_2Ebool_2E_21(U),c_2Ebool_2E_7E))*. % 40.70/23.78 4449[4:Rew:4306.0,4448.1] || del(U) p(c_2Ebool_2ET) mem(c_2Ebool_2E_7E,arr(U,bool)) -> p(ap(c_2Ebool_2E_21(U),c_2Ebool_2E_7E))*. % 40.70/23.78 4450[4:MRR:4449.1,21.0] || del(U) mem(c_2Ebool_2E_7E,arr(U,bool)) -> p(ap(c_2Ebool_2E_21(U),c_2Ebool_2E_7E))*. % 40.70/23.78 4463[0:Res:50.1,102.0] || tp__o(U) mem(V,bool)*+ -> p(inj__o(U))* p(V) equal(inj__o(U),V)*. % 40.70/23.78 4542[0:SpR:34.0,4242.1] || tp__o(fo__c_2Ebool_2EF) -> p(c_2Ebool_2EF) equal(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF),fo__c_2Ebool_2ET)**. % 40.70/23.78 4545[0:SpR:1477.1,4242.1] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2ET,U) p(c_2Ebool_2EF) equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET)**. % 40.70/23.78 4565[0:Obv:4545.0] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) p(c_2Ebool_2EF) equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET)**. % 40.70/23.78 4566[0:MRR:4565.2,30.0] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET)**. % 40.70/23.78 4761[0:Res:32.0,4416.1] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)** -> equal(c_2Ebool_2ET,c_2Ebool_2EF). % 40.70/23.78 4772[3:MRR:4761.1,4308.0] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)** -> . % 40.70/23.78 4929(e)[0:SpR:600.2,4566.2] || mem(U,bool)* p(U) tp__o(surj__o(U)) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF). % 40.70/23.78 4937(e)[0:Rew:1418.0,4929.2] || mem(U,bool)* p(U) tp__o(fo__c_2Ebool_2EF) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF). % 40.70/23.78 4938(e)[3:MRR:4937.2,4937.4,22.0,4772.0] || mem(U,bool)* p(U) -> equal(surj__o(U),fo__c_2Ebool_2ET). % 40.70/23.78 4944(e)[3:Res:3787.1,4938.0] || tp__o(U) p(inj__o(fo__c_2Ebool_2E_7E(U))) -> equal(surj__o(inj__o(fo__c_2Ebool_2E_7E(U))),fo__c_2Ebool_2ET)**. % 40.70/23.78 4945(e)[3:Res:3703.1,4938.0] || mem(U,skc8) p(ap(skc10,U)) -> equal(surj__o(ap(skc10,U)),fo__c_2Ebool_2ET)**. % 40.70/23.78 6133[0:Res:36.0,147.2] || del(bool) del(bool) mem(U,arr(bool,bool))* -> equal(c_2Ebool_2E_7E,U) mem(skf13(bool,V,W),bool)*. % 40.70/23.78 6152[0:Obv:6133.0] || del(bool) mem(U,arr(bool,bool))* -> equal(c_2Ebool_2E_7E,U) mem(skf13(bool,V,W),bool)*. % 40.70/23.78 6153(e)[0:MRR:6152.0,26.0] || mem(U,arr(bool,bool))* -> equal(c_2Ebool_2E_7E,U) mem(skf13(bool,V,W),bool)*. % 40.70/23.78 6325[0:SpR:1746.1,109.3] || tp__o(U) p(c_2Ebool_2ET) mem(inj__o(U),bool) mem(c_2Ebool_2ET,bool) -> p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET)))*. % 40.70/23.78 6370[0:MRR:6325.1,6325.2,6325.3,21.0,50.1,32.0] || tp__o(U) -> p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET)))*. % 40.70/23.78 6396[0:SpR:1477.1,6370.1] || tp__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET))* tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET) p(c_2Ebool_2EF). % 40.70/23.78 6398[0:MRR:6396.3,30.0] || tp__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET))* tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET). % 40.70/23.78 6598[0:Res:66.2,6398.0] || tp__o(U) tp__o(fo__c_2Ebool_2ET) tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 40.70/23.78 6600[0:Obv:6598.0] || tp__o(fo__c_2Ebool_2ET) tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 40.70/23.78 6601[0:MRR:6600.0,23.0] || tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 40.70/23.78 6602[0:Rew:6601.1,1746.1] || tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2ET))**. % 40.70/23.78 6612[0:Rew:35.0,6602.1] || tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2ET),c_2Ebool_2ET)**. % 40.70/23.78 6697[0:SpR:59.1,6612.1] || mem(U,bool) tp__o(surj__o(U)) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2ET),c_2Ebool_2ET)**. % 40.70/23.78 6699[0:MRR:6697.1,33.0] || mem(U,bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2ET),c_2Ebool_2ET)**. % 40.70/23.78 6828[0:SpR:35.0,1747.1] || tp__o(fo__c_2Ebool_2ET) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))**. % 40.70/23.78 6829[0:SpR:34.0,1747.1] || tp__o(fo__c_2Ebool_2EF) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2EF),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))**. % 40.70/23.78 6832[0:SpR:1477.1,1747.1] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2EF),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)))*. % 40.70/23.78 6835[0:SpR:676.2,1747.1] || p(inj__o(U)) tp__o(U) tp__o(fo__c_2Ebool_2E_7E(U)) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)),ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2EF),c_2Ebool_2EF))**. % 40.70/23.78 6858[0:SpR:59.1,1747.1] || mem(U,bool) tp__o(surj__o(U)) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF)),ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF))**. % 40.70/23.78 6860[0:MRR:6828.0,23.0] || -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))**. % 40.70/23.78 6861[0:MRR:6829.0,22.0] || -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2EF),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))**. % 40.70/23.78 6864[0:Obv:6832.0] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2EF),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)))*. % 40.70/23.78 6865[0:Rew:6861.0,6864.2] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)))*. % 40.70/23.78 6866[0:MRR:6858.1,33.0] || mem(U,bool) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF)),ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF))**. % 40.70/23.78 6872[0:Rew:6861.0,6835.3] || p(inj__o(U)) tp__o(U) tp__o(fo__c_2Ebool_2E_7E(U)) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))**. % 40.70/23.78 6873[0:MRR:6872.2,42.1] || p(inj__o(U)) tp__o(U) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))**. % 40.70/23.78 6900[0:SpL:6860.0,133.1] || p(c_2Ebool_2ET) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))* mem(c_2Ebool_2ET,bool) mem(c_2Ebool_2EF,bool) -> p(c_2Ebool_2EF). % 40.70/23.78 6901[0:MRR:6900.0,6900.2,6900.3,6900.4,21.0,32.0,31.0,30.0] || p(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))* -> . % 40.70/23.78 6903[0:SpL:1387.2,6901.0] || tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF))* p(c_2Ebool_2ET) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF). % 40.70/23.78 6907[0:MRR:6903.1,21.0] || tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF))* -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF). % 40.70/23.78 6912[0:SpR:6861.0,105.3] || mem(c_2Ebool_2EF,bool) mem(c_2Ebool_2EF,bool) -> p(c_2Ebool_2EF) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))*. % 40.70/23.78 6914[0:Obv:6912.0] || mem(c_2Ebool_2EF,bool) -> p(c_2Ebool_2EF) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))*. % 40.70/23.78 6915[0:MRR:6914.0,6914.1,31.0,30.0] || -> p(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))*. % 40.70/23.78 6917[0:Res:39.0,156.2] || del(skc7) del(skc8) mem(U,arr(skc8,bool)) -> p(ap(U,skf17(U,V)))* p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(skc7,skc8),skc9),U))*. % 40.70/23.78 6943[0:MRR:6917.0,6917.1,29.0,28.0] || mem(U,arr(skc8,bool))+ -> p(ap(U,skf17(U,V)))* p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(skc7,skc8),skc9),U))*. % 40.70/23.78 6964[0:SpR:1477.1,6915.0] || tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF))* -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2ET) p(c_2Ebool_2EF). % 40.70/23.78 6966[0:MRR:6964.2,30.0] || tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF))* -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2ET). % 40.70/23.78 6968[0:Res:66.2,6907.0] || tp__o(fo__c_2Ebool_2ET) tp__o(fo__c_2Ebool_2EF) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 40.70/23.78 6969[0:MRR:6968.0,6968.1,23.0,22.0] || -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 40.70/23.78 6970[0:Rew:6969.0,6860.0] || -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2EF))**. % 40.70/23.78 6975[0:Rew:34.0,6970.0] || -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 6984[0:Res:39.0,154.2] || del(skc7) del(skc8) mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U))* mem(skf21(skc7,V,W),skc7)*. % 40.70/23.78 7010(e)[0:MRR:6984.0,6984.1,29.0,28.0] || mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U))* mem(skf21(skc7,V,W),skc7)*. % 40.70/23.78 7029[0:Res:66.2,6966.0] || tp__o(fo__c_2Ebool_2EF) tp__o(fo__c_2Ebool_2EF) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2ET)**. % 40.70/23.78 7030[0:Obv:7029.0] || tp__o(fo__c_2Ebool_2EF) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2ET)**. % 40.70/23.78 7031[0:MRR:7030.0,22.0] || -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2ET)**. % 40.70/23.78 7035[0:Rew:7031.0,6865.2] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)),inj__o(fo__c_2Ebool_2ET))**. % 40.70/23.78 7036[0:Rew:7031.0,6873.2] || p(inj__o(U)) tp__o(U) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)),inj__o(fo__c_2Ebool_2ET))**. % 40.70/23.78 7039[0:Rew:35.0,7035.2] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)),c_2Ebool_2ET)**. % 40.70/23.78 7041[0:Rew:35.0,7036.2] || p(inj__o(U)) tp__o(U) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)),c_2Ebool_2ET)**. % 40.70/23.78 7425[0:SpR:1477.1,1748.1] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U)))*. % 40.70/23.78 7455[0:SpR:59.1,1748.1] || mem(U,bool) tp__o(surj__o(U)) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,surj__o(U))),ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),U))**. % 40.70/23.78 7456[0:SpL:1748.1,133.1] || tp__o(U) p(c_2Ebool_2ET) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U)))* mem(c_2Ebool_2ET,bool) mem(inj__o(U),bool) -> p(inj__o(U)). % 40.70/23.78 7461[0:Obv:7425.0] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U)))*. % 40.70/23.78 7462[0:Rew:6975.0,7461.2] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U)),c_2Ebool_2EF)**. % 40.70/23.78 7463[0:MRR:7455.1,33.0] || mem(U,bool) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,surj__o(U))),ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),U))**. % 40.70/23.78 7517[0:MRR:7456.1,7456.3,7456.4,21.0,32.0,50.1] || tp__o(U) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U)))* -> p(inj__o(U)). % 40.70/23.78 7696[0:Res:39.0,157.2] || del(skc7) del(skc8) mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc7,skc8),skc9),U))* mem(skf27(U,skc8,V,W),skc8)*. % 40.70/23.78 7697[0:Res:38.0,157.2] || del(skc8) del(bool) mem(U,arr(bool,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc8,bool),skc10),U))* mem(skf27(U,bool,V,W),bool)*. % 40.70/23.78 7698[0:Res:37.0,157.2] || del(skc8) del(bool) mem(U,arr(bool,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc8,bool),skc11),U))* mem(skf27(U,bool,V,W),bool)*. % 40.70/23.78 7720[0:MRR:7698.0,7698.1,28.0,26.0] || mem(U,arr(bool,bool))+ -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc8,bool),skc11),U))* mem(skf27(U,bool,V,W),bool)*. % 40.70/23.78 7721[0:MRR:7697.0,7697.1,28.0,26.0] || mem(U,arr(bool,bool))+ -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc8,bool),skc10),U))* mem(skf27(U,bool,V,W),bool)*. % 40.70/23.78 7722[0:MRR:7696.0,7696.1,29.0,28.0] || mem(U,arr(skc8,bool))+ -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc7,skc8),skc9),U))* mem(skf27(U,skc8,V,W),skc8)*. % 40.70/23.78 7767[0:SpL:1387.2,7517.1] || tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U))* tp__o(U) p(c_2Ebool_2ET) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2EF) p(inj__o(U)). % 40.70/23.78 7783[0:MRR:7767.2,21.0] || tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U))* tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2EF) p(inj__o(U)). % 40.70/23.78 7952[0:Res:39.0,158.2] || del(skc7) del(skc8) mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(skc7,skc8),skc9),U))* mem(skf24(U,skc8,V,W),skc8)*. % 40.70/23.78 7978[0:MRR:7952.0,7952.1,29.0,28.0] || mem(U,arr(skc8,bool))+ -> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(skc7,skc8),skc9),U))* mem(skf24(U,skc8,V,W),skc8)*. % 40.70/23.78 8815[0:Res:39.0,164.2] || del(skc7) del(skc8) mem(U,arr(skc8,bool)) -> p(ap(U,ap(skc9,skf21(skc7,skc9,U))))* p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U)). % 40.70/23.78 8841(e)[0:MRR:8815.0,8815.1,29.0,28.0] || mem(U,arr(skc8,bool)) -> p(ap(U,ap(skc9,skf21(skc7,skc9,U))))* p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U)). % 40.70/23.78 9376[4:Res:4450.2,4225.0] || del(bool) mem(c_2Ebool_2E_7E,arr(bool,bool))* -> . % 40.70/23.78 9377(e)[4:MRR:9376.0,9376.1,26.0,36.0] || -> . % 40.70/23.78 9379[4:Spt:9377.0,4426.1,4443.0] || equal(skf15(c_2Ebool_2E_7E,bool),c_2Ebool_2EF)** -> . % 40.70/23.78 9380[4:Spt:9377.0,4426.0] || -> p(skf15(c_2Ebool_2E_7E,bool))*. % 40.70/23.78 9476[5:Spt:2800.0] || -> p(ap(c_2Ebool_2E_21(skc8),skc10))*. % 40.70/23.78 9477[5:Res:9476.0,142.1] || del(skc8) mem(U,skc8) mem(skc10,arr(skc8,bool))* -> p(ap(skc10,U))*. % 40.70/23.78 9478[5:MRR:9477.0,9477.2,28.0,38.0] || mem(U,skc8) -> p(ap(skc10,U))*. % 40.70/23.78 9480[5:MRR:4945.1,9478.1] || mem(U,skc8) -> equal(surj__o(ap(skc10,U)),fo__c_2Ebool_2ET)**. % 40.70/23.78 9578[5:SpR:9480.1,59.1] || mem(U,skc8) mem(ap(skc10,U),bool)* -> equal(ap(skc10,U),inj__o(fo__c_2Ebool_2ET)). % 40.70/23.78 9587[5:Rew:35.0,9578.2] || mem(U,skc8) mem(ap(skc10,U),bool)* -> equal(ap(skc10,U),c_2Ebool_2ET). % 40.70/23.78 9588[5:Rew:3736.1,9587.1] || mem(U,skc8) mem(c_2Ebool_2EF,bool) -> equal(ap(skc10,U),c_2Ebool_2ET)**. % 40.70/23.78 9589[5:MRR:9588.1,31.0] || mem(U,skc8) -> equal(ap(skc10,U),c_2Ebool_2ET)**. % 40.70/23.78 10340[0:SpR:1477.1,1768.3] || tp__o(fo__c_2Emin_2E_3D_3D_3E(U,V))* tp__o(U) tp__o(V) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,V),fo__c_2Ebool_2ET) p(inj__o(U)) p(c_2Ebool_2EF). % 40.70/23.78 10386[0:Rew:1422.2,10340.0] || tp__o(fo__c_2Ebool_2EF) tp__o(U) tp__o(V) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,V),fo__c_2Ebool_2ET)** p(inj__o(U)) p(c_2Ebool_2EF). % 40.70/23.78 10387[0:MRR:10386.0,10386.5,22.0,30.0] || tp__o(U) tp__o(V) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,V),fo__c_2Ebool_2ET)** p(inj__o(U)). % 40.70/23.78 10508[0:Res:56.0,169.3] || del(skc7) del(skc8) p(ap(skc10,ap(skc9,U)))* mem(U,skc7) mem(skc9,arr(skc7,skc8)) mem(skc10,arr(skc8,bool)) -> . % 40.70/23.78 10509[0:MRR:10508.0,10508.1,10508.4,10508.5,29.0,28.0,39.0,38.0] || p(ap(skc10,ap(skc9,U)))* mem(U,skc7) -> . % 40.70/23.78 10510[5:SpL:9589.1,10509.0] || mem(ap(skc9,U),skc8)* p(c_2Ebool_2ET) mem(U,skc7) -> . % 40.70/23.78 10511[5:MRR:10510.0,10510.1,3702.1,21.0] || mem(U,skc7)* -> . % 40.70/23.78 10521[5:MRR:7010.2,10511.0] || mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U))*. % 40.70/23.78 10675[5:Res:10521.1,60.0] || mem(skc11,arr(skc8,bool))* -> . % 40.70/23.78 10682(e)[5:MRR:10675.0,37.0] || -> . % 40.70/23.78 10684(e)[5:Spt:10682.0,2800.0,9476.0] || p(ap(c_2Ebool_2E_21(skc8),skc10))* -> . % 40.70/23.78 10685[5:Spt:10682.0,2800.1] || -> mem(skf15(skc10,skc8),skc8)*. % 40.70/23.78 10726[6:Spt:2801.0] || -> p(ap(c_2Ebool_2E_21(skc8),skc11))*. % 40.70/23.78 10727[6:Res:10726.0,142.1] || del(skc8) mem(U,skc8) mem(skc11,arr(skc8,bool))* -> p(ap(skc11,U))*. % 40.70/23.78 10728[6:MRR:10727.0,10727.2,28.0,37.0] || mem(U,skc8) -> p(ap(skc11,U))*. % 40.70/23.78 10729[6:MRR:97.0,10728.1] || mem(U,skc8) -> p(ap(skc10,U))*. % 40.70/23.78 10734[6:MRR:4945.1,10729.1] || mem(U,skc8) -> equal(surj__o(ap(skc10,U)),fo__c_2Ebool_2ET)**. % 40.70/23.78 10810[6:SpR:10734.1,59.1] || mem(U,skc8) mem(ap(skc10,U),bool)* -> equal(ap(skc10,U),inj__o(fo__c_2Ebool_2ET)). % 40.70/23.78 10820[6:Rew:35.0,10810.2] || mem(U,skc8) mem(ap(skc10,U),bool)* -> equal(ap(skc10,U),c_2Ebool_2ET). % 40.70/23.78 10821[6:Rew:3736.1,10820.1] || mem(U,skc8) mem(c_2Ebool_2EF,bool) -> equal(ap(skc10,U),c_2Ebool_2ET)**. % 40.70/23.78 10822[6:MRR:10821.1,31.0] || mem(U,skc8) -> equal(ap(skc10,U),c_2Ebool_2ET)**. % 40.70/23.78 10866[6:SpL:10822.1,10509.0] || mem(ap(skc9,U),skc8)* p(c_2Ebool_2ET) mem(U,skc7) -> . % 40.70/23.78 10867[6:MRR:10866.0,10866.1,3702.1,21.0] || mem(U,skc7)* -> . % 40.70/23.78 10874[6:MRR:7010.2,10867.0] || mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U))*. % 40.70/23.78 10955[6:Res:10874.1,60.0] || mem(skc11,arr(skc8,bool))* -> . % 40.70/23.78 10962(e)[6:MRR:10955.0,37.0] || -> . % 40.70/23.78 10964(e)[6:Spt:10962.0,2801.0,10726.0] || p(ap(c_2Ebool_2E_21(skc8),skc11))* -> . % 40.70/23.78 10965[6:Spt:10962.0,2801.1] || -> mem(skf15(skc11,skc8),skc8)*. % 40.70/23.78 11176[0:SpL:3753.2,3923.0] || mem(U,skc8) p(c_2Ebool_2ET) mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF)** p(ap(c_2Ebool_2E_3F(skc8),skc11))*. % 40.70/23.78 11177[0:SpL:3753.2,97.0] || mem(U,skc8) p(c_2Ebool_2ET) mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF) p(ap(skc10,U))*. % 40.70/23.78 11192[0:Obv:11177.0] || p(c_2Ebool_2ET) mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF) p(ap(skc10,U))*. % 40.70/23.78 11193(e)[0:MRR:11192.0,21.0] || mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF) p(ap(skc10,U))*. % 40.70/23.78 11195[0:Obv:11176.0] || p(c_2Ebool_2ET) mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF)** p(ap(c_2Ebool_2E_3F(skc8),skc11))*. % 40.70/23.78 11196[0:MRR:11195.0,21.0] || mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF)** p(ap(c_2Ebool_2E_3F(skc8),skc11))*. % 40.70/23.78 11207[0:Res:11193.2,3922.0] || mem(U,skc8) mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF)** p(ap(c_2Ebool_2E_3F(skc8),skc10))*. % 40.70/23.78 11212[0:Res:11193.2,10509.0] || mem(ap(skc9,U),skc8) mem(U,skc7) -> equal(ap(skc11,ap(skc9,U)),c_2Ebool_2EF)**. % 40.70/23.78 11214(e)[0:MRR:11212.0,3702.1] || mem(U,skc7) -> equal(ap(skc11,ap(skc9,U)),c_2Ebool_2EF)**. % 40.70/23.78 11215(e)[0:Obv:11207.0] || mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF)** p(ap(c_2Ebool_2E_3F(skc8),skc10))*. % 40.70/23.78 11223[7:Spt:6153.2] || -> mem(skf13(bool,U,V),bool)*. % 40.70/23.78 11310[0:SpL:3736.2,10509.0] || mem(ap(skc9,U),skc8) p(c_2Ebool_2ET) mem(U,skc7) -> equal(ap(skc10,ap(skc9,U)),c_2Ebool_2EF)**. % 40.70/23.78 11312(e)[0:MRR:11310.0,11310.1,3702.1,21.0] || mem(U,skc7) -> equal(ap(skc10,ap(skc9,U)),c_2Ebool_2EF)**. % 40.70/23.78 11631[0:SpR:1477.1,1556.3] || tp__o(fo__c_2Ebool_2E_5C_2F(U,V))* tp__o(U) tp__o(V) p(inj__o(V)) -> equal(fo__c_2Ebool_2E_5C_2F(U,V),fo__c_2Ebool_2ET) p(c_2Ebool_2EF). % 40.70/23.78 11672[0:Rew:1420.2,11631.0] || tp__o(fo__c_2Ebool_2EF) tp__o(U) tp__o(V) p(inj__o(V)) -> equal(fo__c_2Ebool_2E_5C_2F(U,V),fo__c_2Ebool_2ET)** p(c_2Ebool_2EF). % 40.70/23.78 11673[0:MRR:11672.0,11672.5,22.0,30.0] || tp__o(U) tp__o(V) p(inj__o(V)) -> equal(fo__c_2Ebool_2E_5C_2F(U,V),fo__c_2Ebool_2ET)**. % 40.70/23.78 12432[0:SpR:6866.1,79.1] || mem(U,bool) tp__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF)) -> equal(ap(c_2Ebool_2E_7E,ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF)),inj__o(fo__c_2Ebool_2E_7E(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF))))**. % 40.70/23.78 12459[0:SpR:6866.1,7039.2] || mem(U,bool) tp__o(surj__o(U)) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2ET)**. % 40.70/23.78 12461[0:SpR:1418.1,6866.1] || mem(U,bool) -> equal(surj__o(U),fo__c_2Ebool_2EF) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))**. % 40.70/23.78 12463[3:SpR:4944.2,6866.1] || tp__o(U) p(inj__o(fo__c_2Ebool_2E_7E(U))) mem(inj__o(fo__c_2Ebool_2E_7E(U)),bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(fo__c_2Ebool_2E_7E(U))),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))**. % 40.70/23.78 12472[0:SpR:10387.2,6866.1] || tp__o(surj__o(U)) tp__o(fo__c_2Ebool_2EF) mem(U,bool) -> p(inj__o(surj__o(U))) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2ET))**. % 40.70/23.78 12479(e)[0:Rew:34.0,12461.2,6969.0,12461.2] || mem(U,bool) -> equal(surj__o(U),fo__c_2Ebool_2EF) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 12480[0:Rew:1418.0,12459.1] || mem(U,bool) tp__o(fo__c_2Ebool_2EF) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2ET)**. % 40.70/23.78 12481[0:MRR:12480.1,22.0] || mem(U,bool) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2ET)**. % 40.70/23.78 12489[0:Rew:35.0,12472.4,59.1,12472.3] || tp__o(surj__o(U)) tp__o(fo__c_2Ebool_2EF) mem(U,bool) -> p(U) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2ET)**. % 40.70/23.78 12490[0:Rew:12481.1,12489.0] || tp__o(fo__c_2Ebool_2ET) tp__o(fo__c_2Ebool_2EF) mem(U,bool) -> p(U) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2ET)**. % 40.70/23.78 12491[0:MRR:12490.0,12490.1,23.0,22.0] || mem(U,bool) -> p(U) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2ET)**. % 40.70/23.78 12507[3:Rew:34.0,12463.3,6969.0,12463.3] || tp__o(U) p(inj__o(fo__c_2Ebool_2E_7E(U))) mem(inj__o(fo__c_2Ebool_2E_7E(U)),bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(fo__c_2Ebool_2E_7E(U))),c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 12508(e)[3:MRR:12507.2,3787.1] || tp__o(U) p(inj__o(fo__c_2Ebool_2E_7E(U))) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(fo__c_2Ebool_2E_7E(U))),c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 12511[0:SpR:12491.2,1747.1] || mem(inj__o(U),bool) tp__o(U) -> p(inj__o(U)) equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)),c_2Ebool_2ET)**. % 40.70/23.78 12520[0:MRR:12511.0,50.1] || tp__o(U) -> p(inj__o(U)) equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)),c_2Ebool_2ET)**. % 40.70/23.78 12687[0:SpR:7463.1,7462.2] || mem(U,bool) tp__o(surj__o(U)) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 40.70/23.78 12706[0:Rew:1418.0,12687.1] || mem(U,bool) tp__o(fo__c_2Ebool_2EF) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 40.70/23.78 12707[0:MRR:12706.1,22.0] || mem(U,bool) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 40.70/23.78 14579(e)[0:SpR:11673.3,2881.1] || tp__o(fo__c_2Ebool_2EF) tp__o(surj__o(U)) p(inj__o(surj__o(U))) mem(U,bool) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U),inj__o(fo__c_2Ebool_2ET))**. % 40.70/23.78 14608(e)[0:Rew:35.0,14579.4,59.1,14579.2] || tp__o(fo__c_2Ebool_2EF) tp__o(surj__o(U)) p(U) mem(U,bool) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U),c_2Ebool_2ET)**. % 40.70/23.78 14609[3:Rew:4938.2,14608.1] || tp__o(fo__c_2Ebool_2EF) tp__o(fo__c_2Ebool_2ET) p(U) mem(U,bool) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U),c_2Ebool_2ET)**. % 40.70/23.78 14610(e)[3:MRR:14609.0,14609.1,22.0,23.0] || p(U) mem(U,bool) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U),c_2Ebool_2ET)**. % 40.70/23.78 16287[0:Res:50.1,4463.1] || tp__o(U)+ tp__o(V) -> p(inj__o(V))* p(inj__o(U))* equal(inj__o(V),inj__o(U))*. % 40.70/23.78 16888[0:Res:66.2,7783.0] || tp__o(fo__c_2Ebool_2ET) tp__o(U) tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2EF)** p(inj__o(U)). % 40.70/23.78 16894[0:Obv:16888.1] || tp__o(fo__c_2Ebool_2ET) tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2EF)** p(inj__o(U)). % 40.70/23.78 16895[0:MRR:16894.0,23.0] || tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2EF)** p(inj__o(U)). % 40.70/23.78 16921[0:SpR:16895.1,7463.1] || tp__o(surj__o(U)) mem(U,bool) -> p(inj__o(surj__o(U))) equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),U),inj__o(fo__c_2Ebool_2EF))**. % 40.70/23.78 16947[0:Rew:34.0,16921.3,59.1,16921.2] || tp__o(surj__o(U)) mem(U,bool) -> p(U) equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 40.70/23.78 16948[0:Rew:12707.1,16947.0] || tp__o(fo__c_2Ebool_2ET) mem(U,bool) -> p(U) equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 40.70/23.78 16949[0:MRR:16948.0,23.0] || mem(U,bool) -> p(U) equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 40.70/23.78 20510[3:SpR:12508.2,1747.1] || tp__o(U) p(inj__o(fo__c_2Ebool_2E_7E(U))) tp__o(fo__c_2Ebool_2E_7E(U)) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)),c_2Ebool_2EF)**. % 40.70/23.78 20539(e)[3:MRR:20510.2,42.1] || tp__o(U) p(inj__o(fo__c_2Ebool_2E_7E(U))) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)),c_2Ebool_2EF)**. % 40.70/23.78 21836[0:Res:33.0,16287.0] || tp__o(U)+ -> p(inj__o(U))* p(inj__o(surj__o(V)))* equal(inj__o(U),inj__o(surj__o(V)))*. % 40.70/23.78 21845[0:Res:22.0,21836.0] || -> p(inj__o(fo__c_2Ebool_2EF)) p(inj__o(surj__o(U)))* equal(inj__o(surj__o(U)),inj__o(fo__c_2Ebool_2EF)). % 40.70/23.78 21848[0:Res:68.2,21836.0] || tp__o(U) tp__o(V) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(U,V)))* p(inj__o(surj__o(W)))* equal(inj__o(fo__c_2Ebool_2E_5C_2F(U,V)),inj__o(surj__o(W)))*. % 40.70/23.78 21849[0:Res:67.2,21836.0] || tp__o(U) tp__o(V) -> p(inj__o(fo__c_2Ebool_2E_2F_5C(U,V)))* p(inj__o(surj__o(W)))* equal(inj__o(fo__c_2Ebool_2E_2F_5C(U,V)),inj__o(surj__o(W)))*. % 40.70/23.78 21850[0:Res:66.2,21836.0] || tp__o(U) tp__o(V) -> p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)))* p(inj__o(surj__o(W)))* equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)),inj__o(surj__o(W)))*. % 40.70/23.78 21852[0:Rew:34.0,21845.2,34.0,21845.0] || -> p(c_2Ebool_2EF) p(inj__o(surj__o(U)))* equal(inj__o(surj__o(U)),c_2Ebool_2EF). % 40.70/23.78 21853[0:MRR:21852.0,30.0] || -> p(inj__o(surj__o(U)))* equal(inj__o(surj__o(U)),c_2Ebool_2EF). % 40.70/23.78 21859[0:Rew:21853.1,21850.4] || tp__o(U) tp__o(V) -> p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)))* p(inj__o(surj__o(W)))* equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)),c_2Ebool_2EF). % 40.70/23.78 21860[0:Rew:21853.1,21849.4] || tp__o(U) tp__o(V) -> p(inj__o(fo__c_2Ebool_2E_2F_5C(U,V)))* p(inj__o(surj__o(W)))* equal(inj__o(fo__c_2Ebool_2E_2F_5C(U,V)),c_2Ebool_2EF). % 40.70/23.78 21861[0:Rew:21853.1,21848.4] || tp__o(U) tp__o(V) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(U,V)))* p(inj__o(surj__o(W)))* equal(inj__o(fo__c_2Ebool_2E_5C_2F(U,V)),c_2Ebool_2EF). % 40.70/23.78 21985[8:Spt:21859.3] || -> p(inj__o(surj__o(U)))*. % 40.70/23.78 21987(e)[8:SpR:55.1,21985.0] || tp__o(U) -> p(inj__o(U))*. % 40.70/23.78 22002[8:SpR:1477.1,21985.0] || tp__o(surj__o(U))* -> equal(surj__o(U),fo__c_2Ebool_2ET) p(c_2Ebool_2EF). % 40.70/23.78 22004(e)[8:SpR:59.1,21985.0] || mem(U,bool)* -> p(U). % 40.70/23.78 22009[8:MRR:676.0,21987.1] || tp__o(U) -> equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2EF)**. % 40.70/23.78 22061(e)[8:MRR:4938.1,22004.1] || mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2ET). % 40.70/23.78 22174[8:Rew:22009.1,12432.2] || mem(U,bool) tp__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF)) -> equal(ap(c_2Ebool_2E_7E,ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF)),c_2Ebool_2EF)**. % 40.70/23.78 22236[8:Rew:22061.1,12479.1] || mem(U,bool) -> equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 22500[8:Rew:1418.0,22002.0] || tp__o(fo__c_2Ebool_2EF) -> equal(surj__o(U),fo__c_2Ebool_2ET)** p(c_2Ebool_2EF). % 40.70/23.78 22501(e)[8:MRR:22500.0,22500.2,22.0,30.0] || -> equal(surj__o(U),fo__c_2Ebool_2ET)**. % 40.70/23.78 22571(e)[8:MRR:22236.1,4772.0] || mem(U,bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 22814[8:Rew:22571.1,22174.2,22501.0,22174.1] || mem(U,bool)* tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF))* -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2EF). % 40.70/23.78 22815[8:Rew:4306.0,22814.2,6969.0,22814.1] || mem(U,bool)* tp__o(fo__c_2Ebool_2EF) -> equal(c_2Ebool_2ET,c_2Ebool_2EF). % 40.70/23.78 22816[8:MRR:22815.1,22815.2,22.0,4308.0] || mem(U,bool)* -> . % 40.70/23.78 22817(e)[8:UnC:22816.0,11223.0] || -> . % 40.70/23.78 23331(e)[8:Spt:22817.0,21859.0,21859.1,21859.2,21859.4] || tp__o(U) tp__o(V) -> p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)))* equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)),c_2Ebool_2EF). % 40.70/23.78 23465[9:Spt:21861.3] || -> p(inj__o(surj__o(U)))*. % 40.70/23.78 23469(e)[9:SpR:55.1,23465.0] || tp__o(U) -> p(inj__o(U))*. % 40.70/23.78 23472(e)[9:SpR:59.1,23465.0] || mem(U,bool)* -> p(U). % 40.70/23.78 23482[9:MRR:676.0,23469.1] || tp__o(U) -> equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2EF)**. % 40.70/23.78 23534(e)[9:MRR:4938.1,23472.1] || mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2ET). % 40.70/23.78 23626[9:Rew:23482.1,12432.2] || mem(U,bool) tp__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF)) -> equal(ap(c_2Ebool_2E_7E,ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF)),c_2Ebool_2EF)**. % 40.70/23.78 23733[9:Rew:23534.1,12479.1] || mem(U,bool) -> equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 23984(e)[9:MRR:23733.1,4772.0] || mem(U,bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 24135[9:Rew:23984.1,23626.2,23534.1,23626.1] || mem(U,bool)* tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF))* -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2EF). % 40.70/23.78 24136[9:Rew:4306.0,24135.2,6969.0,24135.1] || mem(U,bool)* tp__o(fo__c_2Ebool_2EF) -> equal(c_2Ebool_2ET,c_2Ebool_2EF). % 40.70/23.78 24137[9:MRR:24136.1,24136.2,22.0,4308.0] || mem(U,bool)* -> . % 40.70/23.78 24138(e)[9:UnC:24137.0,11223.0] || -> . % 40.70/23.78 24638(e)[9:Spt:24138.0,21861.0,21861.1,21861.2,21861.4] || tp__o(U) tp__o(V) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(U,V)))* equal(inj__o(fo__c_2Ebool_2E_5C_2F(U,V)),c_2Ebool_2EF). % 40.70/23.78 24743[10:Spt:21860.3] || -> p(inj__o(surj__o(U)))*. % 40.70/23.78 24747(e)[10:SpR:55.1,24743.0] || tp__o(U) -> p(inj__o(U))*. % 40.70/23.78 24750(e)[10:SpR:59.1,24743.0] || mem(U,bool)* -> p(U). % 40.70/23.78 24754[10:MRR:676.0,24747.1] || tp__o(U) -> equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2EF)**. % 40.70/23.78 24812(e)[10:MRR:4938.1,24750.1] || mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2ET). % 40.70/23.78 24901[10:Rew:24754.1,12432.2] || mem(U,bool) tp__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF)) -> equal(ap(c_2Ebool_2E_7E,ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF)),c_2Ebool_2EF)**. % 40.70/23.78 25011[10:Rew:24812.1,12479.1] || mem(U,bool) -> equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF) equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 25262(e)[10:MRR:25011.1,4772.0] || mem(U,bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2EF)**. % 40.70/23.78 25414[10:Rew:25262.1,24901.2,24812.1,24901.1] || mem(U,bool)* tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF))* -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2EF). % 40.70/23.78 25415[10:Rew:4306.0,25414.2,6969.0,25414.1] || mem(U,bool)* tp__o(fo__c_2Ebool_2EF) -> equal(c_2Ebool_2ET,c_2Ebool_2EF). % 40.70/23.78 25416[10:MRR:25415.1,25415.2,22.0,4308.0] || mem(U,bool)* -> . % 40.70/23.78 25417(e)[10:UnC:25416.0,11223.0] || -> . % 40.70/23.78 25920(e)[10:Spt:25417.0,21860.0,21860.1,21860.2,21860.4] || tp__o(U) tp__o(V) -> p(inj__o(fo__c_2Ebool_2E_2F_5C(U,V)))* equal(inj__o(fo__c_2Ebool_2E_2F_5C(U,V)),c_2Ebool_2EF). % 40.70/23.78 29342[11:Spt:11215.2] || -> p(ap(c_2Ebool_2E_3F(skc8),skc10))*. % 40.70/23.78 29343[11:Res:29342.0,136.1] || del(skc8) mem(skc10,arr(skc8,bool)) -> p(ap(skc10,skf14(skc10,U)))*. % 40.70/23.78 29344[11:Res:29342.0,131.1] || del(skc8) mem(skc10,arr(skc8,bool)) -> mem(skf14(skc10,skc8),skc8)*. % 40.70/23.78 29345[11:MRR:29344.0,29344.1,28.0,38.0] || -> mem(skf14(skc10,skc8),skc8)*. % 40.70/23.78 29346[11:MRR:29343.0,29343.1,28.0,38.0] || -> p(ap(skc10,skf14(skc10,U)))*. % 40.70/23.78 36785[0:Res:38.0,3867.0] || -> equal(ap(c_2Ebool_2E_3F(skc8),skc10),c_2Ebool_2EF) equal(ap(c_2Ebool_2E_3F(skc8),skc10),c_2Ebool_2ET)**. % 40.70/23.78 36786[0:Res:37.0,3867.0] || -> equal(ap(c_2Ebool_2E_3F(skc8),skc11),c_2Ebool_2EF) equal(ap(c_2Ebool_2E_3F(skc8),skc11),c_2Ebool_2ET)**. % 40.70/23.78 36790(e)[12:Spt:36785.0] || -> equal(ap(c_2Ebool_2E_3F(skc8),skc10),c_2Ebool_2EF)**. % 40.70/23.78 36791[12:Rew:36790.0,29342.0] || -> p(c_2Ebool_2EF)*. % 40.70/23.78 36792(e)[12:MRR:36791.0,30.0] || -> . % 40.70/23.78 36793[12:Spt:36792.0,36785.0,36790.0] || equal(ap(c_2Ebool_2E_3F(skc8),skc10),c_2Ebool_2EF)** -> . % 40.70/23.78 36794[12:Spt:36792.0,36785.1] || -> equal(ap(c_2Ebool_2E_3F(skc8),skc10),c_2Ebool_2ET)**. % 40.70/23.78 37616[0:SpR:2881.1,1750.2] || mem(U,bool) mem(V,bool) tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,surj__o(U))) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,V),ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U)),inj__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(V),fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,surj__o(U)))))**. % 40.70/23.78 38077[0:SpR:6866.1,1755.2] || mem(U,bool) mem(V,bool) tp__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF)) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF)),V),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF),surj__o(V))))**. % 40.70/23.78 39143(e)[0:Res:38.0,6943.0] || -> p(ap(skc10,skf17(skc10,U)))* p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(skc7,skc8),skc9),skc10))*. % 40.70/23.78 39148[13:Spt:39143.1] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(skc7,skc8),skc9),skc10))*. % 40.70/23.78 39149[13:Res:39148.0,179.3] || del(skc7) del(skc8) p(ap(skc10,U))* mem(U,skc8) mem(skc9,arr(skc7,skc8)) mem(skc10,arr(skc8,bool)) -> p(ap(skc10,ap(skc9,skf16(skc7,skc9,skc10))))*. % 40.70/23.78 39150[13:Res:39148.0,175.3] || del(skc7) del(skc8) p(ap(skc10,U))* mem(U,skc8) mem(skc9,arr(skc7,skc8)) mem(skc10,arr(skc8,bool)) -> mem(skf16(skc7,V,W),skc7)*. % 40.70/23.78 39151[13:MRR:39150.0,39150.1,39150.4,39150.5,29.0,28.0,39.0,38.0] || p(ap(skc10,U))*+ mem(U,skc8) -> mem(skf16(skc7,V,W),skc7)*. % 40.70/23.78 39152[13:MRR:39149.0,39149.1,39149.4,39149.5,29.0,28.0,39.0,38.0] || p(ap(skc10,U))*+ mem(U,skc8) -> p(ap(skc10,ap(skc9,skf16(skc7,skc9,skc10))))*. % 40.70/23.78 39161[13:Res:29346.0,39151.0] || mem(skf14(skc10,U),skc8)*+ -> mem(skf16(skc7,V,W),skc7)*. % 40.70/23.78 39168[13:Res:29345.0,39161.0] || -> mem(skf16(skc7,U,V),skc7)*. % 40.70/23.78 39524[13:Res:29346.0,39152.0] || mem(skf14(skc10,U),skc8)*+ -> p(ap(skc10,ap(skc9,skf16(skc7,skc9,skc10))))*. % 40.70/23.78 39531[13:Res:29345.0,39524.0] || -> p(ap(skc10,ap(skc9,skf16(skc7,skc9,skc10))))*. % 40.70/23.78 39533[13:SpR:11312.1,39531.0] || mem(skf16(skc7,skc9,skc10),skc7)* -> p(c_2Ebool_2EF). % 40.70/23.78 39535(e)[13:MRR:39533.0,39533.1,39168.0,30.0] || -> . % 40.70/23.78 39536[13:Spt:39535.0,39143.1,39148.0] || p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(skc7,skc8),skc9),skc10))* -> . % 40.70/23.78 39537[13:Spt:39535.0,39143.0] || -> p(ap(skc10,skf17(skc10,U)))*. % 40.70/23.78 39598[14:Spt:36786.0] || -> equal(ap(c_2Ebool_2E_3F(skc8),skc11),c_2Ebool_2EF)**. % 40.70/23.78 39599[14:Rew:39598.0,11196.2] || mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF)** p(c_2Ebool_2EF). % 40.70/23.78 39600[14:MRR:39599.2,30.0] || mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF)**. % 40.70/23.78 40479(e)[0:Res:36.0,7720.0] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc8,bool),skc11),c_2Ebool_2E_7E))* mem(skf27(c_2Ebool_2E_7E,bool,U,V),bool)*. % 40.70/23.78 40605(e)[0:Res:36.0,7721.0] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc8,bool),skc10),c_2Ebool_2E_7E))* mem(skf27(c_2Ebool_2E_7E,bool,U,V),bool)*. % 40.70/23.78 40655(e)[0:Res:38.0,7722.0] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc7,skc8),skc9),skc10))* mem(skf27(skc10,skc8,U,V),skc8)*. % 40.70/23.78 40656(e)[0:Res:37.0,7722.0] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc7,skc8),skc9),skc11))* mem(skf27(skc11,skc8,U,V),skc8)*. % 40.70/23.78 40661[15:Spt:40655.0] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc7,skc8),skc9),skc10))*. % 40.70/23.78 40663[15:Res:40661.0,172.2] || del(skc7) del(skc8) mem(U,skc8) mem(skc9,arr(skc7,skc8)) mem(skc10,arr(skc8,bool)) -> p(ap(skc10,U))* mem(skf25(skc7,V,W),skc7)*. % 40.70/23.78 40664(e)[15:MRR:40663.0,40663.1,40663.3,40663.4,29.0,28.0,39.0,38.0] || mem(U,skc8) -> p(ap(skc10,U))* mem(skf25(skc7,V,W),skc7)*. % 40.70/23.78 40666[16:Spt:40664.2] || -> mem(skf25(skc7,U,V),skc7)*. % 40.70/23.78 40669[17:Spt:40656.0] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc7,skc8),skc9),skc11))*. % 40.70/23.78 40670[17:Res:40669.0,176.2] || del(skc7) del(skc8) mem(U,skc8) mem(skc9,arr(skc7,skc8)) mem(skc11,arr(skc8,bool)) -> p(ap(skc11,U)) equal(ap(skc9,skf25(skc7,skc9,U)),U)**. % 40.70/23.78 40672[17:Rew:39600.1,40670.5] || del(skc7) del(skc8) mem(U,skc8) mem(skc9,arr(skc7,skc8)) mem(skc11,arr(skc8,bool)) -> p(c_2Ebool_2EF) equal(ap(skc9,skf25(skc7,skc9,U)),U)**. % 40.70/23.78 40673[17:MRR:40672.0,40672.1,40672.3,40672.4,40672.5,29.0,28.0,39.0,37.0,30.0] || mem(U,skc8) -> equal(ap(skc9,skf25(skc7,skc9,U)),U)**. % 40.70/23.78 40676[17:SpR:40673.1,11312.1] || mem(U,skc8) mem(skf25(skc7,skc9,U),skc7)* -> equal(ap(skc10,U),c_2Ebool_2EF). % 40.70/23.78 40683[17:MRR:40676.1,40666.0] || mem(U,skc8) -> equal(ap(skc10,U),c_2Ebool_2EF)**. % 40.70/23.78 40778[17:SpR:40683.1,300.2] || mem(skf14(skc10,U),skc8)* p(ap(c_2Ebool_2E_3F(skc8),skc10))* mem(skc10,arr(skc8,bool)) -> p(c_2Ebool_2EF). % 40.70/23.78 40800[17:Rew:36794.0,40778.1] || mem(skf14(skc10,U),skc8)* p(c_2Ebool_2ET) mem(skc10,arr(skc8,bool)) -> p(c_2Ebool_2EF). % 40.70/23.78 40801[17:MRR:40800.1,40800.2,40800.3,21.0,38.0,30.0] || mem(skf14(skc10,U),skc8)* -> . % 40.70/23.78 40802(e)[17:UnC:40801.0,29345.0] || -> . % 40.70/23.78 40804[17:Spt:40802.0,40656.0,40669.0] || p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc7,skc8),skc9),skc11))* -> . % 40.70/23.78 40805[17:Spt:40802.0,40656.1] || -> mem(skf27(skc11,skc8,U,V),skc8)*. % 40.70/23.78 41007[18:Spt:40605.0] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc8,bool),skc10),c_2Ebool_2E_7E))*. % 40.70/23.78 41009[18:Res:41007.0,172.2] || del(skc8) del(bool) mem(U,bool) mem(skc10,arr(skc8,bool)) mem(c_2Ebool_2E_7E,arr(bool,bool)) -> p(ap(c_2Ebool_2E_7E,U))* mem(skf25(skc8,V,W),skc8)*. % 40.70/23.78 41010(e)[18:MRR:41009.0,41009.1,41009.3,41009.4,28.0,26.0,38.0,36.0] || mem(U,bool) -> p(ap(c_2Ebool_2E_7E,U))* mem(skf25(skc8,V,W),skc8)*. % 40.70/23.78 41012[19:Spt:41010.2] || -> mem(skf25(skc8,U,V),skc8)*. % 40.70/23.78 41015[20:Spt:40479.0] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc8,bool),skc11),c_2Ebool_2E_7E))*. % 40.70/23.78 41016[20:Res:41015.0,176.2] || del(skc8) del(bool) mem(U,bool) mem(skc11,arr(skc8,bool)) mem(c_2Ebool_2E_7E,arr(bool,bool)) -> p(ap(c_2Ebool_2E_7E,U)) equal(ap(skc11,skf25(skc8,skc11,U)),U)**. % 40.70/23.78 41018[20:MRR:41016.0,41016.1,41016.3,41016.4,28.0,26.0,37.0,36.0] || mem(U,bool) -> p(ap(c_2Ebool_2E_7E,U)) equal(ap(skc11,skf25(skc8,skc11,U)),U)**. % 40.70/23.78 42035[20:SpR:41018.2,39600.1] || mem(U,bool) mem(skf25(skc8,skc11,U),skc8)* -> p(ap(c_2Ebool_2E_7E,U)) equal(U,c_2Ebool_2EF). % 40.70/23.78 42042[20:Rew:705.2,42035.2] || mem(U,bool) mem(skf25(skc8,skc11,U),skc8)* -> p(c_2Ebool_2EF) equal(U,c_2Ebool_2EF). % 40.70/23.78 42043[20:MRR:42042.1,42042.2,41012.0,30.0] || mem(U,bool)* -> equal(U,c_2Ebool_2EF). % 40.70/23.78 42045(e)[0:Res:38.0,7978.0] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(skc7,skc8),skc9),skc10))* mem(skf24(skc10,skc8,U,V),skc8)*. % 40.70/23.78 42053(e)[20:Res:50.1,42043.0] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)**. % 40.70/23.78 42065(e)[20:Res:3706.1,42043.0] || mem(U,bool) -> equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2EF)**. % 40.70/23.78 42271[20:Rew:42053.1,16895.2] || tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2EF)** p(c_2Ebool_2EF). % 40.70/23.78 42640[20:Rew:42065.1,1593.2] || mem(U,bool)* -> p(U) equal(c_2Ebool_2ET,c_2Ebool_2EF). % 40.70/23.78 42787(e)[20:MRR:42640.2,4308.0] || mem(U,bool)* -> p(U). % 40.70/23.78 42789(e)[20:MRR:4938.1,42787.1] || mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2ET). % 40.70/23.78 42798(e)[20:MRR:14610.0,42787.1] || mem(U,bool) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U),c_2Ebool_2ET)**. % 40.70/23.78 42945[20:Rew:42789.1,37616.3] || mem(U,bool) mem(V,bool) tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,surj__o(U))) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,V),ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U)),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,surj__o(U)))))**. % 40.70/23.78 43086(e)[20:MRR:42271.2,30.0] || tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2EF)**. % 40.70/23.78 44432[20:Rew:42798.1,42945.3,43086.1,42945.3,42789.1,42945.3,42789.1,42945.2] || mem(U,bool)* mem(V,bool) tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET)) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,V),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2EF))**. % 40.70/23.78 44433[20:Con:44432.0] || mem(U,bool) tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET)) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2EF))**. % 40.70/23.78 44434[20:Rew:6699.1,44433.2,34.0,44433.2,1943.0,44433.1] || mem(U,bool)* tp__o(fo__c_2Ebool_2ET) -> equal(c_2Ebool_2ET,c_2Ebool_2EF). % 40.70/23.78 44435[20:MRR:44434.1,44434.2,23.0,4308.0] || mem(U,bool)* -> . % 40.70/23.78 44436(e)[20:UnC:44435.0,31.0] || -> . % 40.70/23.78 44719[20:Spt:44436.0,40479.0,41015.0] || p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc8,bool),skc11),c_2Ebool_2E_7E))* -> . % 40.70/23.78 44720[20:Spt:44436.0,40479.1] || -> mem(skf27(c_2Ebool_2E_7E,bool,U,V),bool)*. % 40.70/23.78 50080[21:Spt:42045.0] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(skc7,skc8),skc9),skc10))*. % 40.70/23.78 51022[21:Res:50080.0,174.3] || del(skc7) del(skc8) p(ap(skc10,U))* mem(U,skc8) mem(skc9,arr(skc7,skc8)) mem(skc10,arr(skc8,bool)) -> mem(skf22(skc7,V,W),skc7)*. % 40.70/23.78 51031[21:MRR:51022.0,51022.1,51022.4,51022.5,29.0,28.0,39.0,38.0] || p(ap(skc10,U))*+ mem(U,skc8) -> mem(skf22(skc7,V,W),skc7)*. % 40.70/23.78 51323[21:Res:50080.0,177.3] || del(skc7) del(skc8) p(ap(skc10,U)) mem(U,skc8) mem(skc9,arr(skc7,skc8)) mem(skc10,arr(skc8,bool)) -> equal(ap(skc9,skf22(skc7,skc9,U)),U)**. % 40.70/23.78 51333[21:MRR:51323.0,51323.1,51323.4,51323.5,29.0,28.0,39.0,38.0] || p(ap(skc10,U)) mem(U,skc8) -> equal(ap(skc9,skf22(skc7,skc9,U)),U)**. % 40.70/23.78 51728[21:Res:29346.0,51031.0] || mem(skf14(skc10,U),skc8)*+ -> mem(skf22(skc7,V,W),skc7)*. % 40.70/23.78 51798[21:Res:29345.0,51728.0] || -> mem(skf22(skc7,U,V),skc7)*. % 40.70/23.78 56724[21:SpR:51333.2,11312.1] || p(ap(skc10,U)) mem(U,skc8) mem(skf22(skc7,skc9,U),skc7)* -> equal(ap(skc10,U),c_2Ebool_2EF). % 40.70/23.78 56731[21:Rew:3736.2,56724.0] || p(c_2Ebool_2ET) mem(U,skc8) mem(skf22(skc7,skc9,U),skc7)* -> equal(ap(skc10,U),c_2Ebool_2EF). % 40.70/23.78 56732[21:MRR:56731.0,56731.2,21.0,51798.0] || mem(U,skc8) -> equal(ap(skc10,U),c_2Ebool_2EF)**. % 40.70/23.78 56841[21:SpR:56732.1,300.2] || mem(skf14(skc10,U),skc8)* p(ap(c_2Ebool_2E_3F(skc8),skc10))* mem(skc10,arr(skc8,bool)) -> p(c_2Ebool_2EF). % 40.70/23.78 57638[21:Rew:36794.0,56841.1] || mem(skf14(skc10,U),skc8)* p(c_2Ebool_2ET) mem(skc10,arr(skc8,bool)) -> p(c_2Ebool_2EF). % 40.70/23.78 57639[21:MRR:57638.1,57638.2,57638.3,21.0,38.0,30.0] || mem(skf14(skc10,U),skc8)* -> . % 40.70/23.78 57640(e)[21:UnC:57639.0,29345.0] || -> . % 40.70/23.78 58315[21:Spt:57640.0,42045.0,50080.0] || p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(skc7,skc8),skc9),skc10))* -> . % 40.70/23.78 58316[21:Spt:57640.0,42045.1] || -> mem(skf24(skc10,skc8,U,V),skc8)*. % 40.70/23.78 62958[22:Spt:7010.2] || -> mem(skf21(skc7,U,V),skc7)*. % 40.70/23.78 66539[0:SpR:11214.1,8841.1] || mem(skf21(skc7,skc9,skc11),skc7) mem(skc11,arr(skc8,bool)) -> p(c_2Ebool_2EF) p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),skc11))*. % 40.70/23.78 66564(e)[22:MRR:66539.0,66539.1,66539.2,66539.3,62958.0,37.0,30.0,60.0] || -> . % 40.70/23.78 66576[22:Spt:66564.0,7010.0,7010.1] || mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U))*. % 40.70/23.78 66585[22:Res:66576.1,60.0] || mem(skc11,arr(skc8,bool))* -> . % 40.70/23.78 66595(e)[22:MRR:66585.0,37.0] || -> . % 40.70/23.78 66599[19:Spt:66595.0,41010.0,41010.1] || mem(U,bool) -> p(ap(c_2Ebool_2E_7E,U))*. % 40.70/23.78 66642[0:MRR:66539.1,66539.2,66539.3,37.0,30.0,60.0] || mem(skf21(skc7,skc9,skc11),skc7)* -> . % 40.70/23.78 66655[19:SpR:79.1,66599.1] || tp__o(U) mem(inj__o(U),bool) -> p(inj__o(fo__c_2Ebool_2E_7E(U)))*. % 40.70/23.78 66657[19:SpR:587.2,66599.1] || p(U) mem(U,bool)* mem(U,bool)* -> p(c_2Ebool_2EF). % 40.70/23.78 66671[19:MRR:66655.1,50.1] || tp__o(U) -> p(inj__o(fo__c_2Ebool_2E_7E(U)))*. % 40.70/23.78 66673[19:MRR:20539.1,66671.1] || tp__o(U) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)),c_2Ebool_2EF)**. % 40.70/23.78 66710[19:Rew:66673.1,7041.2] || p(inj__o(U))* tp__o(U) -> equal(c_2Ebool_2ET,c_2Ebool_2EF). % 40.70/23.78 66711[19:MRR:66710.2,4308.0] || p(inj__o(U))* tp__o(U) -> . % 40.70/23.78 66718(e)[19:MRR:12520.1,66711.0] || tp__o(U) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)),c_2Ebool_2ET)**. % 40.70/23.78 67113[19:Obv:66657.1] || p(U) mem(U,bool)* -> p(c_2Ebool_2EF). % 40.70/23.78 67114(e)[19:MRR:67113.2,30.0] || p(U) mem(U,bool)* -> . % 40.70/23.78 67117(e)[19:MRR:645.2,67114.0] || mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2EF). % 40.70/23.78 67121(e)[19:MRR:16949.1,67114.0] || mem(U,bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 40.70/23.78 67124(e)[19:MRR:12491.1,67114.0] || mem(U,bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2ET)**. % 40.70/23.78 67336[19:Rew:67117.1,38077.3] || mem(U,bool) mem(V,bool) tp__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF)) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF)),V),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)))**. % 40.70/23.78 68215[19:Rew:67121.1,67336.3,67124.1,67336.3,66718.1,67336.3,67117.1,67336.3,67117.1,67336.2] || mem(U,bool)* mem(V,bool)* tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF))* -> equal(c_2Ebool_2ET,c_2Ebool_2EF). % 40.70/23.78 68216[19:Con:68215.1] || mem(U,bool)* tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF))* -> equal(c_2Ebool_2ET,c_2Ebool_2EF). % 40.70/23.78 68217[19:Rew:7031.0,68216.1] || mem(U,bool)* tp__o(fo__c_2Ebool_2ET) -> equal(c_2Ebool_2ET,c_2Ebool_2EF). % 40.70/23.78 68218[19:MRR:68217.1,68217.2,23.0,4308.0] || mem(U,bool)* -> . % 40.70/23.78 68219(e)[19:UnC:68218.0,11223.0] || -> . % 40.70/23.78 68426(e)[18:Spt:68219.0,40605.0,41007.0] || p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc8,bool),skc10),c_2Ebool_2E_7E))* -> . % 40.70/23.78 68427[18:Spt:68219.0,40605.1] || -> mem(skf27(c_2Ebool_2E_7E,bool,U,V),bool)*. % 40.70/23.78 68469[19:Spt:7010.2] || -> mem(skf21(skc7,U,V),skc7)*. % 40.70/23.78 68470(e)[19:UnC:68469.0,66642.0] || -> . % 40.70/23.78 68471[19:Spt:68470.0,7010.0,7010.1] || mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U))*. % 40.70/23.78 68472[19:Res:68471.1,60.0] || mem(skc11,arr(skc8,bool))* -> . % 40.70/23.78 68482(e)[19:MRR:68472.0,37.0] || -> . % 40.70/23.78 68486[16:Spt:68482.0,40664.0,40664.1] || mem(U,skc8) -> p(ap(skc10,U))*. % 40.70/23.78 68504[16:Res:68486.1,299.0] || mem(skf15(skc10,U),skc8)* mem(skc10,arr(skc8,bool)) -> p(ap(c_2Ebool_2E_21(skc8),skc10))*. % 40.70/23.78 68557[16:MRR:68504.1,38.0] || mem(skf15(skc10,U),skc8)* -> p(ap(c_2Ebool_2E_21(skc8),skc10))*. % 40.70/23.78 68558[16:MRR:68557.1,10684.0] || mem(skf15(skc10,U),skc8)* -> . % 40.70/23.78 68559(e)[16:UnC:68558.0,10685.0] || -> . % 40.70/23.78 68560(e)[15:Spt:68559.0,40655.0,40661.0] || p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(skc7,skc8),skc9),skc10))* -> . % 40.70/23.78 68561[15:Spt:68559.0,40655.1] || -> mem(skf27(skc10,skc8,U,V),skc8)*. % 40.70/23.78 68603[16:Spt:7010.2] || -> mem(skf21(skc7,U,V),skc7)*. % 40.70/23.78 68604(e)[16:UnC:68603.0,66642.0] || -> . % 40.70/23.78 68605[16:Spt:68604.0,7010.0,7010.1] || mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U))*. % 40.70/23.78 68606[16:Res:68605.1,60.0] || mem(skc11,arr(skc8,bool))* -> . % 40.70/23.78 68615(e)[16:MRR:68606.0,37.0] || -> . % 40.70/23.78 68619[14:Spt:68615.0,36786.0,39598.0] || equal(ap(c_2Ebool_2E_3F(skc8),skc11),c_2Ebool_2EF)** -> . % 40.70/23.78 68620[14:Spt:68615.0,36786.1] || -> equal(ap(c_2Ebool_2E_3F(skc8),skc11),c_2Ebool_2ET)**. % 40.70/23.78 68635[15:Spt:7010.2] || -> mem(skf21(skc7,U,V),skc7)*. % 40.70/23.78 68636(e)[15:UnC:68635.0,66642.0] || -> . % 40.70/23.78 68637[15:Spt:68636.0,7010.0,7010.1] || mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U))*. % 40.70/23.78 68638[15:Res:68637.1,60.0] || mem(skc11,arr(skc8,bool))* -> . % 40.70/23.78 68647(e)[15:MRR:68638.0,37.0] || -> . % 40.70/23.78 68651(e)[11:Spt:68647.0,11215.2,29342.0] || p(ap(c_2Ebool_2E_3F(skc8),skc10))* -> . % 40.70/23.78 68652[11:Spt:68647.0,11215.0,11215.1] || mem(U,skc8) -> equal(ap(skc11,U),c_2Ebool_2EF)**. % 40.70/23.78 68838[12:Spt:7010.2] || -> mem(skf21(skc7,U,V),skc7)*. % 40.70/23.78 68839(e)[12:UnC:68838.0,66642.0] || -> . % 40.70/23.78 68840[12:Spt:68839.0,7010.0,7010.1] || mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U))*. % 40.70/23.78 68841[12:Res:68840.1,60.0] || mem(skc11,arr(skc8,bool))* -> . % 40.70/23.78 68850(e)[12:MRR:68841.0,37.0] || -> . % 40.70/23.78 68854[7:Spt:68850.0,6153.0,6153.1] || mem(U,arr(bool,bool))* -> equal(c_2Ebool_2E_7E,U). % 40.70/23.78 69086[8:Spt:7010.2] || -> mem(skf21(skc7,U,V),skc7)*. % 40.70/23.78 69087(e)[8:UnC:69086.0,66642.0] || -> . % 40.70/23.78 69088[8:Spt:69087.0,7010.0,7010.1] || mem(U,arr(skc8,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc7,skc8),skc9),U))*. % 40.70/23.78 69089[8:Res:69088.1,60.0] || mem(skc11,arr(skc8,bool))* -> . % 40.70/23.78 69098(e)[8:MRR:69089.0,37.0] || -> . % 40.70/23.78 69102[3:Spt:69098.0,4233.2,4306.0] || equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2ET)** -> . % 40.70/23.78 69103(e)[3:Spt:69098.0,4233.0,4233.1] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)**. % 40.70/23.78 69189[3:Rew:69103.1,4542.2] || tp__o(fo__c_2Ebool_2EF) -> p(c_2Ebool_2EF)* equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF). % 40.70/23.78 69190(e)[3:MRR:69189.0,69189.1,22.0,30.0] || -> equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)**. % 40.70/23.78 69192[3:Rew:69190.0,35.0] || -> equal(inj__o(fo__c_2Ebool_2EF),c_2Ebool_2ET)**. % 40.70/23.78 69491(e)[3:Rew:34.0,69192.0] || -> equal(c_2Ebool_2ET,c_2Ebool_2EF)**. % 40.70/23.78 69492[3:Rew:69491.0,21.0] || -> p(c_2Ebool_2EF)*. % 40.70/23.78 69869(e)[3:MRR:69492.0,30.0] || -> . % 40.70/23.78 % 40.70/23.78 % SZS output end CNFRefutation for /tmp/SPASST_16300_n026.cluster.edu % 40.70/23.78 % 40.70/23.78 Formulae used in the proof : fof_ax_true_p fof_stp_fo_c_2Ebool_2EF fof_stp_fo_c_2Ebool_2ET fof_bool fof_conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT fof_ax_false_p fof_mem_c_2Ebool_2EF fof_mem_c_2Ebool_2ET fof_stp_surj_o fof_stp_eq_fo_c_2Ebool_2EF fof_stp_eq_fo_c_2Ebool_2ET fof_mem_c_2Ebool_2E_7E fof_stp_fo_c_2Ebool_2E_7E fof_stp_inj_mem_o fof_stp_inj_surj_o fof_stp_iso_mem_o fof_ax_neg_p fof_stp_fo_c_2Emin_2E_3D_3D_3E fof_stp_fo_c_2Ebool_2E_2F_5C fof_stp_fo_c_2Ebool_2E_5C_2F fof_arr fof_stp_eq_fo_c_2Ebool_2E_7E fof_mem_c_2Ebool_2E_3F fof_boolext fof_ax_imp_p fof_ax_or_p fof_stp_eq_fo_c_2Emin_2E_3D_3D_3E fof_stp_eq_fo_c_2Ebool_2E_5C_2F fof_ax_all_p fof_ax_ex_p fof_ap_tp fof_funcext fof_conj_thm_2EquantHeuristics_2EGUESS__REWRITES % 58.08/41.24 % 58.08/41.24 SPASS+T ended %------------------------------------------------------------------------------