%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN526+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n011.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.19s 0.43s % Output : Saturation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN526+1 : TPTP v8.1.0. Released v2.1.0. % 0.11/0.12 % Command : metis --show proof --show saturation %s % 0.13/0.33 % Computer : n011.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 : Tue Jul 12 08:39:43 EDT 2022 % 0.13/0.33 % CPUTime : % 0.13/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.19/0.43 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.43 % 0.19/0.43 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.43 |- ~c1_0 % 0.19/0.43 |- ~c2_0 % 0.19/0.43 |- ~c3_0 \/ c5_0 % 0.19/0.43 |- ~c3_2 $X18 a244 \/ ~c5_0 \/ ~c5_1 $X18 \/ ~c5_2 $X18 $X19 \/ ~ndr1_0 \/ % 0.19/0.43 ~ndr1_1 $X18 \/ c3_2 $X18 $X19 \/ c4_2 $X18 $X19 % 0.19/0.43 |- ~c5_0 \/ ~c5_1 $X18 \/ ~c5_2 $X18 $X19 \/ ~ndr1_0 \/ ~ndr1_1 $X18 \/ % 0.19/0.43 c2_2 $X18 a244 \/ c3_2 $X18 $X19 \/ c4_2 $X18 $X19 % 0.19/0.43 |- ~c5_0 \/ ~c5_1 $X18 \/ ~c5_2 $X18 $X19 \/ ~ndr1_0 \/ ~ndr1_1 $X18 \/ % 0.19/0.43 c3_2 $X18 $X19 \/ c4_2 $X18 $X19 \/ c5_2 $X18 a244 % 0.19/0.43 |- ~c1_2 a248 a249 \/ c3_0 % 0.19/0.43 |- c2_2 a248 a249 \/ c3_0 % 0.19/0.43 |- c3_0 \/ c3_1 a248 % 0.19/0.43 |- c3_0 \/ c4_2 a248 a249 % 0.19/0.43 |- c3_0 \/ ndr1_0 % 0.19/0.43 |- c3_0 \/ ndr1_1 a248 % 0.19/0.43 |- ~c1_2 $X25 $X26 \/ ~c2_1 $X25 \/ ~c3_1 $X24 \/ ~c4_2 $X25 $X26 \/ % 0.19/0.43 ~c5_2 $X24 a250 \/ ~c5_2 $X25 $X26 \/ ~ndr1_0 \/ ~ndr1_1 $X25 \/ % 0.19/0.43 c4_1 $X24 \/ c5_1 $X25 % 0.19/0.43 |- ~c1_2 $X25 $X26 \/ ~c2_1 $X25 \/ ~c3_1 $X24 \/ ~c4_2 $X25 $X26 \/ % 0.19/0.43 ~c5_2 $X25 $X26 \/ ~ndr1_0 \/ ~ndr1_1 $X25 \/ c4_1 $X24 \/ % 0.19/0.43 c4_2 $X24 a250 \/ c5_1 $X25 % 0.19/0.43 |- ~c1_2 $X25 $X26 \/ ~c2_1 $X25 \/ ~c3_1 $X24 \/ ~c4_2 $X25 $X26 \/ % 0.19/0.43 ~c5_2 $X25 $X26 \/ ~ndr1_0 \/ ~ndr1_1 $X25 \/ c4_1 $X24 \/ c5_1 $X25 \/ % 0.19/0.43 ndr1_1 $X24 % 0.19/0.43 |- ~c5_2 $X4 a227 \/ ~definitionFOFtoCNF_0 $X4 % 0.19/0.43 |- ~definitionFOFtoCNF_0 $X4 \/ c1_2 $X4 a227 % 0.19/0.43 |- ~definitionFOFtoCNF_0 $X4 \/ c4_2 $X4 a227 % 0.19/0.43 |- ~definitionFOFtoCNF_0 $X4 \/ ndr1_1 $X4 % 0.19/0.43 |- ~c1_2 $X4 a227 \/ ~c4_2 $X4 a227 \/ ~ndr1_1 $X4 \/ c5_2 $X4 a227 \/ % 0.19/0.43 definitionFOFtoCNF_0 $X4 % 0.19/0.43 |- ~c2_2 $X4 a228 \/ ~definitionFOFtoCNF_1 $X4 % 0.19/0.43 |- ~definitionFOFtoCNF_1 $X4 \/ c1_2 $X4 a228 % 0.19/0.43 |- ~definitionFOFtoCNF_1 $X4 \/ ndr1_1 $X4 % 0.19/0.43 |- ~c1_2 $X4 a228 \/ ~ndr1_1 $X4 \/ c2_2 $X4 a228 \/ % 0.19/0.43 definitionFOFtoCNF_1 $X4 % 0.19/0.43 |- ~c3_0 \/ ~c4_1 a229 \/ ~ndr1_0 \/ c5_1 $X4 \/ % 0.19/0.43 definitionFOFtoCNF_0 $X4 \/ definitionFOFtoCNF_1 $X4 % 0.19/0.43 |- ~c1_2 a229 $X6 \/ ~c3_0 \/ ~ndr1_0 \/ ~ndr1_1 a229 \/ c4_2 a229 $X6 \/ % 0.19/0.43 c5_1 $X4 \/ c5_2 a229 $X6 \/ definitionFOFtoCNF_0 $X4 \/ % 0.19/0.43 definitionFOFtoCNF_1 $X4 % 0.19/0.43 |- ~c3_0 \/ ~c3_2 a229 $X5 \/ ~c4_2 a229 $X5 \/ ~c5_2 a229 $X5 \/ % 0.19/0.43 ~ndr1_0 \/ ~ndr1_1 a229 \/ c5_1 $X4 \/ definitionFOFtoCNF_0 $X4 \/ % 0.19/0.43 definitionFOFtoCNF_1 $X4 % 0.19/0.43 |- ~c4_1 a236 \/ ~definitionFOFtoCNF_2 % 0.19/0.43 |- ~definitionFOFtoCNF_2 \/ c3_1 a236 % 0.19/0.43 |- ~definitionFOFtoCNF_2 \/ ndr1_0 % 0.19/0.43 |- ~c3_1 a236 \/ ~ndr1_0 \/ c4_1 a236 \/ definitionFOFtoCNF_2 % 0.19/0.43 |- ~c3_0 \/ c2_1 a237 \/ definitionFOFtoCNF_2 % 0.19/0.43 |- ~c3_0 \/ definitionFOFtoCNF_2 \/ ndr1_0 % 0.19/0.43 |- ~c3_0 \/ ~c5_2 a237 $X13 \/ ~ndr1_1 a237 \/ c4_2 a237 $X13 \/ % 0.19/0.43 definitionFOFtoCNF_2 % 0.19/0.43 |- ~c2_2 a237 $X14 \/ ~c3_0 \/ ~c3_2 a237 $X14 \/ ~ndr1_1 a237 \/ % 0.19/0.43 c5_2 a237 $X14 \/ definitionFOFtoCNF_2 % 0.19/0.43 |- ~c3_0 \/ ~c4_2 a236 $X12 \/ ~ndr1_1 a236 \/ c2_1 a237 \/ % 0.19/0.43 c3_2 a236 $X12 \/ c5_2 a236 $X12 % 0.19/0.43 |- ~c3_0 \/ ~c4_2 a236 $X12 \/ ~ndr1_1 a236 \/ c3_2 a236 $X12 \/ % 0.19/0.43 c5_2 a236 $X12 \/ ndr1_0 % 0.19/0.43 |- ~c3_0 \/ ~c4_2 a236 $X12 \/ ~c5_2 a237 $X13 \/ ~ndr1_1 a236 \/ % 0.19/0.43 ~ndr1_1 a237 \/ c3_2 a236 $X12 \/ c4_2 a237 $X13 \/ c5_2 a236 $X12 % 0.19/0.43 |- ~c2_2 a237 $X14 \/ ~c3_0 \/ ~c3_2 a237 $X14 \/ ~c4_2 a236 $X12 \/ % 0.19/0.43 ~ndr1_1 a236 \/ ~ndr1_1 a237 \/ c3_2 a236 $X12 \/ c5_2 a236 $X12 \/ % 0.19/0.43 c5_2 a237 $X14 % 0.19/0.43 |- ~c5_2 $X17 a243 \/ ~definitionFOFtoCNF_3 $X17 % 0.19/0.43 |- ~definitionFOFtoCNF_3 $X17 \/ c1_2 $X17 a243 % 0.19/0.43 |- ~definitionFOFtoCNF_3 $X17 \/ ndr1_1 $X17 % 0.19/0.43 |- ~c1_2 $X17 a243 \/ ~ndr1_1 $X17 \/ c5_2 $X17 a243 \/ % 0.19/0.43 definitionFOFtoCNF_3 $X17 % 0.19/0.43 |- ~c2_1 a242 \/ ~c4_0 \/ ~ndr1_0 \/ c4_1 $X17 \/ definitionFOFtoCNF_3 $X17 % 0.19/0.43 |- ~c3_1 a242 \/ ~c4_0 \/ ~ndr1_0 \/ c4_1 $X17 \/ definitionFOFtoCNF_3 $X17 % 0.19/0.43 |- ~c4_0 \/ ~c4_1 a242 \/ ~ndr1_0 \/ c4_1 $X17 \/ definitionFOFtoCNF_3 $X17 % 0.19/0.43 |- ~c1_2 a230 a231 \/ ~c2_1 $X7 \/ ~c4_0 \/ ~ndr1_0 \/ c5_1 $X7 % 0.19/0.43 |- ~c2_1 $X7 \/ ~c4_0 \/ ~c5_2 a230 a231 \/ ~ndr1_0 \/ c5_1 $X7 % 0.19/0.43 |- ~c2_1 $X7 \/ ~c4_0 \/ ~ndr1_0 \/ c2_1 a230 \/ c5_1 $X7 % 0.19/0.43 |- ~c2_1 $X7 \/ ~c4_0 \/ ~ndr1_0 \/ c3_1 a230 \/ c5_1 $X7 % 0.19/0.43 |- ~c2_1 $X7 \/ ~c4_0 \/ ~ndr1_0 \/ c5_1 $X7 \/ ndr1_1 a230 % 0.19/0.44 |- ~c1_2 $X1 $X2 \/ ~c2_1 $Y \/ ~c2_2 $Y $Z \/ ~c3_2 $Y a220 \/ ~c4_0 \/ % 0.19/0.44 ~c5_2 $X1 $X2 \/ ~ndr1_0 \/ ~ndr1_1 $X1 \/ ~ndr1_1 $Y \/ c2_1 $X1 \/ % 0.19/0.44 c2_2 $X1 $X2 \/ c3_2 $Y $Z \/ c4_2 $Y $Z \/ c5_1 $X1 % 0.19/0.44 |- ~c1_2 $X1 $X2 \/ ~c2_1 $Y \/ ~c2_2 $Y $Z \/ ~c4_0 \/ ~c5_2 $X1 $X2 \/ % 0.19/0.44 ~ndr1_0 \/ ~ndr1_1 $X1 \/ ~ndr1_1 $Y \/ c1_2 $Y a220 \/ c2_1 $X1 \/ % 0.19/0.44 c2_2 $X1 $X2 \/ c3_2 $Y $Z \/ c4_2 $Y $Z \/ c5_1 $X1 % 0.19/0.44 |- ~c1_2 $X1 $X2 \/ ~c2_1 $Y \/ ~c2_2 $Y $Z \/ ~c4_0 \/ ~c5_2 $X1 $X2 \/ % 0.19/0.44 ~ndr1_0 \/ ~ndr1_1 $X1 \/ ~ndr1_1 $Y \/ c2_1 $X1 \/ c2_2 $X1 $X2 \/ % 0.19/0.44 c3_2 $Y $Z \/ c4_2 $Y $Z \/ c4_2 $Y a220 \/ c5_1 $X1 % 0.19/0.44 |- ~c3_1 a232 \/ ~c5_0 \/ c3_0 % 0.19/0.44 |- ~c4_1 a232 \/ ~c5_0 \/ c3_0 % 0.19/0.44 |- ~c3_2 a225 a226 \/ ~definitionFOFtoCNF_4 % 0.19/0.44 |- ~definitionFOFtoCNF_4 \/ c1_2 a225 a226 % 0.19/0.44 |- ~definitionFOFtoCNF_4 \/ c4_1 a225 % 0.19/0.44 |- ~definitionFOFtoCNF_4 \/ ndr1_0 % 0.19/0.44 |- ~definitionFOFtoCNF_4 \/ ndr1_1 a225 % 0.19/0.44 |- ~c1_2 a225 a226 \/ ~c4_1 a225 \/ ~ndr1_0 \/ ~ndr1_1 a225 \/ % 0.19/0.44 c3_2 a225 a226 \/ definitionFOFtoCNF_4 % 0.19/0.44 |- ~c5_0 \/ ~c5_2 a223 a224 \/ definitionFOFtoCNF_4 % 0.19/0.44 |- ~c5_0 \/ c2_1 a223 \/ definitionFOFtoCNF_4 % 0.19/0.44 |- ~c5_0 \/ c2_2 a223 a224 \/ definitionFOFtoCNF_4 % 0.19/0.44 |- ~c5_0 \/ c4_2 a223 a224 \/ definitionFOFtoCNF_4 % 0.19/0.44 |- ~c5_0 \/ c5_1 a223 \/ definitionFOFtoCNF_4 % 0.19/0.44 |- ~c5_0 \/ definitionFOFtoCNF_4 \/ ndr1_0 % 0.19/0.44 |- ~c5_0 \/ definitionFOFtoCNF_4 \/ ndr1_1 a223 % 0.19/0.44 |- ~c1_1 $U \/ ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c3_2 $W a218 \/ ~c5_0 \/ % 0.19/0.44 ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $W \/ c3_1 $U % 0.19/0.44 |- ~c1_1 $U \/ ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c5_0 \/ ~ndr1_0 \/ % 0.19/0.44 ~ndr1_1 $U \/ c1_1 $W \/ c1_2 $W a218 \/ c3_1 $U % 0.19/0.44 |- ~c1_1 $U \/ ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c5_0 \/ ~ndr1_0 \/ % 0.19/0.44 ~ndr1_1 $U \/ c1_1 $W \/ c3_1 $U \/ c5_2 $W a218 % 0.19/0.44 |- ~c1_1 $U \/ ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c5_0 \/ ~ndr1_0 \/ % 0.19/0.44 ~ndr1_1 $U \/ c1_1 $W \/ c3_1 $U \/ ndr1_1 $W % 0.19/0.44 |- ~c5_2 a221 a222 \/ c4_0 \/ c5_0 % 0.19/0.44 |- c1_2 a221 a222 \/ c4_0 \/ c5_0 % 0.19/0.44 |- c4_0 \/ c5_0 \/ ndr1_0 % 0.19/0.44 |- c4_0 \/ c5_0 \/ ndr1_1 a221 % 0.19/0.44 |- ~c1_2 a221 $X3 \/ ~c2_2 a221 $X3 \/ ~ndr1_1 a221 \/ c4_0 \/ c5_0 \/ % 0.19/0.44 c5_2 a221 $X3 % 0.19/0.44 |- ~c1_2 $X a219 \/ ~c2_1 $X \/ ~ndr1_0 \/ c4_0 \/ c4_1 $X \/ c5_0 % 0.19/0.44 |- ~c2_1 $X \/ ~c2_2 $X a219 \/ ~ndr1_0 \/ c4_0 \/ c4_1 $X \/ c5_0 % 0.19/0.44 |- ~c2_1 $X \/ ~c3_2 $X a219 \/ ~ndr1_0 \/ c4_0 \/ c4_1 $X \/ c5_0 % 0.19/0.44 |- ~c2_1 $X \/ ~ndr1_0 \/ c4_0 \/ c4_1 $X \/ c5_0 \/ ndr1_1 $X % 0.19/0.44 |- ~c1_2 $X22 a246 \/ ~definitionFOFtoCNF_5 $X22 % 0.19/0.44 |- ~c2_2 $X22 a246 \/ ~definitionFOFtoCNF_5 $X22 % 0.19/0.44 |- ~c3_2 $X22 a246 \/ ~definitionFOFtoCNF_5 $X22 % 0.19/0.44 |- ~definitionFOFtoCNF_5 $X22 \/ ndr1_1 $X22 % 0.19/0.44 |- ~ndr1_1 $X22 \/ c1_2 $X22 a246 \/ c2_2 $X22 a246 \/ c3_2 $X22 a246 \/ % 0.19/0.44 definitionFOFtoCNF_5 $X22 % 0.19/0.44 |- ~c3_1 a247 \/ ~c5_1 a245 \/ ~ndr1_0 \/ c1_1 $X22 \/ c3_1 $X22 \/ % 0.19/0.44 definitionFOFtoCNF_5 $X22 % 0.19/0.44 |- ~c3_1 a247 \/ ~c3_2 a245 $X20 \/ ~ndr1_0 \/ ~ndr1_1 a245 \/ c1_1 $X22 \/ % 0.19/0.44 c3_1 $X22 \/ c5_2 a245 $X20 \/ definitionFOFtoCNF_5 $X22 % 0.19/0.44 |- ~c3_2 a247 $X23 \/ ~c5_1 a245 \/ ~ndr1_0 \/ ~ndr1_1 a247 \/ c1_1 $X22 \/ % 0.19/0.44 c1_2 a247 $X23 \/ c3_1 $X22 \/ definitionFOFtoCNF_5 $X22 % 0.19/0.44 |- ~c3_1 a247 \/ ~c4_2 a245 $X21 \/ ~ndr1_0 \/ ~ndr1_1 a245 \/ c1_1 $X22 \/ % 0.19/0.44 c1_2 a245 $X21 \/ c3_1 $X22 \/ c5_2 a245 $X21 \/ % 0.19/0.44 definitionFOFtoCNF_5 $X22 % 0.19/0.44 |- ~c3_2 a245 $X20 \/ ~c3_2 a247 $X23 \/ ~ndr1_0 \/ ~ndr1_1 a245 \/ % 0.19/0.44 ~ndr1_1 a247 \/ c1_1 $X22 \/ c1_2 a247 $X23 \/ c3_1 $X22 \/ % 0.19/0.44 c5_2 a245 $X20 \/ definitionFOFtoCNF_5 $X22 % 0.19/0.44 |- ~c3_2 a247 $X23 \/ ~c4_2 a245 $X21 \/ ~ndr1_0 \/ ~ndr1_1 a245 \/ % 0.19/0.44 ~ndr1_1 a247 \/ c1_1 $X22 \/ c1_2 a245 $X21 \/ c1_2 a247 $X23 \/ % 0.19/0.44 c3_1 $X22 \/ c5_2 a245 $X21 \/ definitionFOFtoCNF_5 $X22 % 0.19/0.44 |- ~c1_2 a240 a241 \/ ~definitionFOFtoCNF_6 % 0.19/0.44 |- ~c2_1 a240 \/ ~definitionFOFtoCNF_6 % 0.19/0.44 |- ~c5_2 a240 a241 \/ ~definitionFOFtoCNF_6 % 0.19/0.44 |- ~definitionFOFtoCNF_6 \/ c3_1 a240 % 0.19/0.44 |- ~definitionFOFtoCNF_6 \/ c3_2 a240 a241 % 0.19/0.44 |- ~definitionFOFtoCNF_6 \/ ndr1_0 % 0.19/0.44 |- ~definitionFOFtoCNF_6 \/ ndr1_1 a240 % 0.19/0.44 |- ~c3_1 a240 \/ ~c3_2 a240 a241 \/ ~ndr1_0 \/ ~ndr1_1 a240 \/ % 0.19/0.44 c1_2 a240 a241 \/ c2_1 a240 \/ c5_2 a240 a241 \/ definitionFOFtoCNF_6 % 0.19/0.44 |- ~c2_2 $X15 a238 \/ ~definitionFOFtoCNF_7 $X15 % 0.19/0.44 |- ~definitionFOFtoCNF_7 $X15 \/ c1_2 $X15 a238 % 0.19/0.44 |- ~definitionFOFtoCNF_7 $X15 \/ c3_2 $X15 a238 % 0.19/0.44 |- ~definitionFOFtoCNF_7 $X15 \/ ndr1_1 $X15 % 0.19/0.44 |- ~c1_2 $X15 a238 \/ ~c3_2 $X15 a238 \/ ~ndr1_1 $X15 \/ c2_2 $X15 a238 \/ % 0.19/0.44 definitionFOFtoCNF_7 $X15 % 0.19/0.44 |- ~c2_1 $X15 \/ ~c3_1 $X16 \/ ~c4_1 $X16 \/ ~c4_2 $X16 a239 \/ ~ndr1_0 \/ % 0.19/0.44 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 $X15 % 0.19/0.44 |- ~c2_1 $X15 \/ ~c3_1 $X16 \/ ~c4_1 $X16 \/ ~c5_2 $X16 a239 \/ ~ndr1_0 \/ % 0.19/0.44 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 $X15 % 0.19/0.44 |- ~c2_1 $X15 \/ ~c3_1 $X16 \/ ~c4_1 $X16 \/ ~ndr1_0 \/ c2_2 $X16 a239 \/ % 0.19/0.44 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 $X15 % 0.19/0.44 |- ~c2_1 $X15 \/ ~c3_1 $X16 \/ ~c4_1 $X16 \/ ~ndr1_0 \/ % 0.19/0.44 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 $X15 \/ ndr1_1 $X16 % 0.19/0.44 |- ~c5_2 $X11 a235 \/ ~definitionFOFtoCNF_8 $X11 % 0.19/0.44 |- ~definitionFOFtoCNF_8 $X11 \/ c1_2 $X11 a235 % 0.19/0.44 |- ~definitionFOFtoCNF_8 $X11 \/ c4_2 $X11 a235 % 0.19/0.44 |- ~definitionFOFtoCNF_8 $X11 \/ ndr1_1 $X11 % 0.19/0.44 |- ~c1_2 $X11 a235 \/ ~c4_2 $X11 a235 \/ ~ndr1_1 $X11 \/ c5_2 $X11 a235 \/ % 0.19/0.44 definitionFOFtoCNF_8 $X11 % 0.19/0.44 |- ~c5_2 $X9 a234 \/ ~definitionFOFtoCNF_9 $X9 % 0.19/0.44 |- ~definitionFOFtoCNF_9 $X9 \/ c4_2 $X9 a234 % 0.19/0.44 |- ~definitionFOFtoCNF_9 $X9 \/ ndr1_1 $X9 % 0.19/0.44 |- ~c4_2 $X9 a234 \/ ~ndr1_1 $X9 \/ c5_2 $X9 a234 \/ % 0.19/0.44 definitionFOFtoCNF_9 $X9 % 0.19/0.44 |- ~c1_1 $X9 \/ ~c2_1 $X8 \/ ~c2_2 $X9 $X10 \/ ~c4_2 $X9 $X10 \/ % 0.19/0.44 ~c5_2 $X8 a233 \/ ~c5_2 $X9 $X10 \/ ~ndr1_0 \/ ~ndr1_1 $X9 \/ % 0.19/0.44 c4_1 $X8 \/ c5_1 $X11 \/ definitionFOFtoCNF_8 $X11 \/ % 0.19/0.44 definitionFOFtoCNF_9 $X9 % 0.19/0.44 |- ~c1_1 $X9 \/ ~c2_1 $X8 \/ ~c2_2 $X9 $X10 \/ ~c4_2 $X9 $X10 \/ % 0.19/0.44 ~c5_2 $X9 $X10 \/ ~ndr1_0 \/ ~ndr1_1 $X9 \/ c2_2 $X8 a233 \/ c4_1 $X8 \/ % 0.19/0.44 c5_1 $X11 \/ definitionFOFtoCNF_8 $X11 \/ definitionFOFtoCNF_9 $X9 % 0.19/0.44 |- ~c1_1 $X9 \/ ~c2_1 $X8 \/ ~c2_2 $X9 $X10 \/ ~c4_2 $X9 $X10 \/ % 0.19/0.44 ~c5_2 $X9 $X10 \/ ~ndr1_0 \/ ~ndr1_1 $X9 \/ c3_2 $X8 a233 \/ c4_1 $X8 \/ % 0.19/0.44 c5_1 $X11 \/ definitionFOFtoCNF_8 $X11 \/ definitionFOFtoCNF_9 $X9 % 0.19/0.44 |- ~c1_1 $X9 \/ ~c2_1 $X8 \/ ~c2_2 $X9 $X10 \/ ~c4_2 $X9 $X10 \/ % 0.19/0.44 ~c5_2 $X9 $X10 \/ ~ndr1_0 \/ ~ndr1_1 $X9 \/ c4_1 $X8 \/ c5_1 $X11 \/ % 0.19/0.44 definitionFOFtoCNF_8 $X11 \/ definitionFOFtoCNF_9 $X9 \/ ndr1_1 $X8 % 0.19/0.44 |- ~c1_2 $X25 a250 \/ ~c2_1 $X25 \/ ~c3_1 $X25 \/ ~c4_2 $X25 a250 \/ % 0.19/0.44 ~c5_2 $X25 a250 \/ ~ndr1_0 \/ ~ndr1_1 $X25 \/ c4_1 $X25 \/ c5_1 $X25 % 0.19/0.44 |- ~c1_1 $X9 \/ ~c2_1 $X9 \/ ~c2_2 $X9 a233 \/ ~c4_2 $X9 a233 \/ % 0.19/0.44 ~c5_2 $X9 a233 \/ ~ndr1_0 \/ ~ndr1_1 $X9 \/ c4_1 $X9 \/ c5_1 $X11 \/ % 0.19/0.44 definitionFOFtoCNF_8 $X11 \/ definitionFOFtoCNF_9 $X9 % 0.19/0.44 |- c1_2 a221 a246 \/ c2_2 a221 a246 \/ c3_2 a221 a246 \/ c4_0 \/ c5_0 \/ % 0.19/0.44 definitionFOFtoCNF_5 a221 % 0.19/0.44 |- c1_2 a248 a246 \/ c2_2 a248 a246 \/ c3_0 \/ c3_2 a248 a246 \/ % 0.19/0.44 definitionFOFtoCNF_5 a248 % 0.19/0.44 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.44 %------------------------------------------------------------------------------