%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : KRS011-1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n019.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 : Sun Jul 17 03:18:25 EDT 2022 % Result : Satisfiable 0.19s 0.39s % Output : Saturation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS011-1 : TPTP v8.1.0. Released v2.0.0. % 0.03/0.13 % Command : metis --show proof --show saturation %s % 0.13/0.34 % Computer : n019.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 : 600 % 0.13/0.34 % DateTime : Tue Jun 7 07:51:25 EDT 2022 % 0.13/0.35 % CPUTime : % 0.13/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.19/0.39 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.39 % 0.19/0.39 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.39 |- ~r1 $X1 $X2 \/ r $X1 $X2 % 0.19/0.39 |- ~r2 $X1 $X2 \/ r $X1 $X2 % 0.19/0.39 |- ~r3 $X1 $X2 \/ r $X1 $X2 % 0.19/0.39 |- ~t1 $X1 $X2 \/ t $X1 $X2 % 0.19/0.39 |- ~t2 $X1 $X2 \/ t $X1 $X2 % 0.19/0.39 |- ~t3 $X1 $X2 \/ t $X1 $X2 % 0.19/0.39 |- ~c $X1 \/ ~e $X1 % 0.19/0.39 |- ~c $X1 \/ ~d $X1 % 0.19/0.39 |- ~d $X1 \/ ~e $X1 % 0.19/0.39 |- ~f1 $X1 \/ c (u9r5 $X1) % 0.19/0.39 |- ~f1 $X1 \/ t1 (u9r4 $X1) (u9r5 $X1) % 0.19/0.39 |- ~f1 $X1 \/ ~t (u9r4 $X1) $X3 \/ ~t (u9r4 $X1) $X4 \/ % 0.19/0.39 ~t (u9r4 $X1) $X5 \/ $X4 == $X3 \/ $X5 == $X3 \/ $X5 == $X4 % 0.19/0.39 |- ~f1 $X1 \/ r1 $X1 (u9r4 $X1) % 0.19/0.39 |- ~(u9r2 $X2 $X1 == u9r1 $X2 $X1) \/ ~c $X6 \/ ~r1 $X1 $X2 \/ % 0.19/0.39 ~t1 $X2 $X6 \/ f1 $X1 % 0.19/0.39 |- ~(u9r3 $X2 $X1 == u9r1 $X2 $X1) \/ ~c $X6 \/ ~r1 $X1 $X2 \/ % 0.19/0.39 ~t1 $X2 $X6 \/ f1 $X1 % 0.19/0.39 |- ~(u9r3 $X2 $X1 == u9r2 $X2 $X1) \/ ~c $X6 \/ ~r1 $X1 $X2 \/ % 0.19/0.39 ~t1 $X2 $X6 \/ f1 $X1 % 0.19/0.39 |- ~c $X6 \/ ~r1 $X1 $X2 \/ ~t1 $X2 $X6 \/ f1 $X1 \/ t $X2 (u9r1 $X2 $X1) % 0.19/0.39 |- ~c $X6 \/ ~r1 $X1 $X2 \/ ~t1 $X2 $X6 \/ f1 $X1 \/ t $X2 (u9r2 $X2 $X1) % 0.19/0.39 |- ~c $X6 \/ ~r1 $X1 $X2 \/ ~t1 $X2 $X6 \/ f1 $X1 \/ t $X2 (u9r3 $X2 $X1) % 0.19/0.39 |- ~f2 $X1 \/ d (u10r5 $X1) % 0.19/0.39 |- ~f2 $X1 \/ t2 (u10r4 $X1) (u10r5 $X1) % 0.19/0.39 |- ~f2 $X1 \/ ~t (u10r4 $X1) $X3 \/ ~t (u10r4 $X1) $X4 \/ % 0.19/0.39 ~t (u10r4 $X1) $X5 \/ $X4 == $X3 \/ $X5 == $X3 \/ $X5 == $X4 % 0.19/0.39 |- ~f2 $X1 \/ r2 $X1 (u10r4 $X1) % 0.19/0.39 |- ~(u10r2 $X2 $X1 == u10r1 $X2 $X1) \/ ~d $X6 \/ ~r2 $X1 $X2 \/ % 0.19/0.39 ~t2 $X2 $X6 \/ f2 $X1 % 0.19/0.39 |- ~(u10r3 $X2 $X1 == u10r1 $X2 $X1) \/ ~d $X6 \/ ~r2 $X1 $X2 \/ % 0.19/0.39 ~t2 $X2 $X6 \/ f2 $X1 % 0.19/0.39 |- ~(u10r3 $X2 $X1 == u10r2 $X2 $X1) \/ ~d $X6 \/ ~r2 $X1 $X2 \/ % 0.19/0.39 ~t2 $X2 $X6 \/ f2 $X1 % 0.19/0.39 |- ~d $X6 \/ ~r2 $X1 $X2 \/ ~t2 $X2 $X6 \/ f2 $X1 \/ t $X2 (u10r1 $X2 $X1) % 0.19/0.39 |- ~d $X6 \/ ~r2 $X1 $X2 \/ ~t2 $X2 $X6 \/ f2 $X1 \/ t $X2 (u10r2 $X2 $X1) % 0.19/0.39 |- ~d $X6 \/ ~r2 $X1 $X2 \/ ~t2 $X2 $X6 \/ f2 $X1 \/ t $X2 (u10r3 $X2 $X1) % 0.19/0.39 |- ~f3 $X1 \/ e (u11r5 $X1) % 0.19/0.39 |- ~f3 $X1 \/ t3 (u11r4 $X1) (u11r5 $X1) % 0.19/0.39 |- ~f3 $X1 \/ ~t (u11r4 $X1) $X3 \/ ~t (u11r4 $X1) $X4 \/ % 0.19/0.39 ~t (u11r4 $X1) $X5 \/ $X4 == $X3 \/ $X5 == $X3 \/ $X5 == $X4 % 0.19/0.39 |- ~f3 $X1 \/ r3 $X1 (u11r4 $X1) % 0.19/0.39 |- ~(u11r2 $X2 $X1 == u11r1 $X2 $X1) \/ ~e $X6 \/ ~r3 $X1 $X2 \/ % 0.19/0.39 ~t3 $X2 $X6 \/ f3 $X1 % 0.19/0.39 |- ~(u11r3 $X2 $X1 == u11r1 $X2 $X1) \/ ~e $X6 \/ ~r3 $X1 $X2 \/ % 0.19/0.39 ~t3 $X2 $X6 \/ f3 $X1 % 0.19/0.39 |- ~(u11r3 $X2 $X1 == u11r2 $X2 $X1) \/ ~e $X6 \/ ~r3 $X1 $X2 \/ % 0.19/0.39 ~t3 $X2 $X6 \/ f3 $X1 % 0.19/0.39 |- ~e $X6 \/ ~r3 $X1 $X2 \/ ~t3 $X2 $X6 \/ f3 $X1 \/ t $X2 (u11r1 $X2 $X1) % 0.19/0.39 |- ~e $X6 \/ ~r3 $X1 $X2 \/ ~t3 $X2 $X6 \/ f3 $X1 \/ t $X2 (u11r2 $X2 $X1) % 0.19/0.39 |- ~e $X6 \/ ~r3 $X1 $X2 \/ ~t3 $X2 $X6 \/ f3 $X1 \/ t $X2 (u11r3 $X2 $X1) % 0.19/0.39 |- ~f $X1 \/ f3 $X1 % 0.19/0.39 |- ~f $X1 \/ f2 $X1 % 0.19/0.39 |- ~f $X1 \/ f1 $X1 % 0.19/0.39 |- ~f1 $X1 \/ ~f2 $X1 \/ ~f3 $X1 \/ f $X1 % 0.19/0.39 |- ~g $X1 \/ r2least $X1 % 0.19/0.39 |- ~r2least $X1 \/ g $X1 % 0.19/0.39 |- ~(u14r2 $X1 == u14r1 $X1) \/ ~r2least $X1 % 0.19/0.39 |- ~r2least $X1 \/ r $X1 (u14r1 $X1) % 0.19/0.39 |- ~r2least $X1 \/ r $X1 (u14r2 $X1) % 0.19/0.39 |- ~r $X1 $X2 \/ ~r $X1 $X3 \/ $X3 == $X2 \/ r2least $X1 % 0.19/0.39 |- ~r $X1 $X3 \/ $X3 == $X3 \/ r2least $X1 % 0.19/0.39 |- ~f1 $X1 \/ ~t (u9r4 $X1) $X5 \/ $X5 == $X5 % 0.19/0.39 |- ~f2 $X1 \/ ~t (u10r4 $X1) $X5 \/ $X5 == $X5 % 0.19/0.39 |- ~f3 $X1 \/ ~t (u11r4 $X1) $X5 \/ $X5 == $X5 % 0.19/0.39 |- f exists % 0.19/0.39 |- ~g exists % 0.19/0.39 |- f2 exists % 0.19/0.39 |- f3 exists % 0.19/0.39 |- f1 exists % 0.19/0.39 |- c (u9r5 exists) % 0.19/0.39 |- d (u10r5 exists) % 0.19/0.39 |- ~c (u10r5 exists) % 0.19/0.39 |- e (u11r5 exists) % 0.19/0.39 |- ~d (u11r5 exists) % 0.19/0.39 |- ~c (u11r5 exists) % 0.19/0.39 |- r3 exists (u11r4 exists) % 0.19/0.39 |- r1 exists (u9r4 exists) % 0.19/0.39 |- r2 exists (u10r4 exists) % 0.19/0.39 |- t2 (u10r4 exists) (u10r5 exists) % 0.19/0.39 |- t1 (u9r4 exists) (u9r5 exists) % 0.19/0.39 |- t3 (u11r4 exists) (u11r5 exists) % 0.19/0.39 |- r exists (u9r4 exists) % 0.19/0.39 |- r exists (u10r4 exists) % 0.19/0.39 |- r exists (u11r4 exists) % 0.19/0.39 |- t (u9r4 exists) (u9r5 exists) % 0.19/0.39 |- t (u10r4 exists) (u10r5 exists) % 0.19/0.39 |- t (u11r4 exists) (u11r5 exists) % 0.19/0.39 |- u10r4 exists == u10r4 exists \/ r2least exists % 0.19/0.39 |- u11r4 exists == u11r4 exists \/ r2least exists % 0.19/0.39 |- u9r4 exists == u9r4 exists \/ r2least exists % 0.19/0.39 |- u9r5 exists == u9r5 exists % 0.19/0.39 |- u10r5 exists == u10r5 exists % 0.19/0.39 |- u11r5 exists == u11r5 exists % 0.19/0.39 |- ~r exists $_43 \/ $_43 == u10r4 exists \/ r2least exists % 0.19/0.39 |- ~r exists $_43 \/ $_43 == u11r4 exists \/ r2least exists % 0.19/0.39 |- ~r exists $_43 \/ $_43 == u9r4 exists \/ r2least exists % 0.19/0.39 |- ~r exists $_42 \/ u10r4 exists == $_42 \/ r2least exists % 0.19/0.39 |- ~r exists $_42 \/ u11r4 exists == $_42 \/ r2least exists % 0.19/0.39 |- ~r exists $_42 \/ u9r4 exists == $_42 \/ r2least exists % 0.19/0.39 |- u11r4 exists == u10r4 exists \/ r2least exists % 0.19/0.39 |- u9r4 exists == u10r4 exists \/ r2least exists % 0.19/0.39 |- u10r4 exists == u11r4 exists \/ r2least exists % 0.19/0.39 |- u9r4 exists == u11r4 exists \/ r2least exists % 0.19/0.39 |- u10r4 exists == u9r4 exists \/ r2least exists % 0.19/0.39 |- u11r4 exists == u9r4 exists \/ r2least exists % 0.19/0.39 |- ~r1 $_50 (u9r4 exists) \/ f1 $_50 \/ % 0.19/0.39 t (u9r4 exists) (u9r1 (u9r4 exists) $_50) % 0.19/0.39 |- ~r1 $_54 (u9r4 exists) \/ f1 $_54 \/ % 0.19/0.39 t (u9r4 exists) (u9r2 (u9r4 exists) $_54) % 0.19/0.39 |- ~r1 $_58 (u9r4 exists) \/ f1 $_58 \/ % 0.19/0.39 t (u9r4 exists) (u9r3 (u9r4 exists) $_58) % 0.19/0.39 |- ~r2 $_62 (u10r4 exists) \/ f2 $_62 \/ % 0.19/0.39 t (u10r4 exists) (u10r1 (u10r4 exists) $_62) % 0.19/0.39 |- ~r2 $_66 (u10r4 exists) \/ f2 $_66 \/ % 0.19/0.39 t (u10r4 exists) (u10r2 (u10r4 exists) $_66) % 0.19/0.39 |- ~r2 $_70 (u10r4 exists) \/ f2 $_70 \/ % 0.19/0.39 t (u10r4 exists) (u10r3 (u10r4 exists) $_70) % 0.19/0.39 |- ~r3 $_74 (u11r4 exists) \/ f3 $_74 \/ % 0.19/0.39 t (u11r4 exists) (u11r1 (u11r4 exists) $_74) % 0.19/0.39 |- ~r3 $_78 (u11r4 exists) \/ f3 $_78 \/ % 0.19/0.39 t (u11r4 exists) (u11r2 (u11r4 exists) $_78) % 0.19/0.39 |- ~r3 $_82 (u11r4 exists) \/ f3 $_82 \/ % 0.19/0.39 t (u11r4 exists) (u11r3 (u11r4 exists) $_82) % 0.19/0.39 |- ~t (u9r4 exists) $_115 \/ ~t (u9r4 exists) $_116 \/ % 0.19/0.39 $_115 == u9r5 exists \/ $_116 == $_115 \/ $_116 == u9r5 exists % 0.19/0.39 |- ~t (u9r4 exists) $_114 \/ ~t (u9r4 exists) $_116 \/ $_116 == $_114 \/ % 0.19/0.39 $_116 == u9r5 exists \/ u9r5 exists == $_114 % 0.19/0.39 |- ~t (u9r4 exists) $_114 \/ ~t (u9r4 exists) $_115 \/ $_115 == $_114 \/ % 0.19/0.39 u9r5 exists == $_114 \/ u9r5 exists == $_115 % 0.19/0.39 |- ~t (u9r4 exists) $_116 \/ $_116 == $_116 \/ $_116 == u9r5 exists % 0.19/0.40 |- ~t (u9r4 exists) $_115 \/ $_115 == $_115 \/ u9r5 exists == $_115 % 0.19/0.40 |- ~t (u10r4 exists) $_127 \/ ~t (u10r4 exists) $_128 \/ % 0.19/0.40 $_127 == u10r5 exists \/ $_128 == $_127 \/ $_128 == u10r5 exists % 0.19/0.40 |- ~t (u10r4 exists) $_126 \/ ~t (u10r4 exists) $_128 \/ $_128 == $_126 \/ % 0.19/0.40 $_128 == u10r5 exists \/ u10r5 exists == $_126 % 0.19/0.40 |- ~t (u10r4 exists) $_126 \/ ~t (u10r4 exists) $_127 \/ $_127 == $_126 \/ % 0.19/0.40 u10r5 exists == $_126 \/ u10r5 exists == $_127 % 0.19/0.40 |- ~t (u10r4 exists) $_128 \/ $_128 == $_128 \/ $_128 == u10r5 exists % 0.19/0.40 |- ~t (u10r4 exists) $_127 \/ $_127 == $_127 \/ u10r5 exists == $_127 % 0.19/0.40 |- ~t (u11r4 exists) $_139 \/ ~t (u11r4 exists) $_140 \/ % 0.19/0.40 $_139 == u11r5 exists \/ $_140 == $_139 \/ $_140 == u11r5 exists % 0.19/0.40 |- ~t (u11r4 exists) $_138 \/ ~t (u11r4 exists) $_140 \/ $_140 == $_138 \/ % 0.19/0.40 $_140 == u11r5 exists \/ u11r5 exists == $_138 % 0.19/0.40 |- ~t (u11r4 exists) $_138 \/ ~t (u11r4 exists) $_139 \/ $_139 == $_138 \/ % 0.19/0.40 u11r5 exists == $_138 \/ u11r5 exists == $_139 % 0.19/0.40 |- ~t (u11r4 exists) $_140 \/ $_140 == $_140 \/ $_140 == u11r5 exists % 0.19/0.40 |- ~t (u11r4 exists) $_139 \/ $_139 == $_139 \/ u11r5 exists == $_139 % 0.19/0.40 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.40 %------------------------------------------------------------------------------