%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN456+1 : TPTP v9.0.0. Released v2.1.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 10:03:37 PM UTC 2025 % Result : CounterSatisfiable 70.12s 56.02s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SYN456+1 : TPTP v9.0.0. Released v2.1.0. % 0.11/0.12 % 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.33 % Computer : n020.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 : Wed Apr 9 07:33:34 EDT 2025 % 0.12/0.33 % CPUTime : % 70.12/56.02 % 70.12/56.02 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 70.12/56.02 % 70.12/56.02 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 70.12/56.03 %$ c3_1 > c2_1 > c1_1 > c0_1 > #nlpp > ndr1_0 > hskp9 > hskp8 > hskp7 > hskp6 > hskp5 > hskp4 > hskp30 > hskp3 > hskp29 > hskp28 > hskp27 > hskp26 > hskp25 > hskp24 > hskp23 > hskp22 > hskp21 > hskp20 > hskp2 > hskp19 > hskp18 > hskp17 > hskp16 > hskp15 > hskp14 > hskp13 > hskp12 > hskp11 > hskp10 > hskp1 > hskp0 > a997 > a996 > a995 > a994 > a992 > a991 > a990 > a989 > a988 > a1059 > a1058 > a1051 > a1045 > a1040 > a1037 > a1032 > a1028 > a1025 > a1021 > a1019 > a1017 > a1016 > a1015 > a1012 > a1009 > a1008 > a1007 > a1004 > a1003 > a1002 > a1000 % 70.12/56.03 % 70.12/56.03 %Foreground sorts: % 70.12/56.03 % 70.12/56.03 % 70.12/56.03 %Background operators: % 70.12/56.03 % 70.12/56.03 % 70.12/56.03 %Foreground operators: % 70.12/56.03 tff(a988, type, a988: $i). % 70.12/56.03 tff(hskp17, type, hskp17: $o). % 70.12/56.03 tff(hskp19, type, hskp19: $o). % 70.12/56.03 tff(a1000, type, a1000: $i). % 70.12/56.03 tff(a989, type, a989: $i). % 70.12/56.03 tff(a1003, type, a1003: $i). % 70.12/56.03 tff(hskp6, type, hskp6: $o). % 70.12/56.03 tff(a1028, type, a1028: $i). % 70.12/56.03 tff(a991, type, a991: $i). % 70.12/56.03 tff(hskp10, type, hskp10: $o). % 70.12/56.03 tff(a990, type, a990: $i). % 70.12/56.03 tff(a1025, type, a1025: $i). % 70.12/56.03 tff(a1021, type, a1021: $i). % 70.12/56.03 tff(hskp23, type, hskp23: $o). % 70.12/56.03 tff(hskp13, type, hskp13: $o). % 70.12/56.03 tff(hskp14, type, hskp14: $o). % 70.12/56.03 tff(hskp18, type, hskp18: $o). % 70.12/56.03 tff(a1007, type, a1007: $i). % 70.12/56.03 tff(hskp5, type, hskp5: $o). % 70.12/56.03 tff(a1015, type, a1015: $i). % 70.12/56.03 tff(hskp12, type, hskp12: $o). % 70.12/56.03 tff(a994, type, a994: $i). % 70.12/56.03 tff(a1037, type, a1037: $i). % 70.12/56.03 tff(hskp29, type, hskp29: $o). % 70.12/56.03 tff(a1012, type, a1012: $i). % 70.12/56.03 tff(a1009, type, a1009: $i). % 70.12/56.03 tff(hskp2, type, hskp2: $o). % 70.12/56.03 tff(a1017, type, a1017: $i). % 70.12/56.03 tff(a1008, type, a1008: $i). % 70.12/56.03 tff(hskp28, type, hskp28: $o). % 70.12/56.03 tff(a1002, type, a1002: $i). % 70.12/56.03 tff(hskp1, type, hskp1: $o). % 70.12/56.03 tff(hskp27, type, hskp27: $o). % 70.12/56.03 tff(hskp3, type, hskp3: $o). % 70.12/56.03 tff(a1051, type, a1051: $i). % 70.12/56.03 tff(c2_1, type, c2_1: $i > $o). % 70.12/56.03 tff(a992, type, a992: $i). % 70.12/56.03 tff(a1004, type, a1004: $i). % 70.12/56.03 tff(hskp4, type, hskp4: $o). % 70.12/56.03 tff(c0_1, type, c0_1: $i > $o). % 70.12/56.03 tff(hskp20, type, hskp20: $o). % 70.12/56.03 tff(a1058, type, a1058: $i). % 70.12/56.03 tff(hskp16, type, hskp16: $o). % 70.12/56.03 tff(hskp11, type, hskp11: $o). % 70.12/56.03 tff(hskp30, type, hskp30: $o). % 70.12/56.03 tff(a1016, type, a1016: $i). % 70.12/56.03 tff(hskp24, type, hskp24: $o). % 70.12/56.03 tff(hskp26, type, hskp26: $o). % 70.12/56.03 tff(a1045, type, a1045: $i). % 70.12/56.03 tff(ndr1_0, type, ndr1_0: $o). % 70.12/56.03 tff(hskp25, type, hskp25: $o). % 70.12/56.03 tff(a1019, type, a1019: $i). % 70.12/56.03 tff(hskp22, type, hskp22: $o). % 70.12/56.03 tff(a1059, type, a1059: $i). % 70.12/56.03 tff(hskp9, type, hskp9: $o). % 70.12/56.03 tff(c1_1, type, c1_1: $i > $o). % 70.12/56.03 tff(a1032, type, a1032: $i). % 70.12/56.03 tff(a997, type, a997: $i). % 70.12/56.03 tff(a1040, type, a1040: $i). % 70.12/56.03 tff(hskp8, type, hskp8: $o). % 70.12/56.03 tff(hskp15, type, hskp15: $o). % 70.12/56.03 tff(a995, type, a995: $i). % 70.12/56.03 tff(hskp0, type, hskp0: $o). % 70.12/56.03 tff(a996, type, a996: $i). % 70.12/56.03 tff(hskp7, type, hskp7: $o). % 70.12/56.03 tff(hskp21, type, hskp21: $o). % 70.12/56.03 tff(c3_1, type, c3_1: $i > $o). % 70.12/56.03 % 70.12/56.03 %Saturated clause set: % 70.12/56.03 tff(c_913524, plain, (![W_3]: (~c1_1(W_3) | c2_1(W_3) | c0_1(W_3)))). % 70.12/56.03 tff(c_913489, plain, (~c0_1(a1008))). % 70.12/56.03 tff(c_913461, plain, (![X64_70]: (~c0_1(X64_70) | c3_1(X64_70) | c1_1(X64_70)))). % 70.12/56.03 tff(c_913392, plain, (![X38_44]: (~c2_1(X38_44) | ~c1_1(X38_44) | c3_1(X38_44)))). % 70.12/56.03 tff(c_913329, plain, (![X55_61]: (c2_1(X55_61) | c1_1(X55_61)))). % 70.12/56.03 tff(c_913266, plain, (![X69_75]: (~c1_1(X69_75) | ~c0_1(X69_75)))). % 70.12/56.03 tff(c_913231, plain, (c2_1(a995))). % 70.12/56.03 tff(c_913278, plain, (~c1_1(a1009))). % 70.12/56.03 tff(c_913274, plain, (~c0_1(a1019))). % 70.12/56.03 tff(c_913201, plain, (![X70_76]: (~c3_1(X70_76) | ~c0_1(X70_76) | c2_1(X70_76)))). % 70.12/56.03 tff(c_913162, plain, (![X29_35]: (~c3_1(X29_35) | c2_1(X29_35) | c0_1(X29_35)))). % 70.12/56.03 tff(c_913115, plain, (![X73_79]: (~c3_1(X73_79) | ~c1_1(X73_79) | c2_1(X73_79)))). % 70.12/56.03 tff(c_913102, plain, (c0_1(a1058))). % 70.12/56.04 tff(c_913094, plain, (c1_1(a1004))). % 70.12/56.04 tff(c_913069, plain, (![X22_28]: (~c3_1(X22_28) | c1_1(X22_28) | c0_1(X22_28)))). % 70.12/56.04 tff(c_913063, plain, (c2_1(a992))). % 70.12/56.04 tff(c_913050, plain, (c3_1(a1009))). % 70.12/56.04 tff(c_913048, plain, (c3_1(a1004))). % 70.12/56.04 tff(c_913038, plain, (~hskp10)). % 70.12/56.04 tff(c_913035, plain, (~hskp11)). % 70.12/56.04 tff(c_913034, plain, (~hskp22)). % 70.12/56.04 tff(c_913033, plain, (~hskp21)). % 70.12/56.04 tff(c_913032, plain, (~c0_1(a992))). % 70.12/56.04 tff(c_913030, plain, (c3_1(a1019))). % 70.12/56.04 tff(c_913028, plain, (~c1_1(a992))). % 70.12/56.04 tff(c_913026, plain, (c3_1(a995))). % 70.12/56.04 tff(c_913024, plain, (c3_1(a1058))). % 70.12/56.04 tff(c_913021, plain, (~c1_1(a995))). % 70.12/56.04 tff(c_913019, plain, (~hskp29)). % 70.12/56.04 tff(c_913018, plain, (c0_1(a1009))). % 70.12/56.04 tff(c_913016, plain, (c2_1(a1059))). % 70.12/56.04 tff(c_913014, plain, (~hskp20)). % 70.12/56.04 tff(c_913013, plain, (c2_1(a1019))). % 70.12/56.04 tff(c_913008, plain, (c0_1(a995))). % 70.12/56.04 tff(c_913009, plain, (hskp6)). % 70.12/56.04 tff(c_913011, plain, (~c1_1(a1058))). % 70.12/56.04 tff(c_912384, plain, (~hskp3)). % 70.12/56.04 tff(c_912383, plain, (~c1_1(a1008))). % 70.12/56.04 tff(c_912377, plain, (~c3_1(a992))). % 70.12/56.04 tff(c_912375, plain, (~c1_1(a1059))). % 70.12/56.04 tff(c_912373, plain, (~c3_1(a1008))). % 70.12/56.04 tff(c_912371, plain, (~hskp17)). % 70.12/56.04 tff(c_912368, plain, (~hskp23)). % 70.12/56.04 tff(c_912367, plain, (~hskp30)). % 70.12/56.04 tff(c_912366, plain, (~hskp16)). % 70.12/56.04 tff(c_912365, plain, (~hskp2)). % 70.12/56.04 tff(c_912364, plain, (~hskp19)). % 70.12/56.04 tff(c_912363, plain, (~hskp15)). % 70.12/56.04 tff(c_912362, plain, (~hskp9)). % 70.12/56.04 tff(c_912361, plain, (~c0_1(a1004))). % 70.12/56.04 tff(c_912359, plain, (~hskp8)). % 70.12/56.04 tff(c_912357, plain, (c2_1(a1008))). % 70.12/56.04 tff(c_912358, plain, (hskp14)). % 70.12/56.04 tff(c_882787, plain, (~hskp7)). % 70.12/56.04 tff(c_882786, plain, (~hskp18)). % 70.12/56.04 tff(c_882784, plain, (c0_1(a1059))). % 70.12/56.04 tff(c_882785, plain, (hskp26)). % 70.12/56.04 tff(c_750454, plain, (c2_1(a1009))). % 70.12/56.04 tff(c_750455, plain, (hskp27)). % 70.12/56.04 tff(c_261201, plain, (c2_1(a1058))). % 70.12/56.04 tff(c_581443, plain, (c2_1(a1004))). % 70.12/56.04 tff(c_581444, plain, (hskp12)). % 70.12/56.04 tff(c_261202, plain, (hskp25)). % 70.12/56.04 tff(c_640, plain, (~hskp13)). % 70.12/56.04 tff(c_638, plain, (c1_1(a1019))). % 70.12/56.04 tff(c_639, plain, (hskp28)). % 70.12/56.04 tff(c_453, plain, (~hskp5)). % 70.12/56.04 tff(c_451, plain, (~hskp24)). % 70.12/56.04 tff(c_422, plain, (hskp4)). % 70.12/56.04 tff(c_421, plain, (ndr1_0)). % 70.12/56.04 tff(c_370, plain, (~hskp1)). % 70.12/56.04 tff(c_369, plain, (~hskp0)). % 70.12/56.04 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 70.12/56.04 %------------------------------------------------------------------------------