%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP005-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 : 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:47:50 PM UTC 2025 % Result : Satisfiable 4.44s 2.03s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : NLP005-1 : TPTP v9.0.0. Released v2.4.0. % 0.08/0.13 % 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.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 08:05:04 EDT 2025 % 0.13/0.34 % CPUTime : % 4.44/2.03 % 4.44/2.03 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.44/2.04 % 4.44/2.04 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.62/2.04 %$ in > down > barrel > young > white > way > street > seat > old > man > lonely > hollywood > furniture > front > fellow > event > dirty > city > chevy > car > #nlpp > ssSkC0 > skc29 > skc28 > skc27 > skc26 > skc25 > skc24 > skc23 > skc22 > skc21 > skc20 > skc19 > skc18 > skc17 > skc16 > skc15 % 4.62/2.04 % 4.62/2.04 %Foreground sorts: % 4.62/2.04 % 4.62/2.04 % 4.62/2.04 %Background operators: % 4.62/2.04 % 4.62/2.04 % 4.62/2.04 %Foreground operators: % 4.62/2.04 tff(skc16, type, skc16: $i). % 4.62/2.04 tff(down, type, down: ($i * $i) > $o). % 4.62/2.04 tff(old, type, old: $i > $o). % 4.62/2.04 tff(front, type, front: $i > $o). % 4.62/2.04 tff(hollywood, type, hollywood: $i > $o). % 4.62/2.04 tff(skc18, type, skc18: $i). % 4.62/2.04 tff(skc29, type, skc29: $i). % 4.62/2.04 tff(skc25, type, skc25: $i). % 4.62/2.04 tff(city, type, city: $i > $o). % 4.62/2.04 tff(way, type, way: $i > $o). % 4.62/2.04 tff(seat, type, seat: $i > $o). % 4.62/2.04 tff(skc17, type, skc17: $i). % 4.62/2.04 tff(fellow, type, fellow: $i > $o). % 4.62/2.04 tff(furniture, type, furniture: $i > $o). % 4.62/2.04 tff(skc26, type, skc26: $i). % 4.62/2.04 tff(skc24, type, skc24: $i). % 4.62/2.04 tff(in, type, in: ($i * $i) > $o). % 4.62/2.04 tff(skc20, type, skc20: $i). % 4.62/2.04 tff(chevy, type, chevy: $i > $o). % 4.62/2.04 tff(man, type, man: $i > $o). % 4.62/2.04 tff(skc23, type, skc23: $i). % 4.62/2.04 tff(white, type, white: $i > $o). % 4.62/2.04 tff(skc21, type, skc21: $i). % 4.62/2.04 tff(skc22, type, skc22: $i). % 4.62/2.04 tff(barrel, type, barrel: ($i * $i) > $o). % 4.62/2.04 tff(skc27, type, skc27: $i). % 4.62/2.04 tff(skc15, type, skc15: $i). % 4.62/2.04 tff(dirty, type, dirty: $i > $o). % 4.62/2.04 tff(event, type, event: $i > $o). % 4.62/2.04 tff(car, type, car: $i > $o). % 4.62/2.04 tff(street, type, street: $i > $o). % 4.62/2.04 tff(skc19, type, skc19: $i). % 4.62/2.04 tff(ssSkC0, type, ssSkC0: $o). % 4.62/2.04 tff(lonely, type, lonely: $i > $o). % 4.62/2.04 tff(young, type, young: $i > $o). % 4.62/2.04 tff(skc28, type, skc28: $i). % 4.62/2.04 % 4.62/2.04 %Saturated clause set: % 4.62/2.04 tff(c_242, plain, (~fellow(skc21))). % 4.62/2.05 tff(c_224, plain, (![Y_23]: (skc15=Y_23 | ~in(Y_23, skc18) | ~fellow(Y_23) | ~man(Y_23) | ~young(Y_23)))). % 4.62/2.05 tff(c_221, plain, (![Y_23]: (skc16=Y_23 | ~in(Y_23, skc17) | ~fellow(Y_23) | ~man(Y_23) | ~young(Y_23)))). % 4.62/2.05 tff(c_210, plain, (![Z_3, Y_6, X1_4]: (Z_3=Y_6 | ~seat(X1_4) | ~furniture(X1_4) | ~front(X1_4) | ~in(Z_3, X1_4) | ~in(Y_6, X1_4) | ~young(Z_3) | ~man(Z_3) | ~fellow(Z_3) | ~fellow(Y_6) | ~man(Y_6) | ~young(Y_6)))). % 4.62/2.05 tff(c_174, plain, (barrel(skc21, skc19))). % 4.62/2.05 tff(c_172, plain, (down(skc21, skc20))). % 4.62/2.05 tff(c_170, plain, (in(skc21, skc22))). % 4.62/2.05 tff(c_167, plain, (in(skc16, skc17))). % 4.62/2.05 tff(c_164, plain, (in(skc15, skc18))). % 4.62/2.05 tff(c_157, plain, (white(skc19))). % 4.62/2.05 tff(c_155, plain, (skc16!=skc15)). % 4.67/2.05 tff(c_152, plain, (dirty(skc19))). % 4.67/2.05 tff(c_150, plain, (man(skc16))). % 4.67/2.05 tff(c_146, plain, (furniture(skc18))). % 4.67/2.05 tff(c_144, plain, (young(skc16))). % 4.67/2.05 tff(c_142, plain, (fellow(skc15))). % 4.67/2.05 tff(c_140, plain, (seat(skc18))). % 4.67/2.05 tff(c_138, plain, (chevy(skc19))). % 4.67/2.05 tff(c_136, plain, (front(skc17))). % 4.67/2.05 tff(c_130, plain, (man(skc15))). % 4.67/2.05 tff(c_125, plain, (furniture(skc17))). % 4.67/2.05 tff(c_123, plain, (car(skc19))). % 4.67/2.05 tff(c_121, plain, (way(skc20))). % 4.67/2.05 tff(c_119, plain, (city(skc22))). % 4.67/2.05 tff(c_117, plain, (lonely(skc20))). % 4.67/2.05 tff(c_115, plain, (ssSkC0)). % 4.67/2.05 tff(c_12, plain, (young(skc24))). % 4.67/2.05 tff(c_14, plain, (fellow(skc23))). % 4.67/2.05 tff(c_16, plain, (hollywood(skc22))). % 4.67/2.05 tff(c_18, plain, (event(skc21))). % 4.67/2.05 tff(c_20, plain, (street(skc20))). % 4.67/2.05 tff(c_10, plain, (seat(skc25))). % 4.67/2.05 tff(c_8, plain, (street(skc26))). % 4.67/2.05 tff(c_4, plain, (event(skc28))). % 4.67/2.05 tff(c_2, plain, (city(skc29))). % 4.67/2.05 tff(c_22, plain, (old(skc19))). % 4.67/2.05 tff(c_24, plain, (front(skc18))). % 4.67/2.05 tff(c_6, plain, (old(skc27))). % 4.67/2.05 tff(c_26, plain, (seat(skc17))). % 4.67/2.05 tff(c_28, plain, (fellow(skc16))). % 4.67/2.05 tff(c_30, plain, (young(skc15))). % 4.67/2.05 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.67/2.05 %------------------------------------------------------------------------------