%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN797-1 : TPTP v9.0.0. Released v2.5.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 : n023.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:04:55 PM UTC 2025 % Result : Satisfiable 13.77s 5.50s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN797-1 : TPTP v9.0.0. Released v2.5.0. % 0.03/0.13 % 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.34 % Computer : n023.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 : Wed Apr 9 08:21:39 EDT 2025 % 0.13/0.34 % CPUTime : % 13.77/5.50 % 13.77/5.50 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.88/5.51 % 13.88/5.51 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.88/5.51 %$ ssRr > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf3 > skf2 % 13.88/5.51 % 13.88/5.51 %Foreground sorts: % 13.88/5.51 % 13.88/5.51 % 13.88/5.51 %Background operators: % 13.88/5.51 % 13.88/5.51 % 13.88/5.51 %Foreground operators: % 13.88/5.51 tff(skf3, type, skf3: $i > $i). % 13.88/5.51 tff(ssPv1, type, ssPv1: $i > $o). % 13.88/5.51 tff(ssPv3, type, ssPv3: $i > $o). % 13.88/5.51 tff(skf2, type, skf2: $i > $i). % 13.88/5.51 tff(ssRr, type, ssRr: ($i * $i) > $o). % 13.88/5.51 tff(ssPv4, type, ssPv4: $i > $o). % 13.88/5.51 tff(ssPv2, type, ssPv2: $i > $o). % 13.88/5.51 % 13.88/5.51 %Saturated clause set: % 13.88/5.51 tff(c_23233, plain, (![U_2, W_1382, U_1384]: (ssPv4(U_2) | ssPv3(W_1382) | ~ssRr(U_2, W_1382) | ~ssPv4(U_1384) | ~ssRr(U_1384, U_2)))). % 13.88/5.51 tff(c_22732, plain, (![U_2, W_453, V_454]: (ssPv4(U_2) | ssPv3(W_453) | ~ssRr(U_2, W_453) | ~ssPv3(V_454) | ~ssRr(U_2, V_454)))). % 13.88/5.52 tff(c_22802, plain, (![U_35, W_37, V_36]: (ssPv4(U_35) | ssPv2(W_37) | ~ssRr(U_35, W_37) | ~ssPv4(V_36) | ~ssRr(U_35, V_36)))). % 13.88/5.52 tff(c_22723, plain, (![U_1, U_795]: (ssPv4(skf3(U_1)) | ssPv3(U_1) | ~ssPv4(U_795) | ~ssRr(U_795, skf3(U_1))))). % 13.88/5.52 tff(c_22719, plain, (![U_1, V_809]: (ssPv4(skf3(U_1)) | ssPv3(U_1) | ~ssPv3(V_809) | ~ssRr(skf3(U_1), V_809)))). % 13.88/5.52 tff(c_22939, plain, (![U_1, U_1324]: (ssPv3(skf3(U_1)) | ssPv2(U_1) | ~ssPv2(U_1324) | ~ssRr(U_1324, skf3(U_1))))). % 13.88/5.52 tff(c_22762, plain, (![U_1, V_243]: (ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv4(V_243) | ~ssRr(skf3(U_1), V_243)))). % 13.88/5.52 tff(c_22783, plain, (![V_108, W_109, U_107]: (~ssPv3(V_108) | ~ssPv2(W_109) | ~ssRr(V_108, W_109) | ~ssPv3(U_107) | ~ssRr(U_107, V_108)))). % 13.88/5.52 tff(c_22992, plain, (![U_1, V_1332]: (ssPv2(U_1) | ssPv4(V_1332) | ~ssPv4(skf3(U_1)) | ~ssRr(skf3(U_1), V_1332)))). % 13.88/5.52 tff(c_23142, plain, (![U_1, U_1356]: (ssPv4(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1356) | ~ssRr(U_1356, skf3(U_1))))). % 13.88/5.52 tff(c_23064, plain, (![U_1, U_1344]: (ssPv2(skf3(U_1)) | ssPv2(U_1) | ssPv4(U_1344) | ~ssRr(U_1344, skf3(U_1))))). % 13.88/5.52 tff(c_22853, plain, (![U_1, U_1307]: (ssPv2(U_1) | ssPv3(U_1307) | ~ssPv3(skf3(U_1)) | ~ssRr(U_1307, skf3(U_1))))). % 13.88/5.52 tff(c_22737, plain, (![U_2, U_692]: (ssPv4(U_2) | ssPv3(skf2(U_2)) | ~ssPv4(U_692) | ~ssRr(U_692, U_2)))). % 13.88/5.52 tff(c_22790, plain, (![V_72, W_73, U_71]: (ssPv4(V_72) | ~ssPv4(W_73) | ~ssRr(V_72, W_73) | ~ssPv3(U_71) | ~ssRr(U_71, V_72)))). % 13.88/5.52 tff(c_22731, plain, (![U_2, V_748]: (ssPv4(U_2) | ssPv3(skf2(U_2)) | ~ssPv3(V_748) | ~ssRr(U_2, V_748)))). % 13.88/5.52 tff(c_22789, plain, (![U_2, U_318]: (ssPv4(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv3(U_318) | ~ssRr(U_318, U_2)))). % 13.88/5.52 tff(c_22797, plain, (![U_2, U_271]: (ssPv3(U_2) | ssPv2(skf2(U_2)) | ~ssPv2(U_271) | ~ssRr(U_271, U_2)))). % 13.88/5.52 tff(c_23065, plain, (![U_2, U_1344]: (ssPv2(U_2) | ssPv2(skf2(U_2)) | ssPv4(U_1344) | ~ssRr(U_1344, U_2)))). % 13.88/5.52 tff(c_22722, plain, (![U_797]: (ssPv4(skf3(U_797)) | ssPv3(U_797) | ~ssPv4(skf3(skf3(U_797)))))). % 13.88/5.52 tff(c_22787, plain, (![V_18, W_19, U_17]: (ssPv2(V_18) | ssPv2(W_19) | ssPv4(U_17) | ~ssRr(V_18, W_19) | ~ssRr(U_17, V_18)))). % 13.88/5.52 tff(c_22763, plain, (![U_540]: (ssPv2(skf3(U_540)) | ssPv2(U_540) | ssPv4(skf3(skf3(U_540)))))). % 13.88/5.52 tff(c_22751, plain, (![U_598]: (ssPv3(skf3(U_598)) | ssPv2(U_598) | ~ssPv2(skf3(skf3(U_598)))))). % 13.88/5.52 tff(c_22760, plain, (![U_573]: (ssPv4(skf3(U_573)) | ssPv2(U_573) | ~ssPv4(skf2(skf3(U_573)))))). % 13.88/5.52 tff(c_22775, plain, (![U_1]: (ssPv2(skf2(skf3(U_1))) | ssPv4(U_1) | ~ssPv4(skf3(U_1))))). % 13.88/5.52 tff(c_22993, plain, (![U_2, V_1332]: (ssPv2(skf2(U_2)) | ssPv4(V_1332) | ~ssPv4(U_2) | ~ssRr(U_2, V_1332)))). % 13.88/5.52 tff(c_22795, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv2(skf2(skf2(U_2))) | ~ssPv2(U_2)))). % 13.88/5.52 tff(c_22753, plain, (![U_590]: (ssPv2(U_590) | ssPv3(skf3(skf3(U_590))) | ~ssPv3(skf3(U_590))))). % 13.88/5.52 tff(c_22777, plain, (![W_31, V_30, U_29]: (ssPv2(W_31) | ssPv4(V_30) | ~ssPv4(U_29) | ~ssRr(U_29, W_31) | ~ssRr(U_29, V_30)))). % 13.88/5.52 tff(c_22791, plain, (![U_1, U_311]: (ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv3(U_311) | ~ssRr(U_311, U_1)))). % 13.88/5.52 tff(c_22666, plain, (![U_1256]: (ssPv2(U_1256) | ssPv3(skf3(U_1256)) | ssPv4(skf3(U_1256))))). % 13.88/5.52 tff(c_22854, plain, (![U_2, U_1307]: (ssPv2(skf2(U_2)) | ssPv3(U_1307) | ~ssPv3(U_2) | ~ssRr(U_1307, U_2)))). % 13.88/5.52 tff(c_22841, plain, (![U_553]: (ssPv4(U_553) | ~ssPv4(skf3(U_553)) | ~ssPv2(skf3(U_553))))). % 13.88/5.52 tff(c_22798, plain, (![V_39, W_40, U_38]: (ssPv3(V_39) | ssPv2(W_40) | ~ssRr(V_39, W_40) | ~ssPv2(U_38) | ~ssRr(U_38, V_39)))). % 13.88/5.52 tff(c_22736, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf2(U_1)) | ~ssPv4(skf3(U_1))))). % 13.88/5.52 tff(c_22785, plain, (![U_1]: (ssPv2(U_1) | ssPv2(skf2(U_1)) | ssPv4(skf3(U_1))))). % 13.88/5.52 tff(c_22884, plain, (![U_2, U_1314]: (ssPv2(U_2) | ssPv3(U_1314) | ~ssPv3(U_2) | ~ssRr(U_1314, U_2)))). % 13.88/5.52 tff(c_22796, plain, (![U_1]: (ssPv3(U_1) | ssPv2(skf2(U_1)) | ~ssPv2(skf3(U_1))))). % 13.88/5.52 tff(c_22804, plain, (![U_1]: (ssPv2(skf2(U_1)) | ssPv3(skf3(U_1)) | ~ssPv3(U_1)))). % 13.88/5.52 tff(c_22772, plain, (![U_1]: (ssPv2(U_1) | ssPv3(skf3(U_1)) | ~ssPv3(U_1)))). % 13.88/5.52 tff(c_22761, plain, (![U_1]: (ssPv4(skf3(U_1)) | ssPv2(U_1) | ~ssPv4(U_1)))). % 13.88/5.52 tff(c_22819, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv2(U_2) | ~ssPv2(skf2(U_2))))). % 13.88/5.52 tff(c_22670, plain, (![U_618]: (ssPv4(U_618) | ssPv2(skf3(U_618))))). % 13.88/5.52 tff(c_22806, plain, (![W_34, U_32, V_33]: (ssPv2(W_34) | ssPv3(U_32) | ~ssPv3(V_33) | ~ssRr(V_33, W_34) | ~ssRr(U_32, V_33)))). % 13.88/5.52 tff(c_22671, plain, (![U_1247]: (ssPv4(U_1247) | ~ssPv3(skf2(U_1247))))). % 13.88/5.52 tff(c_22669, plain, (![U_1251]: (ssPv4(U_1251) | ~ssPv3(skf3(U_1251))))). % 13.88/5.52 tff(c_22682, plain, (![U_1191]: (~ssPv2(U_1191) | ~ssPv3(skf3(U_1191))))). % 13.88/5.52 tff(c_22681, plain, (![U_1193]: (ssPv3(U_1193) | ~ssPv3(skf2(U_1193))))). % 13.88/5.52 tff(c_22683, plain, (![U_2]: (~ssPv2(skf2(U_2)) | ~ssPv3(U_2)))). % 13.88/5.52 tff(c_22767, plain, (![U_2]: (ssPv2(skf2(U_2)) | ssPv4(U_2)))). % 13.88/5.52 tff(c_22684, plain, (![U_1058]: (~ssPv2(U_1058) | ~ssPv3(U_1058)))). % 13.88/5.52 tff(c_22809, plain, (![V_8, U_7]: (ssPv4(V_8) | ssPv2(U_7) | ~ssPv2(V_8) | ~ssRr(U_7, V_8)))). % 13.88/5.52 tff(c_22651, plain, (![U_1294]: (~ssPv1(U_1294)))). % 13.88/5.53 tff(c_21179, plain, (![U_2, U_1232]: (ssPv4(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv3(U_1232) | ~ssRr(U_1232, skf2(U_2)) | ~ssPv3(skf2(skf2(U_2)))))). % 13.88/5.53 tff(c_21152, plain, (![U_2, U_1226]: (ssPv4(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv3(U_1226) | ~ssRr(U_1226, skf2(U_2)) | ssPv2(skf2(skf2(U_2)))))). % 13.88/5.53 tff(c_21178, plain, (![U_1, U_1232]: (ssPv4(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv3(U_1232) | ~ssRr(U_1232, U_1) | ~ssPv3(skf2(U_1))))). % 13.88/5.53 tff(c_18667, plain, (![W_477, U_2, U_480]: (ssPv4(W_477) | ~ssPv2(U_2) | ~ssRr(W_477, U_2) | ~ssPv3(U_480) | ~ssRr(U_480, U_2) | ~ssPv3(skf2(U_2))))). % 13.88/5.53 tff(c_21151, plain, (![U_1, U_1226]: (ssPv4(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv3(U_1226) | ~ssRr(U_1226, U_1) | ssPv2(skf2(U_1))))). % 13.88/5.53 tff(c_18718, plain, (![W_477, U_2, U_480]: (ssPv4(W_477) | ~ssPv2(U_2) | ~ssRr(W_477, U_2) | ~ssPv3(U_480) | ~ssRr(U_480, U_2) | ssPv2(skf2(U_2))))). % 13.88/5.53 tff(c_19830, plain, (![U_2, U_1167]: (ssPv4(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv3(U_1167) | ~ssRr(U_1167, skf2(U_2)) | ~ssPv4(skf2(U_2))))). % 13.88/5.53 tff(c_19829, plain, (![U_1, U_1167]: (ssPv4(skf3(U_1)) | ~ssPv2(U_1) | ~ssPv3(U_1167) | ~ssRr(U_1167, U_1) | ~ssPv4(U_1)))). % 13.88/5.53 tff(c_18764, plain, (![W_477, U_1105, U_480]: (ssPv4(W_477) | ~ssPv2(U_1105) | ~ssRr(W_477, U_1105) | ~ssPv3(U_480) | ~ssRr(U_480, U_1105) | ~ssPv4(U_1105)))). % 13.88/5.53 tff(c_18612, plain, (![U_2]: (ssPv4(skf2(U_2)) | ~ssPv4(U_2)))). % 13.88/5.53 tff(c_18611, plain, (![U_1]: (ssPv4(skf3(U_1)) | ~ssPv3(U_1)))). % 13.88/5.53 tff(c_18614, plain, (![U_642]: (ssPv4(U_642) | ssPv2(U_642)))). % 13.88/5.53 tff(c_18610, plain, (![U_1058]: (~ssPv3(U_1058) | ssPv4(U_1058)))). % 13.88/5.53 tff(c_18316, plain, (![U_1093]: (~ssPv2(skf3(U_1093)) | ~ssPv3(U_1093)))). % 13.88/5.53 tff(c_8251, plain, (![U_782, U_783]: (ssPv4(skf3(skf3(U_782))) | ~ssPv2(skf3(U_782)) | ~ssPv4(U_782) | ~ssPv3(U_783) | ~ssRr(U_783, skf3(U_782))))). % 13.88/5.53 tff(c_2220, plain, (![W_477, U_1, U_480]: (ssPv4(W_477) | ~ssPv2(skf3(U_1)) | ~ssPv4(U_1) | ~ssRr(W_477, skf3(U_1)) | ~ssPv3(U_480) | ~ssRr(U_480, skf3(U_1))))). % 13.88/5.53 tff(c_2221, plain, (![W_477, U_2, U_480]: (ssPv4(W_477) | ~ssPv2(U_2) | ~ssPv4(skf2(U_2)) | ~ssRr(W_477, U_2) | ~ssPv3(U_480) | ~ssRr(U_480, U_2)))). % 13.88/5.53 tff(c_2287, plain, (![U_2, W_486, U_487]: (~ssPv2(U_2) | ~ssPv3(skf2(U_2)) | ~ssPv2(W_486) | ~ssRr(W_486, U_2) | ~ssPv3(U_487) | ~ssRr(U_487, U_2)))). % 13.88/5.53 tff(c_104, plain, (![V_152, X_154, W_153, U_151]: (~ssPv2(V_152) | ~ssPv3(X_154) | ~ssRr(V_152, X_154) | ~ssPv2(W_153) | ~ssRr(W_153, V_152) | ~ssPv3(U_151) | ~ssRr(U_151, V_152)))). % 13.88/5.53 tff(c_102, plain, (![W_149, V_148, X_150, U_147]: (ssPv4(W_149) | ~ssPv2(V_148) | ~ssPv4(X_150) | ~ssRr(V_148, X_150) | ~ssRr(W_149, V_148) | ~ssPv3(U_147) | ~ssRr(U_147, V_148)))). % 13.88/5.53 tff(c_58, plain, (![W_76, V_75, U_74]: (ssPv4(W_76) | ~ssPv4(V_75) | ~ssPv3(V_75) | ~ssRr(W_76, V_75) | ~ssPv3(U_74) | ~ssRr(U_74, V_75)))). % 13.88/5.53 tff(c_48, plain, (![V_60, U_59, W_61]: (ssPv4(V_60) | ssPv4(U_59) | ~ssPv2(V_60) | ~ssPv3(W_61) | ~ssRr(V_60, W_61) | ~ssRr(U_59, V_60)))). % 13.88/5.53 tff(c_1358, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv2(skf2(U_2)) | ssPv4(skf2(skf2(U_2))) | ~ssPv3(U_2)))). % 13.88/5.53 tff(c_1357, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ssPv4(skf2(U_1)) | ~ssPv3(skf3(U_1))))). % 13.88/5.53 tff(c_1351, plain, (![U_2, U_378]: (ssPv3(U_2) | ssPv2(U_2) | ssPv4(skf2(U_2)) | ~ssPv3(U_378) | ~ssRr(U_378, U_2)))). % 13.88/5.53 tff(c_26, plain, (![V_27, W_28, U_26]: (ssPv3(V_27) | ssPv2(V_27) | ssPv4(W_28) | ~ssRr(V_27, W_28) | ~ssPv3(U_26) | ~ssRr(U_26, V_27)))). % 13.88/5.53 tff(c_72, plain, (![V_96, W_97, U_95]: (ssPv4(V_96) | ~ssPv2(V_96) | ~ssPv3(W_97) | ~ssRr(V_96, W_97) | ~ssPv3(U_95) | ~ssRr(U_95, V_96)))). % 13.88/5.53 tff(c_36, plain, (![W_43, U_41, V_42]: (ssPv4(W_43) | ssPv3(U_41) | ~ssPv4(V_42) | ~ssPv2(V_42) | ~ssRr(V_42, W_43) | ~ssRr(U_41, V_42)))). % 13.88/5.53 tff(c_16, plain, (![U_13, V_14]: (ssPv3(U_13) | ~ssPv4(U_13) | ~ssPv2(U_13) | ~ssPv3(V_14) | ~ssRr(U_13, V_14)))). % 13.88/5.53 tff(c_2, plain, (![U_1]: (ssRr(skf3(U_1), U_1)))). % 13.88/5.53 tff(c_4, plain, (![U_2]: (ssRr(U_2, skf2(U_2))))). % 13.88/5.53 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.88/5.53 %------------------------------------------------------------------------------