%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN525+1 : TPTP v8.1.0. Released v2.1.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 : Thu Jul 21 09:03:39 EDT 2022 % Result : CounterSatisfiable 0.18s 0.45s % Output : Saturation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SYN525+1 : TPTP v8.1.0. Released v2.1.0. % 0.07/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n019.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 : Mon Jul 11 21:24:53 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.18/0.45 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.45 % 0.18/0.45 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.45 |- ~c2_0 % 0.18/0.45 |- ~c1_1 a195 \/ ~definitionFOFtoCNF_0 % 0.18/0.45 |- ~c2_1 a195 \/ ~definitionFOFtoCNF_0 % 0.18/0.45 |- ~definitionFOFtoCNF_0 \/ ndr1_0 % 0.18/0.45 |- c4_1 a196 \/ definitionFOFtoCNF_0 % 0.18/0.45 |- definitionFOFtoCNF_0 \/ ndr1_0 % 0.18/0.45 |- ~ndr1_1 a196 \/ c1_2 a196 $Y \/ c5_2 a196 $Y \/ definitionFOFtoCNF_0 % 0.18/0.45 |- ~c1_2 a196 $X \/ ~c3_2 a196 $X \/ ~c4_2 a196 $X \/ ~ndr1_1 a196 \/ % 0.18/0.45 definitionFOFtoCNF_0 % 0.18/0.45 |- ~ndr1_1 a195 \/ c1_2 a195 $W \/ c2_2 a195 $W \/ c3_2 a195 $W \/ % 0.18/0.45 c4_1 a196 % 0.18/0.45 |- ~ndr1_1 a195 \/ c1_2 a195 $W \/ c2_2 a195 $W \/ c3_2 a195 $W \/ ndr1_0 % 0.18/0.45 |- ~ndr1_1 a195 \/ ~ndr1_1 a196 \/ c1_2 a195 $W \/ c1_2 a196 $Y \/ % 0.18/0.45 c2_2 a195 $W \/ c3_2 a195 $W \/ c5_2 a196 $Y % 0.18/0.45 |- ~c1_2 a196 $X \/ ~c3_2 a196 $X \/ ~c4_2 a196 $X \/ ~ndr1_1 a195 \/ % 0.18/0.45 ~ndr1_1 a196 \/ c1_2 a195 $W \/ c2_2 a195 $W \/ c3_2 a195 $W % 0.18/0.45 |- ~c4_2 $X15 a217 \/ ~c5_2 $X15 $X16 \/ ~ndr1_0 \/ ~ndr1_1 $X15 \/ % 0.18/0.45 ~ndr1_1 $X17 \/ c1_1 $X17 \/ c1_2 $X15 $X16 \/ c1_2 $X17 $X18 \/ % 0.18/0.45 c2_2 $X15 $X16 \/ c4_1 $X15 \/ c4_2 $X17 $X18 \/ c5_2 $X17 $X18 % 0.18/0.45 |- ~c5_2 $X15 $X16 \/ ~ndr1_0 \/ ~ndr1_1 $X15 \/ ~ndr1_1 $X17 \/ % 0.18/0.45 c1_1 $X17 \/ c1_2 $X15 $X16 \/ c1_2 $X15 a217 \/ c1_2 $X17 $X18 \/ % 0.18/0.45 c2_2 $X15 $X16 \/ c4_1 $X15 \/ c4_2 $X17 $X18 \/ c5_2 $X17 $X18 % 0.18/0.45 |- ~c5_2 $X15 $X16 \/ ~ndr1_0 \/ ~ndr1_1 $X15 \/ ~ndr1_1 $X17 \/ % 0.18/0.45 c1_1 $X17 \/ c1_2 $X15 $X16 \/ c1_2 $X17 $X18 \/ c2_2 $X15 $X16 \/ % 0.18/0.45 c4_1 $X15 \/ c4_2 $X17 $X18 \/ c5_2 $X15 a217 \/ c5_2 $X17 $X18 % 0.18/0.45 |- ~c2_1 a190 \/ ~definitionFOFtoCNF_1 % 0.18/0.45 |- ~definitionFOFtoCNF_1 \/ c4_1 a190 % 0.18/0.45 |- ~definitionFOFtoCNF_1 \/ ndr1_0 % 0.18/0.45 |- ~definitionFOFtoCNF_1 \/ ~ndr1_1 a190 \/ c3_2 a190 $V \/ c5_2 a190 $V % 0.18/0.45 |- ~c3_2 a190 skolemFOFtoCNF_V \/ ~c4_1 a190 \/ ~ndr1_0 \/ c2_1 a190 \/ % 0.18/0.45 definitionFOFtoCNF_1 % 0.18/0.45 |- ~c4_1 a190 \/ ~c5_2 a190 skolemFOFtoCNF_V \/ ~ndr1_0 \/ c2_1 a190 \/ % 0.18/0.45 definitionFOFtoCNF_1 % 0.18/0.45 |- ~c4_1 a190 \/ ~ndr1_0 \/ c2_1 a190 \/ definitionFOFtoCNF_1 \/ % 0.18/0.45 ndr1_1 a190 % 0.18/0.45 |- ~c4_0 \/ ~c4_2 a188 a189 \/ definitionFOFtoCNF_1 % 0.18/0.45 |- ~c4_0 \/ c3_1 a188 \/ definitionFOFtoCNF_1 % 0.18/0.45 |- ~c4_0 \/ c3_2 a188 a189 \/ definitionFOFtoCNF_1 % 0.18/0.45 |- ~c4_0 \/ c5_2 a188 a189 \/ definitionFOFtoCNF_1 % 0.18/0.45 |- ~c4_0 \/ definitionFOFtoCNF_1 \/ ndr1_0 % 0.18/0.45 |- ~c4_0 \/ definitionFOFtoCNF_1 \/ ndr1_1 a188 % 0.18/0.45 |- ~c3_2 a188 $U \/ ~c4_0 \/ ~c4_2 a188 $U \/ ~ndr1_1 a188 \/ % 0.18/0.45 c1_2 a188 $U \/ definitionFOFtoCNF_1 % 0.18/0.45 |- ~definitionFOFtoCNF_2 $Z \/ c1_2 $Z a197 % 0.18/0.45 |- ~definitionFOFtoCNF_2 $Z \/ c4_2 $Z a197 % 0.18/0.45 |- ~definitionFOFtoCNF_2 $Z \/ ndr1_1 $Z % 0.18/0.45 |- ~c1_2 $Z a197 \/ ~c4_2 $Z a197 \/ ~ndr1_1 $Z \/ definitionFOFtoCNF_2 $Z % 0.18/0.45 |- ~c1_1 $X1 \/ ~c2_2 $Z a198 \/ ~c4_0 \/ ~c5_1 $X1 \/ ~ndr1_0 \/ % 0.18/0.45 c3_1 $Z \/ definitionFOFtoCNF_2 $Z % 0.18/0.45 |- ~c1_1 $X1 \/ ~c3_2 $Z a198 \/ ~c4_0 \/ ~c5_1 $X1 \/ ~ndr1_0 \/ % 0.18/0.45 c3_1 $Z \/ definitionFOFtoCNF_2 $Z % 0.18/0.45 |- ~c1_1 $X1 \/ ~c4_0 \/ ~c4_2 $Z a198 \/ ~c5_1 $X1 \/ ~ndr1_0 \/ % 0.18/0.45 c3_1 $Z \/ definitionFOFtoCNF_2 $Z % 0.18/0.45 |- ~c1_1 $X1 \/ ~c4_0 \/ ~c5_1 $X1 \/ ~ndr1_0 \/ c3_1 $Z \/ % 0.18/0.45 definitionFOFtoCNF_2 $Z \/ ndr1_1 $Z % 0.18/0.45 |- ~c3_1 $X12 \/ ~c3_2 $X13 $X14 \/ ~c4_0 \/ ~ndr1_0 \/ ~ndr1_1 $X13 \/ % 0.18/0.45 c1_1 $X12 \/ c2_1 $X13 \/ c3_1 $X13 \/ c4_2 $X13 $X14 % 0.18/0.45 |- ~c1_2 a206 a208 \/ ~c5_0 % 0.18/0.45 |- ~c2_2 a206 a208 \/ ~c5_0 % 0.18/0.45 |- ~c4_2 a206 a207 \/ ~c5_0 % 0.18/0.45 |- ~c5_0 \/ c1_1 a206 % 0.18/0.45 |- ~c5_0 \/ c2_2 a206 a207 % 0.18/0.45 |- ~c5_0 \/ c3_2 a206 a208 % 0.18/0.45 |- ~c5_0 \/ ndr1_0 % 0.18/0.45 |- ~c5_0 \/ ndr1_1 a206 % 0.18/0.45 |- ~c3_1 a191 \/ ~definitionFOFtoCNF_3 % 0.18/0.45 |- ~definitionFOFtoCNF_3 \/ c2_1 a191 % 0.18/0.45 |- ~definitionFOFtoCNF_3 \/ c5_1 a191 % 0.18/0.45 |- ~definitionFOFtoCNF_3 \/ ndr1_0 % 0.18/0.45 |- ~c2_1 a191 \/ ~c5_1 a191 \/ ~ndr1_0 \/ c3_1 a191 \/ definitionFOFtoCNF_3 % 0.18/0.45 |- ~c1_2 a192 a193 \/ c1_0 \/ definitionFOFtoCNF_3 % 0.18/0.45 |- ~c4_2 a192 a193 \/ c1_0 \/ definitionFOFtoCNF_3 % 0.18/0.45 |- ~c5_1 a192 \/ c1_0 \/ definitionFOFtoCNF_3 % 0.18/0.45 |- c1_0 \/ c3_2 a192 a194 \/ definitionFOFtoCNF_3 % 0.18/0.45 |- c1_0 \/ c5_2 a192 a193 \/ definitionFOFtoCNF_3 % 0.18/0.45 |- c1_0 \/ c5_2 a192 a194 \/ definitionFOFtoCNF_3 % 0.18/0.45 |- c1_0 \/ definitionFOFtoCNF_3 \/ ndr1_0 % 0.18/0.45 |- c1_0 \/ definitionFOFtoCNF_3 \/ ndr1_1 a192 % 0.18/0.45 |- ~c3_1 a215 \/ ~definitionFOFtoCNF_4 % 0.18/0.45 |- ~c5_1 a215 \/ ~definitionFOFtoCNF_4 % 0.18/0.45 |- ~definitionFOFtoCNF_4 \/ ndr1_0 % 0.18/0.45 |- ~ndr1_0 \/ c3_1 a215 \/ c5_1 a215 \/ definitionFOFtoCNF_4 % 0.18/0.45 |- ~c4_1 a216 \/ c3_0 \/ definitionFOFtoCNF_4 % 0.18/0.45 |- c1_1 a216 \/ c3_0 \/ definitionFOFtoCNF_4 % 0.18/0.45 |- c2_1 a216 \/ c3_0 \/ definitionFOFtoCNF_4 % 0.18/0.45 |- c3_0 \/ definitionFOFtoCNF_4 \/ ndr1_0 % 0.18/0.45 |- ~c1_1 $X7 \/ ~c2_2 $X6 a205 \/ ~c3_1 $X7 \/ ~c4_1 $X6 \/ ~ndr1_0 \/ % 0.18/0.45 c2_1 $X6 \/ c2_1 $X7 \/ c3_0 % 0.18/0.45 |- ~c1_1 $X7 \/ ~c3_1 $X7 \/ ~c4_1 $X6 \/ ~c5_2 $X6 a205 \/ ~ndr1_0 \/ % 0.18/0.45 c2_1 $X6 \/ c2_1 $X7 \/ c3_0 % 0.18/0.45 |- ~c1_1 $X7 \/ ~c3_1 $X7 \/ ~c4_1 $X6 \/ ~ndr1_0 \/ c2_1 $X6 \/ % 0.18/0.45 c2_1 $X7 \/ c3_0 \/ c4_2 $X6 a205 % 0.18/0.45 |- ~c1_1 $X7 \/ ~c3_1 $X7 \/ ~c4_1 $X6 \/ ~ndr1_0 \/ c2_1 $X6 \/ % 0.18/0.45 c2_1 $X7 \/ c3_0 \/ ndr1_1 $X6 % 0.18/0.45 |- ~c2_1 a202 \/ ~definitionFOFtoCNF_5 % 0.18/0.45 |- ~c3_1 a202 \/ ~definitionFOFtoCNF_5 % 0.18/0.45 |- ~definitionFOFtoCNF_5 \/ ndr1_0 % 0.18/0.45 |- ~ndr1_0 \/ c2_1 a202 \/ c3_1 a202 \/ definitionFOFtoCNF_5 % 0.18/0.46 |- ~c3_2 a203 a204 \/ c4_0 \/ definitionFOFtoCNF_5 % 0.18/0.46 |- c2_1 a203 \/ c4_0 \/ definitionFOFtoCNF_5 % 0.18/0.46 |- c2_2 a203 a204 \/ c4_0 \/ definitionFOFtoCNF_5 % 0.18/0.46 |- c4_0 \/ c5_2 a203 a204 \/ definitionFOFtoCNF_5 % 0.18/0.46 |- c4_0 \/ definitionFOFtoCNF_5 \/ ndr1_0 % 0.18/0.46 |- c4_0 \/ definitionFOFtoCNF_5 \/ ndr1_1 a203 % 0.18/0.46 |- ~c4_2 a203 $X5 \/ ~ndr1_1 a203 \/ c4_0 \/ definitionFOFtoCNF_5 % 0.18/0.46 |- ~c5_1 a201 \/ ~definitionFOFtoCNF_6 % 0.18/0.46 |- ~definitionFOFtoCNF_6 \/ c2_1 a201 % 0.18/0.46 |- ~definitionFOFtoCNF_6 \/ ndr1_0 % 0.18/0.46 |- ~c2_1 a201 \/ ~ndr1_0 \/ c5_1 a201 \/ definitionFOFtoCNF_6 % 0.18/0.46 |- c3_1 a200 \/ c4_0 \/ definitionFOFtoCNF_6 % 0.18/0.46 |- c4_0 \/ definitionFOFtoCNF_6 \/ ndr1_0 % 0.18/0.46 |- ~c1_2 a200 $X3 \/ ~ndr1_1 a200 \/ c3_2 a200 $X3 \/ c4_0 \/ % 0.18/0.46 c5_2 a200 $X3 \/ definitionFOFtoCNF_6 % 0.18/0.46 |- ~c1_2 a201 $X4 \/ ~c2_2 a201 $X4 \/ ~ndr1_1 a201 \/ c3_1 a200 \/ c4_0 \/ % 0.18/0.46 c5_2 a201 $X4 % 0.18/0.46 |- ~c1_2 a201 $X4 \/ ~c2_2 a201 $X4 \/ ~ndr1_1 a201 \/ c4_0 \/ % 0.18/0.46 c5_2 a201 $X4 \/ ndr1_0 % 0.18/0.46 |- ~c2_2 a200 $X2 \/ ~ndr1_1 a200 \/ c1_2 a200 $X2 \/ c4_0 \/ % 0.18/0.46 c4_2 a200 $X2 \/ definitionFOFtoCNF_6 % 0.18/0.46 |- ~c1_2 a200 $X3 \/ ~c1_2 a201 $X4 \/ ~c2_2 a201 $X4 \/ ~ndr1_1 a200 \/ % 0.18/0.46 ~ndr1_1 a201 \/ c3_2 a200 $X3 \/ c4_0 \/ c5_2 a200 $X3 \/ c5_2 a201 $X4 % 0.18/0.46 |- ~c1_2 a201 $X4 \/ ~c2_2 a200 $X2 \/ ~c2_2 a201 $X4 \/ ~ndr1_1 a200 \/ % 0.18/0.46 ~ndr1_1 a201 \/ c1_2 a200 $X2 \/ c4_0 \/ c4_2 a200 $X2 \/ c5_2 a201 $X4 % 0.18/0.46 |- ~c1_2 a212 a213 \/ ~definitionFOFtoCNF_7 % 0.18/0.46 |- ~c2_1 a212 \/ ~definitionFOFtoCNF_7 % 0.18/0.46 |- ~c4_2 a212 a214 \/ ~definitionFOFtoCNF_7 % 0.18/0.46 |- ~definitionFOFtoCNF_7 \/ c1_2 a212 a214 % 0.18/0.46 |- ~definitionFOFtoCNF_7 \/ c3_2 a212 a213 % 0.18/0.46 |- ~definitionFOFtoCNF_7 \/ c4_2 a212 a213 % 0.18/0.46 |- ~definitionFOFtoCNF_7 \/ c5_2 a212 a214 % 0.18/0.46 |- ~definitionFOFtoCNF_7 \/ ndr1_0 % 0.18/0.46 |- ~definitionFOFtoCNF_7 \/ ndr1_1 a212 % 0.18/0.46 |- ~c1_2 a212 a214 \/ ~c3_2 a212 a213 \/ ~c4_2 a212 a213 \/ % 0.18/0.46 ~c5_2 a212 a214 \/ ~ndr1_0 \/ ~ndr1_1 a212 \/ c1_2 a212 a213 \/ % 0.18/0.46 c2_1 a212 \/ c4_2 a212 a214 \/ definitionFOFtoCNF_7 % 0.18/0.46 |- ~c3_2 a210 a211 \/ c5_0 \/ definitionFOFtoCNF_7 % 0.18/0.46 |- ~c5_2 a210 a211 \/ c5_0 \/ definitionFOFtoCNF_7 % 0.18/0.46 |- c1_1 a210 \/ c5_0 \/ definitionFOFtoCNF_7 % 0.18/0.46 |- c4_2 a210 a211 \/ c5_0 \/ definitionFOFtoCNF_7 % 0.18/0.46 |- c5_0 \/ definitionFOFtoCNF_7 \/ ndr1_0 % 0.18/0.46 |- c5_0 \/ definitionFOFtoCNF_7 \/ ndr1_1 a210 % 0.18/0.46 |- c1_1 a195 \/ c2_1 a195 \/ definitionFOFtoCNF_0 % 0.18/0.46 |- c3_1 a215 \/ c5_0 \/ c5_1 a215 \/ definitionFOFtoCNF_4 \/ % 0.18/0.46 definitionFOFtoCNF_7 % 0.18/0.46 |- c3_1 a215 \/ c4_0 \/ c5_1 a215 \/ definitionFOFtoCNF_4 \/ % 0.18/0.46 definitionFOFtoCNF_6 % 0.18/0.46 |- c3_1 a215 \/ c4_0 \/ c5_1 a215 \/ definitionFOFtoCNF_4 \/ % 0.18/0.46 definitionFOFtoCNF_5 % 0.18/0.46 |- c3_0 \/ c3_1 a215 \/ c5_1 a215 \/ definitionFOFtoCNF_4 % 0.18/0.46 |- c1_0 \/ c3_1 a215 \/ c5_1 a215 \/ definitionFOFtoCNF_3 \/ % 0.18/0.46 definitionFOFtoCNF_4 % 0.18/0.46 |- c3_1 a215 \/ c5_1 a215 \/ definitionFOFtoCNF_0 \/ definitionFOFtoCNF_4 % 0.18/0.46 |- c2_1 a202 \/ c3_1 a202 \/ c5_0 \/ definitionFOFtoCNF_5 \/ % 0.18/0.46 definitionFOFtoCNF_7 % 0.18/0.46 |- c2_1 a202 \/ c3_1 a202 \/ c4_0 \/ definitionFOFtoCNF_5 % 0.18/0.46 |- c2_1 a202 \/ c3_0 \/ c3_1 a202 \/ definitionFOFtoCNF_4 \/ % 0.18/0.46 definitionFOFtoCNF_5 % 0.18/0.46 |- c1_0 \/ c2_1 a202 \/ c3_1 a202 \/ definitionFOFtoCNF_3 \/ % 0.18/0.46 definitionFOFtoCNF_5 % 0.18/0.46 |- c2_1 a202 \/ c3_1 a202 \/ definitionFOFtoCNF_0 \/ definitionFOFtoCNF_5 % 0.18/0.46 |- c2_2 a210 $_14 \/ c3_2 a210 $_14 \/ c4_2 a210 $_14 \/ c5_0 \/ % 0.18/0.46 definitionFOFtoCNF_7 % 0.18/0.46 |- ~c1_2 a210 a197 \/ ~ndr1_1 a210 \/ c2_2 a210 a197 \/ c3_2 a210 a197 \/ % 0.18/0.46 c5_0 \/ definitionFOFtoCNF_2 a210 \/ definitionFOFtoCNF_7 % 0.18/0.46 |- ~c1_1 a215 \/ ~c4_0 \/ ~ndr1_0 \/ c1_0 \/ c3_1 $_18 \/ c3_1 a215 \/ % 0.18/0.46 definitionFOFtoCNF_2 $_18 \/ definitionFOFtoCNF_3 \/ % 0.18/0.46 definitionFOFtoCNF_4 \/ ndr1_1 $_18 % 0.18/0.46 |- ~c1_1 a215 \/ ~c4_0 \/ ~ndr1_0 \/ c3_1 $_18 \/ c3_1 a215 \/ c5_0 \/ % 0.18/0.46 definitionFOFtoCNF_2 $_18 \/ definitionFOFtoCNF_4 \/ % 0.18/0.46 definitionFOFtoCNF_7 \/ ndr1_1 $_18 % 0.18/0.46 |- ~c1_1 a215 \/ ~c4_0 \/ ~ndr1_0 \/ c3_1 $_18 \/ c3_1 a215 \/ % 0.18/0.46 definitionFOFtoCNF_0 \/ definitionFOFtoCNF_2 $_18 \/ % 0.18/0.46 definitionFOFtoCNF_4 \/ ndr1_1 $_18 % 0.18/0.46 |- ~c1_1 a215 \/ ~c4_0 \/ ~ndr1_0 \/ c3_0 \/ c3_1 $_18 \/ c3_1 a215 \/ % 0.18/0.46 definitionFOFtoCNF_2 $_18 \/ definitionFOFtoCNF_4 \/ ndr1_1 $_18 % 0.18/0.46 |- ~c1_1 $_23 \/ ~c4_0 \/ ~c5_1 $_23 \/ ~ndr1_0 \/ c2_2 a210 a198 \/ % 0.18/0.46 c3_1 a210 \/ c3_2 a210 a198 \/ c5_0 \/ definitionFOFtoCNF_2 a210 \/ % 0.18/0.46 definitionFOFtoCNF_7 % 0.18/0.46 |- ~c1_1 $_28 \/ ~c3_1 $_28 \/ ~ndr1_0 \/ c2_1 $_28 \/ c2_1 a196 \/ c3_0 \/ % 0.18/0.46 definitionFOFtoCNF_0 \/ ndr1_1 a196 % 0.18/0.46 |- ~c1_1 a200 \/ ~ndr1_0 \/ c2_1 a196 \/ c2_1 a200 \/ c3_0 \/ c4_0 \/ % 0.18/0.46 definitionFOFtoCNF_0 \/ definitionFOFtoCNF_6 \/ ndr1_1 a196 % 0.18/0.46 |- ~c1_1 a202 \/ ~ndr1_0 \/ c2_1 a196 \/ c2_1 a202 \/ c3_0 \/ % 0.18/0.46 definitionFOFtoCNF_0 \/ definitionFOFtoCNF_5 \/ ndr1_1 a196 % 0.18/0.46 |- ~c1_1 $_35 \/ ~c3_1 $_35 \/ ~ndr1_0 \/ c2_1 $_35 \/ c2_1 a196 \/ c3_0 \/ % 0.18/0.46 c4_2 a196 a205 \/ definitionFOFtoCNF_0 % 0.18/0.46 |- ~c1_1 a200 \/ ~ndr1_0 \/ c2_1 a196 \/ c2_1 a200 \/ c3_0 \/ c4_0 \/ % 0.18/0.46 c4_2 a196 a205 \/ definitionFOFtoCNF_0 \/ definitionFOFtoCNF_6 % 0.18/0.46 |- ~c1_1 a202 \/ ~ndr1_0 \/ c2_1 a196 \/ c2_1 a202 \/ c3_0 \/ % 0.18/0.46 c4_2 a196 a205 \/ definitionFOFtoCNF_0 \/ definitionFOFtoCNF_5 % 0.18/0.46 |- ~c1_1 a215 \/ ~c4_0 \/ ~ndr1_0 \/ c2_2 a210 a198 \/ c3_1 a210 \/ % 0.18/0.46 c3_1 a215 \/ c3_2 a210 a198 \/ c5_0 \/ definitionFOFtoCNF_2 a210 \/ % 0.18/0.46 definitionFOFtoCNF_4 \/ definitionFOFtoCNF_7 % 0.18/0.46 |- ~c3_1 $_51 \/ ~c4_0 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_51 \/ c2_1 a192 \/ % 0.18/0.46 c3_1 a192 \/ c4_2 a192 a194 \/ definitionFOFtoCNF_3 % 0.18/0.46 |- ~c4_0 \/ c1_0 \/ c1_1 a202 \/ c2_1 a192 \/ c2_1 a202 \/ c3_1 a192 \/ % 0.18/0.46 c4_2 a192 a194 \/ definitionFOFtoCNF_3 \/ definitionFOFtoCNF_5 % 0.18/0.46 |- c1_0 \/ c1_1 a192 \/ c1_2 a192 $_58 \/ c1_2 a192 a193 \/ % 0.18/0.46 c2_2 a192 a193 \/ c4_1 a192 \/ c4_2 a192 $_58 \/ c5_2 a192 $_58 \/ % 0.18/0.46 c5_2 a192 a217 \/ definitionFOFtoCNF_3 % 0.18/0.46 |- c1_0 \/ c1_1 a192 \/ c1_2 a192 a193 \/ c1_2 a192 a217 \/ % 0.18/0.46 c2_2 a192 a193 \/ c4_1 a192 \/ c4_2 a192 a217 \/ c5_2 a192 a217 \/ % 0.18/0.46 definitionFOFtoCNF_3 % 0.18/0.46 |- c1_0 \/ c1_1 a192 \/ c1_2 a192 $_61 \/ c1_2 a192 a194 \/ % 0.18/0.46 c2_2 a192 a194 \/ c4_1 a192 \/ c4_2 a192 $_61 \/ c5_2 a192 $_61 \/ % 0.18/0.46 c5_2 a192 a217 \/ definitionFOFtoCNF_3 % 0.18/0.46 |- c1_0 \/ c1_1 a192 \/ c1_2 a192 a194 \/ c1_2 a192 a217 \/ % 0.18/0.46 c2_2 a192 a194 \/ c4_1 a192 \/ c4_2 a192 a217 \/ c5_2 a192 a217 \/ % 0.18/0.46 definitionFOFtoCNF_3 % 0.18/0.46 |- ~ndr1_0 \/ ~ndr1_1 $_63 \/ c1_0 \/ c1_1 $_63 \/ c1_2 $_63 $_64 \/ % 0.18/0.46 c1_2 a192 a194 \/ c2_2 a192 a194 \/ c4_1 a192 \/ c4_2 $_63 $_64 \/ % 0.18/0.46 c5_2 $_63 $_64 \/ c5_2 a192 a217 \/ definitionFOFtoCNF_3 % 0.18/0.46 |- c1_0 \/ c1_1 a203 \/ c1_2 a192 a194 \/ c1_2 a203 $_66 \/ % 0.18/0.46 c2_2 a192 a194 \/ c4_0 \/ c4_1 a192 \/ c4_2 a203 $_66 \/ % 0.18/0.46 c5_2 a192 a217 \/ c5_2 a203 $_66 \/ definitionFOFtoCNF_3 \/ % 0.18/0.46 definitionFOFtoCNF_5 % 0.18/0.46 |- ~ndr1_0 \/ ~ndr1_1 $_70 \/ c1_0 \/ c1_1 $_70 \/ c1_2 $_70 $_71 \/ % 0.18/0.46 c1_2 a192 a193 \/ c2_2 a192 a193 \/ c4_1 a192 \/ c4_2 $_70 $_71 \/ % 0.18/0.46 c5_2 $_70 $_71 \/ c5_2 a192 a217 \/ definitionFOFtoCNF_3 % 0.18/0.46 |- c1_0 \/ c1_1 a203 \/ c1_2 a192 a193 \/ c1_2 a203 $_73 \/ % 0.18/0.46 c2_2 a192 a193 \/ c4_0 \/ c4_1 a192 \/ c4_2 a203 $_73 \/ % 0.18/0.46 c5_2 a192 a217 \/ c5_2 a203 $_73 \/ definitionFOFtoCNF_3 \/ % 0.18/0.46 definitionFOFtoCNF_5 % 0.18/0.46 |- ~c4_2 a192 a217 \/ ~ndr1_0 \/ ~ndr1_1 $_79 \/ ~ndr1_1 a192 \/ c1_0 \/ % 0.18/0.46 c1_1 $_79 \/ c1_2 $_79 $_80 \/ c1_2 a192 a193 \/ c2_2 a192 a193 \/ % 0.18/0.46 c4_1 a192 \/ c4_2 $_79 $_80 \/ c5_2 $_79 $_80 \/ definitionFOFtoCNF_3 % 0.18/0.46 |- ~c4_2 a192 a217 \/ ~ndr1_0 \/ ~ndr1_1 $_79 \/ ~ndr1_1 a192 \/ c1_0 \/ % 0.18/0.46 c1_1 $_79 \/ c1_2 $_79 $_80 \/ c1_2 a192 a194 \/ c2_2 a192 a194 \/ % 0.18/0.46 c4_1 a192 \/ c4_2 $_79 $_80 \/ c5_2 $_79 $_80 \/ definitionFOFtoCNF_3 % 0.18/0.46 |- c1_0 \/ c1_1 a192 \/ c1_2 a192 $_90 \/ c1_2 a192 a193 \/ % 0.18/0.46 c1_2 a192 a217 \/ c2_2 a192 a193 \/ c4_1 a192 \/ c4_2 a192 $_90 \/ % 0.18/0.46 c5_2 a192 $_90 \/ definitionFOFtoCNF_3 % 0.18/0.46 |- c1_0 \/ c1_1 a192 \/ c1_2 a192 $_93 \/ c1_2 a192 a194 \/ % 0.18/0.46 c1_2 a192 a217 \/ c2_2 a192 a194 \/ c4_1 a192 \/ c4_2 a192 $_93 \/ % 0.18/0.46 c5_2 a192 $_93 \/ definitionFOFtoCNF_3 % 0.18/0.46 |- ~ndr1_0 \/ ~ndr1_1 $_95 \/ c1_0 \/ c1_1 $_95 \/ c1_2 $_95 $_96 \/ % 0.18/0.46 c1_2 a192 a193 \/ c1_2 a192 a217 \/ c2_2 a192 a193 \/ c4_1 a192 \/ % 0.18/0.46 c4_2 $_95 $_96 \/ c5_2 $_95 $_96 \/ definitionFOFtoCNF_3 % 0.18/0.46 |- c1_0 \/ c1_1 a203 \/ c1_2 a192 a193 \/ c1_2 a192 a217 \/ % 0.18/0.46 c1_2 a203 $_98 \/ c2_2 a192 a193 \/ c4_0 \/ c4_1 a192 \/ % 0.18/0.46 c4_2 a203 $_98 \/ c5_2 a203 $_98 \/ definitionFOFtoCNF_3 \/ % 0.18/0.46 definitionFOFtoCNF_5 % 0.18/0.46 |- ~ndr1_0 \/ ~ndr1_1 $_102 \/ c1_0 \/ c1_1 $_102 \/ c1_2 $_102 $_103 \/ % 0.18/0.46 c1_2 a192 a194 \/ c1_2 a192 a217 \/ c2_2 a192 a194 \/ c4_1 a192 \/ % 0.18/0.46 c4_2 $_102 $_103 \/ c5_2 $_102 $_103 \/ definitionFOFtoCNF_3 % 0.18/0.46 |- c1_0 \/ c1_1 a203 \/ c1_2 a192 a194 \/ c1_2 a192 a217 \/ % 0.18/0.46 c1_2 a203 $_105 \/ c2_2 a192 a194 \/ c4_0 \/ c4_1 a192 \/ % 0.18/0.46 c4_2 a203 $_105 \/ c5_2 a203 $_105 \/ definitionFOFtoCNF_3 \/ % 0.18/0.46 definitionFOFtoCNF_5 % 0.18/0.46 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.46 %------------------------------------------------------------------------------