%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP003-10 : TPTP v9.0.0. Released v7.3.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 : n004.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:47:49 PM UTC 2025 % Result : Satisfiable 4.52s 2.07s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : NLP003-10 : TPTP v9.0.0. Released v7.3.0. % 0.03/0.14 % 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.35 % Computer : n004.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Tue Apr 8 08:04:08 EDT 2025 % 0.13/0.35 % CPUTime : % 4.52/2.07 % 4.52/2.07 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.52/2.07 % 4.52/2.07 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.52/2.08 %$ ifeq3 > ifeq2 > ifeq > have > tuple > skf1 > partof > of > in > down > barrel > #nlpp > woman > white > way > vehicle > transport > street > proposition > owner > old > object > nonhuman > new > man > male > lonely > location > instrumentality > human > hollywood > female > eventuality > event > entity > drs > dirty > city > chevy > car > artifact > abstraction > true > skc7 > skc6 > skc5 > skc4 > b > a % 4.52/2.08 % 4.52/2.08 %Foreground sorts: % 4.52/2.08 % 4.52/2.08 % 4.52/2.08 %Background operators: % 4.52/2.08 % 4.52/2.08 % 4.52/2.08 %Foreground operators: % 4.52/2.08 tff(white, type, white: $i > $i). % 4.52/2.08 tff(hollywood, type, hollywood: $i > $i). % 4.52/2.08 tff(transport, type, transport: $i > $i). % 4.52/2.08 tff(new, type, new: $i > $i). % 4.52/2.08 tff(skc7, type, skc7: $i). % 4.52/2.08 tff(dirty, type, dirty: $i > $i). % 4.52/2.08 tff(owner, type, owner: $i > $i). % 4.52/2.08 tff(a, type, a: $i). % 4.52/2.08 tff(in, type, in: ($i * $i) > $i). % 4.52/2.08 tff(proposition, type, proposition: $i > $i). % 4.52/2.08 tff(tuple, type, tuple: ($i * $i) > $i). % 4.52/2.08 tff(human, type, human: $i > $i). % 4.52/2.08 tff(entity, type, entity: $i > $i). % 4.52/2.08 tff(object, type, object: $i > $i). % 4.52/2.08 tff(vehicle, type, vehicle: $i > $i). % 4.52/2.08 tff(have, type, have: ($i * $i * $i) > $i). % 4.52/2.08 tff(city, type, city: $i > $i). % 4.52/2.08 tff(drs, type, drs: $i > $i). % 4.52/2.08 tff(lonely, type, lonely: $i > $i). % 4.52/2.08 tff(eventuality, type, eventuality: $i > $i). % 4.52/2.08 tff(barrel, type, barrel: ($i * $i) > $i). % 4.52/2.08 tff(location, type, location: $i > $i). % 4.52/2.08 tff(skf1, type, skf1: ($i * $i) > $i). % 4.52/2.08 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 4.52/2.08 tff(chevy, type, chevy: $i > $i). % 4.52/2.08 tff(partof, type, partof: ($i * $i) > $i). % 4.52/2.08 tff(artifact, type, artifact: $i > $i). % 4.52/2.08 tff(car, type, car: $i > $i). % 4.52/2.08 tff(b, type, b: $i). % 4.52/2.08 tff(nonhuman, type, nonhuman: $i > $i). % 4.52/2.08 tff(female, type, female: $i > $i). % 4.52/2.08 tff(way, type, way: $i > $i). % 4.52/2.08 tff(male, type, male: $i > $i). % 4.52/2.08 tff(instrumentality, type, instrumentality: $i > $i). % 4.52/2.08 tff(skc4, type, skc4: $i). % 4.52/2.08 tff(of, type, of: ($i * $i) > $i). % 4.52/2.08 tff(man, type, man: $i > $i). % 4.52/2.08 tff(abstraction, type, abstraction: $i > $i). % 4.52/2.08 tff(old, type, old: $i > $i). % 4.52/2.08 tff(skc5, type, skc5: $i). % 4.52/2.08 tff(true, type, true: $i). % 4.52/2.08 tff(event, type, event: $i > $i). % 4.52/2.08 tff(skc6, type, skc6: $i). % 4.52/2.08 tff(woman, type, woman: $i > $i). % 4.52/2.08 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 4.52/2.08 tff(down, type, down: ($i * $i) > $i). % 4.52/2.08 tff(street, type, street: $i > $i). % 4.52/2.08 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 4.52/2.08 % 4.52/2.08 %Saturated clause set: % 4.52/2.08 tff(c_64, plain, (![W_51, V_52, U_53]: (ifeq2(have(W_51, V_52, U_53), true, ifeq2(nonhuman(V_52), true, ifeq2(nonhuman(U_53), true, partof(U_53, V_52), true), true), true)=true))). % 4.52/2.08 tff(c_62, plain, (![U_48, V_49, W_50]: (ifeq2(of(U_48, V_49), true, ifeq2(owner(U_48), true, have(W_50, U_48, V_49), true), true)=true))). % 4.52/2.08 tff(c_60, plain, (![V_45, U_46, W_47]: (ifeq2(have(V_45, U_46, W_47), true, ifeq2(human(U_46), true, of(U_46, W_47), true), true)=true))). % 4.52/2.08 tff(c_1007, plain, (![U_10, V_11, V_124, W_125]: (ifeq2(have(skf1(U_10, V_11), V_124, W_125), true, of(V_124, W_125), true)=true))). % 4.52/2.08 tff(c_1008, plain, (![V_124, W_125]: (ifeq2(have(skc6, V_124, W_125), true, of(V_124, W_125), true)=true))). % 4.52/2.08 tff(c_58, plain, (![U_42, V_43, W_44]: (ifeq2(have(U_42, V_43, W_44), true, ifeq2(event(U_42), true, of(V_43, W_44), true), true)=true))). % 4.52/2.08 tff(c_54, plain, (![V_36, U_37, W_38]: (ifeq2(have(V_36, U_37, W_38), true, ifeq2(human(U_37), true, owner(U_37), true), true)=true))). % 4.52/2.08 tff(c_964, plain, (![U_115, V_117]: (ifeq3(partof(U_115, ifeq3(partof(U_115, V_117), true, V_117, V_117)), true, V_117, V_117)=V_117))). % 4.52/2.08 tff(c_56, plain, (![U_39, W_40, V_41]: (ifeq3(partof(U_39, W_40), true, ifeq3(partof(U_39, V_41), true, W_40, V_41), V_41)=V_41))). % 4.52/2.08 tff(c_50, plain, (![U_32, V_33]: (ifeq2(of(U_32, V_33), true, ifeq2(owner(U_32), true, human(U_32), true), true)=true))). % 4.52/2.08 tff(c_880, plain, (![U_95, V_96]: (ifeq(tuple(entity(skf1(U_95, V_96)), true), tuple(true, true), a, b)=b))). % 4.52/2.08 tff(c_787, plain, (![U_95, V_96]: (ifeq(tuple(true, abstraction(skf1(U_95, V_96))), tuple(true, true), a, b)=b))). % 4.61/2.08 tff(c_52, plain, (![U_34, V_35]: (ifeq2(of(U_34, V_35), true, have(skf1(U_34, V_35), V_35, U_34), true)=true))). % 4.61/2.08 tff(c_94, plain, (![U_54]: (ifeq(tuple(nonhuman(U_54), human(U_54)), tuple(true, true), a, b)=b))). % 4.61/2.08 tff(c_886, plain, (ifeq(tuple(true, eventuality(skc5)), tuple(true, true), a, b)=b)). % 4.61/2.08 tff(c_96, plain, (![U_55]: (ifeq(tuple(woman(U_55), man(U_55)), tuple(true, true), a, b)=b))). % 4.61/2.09 tff(c_889, plain, (ifeq(tuple(true, eventuality(skc4)), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_883, plain, (ifeq(tuple(true, eventuality(skc7)), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_892, plain, (ifeq(tuple(entity(skc6), true), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_98, plain, (![U_56]: (ifeq(tuple(female(U_56), male(U_56)), tuple(true, true), a, b)=b))). % 4.61/2.09 tff(c_104, plain, (![U_59]: (ifeq(tuple(entity(U_59), eventuality(U_59)), tuple(true, true), a, b)=b))). % 4.61/2.09 tff(c_851, plain, (ifeq(tuple(true, abstraction(skc5)), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_848, plain, (ifeq(tuple(true, abstraction(skc7)), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_854, plain, (ifeq(tuple(true, abstraction(skc4)), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_831, plain, (ifeq(tuple(way(skc5), true), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_102, plain, (![U_58]: (ifeq(tuple(entity(U_58), abstraction(U_58)), tuple(true, true), a, b)=b))). % 4.61/2.09 tff(c_834, plain, (ifeq(tuple(true, instrumentality(skc4)), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_110, plain, (![U_62]: (ifeq(tuple(way(U_62), instrumentality(U_62)), tuple(true, true), a, b)=b))). % 4.61/2.09 tff(c_817, plain, (ifeq(tuple(true, new(skc5)), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_106, plain, (![U_60]: (ifeq(tuple(old(U_60), new(U_60)), tuple(true, true), a, b)=b))). % 4.61/2.09 tff(c_747, plain, (ifeq(tuple(location(skc5), true), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_790, plain, (ifeq(tuple(true, abstraction(skc6)), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_741, plain, (ifeq(tuple(location(skc4), true), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_744, plain, (ifeq(tuple(true, artifact(skc7)), tuple(true, true), a, b)=b)). % 4.61/2.09 tff(c_100, plain, (![U_57]: (ifeq(tuple(eventuality(U_57), abstraction(U_57)), tuple(true, true), a, b)=b))). % 4.61/2.09 tff(c_759, plain, (![U_95, V_96]: (eventuality(skf1(U_95, V_96))=true))). % 4.61/2.09 tff(c_669, plain, (ifeq2(nonhuman(skc5), true, true, true)=true)). % 4.61/2.09 tff(c_108, plain, (![U_61]: (ifeq(tuple(location(U_61), artifact(U_61)), tuple(true, true), a, b)=b))). % 4.61/2.09 tff(c_618, plain, (ifeq2(location(skc5), true, true, true)=true)). % 4.61/2.09 tff(c_713, plain, (ifeq2(nonhuman(skc7), true, true, true)=true)). % 4.61/2.09 tff(c_672, plain, (ifeq2(nonhuman(skc4), true, true, true)=true)). % 4.61/2.09 tff(c_686, plain, (entity(skc7)=true)). % 4.61/2.09 tff(c_30, plain, (![U_22]: (ifeq2(hollywood(U_22), true, city(U_22), true)=true))). % 4.61/2.09 tff(c_656, plain, (ifeq2(artifact(skc7), true, true, true)=true)). % 4.61/2.09 tff(c_615, plain, (ifeq2(location(skc4), true, true, true)=true)). % 4.61/2.09 tff(c_10, plain, (![U_12]: (ifeq2(nonhuman(U_12), true, entity(U_12), true)=true))). % 4.61/2.09 tff(c_638, plain, (object(skc7)=true)). % 4.61/2.09 tff(c_601, plain, (entity(skc5)=true)). % 4.61/2.09 tff(c_26, plain, (![U_20]: (ifeq2(location(U_20), true, object(U_20), true)=true))). % 4.61/2.09 tff(c_488, plain, (ifeq2(way(skc5), true, true, true)=true)). % 4.61/2.09 tff(c_18, plain, (![U_16]: (ifeq2(female(U_16), true, human(U_16), true)=true))). % 4.61/2.09 tff(c_569, plain, (entity(skc4)=true)). % 4.61/2.09 tff(c_522, plain, (ifeq2(instrumentality(skc4), true, true, true)=true)). % 4.61/2.09 tff(c_531, plain, (object(skc4)=true)). % 4.61/2.09 tff(c_24, plain, (![U_19]: (ifeq2(object(U_19), true, entity(U_19), true)=true))). % 4.61/2.09 tff(c_497, plain, (artifact(skc4)=true)). % 4.61/2.09 tff(c_12, plain, (![U_13]: (ifeq2(drs(U_13), true, proposition(U_13), true)=true))). % 4.61/2.09 tff(c_36, plain, (![U_25]: (ifeq2(way(U_25), true, artifact(U_25), true)=true))). % 4.61/2.09 tff(c_463, plain, (object(skc5)=true)). % 4.61/2.09 tff(c_34, plain, (![U_24]: (ifeq2(artifact(U_24), true, object(U_24), true)=true))). % 4.61/2.09 tff(c_432, plain, (eventuality(skc6)=true)). % 4.61/2.09 tff(c_22, plain, (![U_18]: (ifeq2(man(U_18), true, male(U_18), true)=true))). % 4.61/2.09 tff(c_32, plain, (![U_23]: (ifeq2(event(U_23), true, eventuality(U_23), true)=true))). % 4.61/2.09 tff(c_14, plain, (![U_14]: (ifeq2(proposition(U_14), true, drs(U_14), true)=true))). % 4.61/2.09 tff(c_384, plain, (location(skc7)=true)). % 4.61/2.09 tff(c_28, plain, (![U_21]: (ifeq2(city(U_21), true, location(U_21), true)=true))). % 4.61/2.09 tff(c_20, plain, (![U_17]: (ifeq2(male(U_17), true, human(U_17), true)=true))). % 4.61/2.09 tff(c_343, plain, (artifact(skc5)=true)). % 4.61/2.09 tff(c_16, plain, (![U_15]: (ifeq2(woman(U_15), true, female(U_15), true)=true))). % 4.61/2.09 tff(c_315, plain, (instrumentality(skc5)=true)). % 4.61/2.09 tff(c_40, plain, (![U_27]: (ifeq2(instrumentality(U_27), true, artifact(U_27), true)=true))). % 4.61/2.09 tff(c_284, plain, (transport(skc5)=true)). % 4.61/2.09 tff(c_44, plain, (![U_29]: (ifeq2(vehicle(U_29), true, transport(U_29), true)=true))). % 4.61/2.09 tff(c_253, plain, (vehicle(skc5)=true)). % 4.61/2.09 tff(c_46, plain, (![U_30]: (ifeq2(car(U_30), true, vehicle(U_30), true)=true))). % 4.61/2.09 tff(c_48, plain, (![U_31]: (ifeq2(chevy(U_31), true, car(U_31), true)=true))). % 4.61/2.09 tff(c_42, plain, (![U_28]: (ifeq2(transport(U_28), true, instrumentality(U_28), true)=true))). % 4.61/2.09 tff(c_38, plain, (![U_26]: (ifeq2(street(U_26), true, way(U_26), true)=true))). % 4.61/2.10 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 4.61/2.10 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 4.61/2.10 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 4.61/2.10 tff(c_8, plain, (![U_10, V_11]: (event(skf1(U_10, V_11))=true))). % 4.61/2.10 tff(c_90, plain, (down(skc6, skc4)=true)). % 4.61/2.10 tff(c_88, plain, (in(skc6, skc7)=true)). % 4.61/2.10 tff(c_92, plain, (barrel(skc6, skc5)=true)). % 4.61/2.10 tff(c_70, plain, (event(skc6)=true)). % 4.61/2.10 tff(c_72, plain, (chevy(skc5)=true)). % 4.61/2.10 tff(c_68, plain, (city(skc7)=true)). % 4.61/2.10 tff(c_86, plain, (street(skc4)=true)). % 4.61/2.10 tff(c_66, plain, (hollywood(skc7)=true)). % 4.61/2.10 tff(c_84, plain, (way(skc4)=true)). % 4.61/2.10 tff(c_74, plain, (car(skc5)=true)). % 4.61/2.10 tff(c_76, plain, (white(skc5)=true)). % 4.61/2.10 tff(c_78, plain, (dirty(skc5)=true)). % 4.61/2.10 tff(c_80, plain, (old(skc5)=true)). % 4.61/2.10 tff(c_82, plain, (lonely(skc4)=true)). % 4.61/2.10 tff(c_112, plain, (b!=a)). % 4.61/2.10 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.61/2.10 %------------------------------------------------------------------------------