%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP221-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 : n012.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:39 PM UTC 2025 % Result : Satisfiable 4.69s 2.06s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : NLP221-1 : TPTP v9.0.0. Released v2.4.0. % 0.07/0.14 % 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.14/0.34 % Computer : n012.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Tue Apr 8 09:26:45 EDT 2025 % 0.14/0.35 % CPUTime : % 4.69/2.05 % 4.69/2.06 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.69/2.06 % 4.69/2.06 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.69/2.06 %$ be > theme > of > agent > vincent_forename > think_believe_consider > state > smoke > proposition > present > man > jules_forename > forename > event > accessible_world > actual_world > #nlpp > skf7 > skf5 > skf13 > skf11 > ssSkC0 > skc36 > skc35 > skc34 > skc33 > skc32 > skc31 > skc30 > skc29 > skc25 > skc24 > skc23 > skc22 > skc21 > skc20 > skc19 > skc18 > skc17 % 4.69/2.06 % 4.69/2.06 %Foreground sorts: % 4.69/2.06 % 4.69/2.06 % 4.69/2.06 %Background operators: % 4.69/2.06 % 4.69/2.06 % 4.69/2.06 %Foreground operators: % 4.69/2.06 tff(forename, type, forename: ($i * $i) > $o). % 4.69/2.06 tff(be, type, be: ($i * $i * $i * $i) > $o). % 4.69/2.06 tff(skc34, type, skc34: $i). % 4.69/2.06 tff(theme, type, theme: ($i * $i * $i) > $o). % 4.69/2.06 tff(present, type, present: ($i * $i) > $o). % 4.69/2.06 tff(skc18, type, skc18: $i). % 4.69/2.06 tff(skc29, type, skc29: $i). % 4.69/2.06 tff(skc25, type, skc25: $i). % 4.69/2.06 tff(proposition, type, proposition: ($i * $i) > $o). % 4.69/2.06 tff(skc17, type, skc17: $i). % 4.69/2.06 tff(of, type, of: ($i * $i * $i) > $o). % 4.69/2.06 tff(actual_world, type, actual_world: $i > $o). % 4.69/2.06 tff(agent, type, agent: ($i * $i * $i) > $o). % 4.69/2.06 tff(skc36, type, skc36: $i). % 4.69/2.06 tff(skc24, type, skc24: $i). % 4.69/2.06 tff(skc32, type, skc32: $i). % 4.69/2.06 tff(skc20, type, skc20: $i). % 4.69/2.06 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 4.69/2.06 tff(smoke, type, smoke: ($i * $i) > $o). % 4.69/2.06 tff(skf5, type, skf5: $i > $i). % 4.69/2.06 tff(skc23, type, skc23: $i). % 4.69/2.06 tff(event, type, event: ($i * $i) > $o). % 4.69/2.06 tff(skc21, type, skc21: $i). % 4.69/2.06 tff(skf7, type, skf7: $i > $i). % 4.69/2.06 tff(skc22, type, skc22: $i). % 4.69/2.06 tff(skf13, type, skf13: $i > $i). % 4.69/2.06 tff(state, type, state: ($i * $i) > $o). % 4.69/2.06 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 4.69/2.06 tff(man, type, man: ($i * $i) > $o). % 4.69/2.06 tff(skf11, type, skf11: $i > $i). % 4.69/2.06 tff(skc31, type, skc31: $i). % 4.69/2.06 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 4.69/2.06 tff(skc35, type, skc35: $i). % 4.69/2.06 tff(skc30, type, skc30: $i). % 4.69/2.06 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 4.69/2.06 tff(skc19, type, skc19: $i). % 4.69/2.06 tff(ssSkC0, type, ssSkC0: $o). % 4.69/2.06 tff(skc33, type, skc33: $i). % 4.69/2.06 % 4.69/2.06 %Saturated clause set: % 4.69/2.07 tff(c_463, plain, (![U_34, W_32, Y_39, X3_33, Z_35, X_38, V_40, X1_36, X2_37]: (~actual_world(U_34) | ~of(U_34, X3_33, X2_37) | ~jules_forename(U_34, X3_33) | ~forename(U_34, X3_33) | ~be(U_34, V_40, X2_37, W_32) | ~agent(U_34, Z_35, X2_37) | ~man(U_34, X2_37) | ~of(U_34, X1_36, X2_37) | ~vincent_forename(U_34, X1_36) | ~forename(U_34, X1_36) | ~think_believe_consider(U_34, Z_35) | ~present(U_34, Z_35) | ~event(U_34, Z_35) | ~theme(U_34, Z_35, X_38) | ~proposition(U_34, X_38) | ~accessible_world(U_34, X_38) | ~event(X_38, Y_39) | ~agent(X_38, Y_39, skf7(X_38)) | ~present(X_38, Y_39) | ~smoke(X_38, Y_39) | ~man(U_34, W_32) | ~state(U_34, V_40)))). % 5.04/2.07 tff(c_461, plain, (~jules_forename(skc17, skc24))). % 5.04/2.07 tff(c_459, plain, (~vincent_forename(skc17, skc20))). % 5.04/2.07 tff(c_452, plain, (![Z_162]: (~of(skc17, Z_162, skc21) | ~vincent_forename(skc17, Z_162) | ~forename(skc17, Z_162)))). % 5.04/2.07 tff(c_430, plain, (![X2_19, Z_17, X1_18, X_20, Y_21, V_22, W_15, U_16]: (man(X_20, skf7(X_20)) | ~actual_world(U_16) | ~of(U_16, X2_19, X1_18) | ~jules_forename(U_16, X2_19) | ~forename(U_16, X2_19) | ~be(U_16, V_22, X1_18, W_15) | ~agent(U_16, Y_21, X1_18) | ~man(U_16, X1_18) | ~of(U_16, Z_17, X1_18) | ~vincent_forename(U_16, Z_17) | ~forename(U_16, Z_17) | ~think_believe_consider(U_16, Y_21) | ~present(U_16, Y_21) | ~event(U_16, Y_21) | ~theme(U_16, Y_21, X_20) | ~proposition(U_16, X_20) | ~accessible_world(U_16, X_20) | ~man(U_16, W_15) | ~state(U_16, V_22)))). % 5.04/2.07 tff(c_418, plain, (![U_7]: (~man(skc22, U_7)))). % 5.04/2.07 tff(c_414, plain, (be(skc17, skc18, skc21, skc19))). % 5.04/2.07 tff(c_411, plain, (theme(skc17, skc23, skc22))). % 5.04/2.07 tff(c_408, plain, (agent(skc17, skc23, skc25))). % 5.04/2.07 tff(c_403, plain, (of(skc17, skc20, skc21))). % 5.04/2.07 tff(c_401, plain, (of(skc17, skc24, skc25))). % 5.04/2.07 tff(c_399, plain, (state(skc17, skc18))). % 5.04/2.07 tff(c_397, plain, (man(skc17, skc25))). % 5.04/2.07 tff(c_395, plain, (forename(skc17, skc24))). % 5.04/2.07 tff(c_393, plain, (man(skc17, skc19))). % 5.04/2.07 tff(c_391, plain, (event(skc17, skc23))). % 5.04/2.07 tff(c_389, plain, (jules_forename(skc17, skc20))). % 5.04/2.07 tff(c_387, plain, (forename(skc17, skc20))). % 5.04/2.07 tff(c_385, plain, (man(skc17, skc21))). % 5.04/2.07 tff(c_380, plain, (think_believe_consider(skc17, skc23))). % 5.04/2.07 tff(c_376, plain, (proposition(skc17, skc22))). % 5.04/2.07 tff(c_371, plain, (accessible_world(skc17, skc22))). % 5.04/2.07 tff(c_365, plain, (vincent_forename(skc17, skc24))). % 5.04/2.07 tff(c_362, plain, (present(skc17, skc23))). % 5.04/2.07 tff(c_363, plain, (ssSkC0)). % 5.04/2.07 tff(c_2, plain, (actual_world(skc29))). % 5.04/2.07 tff(c_4, plain, (actual_world(skc17))). % 5.04/2.07 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.04/2.07 %------------------------------------------------------------------------------