%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP126-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n016.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:19 PM UTC 2025 % Result : Satisfiable 5.49s 2.40s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP126-10 : TPTP v9.0.0. Released v7.5.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.33 % Computer : n016.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Apr 8 08:39:23 EDT 2025 % 0.13/0.34 % CPUTime : % 5.49/2.40 % 5.49/2.40 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.49/2.40 % 5.49/2.40 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.49/2.41 %$ ifeq3 > ifeq2 > ifeq > of > in > down > agent > white > way > vehicle > unisex > tuple > transport > thing > street > specific > singleton > relname > relation > present > placename > old > object > nonliving > nonhuman > nonexistent > lonely > location > instrumentality > impartial > hollywood_placename > general > existent > eventuality > event > entity > dirty > city > chevy > car > barrel > artifact > abstraction > #nlpp > actual_world > true > skc9 > skc8 > skc7 > skc6 > skc5 > b > a % 5.49/2.41 % 5.49/2.41 %Foreground sorts: % 5.49/2.41 % 5.49/2.41 % 5.49/2.41 %Background operators: % 5.49/2.41 % 5.49/2.41 % 5.49/2.41 %Foreground operators: % 5.49/2.41 tff(agent, type, agent: ($i * $i * $i) > $i). % 5.49/2.41 tff(white, type, white: ($i * $i) > $i). % 5.49/2.41 tff(down, type, down: ($i * $i * $i) > $i). % 5.49/2.41 tff(city, type, city: ($i * $i) > $i). % 5.49/2.41 tff(street, type, street: ($i * $i) > $i). % 5.49/2.41 tff(nonliving, type, nonliving: ($i * $i) > $i). % 5.49/2.41 tff(old, type, old: ($i * $i) > $i). % 5.49/2.41 tff(specific, type, specific: ($i * $i) > $i). % 5.49/2.41 tff(impartial, type, impartial: ($i * $i) > $i). % 5.49/2.41 tff(skc7, type, skc7: $i). % 5.49/2.41 tff(transport, type, transport: ($i * $i) > $i). % 5.49/2.41 tff(a, type, a: $i). % 5.49/2.41 tff(in, type, in: ($i * $i * $i) > $i). % 5.49/2.41 tff(skc9, type, skc9: $i). % 5.49/2.41 tff(eventuality, type, eventuality: ($i * $i) > $i). % 5.49/2.41 tff(tuple, type, tuple: ($i * $i) > $i). % 5.49/2.41 tff(skc8, type, skc8: $i). % 5.49/2.41 tff(artifact, type, artifact: ($i * $i) > $i). % 5.49/2.41 tff(relname, type, relname: ($i * $i) > $i). % 5.49/2.41 tff(placename, type, placename: ($i * $i) > $i). % 5.49/2.41 tff(thing, type, thing: ($i * $i) > $i). % 5.49/2.41 tff(chevy, type, chevy: ($i * $i) > $i). % 5.49/2.41 tff(barrel, type, barrel: ($i * $i) > $i). % 5.49/2.41 tff(unisex, type, unisex: ($i * $i) > $i). % 5.49/2.41 tff(abstraction, type, abstraction: ($i * $i) > $i). % 5.49/2.41 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 5.49/2.41 tff(relation, type, relation: ($i * $i) > $i). % 5.49/2.41 tff(instrumentality, type, instrumentality: ($i * $i) > $i). % 5.49/2.41 tff(actual_world, type, actual_world: $i > $i). % 5.49/2.41 tff(of, type, of: ($i * $i * $i) > $i). % 5.49/2.41 tff(present, type, present: ($i * $i) > $i). % 5.49/2.41 tff(b, type, b: $i). % 5.49/2.41 tff(lonely, type, lonely: ($i * $i) > $i). % 5.49/2.41 tff(dirty, type, dirty: ($i * $i) > $i). % 5.49/2.41 tff(car, type, car: ($i * $i) > $i). % 5.49/2.41 tff(vehicle, type, vehicle: ($i * $i) > $i). % 5.49/2.41 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 5.49/2.41 tff(existent, type, existent: ($i * $i) > $i). % 5.49/2.41 tff(skc5, type, skc5: $i). % 5.49/2.41 tff(true, type, true: $i). % 5.49/2.41 tff(skc6, type, skc6: $i). % 5.49/2.41 tff(nonhuman, type, nonhuman: ($i * $i) > $i). % 5.49/2.41 tff(entity, type, entity: ($i * $i) > $i). % 5.49/2.41 tff(singleton, type, singleton: ($i * $i) > $i). % 5.49/2.41 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 5.49/2.41 tff(hollywood_placename, type, hollywood_placename: ($i * $i) > $i). % 5.49/2.41 tff(object, type, object: ($i * $i) > $i). % 5.49/2.41 tff(location, type, location: ($i * $i) > $i). % 5.49/2.41 tff(way, type, way: ($i * $i) > $i). % 5.49/2.41 tff(event, type, event: ($i * $i) > $i). % 5.49/2.41 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 5.49/2.41 tff(general, type, general: ($i * $i) > $i). % 5.49/2.41 % 5.49/2.41 %Saturated clause set: % 5.49/2.41 tff(c_1303, plain, (![W_160, V_162]: (ifeq3(of(skc5, W_160, skc9), true, ifeq3(of(skc5, V_162, skc9), true, ifeq3(placename(skc5, W_160), true, ifeq3(placename(skc5, V_162), true, W_160, V_162), V_162), V_162), V_162)=V_162))). % 5.49/2.41 tff(c_1453, plain, (![V_166]: (ifeq3(of(skc5, skc8, skc9), true, ifeq3(of(skc5, V_166, skc9), true, ifeq3(placename(skc5, V_166), true, skc8, V_166), V_166), V_166)=V_166))). % 5.49/2.41 tff(c_1375, plain, (![W_163]: (ifeq3(of(skc5, W_163, skc9), true, ifeq3(of(skc5, skc8, skc9), true, ifeq3(placename(skc5, W_163), true, W_163, skc8), skc8), skc8)=skc8))). % 5.49/2.41 tff(c_1302, plain, (![W_160, V_162]: (ifeq3(of(skc5, W_160, skc7), true, ifeq3(of(skc5, V_162, skc7), true, ifeq3(placename(skc5, W_160), true, ifeq3(placename(skc5, V_162), true, W_160, V_162), V_162), V_162), V_162)=V_162))). % 5.49/2.41 tff(c_1552, plain, (ifeq3(of(skc5, skc8, skc9), true, ifeq3(of(skc5, skc8, skc9), true, skc8, skc8), skc8)=skc8)). % 5.49/2.41 tff(c_1305, plain, (![W_160]: (ifeq3(of(skc5, W_160, skc7), true, ifeq3(placename(skc5, W_160), true, W_160, skc8), skc8)=skc8))). % 5.49/2.41 tff(c_1671, plain, (ifeq(tuple(nonexistent(skc5, skc9), true), tuple(true, true), a, b)=b)). % 5.49/2.41 tff(c_1197, plain, (ifeq(tuple(true, general(skc5, skc9)), tuple(true, true), a, b)=b)). % 5.49/2.41 tff(c_1248, plain, (ifeq(tuple(nonexistent(skc5, skc7), true), tuple(true, true), a, b)=b)). % 5.49/2.41 tff(c_1304, plain, (![V_162]: (ifeq3(of(skc5, V_162, skc7), true, ifeq3(placename(skc5, V_162), true, skc8, V_162), V_162)=V_162))). % 5.49/2.41 tff(c_1191, plain, (ifeq(tuple(specific(skc5, skc8), true), tuple(true, true), a, b)=b)). % 5.49/2.41 tff(c_1194, plain, (ifeq(tuple(true, general(skc5, skc7)), tuple(true, true), a, b)=b)). % 5.49/2.41 tff(c_1266, plain, (ifeq(tuple(true, existent(skc5, skc6)), tuple(true, true), a, b)=b)). % 5.49/2.41 tff(c_1607, plain, (ifeq2(way(skc5, skc7), true, true, true)=true)). % 5.49/2.41 tff(c_1687, plain, (singleton(skc5, skc9)=true)). % 5.49/2.41 tff(c_1229, plain, (ifeq(tuple(true, general(skc5, skc6)), tuple(true, true), a, b)=b)). % 5.49/2.41 tff(c_1659, plain, (existent(skc5, skc9)=true)). % 5.49/2.41 tff(c_1502, plain, (ifeq2(entity(skc5, skc8), true, true, true)=true)). % 5.49/2.41 tff(c_1103, plain, (ifeq2(abstraction(skc5, skc9), true, true, true)=true)). % 5.49/2.41 tff(c_1630, plain, (singleton(skc5, skc8)=true)). % 5.49/2.41 tff(c_1577, plain, (ifeq2(eventuality(skc5, skc8), true, true, true)=true)). % 5.49/2.41 tff(c_1593, plain, (artifact(skc5, skc7)=true)). % 5.49/2.41 tff(c_1580, plain, (ifeq2(object(skc5, skc8), true, true, true)=true)). % 5.49/2.41 tff(c_1562, plain, (unisex(skc5, skc8)=true)). % 5.49/2.41 tff(c_1100, plain, (ifeq2(abstraction(skc5, skc7), true, true, true)=true)). % 5.49/2.41 tff(c_1378, plain, (![X_164]: (ifeq3(of(skc5, skc8, X_164), true, ifeq3(of(skc5, skc8, X_164), true, ifeq3(entity(skc5, X_164), true, skc8, skc8), skc8), skc8)=skc8))). % 5.49/2.41 tff(c_1514, plain, (nonhuman(skc5, skc8)=true)). % 5.49/2.41 tff(c_1484, plain, (thing(skc5, skc8)=true)). % 5.49/2.41 tff(c_1460, plain, (instrumentality(skc5, skc7)=true)). % 5.49/2.42 tff(c_1306, plain, (![X_161, V_162]: (ifeq3(of(skc5, skc8, X_161), true, ifeq3(of(skc5, V_162, X_161), true, ifeq3(placename(skc5, V_162), true, ifeq3(entity(skc5, X_161), true, skc8, V_162), V_162), V_162), V_162)=V_162))). % 5.49/2.42 tff(c_1397, plain, (transport(skc5, skc7)=true)). % 5.49/2.42 tff(c_1165, plain, (ifeq2(entity(skc5, skc6), true, true, true)=true)). % 5.49/2.42 tff(c_1162, plain, (ifeq2(abstraction(skc5, skc6), true, true, true)=true)). % 5.49/2.42 tff(c_1128, plain, (ifeq2(object(skc5, skc6), true, true, true)=true)). % 5.49/2.42 tff(c_1307, plain, (![W_160, X_161]: (ifeq3(of(skc5, W_160, X_161), true, ifeq3(of(skc5, skc8, X_161), true, ifeq3(placename(skc5, W_160), true, ifeq3(entity(skc5, X_161), true, W_160, skc8), skc8), skc8), skc8)=skc8))). % 5.49/2.42 tff(c_1335, plain, (singleton(skc5, skc6)=true)). % 5.49/2.42 tff(c_1311, plain, (vehicle(skc5, skc7)=true)). % 5.49/2.42 tff(c_72, plain, (![U_74, W_75, X_76, V_77]: (ifeq3(of(U_74, W_75, X_76), true, ifeq3(of(U_74, V_77, X_76), true, ifeq3(placename(U_74, W_75), true, ifeq3(placename(U_74, V_77), true, ifeq3(entity(U_74, X_76), true, W_75, V_77), V_77), V_77), V_77), V_77)=V_77))). % 5.49/2.42 tff(c_1254, plain, (nonexistent(skc5, skc6)=true)). % 5.49/2.42 tff(c_110, plain, (![U_80, V_81]: (ifeq(tuple(nonexistent(U_80, V_81), existent(U_80, V_81)), tuple(true, true), a, b)=b))). % 5.49/2.42 tff(c_1217, plain, (specific(skc5, skc6)=true)). % 5.49/2.42 tff(c_1181, plain, (car(skc5, skc7)=true)). % 5.49/2.42 tff(c_108, plain, (![U_78, V_79]: (ifeq(tuple(specific(U_78, V_79), general(U_78, V_79)), tuple(true, true), a, b)=b))). % 5.49/2.42 tff(c_1137, plain, (thing(skc5, skc6)=true)). % 5.49/2.42 tff(c_62, plain, (![U_64, V_65]: (ifeq2(chevy(U_64, V_65), true, car(U_64, V_65), true)=true))). % 5.49/2.42 tff(c_1110, plain, (unisex(skc5, skc6)=true)). % 5.49/2.42 tff(c_54, plain, (![U_56, V_57]: (ifeq2(abstraction(U_56, V_57), true, unisex(U_56, V_57), true)=true))). % 5.49/2.42 tff(c_1061, plain, (eventuality(skc5, skc6)=true)). % 5.49/2.42 tff(c_10, plain, (![U_12, V_13]: (ifeq2(event(U_12, V_13), true, eventuality(U_12, V_13), true)=true))). % 5.49/2.42 tff(c_1030, plain, (general(skc5, skc8)=true)). % 5.49/2.42 tff(c_1000, plain, (abstraction(skc5, skc8)=true)). % 5.49/2.42 tff(c_46, plain, (![U_48, V_49]: (ifeq2(relation(U_48, V_49), true, abstraction(U_48, V_49), true)=true))). % 5.49/2.42 tff(c_969, plain, (existent(skc5, skc7)=true)). % 5.49/2.42 tff(c_34, plain, (![U_36, V_37]: (ifeq2(entity(U_36, V_37), true, existent(U_36, V_37), true)=true))). % 5.49/2.42 tff(c_933, plain, (singleton(skc5, skc7)=true)). % 5.49/2.42 tff(c_52, plain, (![U_54, V_55]: (ifeq2(abstraction(U_54, V_55), true, general(U_54, V_55), true)=true))). % 5.49/2.42 tff(c_905, plain, (impartial(skc5, skc9)=true)). % 5.49/2.42 tff(c_56, plain, (![U_58, V_59]: (ifeq2(hollywood_placename(U_58, V_59), true, placename(U_58, V_59), true)=true))). % 5.49/2.42 tff(c_774, plain, (ifeq2(eventuality(skc5, skc7), true, true, true)=true)). % 5.49/2.42 tff(c_856, plain, (thing(skc5, skc7)=true)). % 5.49/2.42 tff(c_12, plain, (![U_14, V_15]: (ifeq2(eventuality(U_14, V_15), true, thing(U_14, V_15), true)=true))). % 5.49/2.42 tff(c_821, plain, (specific(skc5, skc7)=true)). % 5.49/2.42 tff(c_633, plain, (ifeq2(location(skc5, skc9), true, true, true)=true)). % 5.49/2.42 tff(c_48, plain, (![U_50, V_51]: (ifeq2(abstraction(U_50, V_51), true, thing(U_50, V_51), true)=true))). % 5.49/2.42 tff(c_786, plain, (impartial(skc5, skc7)=true)). % 5.49/2.42 tff(c_753, plain, (unisex(skc5, skc7)=true)). % 5.49/2.42 tff(c_38, plain, (![U_40, V_41]: (ifeq2(object(U_40, V_41), true, impartial(U_40, V_41), true)=true))). % 5.49/2.42 tff(c_721, plain, (nonliving(skc5, skc7)=true)). % 5.49/2.42 tff(c_50, plain, (![U_52, V_53]: (ifeq2(abstraction(U_52, V_53), true, nonhuman(U_52, V_53), true)=true))). % 5.49/2.42 tff(c_694, plain, (entity(skc5, skc7)=true)). % 5.49/2.42 tff(c_8, plain, (![U_10, V_11]: (ifeq2(barrel(U_10, V_11), true, event(U_10, V_11), true)=true))). % 5.49/2.42 tff(c_642, plain, (object(skc5, skc7)=true)). % 5.49/2.42 tff(c_60, plain, (![U_62, V_63]: (ifeq2(location(U_62, V_63), true, object(U_62, V_63), true)=true))). % 5.49/2.42 tff(c_605, plain, (thing(skc5, skc9)=true)). % 5.49/2.42 tff(c_573, plain, (specific(skc5, skc9)=true)). % 5.49/2.42 tff(c_64, plain, (![U_66, V_67]: (ifeq2(car(U_66, V_67), true, vehicle(U_66, V_67), true)=true))). % 5.49/2.42 tff(c_550, plain, (ifeq2(eventuality(skc5, skc9), true, true, true)=true)). % 5.49/2.42 tff(c_68, plain, (![U_70, V_71]: (ifeq2(transport(U_70, V_71), true, instrumentality(U_70, V_71), true)=true))). % 5.49/2.42 tff(c_538, plain, (unisex(skc5, skc9)=true)). % 5.49/2.42 tff(c_517, plain, (nonliving(skc5, skc9)=true)). % 5.49/2.42 tff(c_20, plain, (![U_22, V_23]: (ifeq2(eventuality(U_22, V_23), true, unisex(U_22, V_23), true)=true))). % 5.49/2.42 tff(c_483, plain, (entity(skc5, skc9)=true)). % 5.49/2.42 tff(c_40, plain, (![U_42, V_43]: (ifeq2(object(U_42, V_43), true, unisex(U_42, V_43), true)=true))). % 5.49/2.42 tff(c_392, plain, (ifeq2(instrumentality(skc5, skc9), true, true, true)=true)). % 5.49/2.42 tff(c_448, plain, (relation(skc5, skc8)=true)). % 5.49/2.42 tff(c_44, plain, (![U_46, V_47]: (ifeq2(relname(U_46, V_47), true, relation(U_46, V_47), true)=true))). % 5.49/2.42 tff(c_411, plain, (object(skc5, skc9)=true)). % 5.49/2.42 tff(c_30, plain, (![U_32, V_33]: (ifeq2(entity(U_32, V_33), true, thing(U_32, V_33), true)=true))). % 5.49/2.42 tff(c_377, plain, (artifact(skc5, skc9)=true)). % 5.49/2.42 tff(c_24, plain, (![U_26, V_27]: (ifeq2(way(U_26, V_27), true, artifact(U_26, V_27), true)=true))). % 5.49/2.42 tff(c_16, plain, (![U_18, V_19]: (ifeq2(eventuality(U_18, V_19), true, specific(U_18, V_19), true)=true))). % 5.49/2.42 tff(c_32, plain, (![U_34, V_35]: (ifeq2(entity(U_34, V_35), true, specific(U_34, V_35), true)=true))). % 5.49/2.42 tff(c_36, plain, (![U_38, V_39]: (ifeq2(object(U_38, V_39), true, nonliving(U_38, V_39), true)=true))). % 5.49/2.43 tff(c_14, plain, (![U_16, V_17]: (ifeq2(thing(U_16, V_17), true, singleton(U_16, V_17), true)=true))). % 5.49/2.43 tff(c_311, plain, (location(skc5, skc7)=true)). % 5.49/2.43 tff(c_18, plain, (![U_20, V_21]: (ifeq2(eventuality(U_20, V_21), true, nonexistent(U_20, V_21), true)=true))). % 5.49/2.43 tff(c_58, plain, (![U_60, V_61]: (ifeq2(city(U_60, V_61), true, location(U_60, V_61), true)=true))). % 5.49/2.43 tff(c_280, plain, (way(skc5, skc9)=true)). % 5.49/2.43 tff(c_22, plain, (![U_24, V_25]: (ifeq2(street(U_24, V_25), true, way(U_24, V_25), true)=true))). % 5.49/2.43 tff(c_249, plain, (relname(skc5, skc8)=true)). % 5.49/2.43 tff(c_42, plain, (![U_44, V_45]: (ifeq2(placename(U_44, V_45), true, relname(U_44, V_45), true)=true))). % 5.49/2.43 tff(c_70, plain, (![U_72, V_73]: (ifeq2(instrumentality(U_72, V_73), true, artifact(U_72, V_73), true)=true))). % 5.49/2.43 tff(c_66, plain, (![U_68, V_69]: (ifeq2(vehicle(U_68, V_69), true, transport(U_68, V_69), true)=true))). % 5.49/2.43 tff(c_28, plain, (![U_30, V_31]: (ifeq2(object(U_30, V_31), true, entity(U_30, V_31), true)=true))). % 5.49/2.43 tff(c_26, plain, (![U_28, V_29]: (ifeq2(artifact(U_28, V_29), true, object(U_28, V_29), true)=true))). % 5.49/2.43 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 5.49/2.43 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 5.49/2.43 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 5.49/2.43 tff(c_102, plain, (agent(skc5, skc6, skc7)=true)). % 5.49/2.43 tff(c_100, plain, (of(skc5, skc8, skc7)=true)). % 5.49/2.43 tff(c_104, plain, (in(skc5, skc6, skc7)=true)). % 5.49/2.43 tff(c_106, plain, (down(skc5, skc6, skc9)=true)). % 5.49/2.43 tff(c_92, plain, (lonely(skc5, skc9)=true)). % 5.49/2.43 tff(c_94, plain, (barrel(skc5, skc6)=true)). % 5.49/2.43 tff(c_98, plain, (event(skc5, skc6)=true)). % 5.49/2.43 tff(c_76, plain, (street(skc5, skc9)=true)). % 5.49/2.43 tff(c_90, plain, (old(skc5, skc7)=true)). % 5.49/2.43 tff(c_88, plain, (dirty(skc5, skc7)=true)). % 5.49/2.43 tff(c_86, plain, (white(skc5, skc7)=true)). % 5.49/2.43 tff(c_84, plain, (chevy(skc5, skc7)=true)). % 5.49/2.43 tff(c_78, plain, (placename(skc5, skc8)=true)). % 5.49/2.43 tff(c_80, plain, (hollywood_placename(skc5, skc8)=true)). % 5.49/2.43 tff(c_82, plain, (city(skc5, skc7)=true)). % 5.49/2.43 tff(c_96, plain, (present(skc5, skc6)=true)). % 5.49/2.43 tff(c_74, plain, (actual_world(skc5)=true)). % 5.49/2.43 tff(c_112, plain, (b!=a)). % 5.49/2.43 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.49/2.43 %------------------------------------------------------------------------------