%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : PHI044_1 : TPTP v8.1.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n021.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 16:49:02 EDT 2022 % Result : Unsatisfiable 4.74s 4.10s % Output : Refutation 4.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PHI044_1 : TPTP v8.1.0. Released v7.5.0. % 0.07/0.13 % Command : spasst-tptp-script %s %d % 0.13/0.34 % Computer : n021.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 : Thu Jun 2 00:48:31 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.47 % Using EUF theory % 4.74/4.10 % 4.74/4.10 % 4.74/4.10 % SZS status Theorem for /tmp/SPASST_27470_n021.cluster.edu % 4.74/4.10 % 4.74/4.10 SPASS V 2.2.22 in combination with yices. % 4.74/4.10 SPASS beiseite: Proof found by SPASS. % 4.74/4.10 Problem: /tmp/SPASST_27470_n021.cluster.edu % 4.74/4.10 SPASS derived 38853 clauses, backtracked 11506 clauses and kept 8754 clauses. % 4.74/4.10 SPASS backtracked 73 times (0 times due to theory inconsistency). % 4.74/4.10 SPASS allocated 50559 KBytes. % 4.74/4.10 SPASS spent 0:00:02.99 on the problem. % 4.74/4.10 0:00:00.00 for the input. % 4.74/4.10 0:00:00.01 for the FLOTTER CNF translation. % 4.74/4.10 0:00:00.23 for inferences. % 4.74/4.10 0:00:00.31 for the backtracking. % 4.74/4.10 0:00:01.75 for the reduction. % 4.74/4.10 0:00:00.51 for interacting with the SMT procedure. % 4.74/4.10 % 4.74/4.10 % 4.74/4.10 % SZS output start CNFRefutation for /tmp/SPASST_27470_n021.cluster.edu % 4.74/4.10 % 4.74/4.10 % Here is a proof with depth 18, length 641 : % 4.74/4.10 1[0:Inp] || -> option(skc17)*. % 4.74/4.10 2[0:Inp] || -> option(skc16)*. % 4.74/4.10 3[0:Inp] || -> option(skc15)*. % 4.74/4.10 4[0:Inp] || -> option_set(skc14)*. % 4.74/4.10 5[0:Inp] || -> option_set(skc13)*. % 4.74/4.10 6[0:Inp] || -> option_set(skc12)*. % 4.74/4.10 7[0:Inp] || -> option_set(skc11)*. % 4.74/4.10 10[0:Inp] || -> permitted_preference(skc17,skc16)*. % 4.74/4.10 11[0:Inp] || -> permitted_preference(skc16,skc17)*. % 4.74/4.10 12[0:Inp] || -> required_preference(skc15,skc17)*. % 4.74/4.10 13[0:Inp] || -> member(skc17,skc14)*. % 4.74/4.10 14[0:Inp] || -> member(skc17,skc12)*. % 4.74/4.10 15[0:Inp] || -> member(skc17,skc11)*. % 4.74/4.10 18[0:Inp] || -> required_preference(skc15,skc16)*. % 4.74/4.10 19[0:Inp] || -> member(skc15,skc13)*. % 4.74/4.10 20[0:Inp] || -> member(skc15,skc11)*. % 4.74/4.10 21[0:Inp] || -> option(skf9(U,V))*. % 4.74/4.10 22[0:Inp] || -> option(skf6(U,V))*. % 4.74/4.10 23[0:Inp] || -> option(skf5(U,V))*. % 4.74/4.10 24[0:Inp] || -> option(skf8(U,V,W))*. % 4.74/4.10 25[0:Inp] || -> option(skf7(U,V,W))*. % 4.74/4.10 26[0:Inp] || option(U) equal(U,skc17) -> member(U,skc14)*. % 4.74/4.10 27[0:Inp] || option(U) member(U,skc14)* -> equal(U,skc17). % 4.74/4.10 28[0:Inp] || option(U) equal(U,skc17) -> member(U,skc12)*. % 4.74/4.10 29[0:Inp] || option(U) equal(U,skc16) -> member(U,skc12)*. % 4.74/4.10 30[0:Inp] || option(U) equal(U,skc17) -> member(U,skc11)*. % 4.74/4.10 31[0:Inp] || option(U) equal(U,skc16) -> member(U,skc11)*. % 4.74/4.10 32[0:Inp] || option(U) equal(U,skc15) -> member(U,skc11)*. % 4.74/4.10 33[0:Inp] || option(U) equal(U,skc15) -> member(U,skc13)*. % 4.74/4.10 34[0:Inp] || option(U) member(U,skc13)* -> equal(U,skc15). % 4.74/4.10 35[0:Inp] || -> member(skf7(U,V,W),W)* SkP0(U,V,W). % 4.74/4.10 36[0:Inp] || equal(skf7(U,V,W),U)** -> SkP0(U,V,W). % 4.74/4.10 37[0:Inp] || equal(skf7(U,V,W),V)** -> SkP0(U,V,W). % 4.74/4.10 38[0:Inp] || option(U) member(U,skc12)* -> equal(U,skc17) equal(U,skc16). % 4.74/4.10 39[0:Inp] || -> SkP1(U,V) member(skf9(U,V),V)* equal(skf9(U,V),U). % 4.74/4.10 40[0:Inp] || option_set(U) option_set(V) subset(U,V) -> weakly_better(V,U)*. % 4.74/4.10 41[0:Inp] || option_set(U) option_set(V) better(U,V) -> weakly_better(U,V)*. % 4.74/4.10 42[0:Inp] || option_set(U) option_set(V) better(U,V) weakly_better(V,U)* -> . % 4.74/4.10 43[0:Inp] || option_set(U) option_set(V) -> subset(U,V) member(skf5(V,U),U)*. % 4.74/4.10 44[0:Inp] || member(skf9(U,V),V)* equal(skf9(U,V),U) -> SkP1(U,V). % 4.74/4.10 45[0:Inp] || option_set(U) option_set(V) member(skf5(V,U),V)* -> subset(U,V). % 4.74/4.10 46[0:Inp] || option(U) member(U,skc11)* -> equal(U,skc17) equal(U,skc16) equal(U,skc15). % 4.74/4.10 47[0:Inp] || option_set(U) option_set(V) weakly_better(U,V)*+ -> weakly_better(V,U)* better(U,V). % 4.74/4.10 48[0:Inp] || option_set(U) option(V) option_set(W) subset(U,W)*+ member(V,U)* -> member(V,W)*. % 4.74/4.10 49[0:Inp] || option_set(U) option_set(V) option_set(W) weakly_better(U,V)*+ weakly_better(V,W)* -> weakly_better(U,W)*. % 4.74/4.10 50[0:Inp] || option_set(U) option(V) option_set(W) option(X) better(U,W)*+ SkP1(V,U)* SkP1(X,W)* -> . % 4.74/4.10 51[0:Inp] || option_set(U) option(V) option_set(W) subset(U,W) member(V,U) better(W,U) -> member(skf8(V,U,W),W)*. % 4.74/4.10 52[0:Inp] || option_set(U) option(V) option_set(W) subset(U,W) member(V,U) better(W,U) required_preference(V,skf8(V,U,W))* -> . % 4.74/4.10 53[0:Inp] || option_set(U) option(V) option_set(W) subset(U,W) member(V,U) better(W,U) member(skf8(V,U,W),U)* -> . % 4.74/4.10 54[0:Inp] || option(U) option(V) option_set(W) option_set(X) permitted_preference(U,V) permitted_preference(V,U) member(U,W) member(U,X) member(V,W) SkP0(V,U,W)*+ -> better(W,X)* member(skf6(U,X),X)*. % 4.74/4.10 55[0:Inp] || option(U) option(V) option_set(W) option_set(X) permitted_preference(U,V) permitted_preference(V,U) member(U,W) member(U,X) member(V,W) equal(skf6(U,X),U)**+ SkP0(V,U,W)* -> better(W,X)*. % 4.74/4.10 84[0:Res:35.0,38.1] || option(skf7(U,V,skc12))* -> SkP0(U,V,skc12) equal(skf7(U,V,skc12),skc17) equal(skf7(U,V,skc12),skc16). % 4.74/4.10 85[0:MRR:84.0,25.0] || -> SkP0(U,V,skc12) equal(skf7(U,V,skc12),skc17)** equal(skf7(U,V,skc12),skc16). % 4.74/4.10 86[0:Res:39.1,34.1] || option(skf9(U,skc13))* -> SkP1(U,skc13) equal(skf9(U,skc13),U) equal(skf9(U,skc13),skc15). % 4.74/4.10 87[0:Res:39.1,38.1] || option(skf9(U,skc12))* -> SkP1(U,skc12) equal(skf9(U,skc12),U) equal(skf9(U,skc12),skc17) equal(skf9(U,skc12),skc16). % 4.74/4.10 88[0:Res:39.1,27.1] || option(skf9(U,skc14))* -> SkP1(U,skc14) equal(skf9(U,skc14),U) equal(skf9(U,skc14),skc17). % 4.74/4.10 89[0:MRR:86.0,21.0] || -> SkP1(U,skc13) equal(skf9(U,skc13),U)** equal(skf9(U,skc13),skc15)**. % 4.74/4.10 90[0:MRR:88.0,21.0] || -> SkP1(U,skc14) equal(skf9(U,skc14),U)** equal(skf9(U,skc14),skc17)**. % 4.74/4.10 91[0:MRR:87.0,21.0] || -> SkP1(U,skc12) equal(skf9(U,skc12),U)** equal(skf9(U,skc12),skc17)** equal(skf9(U,skc12),skc16). % 4.74/4.10 94(e)[0:Fac:89.1,89.2] || -> SkP1(skc15,skc13) equal(skf9(skc15,skc13),skc15)**. % 4.74/4.10 108[1:Spt:94.0] || -> SkP1(skc15,skc13)*. % 4.74/4.10 109[0:Res:40.3,42.3] || option_set(U) option_set(V) subset(U,V)* option_set(U) option_set(V) better(U,V) -> . % 4.74/4.10 112[0:Obv:109.1] || subset(U,V)* option_set(U) option_set(V) better(U,V) -> . % 4.74/4.10 130(e)[0:Fac:90.1,90.2] || -> SkP1(skc17,skc14) equal(skf9(skc17,skc14),skc17)**. % 4.74/4.10 145[0:Res:43.3,34.1] || option_set(skc13) option_set(U) option(skf5(U,skc13))* -> subset(skc13,U) equal(skf5(U,skc13),skc15). % 4.74/4.10 146[0:Res:43.3,38.1] || option_set(skc12) option_set(U) option(skf5(U,skc12))* -> subset(skc12,U) equal(skf5(U,skc12),skc17) equal(skf5(U,skc12),skc16). % 4.74/4.10 147[0:Res:43.3,27.1] || option_set(skc14) option_set(U) option(skf5(U,skc14))* -> subset(skc14,U) equal(skf5(U,skc14),skc17). % 4.74/4.10 148[0:MRR:145.0,145.2,5.0,23.0] || option_set(U) -> subset(skc13,U) equal(skf5(U,skc13),skc15)**. % 4.74/4.10 149[0:MRR:147.0,147.2,4.0,23.0] || option_set(U) -> subset(skc14,U) equal(skf5(U,skc14),skc17)**. % 4.74/4.10 150[0:MRR:146.0,146.2,6.0,23.0] || option_set(U) -> subset(skc12,U) equal(skf5(U,skc12),skc17)** equal(skf5(U,skc12),skc16). % 4.74/4.10 174[0:SpL:148.2,45.2] || option_set(U) option_set(skc13) option_set(U) member(skc15,U) -> subset(skc13,U)* subset(skc13,U)*. % 4.74/4.10 177[0:Res:30.2,45.2] || option(skf5(skc11,U))* equal(skf5(skc11,U),skc17) option_set(U) option_set(skc11) -> subset(U,skc11). % 4.74/4.10 178[0:Res:31.2,45.2] || option(skf5(skc11,U))* equal(skf5(skc11,U),skc16) option_set(U) option_set(skc11) -> subset(U,skc11). % 4.74/4.10 179[0:Res:32.2,45.2] || option(skf5(skc11,U))* equal(skf5(skc11,U),skc15) option_set(U) option_set(skc11) -> subset(U,skc11). % 4.74/4.10 180[0:Res:28.2,45.2] || option(skf5(skc12,U))* equal(skf5(skc12,U),skc17) option_set(U) option_set(skc12) -> subset(U,skc12). % 4.74/4.10 181[0:Res:29.2,45.2] || option(skf5(skc12,U))* equal(skf5(skc12,U),skc16) option_set(U) option_set(skc12) -> subset(U,skc12). % 4.74/4.10 183[0:Res:43.3,45.2] || option_set(U) option_set(U) option_set(U) option_set(U) -> subset(U,U)* subset(U,U)*. % 4.74/4.10 184[0:Obv:183.4] || option_set(U) -> subset(U,U)*. % 4.74/4.10 185[0:Obv:174.4] || option_set(skc13) option_set(U) member(skc15,U) -> subset(skc13,U)*. % 4.74/4.10 186[0:MRR:185.0,5.0] || option_set(U) member(skc15,U) -> subset(skc13,U)*. % 4.74/4.10 190[0:MRR:181.0,181.3,23.0,6.0] || equal(skf5(skc12,U),skc16)** option_set(U) -> subset(U,skc12). % 4.74/4.10 191[0:MRR:180.0,180.3,23.0,6.0] || equal(skf5(skc12,U),skc17)** option_set(U) -> subset(U,skc12). % 4.74/4.10 192[0:MRR:179.0,179.3,23.0,7.0] || equal(skf5(skc11,U),skc15)** option_set(U) -> subset(U,skc11). % 4.74/4.10 193[0:MRR:178.0,178.3,23.0,7.0] || equal(skf5(skc11,U),skc16)** option_set(U) -> subset(U,skc11). % 4.74/4.10 194[0:MRR:177.0,177.3,23.0,7.0] || equal(skf5(skc11,U),skc17)** option_set(U) -> subset(U,skc11). % 4.74/4.10 210[0:Res:30.2,44.0] || option(skf9(U,skc11))* equal(skf9(U,skc11),skc17) equal(skf9(U,skc11),U) -> SkP1(U,skc11). % 4.74/4.10 213[0:Res:28.2,44.0] || option(skf9(U,skc12))* equal(skf9(U,skc12),skc17) equal(skf9(U,skc12),U) -> SkP1(U,skc12). % 4.74/4.10 215[0:Res:26.2,44.0] || option(skf9(U,skc14))* equal(skf9(U,skc14),skc17) equal(skf9(U,skc14),U) -> SkP1(U,skc14). % 4.74/4.10 223[0:MRR:215.0,21.0] || equal(skf9(U,skc14),skc17)**+ equal(skf9(U,skc14),U)** -> SkP1(U,skc14). % 4.74/4.10 225[0:MRR:213.0,21.0] || equal(skf9(U,skc12),skc17)**+ equal(skf9(U,skc12),U)** -> SkP1(U,skc12). % 4.74/4.10 228[0:MRR:210.0,21.0] || equal(skf9(U,skc11),skc17)**+ equal(skf9(U,skc11),U)** -> SkP1(U,skc11). % 4.74/4.10 256[0:Res:35.0,46.1] || option(skf7(U,V,skc11))* -> SkP0(U,V,skc11) equal(skf7(U,V,skc11),skc17) equal(skf7(U,V,skc11),skc16) equal(skf7(U,V,skc11),skc15). % 4.74/4.10 257[0:Res:39.1,46.1] || option(skf9(U,skc11))* -> SkP1(U,skc11) equal(skf9(U,skc11),U) equal(skf9(U,skc11),skc17) equal(skf9(U,skc11),skc16) equal(skf9(U,skc11),skc15). % 4.74/4.10 258[0:Res:43.3,46.1] || option_set(skc11) option_set(U) option(skf5(U,skc11))* -> subset(skc11,U) equal(skf5(U,skc11),skc17) equal(skf5(U,skc11),skc16) equal(skf5(U,skc11),skc15). % 4.74/4.10 259[0:MRR:257.0,21.0] || -> SkP1(U,skc11) equal(skf9(U,skc11),U)** equal(skf9(U,skc11),skc17)** equal(skf9(U,skc11),skc16) equal(skf9(U,skc11),skc15). % 4.74/4.10 260[0:MRR:256.0,25.0] || -> SkP0(U,V,skc11) equal(skf7(U,V,skc11),skc17)** equal(skf7(U,V,skc11),skc16) equal(skf7(U,V,skc11),skc15). % 4.74/4.10 261[0:MRR:258.0,258.2,7.0,23.0] || option_set(U) -> subset(skc11,U) equal(skf5(U,skc11),skc17)** equal(skf5(U,skc11),skc16) equal(skf5(U,skc11),skc15). % 4.74/4.10 263[0:SpL:149.2,191.0] || option_set(skc12) equal(skc17,skc17) option_set(skc14) -> subset(skc14,skc12)* subset(skc14,skc12)*. % 4.74/4.10 266[0:Obv:263.3] || option_set(skc12) option_set(skc14) -> subset(skc14,skc12)*. % 4.74/4.10 267[0:MRR:266.0,266.1,6.0,4.0] || -> subset(skc14,skc12)*. % 4.74/4.10 268[0:Res:40.3,47.2] || option_set(U) option_set(V) subset(U,V) option_set(V) option_set(U) -> weakly_better(U,V)* better(V,U). % 4.74/4.10 270[0:Obv:268.1] || subset(U,V) option_set(V) option_set(U) -> weakly_better(U,V)* better(V,U). % 4.74/4.10 271[0:SpL:148.2,192.0] || option_set(skc11) equal(skc15,skc15) option_set(skc13) -> subset(skc13,skc11)* subset(skc13,skc11)*. % 4.74/4.10 273[0:Obv:271.3] || option_set(skc11) option_set(skc13) -> subset(skc13,skc11)*. % 4.74/4.10 274[0:MRR:273.0,273.1,7.0,5.0] || -> subset(skc13,skc11)*. % 4.74/4.10 277[0:Res:40.3,49.3] || option_set(U) option_set(V) subset(U,V)* option_set(V) option_set(U) option_set(W) weakly_better(U,W)* -> weakly_better(V,W)*. % 4.74/4.10 278[0:Res:41.3,49.3] || option_set(U) option_set(V) better(U,V)* option_set(U) option_set(V) option_set(W) weakly_better(V,W)* -> weakly_better(U,W)*. % 4.74/4.10 279[0:Obv:278.1] || better(U,V)*+ option_set(U) option_set(V) option_set(W) weakly_better(V,W)* -> weakly_better(U,W)*. % 4.74/4.10 280[0:Obv:277.1] || subset(U,V)*+ option_set(V) option_set(U) option_set(W) weakly_better(U,W)* -> weakly_better(V,W)*. % 4.74/4.10 287[0:SpL:149.2,194.0] || option_set(skc11) equal(skc17,skc17) option_set(skc14) -> subset(skc14,skc11)* subset(skc14,skc11)*. % 4.74/4.10 289[0:Obv:287.3] || option_set(skc11) option_set(skc14) -> subset(skc14,skc11)*. % 4.74/4.10 290[0:MRR:289.0,289.1,7.0,4.0] || -> subset(skc14,skc11)*. % 4.74/4.10 378[0:Res:51.6,46.1] || option_set(U) option(V) option_set(skc11) subset(U,skc11) member(V,U) better(skc11,U) option(skf8(V,U,skc11))* -> equal(skf8(V,U,skc11),skc17) equal(skf8(V,U,skc11),skc16) equal(skf8(V,U,skc11),skc15). % 4.74/4.10 379[0:Res:51.6,38.1] || option_set(U) option(V) option_set(skc12) subset(U,skc12) member(V,U) better(skc12,U) option(skf8(V,U,skc12))* -> equal(skf8(V,U,skc12),skc17) equal(skf8(V,U,skc12),skc16). % 4.74/4.10 389[0:MRR:379.2,379.6,6.0,24.0] || option_set(U) option(V) subset(U,skc12) member(V,U) better(skc12,U) -> equal(skf8(V,U,skc12),skc17)** equal(skf8(V,U,skc12),skc16). % 4.74/4.10 390[0:MRR:378.2,378.6,7.0,24.0] || option_set(U) option(V) subset(U,skc11) member(V,U) better(skc11,U) -> equal(skf8(V,U,skc11),skc17)** equal(skf8(V,U,skc11),skc16) equal(skf8(V,U,skc11),skc15). % 4.74/4.10 430[0:Res:33.2,53.6] || option(skf8(U,skc13,V))* equal(skf8(U,skc13,V),skc15) option_set(skc13) option(U) option_set(V) subset(skc13,V) member(U,skc13) better(V,skc13) -> . % 4.74/4.10 446[0:MRR:430.0,430.2,24.0,5.0] || equal(skf8(U,skc13,V),skc15)** option(U) option_set(V) subset(skc13,V) member(U,skc13) better(V,skc13) -> . % 4.74/4.10 519[0:Res:274.0,112.0] || option_set(skc13) option_set(skc11) better(skc13,skc11)* -> . % 4.74/4.10 523[0:MRR:519.0,519.1,5.0,7.0] || better(skc13,skc11)* -> . % 4.74/4.10 618[0:SpL:150.2,45.2] || option_set(U) option_set(skc12) option_set(U) member(skc17,U) -> subset(skc12,U) equal(skf5(U,skc12),skc16)** subset(skc12,U). % 4.74/4.10 637[0:Obv:618.4] || option_set(skc12) option_set(U) member(skc17,U) -> equal(skf5(U,skc12),skc16)** subset(skc12,U). % 4.74/4.10 638[0:MRR:637.0,6.0] || option_set(U) member(skc17,U) -> equal(skf5(U,skc12),skc16)** subset(skc12,U). % 4.74/4.10 673[0:SpL:85.1,37.0] || equal(skc17,U) -> SkP0(V,U,skc12) equal(skf7(V,U,skc12),skc16)** SkP0(V,U,skc12). % 4.74/4.10 676[0:Obv:673.1] || equal(skc17,U) -> equal(skf7(V,U,skc12),skc16)** SkP0(V,U,skc12). % 4.74/4.10 690[0:Res:270.3,49.3] || subset(U,V)* option_set(V) option_set(U) option_set(U) option_set(V) option_set(W) weakly_better(V,W)* -> better(V,U) weakly_better(U,W)*. % 4.74/4.10 693[0:Obv:690.2] || subset(U,V)*+ option_set(U) option_set(V) option_set(W) weakly_better(V,W)* -> better(V,U) weakly_better(U,W)*. % 4.74/4.10 739(e)[0:Fac:91.1,91.2] || -> SkP1(skc17,skc12) equal(skf9(skc17,skc12),skc17)** equal(skf9(skc17,skc12),skc16). % 4.74/4.10 792[0:Res:274.0,280.0] || option_set(skc11) option_set(skc13) option_set(U) weakly_better(skc13,U)* -> weakly_better(skc11,U). % 4.74/4.10 793[0:Res:267.0,280.0] || option_set(skc12) option_set(skc14) option_set(U) weakly_better(skc14,U)* -> weakly_better(skc12,U). % 4.74/4.10 794[0:Res:290.0,280.0] || option_set(skc11) option_set(skc14) option_set(U) weakly_better(skc14,U)* -> weakly_better(skc11,U). % 4.74/4.10 801[0:MRR:792.0,792.1,7.0,5.0] || option_set(U) weakly_better(skc13,U)* -> weakly_better(skc11,U). % 4.74/4.10 802[0:MRR:793.0,793.1,6.0,4.0] || option_set(U) weakly_better(skc14,U)* -> weakly_better(skc12,U). % 4.74/4.10 803[0:MRR:794.0,794.1,7.0,4.0] || option_set(U) weakly_better(skc14,U)* -> weakly_better(skc11,U). % 4.74/4.10 817[0:Res:40.3,801.1] || option_set(U) option_set(skc13) subset(U,skc13) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 818[0:Res:270.3,801.1] || subset(skc13,U) option_set(U) option_set(skc13) option_set(U) -> better(U,skc13) weakly_better(skc11,U)*. % 4.74/4.10 819[0:Res:41.3,801.1] || option_set(skc13) option_set(U) better(skc13,U) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 820[0:Obv:817.0] || option_set(skc13) subset(U,skc13) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 821[0:MRR:820.0,5.0] || subset(U,skc13) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 822[0:Obv:819.1] || option_set(skc13) better(skc13,U) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 823[0:MRR:822.0,5.0] || better(skc13,U) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 824[0:Obv:818.1] || subset(skc13,U) option_set(skc13) option_set(U) -> better(U,skc13) weakly_better(skc11,U)*. % 4.74/4.10 825[0:MRR:824.1,5.0] || subset(skc13,U) option_set(U) -> better(U,skc13) weakly_better(skc11,U)*. % 4.74/4.10 826[0:Res:40.3,802.1] || option_set(U) option_set(skc14) subset(U,skc14) option_set(U) -> weakly_better(skc12,U)*. % 4.74/4.10 827[0:Res:270.3,802.1] || subset(skc14,U) option_set(U) option_set(skc14) option_set(U) -> better(U,skc14) weakly_better(skc12,U)*. % 4.74/4.10 829[0:Obv:826.0] || option_set(skc14) subset(U,skc14) option_set(U) -> weakly_better(skc12,U)*. % 4.74/4.10 830[0:MRR:829.0,4.0] || subset(U,skc14) option_set(U) -> weakly_better(skc12,U)*. % 4.74/4.10 833[0:Obv:827.1] || subset(skc14,U) option_set(skc14) option_set(U) -> better(U,skc14) weakly_better(skc12,U)*. % 4.74/4.10 834[0:MRR:833.1,4.0] || subset(skc14,U) option_set(U) -> better(U,skc14) weakly_better(skc12,U)*. % 4.74/4.10 835[0:Res:40.3,803.1] || option_set(U) option_set(skc14) subset(U,skc14) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 838[0:Obv:835.0] || option_set(skc14) subset(U,skc14) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 839[0:MRR:838.0,4.0] || subset(U,skc14) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 862[0:SpL:261.2,191.0] || option_set(skc12) equal(skc17,skc17) option_set(skc11) -> subset(skc11,skc12) equal(skf5(skc12,skc11),skc16)** equal(skf5(skc12,skc11),skc15) subset(skc11,skc12). % 4.74/4.10 871[0:Obv:862.3] || option_set(skc12) option_set(skc11) -> equal(skf5(skc12,skc11),skc16)** equal(skf5(skc12,skc11),skc15) subset(skc11,skc12). % 4.74/4.10 872(e)[0:MRR:871.0,871.1,6.0,7.0] || -> equal(skf5(skc12,skc11),skc16)** equal(skf5(skc12,skc11),skc15) subset(skc11,skc12). % 4.74/4.10 882[0:Res:821.2,47.2] || subset(U,skc13) option_set(U) option_set(skc11) option_set(U) -> weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 885[0:Obv:882.1] || subset(U,skc13) option_set(skc11) option_set(U) -> weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 886[0:MRR:885.1,7.0] || subset(U,skc13) option_set(U) -> weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 900[0:Res:830.2,47.2] || subset(U,skc14) option_set(U) option_set(skc12) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 905[0:Obv:900.1] || subset(U,skc14) option_set(skc12) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 906[0:MRR:905.1,6.0] || subset(U,skc14) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 925[0:SpL:260.1,37.0] || equal(skc17,U) -> SkP0(V,U,skc11) equal(skf7(V,U,skc11),skc16)** equal(skf7(V,U,skc11),skc15) SkP0(V,U,skc11). % 4.74/4.10 929[0:Obv:925.1] || equal(skc17,U) -> equal(skf7(V,U,skc11),skc16)** equal(skf7(V,U,skc11),skc15) SkP0(V,U,skc11). % 4.74/4.10 932[0:Res:839.2,47.2] || subset(U,skc14) option_set(U) option_set(skc11) option_set(U) -> weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 935[0:Obv:932.1] || subset(U,skc14) option_set(skc11) option_set(U) -> weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 936[0:MRR:935.1,7.0] || subset(U,skc14) option_set(U) -> weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 969[0:EqF:259.2,259.1] || equal(skc17,U)+ -> SkP1(U,skc11) equal(skf9(U,skc11),U)** equal(skf9(U,skc11),skc16)** equal(skf9(U,skc11),skc15). % 4.74/4.10 972(e)[0:Fac:259.1,259.2] || -> SkP1(skc17,skc11) equal(skf9(skc17,skc11),skc17)** equal(skf9(skc17,skc11),skc16) equal(skf9(skc17,skc11),skc15). % 4.74/4.10 1059[2:Spt:872.0] || -> equal(skf5(skc12,skc11),skc16)**. % 4.74/4.10 1066[2:SpL:1059.0,190.0] || equal(skc16,skc16) option_set(skc11) -> subset(skc11,skc12)*. % 4.74/4.10 1068(e)[2:Obv:1066.0] || option_set(skc11) -> subset(skc11,skc12)*. % 4.74/4.10 1069[2:MRR:1068.0,7.0] || -> subset(skc11,skc12)*. % 4.74/4.10 1071(e)[2:Res:1069.0,280.0] || option_set(skc12) option_set(skc11) option_set(U) weakly_better(skc11,U) -> weakly_better(skc12,U)*. % 4.74/4.10 1072(e)[2:Res:1069.0,112.0] || option_set(skc11) option_set(skc12) better(skc11,skc12)* -> . % 4.74/4.10 1074(e)[2:Res:1069.0,48.3] || option_set(skc11) option(U) option_set(skc12) member(U,skc11) -> member(U,skc12)*. % 4.74/4.10 1075[2:MRR:1072.0,1072.1,7.0,6.0] || better(skc11,skc12)* -> . % 4.74/4.10 1076[2:MRR:1071.0,1071.1,6.0,7.0] || option_set(U) weakly_better(skc11,U) -> weakly_better(skc12,U)*. % 4.74/4.10 1077[2:MRR:1074.0,1074.2,7.0,6.0] || option(U) member(U,skc11) -> member(U,skc12)*. % 4.74/4.10 1084[2:Res:1076.2,47.2] || option_set(U) weakly_better(skc11,U)* option_set(skc12) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 1088(e)[2:Obv:1084.0] || weakly_better(skc11,U)* option_set(skc12) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 1089[2:MRR:1088.1,6.0] || weakly_better(skc11,U)*+ option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 1097(e)[2:Res:1077.2,45.2] || option(skf5(skc12,U)) member(skf5(skc12,U),skc11)* option_set(U) option_set(skc12) -> subset(U,skc12). % 4.74/4.10 1101[2:MRR:1097.0,1097.3,23.0,6.0] || member(skf5(skc12,U),skc11)* option_set(U) -> subset(U,skc12). % 4.74/4.10 1156[2:SpL:148.2,1101.0] || option_set(skc12) member(skc15,skc11) option_set(skc13) -> subset(skc13,skc12)* subset(skc13,skc12)*. % 4.74/4.10 1168(e)[2:Obv:1156.3] || option_set(skc12) member(skc15,skc11) option_set(skc13) -> subset(skc13,skc12)*. % 4.74/4.10 1169[2:MRR:1168.0,1168.1,1168.2,6.0,20.0,5.0] || -> subset(skc13,skc12)*. % 4.74/4.10 1174(e)[2:Res:1169.0,280.0] || option_set(skc12) option_set(skc13) option_set(U) weakly_better(skc13,U)* -> weakly_better(skc12,U). % 4.74/4.10 1178(e)[2:Res:1169.0,48.3] || option_set(skc13) option(U) option_set(skc12) member(U,skc13)* -> member(U,skc12). % 4.74/4.10 1179[2:MRR:1174.0,1174.1,6.0,5.0] || option_set(U) weakly_better(skc13,U)* -> weakly_better(skc12,U). % 4.74/4.10 1180[2:MRR:1178.0,1178.2,5.0,6.0] || option(U) member(U,skc13)* -> member(U,skc12). % 4.74/4.10 1185[2:Res:40.3,1179.1] || option_set(U) option_set(skc13) subset(U,skc13) option_set(U) -> weakly_better(skc12,U)*. % 4.74/4.10 1188(e)[2:Obv:1185.0] || option_set(skc13) subset(U,skc13) option_set(U) -> weakly_better(skc12,U)*. % 4.74/4.10 1189[2:MRR:1188.0,5.0] || subset(U,skc13) option_set(U) -> weakly_better(skc12,U)*. % 4.74/4.10 1194(e)[2:Res:19.0,1180.1] || option(skc15) -> member(skc15,skc12)*. % 4.74/4.10 1196[2:Res:33.2,1180.1] || option(U) equal(U,skc15) option(U) -> member(U,skc12)*. % 4.74/4.10 1201[2:MRR:1194.0,3.0] || -> member(skc15,skc12)*. % 4.74/4.10 1202[2:Obv:1196.0] || equal(U,skc15) option(U) -> member(U,skc12)*. % 4.74/4.10 1210(e)[2:Res:1201.0,38.1] || option(skc15)* -> equal(skc17,skc15) equal(skc16,skc15). % 4.74/4.10 1211(e)[2:MRR:1210.0,3.0] || -> equal(skc17,skc15)** equal(skc16,skc15). % 4.74/4.10 1215[3:Spt:1211.0] || -> equal(skc17,skc15)**. % 4.74/4.10 1217[3:Rew:1215.0,12.0] || -> required_preference(skc15,skc15)*. % 4.74/4.10 1218[3:Rew:1215.0,11.0] || -> permitted_preference(skc16,skc15)*. % 4.74/4.10 1219[3:Rew:1215.0,10.0] || -> permitted_preference(skc15,skc16)*. % 4.74/4.10 1310[3:Rew:1215.0,389.5] || option_set(U) option(V) subset(U,skc12) member(V,U) better(skc12,U) -> equal(skf8(V,U,skc12),skc15) equal(skf8(V,U,skc12),skc16)**. % 4.74/4.10 1320[3:Rew:1215.0,676.0] || equal(skc15,U) -> equal(skf7(V,U,skc12),skc16)** SkP0(V,U,skc12). % 4.74/4.10 1489[2:Res:1189.2,47.2] || subset(U,skc13) option_set(U) option_set(skc12) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 1493(e)[2:Obv:1489.1] || subset(U,skc13) option_set(skc12) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 1494[2:MRR:1493.1,6.0] || subset(U,skc13) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 1910[0:Res:825.3,47.2] || subset(skc13,U) option_set(U) option_set(skc11) option_set(U) -> better(U,skc13) weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 1915[0:Obv:1910.1] || subset(skc13,U) option_set(skc11) option_set(U) -> better(U,skc13) weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 1916[0:MRR:1915.1,7.0] || subset(skc13,U) option_set(U) -> better(U,skc13) weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 1925[0:Res:834.3,47.2] || subset(skc14,U) option_set(U) option_set(skc12) option_set(U) -> better(U,skc14) weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 1930[0:Obv:1925.1] || subset(skc14,U) option_set(skc12) option_set(U) -> better(U,skc14) weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 1931[0:MRR:1930.1,6.0] || subset(skc14,U) option_set(U) -> better(U,skc14) weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 1960[0:Res:886.2,801.1] || subset(skc13,skc13) option_set(skc13) option_set(skc11) -> better(skc11,skc13) weakly_better(skc11,skc11)*. % 4.74/4.10 1967[0:MRR:1960.0,1960.1,1960.2,184.1,5.0,7.0] || -> better(skc11,skc13) weakly_better(skc11,skc11)*. % 4.74/4.10 2025[0:Res:906.2,49.3] || subset(U,skc14) option_set(U) option_set(U) option_set(skc12) option_set(V) weakly_better(skc12,V)* -> better(skc12,U) weakly_better(U,V)*. % 4.74/4.10 2029[0:Res:906.2,801.1] || subset(skc13,skc14) option_set(skc13) option_set(skc12) -> better(skc12,skc13) weakly_better(skc11,skc12)*. % 4.74/4.10 2033[0:Res:906.2,802.1] || subset(skc14,skc14) option_set(skc14) option_set(skc12) -> better(skc12,skc14) weakly_better(skc12,skc12)*. % 4.74/4.10 2039(e)[0:MRR:2033.0,2033.1,2033.2,184.1,4.0,6.0] || -> better(skc12,skc14) weakly_better(skc12,skc12)*. % 4.74/4.10 2043[0:Obv:2025.1] || subset(U,skc14) option_set(U) option_set(skc12) option_set(V) weakly_better(skc12,V)* -> better(skc12,U) weakly_better(U,V)*. % 4.74/4.10 2044[0:MRR:2043.2,6.0] || subset(U,skc14)+ option_set(U) option_set(V) weakly_better(skc12,V)* -> better(skc12,U) weakly_better(U,V)*. % 4.74/4.10 2057[3:SpL:1310.6,52.6] || option_set(U) option(V) subset(U,skc12) member(V,U) better(skc12,U) option_set(U) option(V) option_set(skc12) subset(U,skc12) member(V,U) better(skc12,U) required_preference(V,skc16) -> equal(skf8(V,U,skc12),skc15)**. % 4.74/4.10 2071(e)[3:Obv:2057.4] || option_set(U) option(V) option_set(skc12) subset(U,skc12) member(V,U) better(skc12,U) required_preference(V,skc16) -> equal(skf8(V,U,skc12),skc15)**. % 4.74/4.10 2072[3:MRR:2071.2,6.0] || option_set(U) option(V) subset(U,skc12) member(V,U) better(skc12,U) required_preference(V,skc16) -> equal(skf8(V,U,skc12),skc15)**. % 4.74/4.10 2098[0:Res:936.2,49.3] || subset(U,skc14) option_set(U) option_set(U) option_set(skc11) option_set(V) weakly_better(skc11,V)* -> better(skc11,U) weakly_better(U,V)*. % 4.74/4.10 2106[0:Res:936.2,802.1] || subset(skc14,skc14) option_set(skc14) option_set(skc11) -> better(skc11,skc14) weakly_better(skc12,skc11)*. % 4.74/4.10 2111[0:Obv:2098.1] || subset(U,skc14) option_set(U) option_set(skc11) option_set(V) weakly_better(skc11,V)* -> better(skc11,U) weakly_better(U,V)*. % 4.74/4.10 2112[0:MRR:2111.2,7.0] || subset(U,skc14)+ option_set(U) option_set(V) weakly_better(skc11,V)* -> better(skc11,U) weakly_better(U,V)*. % 4.74/4.10 2222[2:Res:825.3,1089.0] || subset(skc13,U) option_set(U) option_set(U) -> better(U,skc13) weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 2248[2:Obv:2222.1] || subset(skc13,U) option_set(U) -> better(U,skc13) weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 2265[3:SpL:1320.1,36.0] || equal(skc15,U) equal(skc16,V) -> SkP0(V,U,skc12)* SkP0(V,U,skc12)*. % 4.74/4.10 2269[3:Obv:2265.2] || equal(skc15,U) equal(skc16,V) -> SkP0(V,U,skc12)*. % 4.74/4.10 2283(e)[3:Res:2269.2,54.9] || equal(skc15,U) equal(skc16,V) option(U) option(V) option_set(skc12) option_set(W) permitted_preference(U,V)* permitted_preference(V,U)* member(U,skc12) member(U,W) member(V,skc12)* -> better(skc12,W) member(skf6(U,W),W)*. % 4.74/4.10 2284[3:MRR:2283.4,2283.8,2283.10,6.0,1202.2,29.2] || equal(skc15,U)+ equal(skc16,V) option(U) option(V) option_set(W) permitted_preference(U,V)* permitted_preference(V,U)* member(U,W) -> better(skc12,W) member(skf6(U,W),W)*. % 4.74/4.10 2325[2:Res:1494.2,1179.1] || subset(skc13,skc13) option_set(skc13) option_set(skc12) -> better(skc12,skc13) weakly_better(skc12,skc12)*. % 4.74/4.10 2326[2:Res:1494.2,801.1] || subset(skc13,skc13) option_set(skc13) option_set(skc12) -> better(skc12,skc13) weakly_better(skc11,skc12)*. % 4.74/4.10 4695[0:Res:186.2,693.0] || option_set(U) member(skc15,U) option_set(skc13) option_set(U) option_set(V) weakly_better(U,V)* -> better(U,skc13) weakly_better(skc13,V)*. % 4.74/4.10 4718[0:Obv:4695.0] || member(skc15,U) option_set(skc13) option_set(U) option_set(V) weakly_better(U,V)* -> better(U,skc13) weakly_better(skc13,V)*. % 4.74/4.10 4719[0:MRR:4718.1,5.0] || member(skc15,U)+ option_set(U) option_set(V) weakly_better(U,V)* -> better(U,skc13) weakly_better(skc13,V)*. % 4.74/4.10 5560(e)[0:Res:20.0,4719.0] || option_set(skc11) option_set(U) weakly_better(skc11,U) -> better(skc11,skc13) weakly_better(skc13,U)*. % 4.74/4.10 5562(e)[2:Res:1201.0,4719.0] || option_set(skc12) option_set(U) weakly_better(skc12,U) -> better(skc12,skc13) weakly_better(skc13,U)*. % 4.74/4.10 7704[0:Res:184.1,2044.0] || option_set(skc14) option_set(skc14) option_set(U) weakly_better(skc12,U) -> better(skc12,skc14) weakly_better(skc14,U)*. % 4.74/4.10 7711[0:Obv:7704.0] || option_set(skc14) option_set(U) weakly_better(skc12,U) -> better(skc12,skc14) weakly_better(skc14,U)*. % 4.74/4.10 7714[0:Res:184.1,2112.0] || option_set(skc14) option_set(skc14) option_set(U) weakly_better(skc11,U) -> better(skc11,skc14) weakly_better(skc14,U)*. % 4.74/4.10 7721[0:Obv:7714.0] || option_set(skc14) option_set(U) weakly_better(skc11,U) -> better(skc11,skc14) weakly_better(skc14,U)*. % 4.74/4.10 9715[3:SpL:2072.6,52.6] || option_set(U) option(V) subset(U,skc12)* member(V,U)* better(skc12,U) required_preference(V,skc16) option_set(U) option(V) option_set(skc12) subset(U,skc12)* member(V,U)* better(skc12,U) required_preference(V,skc15) -> . % 4.74/4.10 9733[3:Obv:9715.4] || required_preference(U,skc16) option_set(V) option(U) option_set(skc12) subset(V,skc12)* member(U,V)* better(skc12,V) required_preference(U,skc15) -> . % 4.74/4.10 9734[3:MRR:9733.3,6.0] || required_preference(U,skc16)+ option_set(V) option(U) subset(V,skc12)* member(U,V)* better(skc12,V) required_preference(U,skc15) -> . % 4.74/4.10 9957[3:Res:18.0,9734.0] || option_set(U) option(skc15) subset(U,skc12)* member(skc15,U) better(skc12,U) required_preference(skc15,skc15) -> . % 4.74/4.10 9958[3:MRR:9957.1,9957.5,3.0,1217.0] || option_set(U) subset(U,skc12)* member(skc15,U) better(skc12,U) -> . % 4.74/4.10 9962[3:Res:1169.0,9958.1] || option_set(skc13) member(skc15,skc13)* better(skc12,skc13) -> . % 4.74/4.10 10123[3:EqR:2284.0] || equal(skc16,U) option(skc15) option(U) option_set(V) permitted_preference(skc15,U)* permitted_preference(U,skc15)* member(skc15,V) -> better(skc12,V) member(skf6(skc15,V),V)*. % 4.74/4.10 10124[3:MRR:10123.1,3.0] || equal(skc16,U)+ option(U) option_set(V) permitted_preference(skc15,U)* permitted_preference(U,skc15)* member(skc15,V) -> better(skc12,V) member(skf6(skc15,V),V)*. % 4.74/4.10 10221[3:EqR:10124.0] || option(skc16) option_set(U) permitted_preference(skc15,skc16) permitted_preference(skc16,skc15) member(skc15,U) -> better(skc12,U) member(skf6(skc15,U),U)*. % 4.74/4.10 10222[3:MRR:10221.0,10221.2,10221.3,2.0,1219.0,1218.0] || option_set(U) member(skc15,U) -> better(skc12,U) member(skf6(skc15,U),U)*. % 4.74/4.10 10233[3:Res:10222.3,34.1] || option_set(skc13) member(skc15,skc13) option(skf6(skc15,skc13))* -> better(skc12,skc13) equal(skf6(skc15,skc13),skc15). % 4.74/4.10 10559[3:MRR:9962.0,9962.1,5.0,19.0] || better(skc12,skc13)* -> . % 4.74/4.10 10577[2:MRR:5562.0,6.0] || option_set(U) weakly_better(skc12,U) -> better(skc12,skc13) weakly_better(skc13,U)*. % 4.74/4.10 10581[0:MRR:5560.0,7.0] || option_set(U) weakly_better(skc11,U) -> better(skc11,skc13) weakly_better(skc13,U)*. % 4.74/4.10 10592[3:MRR:10233.0,10233.1,10233.2,5.0,19.0,22.0] || -> better(skc12,skc13) equal(skf6(skc15,skc13),skc15)**. % 4.74/4.10 10593[3:MRR:10592.0,10559.0] || -> equal(skf6(skc15,skc13),skc15)**. % 4.74/4.10 10738[3:SpL:10593.0,55.9] || option(skc15) option(U) option_set(V) option_set(skc13) permitted_preference(skc15,U) permitted_preference(U,skc15) member(skc15,V) member(skc15,skc13) member(U,V) equal(skc15,skc15) SkP0(U,skc15,V)* -> better(V,skc13). % 4.74/4.10 10739[3:Obv:10738.9] || option(skc15) option(U) option_set(V) option_set(skc13) permitted_preference(skc15,U) permitted_preference(U,skc15) member(skc15,V) member(skc15,skc13) member(U,V) SkP0(U,skc15,V)* -> better(V,skc13). % 4.74/4.10 10740[3:MRR:10739.0,10739.3,10739.7,3.0,5.0,19.0] || option(U) option_set(V) permitted_preference(skc15,U) permitted_preference(U,skc15) member(skc15,V) member(U,V) SkP0(U,skc15,V)* -> better(V,skc13). % 4.74/4.10 14276[3:Res:2269.2,10740.6] || equal(skc15,skc15) equal(skc16,U) option(U) option_set(skc12) permitted_preference(skc15,U) permitted_preference(U,skc15) member(skc15,skc12)* member(U,skc12)* -> better(skc12,skc13). % 4.74/4.10 14281[3:Obv:14276.0] || equal(skc16,U) option(U) option_set(skc12) permitted_preference(skc15,U) permitted_preference(U,skc15) member(skc15,skc12)* member(U,skc12)* -> better(skc12,skc13). % 4.74/4.10 14282[3:MRR:14281.2,14281.5,14281.6,14281.7,6.0,1201.0,29.2,10559.0] || equal(skc16,U)+ option(U) permitted_preference(skc15,U)* permitted_preference(U,skc15)* -> . % 4.74/4.10 14331[3:EqR:14282.0] || option(skc16) permitted_preference(skc15,skc16) permitted_preference(skc16,skc15)* -> . % 4.74/4.10 14332(e)[3:MRR:14331.0,14331.1,14331.2,2.0,1219.0,1218.0] || -> . % 4.74/4.10 14333[3:Spt:14332.0,1211.0,1215.0] || equal(skc17,skc15)** -> . % 4.74/4.10 14334[3:Spt:14332.0,1211.1] || -> equal(skc16,skc15)**. % 4.74/4.10 14338[3:Rew:14334.0,18.0] || -> required_preference(skc15,skc15)*. % 4.74/4.10 14348[3:Rew:14334.0,10.0] || -> permitted_preference(skc17,skc15)*. % 4.74/4.10 14349[3:Rew:14334.0,11.0] || -> permitted_preference(skc15,skc17)*. % 4.74/4.10 14357(e)[3:Rew:14334.0,739.2] || -> SkP1(skc17,skc12) equal(skf9(skc17,skc12),skc17)** equal(skf9(skc17,skc12),skc15). % 4.74/4.10 14360[3:Rew:14334.0,676.1] || equal(skc17,U) -> equal(skf7(V,U,skc12),skc15)** SkP0(V,U,skc12). % 4.74/4.10 14364[3:Rew:14334.0,638.2] || option_set(U) member(skc17,U) -> equal(skf5(U,skc12),skc15)** subset(skc12,U). % 4.74/4.10 14370[0:MRR:2029.1,2029.2,5.0,6.0] || subset(skc13,skc14) -> better(skc12,skc13) weakly_better(skc11,skc12)*. % 4.74/4.10 14373[2:MRR:2325.0,2325.1,2325.2,184.1,5.0,6.0] || -> better(skc12,skc13) weakly_better(skc12,skc12)*. % 4.74/4.10 14374[2:MRR:2326.0,2326.1,2326.2,184.1,5.0,6.0] || -> better(skc12,skc13) weakly_better(skc11,skc12)*. % 4.74/4.10 14380(e)[0:MRR:7711.0,4.0] || option_set(U) weakly_better(skc12,U) -> better(skc12,skc14) weakly_better(skc14,U)*. % 4.74/4.10 14384(e)[0:MRR:2106.0,2106.1,2106.2,184.1,4.0,7.0] || -> better(skc11,skc14) weakly_better(skc12,skc11)*. % 4.74/4.10 14385(e)[0:MRR:7721.0,4.0] || option_set(U) weakly_better(skc11,U) -> better(skc11,skc14) weakly_better(skc14,U)*. % 4.74/4.10 14393[3:Rew:14334.0,972.2] || -> SkP1(skc17,skc11) equal(skf9(skc17,skc11),skc17)** equal(skf9(skc17,skc11),skc15) equal(skf9(skc17,skc11),skc15). % 4.74/4.10 14394(e)[3:Obv:14393.2] || -> SkP1(skc17,skc11) equal(skf9(skc17,skc11),skc17)** equal(skf9(skc17,skc11),skc15). % 4.74/4.10 14405[3:Rew:14334.0,929.1] || equal(skc17,U) -> equal(skf7(V,U,skc11),skc15)** equal(skf7(V,U,skc11),skc15)** SkP0(V,U,skc11). % 4.74/4.10 14406[3:Obv:14405.1] || equal(skc17,U) -> equal(skf7(V,U,skc11),skc15)** SkP0(V,U,skc11). % 4.74/4.10 14424[3:Rew:14334.0,389.6] || option_set(U) option(V) subset(U,skc12) member(V,U) better(skc12,U) -> equal(skf8(V,U,skc12),skc17)** equal(skf8(V,U,skc12),skc15). % 4.74/4.10 14442[3:Rew:14334.0,390.6] || option_set(U) option(V) subset(U,skc11) member(V,U) better(skc11,U) -> equal(skf8(V,U,skc11),skc17)** equal(skf8(V,U,skc11),skc15) equal(skf8(V,U,skc11),skc15). % 4.74/4.10 14443[3:Obv:14442.6] || option_set(U) option(V) subset(U,skc11) member(V,U) better(skc11,U) -> equal(skf8(V,U,skc11),skc17)** equal(skf8(V,U,skc11),skc15). % 4.74/4.10 14454[4:Spt:2039.0] || -> better(skc12,skc14)*. % 4.74/4.10 14457[4:Res:14454.0,50.4] || option_set(skc12) option(U) option_set(skc14) option(V) SkP1(U,skc12)* SkP1(V,skc14)* -> . % 4.74/4.10 14458(e)[4:MRR:14457.0,14457.2,6.0,4.0] || option(U) option(V) SkP1(U,skc12)*+ SkP1(V,skc14)* -> . % 4.74/4.10 14525[5:Spt:130.0] || -> SkP1(skc17,skc14)*. % 4.74/4.10 14883[6:Spt:14357.0] || -> SkP1(skc17,skc12)*. % 4.74/4.10 15032[6:Res:14883.0,14458.2] || option(skc17) option(U) SkP1(U,skc14)* -> . % 4.74/4.10 15033[6:MRR:15032.0,1.0] || option(U) SkP1(U,skc14)* -> . % 4.74/4.10 15035[6:Res:14525.0,15033.1] || option(skc17)* -> . % 4.74/4.10 15036(e)[6:MRR:15035.0,1.0] || -> . % 4.74/4.10 15037[6:Spt:15036.0,14357.0,14883.0] || SkP1(skc17,skc12)* -> . % 4.74/4.10 15038(e)[6:Spt:15036.0,14357.1,14357.2] || -> equal(skf9(skc17,skc12),skc17)** equal(skf9(skc17,skc12),skc15). % 4.74/4.10 15039[7:Spt:15038.0] || -> equal(skf9(skc17,skc12),skc17)**. % 4.74/4.10 15045[7:SpL:15039.0,225.0] || equal(skc17,skc17) equal(skf9(skc17,skc12),skc17)** -> SkP1(skc17,skc12). % 4.74/4.10 15054[7:Obv:15045.0] || equal(skf9(skc17,skc12),skc17)** -> SkP1(skc17,skc12). % 4.74/4.10 15055[7:Rew:15039.0,15054.0] || equal(skc17,skc17) -> SkP1(skc17,skc12)*. % 4.74/4.10 15056[7:Obv:15055.0] || -> SkP1(skc17,skc12)*. % 4.74/4.10 15057(e)[7:MRR:15056.0,15037.0] || -> . % 4.74/4.10 15058[7:Spt:15057.0,15038.0,15039.0] || equal(skf9(skc17,skc12),skc17)** -> . % 4.74/4.10 15059[7:Spt:15057.0,15038.1] || -> equal(skf9(skc17,skc12),skc15)**. % 4.74/4.10 15069[8:Spt:14384.0] || -> better(skc11,skc14)*. % 4.74/4.10 15072[8:Res:15069.0,50.4] || option_set(skc11) option(U) option_set(skc14) option(V) SkP1(U,skc11)* SkP1(V,skc14)* -> . % 4.74/4.10 15075(e)[8:MRR:15072.0,15072.2,7.0,4.0] || option(U) option(V) SkP1(U,skc11)*+ SkP1(V,skc14)* -> . % 4.74/4.10 15427[9:Spt:14394.0] || -> SkP1(skc17,skc11)*. % 4.74/4.10 15593[9:Res:15427.0,15075.2] || option(skc17) option(U) SkP1(U,skc14)* -> . % 4.74/4.10 15594[9:MRR:15593.0,1.0] || option(U) SkP1(U,skc14)* -> . % 4.74/4.10 15596[9:Res:14525.0,15594.1] || option(skc17)* -> . % 4.74/4.10 15597(e)[9:MRR:15596.0,1.0] || -> . % 4.74/4.10 15598[9:Spt:15597.0,14394.0,15427.0] || SkP1(skc17,skc11)* -> . % 4.74/4.10 15599(e)[9:Spt:15597.0,14394.1,14394.2] || -> equal(skf9(skc17,skc11),skc17)** equal(skf9(skc17,skc11),skc15). % 4.74/4.10 15600[10:Spt:15599.0] || -> equal(skf9(skc17,skc11),skc17)**. % 4.74/4.10 15606[10:SpL:15600.0,228.0] || equal(skc17,skc17) equal(skf9(skc17,skc11),skc17)** -> SkP1(skc17,skc11). % 4.74/4.10 15611[10:Obv:15606.0] || equal(skf9(skc17,skc11),skc17)** -> SkP1(skc17,skc11). % 4.74/4.10 15612[10:Rew:15600.0,15611.0] || equal(skc17,skc17) -> SkP1(skc17,skc11)*. % 4.74/4.10 15613[10:Obv:15612.0] || -> SkP1(skc17,skc11)*. % 4.74/4.10 15614(e)[10:MRR:15613.0,15598.0] || -> . % 4.74/4.10 15615[10:Spt:15614.0,15599.0,15600.0] || equal(skf9(skc17,skc11),skc17)** -> . % 4.74/4.10 15616[10:Spt:15614.0,15599.1] || -> equal(skf9(skc17,skc11),skc15)**. % 4.74/4.10 15657[11:Spt:14373.0] || -> better(skc12,skc13)*. % 4.74/4.10 16036[3:SpL:14424.5,52.6] || option_set(U) option(V) subset(U,skc12) member(V,U) better(skc12,U) option_set(U) option(V) option_set(skc12) subset(U,skc12) member(V,U) better(skc12,U) required_preference(V,skc17) -> equal(skf8(V,U,skc12),skc15)**. % 4.74/4.10 16053[3:Obv:16036.4] || option_set(U) option(V) option_set(skc12) subset(U,skc12) member(V,U) better(skc12,U) required_preference(V,skc17) -> equal(skf8(V,U,skc12),skc15)**. % 4.74/4.10 16054[3:MRR:16053.2,6.0] || option_set(U) option(V) subset(U,skc12) member(V,U) better(skc12,U) required_preference(V,skc17) -> equal(skf8(V,U,skc12),skc15)**. % 4.74/4.10 16088[3:SpL:14443.5,52.6] || option_set(U) option(V) subset(U,skc11) member(V,U) better(skc11,U) option_set(U) option(V) option_set(skc11) subset(U,skc11) member(V,U) better(skc11,U) required_preference(V,skc17) -> equal(skf8(V,U,skc11),skc15)**. % 4.74/4.10 16105[3:Obv:16088.4] || option_set(U) option(V) option_set(skc11) subset(U,skc11) member(V,U) better(skc11,U) required_preference(V,skc17) -> equal(skf8(V,U,skc11),skc15)**. % 4.74/4.10 16106[3:MRR:16105.2,7.0] || option_set(U) option(V) subset(U,skc11) member(V,U) better(skc11,U) required_preference(V,skc17) -> equal(skf8(V,U,skc11),skc15)**. % 4.74/4.10 16130[3:SpL:14360.1,36.0] || equal(skc17,U) equal(skc15,V) -> SkP0(V,U,skc12)* SkP0(V,U,skc12)*. % 4.74/4.10 16134[3:Obv:16130.2] || equal(skc17,U) equal(skc15,V) -> SkP0(V,U,skc12)*. % 4.74/4.10 16151[3:Res:16134.2,54.9] || equal(skc17,U) equal(skc15,V) option(U) option(V) option_set(skc12) option_set(W) permitted_preference(U,V)* permitted_preference(V,U)* member(U,skc12) member(U,W) member(V,skc12)* -> better(skc12,W) member(skf6(U,W),W)*. % 4.74/4.10 16152[3:MRR:16151.4,16151.8,16151.10,6.0,28.2,1202.2] || equal(skc17,U)+ equal(skc15,V) option(U) option(V) option_set(W) permitted_preference(U,V)* permitted_preference(V,U)* member(U,W) -> better(skc12,W) member(skf6(U,W),W)*. % 4.74/4.10 16177[3:SpL:14406.1,36.0] || equal(skc17,U) equal(skc15,V) -> SkP0(V,U,skc11)* SkP0(V,U,skc11)*. % 4.74/4.10 16180[3:Obv:16177.2] || equal(skc17,U) equal(skc15,V) -> SkP0(V,U,skc11)*. % 4.74/4.10 16247[3:SpL:14364.2,192.0] || option_set(skc11) member(skc17,skc11) equal(skc15,skc15) option_set(skc12) -> subset(skc12,skc11)* subset(skc12,skc11)*. % 4.74/4.10 16256[3:Obv:16247.4] || option_set(skc11) member(skc17,skc11) option_set(skc12) -> subset(skc12,skc11)*. % 4.74/4.10 16842[3:SpL:16054.6,52.6] || option_set(U) option(V) subset(U,skc12)* member(V,U)* better(skc12,U) required_preference(V,skc17) option_set(U) option(V) option_set(skc12) subset(U,skc12)* member(V,U)* better(skc12,U) required_preference(V,skc15) -> . % 4.74/4.10 16846[3:SpL:16054.6,446.0] || option_set(skc13) option(U) subset(skc13,skc12)* member(U,skc13)* better(skc12,skc13) required_preference(U,skc17) equal(skc15,skc15) option(U) option_set(skc12) subset(skc13,skc12)* member(U,skc13)* better(skc12,skc13) -> . % 4.74/4.10 16853(e)[3:Obv:16846.6] || option_set(skc13) required_preference(U,skc17) option(U) option_set(skc12) subset(skc13,skc12)* member(U,skc13)* better(skc12,skc13) -> . % 4.74/4.10 16854[11:MRR:16853.0,16853.3,16853.4,16853.6,5.0,6.0,1169.0,15657.0] || required_preference(U,skc17) option(U) member(U,skc13)* -> . % 4.74/4.10 16859[3:Obv:16842.4] || required_preference(U,skc17) option_set(V) option(U) option_set(skc12) subset(V,skc12)* member(U,V)* better(skc12,V) required_preference(U,skc15) -> . % 4.74/4.10 16860[3:MRR:16859.3,6.0] || required_preference(U,skc17)+ option_set(V) option(U) subset(V,skc12)* member(U,V)* better(skc12,V) required_preference(U,skc15) -> . % 4.74/4.10 16864[11:Res:19.0,16854.2] || required_preference(skc15,skc17)* option(skc15) -> . % 4.74/4.10 16870(e)[11:MRR:16864.0,16864.1,12.0,3.0] || -> . % 4.74/4.10 16896[11:Spt:16870.0,14373.0,15657.0] || better(skc12,skc13)* -> . % 4.74/4.10 16897[11:Spt:16870.0,14373.1] || -> weakly_better(skc12,skc12)*. % 4.74/4.10 16898[11:MRR:14374.0,16896.0] || -> weakly_better(skc11,skc12)*. % 4.74/4.10 16902[3:MRR:16256.0,16256.1,16256.2,7.0,15.0,6.0] || -> subset(skc12,skc11)*. % 4.74/4.10 16903[11:MRR:10577.2,16896.0] || option_set(U) weakly_better(skc12,U) -> weakly_better(skc13,U)*. % 4.74/4.10 16914[11:Res:16898.0,47.2] || option_set(skc11) option_set(skc12) -> weakly_better(skc12,skc11)* better(skc11,skc12). % 4.74/4.10 16918[11:MRR:16914.0,16914.1,16914.3,7.0,6.0,1075.0] || -> weakly_better(skc12,skc11)*. % 4.74/4.10 16921[3:Res:16902.0,112.0] || option_set(skc12) option_set(skc11) better(skc12,skc11)* -> . % 4.74/4.10 16931[12:Spt:1967.0] || -> better(skc11,skc13)*. % 4.74/4.10 17129[11:Res:16903.2,42.3] || option_set(U) weakly_better(skc12,U)* option_set(U) option_set(skc13) better(U,skc13) -> . % 4.74/4.10 17131[11:Res:16903.2,47.2] || option_set(U) weakly_better(skc12,U)* option_set(skc13) option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 17135[11:Obv:17129.0] || weakly_better(skc12,U)* option_set(U) option_set(skc13) better(U,skc13) -> . % 4.74/4.10 17136[11:MRR:17135.2,5.0] || weakly_better(skc12,U)* option_set(U) better(U,skc13) -> . % 4.74/4.10 17137[11:Obv:17131.0] || weakly_better(skc12,U)* option_set(skc13) option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 17138[11:MRR:17137.1,5.0] || weakly_better(skc12,U)*+ option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 17267(e)[11:Res:16918.0,17136.0] || option_set(skc11) better(skc11,skc13)* -> . % 4.74/4.10 17268(e)[12:MRR:17267.0,17267.1,7.0,16931.0] || -> . % 4.74/4.10 17297[12:Spt:17268.0,1967.0,16931.0] || better(skc11,skc13)* -> . % 4.74/4.10 17298(e)[12:Spt:17268.0,1967.1] || -> weakly_better(skc11,skc11)*. % 4.74/4.10 17520[3:SpL:16106.6,52.6] || option_set(U) option(V) subset(U,skc11)* member(V,U)* better(skc11,U) required_preference(V,skc17) option_set(U) option(V) option_set(skc11) subset(U,skc11)* member(V,U)* better(skc11,U) required_preference(V,skc15) -> . % 4.74/4.10 17536[3:Obv:17520.4] || required_preference(U,skc17) option_set(V) option(U) option_set(skc11) subset(V,skc11)* member(U,V)* better(skc11,V) required_preference(U,skc15) -> . % 4.74/4.10 17537[3:MRR:17536.3,7.0] || required_preference(U,skc17)+ option_set(V) option(U) subset(V,skc11)* member(U,V)* better(skc11,V) required_preference(U,skc15) -> . % 4.74/4.10 17656[11:Res:830.2,17138.0] || subset(U,skc14) option_set(U) option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 17664[11:Obv:17656.1] || subset(U,skc14) option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 17724[3:Res:12.0,16860.0] || option_set(U) option(skc15) subset(U,skc12)* member(skc15,U) better(skc12,U) required_preference(skc15,skc15) -> . % 4.74/4.10 17725[3:MRR:17724.1,17724.5,3.0,14338.0] || option_set(U) subset(U,skc12)* member(skc15,U) better(skc12,U) -> . % 4.74/4.10 17918[3:Res:12.0,17537.0] || option_set(U) option(skc15) subset(U,skc11)* member(skc15,U) better(skc11,U) required_preference(skc15,skc15) -> . % 4.74/4.10 17919[3:MRR:17918.1,17918.5,3.0,14338.0] || option_set(U) subset(U,skc11)* member(skc15,U) better(skc11,U) -> . % 4.74/4.10 17921[11:Res:17664.2,49.3] || subset(U,skc14) option_set(U) option_set(U) option_set(skc13) option_set(V) weakly_better(skc13,V)* -> better(skc13,U) weakly_better(U,V)*. % 4.74/4.10 17939[11:Obv:17921.1] || subset(U,skc14) option_set(U) option_set(skc13) option_set(V) weakly_better(skc13,V)* -> better(skc13,U) weakly_better(U,V)*. % 4.74/4.10 17940[11:MRR:17939.2,5.0] || subset(U,skc14)+ option_set(U) option_set(V) weakly_better(skc13,V)* -> better(skc13,U) weakly_better(U,V)*. % 4.74/4.10 18201[3:Res:1169.0,17725.1] || option_set(skc13) member(skc15,skc13)* better(skc12,skc13) -> . % 4.74/4.10 18242[3:Res:274.0,17919.1] || option_set(skc13) member(skc15,skc13)* better(skc11,skc13) -> . % 4.74/4.10 18998[3:EqR:16152.0] || equal(skc15,U) option(skc17) option(U) option_set(V) permitted_preference(skc17,U)* permitted_preference(U,skc17)* member(skc17,V) -> better(skc12,V) member(skf6(skc17,V),V)*. % 4.74/4.10 18999[3:MRR:18998.1,1.0] || equal(skc15,U)+ option(U) option_set(V) permitted_preference(skc17,U)* permitted_preference(U,skc17)* member(skc17,V) -> better(skc12,V) member(skf6(skc17,V),V)*. % 4.74/4.10 19074[11:Res:184.1,17940.0] || option_set(skc14) option_set(skc14) option_set(U) weakly_better(skc13,U) -> better(skc13,skc14) weakly_better(skc14,U)*. % 4.74/4.10 19079[11:Obv:19074.0] || option_set(skc14) option_set(U) weakly_better(skc13,U) -> better(skc13,skc14) weakly_better(skc14,U)*. % 4.74/4.10 19080(e)[11:MRR:19079.0,4.0] || option_set(U) weakly_better(skc13,U) -> better(skc13,skc14) weakly_better(skc14,U)*. % 4.74/4.10 19082[13:Spt:19080.2] || -> better(skc13,skc14)*. % 4.74/4.10 19085[13:Res:19082.0,50.4] || option_set(skc13) option(U) option_set(skc14) option(V) SkP1(U,skc13)* SkP1(V,skc14)* -> . % 4.74/4.10 19094[13:MRR:19085.0,19085.2,5.0,4.0] || option(U) option(V) SkP1(U,skc13)*+ SkP1(V,skc14)* -> . % 4.74/4.10 19098[13:Res:108.0,19094.2] || option(skc15) option(U) SkP1(U,skc14)* -> . % 4.74/4.10 19099[13:MRR:19098.0,3.0] || option(U) SkP1(U,skc14)* -> . % 4.74/4.10 19101[13:Res:14525.0,19099.1] || option(skc17)* -> . % 4.74/4.10 19102(e)[13:MRR:19101.0,1.0] || -> . % 4.74/4.10 19104[13:Spt:19102.0,19080.2,19082.0] || better(skc13,skc14)* -> . % 4.74/4.10 19105[13:Spt:19102.0,19080.0,19080.1,19080.3] || option_set(U) weakly_better(skc13,U) -> weakly_better(skc14,U)*. % 4.74/4.10 19109[13:Res:19105.2,42.3] || option_set(U) weakly_better(skc13,U)* option_set(U) option_set(skc14) better(U,skc14) -> . % 4.74/4.10 19117[13:Obv:19109.0] || weakly_better(skc13,U)* option_set(U) option_set(skc14) better(U,skc14) -> . % 4.74/4.10 19118[13:MRR:19117.2,4.0] || weakly_better(skc13,U)* option_set(U) better(U,skc14) -> . % 4.74/4.10 19356[13:Res:1494.2,19118.0] || subset(skc13,skc13)* option_set(skc13) option_set(skc12) better(skc12,skc14) -> better(skc12,skc13). % 4.74/4.10 19399(e)[13:MRR:19356.0,19356.1,19356.2,19356.3,19356.4,184.1,5.0,6.0,14454.0,16896.0] || -> . % 4.74/4.10 19429[8:Spt:19399.0,14384.0,15069.0] || better(skc11,skc14)* -> . % 4.74/4.10 19430[8:Spt:19399.0,14384.1] || -> weakly_better(skc12,skc11)*. % 4.74/4.10 19432[3:MRR:16921.0,16921.1,6.0,7.0] || better(skc12,skc11)* -> . % 4.74/4.10 19434[3:MRR:18242.0,18242.1,5.0,19.0] || better(skc11,skc13)* -> . % 4.74/4.10 19435[3:MRR:18201.0,18201.1,5.0,19.0] || better(skc12,skc13)* -> . % 4.74/4.10 19441[8:MRR:14385.2,19429.0] || option_set(U) weakly_better(skc11,U) -> weakly_better(skc14,U)*. % 4.74/4.10 19604[8:Res:19441.2,42.3] || option_set(U) weakly_better(skc11,U)* option_set(U) option_set(skc14) better(U,skc14) -> . % 4.74/4.10 19610[8:Obv:19604.0] || weakly_better(skc11,U)* option_set(U) option_set(skc14) better(U,skc14) -> . % 4.74/4.10 19611[8:MRR:19610.2,4.0] || weakly_better(skc11,U)* option_set(U) better(U,skc14) -> . % 4.74/4.10 19767[8:Res:2248.3,19611.0] || subset(skc13,skc11)* option_set(skc11) option_set(skc12) better(skc12,skc14) -> better(skc11,skc13) better(skc12,skc11). % 4.74/4.10 19808(e)[8:MRR:19767.0,19767.1,19767.2,19767.3,19767.4,19767.5,274.0,7.0,6.0,14454.0,19434.0,19432.0] || -> . % 4.74/4.10 19812(e)[5:Spt:19808.0,130.0,14525.0] || SkP1(skc17,skc14)* -> . % 4.74/4.10 19813[5:Spt:19808.0,130.1] || -> equal(skf9(skc17,skc14),skc17)**. % 4.74/4.10 19823[5:SpL:19813.0,223.0] || equal(skc17,skc17) equal(skf9(skc17,skc14),skc17)** -> SkP1(skc17,skc14). % 4.74/4.10 19828[5:Obv:19823.0] || equal(skf9(skc17,skc14),skc17)** -> SkP1(skc17,skc14). % 4.74/4.10 19829[5:Rew:19813.0,19828.0] || equal(skc17,skc17) -> SkP1(skc17,skc14)*. % 4.74/4.10 19830[5:Obv:19829.0] || -> SkP1(skc17,skc14)*. % 4.74/4.10 19831(e)[5:MRR:19830.0,19812.0] || -> . % 4.74/4.10 19832[4:Spt:19831.0,2039.0,14454.0] || better(skc12,skc14)* -> . % 4.74/4.10 19833(e)[4:Spt:19831.0,2039.1] || -> weakly_better(skc12,skc12)*. % 4.74/4.10 19835[4:MRR:14380.2,19832.0] || option_set(U) weakly_better(skc12,U) -> weakly_better(skc14,U)*. % 4.74/4.10 19931[5:Spt:14385.2] || -> better(skc11,skc14)*. % 4.74/4.10 19962[4:Res:19835.2,42.3] || option_set(U) weakly_better(skc12,U)* option_set(U) option_set(skc14) better(U,skc14) -> . % 4.74/4.10 19968[4:Obv:19962.0] || weakly_better(skc12,U)* option_set(U) option_set(skc14) better(U,skc14) -> . % 4.74/4.10 19969[4:MRR:19968.2,4.0] || weakly_better(skc12,U)* option_set(U) better(U,skc14) -> . % 4.74/4.10 20092(e)[4:Res:1916.3,19969.0] || subset(skc13,skc12)* option_set(skc12) option_set(skc11) better(skc11,skc14) -> better(skc12,skc13) better(skc11,skc12). % 4.74/4.10 20139(e)[5:MRR:20092.0,20092.1,20092.2,20092.3,20092.4,20092.5,1169.0,6.0,7.0,19931.0,19435.0,1075.0] || -> . % 4.74/4.10 20142[5:Spt:20139.0,14385.2,19931.0] || better(skc11,skc14)* -> . % 4.74/4.10 20143[5:Spt:20139.0,14385.0,14385.1,14385.3] || option_set(U) weakly_better(skc11,U) -> weakly_better(skc14,U)*. % 4.74/4.10 22428[3:EqR:18999.0] || option(skc15) option_set(U) permitted_preference(skc17,skc15) permitted_preference(skc15,skc17) member(skc17,U) -> better(skc12,U) member(skf6(skc17,U),U)*. % 4.74/4.10 22429[3:MRR:22428.0,22428.2,22428.3,3.0,14348.0,14349.0] || option_set(U) member(skc17,U) -> better(skc12,U) member(skf6(skc17,U),U)*. % 4.74/4.10 22446[3:Res:22429.3,27.1] || option_set(skc14) member(skc17,skc14) option(skf6(skc17,skc14))* -> better(skc12,skc14) equal(skf6(skc17,skc14),skc17). % 4.74/4.10 22451[4:MRR:22446.0,22446.1,22446.2,22446.3,4.0,13.0,22.0,19832.0] || -> equal(skf6(skc17,skc14),skc17)**. % 4.74/4.10 22480[4:SpL:22451.0,55.9] || option(skc17) option(U) option_set(V) option_set(skc14) permitted_preference(skc17,U) permitted_preference(U,skc17) member(skc17,V) member(skc17,skc14) member(U,V) equal(skc17,skc17) SkP0(U,skc17,V)* -> better(V,skc14). % 4.74/4.10 22481[4:Obv:22480.9] || option(skc17) option(U) option_set(V) option_set(skc14) permitted_preference(skc17,U) permitted_preference(U,skc17) member(skc17,V) member(skc17,skc14) member(U,V) SkP0(U,skc17,V)* -> better(V,skc14). % 4.74/4.10 22482[4:MRR:22481.0,22481.3,22481.7,1.0,4.0,13.0] || option(U) option_set(V) permitted_preference(skc17,U) permitted_preference(U,skc17) member(skc17,V) member(U,V) SkP0(U,skc17,V)* -> better(V,skc14). % 4.74/4.10 24284[4:Res:16180.2,22482.6] || equal(skc17,skc17) equal(skc15,U) option(U) option_set(skc11) permitted_preference(skc17,U) permitted_preference(U,skc17) member(skc17,skc11)* member(U,skc11)* -> better(skc11,skc14). % 4.74/4.10 24290[4:Obv:24284.0] || equal(skc15,U) option(U) option_set(skc11) permitted_preference(skc17,U) permitted_preference(U,skc17) member(skc17,skc11)* member(U,skc11)* -> better(skc11,skc14). % 4.74/4.10 24291[5:MRR:24290.2,24290.5,24290.6,24290.7,7.0,15.0,32.2,20142.0] || equal(skc15,U)+ option(U) permitted_preference(skc17,U)* permitted_preference(U,skc17)* -> . % 4.74/4.10 24325[5:EqR:24291.0] || option(skc15) permitted_preference(skc17,skc15)* permitted_preference(skc15,skc17) -> . % 4.74/4.10 24326(e)[5:MRR:24325.0,24325.1,24325.2,3.0,14348.0,14349.0] || -> . % 4.74/4.10 24327[2:Spt:24326.0,872.0,1059.0] || equal(skf5(skc12,skc11),skc16)** -> . % 4.74/4.10 24328(e)[2:Spt:24326.0,872.1,872.2] || -> equal(skf5(skc12,skc11),skc15)** subset(skc11,skc12). % 4.74/4.10 24381[3:Spt:2039.0] || -> better(skc12,skc14)*. % 4.74/4.10 24384[3:Res:24381.0,50.4] || option_set(skc12) option(U) option_set(skc14) option(V) SkP1(U,skc12)* SkP1(V,skc14)* -> . % 4.74/4.10 24385(e)[3:MRR:24384.0,24384.2,6.0,4.0] || option(U) option(V) SkP1(U,skc12)*+ SkP1(V,skc14)* -> . % 4.74/4.10 24478[4:Spt:130.0] || -> SkP1(skc17,skc14)*. % 4.74/4.10 24849[5:Spt:739.0] || -> SkP1(skc17,skc12)*. % 4.74/4.10 25052[5:Res:24849.0,24385.2] || option(skc17) option(U) SkP1(U,skc14)* -> . % 4.74/4.10 25053[5:MRR:25052.0,1.0] || option(U) SkP1(U,skc14)* -> . % 4.74/4.10 25055[5:Res:24478.0,25053.1] || option(skc17)* -> . % 4.74/4.10 25056(e)[5:MRR:25055.0,1.0] || -> . % 4.74/4.10 25057[5:Spt:25056.0,739.0,24849.0] || SkP1(skc17,skc12)* -> . % 4.74/4.10 25058(e)[5:Spt:25056.0,739.1,739.2] || -> equal(skf9(skc17,skc12),skc17)** equal(skf9(skc17,skc12),skc16). % 4.74/4.10 25059[6:Spt:25058.0] || -> equal(skf9(skc17,skc12),skc17)**. % 4.74/4.10 25064[6:SpL:25059.0,225.0] || equal(skc17,skc17) equal(skf9(skc17,skc12),skc17)** -> SkP1(skc17,skc12). % 4.74/4.10 25070[6:Obv:25064.0] || equal(skf9(skc17,skc12),skc17)** -> SkP1(skc17,skc12). % 4.74/4.10 25071[6:Rew:25059.0,25070.0] || equal(skc17,skc17) -> SkP1(skc17,skc12)*. % 4.74/4.10 25072[6:Obv:25071.0] || -> SkP1(skc17,skc12)*. % 4.74/4.10 25073(e)[6:MRR:25072.0,25057.0] || -> . % 4.74/4.10 25078[6:Spt:25073.0,25058.0,25059.0] || equal(skf9(skc17,skc12),skc17)** -> . % 4.74/4.10 25079[6:Spt:25073.0,25058.1] || -> equal(skf9(skc17,skc12),skc16)**. % 4.74/4.10 25091[7:Spt:1967.0] || -> better(skc11,skc13)*. % 4.74/4.10 25397[0:SpL:390.5,52.6] || option_set(U) option(V) subset(U,skc11) member(V,U) better(skc11,U) option_set(U) option(V) option_set(skc11) subset(U,skc11) member(V,U) better(skc11,U) required_preference(V,skc17) -> equal(skf8(V,U,skc11),skc16)** equal(skf8(V,U,skc11),skc15). % 4.74/4.10 25414[0:Obv:25397.4] || option_set(U) option(V) option_set(skc11) subset(U,skc11) member(V,U) better(skc11,U) required_preference(V,skc17) -> equal(skf8(V,U,skc11),skc16)** equal(skf8(V,U,skc11),skc15). % 4.74/4.10 25415[0:MRR:25414.2,7.0] || option_set(U) option(V) subset(U,skc11) member(V,U) better(skc11,U) required_preference(V,skc17) -> equal(skf8(V,U,skc11),skc16)** equal(skf8(V,U,skc11),skc15). % 4.74/4.10 25656[0:SpL:676.1,36.0] || equal(skc17,U) equal(skc16,V) -> SkP0(V,U,skc12)* SkP0(V,U,skc12)*. % 4.74/4.10 25660[0:Obv:25656.2] || equal(skc17,U) equal(skc16,V) -> SkP0(V,U,skc12)*. % 4.74/4.10 25705[0:Res:25660.2,54.9] || equal(skc17,U) equal(skc16,V) option(U) option(V) option_set(skc12) option_set(W) permitted_preference(U,V)* permitted_preference(V,U)* member(U,skc12) member(U,W) member(V,skc12)* -> better(skc12,W) member(skf6(U,W),W)*. % 4.74/4.10 25706(e)[0:MRR:25705.4,25705.8,25705.10,6.0,28.2,29.2] || equal(skc17,U) equal(skc16,V) option(U) option(V) option_set(W) permitted_preference(U,V)* permitted_preference(V,U)* member(U,W) -> better(skc12,W) member(skf6(U,W),W)*. % 4.74/4.10 25776[0:SpL:638.2,193.0] || option_set(skc11) member(skc17,skc11) equal(skc16,skc16) option_set(skc12) -> subset(skc12,skc11)* subset(skc12,skc11)*. % 4.74/4.10 25782[0:Obv:25776.4] || option_set(skc11) member(skc17,skc11) option_set(skc12) -> subset(skc12,skc11)*. % 4.74/4.10 26062[0:MRR:25782.0,25782.1,25782.2,7.0,15.0,6.0] || -> subset(skc12,skc11)*. % 4.74/4.10 26095[0:Res:26062.0,693.0] || option_set(skc12) option_set(skc11) option_set(U) weakly_better(skc11,U) -> better(skc11,skc12) weakly_better(skc12,U)*. % 4.74/4.10 26096[0:Res:26062.0,280.0] || option_set(skc11) option_set(skc12) option_set(U) weakly_better(skc12,U)* -> weakly_better(skc11,U). % 4.74/4.10 26097[0:Res:26062.0,112.0] || option_set(skc12) option_set(skc11) better(skc12,skc11)* -> . % 4.74/4.10 26651[0:MRR:26097.0,26097.1,6.0,7.0] || better(skc12,skc11)* -> . % 4.74/4.10 26653[0:MRR:26096.0,26096.1,7.0,6.0] || option_set(U) weakly_better(skc12,U)* -> weakly_better(skc11,U). % 4.74/4.10 26655(e)[0:MRR:26095.0,26095.1,6.0,7.0] || option_set(U) weakly_better(skc11,U) -> better(skc11,skc12) weakly_better(skc12,U)*. % 4.74/4.10 26830[0:Res:41.3,26653.1] || option_set(skc12) option_set(U) better(skc12,U) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 26847[0:Obv:26830.1] || option_set(skc12) better(skc12,U) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 26848[0:MRR:26847.0,6.0] || better(skc12,U) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 26892[0:Res:26848.2,47.2] || better(skc12,U) option_set(U) option_set(skc11) option_set(U) -> weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 26895[0:Obv:26892.1] || better(skc12,U) option_set(skc11) option_set(U) -> weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 26896[0:MRR:26895.1,7.0] || better(skc12,U) option_set(U) -> weakly_better(U,skc11)* better(skc11,U). % 4.74/4.10 27261(e)[0:EqR:969.0] || -> SkP1(skc17,skc11) equal(skf9(skc17,skc11),skc17)** equal(skf9(skc17,skc11),skc16) equal(skf9(skc17,skc11),skc15). % 4.74/4.10 27401[0:SpL:25415.6,52.6] || option_set(U) option(V) subset(U,skc11) member(V,U) better(skc11,U) required_preference(V,skc17) option_set(U) option(V) option_set(skc11) subset(U,skc11) member(V,U) better(skc11,U) required_preference(V,skc16) -> equal(skf8(V,U,skc11),skc15)**. % 4.74/4.10 27418[0:Obv:27401.4] || required_preference(U,skc17) option_set(V) option(U) option_set(skc11) subset(V,skc11) member(U,V) better(skc11,V) required_preference(U,skc16) -> equal(skf8(U,V,skc11),skc15)**. % 4.74/4.10 27419[0:MRR:27418.3,7.0] || required_preference(U,skc17) option_set(V) option(U) subset(V,skc11) member(U,V) better(skc11,V) required_preference(U,skc16) -> equal(skf8(U,V,skc11),skc15)**. % 4.74/4.10 28872[0:SpL:27419.7,446.0] || required_preference(U,skc17) option_set(skc13) option(U) subset(skc13,skc11)* member(U,skc13)* better(skc11,skc13) required_preference(U,skc16) equal(skc15,skc15) option(U) option_set(skc11) subset(skc13,skc11)* member(U,skc13)* better(skc11,skc13) -> . % 4.74/4.10 28874(e)[0:Obv:28872.7] || required_preference(U,skc17) option_set(skc13) required_preference(U,skc16) option(U) option_set(skc11) subset(skc13,skc11)* member(U,skc13)* better(skc11,skc13) -> . % 4.74/4.10 28875[7:MRR:28874.1,28874.4,28874.5,28874.7,5.0,7.0,274.0,25091.0] || required_preference(U,skc17) required_preference(U,skc16) option(U) member(U,skc13)* -> . % 4.74/4.10 28890[7:Res:19.0,28875.3] || required_preference(skc15,skc17)* required_preference(skc15,skc16) option(skc15) -> . % 4.74/4.10 28897(e)[7:MRR:28890.0,28890.1,28890.2,12.0,18.0,3.0] || -> . % 4.74/4.10 28923[7:Spt:28897.0,1967.0,25091.0] || better(skc11,skc13)* -> . % 4.74/4.10 28924[7:Spt:28897.0,1967.1] || -> weakly_better(skc11,skc11)*. % 4.74/4.10 28925[7:MRR:10581.2,28923.0] || option_set(U) weakly_better(skc11,U) -> weakly_better(skc13,U)*. % 4.74/4.10 28988[8:Spt:14370.1] || -> better(skc12,skc13)*. % 4.74/4.10 28990[8:Res:28988.0,279.0] || option_set(skc12) option_set(skc13) option_set(U) weakly_better(skc13,U)* -> weakly_better(skc12,U). % 4.74/4.10 28998[8:MRR:28990.0,28990.1,6.0,5.0] || option_set(U) weakly_better(skc13,U)* -> weakly_better(skc12,U). % 4.74/4.10 29076[7:Res:28925.2,42.3] || option_set(U) weakly_better(skc11,U)* option_set(U) option_set(skc13) better(U,skc13) -> . % 4.74/4.10 29078[7:Res:28925.2,47.2] || option_set(U) weakly_better(skc11,U)* option_set(skc13) option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 29080[7:Obv:29076.0] || weakly_better(skc11,U)* option_set(U) option_set(skc13) better(U,skc13) -> . % 4.74/4.10 29081[7:MRR:29080.2,5.0] || weakly_better(skc11,U)* option_set(U) better(U,skc13) -> . % 4.74/4.10 29082[7:Obv:29078.0] || weakly_better(skc11,U)* option_set(skc13) option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 29083[7:MRR:29082.1,5.0] || weakly_better(skc11,U)*+ option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 29090[8:Res:26896.2,28998.1] || better(skc12,skc13) option_set(skc13) option_set(skc11) -> better(skc11,skc13) weakly_better(skc12,skc11)*. % 4.74/4.10 29106[8:MRR:29090.0,29090.1,29090.2,29090.3,28988.0,5.0,7.0,28923.0] || -> weakly_better(skc12,skc11)*. % 4.74/4.10 29117[8:Res:29106.0,47.2] || option_set(skc12) option_set(skc11) -> weakly_better(skc11,skc12)* better(skc12,skc11). % 4.74/4.10 29120[8:MRR:29117.0,29117.1,29117.3,6.0,7.0,26651.0] || -> weakly_better(skc11,skc12)*. % 4.74/4.10 29183[7:Res:40.3,29081.0] || option_set(U) option_set(skc11) subset(U,skc11)* option_set(U) better(U,skc13) -> . % 4.74/4.10 29206[8:Res:29120.0,29081.0] || option_set(skc12) better(skc12,skc13)* -> . % 4.74/4.10 29207(e)[8:MRR:29206.0,29206.1,6.0,28988.0] || -> . % 4.74/4.10 29214[7:Obv:29183.0] || option_set(skc11) subset(U,skc11)* option_set(U) better(U,skc13) -> . % 4.74/4.10 29215[7:MRR:29214.0,7.0] || subset(U,skc11)* option_set(U) better(U,skc13) -> . % 4.74/4.10 29232[8:Spt:29207.0,14370.1,28988.0] || better(skc12,skc13)* -> . % 4.74/4.10 29233(e)[8:Spt:29207.0,14370.0,14370.2] || subset(skc13,skc14) -> weakly_better(skc11,skc12)*. % 4.74/4.10 29239[8:Res:29233.1,47.2] || subset(skc13,skc14) option_set(skc11) option_set(skc12) -> weakly_better(skc12,skc11)* better(skc11,skc12). % 4.74/4.10 29241(e)[8:MRR:29239.1,29239.2,7.0,6.0] || subset(skc13,skc14) -> weakly_better(skc12,skc11)* better(skc11,skc12). % 4.74/4.10 29248[9:Spt:14384.0] || -> better(skc11,skc14)*. % 4.74/4.10 29252[9:Res:29248.0,50.4] || option_set(skc11) option(U) option_set(skc14) option(V) SkP1(U,skc11)* SkP1(V,skc14)* -> . % 4.74/4.10 29253(e)[9:MRR:29252.0,29252.2,7.0,4.0] || option(U) option(V) SkP1(U,skc11)*+ SkP1(V,skc14)* -> . % 4.74/4.10 29473[10:Spt:27261.0] || -> SkP1(skc17,skc11)*. % 4.74/4.10 29484[7:Res:40.3,29083.0] || option_set(U) option_set(skc11) subset(U,skc11) option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 29500[7:Res:26848.2,29083.0] || better(skc12,U) option_set(U) option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 29507[7:Res:28924.0,29083.0] || option_set(skc11) -> weakly_better(skc11,skc13)* better(skc13,skc11). % 4.74/4.10 29509[7:MRR:29507.0,29507.2,7.0,523.0] || -> weakly_better(skc11,skc13)*. % 4.74/4.10 29511[7:Obv:29500.1] || better(skc12,U) option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 29516[7:Obv:29484.0] || option_set(skc11) subset(U,skc11) option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 29517[7:MRR:29516.0,7.0] || subset(U,skc11) option_set(U) -> weakly_better(U,skc13)* better(skc13,U). % 4.74/4.10 29534[7:Res:29509.0,47.2] || option_set(skc11) option_set(skc13) -> weakly_better(skc13,skc11)* better(skc11,skc13). % 4.74/4.10 29539[7:MRR:29534.0,29534.1,29534.3,7.0,5.0,28923.0] || -> weakly_better(skc13,skc11)*. % 4.74/4.10 29832[7:Res:29511.2,49.3] || better(skc12,U) option_set(U) option_set(U) option_set(skc13) option_set(V) weakly_better(skc13,V)* -> better(skc13,U) weakly_better(U,V)*. % 4.74/4.10 29842[7:Res:29511.2,802.1] || better(skc12,skc14) option_set(skc14) option_set(skc13) -> better(skc13,skc14) weakly_better(skc12,skc13)*. % 4.74/4.10 29849[7:Obv:29832.1] || better(skc12,U) option_set(U) option_set(skc13) option_set(V) weakly_better(skc13,V)* -> better(skc13,U) weakly_better(U,V)*. % 4.74/4.10 29850[7:MRR:29849.2,5.0] || better(skc12,U)+ option_set(U) option_set(V) weakly_better(skc13,V)* -> better(skc13,U) weakly_better(U,V)*. % 4.74/4.10 29964[7:Res:29517.2,47.2] || subset(U,skc11) option_set(U) option_set(U) option_set(skc13) -> better(skc13,U) weakly_better(skc13,U)* better(U,skc13). % 4.74/4.10 29978[7:Obv:29964.1] || subset(U,skc11) option_set(U) option_set(skc13) -> better(skc13,U) weakly_better(skc13,U)* better(U,skc13). % 4.74/4.10 29979[7:MRR:29978.2,29978.5,5.0,29215.2] || subset(U,skc11) option_set(U) -> better(skc13,U) weakly_better(skc13,U)*. % 4.74/4.10 30283[7:Res:29979.3,801.1] || subset(U,skc11) option_set(U) option_set(U) -> better(skc13,U) weakly_better(skc11,U)*. % 4.74/4.10 30285[7:Obv:30283.1] || subset(U,skc11) option_set(U) -> better(skc13,U) weakly_better(skc11,U)*. % 4.74/4.10 30384[10:Res:29473.0,29253.2] || option(skc17) option(U) SkP1(U,skc14)* -> . % 4.74/4.10 30385[10:MRR:30384.0,1.0] || option(U) SkP1(U,skc14)* -> . % 4.74/4.10 30387[10:Res:24478.0,30385.1] || option(skc17)* -> . % 4.74/4.10 30388(e)[10:MRR:30387.0,1.0] || -> . % 4.74/4.10 30390[10:Spt:30388.0,27261.0,29473.0] || SkP1(skc17,skc11)* -> . % 4.74/4.10 30391(e)[10:Spt:30388.0,27261.1,27261.2,27261.3] || -> equal(skf9(skc17,skc11),skc17)** equal(skf9(skc17,skc11),skc16) equal(skf9(skc17,skc11),skc15). % 4.74/4.10 30392[7:MRR:30285.2,823.0] || subset(U,skc11) option_set(U) -> weakly_better(skc11,U)*. % 4.74/4.10 30394(e)[7:MRR:29842.0,29842.1,29842.2,24381.0,4.0,5.0] || -> better(skc13,skc14) weakly_better(skc12,skc13)*. % 4.74/4.10 30399[11:Spt:30391.0] || -> equal(skf9(skc17,skc11),skc17)**. % 4.74/4.10 30410[11:SpL:30399.0,228.0] || equal(skc17,skc17) equal(skf9(skc17,skc11),skc17)** -> SkP1(skc17,skc11). % 4.74/4.10 30416[11:Obv:30410.0] || equal(skf9(skc17,skc11),skc17)** -> SkP1(skc17,skc11). % 4.74/4.10 30417[11:Rew:30399.0,30416.0] || equal(skc17,skc17) -> SkP1(skc17,skc11)*. % 4.74/4.10 30418[11:Obv:30417.0] || -> SkP1(skc17,skc11)*. % 4.74/4.10 30419(e)[11:MRR:30418.0,30390.0] || -> . % 4.74/4.10 30421[11:Spt:30419.0,30391.0,30399.0] || equal(skf9(skc17,skc11),skc17)** -> . % 4.74/4.10 30422(e)[11:Spt:30419.0,30391.1,30391.2] || -> equal(skf9(skc17,skc11),skc16)** equal(skf9(skc17,skc11),skc15). % 4.74/4.10 30481[8:Res:29233.1,29083.0] || subset(skc13,skc14) option_set(skc12) -> weakly_better(skc12,skc13)* better(skc13,skc12). % 4.74/4.10 30483(e)[8:MRR:30481.1,6.0] || subset(skc13,skc14) -> weakly_better(skc12,skc13)* better(skc13,skc12). % 4.74/4.10 30541[12:Spt:29241.2] || -> better(skc11,skc12)*. % 4.74/4.10 30595[13:Spt:30483.1] || -> weakly_better(skc12,skc13)*. % 4.74/4.10 30597[13:Res:30595.0,49.3] || option_set(skc12) option_set(skc13) option_set(U) weakly_better(skc13,U)* -> weakly_better(skc12,U). % 4.74/4.10 30604[13:MRR:30597.0,30597.1,6.0,5.0] || option_set(U) weakly_better(skc13,U)* -> weakly_better(skc12,U). % 4.74/4.10 30730[13:Res:29539.0,30604.1] || option_set(skc11) -> weakly_better(skc12,skc11)*. % 4.74/4.10 30733[13:MRR:30730.0,7.0] || -> weakly_better(skc12,skc11)*. % 4.74/4.10 30766[13:Res:30733.0,42.3] || option_set(skc11) option_set(skc12) better(skc11,skc12)* -> . % 4.74/4.10 30770(e)[13:MRR:30766.0,30766.1,30766.2,7.0,6.0,30541.0] || -> . % 4.74/4.10 30771[13:Spt:30770.0,30483.1,30595.0] || weakly_better(skc12,skc13)* -> . % 4.74/4.10 30772[13:Spt:30770.0,30483.0,30483.2] || subset(skc13,skc14)* -> better(skc13,skc12). % 4.74/4.10 30773[13:MRR:30394.1,30771.0] || -> better(skc13,skc14)*. % 4.74/4.10 30794[13:Res:30773.0,50.4] || option_set(skc13) option(U) option_set(skc14) option(V) SkP1(U,skc13)* SkP1(V,skc14)* -> . % 4.74/4.10 30800[13:MRR:30794.0,30794.2,5.0,4.0] || option(U) option(V) SkP1(U,skc13)*+ SkP1(V,skc14)* -> . % 4.74/4.10 31246[13:Res:108.0,30800.2] || option(skc15) option(U) SkP1(U,skc14)* -> . % 4.74/4.10 31247[13:MRR:31246.0,3.0] || option(U) SkP1(U,skc14)* -> . % 4.74/4.10 31249[13:Res:24478.0,31247.1] || option(skc17)* -> . % 4.74/4.10 31250(e)[13:MRR:31249.0,1.0] || -> . % 4.74/4.10 31252[12:Spt:31250.0,29241.2,30541.0] || better(skc11,skc12)* -> . % 4.74/4.10 31253(e)[12:Spt:31250.0,29241.0,29241.1] || subset(skc13,skc14) -> weakly_better(skc12,skc11)*. % 4.74/4.10 31254[12:MRR:26655.2,31252.0] || option_set(U) weakly_better(skc11,U) -> weakly_better(skc12,U)*. % 4.74/4.10 31311[13:Spt:30394.0] || -> better(skc13,skc14)*. % 4.74/4.10 31315[13:Res:31311.0,50.4] || option_set(skc13) option(U) option_set(skc14) option(V) SkP1(U,skc13)* SkP1(V,skc14)* -> . % 4.74/4.10 31321[13:MRR:31315.0,31315.2,5.0,4.0] || option(U) option(V) SkP1(U,skc13)*+ SkP1(V,skc14)* -> . % 4.74/4.10 31507[12:Res:31254.2,47.2] || option_set(U) weakly_better(skc11,U)* option_set(skc12) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 31511[12:Obv:31507.0] || weakly_better(skc11,U)* option_set(skc12) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 31512[12:MRR:31511.1,6.0] || weakly_better(skc11,U)*+ option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 31947[12:Res:30392.2,31512.0] || subset(U,skc11) option_set(U) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 31961[12:Obv:31947.1] || subset(U,skc11) option_set(U) -> weakly_better(U,skc12)* better(skc12,U). % 4.74/4.10 32175[13:Res:108.0,31321.2] || option(skc15) option(U) SkP1(U,skc14)* -> . % 4.74/4.10 32176[13:MRR:32175.0,3.0] || option(U) SkP1(U,skc14)* -> . % 4.74/4.10 32178[13:Res:24478.0,32176.1] || option(skc17)* -> . % 4.74/4.10 32179(e)[13:MRR:32178.0,1.0] || -> . % 4.74/4.10 32181[13:Spt:32179.0,30394.0,31311.0] || better(skc13,skc14)* -> . % 4.74/4.10 32182[13:Spt:32179.0,30394.1] || -> weakly_better(skc12,skc13)*. % 4.74/4.10 33565[0:EqR:25706.0] || equal(skc16,U) option(skc17) option(U) option_set(V) permitted_preference(skc17,U)* permitted_preference(U,skc17)* member(skc17,V) -> better(skc12,V) member(skf6(skc17,V),V)*. % 4.74/4.10 33566[0:MRR:33565.1,1.0] || equal(skc16,U)+ option(U) option_set(V) permitted_preference(skc17,U)* permitted_preference(U,skc17)* member(skc17,V) -> better(skc12,V) member(skf6(skc17,V),V)*. % 4.74/4.10 33628[7:Res:24381.0,29850.0] || option_set(skc14) option_set(U) weakly_better(skc13,U) -> better(skc13,skc14) weakly_better(skc14,U)*. % 4.74/4.10 33629[13:MRR:33628.0,33628.3,4.0,32181.0] || option_set(U) weakly_better(skc13,U) -> weakly_better(skc14,U)*. % 4.74/4.10 33630[13:Res:33629.2,42.3] || option_set(U) weakly_better(skc13,U)* option_set(U) option_set(skc14) better(U,skc14) -> . % 4.74/4.10 33638[13:Obv:33630.0] || weakly_better(skc13,U)* option_set(U) option_set(skc14) better(U,skc14) -> . % 4.74/4.10 33639[13:MRR:33638.2,4.0] || weakly_better(skc13,U)* option_set(U) better(U,skc14) -> . % 4.74/4.10 33786[13:Res:31961.2,33639.0] || subset(skc13,skc11)* option_set(skc13) option_set(skc12) better(skc12,skc14) -> better(skc12,skc13). % 4.74/4.10 33831(e)[13:MRR:33786.0,33786.1,33786.2,33786.3,33786.4,274.0,5.0,6.0,24381.0,29232.0] || -> . % 4.74/4.10 33861[9:Spt:33831.0,14384.0,29248.0] || better(skc11,skc14)* -> . % 4.74/4.10 33862[9:Spt:33831.0,14384.1] || -> weakly_better(skc12,skc11)*. % 4.74/4.10 33866[9:MRR:14385.2,33861.0] || option_set(U) weakly_better(skc11,U) -> weakly_better(skc14,U)*. % 4.74/4.10 33983[9:Res:33866.2,42.3] || option_set(U) weakly_better(skc11,U)* option_set(U) option_set(skc14) better(U,skc14) -> . % 4.74/4.10 33991[9:Obv:33983.0] || weakly_better(skc11,U)* option_set(U) option_set(skc14) better(U,skc14) -> . % 4.74/4.10 33992[9:MRR:33991.2,4.0] || weakly_better(skc11,U)* option_set(U) better(U,skc14) -> . % 4.74/4.10 34277[9:Res:1931.3,33992.0] || subset(skc14,skc11)* option_set(skc11) option_set(skc12) better(skc12,skc14) -> better(skc11,skc14) better(skc12,skc11). % 4.74/4.10 34334(e)[9:MRR:34277.0,34277.1,34277.2,34277.3,34277.4,34277.5,290.0,7.0,6.0,24381.0,33861.0,26651.0] || -> . % 4.74/4.10 34339(e)[4:Spt:34334.0,130.0,24478.0] || SkP1(skc17,skc14)* -> . % 4.74/4.10 34340[4:Spt:34334.0,130.1] || -> equal(skf9(skc17,skc14),skc17)**. % 4.74/4.10 34357[4:SpL:34340.0,223.0] || equal(skc17,skc17) equal(skf9(skc17,skc14),skc17)** -> SkP1(skc17,skc14). % 4.74/4.10 34362[4:Obv:34357.0] || equal(skf9(skc17,skc14),skc17)** -> SkP1(skc17,skc14). % 4.74/4.10 34363[4:Rew:34340.0,34362.0] || equal(skc17,skc17) -> SkP1(skc17,skc14)*. % 4.74/4.10 34364[4:Obv:34363.0] || -> SkP1(skc17,skc14)*. % 4.74/4.10 34365(e)[4:MRR:34364.0,34339.0] || -> . % 4.74/4.10 34366[3:Spt:34365.0,2039.0,24381.0] || better(skc12,skc14)* -> . % 4.74/4.10 34367[3:Spt:34365.0,2039.1] || -> weakly_better(skc12,skc12)*. % 4.74/4.10 59959[0:EqR:33566.0] || option(skc16) option_set(U) permitted_preference(skc17,skc16) permitted_preference(skc16,skc17) member(skc17,U) -> better(skc12,U) member(skf6(skc17,U),U)*. % 4.74/4.10 59960[0:MRR:59959.0,59959.2,59959.3,2.0,10.0,11.0] || option_set(U) member(skc17,U) -> better(skc12,U) member(skf6(skc17,U),U)*. % 4.74/4.10 59974[0:Res:59960.3,27.1] || option_set(skc14) member(skc17,skc14) option(skf6(skc17,skc14))* -> better(skc12,skc14) equal(skf6(skc17,skc14),skc17). % 4.74/4.10 59979[3:MRR:59974.0,59974.1,59974.2,59974.3,4.0,13.0,22.0,34366.0] || -> equal(skf6(skc17,skc14),skc17)**. % 4.74/4.10 59995[3:SpL:59979.0,55.9] || option(skc17) option(U) option_set(V) option_set(skc14) permitted_preference(skc17,U) permitted_preference(U,skc17) member(skc17,V) member(skc17,skc14) member(U,V) equal(skc17,skc17) SkP0(U,skc17,V)* -> better(V,skc14). % 4.74/4.10 59996[3:Obv:59995.9] || option(skc17) option(U) option_set(V) option_set(skc14) permitted_preference(skc17,U) permitted_preference(U,skc17) member(skc17,V) member(skc17,skc14) member(U,V) SkP0(U,skc17,V)* -> better(V,skc14). % 4.74/4.10 59997[3:MRR:59996.0,59996.3,59996.7,1.0,4.0,13.0] || option(U) option_set(V) permitted_preference(skc17,U) permitted_preference(U,skc17) member(skc17,V) member(U,V) SkP0(U,skc17,V)* -> better(V,skc14). % 4.74/4.10 60115[3:Res:25660.2,59997.6] || equal(skc17,skc17) equal(skc16,U) option(U) option_set(skc12) permitted_preference(skc17,U) permitted_preference(U,skc17) member(skc17,skc12)* member(U,skc12)* -> better(skc12,skc14). % 4.74/4.10 60125[3:Obv:60115.0] || equal(skc16,U) option(U) option_set(skc12) permitted_preference(skc17,U) permitted_preference(U,skc17) member(skc17,skc12)* member(U,skc12)* -> better(skc12,skc14). % 4.74/4.10 60126[3:MRR:60125.2,60125.5,60125.6,60125.7,6.0,14.0,29.2,34366.0] || equal(skc16,U)+ option(U) permitted_preference(skc17,U)* permitted_preference(U,skc17)* -> . % 4.74/4.10 60154[3:EqR:60126.0] || option(skc16) permitted_preference(skc17,skc16)* permitted_preference(skc16,skc17) -> . % 4.74/4.10 60155(e)[3:MRR:60154.0,60154.1,60154.2,2.0,10.0,11.0] || -> . % 4.74/4.10 60156(e)[1:Spt:60155.0,94.0,108.0] || SkP1(skc15,skc13)* -> . % 4.74/4.10 60157[1:Spt:60155.0,94.1] || -> equal(skf9(skc15,skc13),skc15)**. % 4.74/4.10 60237[1:SpL:60157.0,44.0] || member(skc15,skc13) equal(skf9(skc15,skc13),skc15)** -> SkP1(skc15,skc13). % 4.74/4.10 60239[1:Rew:60157.0,60237.1] || member(skc15,skc13) equal(skc15,skc15) -> SkP1(skc15,skc13)*. % 4.74/4.10 60240[1:Obv:60239.1] || member(skc15,skc13) -> SkP1(skc15,skc13)*. % 4.74/4.10 60241[1:MRR:60240.0,19.0] || -> SkP1(skc15,skc13)*. % 4.74/4.10 60242(e)[1:MRR:60241.0,60156.0] || -> . % 4.74/4.10 % 4.74/4.10 % SZS output end CNFRefutation for /tmp/SPASST_27470_n021.cluster.edu % 4.74/4.10 % 4.74/4.10 Formulae used in the proof : fof_existence_of_dominated_diversity fof_parity_of_no_choice_situations fof_value_of_rational_diversity fof_subset fof_insignificance_of_dominated_options fof_harmlessness_of_expansions fof_better fof_transitivity_of_weakly_better_freedom_of_choice % 21.90/21.22 % 21.90/21.22 SPASS+T ended %------------------------------------------------------------------------------