%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP224-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 07:48:40 PM UTC 2025 % Result : Satisfiable 9.61s 3.21s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP224-1 : TPTP v9.0.0. Released v2.4.0. % 0.11/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Apr 8 09:30:09 EDT 2025 % 0.12/0.33 % CPUTime : % 9.61/3.21 % 9.61/3.21 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.61/3.22 % 9.61/3.22 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.61/3.22 %$ be > theme > of > agent > vincent_forename > unisex > think_believe_consider > thing > state > specific > smoke > singleton > relname > relation > proposition > present > organism > nonhuman > nonexistent > man > male > living > jules_forename > impartial > human_person > human > general > forename > existent > eventuality > event > entity > animate > accessible_world > abstraction > actual_world > #nlpp > skf1 > skc9 > skc17 > skc16 > skc15 > skc14 > skc13 > skc12 > skc11 > skc10 % 9.61/3.22 % 9.61/3.22 %Foreground sorts: % 9.61/3.22 % 9.61/3.22 % 9.61/3.22 %Background operators: % 9.61/3.22 % 9.61/3.22 % 9.61/3.22 %Foreground operators: % 9.61/3.22 tff(skc16, type, skc16: $i). % 9.61/3.22 tff(relation, type, relation: ($i * $i) > $o). % 9.61/3.22 tff(forename, type, forename: ($i * $i) > $o). % 9.61/3.22 tff(be, type, be: ($i * $i * $i * $i) > $o). % 9.61/3.22 tff(theme, type, theme: ($i * $i * $i) > $o). % 9.61/3.22 tff(living, type, living: ($i * $i) > $o). % 9.61/3.22 tff(human_person, type, human_person: ($i * $i) > $o). % 9.61/3.22 tff(present, type, present: ($i * $i) > $o). % 9.61/3.22 tff(skc11, type, skc11: $i). % 9.61/3.22 tff(entity, type, entity: ($i * $i) > $o). % 9.61/3.22 tff(skc9, type, skc9: $i). % 9.61/3.22 tff(eventuality, type, eventuality: ($i * $i) > $o). % 9.61/3.22 tff(existent, type, existent: ($i * $i) > $o). % 9.61/3.22 tff(abstraction, type, abstraction: ($i * $i) > $o). % 9.61/3.22 tff(skf1, type, skf1: $i > $i). % 9.61/3.22 tff(proposition, type, proposition: ($i * $i) > $o). % 9.61/3.22 tff(relname, type, relname: ($i * $i) > $o). % 9.61/3.22 tff(skc14, type, skc14: $i). % 9.61/3.22 tff(singleton, type, singleton: ($i * $i) > $o). % 9.61/3.22 tff(skc17, type, skc17: $i). % 9.61/3.22 tff(skc13, type, skc13: $i). % 9.61/3.22 tff(male, type, male: ($i * $i) > $o). % 9.61/3.22 tff(organism, type, organism: ($i * $i) > $o). % 9.61/3.22 tff(animate, type, animate: ($i * $i) > $o). % 9.61/3.22 tff(of, type, of: ($i * $i * $i) > $o). % 9.61/3.22 tff(actual_world, type, actual_world: $i > $o). % 9.61/3.22 tff(agent, type, agent: ($i * $i * $i) > $o). % 9.61/3.22 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 9.61/3.22 tff(general, type, general: ($i * $i) > $o). % 9.61/3.22 tff(smoke, type, smoke: ($i * $i) > $o). % 9.61/3.22 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 9.61/3.22 tff(event, type, event: ($i * $i) > $o). % 9.61/3.22 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 9.61/3.22 tff(state, type, state: ($i * $i) > $o). % 9.61/3.22 tff(thing, type, thing: ($i * $i) > $o). % 9.61/3.22 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 9.61/3.22 tff(skc15, type, skc15: $i). % 9.61/3.22 tff(human, type, human: ($i * $i) > $o). % 9.61/3.22 tff(man, type, man: ($i * $i) > $o). % 9.61/3.22 tff(unisex, type, unisex: ($i * $i) > $o). % 9.61/3.22 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 9.61/3.22 tff(impartial, type, impartial: ($i * $i) > $o). % 9.61/3.22 tff(skc12, type, skc12: $i). % 9.61/3.22 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 9.61/3.22 tff(specific, type, specific: ($i * $i) > $o). % 9.61/3.22 tff(skc10, type, skc10: $i). % 9.61/3.22 % 9.61/3.22 %Saturated clause set: % 9.61/3.23 tff(c_3692, plain, (![V_1110, V_704]: (skc14=V_1110 | ~think_believe_consider(V_704, skc15) | ~think_believe_consider(V_704, skf1(skc17)) | ~theme(V_704, skf1(skc17), V_1110) | ~proposition(V_704, skc14) | ~proposition(V_704, V_1110) | ~accessible_world(skc14, V_704) | ~accessible_world(skc9, V_704)))). % 9.61/3.23 tff(c_3668, plain, (![W_1102, V_1099, V_713]: (W_1102=V_1099 | ~theme(V_713, skc15, W_1102) | ~think_believe_consider(V_713, skc15) | ~think_believe_consider(V_713, skf1(skc17)) | ~theme(V_713, skf1(skc17), V_1099) | ~proposition(V_713, W_1102) | ~proposition(V_713, V_1099) | ~accessible_world(skc14, V_713) | ~accessible_world(skc9, V_713)))). % 9.61/3.23 tff(c_3665, plain, (![W_1102, V_1099, V_713, U_196]: (W_1102=V_1099 | ~theme(V_713, skf1(U_196), W_1102) | ~think_believe_consider(V_713, skf1(U_196)) | ~theme(V_713, skf1(U_196), V_1099) | ~proposition(V_713, W_1102) | ~proposition(V_713, V_1099) | ~accessible_world(skc14, V_713) | ~man(skc14, U_196)))). % 9.61/3.23 tff(c_3685, plain, (~accessible_world(skc14, skc9))). % 9.61/3.23 tff(c_3652, plain, (![V_1095, V_704]: (skc14=V_1095 | ~agent(V_704, skc15, skc17) | ~think_believe_consider(V_704, skc15) | ~theme(V_704, skc15, V_1095) | ~proposition(V_704, skc14) | ~proposition(V_704, V_1095) | ~accessible_world(skc9, V_704)))). % 9.61/3.23 tff(c_2539, plain, (![U_824, V_189, Y_188, V_823, W_184]: (W_184=V_189 | ~agent(V_823, Y_188, U_824) | ~theme(V_823, Y_188, W_184) | ~think_believe_consider(V_823, Y_188) | ~think_believe_consider(V_823, skf1(U_824)) | ~theme(V_823, skf1(U_824), V_189) | ~proposition(V_823, W_184) | ~proposition(V_823, V_189) | ~accessible_world(skc14, V_823) | ~man(skc14, U_824)))). % 9.61/3.23 tff(c_2027, plain, (![W_748, V_746, V_713, Y_747]: (W_748=V_746 | ~agent(V_713, Y_747, skc17) | ~theme(V_713, Y_747, W_748) | ~think_believe_consider(V_713, Y_747) | ~think_believe_consider(V_713, skc15) | ~theme(V_713, skc15, V_746) | ~proposition(V_713, W_748) | ~proposition(V_713, V_746) | ~accessible_world(skc9, V_713)))). % 9.61/3.23 tff(c_2005, plain, (![W_182, V_739]: (skc12=W_182 | ~entity(V_739, skc11) | ~forename(V_739, W_182) | ~of(V_739, W_182, skc11) | ~forename(V_739, skc12) | ~accessible_world(skc9, V_739)))). % 9.61/3.23 tff(c_3053, plain, (![V_113, V_948, V_947]: (impartial(V_113, V_948) | ~accessible_world(V_947, V_113) | ~accessible_world(skc14, V_947) | ~human_person(skc9, V_948)))). % 9.61/3.23 tff(c_3096, plain, (![V_134, V_958, V_957]: (relation(V_134, V_958) | ~accessible_world(V_957, V_134) | ~accessible_world(skc14, V_957) | ~forename(skc9, V_958)))). % 9.61/3.23 tff(c_2997, plain, (![V_116, V_933, V_932]: (living(V_116, V_933) | ~accessible_world(V_932, V_116) | ~accessible_world(skc14, V_932) | ~human_person(skc9, V_933)))). % 9.61/3.23 tff(c_3089, plain, (![V_83, V_956, V_955]: (singleton(V_83, V_956) | ~accessible_world(V_955, V_83) | ~accessible_world(skc14, V_955) | ~entity(skc9, V_956)))). % 9.61/3.23 tff(c_3010, plain, (![V_83, V_939, V_938]: (singleton(V_83, V_939) | ~accessible_world(V_938, V_83) | ~accessible_world(skc14, V_938) | ~eventuality(skc9, V_939)))). % 9.61/3.23 tff(c_3566, plain, (![V_122, V_1062]: (animate(V_122, skc17) | ~accessible_world(V_1062, V_122) | ~accessible_world(skc14, V_1062)))). % 9.61/3.23 tff(c_3561, plain, (![V_119, V_1061]: (human(V_119, skc17) | ~accessible_world(V_1061, V_119) | ~accessible_world(skc14, V_1061)))). % 9.61/3.23 tff(c_3543, plain, (![V_125, V_1060]: (male(V_125, skc17) | ~accessible_world(V_1060, V_125) | ~accessible_world(skc14, V_1060)))). % 9.61/3.23 tff(c_3512, plain, (![V_101, V_1059]: (human_person(V_101, skc17) | ~accessible_world(V_1059, V_101) | ~accessible_world(skc14, V_1059)))). % 9.61/3.23 tff(c_3470, plain, (![V_98, V_1057]: (man(V_98, skc17) | ~accessible_world(V_1057, V_98) | ~accessible_world(skc14, V_1057)))). % 9.61/3.23 tff(c_3489, plain, (![V_155, V_1058]: (think_believe_consider(V_155, skc15) | ~accessible_world(V_1058, V_155) | ~accessible_world(skc14, V_1058)))). % 9.61/3.23 tff(c_3583, plain, (![U_15]: (~accessible_world(skc14, U_15) | ~event(U_15, skc17)))). % 9.61/3.23 tff(c_3545, plain, (![V_1060]: (~eventuality(V_1060, skc17) | ~accessible_world(skc14, V_1060)))). % 9.61/3.23 tff(c_3567, plain, (~think_believe_consider(skc14, skf1(skc17)))). % 9.61/3.23 tff(c_3515, plain, (![V_1059]: (animate(V_1059, skc17) | ~accessible_world(skc14, V_1059)))). % 9.61/3.23 tff(c_3514, plain, (![V_1059]: (human(V_1059, skc17) | ~accessible_world(skc14, V_1059)))). % 9.61/3.23 tff(c_3428, plain, (![V_125]: (male(V_125, skc17) | ~accessible_world(skc14, V_125)))). % 9.61/3.23 tff(c_3471, plain, (![V_1057]: (human_person(V_1057, skc17) | ~accessible_world(skc14, V_1057)))). % 9.61/3.23 tff(c_3485, plain, (![V_155]: (think_believe_consider(V_155, skc15) | ~accessible_world(skc14, V_155)))). % 9.61/3.23 tff(c_3482, plain, (think_believe_consider(skc14, skc15))). % 9.61/3.23 tff(c_3385, plain, (![V_98]: (man(V_98, skc17) | ~accessible_world(skc14, V_98)))). % 9.61/3.23 tff(c_3445, plain, (~event(skc14, skc17))). % 9.61/3.23 tff(c_3402, plain, (human(skc14, skc17))). % 9.61/3.23 tff(c_3430, plain, (~eventuality(skc14, skc17))). % 9.61/3.23 tff(c_3403, plain, (animate(skc14, skc17))). % 9.61/3.23 tff(c_3387, plain, (male(skc14, skc17))). % 9.61/3.23 tff(c_3386, plain, (human_person(skc14, skc17))). % 9.61/3.23 tff(c_3376, plain, (man(skc14, skc17))). % 9.61/3.23 tff(c_3001, plain, (![V_83, V_935, V_934]: (singleton(V_83, V_935) | ~accessible_world(V_934, V_83) | ~accessible_world(skc14, V_934) | ~abstraction(skc9, V_935)))). % 9.61/3.23 tff(c_2837, plain, (![V_80, V_911, V_910]: (thing(V_80, V_911) | ~accessible_world(V_910, V_80) | ~accessible_world(skc14, V_910) | ~eventuality(skc9, V_911)))). % 9.61/3.23 tff(c_2718, plain, (![V_80, V_886, V_885]: (thing(V_80, V_886) | ~accessible_world(V_885, V_80) | ~accessible_world(skc14, V_885) | ~abstraction(skc9, V_886)))). % 9.61/3.23 tff(c_2858, plain, (![V_92, V_915, V_914]: (unisex(V_92, V_915) | ~accessible_world(V_914, V_92) | ~accessible_world(skc14, V_914) | ~eventuality(skc9, V_915)))). % 9.61/3.23 tff(c_2850, plain, (![V_110, V_913, V_912]: (existent(V_110, V_913) | ~accessible_world(V_912, V_110) | ~accessible_world(skc14, V_912) | ~entity(skc9, V_913)))). % 9.61/3.23 tff(c_2686, plain, (![V_86, V_876, V_875]: (specific(V_86, V_876) | ~accessible_world(V_875, V_86) | ~accessible_world(skc14, V_875) | ~eventuality(skc9, V_876)))). % 9.61/3.23 tff(c_2813, plain, (![V_77, V_905, V_904]: (eventuality(V_77, V_905) | ~accessible_world(V_904, V_77) | ~accessible_world(skc14, V_904) | ~event(skc9, V_905)))). % 9.61/3.24 tff(c_2759, plain, (![V_92, V_901, V_900]: (unisex(V_92, V_901) | ~accessible_world(V_900, V_92) | ~accessible_world(skc14, V_900) | ~abstraction(skc9, V_901)))). % 9.61/3.24 tff(c_2694, plain, (![V_131, V_878, V_877]: (relname(V_131, V_878) | ~accessible_world(V_877, V_131) | ~accessible_world(skc14, V_877) | ~forename(skc9, V_878)))). % 9.61/3.24 tff(c_2667, plain, (![W_864, V_865, U_196]: (W_864=V_865 | ~theme(skc14, skf1(U_196), W_864) | ~think_believe_consider(skc14, skf1(U_196)) | ~theme(skc14, skf1(U_196), V_865) | ~proposition(skc14, W_864) | ~proposition(skc14, V_865) | ~man(skc14, U_196)))). % 9.61/3.24 tff(c_2767, plain, (![V_134, V_903, V_902]: (relation(V_134, V_903) | ~accessible_world(V_902, V_134) | ~accessible_world(skc14, V_902) | ~proposition(skc9, V_903)))). % 9.61/3.24 tff(c_2747, plain, (![V_86, V_897, V_896]: (specific(V_86, V_897) | ~accessible_world(V_896, V_86) | ~accessible_world(skc14, V_896) | ~entity(skc9, V_897)))). % 9.61/3.24 tff(c_2895, plain, (![V_143, V_919, V_918]: (general(V_143, V_919) | ~accessible_world(V_918, V_143) | ~accessible_world(skc14, V_918) | ~abstraction(skc9, V_919)))). % 9.61/3.24 tff(c_2825, plain, (![V_80, V_907, V_906]: (thing(V_80, V_907) | ~accessible_world(V_906, V_80) | ~accessible_world(skc14, V_906) | ~entity(skc9, V_907)))). % 9.61/3.24 tff(c_2739, plain, (![V_89, V_895, V_894]: (nonexistent(V_89, V_895) | ~accessible_world(V_894, V_89) | ~accessible_world(skc14, V_894) | ~eventuality(skc9, V_895)))). % 9.61/3.24 tff(c_2872, plain, (![V_104, V_917, V_916]: (organism(V_104, V_917) | ~accessible_world(V_916, V_104) | ~accessible_world(skc14, V_916) | ~human_person(skc9, V_917)))). % 9.61/3.24 tff(c_2706, plain, (![V_140, V_882, V_881]: (nonhuman(V_140, V_882) | ~accessible_world(V_881, V_140) | ~accessible_world(skc14, V_881) | ~abstraction(skc9, V_882)))). % 9.61/3.24 tff(c_2013, plain, (![V_179, V_740]: (be(V_179, skc10, skc11, skc11) | ~accessible_world(V_740, V_179) | ~accessible_world(skc9, V_740)))). % 9.61/3.24 tff(c_2006, plain, (![V_164, V_739]: (of(V_164, skc12, skc11) | ~accessible_world(V_739, V_164) | ~accessible_world(skc9, V_739)))). % 9.61/3.24 tff(c_1993, plain, (![W_735, V_720]: (skc16=W_735 | ~entity(V_720, skc17) | ~forename(V_720, W_735) | ~of(V_720, W_735, skc17) | ~forename(V_720, skc16) | ~accessible_world(skc9, V_720)))). % 9.61/3.24 tff(c_1962, plain, (![V_107, V_724]: (entity(V_107, skc11) | ~accessible_world(V_724, V_107) | ~accessible_world(skc14, V_724)))). % 9.61/3.24 tff(c_1974, plain, (![V_107, V_730]: (entity(V_107, skc17) | ~accessible_world(V_730, V_107) | ~accessible_world(skc14, V_730)))). % 9.61/3.24 tff(c_2956, plain, (![U_15, V_16]: (~accessible_world(skc14, U_15) | ~abstraction(skc9, V_16) | ~event(U_15, V_16)))). % 9.61/3.24 tff(c_2918, plain, (![U_15, V_16]: (~accessible_world(skc14, U_15) | ~entity(skc9, V_16) | ~event(U_15, V_16)))). % 9.61/3.24 tff(c_3219, plain, (![U_989]: (~accessible_world(skc14, U_989) | ~entity(U_989, skc10)))). % 9.61/3.24 tff(c_2935, plain, (![U_27, V_28]: (~accessible_world(skc14, U_27) | ~eventuality(skc9, V_28) | ~entity(U_27, V_28)))). % 9.61/3.24 tff(c_3097, plain, (![V_957, V_958]: (abstraction(V_957, V_958) | ~accessible_world(skc14, V_957) | ~forename(skc9, V_958)))). % 9.61/3.24 tff(c_3066, plain, (![U_49, V_50]: (~accessible_world(skc14, U_49) | ~eventuality(skc9, V_50) | ~abstraction(U_49, V_50)))). % 9.61/3.24 tff(c_3164, plain, (![U_49, V_50]: (~accessible_world(skc14, U_49) | ~entity(skc9, V_50) | ~abstraction(U_49, V_50)))). % 9.61/3.24 tff(c_2540, plain, (![V_168, U_824, V_823]: (agent(V_168, skf1(U_824), U_824) | ~accessible_world(V_823, V_168) | ~accessible_world(skc14, V_823) | ~man(skc14, U_824)))). % 9.61/3.24 tff(c_1821, plain, (![V_692, V_597]: (animate(V_692, skc11) | ~accessible_world(V_597, V_692) | ~accessible_world(skc9, V_597)))). % 9.61/3.24 tff(c_1820, plain, (![V_692, V_598]: (animate(V_692, skc17) | ~accessible_world(V_598, V_692) | ~accessible_world(skc9, V_598)))). % 9.61/3.24 tff(c_2815, plain, (![V_904, V_905]: (~entity(V_904, V_905) | ~accessible_world(skc14, V_904) | ~event(skc9, V_905)))). % 9.61/3.24 tff(c_2748, plain, (![V_896, V_897]: (~general(V_896, V_897) | ~accessible_world(skc14, V_896) | ~entity(skc9, V_897)))). % 9.61/3.24 tff(c_3151, plain, (~event(skc9, skc12))). % 9.61/3.24 tff(c_1981, plain, (![V_164, V_733]: (of(V_164, skc16, skc17) | ~accessible_world(V_733, V_164) | ~accessible_world(skc9, V_733)))). % 9.61/3.24 tff(c_3146, plain, (~event(skc9, skc14))). % 9.61/3.24 tff(c_3145, plain, (~event(skc9, skc16))). % 9.61/3.24 tff(c_2816, plain, (![V_904, V_905]: (~abstraction(V_904, V_905) | ~accessible_world(skc14, V_904) | ~event(skc9, V_905)))). % 9.61/3.24 tff(c_2768, plain, (![V_902, V_903]: (abstraction(V_902, V_903) | ~accessible_world(skc14, V_902) | ~proposition(skc9, V_903)))). % 9.61/3.24 tff(c_2707, plain, (![V_881, V_882]: (~human(V_881, V_882) | ~accessible_world(skc14, V_881) | ~abstraction(skc9, V_882)))). % 9.61/3.24 tff(c_1423, plain, (![V_152, V_589, V_588]: (present(V_152, skf1(V_589)) | ~accessible_world(V_588, V_152) | ~accessible_world(skc14, V_588)))). % 9.61/3.24 tff(c_1803, plain, (![V_686, V_598]: (entity(V_686, skc17) | ~accessible_world(V_598, V_686) | ~accessible_world(skc9, V_598)))). % 9.61/3.24 tff(c_1846, plain, (![V_134, V_702]: (relation(V_134, V_702) | ~accessible_world(skc14, V_134) | ~forename(skc9, V_702)))). % 9.61/3.24 tff(c_2225, plain, (![V_83, V_774]: (singleton(V_83, V_774) | ~accessible_world(skc14, V_83) | ~entity(skc9, V_774)))). % 9.61/3.24 tff(c_1390, plain, (![V_119, V_578]: (human(V_119, skc11) | ~accessible_world(V_578, V_119) | ~accessible_world(skc9, V_578)))). % 9.61/3.24 tff(c_2873, plain, (![V_916, V_917]: (entity(V_916, V_917) | ~accessible_world(skc14, V_916) | ~human_person(skc9, V_917)))). % 9.61/3.24 tff(c_2687, plain, (![V_875, V_876]: (~general(V_875, V_876) | ~accessible_world(skc14, V_875) | ~eventuality(skc9, V_876)))). % 9.61/3.24 tff(c_2874, plain, (![V_916, V_917]: (impartial(V_916, V_917) | ~accessible_world(skc14, V_916) | ~human_person(skc9, V_917)))). % 9.61/3.24 tff(c_1792, plain, (![V_149, V_685, V_684]: (smoke(V_149, skf1(V_685)) | ~accessible_world(V_684, V_149) | ~accessible_world(skc14, V_684)))). % 9.61/3.24 tff(c_2760, plain, (![V_900, V_901]: (~male(V_900, V_901) | ~accessible_world(skc14, V_900) | ~abstraction(skc9, V_901)))). % 9.61/3.24 tff(c_2859, plain, (![V_914, V_915]: (~male(V_914, V_915) | ~accessible_world(skc14, V_914) | ~eventuality(skc9, V_915)))). % 9.61/3.24 tff(c_2838, plain, (![V_910, V_911]: (singleton(V_910, V_911) | ~accessible_world(skc14, V_910) | ~eventuality(skc9, V_911)))). % 9.61/3.24 tff(c_1804, plain, (![V_686, V_597]: (entity(V_686, skc11) | ~accessible_world(V_597, V_686) | ~accessible_world(skc9, V_597)))). % 9.61/3.24 tff(c_2719, plain, (![V_885, V_886]: (singleton(V_885, V_886) | ~accessible_world(skc14, V_885) | ~abstraction(skc9, V_886)))). % 9.61/3.24 tff(c_2875, plain, (![V_916, V_917]: (living(V_916, V_917) | ~accessible_world(skc14, V_916) | ~human_person(skc9, V_917)))). % 9.61/3.24 tff(c_2897, plain, (![V_918, V_919]: (~entity(V_918, V_919) | ~accessible_world(skc14, V_918) | ~abstraction(skc9, V_919)))). % 9.61/3.24 tff(c_1878, plain, (![V_172, V_708]: (theme(V_172, skc15, skc14) | ~accessible_world(V_708, V_172) | ~accessible_world(skc9, V_708)))). % 9.61/3.24 tff(c_2896, plain, (![V_918, V_919]: (~eventuality(V_918, V_919) | ~accessible_world(skc14, V_918) | ~abstraction(skc9, V_919)))). % 9.61/3.24 tff(c_2740, plain, (![V_894, V_895]: (~existent(V_894, V_895) | ~accessible_world(skc14, V_894) | ~eventuality(skc9, V_895)))). % 9.61/3.24 tff(c_1344, plain, (![V_119, V_568]: (human(V_119, skc17) | ~accessible_world(V_568, V_119) | ~accessible_world(skc9, V_568)))). % 9.61/3.24 tff(c_2851, plain, (![V_912, V_913]: (~eventuality(V_912, V_913) | ~accessible_world(skc14, V_912) | ~entity(skc9, V_913)))). % 9.61/3.24 tff(c_2286, plain, (![V_143, V_787]: (general(V_143, V_787) | ~accessible_world(skc14, V_143) | ~abstraction(skc9, V_787)))). % 9.61/3.24 tff(c_1895, plain, (![V_104, V_712]: (organism(V_104, V_712) | ~accessible_world(skc14, V_104) | ~human_person(skc9, V_712)))). % 9.61/3.24 tff(c_2405, plain, (![V_92, V_801]: (unisex(V_92, V_801) | ~accessible_world(skc14, V_92) | ~eventuality(skc9, V_801)))). % 9.61/3.25 tff(c_2448, plain, (![V_110, V_811]: (existent(V_110, V_811) | ~accessible_world(skc14, V_110) | ~entity(skc9, V_811)))). % 9.61/3.25 tff(c_2314, plain, (![V_80, V_792]: (thing(V_80, V_792) | ~accessible_world(skc14, V_80) | ~eventuality(skc9, V_792)))). % 9.61/3.25 tff(c_1985, plain, (![V_168, V_734]: (agent(V_168, skc15, skc17) | ~accessible_world(V_734, V_168) | ~accessible_world(skc9, V_734)))). % 9.61/3.25 tff(c_2220, plain, (![V_80, V_773]: (thing(V_80, V_773) | ~accessible_world(skc14, V_80) | ~entity(skc9, V_773)))). % 9.61/3.25 tff(c_2052, plain, (![V_77, V_750]: (eventuality(V_77, V_750) | ~accessible_world(skc14, V_77) | ~event(skc9, V_750)))). % 9.61/3.25 tff(c_2196, plain, (![V_134, V_768]: (relation(V_134, V_768) | ~accessible_world(skc14, V_134) | ~proposition(skc9, V_768)))). % 9.61/3.25 tff(c_2267, plain, (![V_92, V_786]: (unisex(V_92, V_786) | ~accessible_world(skc14, V_92) | ~abstraction(skc9, V_786)))). % 9.61/3.25 tff(c_1607, plain, (![V_628, V_609]: (eventuality(V_628, skc10) | ~accessible_world(V_609, V_628) | ~accessible_world(skc9, V_609)))). % 9.61/3.25 tff(c_2116, plain, (![V_86, V_756]: (specific(V_86, V_756) | ~accessible_world(skc14, V_86) | ~entity(skc9, V_756)))). % 9.61/3.25 tff(c_2460, plain, (![V_89, V_815]: (nonexistent(V_89, V_815) | ~accessible_world(skc14, V_89) | ~eventuality(skc9, V_815)))). % 9.61/3.25 tff(c_1561, plain, (![V_125, V_619]: (male(V_125, skc11) | ~accessible_world(V_619, V_125) | ~accessible_world(skc9, V_619)))). % 9.61/3.25 tff(c_1573, plain, (![V_125, V_620]: (male(V_125, skc17) | ~accessible_world(V_620, V_125) | ~accessible_world(skc9, V_620)))). % 9.61/3.25 tff(c_1716, plain, (![V_95, V_658, V_657]: (event(V_95, skf1(V_658)) | ~accessible_world(V_657, V_95) | ~accessible_world(skc14, V_657)))). % 9.61/3.25 tff(c_2432, plain, (![V_80, V_806]: (thing(V_80, V_806) | ~accessible_world(skc14, V_80) | ~abstraction(skc9, V_806)))). % 9.61/3.25 tff(c_1634, plain, (![V_634, V_609]: (event(V_634, skc10) | ~accessible_world(V_609, V_634) | ~accessible_world(skc9, V_609)))). % 9.61/3.25 tff(c_2236, plain, (![V_140, V_778]: (nonhuman(V_140, V_778) | ~accessible_world(skc14, V_140) | ~abstraction(skc9, V_778)))). % 9.61/3.25 tff(c_1451, plain, (![V_101, V_597]: (human_person(V_101, skc11) | ~accessible_world(V_597, V_101) | ~accessible_world(skc9, V_597)))). % 9.61/3.25 tff(c_1838, plain, (![V_131, V_701]: (relname(V_131, V_701) | ~accessible_world(skc14, V_131) | ~forename(skc9, V_701)))). % 9.61/3.25 tff(c_2163, plain, (![V_86, V_762]: (specific(V_86, V_762) | ~accessible_world(skc14, V_86) | ~eventuality(skc9, V_762)))). % 9.61/3.25 tff(c_1467, plain, (![V_101, V_598]: (human_person(V_101, skc17) | ~accessible_world(V_598, V_101) | ~accessible_world(skc9, V_598)))). % 9.61/3.25 tff(c_1337, plain, (![V_565, V_238, U_237]: (living(V_565, V_238) | ~accessible_world(U_237, V_565) | ~human_person(U_237, V_238)))). % 9.61/3.25 tff(c_1647, plain, (![V_95, V_637]: (event(V_95, skc15) | ~accessible_world(V_637, V_95) | ~accessible_world(skc9, V_637)))). % 9.61/3.25 tff(c_2028, plain, (![W_748, V_746, Y_747, U_196]: (W_748=V_746 | ~agent(skc14, Y_747, U_196) | ~theme(skc14, Y_747, W_748) | ~think_believe_consider(skc14, Y_747) | ~think_believe_consider(skc14, skf1(U_196)) | ~theme(skc14, skf1(U_196), V_746) | ~proposition(skc14, W_748) | ~proposition(skc14, V_746) | ~man(skc14, U_196)))). % 9.61/3.25 tff(c_1999, plain, (![W_735]: (skc16=W_735 | ~forename(skc9, W_735) | ~of(skc9, W_735, skc17)))). % 9.61/3.25 tff(c_1368, plain, (![V_571, V_46, U_45]: (singleton(V_571, V_46) | ~accessible_world(U_45, V_571) | ~abstraction(U_45, V_46)))). % 9.61/3.25 tff(c_1397, plain, (![V_579, V_40, U_39]: (relation(V_579, V_40) | ~accessible_world(U_39, V_579) | ~forename(U_39, V_40)))). % 9.61/3.25 tff(c_1745, plain, (![V_98, V_672]: (man(V_98, skc17) | ~accessible_world(V_672, V_98) | ~accessible_world(skc9, V_672)))). % 9.61/3.25 tff(c_2584, plain, (![V_845]: (skc14=V_845 | ~theme(skc9, skc15, V_845) | ~proposition(skc9, V_845)))). % 9.61/3.25 tff(c_1664, plain, (![V_128, V_642]: (forename(V_128, skc16) | ~accessible_world(V_642, V_128) | ~accessible_world(skc9, V_642)))). % 9.61/3.25 tff(c_1672, plain, (![V_128, V_643]: (forename(V_128, skc12) | ~accessible_world(V_643, V_128) | ~accessible_world(skc9, V_643)))). % 9.61/3.25 tff(c_1996, plain, (![W_735]: (skc12=W_735 | ~forename(skc9, W_735) | ~of(skc9, W_735, skc11)))). % 9.61/3.25 tff(c_1506, plain, (![V_74, V_609]: (state(V_74, skc10) | ~accessible_world(V_609, V_74) | ~accessible_world(skc9, V_609)))). % 9.61/3.25 tff(c_2031, plain, (![W_748, V_746, Y_747]: (W_748=V_746 | ~agent(skc9, Y_747, skc17) | ~theme(skc9, Y_747, W_748) | ~think_believe_consider(skc9, Y_747) | ~theme(skc9, skc15, V_746) | ~proposition(skc9, W_748) | ~proposition(skc9, V_746)))). % 9.61/3.25 tff(c_1591, plain, (![V_158, V_625]: (proposition(V_158, skc14) | ~accessible_world(V_625, V_158) | ~accessible_world(skc9, V_625)))). % 9.61/3.25 tff(c_1366, plain, (![V_571, V_24, U_23]: (singleton(V_571, V_24) | ~accessible_world(U_23, V_571) | ~entity(U_23, V_24)))). % 9.61/3.25 tff(c_1419, plain, (![V_152, V_587]: (present(V_152, skc15) | ~accessible_world(V_587, V_152) | ~accessible_world(skc9, V_587)))). % 9.61/3.25 tff(c_1367, plain, (![V_571, V_4, U_3]: (singleton(V_571, V_4) | ~accessible_world(U_3, V_571) | ~eventuality(U_3, V_4)))). % 9.61/3.25 tff(c_1766, plain, (![V_146, V_674]: (jules_forename(V_146, skc12) | ~accessible_world(V_674, V_146) | ~accessible_world(skc9, V_674)))). % 9.61/3.25 tff(c_1431, plain, (![V_155, V_593]: (think_believe_consider(V_155, skc15) | ~accessible_world(V_593, V_155) | ~accessible_world(skc9, V_593)))). % 9.61/3.25 tff(c_1261, plain, (![V_535, V_238, U_237]: (impartial(V_535, V_238) | ~accessible_world(U_237, V_535) | ~human_person(U_237, V_238)))). % 9.61/3.25 tff(c_1692, plain, (![V_161, V_648]: (vincent_forename(V_161, skc16) | ~accessible_world(V_648, V_161) | ~accessible_world(skc9, V_648)))). % 9.61/3.25 tff(c_2533, plain, (~accessible_world(skc9, skc9))). % 9.61/3.25 tff(c_1904, plain, (![V_713, U_196]: (agent(V_713, skf1(U_196), U_196) | ~accessible_world(skc14, V_713) | ~man(skc14, U_196)))). % 9.61/3.25 tff(c_1757, plain, (![V_98, V_673]: (man(V_98, skc11) | ~accessible_world(V_673, V_98) | ~accessible_world(skc9, V_673)))). % 9.61/3.25 tff(c_2488, plain, (![V_28]: (~eventuality(skc9, V_28) | ~entity(skc14, V_28)))). % 9.61/3.25 tff(c_2512, plain, (![V_195]: (~entity(skc9, skf1(V_195))))). % 9.61/3.25 tff(c_2478, plain, (![V_16]: (~entity(skc9, V_16) | ~event(skc14, V_16)))). % 9.61/3.25 tff(c_2461, plain, (![V_815]: (~existent(skc14, V_815) | ~eventuality(skc9, V_815)))). % 9.61/3.25 tff(c_2449, plain, (![V_811]: (~eventuality(skc14, V_811) | ~entity(skc9, V_811)))). % 9.61/3.25 tff(c_2453, plain, (![V_813]: (nonexistent(skc14, V_813) | ~eventuality(skc9, V_813)))). % 9.61/3.25 tff(c_1315, plain, (![V_558, V_10, U_9]: (nonexistent(V_558, V_10) | ~accessible_world(U_9, V_558) | ~eventuality(U_9, V_10)))). % 9.61/3.25 tff(c_2441, plain, (![V_809]: (existent(skc14, V_809) | ~entity(skc9, V_809)))). % 9.61/3.25 tff(c_1722, plain, (![V_659, V_28, U_27]: (existent(V_659, V_28) | ~accessible_world(U_27, V_659) | ~entity(U_27, V_28)))). % 9.61/3.25 tff(c_2433, plain, (![V_806]: (singleton(skc14, V_806) | ~abstraction(skc9, V_806)))). % 9.61/3.25 tff(c_2425, plain, (![V_804]: (thing(skc14, V_804) | ~abstraction(skc9, V_804)))). % 9.61/3.25 tff(c_1485, plain, (![V_600, V_46, U_45]: (thing(V_600, V_46) | ~accessible_world(U_45, V_600) | ~abstraction(U_45, V_46)))). % 9.61/3.25 tff(c_2406, plain, (![V_801]: (~male(skc14, V_801) | ~eventuality(skc9, V_801)))). % 9.61/3.25 tff(c_2397, plain, (![V_798]: (unisex(skc14, V_798) | ~eventuality(skc9, V_798)))). % 9.61/3.25 tff(c_2393, plain, (![V_195]: (~abstraction(skc9, skf1(V_195))))). % 9.61/3.25 tff(c_1780, plain, (![V_678, V_12, U_11]: (unisex(V_678, V_12) | ~accessible_world(U_11, V_678) | ~eventuality(U_11, V_12)))). % 9.61/3.25 tff(c_2332, plain, (![V_16]: (~abstraction(skc9, V_16) | ~event(skc14, V_16)))). % 9.61/3.25 tff(c_2315, plain, (![V_792]: (singleton(skc14, V_792) | ~eventuality(skc9, V_792)))). % 9.61/3.25 tff(c_2288, plain, (![V_787]: (~entity(skc14, V_787) | ~abstraction(skc9, V_787)))). % 9.61/3.25 tff(c_2287, plain, (![V_787]: (~eventuality(skc14, V_787) | ~abstraction(skc9, V_787)))). % 9.61/3.25 tff(c_2307, plain, (![V_790]: (thing(skc14, V_790) | ~eventuality(skc9, V_790)))). % 9.61/3.25 tff(c_1484, plain, (![V_600, V_4, U_3]: (thing(V_600, V_4) | ~accessible_world(U_3, V_600) | ~eventuality(U_3, V_4)))). % 9.61/3.25 tff(c_2268, plain, (![V_786]: (~male(skc14, V_786) | ~abstraction(skc9, V_786)))). % 9.61/3.25 tff(c_2260, plain, (![V_784]: (general(skc14, V_784) | ~abstraction(skc9, V_784)))). % 9.61/3.25 tff(c_2256, plain, (![V_781]: (unisex(skc14, V_781) | ~abstraction(skc9, V_781)))). % 9.61/3.25 tff(c_1703, plain, (![V_651, V_50, U_49]: (general(V_651, V_50) | ~accessible_world(U_49, V_651) | ~abstraction(U_49, V_50)))). % 9.61/3.25 tff(c_1781, plain, (![V_678, V_52, U_51]: (unisex(V_678, V_52) | ~accessible_world(U_51, V_678) | ~abstraction(U_51, V_52)))). % 9.61/3.25 tff(c_2237, plain, (![V_778]: (~human(skc14, V_778) | ~abstraction(skc9, V_778)))). % 9.61/3.25 tff(c_2229, plain, (![V_776]: (nonhuman(skc14, V_776) | ~abstraction(skc9, V_776)))). % 9.61/3.25 tff(c_1266, plain, (![V_540, V_48, U_47]: (nonhuman(V_540, V_48) | ~accessible_world(U_47, V_540) | ~abstraction(U_47, V_48)))). % 9.61/3.25 tff(c_2221, plain, (![V_773]: (singleton(skc14, V_773) | ~entity(skc9, V_773)))). % 9.61/3.25 tff(c_2213, plain, (![V_771]: (thing(skc14, V_771) | ~entity(skc9, V_771)))). % 9.61/3.25 tff(c_1483, plain, (![V_600, V_24, U_23]: (thing(V_600, V_24) | ~accessible_world(U_23, V_600) | ~entity(U_23, V_24)))). % 9.61/3.25 tff(c_2197, plain, (![V_768]: (abstraction(skc14, V_768) | ~proposition(skc9, V_768)))). % 9.61/3.25 tff(c_2189, plain, (![V_766]: (relation(skc14, V_766) | ~proposition(skc9, V_766)))). % 9.61/3.25 tff(c_1398, plain, (![V_579, V_58, U_57]: (relation(V_579, V_58) | ~accessible_world(U_57, V_579) | ~proposition(U_57, V_58)))). % 9.61/3.25 tff(c_2170, plain, (![V_50]: (~eventuality(skc9, V_50) | ~abstraction(skc14, V_50)))). % 9.61/3.25 tff(c_2164, plain, (![V_762]: (~general(skc14, V_762) | ~eventuality(skc9, V_762)))). % 9.61/3.25 tff(c_2156, plain, (![V_760]: (specific(skc14, V_760) | ~eventuality(skc9, V_760)))). % 9.61/3.25 tff(c_1774, plain, (![V_675, V_8, U_7]: (specific(V_675, V_8) | ~accessible_world(U_7, V_675) | ~eventuality(U_7, V_8)))). % 9.61/3.26 tff(c_2123, plain, (![V_50]: (~entity(skc9, V_50) | ~abstraction(skc14, V_50)))). % 9.61/3.26 tff(c_2117, plain, (![V_756]: (~general(skc14, V_756) | ~entity(skc9, V_756)))). % 9.61/3.26 tff(c_2109, plain, (![V_754]: (specific(skc14, V_754) | ~entity(skc9, V_754)))). % 9.61/3.26 tff(c_1773, plain, (![V_675, V_26, U_25]: (specific(V_675, V_26) | ~accessible_world(U_25, V_675) | ~entity(U_25, V_26)))). % 9.61/3.26 tff(c_2057, plain, (![V_750]: (~abstraction(skc14, V_750) | ~event(skc9, V_750)))). % 9.61/3.26 tff(c_2081, plain, (~entity(skc14, skc15))). % 9.61/3.26 tff(c_2080, plain, (~entity(skc14, skc10))). % 9.61/3.26 tff(c_2056, plain, (![V_750]: (~entity(skc14, V_750) | ~event(skc9, V_750)))). % 9.61/3.26 tff(c_2019, plain, (![V_742]: (eventuality(skc14, V_742) | ~event(skc9, V_742)))). % 9.61/3.26 tff(c_142, plain, (![Z_186, V_189, X_187, Y_188, U_185, W_184]: (W_184=V_189 | ~agent(U_185, X_187, Z_186) | ~agent(U_185, Y_188, Z_186) | ~theme(U_185, Y_188, W_184) | ~think_believe_consider(U_185, Y_188) | ~think_believe_consider(U_185, X_187) | ~theme(U_185, X_187, V_189) | ~proposition(U_185, W_184) | ~proposition(U_185, V_189)))). % 9.61/3.26 tff(c_1609, plain, (![V_628, V_16, U_15]: (eventuality(V_628, V_16) | ~accessible_world(U_15, V_628) | ~event(U_15, V_16)))). % 9.61/3.26 tff(c_1967, plain, (![V_729]: (be(V_729, skc10, skc11, skc11) | ~accessible_world(skc9, V_729)))). % 9.61/3.26 tff(c_1952, plain, (![V_720]: (of(V_720, skc12, skc11) | ~accessible_world(skc9, V_720)))). % 9.61/3.26 tff(c_140, plain, (![W_182, V_181, U_180, X_183]: (W_182=V_181 | ~entity(U_180, X_183) | ~of(U_180, V_181, X_183) | ~forename(U_180, W_182) | ~of(U_180, W_182, X_183) | ~forename(U_180, V_181)))). % 9.61/3.26 tff(c_1905, plain, (![V_713]: (agent(V_713, skc15, skc17) | ~accessible_world(skc9, V_713)))). % 9.61/3.26 tff(c_1953, plain, (![V_720]: (of(V_720, skc16, skc17) | ~accessible_world(skc9, V_720)))). % 9.61/3.26 tff(c_1975, plain, (![V_730]: (~abstraction(V_730, skc17) | ~accessible_world(skc14, V_730)))). % 9.61/3.26 tff(c_1963, plain, (![V_724]: (~abstraction(V_724, skc11) | ~accessible_world(skc14, V_724)))). % 9.61/3.26 tff(c_1937, plain, (![V_107]: (entity(V_107, skc17) | ~accessible_world(skc14, V_107)))). % 9.61/3.26 tff(c_138, plain, (![X_177, Y_178, U_176, W_175, V_179]: (be(V_179, W_175, X_177, Y_178) | ~be(U_176, W_175, X_177, Y_178) | ~accessible_world(U_176, V_179)))). % 9.61/3.26 tff(c_1930, plain, (![V_107]: (entity(V_107, skc11) | ~accessible_world(skc14, V_107)))). % 9.61/3.26 tff(c_132, plain, (![V_164, W_165, X_166, U_163]: (of(V_164, W_165, X_166) | ~of(U_163, W_165, X_166) | ~accessible_world(U_163, V_164)))). % 9.61/3.26 tff(c_1897, plain, (![V_712]: (impartial(skc14, V_712) | ~human_person(skc9, V_712)))). % 9.61/3.26 tff(c_1898, plain, (![V_712]: (living(skc14, V_712) | ~human_person(skc9, V_712)))). % 9.61/3.26 tff(c_1924, plain, (entity(skc14, skc17))). % 9.61/3.26 tff(c_1923, plain, (entity(skc14, skc11))). % 9.61/3.26 tff(c_1896, plain, (![V_712]: (entity(skc14, V_712) | ~human_person(skc9, V_712)))). % 9.61/3.26 tff(c_134, plain, (![V_168, W_169, X_170, U_167]: (agent(V_168, W_169, X_170) | ~agent(U_167, W_169, X_170) | ~accessible_world(U_167, V_168)))). % 9.61/3.26 tff(c_1882, plain, (![V_710]: (organism(skc14, V_710) | ~human_person(skc9, V_710)))). % 9.61/3.26 tff(c_1827, plain, (![V_695, V_20, U_19]: (organism(V_695, V_20) | ~accessible_world(U_19, V_695) | ~human_person(U_19, V_20)))). % 9.61/3.26 tff(c_1874, plain, (![V_704]: (theme(V_704, skc15, skc14) | ~accessible_world(skc9, V_704)))). % 9.61/3.26 tff(c_136, plain, (![V_172, W_173, X_174, U_171]: (theme(V_172, W_173, X_174) | ~theme(U_171, W_173, X_174) | ~accessible_world(U_171, V_172)))). % 9.61/3.26 tff(c_1847, plain, (![V_702]: (abstraction(skc14, V_702) | ~forename(skc9, V_702)))). % 9.61/3.26 tff(c_1839, plain, (![V_701]: (relation(skc14, V_701) | ~forename(skc9, V_701)))). % 9.61/3.26 tff(c_1831, plain, (![V_699]: (relname(skc14, V_699) | ~forename(skc9, V_699)))). % 9.61/3.26 tff(c_1810, plain, (![V_689, V_40, U_39]: (relname(V_689, V_40) | ~accessible_world(U_39, V_689) | ~forename(U_39, V_40)))). % 9.61/3.26 tff(c_92, plain, (![V_104, W_105, U_103]: (organism(V_104, W_105) | ~organism(U_103, W_105) | ~accessible_world(U_103, V_104)))). % 9.61/3.26 tff(c_104, plain, (![V_122, W_123, U_121]: (animate(V_122, W_123) | ~animate(U_121, W_123) | ~accessible_world(U_121, V_122)))). % 9.61/3.26 tff(c_110, plain, (![V_131, W_132, U_130]: (relname(V_131, W_132) | ~relname(U_130, W_132) | ~accessible_world(U_130, V_131)))). % 9.61/3.26 tff(c_94, plain, (![V_107, W_108, U_106]: (entity(V_107, W_108) | ~entity(U_106, W_108) | ~accessible_world(U_106, V_107)))). % 9.61/3.26 tff(c_1785, plain, (![V_681, V_191]: (smoke(V_681, skf1(V_191)) | ~accessible_world(skc14, V_681)))). % 9.61/3.26 tff(c_122, plain, (![V_149, W_150, U_148]: (smoke(V_149, W_150) | ~smoke(U_148, W_150) | ~accessible_world(U_148, V_149)))). % 9.61/3.26 tff(c_84, plain, (![V_92, W_93, U_91]: (unisex(V_92, W_93) | ~unisex(U_91, W_93) | ~accessible_world(U_91, V_92)))). % 9.61/3.26 tff(c_80, plain, (![V_86, W_87, U_85]: (specific(V_86, W_87) | ~specific(U_85, W_87) | ~accessible_world(U_85, V_86)))). % 9.61/3.26 tff(c_1735, plain, (![V_669]: (jules_forename(V_669, skc12) | ~accessible_world(skc9, V_669)))). % 9.61/3.26 tff(c_1731, plain, (![V_666]: (man(V_666, skc11) | ~accessible_world(skc9, V_666)))). % 9.61/3.26 tff(c_1730, plain, (![V_666]: (man(V_666, skc17) | ~accessible_world(skc9, V_666)))). % 9.61/3.26 tff(c_120, plain, (![V_146, W_147, U_145]: (jules_forename(V_146, W_147) | ~jules_forename(U_145, W_147) | ~accessible_world(U_145, V_146)))). % 9.61/3.26 tff(c_88, plain, (![V_98, W_99, U_97]: (man(V_98, W_99) | ~man(U_97, W_99) | ~accessible_world(U_97, V_98)))). % 9.61/3.26 tff(c_1718, plain, (![V_657, V_658]: (~entity(V_657, skf1(V_658)) | ~accessible_world(skc14, V_657)))). % 9.61/3.26 tff(c_1717, plain, (![V_657, V_658]: (~abstraction(V_657, skf1(V_658)) | ~accessible_world(skc14, V_657)))). % 9.61/3.26 tff(c_96, plain, (![V_110, W_111, U_109]: (existent(V_110, W_111) | ~existent(U_109, W_111) | ~accessible_world(U_109, V_110)))). % 9.61/3.26 tff(c_1635, plain, (![V_634, V_195]: (event(V_634, skf1(V_195)) | ~accessible_world(skc14, V_634)))). % 9.61/3.26 tff(c_1623, plain, (![V_137]: (abstraction(V_137, skc12) | ~accessible_world(skc14, V_137)))). % 9.61/3.26 tff(c_1551, plain, (![V_137]: (abstraction(V_137, skc14) | ~accessible_world(skc14, V_137)))). % 9.61/3.26 tff(c_1681, plain, (![V_137]: (abstraction(V_137, skc16) | ~accessible_world(skc14, V_137)))). % 9.61/3.26 tff(c_1699, plain, (~abstraction(skc14, skc15))). % 9.61/3.26 tff(c_118, plain, (![V_143, W_144, U_142]: (general(V_143, W_144) | ~general(U_142, W_144) | ~accessible_world(U_142, V_143)))). % 9.61/3.26 tff(c_1648, plain, (![V_637]: (~abstraction(V_637, skc15) | ~accessible_world(skc9, V_637)))). % 9.61/3.26 tff(c_1649, plain, (![V_637]: (~entity(V_637, skc15) | ~accessible_world(skc9, V_637)))). % 9.61/3.26 tff(c_1685, plain, (![V_645]: (vincent_forename(V_645, skc16) | ~accessible_world(skc9, V_645)))). % 9.61/3.26 tff(c_130, plain, (![V_161, W_162, U_160]: (vincent_forename(V_161, W_162) | ~vincent_forename(U_160, W_162) | ~accessible_world(U_160, V_161)))). % 9.61/3.26 tff(c_1678, plain, (abstraction(skc14, skc16))). % 9.61/3.26 tff(c_1665, plain, (![V_642]: (abstraction(V_642, skc16) | ~accessible_world(skc9, V_642)))). % 9.61/3.26 tff(c_1657, plain, (![V_639]: (forename(V_639, skc12) | ~accessible_world(skc9, V_639)))). % 9.61/3.26 tff(c_1656, plain, (![V_639]: (forename(V_639, skc16) | ~accessible_world(skc9, V_639)))). % 9.61/3.26 tff(c_108, plain, (![V_128, W_129, U_127]: (forename(V_128, W_129) | ~forename(U_127, W_129) | ~accessible_world(U_127, V_128)))). % 9.61/3.26 tff(c_1615, plain, (![U_15]: (~accessible_world(skc9, U_15) | ~event(U_15, skc11)))). % 9.61/3.26 tff(c_1637, plain, (![V_634]: (event(V_634, skc15) | ~accessible_world(skc9, V_634)))). % 9.61/3.26 tff(c_86, plain, (![V_95, W_96, U_94]: (event(V_95, W_96) | ~event(U_94, W_96) | ~accessible_world(U_94, V_95)))). % 9.61/3.26 tff(c_1599, plain, (![U_15]: (~accessible_world(skc9, U_15) | ~event(U_15, skc17)))). % 9.61/3.26 tff(c_1620, plain, (abstraction(skc14, skc12))). % 9.61/3.26 tff(c_1516, plain, (![V_610]: (abstraction(V_610, skc12) | ~accessible_world(skc9, V_610)))). % 9.61/3.26 tff(c_1563, plain, (![V_619]: (~eventuality(V_619, skc11) | ~accessible_world(skc9, V_619)))). % 9.61/3.26 tff(c_74, plain, (![V_77, W_78, U_76]: (eventuality(V_77, W_78) | ~eventuality(U_76, W_78) | ~accessible_world(U_76, V_77)))). % 9.61/3.26 tff(c_1575, plain, (![V_620]: (~eventuality(V_620, skc17) | ~accessible_world(skc9, V_620)))). % 9.61/3.26 tff(c_1535, plain, (![V_614]: (~entity(V_614, skc10) | ~accessible_world(skc9, V_614)))). % 9.61/3.26 tff(c_1584, plain, (![V_622]: (proposition(V_622, skc14) | ~accessible_world(skc9, V_622)))). % 9.61/3.26 tff(c_128, plain, (![V_158, W_159, U_157]: (proposition(V_158, W_159) | ~proposition(U_157, W_159) | ~accessible_world(U_157, V_158)))). % 9.61/3.26 tff(c_1580, plain, (~abstraction(skc14, skc10))). % 9.61/3.26 tff(c_1536, plain, (![V_614]: (~abstraction(V_614, skc10) | ~accessible_world(skc9, V_614)))). % 9.61/3.26 tff(c_1548, plain, (![V_616]: (male(V_616, skc17) | ~accessible_world(skc9, V_616)))). % 9.61/3.26 tff(c_1547, plain, (![V_616]: (male(V_616, skc11) | ~accessible_world(skc9, V_616)))). % 9.61/3.26 tff(c_1541, plain, (abstraction(skc14, skc14))). % 9.61/3.26 tff(c_106, plain, (![V_125, W_126, U_124]: (male(V_125, W_126) | ~male(U_124, W_126) | ~accessible_world(U_124, V_125)))). % 9.61/3.26 tff(c_1518, plain, (![V_610]: (abstraction(V_610, skc14) | ~accessible_world(skc9, V_610)))). % 9.61/3.26 tff(c_1508, plain, (![V_609]: (eventuality(V_609, skc10) | ~accessible_world(skc9, V_609)))). % 9.61/3.26 tff(c_1507, plain, (![V_609]: (event(V_609, skc10) | ~accessible_world(skc9, V_609)))). % 9.61/3.26 tff(c_114, plain, (![V_137, W_138, U_136]: (abstraction(V_137, W_138) | ~abstraction(U_136, W_138) | ~accessible_world(U_136, V_137)))). % 9.61/3.26 tff(c_1496, plain, (![V_606]: (state(V_606, skc10) | ~accessible_world(skc9, V_606)))). % 9.61/3.26 tff(c_72, plain, (![V_74, W_75, U_73]: (state(V_74, W_75) | ~state(U_73, W_75) | ~accessible_world(U_73, V_74)))). % 9.61/3.27 tff(c_1468, plain, (![V_598]: (entity(V_598, skc17) | ~accessible_world(skc9, V_598)))). % 9.61/3.27 tff(c_1470, plain, (![V_598]: (animate(V_598, skc17) | ~accessible_world(skc9, V_598)))). % 9.61/3.27 tff(c_1454, plain, (![V_597]: (animate(V_597, skc11) | ~accessible_world(skc9, V_597)))). % 9.61/3.27 tff(c_76, plain, (![V_80, W_81, U_79]: (thing(V_80, W_81) | ~thing(U_79, W_81) | ~accessible_world(U_79, V_80)))). % 9.61/3.27 tff(c_1452, plain, (![V_597]: (entity(V_597, skc11) | ~accessible_world(skc9, V_597)))). % 9.61/3.27 tff(c_1438, plain, (![V_594]: (human_person(V_594, skc17) | ~accessible_world(skc9, V_594)))). % 9.61/3.27 tff(c_1437, plain, (![V_594]: (human_person(V_594, skc11) | ~accessible_world(skc9, V_594)))). % 9.61/3.27 tff(c_90, plain, (![V_101, W_102, U_100]: (human_person(V_101, W_102) | ~human_person(U_100, W_102) | ~accessible_world(U_100, V_101)))). % 9.61/3.27 tff(c_1427, plain, (![V_590]: (think_believe_consider(V_590, skc15) | ~accessible_world(skc9, V_590)))). % 9.61/3.27 tff(c_126, plain, (![V_155, W_156, U_154]: (think_believe_consider(V_155, W_156) | ~think_believe_consider(U_154, W_156) | ~accessible_world(U_154, V_155)))). % 9.61/3.27 tff(c_1414, plain, (![V_584, V_193]: (present(V_584, skf1(V_193)) | ~accessible_world(skc14, V_584)))). % 9.61/3.27 tff(c_1415, plain, (![V_584]: (present(V_584, skc15) | ~accessible_world(skc9, V_584)))). % 9.61/3.27 tff(c_1408, plain, (~abstraction(skc14, skc11))). % 9.61/3.27 tff(c_124, plain, (![V_152, W_153, U_151]: (present(V_152, W_153) | ~present(U_151, W_153) | ~accessible_world(U_151, V_152)))). % 9.61/3.27 tff(c_1391, plain, (![V_578]: (~abstraction(V_578, skc11) | ~accessible_world(skc9, V_578)))). % 9.61/3.27 tff(c_1403, plain, (~abstraction(skc14, skc17))). % 9.61/3.27 tff(c_1345, plain, (![V_568]: (~abstraction(V_568, skc17) | ~accessible_world(skc9, V_568)))). % 9.61/3.27 tff(c_112, plain, (![V_134, W_135, U_133]: (relation(V_134, W_135) | ~relation(U_133, W_135) | ~accessible_world(U_133, V_134)))). % 9.61/3.27 tff(c_1293, plain, (![V_551]: (human(V_551, skc11) | ~accessible_world(skc9, V_551)))). % 9.61/3.27 tff(c_1380, plain, (![V_195]: (~abstraction(skc14, skf1(V_195))))). % 9.61/3.27 tff(c_1382, plain, (~abstraction(skc9, skc15))). % 9.61/3.27 tff(c_1324, plain, (![U_15, V_16]: (~abstraction(U_15, V_16) | ~event(U_15, V_16)))). % 9.61/3.27 tff(c_1356, plain, (![V_195]: (~entity(skc14, skf1(V_195))))). % 9.61/3.27 tff(c_78, plain, (![V_83, W_84, U_82]: (singleton(V_83, W_84) | ~singleton(U_82, W_84) | ~accessible_world(U_82, V_83)))). % 9.61/3.27 tff(c_1358, plain, (~entity(skc9, skc15))). % 9.61/3.27 tff(c_1333, plain, (![U_15, V_16]: (~entity(U_15, V_16) | ~event(U_15, V_16)))). % 9.61/3.27 tff(c_1292, plain, (![V_551]: (human(V_551, skc17) | ~accessible_world(skc9, V_551)))). % 9.61/3.27 tff(c_100, plain, (![V_116, W_117, U_115]: (living(V_116, W_117) | ~living(U_115, W_117) | ~accessible_world(U_115, V_116)))). % 9.61/3.27 tff(c_1332, plain, (~entity(skc9, skc10))). % 9.61/3.27 tff(c_1235, plain, (![U_27, V_28]: (~eventuality(U_27, V_28) | ~entity(U_27, V_28)))). % 9.61/3.27 tff(c_1323, plain, (~abstraction(skc9, skc10))). % 9.61/3.27 tff(c_1248, plain, (![U_49, V_50]: (~eventuality(U_49, V_50) | ~abstraction(U_49, V_50)))). % 9.61/3.27 tff(c_1311, plain, (abstraction(skc9, skc12))). % 9.61/3.27 tff(c_82, plain, (![V_89, W_90, U_88]: (nonexistent(V_89, W_90) | ~nonexistent(U_88, W_90) | ~accessible_world(U_88, V_89)))). % 9.61/3.27 tff(c_1310, plain, (abstraction(skc9, skc16))). % 9.61/3.27 tff(c_1286, plain, (![U_549, V_550]: (abstraction(U_549, V_550) | ~forename(U_549, V_550)))). % 9.61/3.27 tff(c_1241, plain, (![U_49, V_50]: (~entity(U_49, V_50) | ~abstraction(U_49, V_50)))). % 9.61/3.27 tff(c_102, plain, (![V_119, W_120, U_118]: (human(V_119, W_120) | ~human(U_118, W_120) | ~accessible_world(U_118, V_119)))). % 9.61/3.27 tff(c_229, plain, (![U_39, V_40]: (relation(U_39, V_40) | ~forename(U_39, V_40)))). % 9.61/3.27 tff(c_1281, plain, (abstraction(skc9, skc14))). % 9.61/3.27 tff(c_224, plain, (![U_57, V_58]: (abstraction(U_57, V_58) | ~proposition(U_57, V_58)))). % 9.61/3.27 tff(c_279, plain, (![U_23, V_24]: (singleton(U_23, V_24) | ~entity(U_23, V_24)))). % 9.61/3.27 tff(c_207, plain, (![U_215, V_216]: (~male(U_215, V_216) | ~abstraction(U_215, V_216)))). % 9.61/3.27 tff(c_116, plain, (![V_140, W_141, U_139]: (nonhuman(V_140, W_141) | ~nonhuman(U_139, W_141) | ~accessible_world(U_139, V_140)))). % 9.61/3.27 tff(c_255, plain, (![U_237, V_238]: (living(U_237, V_238) | ~human_person(U_237, V_238)))). % 9.61/3.27 tff(c_1257, plain, (~abstraction(skc9, skc11))). % 9.61/3.27 tff(c_1256, plain, (~abstraction(skc9, skc17))). % 9.61/3.27 tff(c_98, plain, (![V_113, W_114, U_112]: (impartial(V_113, W_114) | ~impartial(U_112, W_114) | ~accessible_world(U_112, V_113)))). % 9.61/3.27 tff(c_268, plain, (![U_47, V_48]: (~human(U_47, V_48) | ~abstraction(U_47, V_48)))). % 9.61/3.27 tff(c_218, plain, (![U_7, V_8]: (~general(U_7, V_8) | ~eventuality(U_7, V_8)))). % 9.61/3.27 tff(c_254, plain, (![U_237, V_238]: (impartial(U_237, V_238) | ~human_person(U_237, V_238)))). % 9.61/3.27 tff(c_280, plain, (![U_3, V_4]: (singleton(U_3, V_4) | ~eventuality(U_3, V_4)))). % 9.61/3.27 tff(c_339, plain, (![U_261, V_262]: (~general(U_261, V_262) | ~entity(U_261, V_262)))). % 9.61/3.27 tff(c_188, plain, (![U_196]: (agent(skc14, skf1(U_196), U_196) | ~man(skc14, U_196)))). % 9.61/3.27 tff(c_316, plain, (![U_255, V_256]: (~existent(U_255, V_256) | ~eventuality(U_255, V_256)))). % 9.61/3.27 tff(c_1229, plain, (![V_193]: (present(skc14, skf1(V_193))))). % 9.61/3.27 tff(c_894, plain, (entity(skc9, skc17))). % 9.61/3.27 tff(c_893, plain, (entity(skc9, skc11))). % 9.61/3.27 tff(c_286, plain, (![U_19, V_20]: (entity(U_19, V_20) | ~human_person(U_19, V_20)))). % 9.61/3.27 tff(c_879, plain, (![V_191]: (smoke(skc14, skf1(V_191))))). % 9.61/3.27 tff(c_368, plain, (be(skc9, skc10, skc11, skc11))). % 9.61/3.27 tff(c_369, plain, (of(skc9, skc12, skc11))). % 9.61/3.27 tff(c_388, plain, (~event(skc9, skc17))). % 9.61/3.27 tff(c_676, plain, (![V_195]: (event(skc14, skf1(V_195))))). % 9.61/3.27 tff(c_384, plain, (~event(skc9, skc11))). % 9.61/3.27 tff(c_358, plain, (~eventuality(skc9, skc17))). % 9.61/3.27 tff(c_380, plain, (~eventuality(skc9, skc11))). % 9.61/3.27 tff(c_363, plain, (skc13=skc11)). % 9.61/3.27 tff(c_70, plain, (![X_72, W_71, U_69, V_70]: (X_72=W_71 | ~be(U_69, V_70, W_71, X_72)))). % 9.61/3.27 tff(c_344, plain, (![U_263, V_264]: (~male(U_263, V_264) | ~eventuality(U_263, V_264)))). % 9.61/3.27 tff(c_281, plain, (![U_45, V_46]: (singleton(U_45, V_46) | ~abstraction(U_45, V_46)))). % 9.61/3.27 tff(c_12, plain, (![U_11, V_12]: (unisex(U_11, V_12) | ~eventuality(U_11, V_12)))). % 9.61/3.27 tff(c_26, plain, (![U_25, V_26]: (specific(U_25, V_26) | ~entity(U_25, V_26)))). % 9.61/3.27 tff(c_334, plain, (human(skc9, skc17))). % 9.61/3.27 tff(c_333, plain, (human(skc9, skc11))). % 9.61/3.27 tff(c_34, plain, (![U_33, V_34]: (human(U_33, V_34) | ~human_person(U_33, V_34)))). % 9.61/3.27 tff(c_321, plain, (event(skc9, skc10))). % 9.61/3.27 tff(c_14, plain, (![U_13, V_14]: (event(U_13, V_14) | ~state(U_13, V_14)))). % 9.61/3.27 tff(c_307, plain, (animate(skc9, skc11))). % 9.61/3.27 tff(c_303, plain, (animate(skc9, skc17))). % 9.61/3.27 tff(c_10, plain, (![U_9, V_10]: (nonexistent(U_9, V_10) | ~eventuality(U_9, V_10)))). % 9.61/3.27 tff(c_298, plain, (human_person(skc9, skc11))). % 9.61/3.27 tff(c_297, plain, (human_person(skc9, skc17))). % 9.61/3.27 tff(c_18, plain, (![U_17, V_18]: (human_person(U_17, V_18) | ~man(U_17, V_18)))). % 9.61/3.27 tff(c_22, plain, (![U_21, V_22]: (entity(U_21, V_22) | ~organism(U_21, V_22)))). % 9.61/3.27 tff(c_6, plain, (![U_5, V_6]: (singleton(U_5, V_6) | ~thing(U_5, V_6)))). % 9.61/3.27 tff(c_66, plain, (![U_65, V_66]: (~nonhuman(U_65, V_66) | ~human(U_65, V_66)))). % 9.61/3.27 tff(c_24, plain, (![U_23, V_24]: (thing(U_23, V_24) | ~entity(U_23, V_24)))). % 9.61/3.27 tff(c_261, plain, (eventuality(skc9, skc10))). % 9.61/3.27 tff(c_28, plain, (![U_27, V_28]: (existent(U_27, V_28) | ~entity(U_27, V_28)))). % 9.61/3.27 tff(c_2, plain, (![U_1, V_2]: (eventuality(U_1, V_2) | ~state(U_1, V_2)))). % 9.61/3.27 tff(c_36, plain, (![U_35, V_36]: (animate(U_35, V_36) | ~human_person(U_35, V_36)))). % 9.61/3.27 tff(c_20, plain, (![U_19, V_20]: (organism(U_19, V_20) | ~human_person(U_19, V_20)))). % 9.61/3.27 tff(c_16, plain, (![U_15, V_16]: (eventuality(U_15, V_16) | ~event(U_15, V_16)))). % 9.61/3.27 tff(c_30, plain, (![U_29, V_30]: (impartial(U_29, V_30) | ~organism(U_29, V_30)))). % 9.61/3.27 tff(c_68, plain, (![U_67, V_68]: (~existent(U_67, V_68) | ~nonexistent(U_67, V_68)))). % 9.61/3.27 tff(c_242, plain, (male(skc9, skc11))). % 9.61/3.27 tff(c_241, plain, (male(skc9, skc17))). % 9.61/3.27 tff(c_38, plain, (![U_37, V_38]: (male(U_37, V_38) | ~man(U_37, V_38)))). % 9.61/3.27 tff(c_4, plain, (![U_3, V_4]: (thing(U_3, V_4) | ~eventuality(U_3, V_4)))). % 9.61/3.27 tff(c_42, plain, (![U_41, V_42]: (relation(U_41, V_42) | ~relname(U_41, V_42)))). % 9.61/3.27 tff(c_44, plain, (![U_43, V_44]: (abstraction(U_43, V_44) | ~relation(U_43, V_44)))). % 9.61/3.27 tff(c_56, plain, (![U_55, V_56]: (event(U_55, V_56) | ~smoke(U_55, V_56)))). % 9.61/3.27 tff(c_64, plain, (![U_63, V_64]: (~specific(U_63, V_64) | ~general(U_63, V_64)))). % 9.61/3.27 tff(c_54, plain, (![U_53, V_54]: (forename(U_53, V_54) | ~jules_forename(U_53, V_54)))). % 9.61/3.27 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~abstraction(U_51, V_52)))). % 9.61/3.27 tff(c_50, plain, (![U_49, V_50]: (general(U_49, V_50) | ~abstraction(U_49, V_50)))). % 9.61/3.27 tff(c_40, plain, (![U_39, V_40]: (relname(U_39, V_40) | ~forename(U_39, V_40)))). % 9.61/3.27 tff(c_58, plain, (![U_57, V_58]: (relation(U_57, V_58) | ~proposition(U_57, V_58)))). % 9.61/3.27 tff(c_48, plain, (![U_47, V_48]: (nonhuman(U_47, V_48) | ~abstraction(U_47, V_48)))). % 9.61/3.27 tff(c_60, plain, (![U_59, V_60]: (forename(U_59, V_60) | ~vincent_forename(U_59, V_60)))). % 9.61/3.28 tff(c_62, plain, (![U_61, V_62]: (~unisex(U_61, V_62) | ~male(U_61, V_62)))). % 9.61/3.28 tff(c_8, plain, (![U_7, V_8]: (specific(U_7, V_8) | ~eventuality(U_7, V_8)))). % 9.61/3.28 tff(c_46, plain, (![U_45, V_46]: (thing(U_45, V_46) | ~abstraction(U_45, V_46)))). % 9.61/3.28 tff(c_32, plain, (![U_31, V_32]: (living(U_31, V_32) | ~organism(U_31, V_32)))). % 9.61/3.28 tff(c_174, plain, (agent(skc9, skc15, skc17))). % 9.61/3.28 tff(c_176, plain, (theme(skc9, skc15, skc14))). % 9.61/3.28 tff(c_172, plain, (of(skc9, skc16, skc17))). % 9.61/3.28 tff(c_146, plain, (man(skc9, skc17))). % 9.61/3.28 tff(c_150, plain, (vincent_forename(skc9, skc16))). % 9.61/3.28 tff(c_148, plain, (forename(skc9, skc16))). % 9.61/3.28 tff(c_168, plain, (accessible_world(skc9, skc14))). % 9.61/3.28 tff(c_166, plain, (state(skc9, skc10))). % 9.61/3.28 tff(c_164, plain, (man(skc9, skc11))). % 9.61/3.28 tff(c_162, plain, (jules_forename(skc9, skc12))). % 9.61/3.28 tff(c_160, plain, (forename(skc9, skc12))). % 9.61/3.28 tff(c_152, plain, (event(skc9, skc15))). % 9.61/3.28 tff(c_154, plain, (present(skc9, skc15))). % 9.61/3.28 tff(c_156, plain, (think_believe_consider(skc9, skc15))). % 9.61/3.28 tff(c_170, plain, (proposition(skc9, skc14))). % 9.61/3.28 tff(c_144, plain, (actual_world(skc9))). % 9.61/3.28 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.61/3.28 %------------------------------------------------------------------------------