%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : GRA013+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n021.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 : Sat Jul 16 07:19:51 EDT 2022 % Result : CounterSatisfiable 0.13s 0.39s % Output : Saturation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : GRA013+1 : TPTP v8.1.0. Released v3.2.0. % 0.07/0.12 % Command : metis --show proof --show saturation %s % 0.13/0.33 % Computer : n021.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Mon May 30 22:41:29 EDT 2022 % 0.13/0.33 % CPUTime : % 0.13/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.13/0.39 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.39 % 0.13/0.39 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.39 |- ~red $A $B \/ ~red $A $C \/ ~red $B $C % 0.13/0.39 |- ~green $A $B \/ ~green $A $C \/ ~green $B $C % 0.13/0.39 |- n1 < n2 % 0.13/0.39 |- n2 < n3 % 0.13/0.39 |- n3 < n4 % 0.13/0.39 |- n4 < n5 % 0.13/0.39 |- ~($A < $B) \/ ~($B < $C) \/ $A < $C % 0.13/0.39 |- ~($A < $B) \/ green $A $B \/ red $A $B % 0.13/0.39 |- ~red $C $C % 0.13/0.39 |- ~green $C $C % 0.13/0.39 |- ~goal % 0.13/0.39 |- green n1 n2 \/ red n1 n2 % 0.13/0.39 |- green n2 n3 \/ red n2 n3 % 0.13/0.39 |- green n3 n4 \/ red n3 n4 % 0.13/0.39 |- green n4 n5 \/ red n4 n5 % 0.13/0.39 |- ~($_4 < n1) \/ $_4 < n2 % 0.13/0.39 |- ~($_4 < n2) \/ $_4 < n3 % 0.13/0.39 |- ~($_4 < n3) \/ $_4 < n4 % 0.13/0.39 |- ~($_4 < n4) \/ $_4 < n5 % 0.13/0.39 |- n1 < n3 % 0.13/0.39 |- ~($A < n1) \/ $A < n3 % 0.13/0.39 |- green n1 n3 \/ red n1 n3 % 0.13/0.39 |- n1 < n4 % 0.13/0.39 |- n2 < n4 % 0.13/0.39 |- ~($A < n1) \/ $A < n4 % 0.13/0.39 |- green n1 n4 \/ red n1 n4 % 0.13/0.39 |- ~($A < n2) \/ $A < n4 % 0.13/0.39 |- green n2 n4 \/ red n2 n4 % 0.13/0.39 |- n1 < n5 % 0.13/0.39 |- n2 < n5 % 0.13/0.39 |- n3 < n5 % 0.13/0.39 |- ~($A < n1) \/ $A < n5 % 0.13/0.39 |- green n1 n5 \/ red n1 n5 % 0.13/0.39 |- ~($A < n2) \/ $A < n5 % 0.13/0.39 |- green n2 n5 \/ red n2 n5 % 0.13/0.39 |- ~($A < n3) \/ $A < n5 % 0.13/0.39 |- green n3 n5 \/ red n3 n5 % 0.13/0.39 |- ~red $_18 n2 \/ ~red n1 $_18 \/ green n1 n2 % 0.13/0.39 |- ~red $_18 n3 \/ ~red n1 $_18 \/ green n1 n3 % 0.13/0.39 |- ~red $_18 n4 \/ ~red n1 $_18 \/ green n1 n4 % 0.13/0.39 |- ~red $_18 n5 \/ ~red n1 $_18 \/ green n1 n5 % 0.13/0.39 |- ~red $_18 n3 \/ ~red n2 $_18 \/ green n2 n3 % 0.13/0.39 |- ~red $_18 n4 \/ ~red n2 $_18 \/ green n2 n4 % 0.13/0.40 |- ~red $_18 n5 \/ ~red n2 $_18 \/ green n2 n5 % 0.13/0.40 |- ~red $_18 n4 \/ ~red n3 $_18 \/ green n3 n4 % 0.13/0.40 |- ~red $_18 n5 \/ ~red n3 $_18 \/ green n3 n5 % 0.13/0.40 |- ~red $_18 n5 \/ ~red n4 $_18 \/ green n4 n5 % 0.13/0.40 |- ~red $_17 n1 \/ ~red $_17 n2 \/ green n1 n2 % 0.13/0.40 |- ~red $_17 n1 \/ ~red $_17 n3 \/ green n1 n3 % 0.13/0.40 |- ~red $_17 n1 \/ ~red $_17 n4 \/ green n1 n4 % 0.13/0.40 |- ~red $_17 n1 \/ ~red $_17 n5 \/ green n1 n5 % 0.13/0.40 |- ~red $_17 n2 \/ ~red $_17 n3 \/ green n2 n3 % 0.19/0.40 |- ~red $_17 n2 \/ ~red $_17 n4 \/ green n2 n4 % 0.19/0.40 |- ~red $_17 n2 \/ ~red $_17 n5 \/ green n2 n5 % 0.19/0.40 |- ~red $_17 n3 \/ ~red $_17 n4 \/ green n3 n4 % 0.19/0.40 |- ~red $_17 n3 \/ ~red $_17 n5 \/ green n3 n5 % 0.19/0.40 |- ~red $_17 n4 \/ ~red $_17 n5 \/ green n4 n5 % 0.19/0.40 |- ~red n3 n4 \/ green n3 n5 \/ green n4 n5 % 0.19/0.40 |- green n3 n4 \/ green n3 n5 \/ green n4 n5 % 0.19/0.40 |- ~red n1 n2 \/ green n1 n4 \/ green n2 n4 % 0.19/0.40 |- ~red n3 n2 \/ green n2 n4 \/ green n3 n4 % 0.19/0.40 |- green n1 n2 \/ green n1 n4 \/ green n2 n4 % 0.19/0.40 |- ~red n2 n3 \/ green n2 n5 \/ green n3 n5 % 0.19/0.40 |- ~red n2 n4 \/ green n2 n5 \/ green n4 n5 % 0.19/0.40 |- green n2 n4 \/ green n2 n5 \/ green n4 n5 % 0.19/0.40 |- green n2 n3 \/ green n2 n5 \/ green n3 n5 % 0.19/0.40 |- ~red n1 n4 \/ green n1 n5 \/ green n4 n5 % 0.19/0.40 |- green n1 n4 \/ green n1 n5 \/ green n4 n5 % 0.19/0.40 |- ~red n2 n3 \/ green n2 n4 \/ green n3 n4 % 0.19/0.40 |- green n2 n3 \/ green n2 n4 \/ green n3 n4 % 0.19/0.40 |- ~red n1 n2 \/ green n1 n5 \/ green n2 n5 % 0.19/0.40 |- ~red n3 n2 \/ green n2 n5 \/ green n3 n5 % 0.19/0.40 |- ~red n4 n2 \/ green n2 n5 \/ green n4 n5 % 0.19/0.40 |- green n1 n2 \/ green n1 n5 \/ green n2 n5 % 0.19/0.40 |- ~red n1 n3 \/ green n1 n5 \/ green n3 n5 % 0.19/0.40 |- ~red n4 n3 \/ green n3 n5 \/ green n4 n5 % 0.19/0.40 |- green n1 n3 \/ green n1 n5 \/ green n3 n5 % 0.19/0.40 |- ~red n1 n3 \/ green n1 n4 \/ green n3 n4 % 0.19/0.40 |- green n1 n3 \/ green n1 n4 \/ green n3 n4 % 0.19/0.40 |- ~red n1 n2 \/ green n1 n3 \/ green n2 n3 % 0.19/0.40 |- green n1 n2 \/ green n1 n3 \/ green n2 n3 % 0.19/0.40 |- ~red n2 n1 \/ green n1 n3 \/ green n2 n3 % 0.19/0.40 |- ~red n2 n1 \/ green n1 n4 \/ green n2 n4 % 0.19/0.40 |- ~red n3 n1 \/ green n1 n4 \/ green n3 n4 % 0.19/0.40 |- ~red n2 n1 \/ green n1 n5 \/ green n2 n5 % 0.19/0.40 |- ~red n3 n1 \/ green n1 n5 \/ green n3 n5 % 0.19/0.40 |- ~red n4 n1 \/ green n1 n5 \/ green n4 n5 % 0.19/0.40 |- ~green $_41 n3 \/ ~green n2 $_41 \/ green n1 n2 \/ green n1 n3 % 0.19/0.40 |- ~green $_41 n4 \/ ~green n2 $_41 \/ green n1 n2 \/ green n1 n4 % 0.19/0.40 |- ~green $_41 n5 \/ ~green n2 $_41 \/ green n1 n2 \/ green n1 n5 % 0.19/0.40 |- ~green $_41 n4 \/ ~green n3 $_41 \/ green n1 n3 \/ green n1 n4 % 0.19/0.40 |- ~green $_41 n4 \/ ~green n3 $_41 \/ green n2 n3 \/ green n2 n4 % 0.19/0.40 |- ~green $_41 n5 \/ ~green n3 $_41 \/ green n1 n3 \/ green n1 n5 % 0.19/0.40 |- ~green $_41 n5 \/ ~green n3 $_41 \/ green n2 n3 \/ green n2 n5 % 0.19/0.40 |- ~green $_41 n5 \/ ~green n4 $_41 \/ green n1 n4 \/ green n1 n5 % 0.19/0.40 |- ~green $_41 n5 \/ ~green n4 $_41 \/ green n2 n4 \/ green n2 n5 % 0.19/0.40 |- ~green $_41 n5 \/ ~green n4 $_41 \/ green n3 n4 \/ green n3 n5 % 0.19/0.40 |- ~green $_40 n2 \/ ~green $_40 n3 \/ green n1 n2 \/ green n1 n3 % 0.19/0.40 |- ~green $_40 n2 \/ ~green $_40 n4 \/ green n1 n2 \/ green n1 n4 % 0.19/0.40 |- ~green $_40 n2 \/ ~green $_40 n5 \/ green n1 n2 \/ green n1 n5 % 0.19/0.40 |- ~green $_40 n3 \/ ~green $_40 n4 \/ green n1 n3 \/ green n1 n4 % 0.19/0.40 |- ~green $_40 n3 \/ ~green $_40 n4 \/ green n2 n3 \/ green n2 n4 % 0.19/0.40 |- ~green $_40 n3 \/ ~green $_40 n5 \/ green n1 n3 \/ green n1 n5 % 0.19/0.40 |- ~green $_40 n3 \/ ~green $_40 n5 \/ green n2 n3 \/ green n2 n5 % 0.19/0.40 |- ~green $_40 n4 \/ ~green $_40 n5 \/ green n1 n4 \/ green n1 n5 % 0.19/0.40 |- ~green $_40 n4 \/ ~green $_40 n5 \/ green n2 n4 \/ green n2 n5 % 0.19/0.40 |- ~green $_40 n4 \/ ~green $_40 n5 \/ green n3 n4 \/ green n3 n5 % 0.19/0.40 |- ~green n3 n4 \/ green n1 n3 \/ green n1 n5 \/ green n2 n4 \/ green n2 n5 % 0.19/0.40 |- green n2 n3 \/ green n2 n4 \/ green n2 n5 % 0.19/0.40 |- ~green $A n2 \/ ~green $A n5 \/ green n2 n3 \/ green n2 n4 % 0.19/0.40 |- ~green $B n5 \/ ~green n2 $B \/ green n2 n3 \/ green n2 n4 % 0.19/0.40 |- ~green n2 n4 \/ green n1 n2 \/ green n1 n5 \/ green n3 n4 \/ green n3 n5 % 0.19/0.40 |- green n1 n2 \/ green n1 n3 \/ green n1 n4 % 0.19/0.40 |- ~green $A n1 \/ ~green $A n4 \/ green n1 n2 \/ green n1 n3 % 0.19/0.40 |- ~green $B n4 \/ ~green n1 $B \/ green n1 n2 \/ green n1 n3 % 0.19/0.40 |- green n1 n2 \/ green n1 n3 \/ green n1 n5 % 0.19/0.40 |- ~green $A n1 \/ ~green $A n5 \/ green n1 n2 \/ green n1 n3 % 0.19/0.40 |- ~green $B n5 \/ ~green n1 $B \/ green n1 n2 \/ green n1 n3 % 0.19/0.40 |- green n1 n2 \/ green n1 n4 \/ green n1 n5 % 0.19/0.40 |- ~green $A n1 \/ ~green $A n5 \/ green n1 n2 \/ green n1 n4 % 0.19/0.40 |- ~green $B n5 \/ ~green n1 $B \/ green n1 n2 \/ green n1 n4 % 0.19/0.40 |- green n1 n3 \/ green n1 n4 \/ green n1 n5 % 0.19/0.40 |- ~green $A n1 \/ ~green $A n5 \/ green n1 n3 \/ green n1 n4 % 0.19/0.40 |- ~green $B n5 \/ ~green n1 $B \/ green n1 n3 \/ green n1 n4 % 0.19/0.40 |- ~green n3 n4 \/ green n1 n4 \/ green n1 n5 \/ green n2 n3 \/ green n2 n5 % 0.19/0.40 |- ~green n4 n2 \/ green n1 n2 \/ green n1 n5 \/ green n3 n4 \/ green n3 n5 % 0.19/0.40 |- ~green n4 n3 \/ green n1 n3 \/ green n1 n5 \/ green n2 n4 \/ green n2 n5 % 0.19/0.40 |- ~green n1 n3 \/ green n1 n2 \/ green n1 n4 \/ green n2 n3 \/ green n2 n5 % 0.19/0.40 |- ~green n4 n3 \/ green n1 n4 \/ green n1 n5 \/ green n2 n3 \/ green n2 n5 % 0.19/0.40 |- ~green n2 n1 \/ green n1 n3 \/ green n1 n4 \/ green n2 n3 \/ green n2 n4 % 0.19/0.40 |- ~green n3 n1 \/ green n1 n3 \/ green n1 n4 \/ green n2 n3 \/ green n2 n5 % 0.19/0.40 |- ~green n4 n1 \/ green n1 n3 \/ green n1 n4 \/ green n2 n4 \/ green n2 n5 % 0.19/0.40 |- ~green n1 n2 \/ green n1 n3 \/ green n1 n4 \/ green n2 n3 \/ green n2 n4 % 0.19/0.40 |- green n1 n2 \/ green n1 n3 \/ green n3 n4 \/ green n3 n5 % 0.19/0.41 |- ~green $A n3 \/ ~green $A n5 \/ green n1 n2 \/ green n1 n3 \/ % 0.19/0.41 green n3 n4 % 0.19/0.41 |- ~green $B n5 \/ ~green n3 $B \/ green n1 n2 \/ green n1 n3 \/ % 0.19/0.41 green n3 n4 % 0.19/0.41 |- green n1 n2 \/ green n1 n3 \/ green n2 n4 \/ green n2 n5 % 0.19/0.41 |- ~green $A n2 \/ ~green $A n5 \/ green n1 n2 \/ green n1 n3 \/ % 0.19/0.41 green n2 n4 % 0.19/0.41 |- ~green $B n5 \/ ~green n2 $B \/ green n1 n2 \/ green n1 n3 \/ % 0.19/0.41 green n2 n4 % 0.19/0.41 |- ~green n3 n2 \/ green n1 n3 \/ green n1 n5 \/ green n2 n3 \/ green n2 n4 % 0.19/0.41 |- ~green n4 n2 \/ green n1 n4 \/ green n1 n5 \/ green n2 n3 \/ green n2 n4 % 0.19/0.41 |- ~green n3 n1 \/ green n1 n2 \/ green n1 n4 \/ green n2 n3 \/ green n2 n5 % 0.19/0.41 |- ~green n4 n1 \/ green n1 n2 \/ green n1 n4 \/ green n3 n4 \/ green n3 n5 % 0.19/0.41 |- ~green n2 n1 \/ green n1 n2 \/ green n1 n3 \/ green n2 n4 % 0.19/0.41 |- ~green n3 n1 \/ green n1 n2 \/ green n1 n3 \/ green n3 n4 % 0.19/0.41 |- green n1 n2 \/ green n1 n3 \/ green n2 n4 \/ green n3 n4 % 0.19/0.41 |- ~green $A n3 \/ ~green $A n4 \/ green n1 n2 \/ green n1 n3 \/ % 0.19/0.41 green n2 n4 % 0.19/0.41 |- ~green $B n4 \/ ~green n3 $B \/ green n1 n2 \/ green n1 n3 \/ % 0.19/0.41 green n2 n4 % 0.19/0.41 |- ~green n3 n1 \/ green n1 n2 \/ green n1 n3 \/ green n2 n4 % 0.19/0.41 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.41 %------------------------------------------------------------------------------