%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP006-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 : n005.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.10s 1.94s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP006-1 : TPTP v9.0.0. Released v2.4.0. % 0.11/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.12/0.33 % Computer : n005.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Apr 8 08:04:57 EDT 2025 % 0.12/0.34 % CPUTime : % 4.10/1.94 % 4.10/1.94 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.10/1.94 % 4.10/1.94 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.10/1.95 %$ 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.10/1.95 % 4.10/1.95 %Foreground sorts: % 4.10/1.95 % 4.10/1.95 % 4.10/1.95 %Background operators: % 4.10/1.95 % 4.10/1.95 % 4.10/1.95 %Foreground operators: % 4.10/1.95 tff(skc16, type, skc16: $i). % 4.10/1.95 tff(down, type, down: ($i * $i) > $o). % 4.10/1.95 tff(old, type, old: $i > $o). % 4.10/1.95 tff(front, type, front: $i > $o). % 4.10/1.95 tff(hollywood, type, hollywood: $i > $o). % 4.10/1.95 tff(skc18, type, skc18: $i). % 4.10/1.95 tff(skc29, type, skc29: $i). % 4.10/1.95 tff(skc25, type, skc25: $i). % 4.10/1.95 tff(city, type, city: $i > $o). % 4.10/1.95 tff(way, type, way: $i > $o). % 4.10/1.95 tff(seat, type, seat: $i > $o). % 4.10/1.95 tff(skc17, type, skc17: $i). % 4.10/1.95 tff(fellow, type, fellow: $i > $o). % 4.10/1.95 tff(furniture, type, furniture: $i > $o). % 4.10/1.95 tff(skc26, type, skc26: $i). % 4.10/1.95 tff(skc24, type, skc24: $i). % 4.10/1.95 tff(in, type, in: ($i * $i) > $o). % 4.10/1.95 tff(skc20, type, skc20: $i). % 4.10/1.95 tff(chevy, type, chevy: $i > $o). % 4.10/1.95 tff(man, type, man: $i > $o). % 4.10/1.95 tff(skc23, type, skc23: $i). % 4.10/1.95 tff(white, type, white: $i > $o). % 4.10/1.95 tff(skc21, type, skc21: $i). % 4.10/1.95 tff(skc22, type, skc22: $i). % 4.10/1.95 tff(barrel, type, barrel: ($i * $i) > $o). % 4.10/1.95 tff(skc27, type, skc27: $i). % 4.10/1.95 tff(skc15, type, skc15: $i). % 4.10/1.95 tff(dirty, type, dirty: $i > $o). % 4.10/1.95 tff(event, type, event: $i > $o). % 4.10/1.95 tff(car, type, car: $i > $o). % 4.10/1.95 tff(street, type, street: $i > $o). % 4.10/1.95 tff(skc19, type, skc19: $i). % 4.10/1.95 tff(ssSkC0, type, ssSkC0: $o). % 4.10/1.95 tff(lonely, type, lonely: $i > $o). % 4.10/1.95 tff(young, type, young: $i > $o). % 4.10/1.95 tff(skc28, type, skc28: $i). % 4.10/1.95 % 4.10/1.95 %Saturated clause set: % 4.10/1.95 tff(c_329, plain, (~fellow(skc28))). % 4.10/1.95 tff(c_312, plain, (![Y_35]: (skc23=Y_35 | ~in(Y_35, skc24) | ~fellow(Y_35) | ~man(Y_35) | ~young(Y_35)))). % 4.10/1.95 tff(c_309, plain, (![Y_35]: (skc22=Y_35 | ~in(Y_35, skc25) | ~fellow(Y_35) | ~man(Y_35) | ~young(Y_35)))). % 4.10/1.95 tff(c_298, 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.10/1.95 tff(c_265, plain, (down(skc28, skc26))). % 4.10/1.95 tff(c_264, plain, (in(skc28, skc29))). % 4.10/1.95 tff(c_263, plain, (barrel(skc28, skc27))). % 4.10/1.96 tff(c_262, plain, (in(skc22, skc25))). % 4.10/1.96 tff(c_261, plain, (in(skc23, skc24))). % 4.10/1.96 tff(c_260, plain, (seat(skc25))). % 4.10/1.96 tff(c_259, plain, (white(skc27))). % 4.10/1.96 tff(c_258, plain, (dirty(skc27))). % 4.10/1.96 tff(c_257, plain, (furniture(skc25))). % 4.10/1.96 tff(c_256, plain, (chevy(skc27))). % 4.10/1.96 tff(c_255, plain, (front(skc24))). % 4.10/1.96 tff(c_254, plain, (young(skc23))). % 4.10/1.96 tff(c_253, plain, (car(skc27))). % 4.10/1.96 tff(c_252, plain, (skc23!=skc22)). % 4.10/1.96 tff(c_251, plain, (man(skc22))). % 4.10/1.96 tff(c_250, plain, (hollywood(skc29))). % 4.10/1.96 tff(c_249, plain, (furniture(skc24))). % 4.10/1.96 tff(c_248, plain, (way(skc26))). % 4.10/1.96 tff(c_247, plain, (fellow(skc22))). % 4.10/1.96 tff(c_246, plain, (man(skc23))). % 4.10/1.96 tff(c_244, plain, (lonely(skc26))). % 4.10/1.96 tff(c_245, plain, (~ssSkC0)). % 4.10/1.96 tff(c_12, plain, (seat(skc24))). % 4.10/1.96 tff(c_14, plain, (fellow(skc23))). % 4.10/1.96 tff(c_16, plain, (young(skc22))). % 4.10/1.96 tff(c_18, plain, (city(skc21))). % 4.10/1.96 tff(c_20, plain, (event(skc20))). % 4.10/1.96 tff(c_10, plain, (front(skc25))). % 4.10/1.96 tff(c_8, plain, (street(skc26))). % 4.10/1.96 tff(c_4, plain, (event(skc28))). % 4.10/1.96 tff(c_2, plain, (city(skc29))). % 4.10/1.96 tff(c_22, plain, (old(skc19))). % 4.10/1.96 tff(c_24, plain, (street(skc18))). % 4.10/1.96 tff(c_6, plain, (old(skc27))). % 4.10/1.96 tff(c_26, plain, (seat(skc17))). % 4.10/1.96 tff(c_28, plain, (young(skc16))). % 4.10/1.96 tff(c_30, plain, (fellow(skc15))). % 4.10/1.96 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.10/1.96 %------------------------------------------------------------------------------