%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYO582+1 : TPTP v8.1.0. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n026.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 : 600s % DateTime : Thu Jul 21 18:40:02 EDT 2022 % Result : CounterSatisfiable 0.18s 0.40s % Output : Saturation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.11 % Problem : SYO582+1 : TPTP v8.1.0. Released v5.5.0. % 0.04/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n026.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 : 600 % 0.12/0.33 % DateTime : Fri Jul 8 22:08:55 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.18/0.40 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.40 % 0.18/0.40 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.40 |- ~k04_buttercup10517 $X0 \/ k04_buttercup10516 $X0 % 0.18/0.40 |- ~b48_buttercup10518 $X1 \/ b48_buttercup10515 $X1 % 0.18/0.40 |- ~b48_buttercup10519 $X2 \/ b48_buttercup10515 $X2 % 0.18/0.40 |- ~b48_buttercup10520 $X3 \/ b48_buttercup10515 $X3 % 0.18/0.40 |- ~b48_buttercup10521 $X4 \/ b48_buttercup10515 $X4 % 0.18/0.40 |- ~b48_buttercup10421 $X5 \/ b48_buttercup10417 $X5 % 0.18/0.40 |- ~b48_buttercup10422 $X6 \/ b48_buttercup10417 $X6 % 0.18/0.40 |- ~b48_buttercup10227 $X7 \/ b48_buttercup10222 $X7 % 0.18/0.40 |- ~b48_buttercup10228 $X8 \/ b48_buttercup10222 $X8 % 0.18/0.40 |- ~b48_buttercup10229 $X9 \/ b48_buttercup10222 $X9 % 0.18/0.40 |- ~b48_buttercup10422 skolemFOFtoCNF_X11 % 0.18/0.40 |- k04_buttercup10419 skolemFOFtoCNF_X11 % 0.18/0.40 |- ~b48_buttercup10422 $X10 \/ k04_buttercup10419 $X10 % 0.18/0.40 |- ~b48_buttercup10227 skolemFOFtoCNF_X13 % 0.18/0.40 |- k04_buttercup10225 skolemFOFtoCNF_X13 % 0.18/0.40 |- ~b48_buttercup10227 $X12 \/ k04_buttercup10225 $X12 % 0.18/0.40 |- ~b48_buttercup10228 skolemFOFtoCNF_X15 % 0.18/0.40 |- k04_buttercup10419 skolemFOFtoCNF_X15 % 0.18/0.40 |- ~b48_buttercup10228 $X14 \/ k04_buttercup10419 $X14 % 0.18/0.40 |- ~b48_buttercup10222 skolemFOFtoCNF_X17 % 0.18/0.40 |- ~k04_buttercup10419 skolemFOFtoCNF_X18 % 0.18/0.40 |- b48_buttercup10222 skolemFOFtoCNF_X16 % 0.18/0.40 |- b48_buttercup10222 skolemFOFtoCNF_X18 % 0.18/0.40 |- k04_buttercup10419 skolemFOFtoCNF_X16 % 0.18/0.40 |- k04_buttercup10419 skolemFOFtoCNF_X17 % 0.18/0.40 |- ~k04_buttercup10516 skolemFOFtoCNF_X20 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X20 % 0.18/0.40 |- ~k04_buttercup10516 $X19 \/ b48_buttercup10417 $X19 % 0.18/0.40 |- ~b48_buttercup10229 skolemFOFtoCNF_X22 % 0.18/0.40 |- k04_buttercup10225 skolemFOFtoCNF_X22 % 0.18/0.40 |- ~b48_buttercup10229 $X21 \/ k04_buttercup10225 $X21 % 0.18/0.40 |- ~b48_buttercup10515 skolemFOFtoCNF_X24 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X24 % 0.18/0.40 |- ~b48_buttercup10515 $X23 \/ k04_buttercup10516 $X23 % 0.18/0.40 |- ~k04_buttercup10225 skolemFOFtoCNF_X26 % 0.18/0.40 |- b48_buttercup10222 skolemFOFtoCNF_X26 % 0.18/0.40 |- ~k04_buttercup10225 $X25 \/ b48_buttercup10222 $X25 % 0.18/0.40 |- ~b48_buttercup10421 skolemFOFtoCNF_X27 \/ % 0.18/0.40 ~k04_buttercup10419 skolemFOFtoCNF_X27 % 0.18/0.40 |- b48_buttercup10421 skolemFOFtoCNF_X27 \/ % 0.18/0.40 k04_buttercup10419 skolemFOFtoCNF_X27 % 0.18/0.40 |- ~b48_buttercup10421 $X28 \/ k04_buttercup10517 $X28 % 0.18/0.40 |- ~k04_buttercup10517 $X28 \/ b48_buttercup10421 $X28 % 0.18/0.40 |- ~b48_buttercup10417 skolemFOFtoCNF_X30 % 0.18/0.40 |- ~k04_buttercup10419 skolemFOFtoCNF_X31 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X29 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X31 % 0.18/0.40 |- k04_buttercup10419 skolemFOFtoCNF_X29 % 0.18/0.40 |- k04_buttercup10419 skolemFOFtoCNF_X30 % 0.18/0.40 |- k04_buttercup10225 skolemFOFtoCNF_X32 % 0.18/0.40 |- k04_buttercup10517 skolemFOFtoCNF_X33 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X34 % 0.18/0.40 |- k04_buttercup10419 skolemFOFtoCNF_X35 % 0.18/0.40 |- b48_buttercup10521 skolemFOFtoCNF_X36 % 0.18/0.40 |- b48_buttercup10422 skolemFOFtoCNF_X37 % 0.18/0.40 |- b48_buttercup10421 skolemFOFtoCNF_X38 % 0.18/0.40 |- b48_buttercup10227 skolemFOFtoCNF_X39 % 0.18/0.40 |- b48_buttercup10229 skolemFOFtoCNF_X40 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X41 % 0.18/0.40 |- b48_buttercup10222 skolemFOFtoCNF_X42 % 0.18/0.40 |- b48_buttercup10515 skolemFOFtoCNF_X43 % 0.18/0.40 |- b48_buttercup10228 skolemFOFtoCNF_X44 % 0.18/0.40 |- b48_buttercup10519 skolemFOFtoCNF_X45 % 0.18/0.40 |- b48_buttercup10518 skolemFOFtoCNF_X46 % 0.18/0.40 |- b48_buttercup10520 skolemFOFtoCNF_X47 % 0.18/0.40 |- ~k04_buttercup10225 $X50 \/ ~k04_buttercup10225 skolemFOFtoCNF_X49 \/ % 0.18/0.40 b48_buttercup10519 $X50 % 0.18/0.40 |- ~k04_buttercup10225 $X50 \/ b48_buttercup10519 $X50 \/ % 0.18/0.40 b48_buttercup10519 skolemFOFtoCNF_X49 % 0.18/0.40 |- ~b48_buttercup10519 skolemFOFtoCNF_X48 \/ % 0.18/0.40 ~k04_buttercup10225 skolemFOFtoCNF_X48 % 0.18/0.40 |- b48_buttercup10519 skolemFOFtoCNF_X54 % 0.18/0.40 |- k04_buttercup10225 skolemFOFtoCNF_X54 % 0.18/0.40 |- ~k04_buttercup10225 skolemFOFtoCNF_X49 \/ % 0.18/0.40 b48_buttercup10519 skolemFOFtoCNF_X49 % 0.18/0.40 |- k04_buttercup10419 skolemFOFtoCNF_X44 % 0.18/0.40 |- b48_buttercup10515 skolemFOFtoCNF_X36 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X24 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X34 % 0.18/0.40 |- k04_buttercup10517 skolemFOFtoCNF_X38 % 0.18/0.40 |- b48_buttercup10515 skolemFOFtoCNF_X46 % 0.18/0.40 |- b48_buttercup10515 skolemFOFtoCNF_X47 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X38 % 0.18/0.40 |- b48_buttercup10222 skolemFOFtoCNF_X40 % 0.18/0.40 |- k04_buttercup10419 skolemFOFtoCNF_X37 % 0.18/0.40 |- k04_buttercup10225 skolemFOFtoCNF_X40 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X36 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X43 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X46 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X47 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X46 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X36 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X43 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X47 % 0.18/0.40 |- b48_buttercup10222 skolemFOFtoCNF_X13 % 0.18/0.40 |- b48_buttercup10222 skolemFOFtoCNF_X22 % 0.18/0.40 |- b48_buttercup10222 skolemFOFtoCNF_X32 % 0.18/0.40 |- b48_buttercup10222 skolemFOFtoCNF_X54 % 0.18/0.40 |- b48_buttercup10421 skolemFOFtoCNF_X33 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X33 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X33 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X38 % 0.18/0.40 |- b48_buttercup10515 skolemFOFtoCNF_X45 % 0.18/0.40 |- b48_buttercup10515 skolemFOFtoCNF_X54 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X45 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X45 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X54 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X54 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X37 % 0.18/0.40 |- b48_buttercup10222 skolemFOFtoCNF_X39 % 0.18/0.40 |- b48_buttercup10222 skolemFOFtoCNF_X44 % 0.18/0.40 |- k04_buttercup10225 skolemFOFtoCNF_X39 % 0.18/0.40 |- ~b48_buttercup10519 $_23 \/ ~k04_buttercup10225 $_22 \/ % 0.18/0.40 b48_buttercup10519 $_22 \/ k04_buttercup10225 $_23 % 0.18/0.40 |- b48_buttercup10519 skolemFOFtoCNF_X32 % 0.18/0.40 |- b48_buttercup10515 skolemFOFtoCNF_X32 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X32 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X32 % 0.18/0.40 |- b48_buttercup10519 skolemFOFtoCNF_X39 % 0.18/0.40 |- b48_buttercup10515 skolemFOFtoCNF_X39 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X39 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X39 % 0.18/0.40 |- b48_buttercup10519 skolemFOFtoCNF_X40 % 0.18/0.40 |- b48_buttercup10515 skolemFOFtoCNF_X40 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X40 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X40 % 0.18/0.40 |- b48_buttercup10519 skolemFOFtoCNF_X48 % 0.18/0.40 |- b48_buttercup10515 skolemFOFtoCNF_X48 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X48 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X48 % 0.18/0.40 |- b48_buttercup10519 skolemFOFtoCNF_X22 % 0.18/0.40 |- b48_buttercup10515 skolemFOFtoCNF_X22 % 0.18/0.40 |- k04_buttercup10516 skolemFOFtoCNF_X22 % 0.18/0.40 |- b48_buttercup10417 skolemFOFtoCNF_X22 % 0.18/0.40 |- b48_buttercup10519 skolemFOFtoCNF_X13 % 0.18/0.41 |- b48_buttercup10515 skolemFOFtoCNF_X13 % 0.18/0.41 |- k04_buttercup10516 skolemFOFtoCNF_X13 % 0.18/0.41 |- b48_buttercup10417 skolemFOFtoCNF_X13 % 0.18/0.41 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.41 %------------------------------------------------------------------------------