%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : LCL675+1.001 : TPTP v9.3.1. Released v4.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 : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 12:43:15 PM UTC 2026 % Result : CounterSatisfiable 0.13s 0.37s % Output : Saturation 0.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL675+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : metis --show proof --show saturation %s % 0.09/0.34 % Computer : n019.cluster.edu % 0.09/0.34 % Model : x86_64 x86_64 % 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.34 % Memory : 8046.5625MB % 0.09/0.34 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Sat Sep 5 21:27:08 UTC 2026 % 0.09/0.35 % CPUTime : % 0.09/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.13/0.37 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.13/0.37 % 0.13/0.37 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.13/0.37 |- r1 $X $X % 0.13/0.37 |- ~r1 $X $Y \/ ~r1 $Y $Z \/ r1 $X $Z % 0.13/0.37 |- ~p101 skolemFOFtoCNF_X % 0.13/0.37 |- p100 skolemFOFtoCNF_X % 0.13/0.37 |- ~p101 $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ p100 $Y % 0.13/0.37 |- ~p102 $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ p101 $Y % 0.13/0.37 |- ~p100 $Y \/ ~p102 (skolemFOFtoCNF_X_1 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.13/0.37 p101 $Y % 0.13/0.37 |- ~p100 $Y \/ ~p102 (skolemFOFtoCNF_X_2 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.13/0.37 p101 $Y % 0.13/0.37 |- ~p100 $Y \/ ~p2 (skolemFOFtoCNF_X_2 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.13/0.37 p101 $Y % 0.13/0.37 |- ~p100 $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ p101 $Y \/ % 0.13/0.37 p101 (skolemFOFtoCNF_X_1 $Y) % 0.13/0.37 |- ~p100 $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ p101 $Y \/ % 0.13/0.37 p101 (skolemFOFtoCNF_X_2 $Y) % 0.13/0.37 |- ~p100 $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ p101 $Y \/ % 0.13/0.37 p2 (skolemFOFtoCNF_X_1 $Y) % 0.13/0.37 |- ~p100 $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ p101 $Y \/ % 0.13/0.37 r1 $Y (skolemFOFtoCNF_X_1 $Y) % 0.13/0.37 |- ~p100 $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ p101 $Y \/ % 0.13/0.37 r1 $Y (skolemFOFtoCNF_X_2 $Y) % 0.13/0.37 |- ~p1 $X \/ ~p100 $X \/ ~p100 $Y \/ ~r1 $Y $X \/ % 0.13/0.37 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y % 0.13/0.37 |- ~p1 $Y \/ ~p100 $X \/ ~p100 $Y \/ ~r1 $Y $X \/ % 0.13/0.37 ~r1 skolemFOFtoCNF_X $Y \/ p1 $X % 0.13/0.37 |- ~p101 $X \/ ~p101 $Y \/ ~p2 $X \/ ~r1 $Y $X \/ % 0.13/0.37 ~r1 skolemFOFtoCNF_X $Y \/ p2 $Y % 0.13/0.37 |- ~p101 $X \/ ~p101 $Y \/ ~p2 $Y \/ ~r1 $Y $X \/ % 0.13/0.37 ~r1 skolemFOFtoCNF_X $Y \/ p2 $X % 0.13/0.37 |- ~p102 skolemFOFtoCNF_X % 0.13/0.37 |- ~p102 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.13/0.37 |- ~p102 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.13/0.37 |- ~p2 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.13/0.37 |- p101 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.13/0.37 |- p101 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.13/0.37 |- p2 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.13/0.37 |- r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.13/0.37 |- p100 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.13/0.37 |- r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.13/0.37 |- p100 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.13/0.37 |- ~r1 $_11 skolemFOFtoCNF_X \/ % 0.13/0.37 r1 $_11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.13/0.37 |- ~r1 $_11 skolemFOFtoCNF_X \/ % 0.13/0.37 r1 $_11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.13/0.37 |- ~p1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ p1 skolemFOFtoCNF_X % 0.13/0.37 |- ~p1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ p1 skolemFOFtoCNF_X % 0.13/0.37 |- ~p1 $_16 \/ ~p100 $_16 \/ ~r1 skolemFOFtoCNF_X $_16 \/ % 0.13/0.37 p1 skolemFOFtoCNF_X % 0.13/0.37 |- ~p1 skolemFOFtoCNF_X \/ p1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.13/0.37 |- ~p1 skolemFOFtoCNF_X \/ p1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.13/0.37 |- ~p1 skolemFOFtoCNF_X \/ ~p100 $_19 \/ ~r1 skolemFOFtoCNF_X $_19 \/ % 0.13/0.37 p1 $_19 % 0.13/0.37 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.13/0.37 %------------------------------------------------------------------------------