%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : KRS040+1 : TPTP v9.0.0. Released v3.1.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 : 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 07:07:12 PM UTC 2025 % Result : Satisfiable 15.83s 5.86s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.07 % Problem : KRS040+1 : TPTP v9.0.0. Released v3.1.0. % 0.06/0.08 % 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.09/0.27 % Computer : n023.cluster.edu % 0.09/0.27 % Model : x86_64 x86_64 % 0.09/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.27 % Memory : 8042.1875MB % 0.09/0.27 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.27 % CPULimit : 300 % 0.09/0.27 % WCLimit : 300 % 0.09/0.27 % DateTime : Tue Apr 8 02:55:24 EDT 2025 % 0.09/0.27 % CPUTime : % 15.83/5.86 % 15.83/5.86 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.83/5.87 % 15.83/5.87 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.83/5.87 %$ xsd_string > xsd_integer > cowlThing > cowlNothing > cTorF > #nlpp > iplus9 > iplus8 > iplus7 > iplus6 > iplus5 > iplus4 > iplus3 > iplus2 > iplus1 > iminus9 > iminus8 > iminus7 > iminus6 > iminus5 > iminus4 > iminus3 > iminus2 > iminus1 > iT > iF % 15.83/5.87 % 15.83/5.87 %Foreground sorts: % 15.83/5.87 % 15.83/5.87 % 15.83/5.87 %Background operators: % 15.83/5.87 % 15.83/5.87 % 15.83/5.87 %Foreground operators: % 15.83/5.87 tff(iplus4, type, iplus4: $i). % 15.83/5.87 tff(iminus8, type, iminus8: $i). % 15.83/5.87 tff(iplus1, type, iplus1: $i). % 15.83/5.87 tff(cowlThing, type, cowlThing: $i > $o). % 15.83/5.87 tff(iplus5, type, iplus5: $i). % 15.83/5.87 tff(iplus9, type, iplus9: $i). % 15.83/5.87 tff(iplus7, type, iplus7: $i). % 15.83/5.87 tff(iplus3, type, iplus3: $i). % 15.83/5.87 tff(iminus3, type, iminus3: $i). % 15.83/5.87 tff(iminus1, type, iminus1: $i). % 15.83/5.87 tff(xsd_integer, type, xsd_integer: $i > $o). % 15.83/5.87 tff(iminus7, type, iminus7: $i). % 15.83/5.87 tff(iplus2, type, iplus2: $i). % 15.83/5.87 tff(iF, type, iF: $i). % 15.83/5.87 tff(iT, type, iT: $i). % 15.83/5.87 tff(iplus6, type, iplus6: $i). % 15.83/5.87 tff(cTorF, type, cTorF: $i > $o). % 15.83/5.87 tff(iminus6, type, iminus6: $i). % 15.83/5.87 tff(iminus4, type, iminus4: $i). % 15.83/5.87 tff(iminus9, type, iminus9: $i). % 15.83/5.87 tff(iminus2, type, iminus2: $i). % 15.83/5.87 tff(xsd_string, type, xsd_string: $i > $o). % 15.83/5.87 tff(iplus8, type, iplus8: $i). % 15.83/5.87 tff(cowlNothing, type, cowlNothing: $i > $o). % 15.83/5.87 tff(iminus5, type, iminus5: $i). % 15.83/5.87 % 15.83/5.87 %Saturated clause set: % 15.83/5.87 tff(c_93721, plain, (iplus8=iT)). % 15.83/5.87 tff(c_93701, plain, (iminus2=iF)). % 15.83/5.87 tff(c_93698, plain, (iminus6=iF)). % 15.83/5.87 tff(c_93674, plain, (![X_16]: (iF=X_16 | iT=X_16 | ~cTorF(X_16)))). % 15.83/5.87 tff(c_93663, plain, (iplus6=iT)). % 15.83/5.87 tff(c_93645, plain, (iplus9=iF)). % 15.83/5.87 tff(c_93608, plain, (iminus8=iF)). % 15.83/5.87 tff(c_93613, plain, (iplus1=iF)). % 15.83/5.87 tff(c_93611, plain, (iplus4=iF)). % 15.83/5.87 tff(c_93610, plain, (iplus3=iF)). % 15.83/5.88 tff(c_93609, plain, (iplus5=iF)). % 15.83/5.88 tff(c_93607, plain, (iminus7=iF)). % 15.83/5.88 tff(c_93595, plain, (iminus4=iT)). % 15.83/5.88 tff(c_93587, plain, (iplus2=iT)). % 15.83/5.88 tff(c_93563, plain, (iminus9=iT)). % 15.83/5.88 tff(c_93099, plain, (iminus5=iT)). % 15.83/5.88 tff(c_93092, plain, (iminus3=iT)). % 15.83/5.88 tff(c_93089, plain, (iminus1=iT)). % 15.83/5.88 tff(c_82558, plain, (iplus7=iT)). % 15.83/5.88 tff(c_18, plain, (![X_12]: (xsd_string(X_12) | xsd_integer(X_12)))). % 15.83/5.88 tff(c_16, plain, (![X_12]: (~xsd_integer(X_12) | ~xsd_string(X_12)))). % 15.83/5.88 tff(c_76, plain, (cTorF(iT))). % 15.83/5.88 tff(c_78, plain, (cTorF(iF))). % 15.83/5.88 tff(c_12, plain, (![X_11]: (cowlThing(X_11)))). % 15.83/5.88 tff(c_14, plain, (![X_11]: (~cowlNothing(X_11)))). % 15.83/5.88 tff(c_210, plain, (iT!=iF)). % 15.83/5.88 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.83/5.88 %------------------------------------------------------------------------------