%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP129-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 : n020.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:20 PM UTC 2025 % Result : Satisfiable 6.43s 2.66s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP129-10 : TPTP v9.0.0. Released v7.5.0. % 0.11/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.12/0.34 % Computer : n020.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Apr 8 08:41:49 EDT 2025 % 0.12/0.34 % CPUTime : % 6.43/2.66 % 6.43/2.66 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.43/2.66 % 6.43/2.66 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.43/2.67 %$ 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 % 6.43/2.67 % 6.43/2.67 %Foreground sorts: % 6.43/2.67 % 6.43/2.67 % 6.43/2.67 %Background operators: % 6.43/2.67 % 6.43/2.67 % 6.43/2.67 %Foreground operators: % 6.43/2.67 tff(agent, type, agent: ($i * $i * $i) > $i). % 6.43/2.67 tff(white, type, white: ($i * $i) > $i). % 6.43/2.67 tff(down, type, down: ($i * $i * $i) > $i). % 6.43/2.67 tff(city, type, city: ($i * $i) > $i). % 6.43/2.67 tff(street, type, street: ($i * $i) > $i). % 6.43/2.67 tff(nonliving, type, nonliving: ($i * $i) > $i). % 6.43/2.67 tff(old, type, old: ($i * $i) > $i). % 6.43/2.67 tff(specific, type, specific: ($i * $i) > $i). % 6.43/2.67 tff(impartial, type, impartial: ($i * $i) > $i). % 6.43/2.67 tff(skc7, type, skc7: $i). % 6.43/2.67 tff(transport, type, transport: ($i * $i) > $i). % 6.43/2.67 tff(a, type, a: $i). % 6.43/2.67 tff(in, type, in: ($i * $i * $i) > $i). % 6.43/2.67 tff(skc9, type, skc9: $i). % 6.43/2.67 tff(eventuality, type, eventuality: ($i * $i) > $i). % 6.43/2.67 tff(tuple, type, tuple: ($i * $i) > $i). % 6.43/2.67 tff(skc8, type, skc8: $i). % 6.43/2.67 tff(artifact, type, artifact: ($i * $i) > $i). % 6.43/2.67 tff(relname, type, relname: ($i * $i) > $i). % 6.43/2.67 tff(placename, type, placename: ($i * $i) > $i). % 6.43/2.67 tff(thing, type, thing: ($i * $i) > $i). % 6.43/2.67 tff(chevy, type, chevy: ($i * $i) > $i). % 6.43/2.67 tff(barrel, type, barrel: ($i * $i) > $i). % 6.43/2.67 tff(unisex, type, unisex: ($i * $i) > $i). % 6.43/2.67 tff(abstraction, type, abstraction: ($i * $i) > $i). % 6.43/2.67 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 6.43/2.67 tff(relation, type, relation: ($i * $i) > $i). % 6.43/2.67 tff(instrumentality, type, instrumentality: ($i * $i) > $i). % 6.43/2.67 tff(actual_world, type, actual_world: $i > $i). % 6.43/2.67 tff(of, type, of: ($i * $i * $i) > $i). % 6.43/2.67 tff(present, type, present: ($i * $i) > $i). % 6.43/2.67 tff(b, type, b: $i). % 6.43/2.67 tff(lonely, type, lonely: ($i * $i) > $i). % 6.43/2.67 tff(dirty, type, dirty: ($i * $i) > $i). % 6.43/2.67 tff(car, type, car: ($i * $i) > $i). % 6.43/2.67 tff(vehicle, type, vehicle: ($i * $i) > $i). % 6.43/2.67 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 6.43/2.67 tff(existent, type, existent: ($i * $i) > $i). % 6.43/2.67 tff(skc5, type, skc5: $i). % 6.43/2.67 tff(true, type, true: $i). % 6.43/2.67 tff(skc6, type, skc6: $i). % 6.43/2.67 tff(nonhuman, type, nonhuman: ($i * $i) > $i). % 6.43/2.67 tff(entity, type, entity: ($i * $i) > $i). % 6.43/2.67 tff(singleton, type, singleton: ($i * $i) > $i). % 6.43/2.67 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 6.43/2.67 tff(hollywood_placename, type, hollywood_placename: ($i * $i) > $i). % 6.43/2.67 tff(object, type, object: ($i * $i) > $i). % 6.43/2.67 tff(location, type, location: ($i * $i) > $i). % 6.43/2.67 tff(way, type, way: ($i * $i) > $i). % 6.43/2.67 tff(event, type, event: ($i * $i) > $i). % 6.43/2.67 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 6.43/2.67 tff(general, type, general: ($i * $i) > $i). % 6.43/2.67 % 6.43/2.67 %Saturated clause set: % 6.80/2.68 tff(c_1562, plain, (![W_75, V_77]: (ifeq3(of(skc5, W_75, skc9), true, ifeq3(of(skc5, V_77, skc9), true, ifeq3(placename(skc5, W_75), true, ifeq3(placename(skc5, V_77), true, W_75, V_77), V_77), V_77), V_77)=V_77))). % 6.80/2.68 tff(c_1560, plain, (![V_162]: (ifeq3(of(skc5, skc8, skc9), true, ifeq3(of(skc5, V_162, skc9), true, ifeq3(placename(skc5, V_162), true, skc8, V_162), V_162), V_162)=V_162))). % 6.80/2.68 tff(c_1561, plain, (![W_160]: (ifeq3(of(skc5, W_160, skc9), true, ifeq3(of(skc5, skc8, skc9), true, ifeq3(placename(skc5, W_160), true, W_160, skc8), skc8), skc8)=skc8))). % 6.80/2.68 tff(c_1559, plain, (ifeq3(of(skc5, skc8, skc9), true, ifeq3(of(skc5, skc8, skc9), true, skc8, skc8), skc8)=skc8)). % 6.80/2.68 tff(c_1179, 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))). % 6.80/2.68 tff(c_1286, plain, (![W_163]: (ifeq3(of(skc5, W_163, skc7), true, ifeq3(placename(skc5, W_163), true, W_163, skc8), skc8)=skc8))). % 6.80/2.68 tff(c_1180, plain, (![V_162]: (ifeq3(of(skc5, V_162, skc7), true, ifeq3(placename(skc5, V_162), true, skc8, V_162), V_162)=V_162))). % 6.80/2.68 tff(c_1641, plain, (ifeq(tuple(nonexistent(skc5, skc9), true), tuple(true, true), a, b)=b)). % 6.80/2.68 tff(c_1669, plain, (ifeq(tuple(true, general(skc5, skc9)), tuple(true, true), a, b)=b)). % 6.80/2.68 tff(c_1080, plain, (ifeq(tuple(true, general(skc5, skc7)), tuple(true, true), a, b)=b)). % 6.80/2.68 tff(c_1304, plain, (ifeq(tuple(nonexistent(skc5, skc7), true), tuple(true, true), a, b)=b)). % 6.82/2.68 tff(c_1074, plain, (ifeq(tuple(specific(skc5, skc8), true), tuple(true, true), a, b)=b)). % 6.82/2.68 tff(c_1111, plain, (ifeq(tuple(true, existent(skc5, skc6)), tuple(true, true), a, b)=b)). % 6.82/2.68 tff(c_1685, plain, (singleton(skc5, skc9)=true)). % 6.82/2.68 tff(c_1657, plain, (specific(skc5, skc9)=true)). % 6.82/2.68 tff(c_1507, plain, (ifeq2(eventuality(skc5, skc9), true, true, true)=true)). % 6.82/2.68 tff(c_1625, plain, (existent(skc5, skc9)=true)). % 6.82/2.68 tff(c_1077, plain, (ifeq(tuple(true, general(skc5, skc6)), tuple(true, true), a, b)=b)). % 6.82/2.68 tff(c_1504, plain, (ifeq2(abstraction(skc5, skc9), true, true, true)=true)). % 6.82/2.68 tff(c_1591, plain, (thing(skc5, skc9)=true)). % 6.82/2.68 tff(c_1570, plain, (impartial(skc5, skc9)=true)). % 6.82/2.68 tff(c_1523, plain, (entity(skc5, skc9)=true)). % 6.82/2.68 tff(c_1427, plain, (ifeq2(location(skc5, skc9), true, true, true)=true)). % 6.82/2.68 tff(c_1492, plain, (unisex(skc5, skc9)=true)). % 6.82/2.68 tff(c_1471, plain, (nonliving(skc5, skc9)=true)). % 6.82/2.68 tff(c_1287, 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))). % 6.82/2.68 tff(c_1349, plain, (ifeq2(way(skc5, skc9), true, true, true)=true)). % 6.82/2.68 tff(c_1412, plain, (object(skc5, skc9)=true)). % 6.82/2.68 tff(c_1206, plain, (ifeq2(object(skc5, skc8), true, true, true)=true)). % 6.82/2.68 tff(c_1257, plain, (ifeq2(entity(skc5, skc8), true, true, true)=true)). % 6.82/2.68 tff(c_1251, plain, (ifeq2(eventuality(skc5, skc8), true, true, true)=true)). % 6.82/2.69 tff(c_1182, 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))). % 6.82/2.69 tff(c_1337, plain, (artifact(skc5, skc9)=true)). % 6.82/2.69 tff(c_1316, plain, (singleton(skc5, skc8)=true)). % 6.82/2.69 tff(c_1292, plain, (existent(skc5, skc7)=true)). % 6.82/2.69 tff(c_1183, 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))). % 6.82/2.69 tff(c_1239, plain, (thing(skc5, skc8)=true)). % 6.82/2.69 tff(c_1215, plain, (instrumentality(skc5, skc9)=true)). % 6.82/2.69 tff(c_1188, plain, (unisex(skc5, skc8)=true)). % 6.82/2.69 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))). % 6.82/2.69 tff(c_1138, plain, (impartial(skc5, skc7)=true)). % 6.82/2.69 tff(c_1117, plain, (nonhuman(skc5, skc8)=true)). % 6.82/2.69 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))). % 6.82/2.69 tff(c_1086, plain, (singleton(skc5, skc6)=true)). % 6.82/2.69 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))). % 6.82/2.69 tff(c_1038, plain, (thing(skc5, skc6)=true)). % 6.82/2.69 tff(c_1003, plain, (general(skc5, skc8)=true)). % 6.82/2.69 tff(c_12, plain, (![U_14, V_15]: (ifeq2(eventuality(U_14, V_15), true, thing(U_14, V_15), true)=true))). % 6.82/2.69 tff(c_964, plain, (transport(skc5, skc9)=true)). % 6.82/2.69 tff(c_8, plain, (![U_10, V_11]: (ifeq2(barrel(U_10, V_11), true, event(U_10, V_11), true)=true))). % 6.82/2.69 tff(c_931, plain, (abstraction(skc5, skc8)=true)). % 6.82/2.69 tff(c_890, plain, (ifeq2(object(skc5, skc6), true, true, true)=true)). % 6.82/2.69 tff(c_46, plain, (![U_48, V_49]: (ifeq2(relation(U_48, V_49), true, abstraction(U_48, V_49), true)=true))). % 6.82/2.69 tff(c_863, plain, (ifeq2(entity(skc5, skc6), true, true, true)=true)). % 6.82/2.69 tff(c_884, plain, (ifeq2(abstraction(skc5, skc6), true, true, true)=true)). % 6.82/2.69 tff(c_38, plain, (![U_40, V_41]: (ifeq2(object(U_40, V_41), true, impartial(U_40, V_41), true)=true))). % 6.82/2.69 tff(c_872, plain, (unisex(skc5, skc6)=true)). % 6.82/2.69 tff(c_848, plain, (specific(skc5, skc6)=true)). % 6.82/2.69 tff(c_50, plain, (![U_52, V_53]: (ifeq2(abstraction(U_52, V_53), true, nonhuman(U_52, V_53), true)=true))). % 6.82/2.69 tff(c_817, plain, (vehicle(skc5, skc9)=true)). % 6.82/2.69 tff(c_54, plain, (![U_56, V_57]: (ifeq2(abstraction(U_56, V_57), true, unisex(U_56, V_57), true)=true))). % 6.82/2.69 tff(c_785, plain, (nonexistent(skc5, skc6)=true)). % 6.82/2.69 tff(c_751, plain, (car(skc5, skc9)=true)). % 6.82/2.69 tff(c_34, plain, (![U_36, V_37]: (ifeq2(entity(U_36, V_37), true, existent(U_36, V_37), true)=true))). % 6.82/2.69 tff(c_711, plain, (eventuality(skc5, skc6)=true)). % 6.82/2.69 tff(c_62, plain, (![U_64, V_65]: (ifeq2(chevy(U_64, V_65), true, car(U_64, V_65), true)=true))). % 6.82/2.69 tff(c_10, plain, (![U_12, V_13]: (ifeq2(event(U_12, V_13), true, eventuality(U_12, V_13), true)=true))). % 6.82/2.69 tff(c_52, plain, (![U_54, V_55]: (ifeq2(abstraction(U_54, V_55), true, general(U_54, V_55), true)=true))). % 6.82/2.69 tff(c_684, plain, (ifeq2(abstraction(skc5, skc7), true, true, true)=true)). % 6.82/2.69 tff(c_48, plain, (![U_50, V_51]: (ifeq2(abstraction(U_50, V_51), true, thing(U_50, V_51), true)=true))). % 6.82/2.69 tff(c_56, plain, (![U_58, V_59]: (ifeq2(hollywood_placename(U_58, V_59), true, placename(U_58, V_59), true)=true))). % 6.82/2.69 tff(c_644, plain, (singleton(skc5, skc7)=true)). % 6.82/2.70 tff(c_60, plain, (![U_62, V_63]: (ifeq2(location(U_62, V_63), true, object(U_62, V_63), true)=true))). % 6.82/2.70 tff(c_605, plain, (thing(skc5, skc7)=true)). % 6.82/2.70 tff(c_573, plain, (specific(skc5, skc7)=true)). % 6.82/2.70 tff(c_64, plain, (![U_66, V_67]: (ifeq2(car(U_66, V_67), true, vehicle(U_66, V_67), true)=true))). % 6.82/2.70 tff(c_550, plain, (ifeq2(eventuality(skc5, skc7), true, true, true)=true)). % 6.82/2.70 tff(c_68, plain, (![U_70, V_71]: (ifeq2(transport(U_70, V_71), true, instrumentality(U_70, V_71), true)=true))). % 6.82/2.70 tff(c_538, plain, (unisex(skc5, skc7)=true)). % 6.82/2.70 tff(c_517, plain, (nonliving(skc5, skc7)=true)). % 6.82/2.70 tff(c_20, plain, (![U_22, V_23]: (ifeq2(eventuality(U_22, V_23), true, unisex(U_22, V_23), true)=true))). % 6.82/2.70 tff(c_483, plain, (entity(skc5, skc7)=true)). % 6.82/2.70 tff(c_40, plain, (![U_42, V_43]: (ifeq2(object(U_42, V_43), true, unisex(U_42, V_43), true)=true))). % 6.82/2.70 tff(c_392, plain, (ifeq2(instrumentality(skc5, skc7), true, true, true)=true)). % 6.82/2.70 tff(c_448, plain, (relation(skc5, skc8)=true)). % 6.82/2.70 tff(c_44, plain, (![U_46, V_47]: (ifeq2(relname(U_46, V_47), true, relation(U_46, V_47), true)=true))). % 6.82/2.70 tff(c_411, plain, (object(skc5, skc7)=true)). % 6.82/2.70 tff(c_30, plain, (![U_32, V_33]: (ifeq2(entity(U_32, V_33), true, thing(U_32, V_33), true)=true))). % 6.82/2.70 tff(c_377, plain, (artifact(skc5, skc7)=true)). % 6.82/2.70 tff(c_24, plain, (![U_26, V_27]: (ifeq2(way(U_26, V_27), true, artifact(U_26, V_27), true)=true))). % 6.82/2.70 tff(c_16, plain, (![U_18, V_19]: (ifeq2(eventuality(U_18, V_19), true, specific(U_18, V_19), true)=true))). % 6.82/2.70 tff(c_32, plain, (![U_34, V_35]: (ifeq2(entity(U_34, V_35), true, specific(U_34, V_35), true)=true))). % 6.82/2.70 tff(c_36, plain, (![U_38, V_39]: (ifeq2(object(U_38, V_39), true, nonliving(U_38, V_39), true)=true))). % 6.82/2.70 tff(c_14, plain, (![U_16, V_17]: (ifeq2(thing(U_16, V_17), true, singleton(U_16, V_17), true)=true))). % 6.82/2.70 tff(c_311, plain, (location(skc5, skc7)=true)). % 6.82/2.70 tff(c_18, plain, (![U_20, V_21]: (ifeq2(eventuality(U_20, V_21), true, nonexistent(U_20, V_21), true)=true))). % 6.82/2.70 tff(c_58, plain, (![U_60, V_61]: (ifeq2(city(U_60, V_61), true, location(U_60, V_61), true)=true))). % 6.82/2.70 tff(c_280, plain, (way(skc5, skc7)=true)). % 6.82/2.70 tff(c_22, plain, (![U_24, V_25]: (ifeq2(street(U_24, V_25), true, way(U_24, V_25), true)=true))). % 6.82/2.70 tff(c_249, plain, (relname(skc5, skc8)=true)). % 6.92/2.70 tff(c_42, plain, (![U_44, V_45]: (ifeq2(placename(U_44, V_45), true, relname(U_44, V_45), true)=true))). % 6.92/2.70 tff(c_70, plain, (![U_72, V_73]: (ifeq2(instrumentality(U_72, V_73), true, artifact(U_72, V_73), true)=true))). % 6.92/2.70 tff(c_66, plain, (![U_68, V_69]: (ifeq2(vehicle(U_68, V_69), true, transport(U_68, V_69), true)=true))). % 6.92/2.70 tff(c_28, plain, (![U_30, V_31]: (ifeq2(object(U_30, V_31), true, entity(U_30, V_31), true)=true))). % 6.92/2.70 tff(c_26, plain, (![U_28, V_29]: (ifeq2(artifact(U_28, V_29), true, object(U_28, V_29), true)=true))). % 6.92/2.70 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 6.92/2.70 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 6.92/2.70 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 6.92/2.70 tff(c_102, plain, (down(skc5, skc6, skc7)=true)). % 6.92/2.70 tff(c_100, plain, (of(skc5, skc8, skc7)=true)). % 6.92/2.70 tff(c_104, plain, (in(skc5, skc6, skc7)=true)). % 6.92/2.70 tff(c_106, plain, (agent(skc5, skc6, skc9)=true)). % 6.92/2.70 tff(c_92, plain, (old(skc5, skc9)=true)). % 6.92/2.70 tff(c_94, plain, (barrel(skc5, skc6)=true)). % 6.92/2.70 tff(c_98, plain, (event(skc5, skc6)=true)). % 6.92/2.70 tff(c_76, plain, (chevy(skc5, skc9)=true)). % 6.92/2.70 tff(c_90, plain, (dirty(skc5, skc9)=true)). % 6.92/2.70 tff(c_88, plain, (white(skc5, skc9)=true)). % 6.92/2.70 tff(c_86, plain, (lonely(skc5, skc7)=true)). % 6.92/2.70 tff(c_84, plain, (street(skc5, skc7)=true)). % 6.92/2.70 tff(c_78, plain, (placename(skc5, skc8)=true)). % 6.92/2.71 tff(c_80, plain, (hollywood_placename(skc5, skc8)=true)). % 6.92/2.71 tff(c_82, plain, (city(skc5, skc7)=true)). % 6.92/2.71 tff(c_96, plain, (present(skc5, skc6)=true)). % 6.92/2.71 tff(c_74, plain, (actual_world(skc5)=true)). % 6.92/2.71 tff(c_112, plain, (b!=a)). % 6.92/2.71 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.92/2.71 %------------------------------------------------------------------------------