%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN522+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:36 EDT 2022 % Result : CounterSatisfiable 0.18s 0.48s % Output : Saturation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN522+1 : TPTP v8.1.0. Released v2.1.0. % 0.03/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 15:30:53 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.18/0.48 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.48 % 0.18/0.48 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.48 |- c4_0 % 0.18/0.48 |- ~c1_0 \/ ~c2_2 a121 a122 % 0.18/0.48 |- ~c1_0 \/ c3_2 a121 a122 % 0.18/0.48 |- ~c1_0 \/ ndr1_0 % 0.18/0.48 |- ~c1_0 \/ ndr1_1 a121 % 0.18/0.48 |- ~c1_0 \/ ~c1_2 a121 $X12 \/ ~c4_2 a121 $X12 \/ ~ndr1_1 a121 \/ % 0.18/0.48 c3_2 a121 $X12 % 0.18/0.48 |- ~c1_0 \/ ~c1_2 a121 $X13 \/ ~c5_2 a121 $X13 \/ ~ndr1_1 a121 \/ % 0.18/0.48 c3_2 a121 $X13 % 0.18/0.48 |- ~c2_1 a118 \/ c1_0 % 0.18/0.48 |- c1_0 \/ c1_1 a118 % 0.18/0.48 |- c1_0 \/ c5_1 a118 % 0.18/0.48 |- c1_0 \/ ndr1_0 % 0.18/0.48 |- ~c1_1 a114 \/ c2_0 % 0.18/0.48 |- c2_0 \/ ndr1_0 % 0.18/0.48 |- ~c3_2 a114 $X7 \/ ~ndr1_1 a114 \/ c2_0 \/ c5_2 a114 $X7 % 0.18/0.48 |- ~ndr1_1 a114 \/ c1_2 a114 $X8 \/ c2_0 \/ c4_2 a114 $X8 \/ c5_2 a114 $X8 % 0.18/0.48 |- ~c1_0 \/ ~c5_0 \/ c3_0 % 0.18/0.48 |- ~c1_0 \/ ~c3_1 $X5 \/ ~c4_1 $X5 \/ ~ndr1_0 \/ ~ndr1_1 $X5 \/ % 0.18/0.48 c4_2 $X5 $X6 \/ c5_0 \/ c5_2 $X5 $X6 % 0.18/0.48 |- ~c3_2 $X1 a111 \/ ~definitionFOFtoCNF_0 $X1 % 0.18/0.48 |- ~definitionFOFtoCNF_0 $X1 \/ c2_2 $X1 a111 % 0.18/0.48 |- ~definitionFOFtoCNF_0 $X1 \/ c5_2 $X1 a111 % 0.18/0.48 |- ~definitionFOFtoCNF_0 $X1 \/ ndr1_1 $X1 % 0.18/0.48 |- ~c2_2 $X1 a111 \/ ~c5_2 $X1 a111 \/ ~ndr1_1 $X1 \/ c3_2 $X1 a111 \/ % 0.18/0.48 definitionFOFtoCNF_0 $X1 % 0.18/0.48 |- ~c1_0 \/ ~c2_2 $X1 $X2 \/ ~c3_2 a112 a113 \/ ~c4_1 $X1 \/ ~ndr1_0 \/ % 0.18/0.48 ~ndr1_1 $X1 \/ c1_2 $X1 $X2 \/ c4_2 $X1 $X2 \/ definitionFOFtoCNF_0 $X1 % 0.18/0.48 |- ~c1_0 \/ ~c2_2 $X1 $X2 \/ ~c4_1 $X1 \/ ~c5_2 a112 a113 \/ ~ndr1_0 \/ % 0.18/0.48 ~ndr1_1 $X1 \/ c1_2 $X1 $X2 \/ c4_2 $X1 $X2 \/ definitionFOFtoCNF_0 $X1 % 0.18/0.48 |- ~c1_0 \/ ~c2_2 $X1 $X2 \/ ~c4_1 $X1 \/ ~ndr1_0 \/ ~ndr1_1 $X1 \/ % 0.18/0.48 c1_2 $X1 $X2 \/ c2_2 a112 a113 \/ c4_2 $X1 $X2 \/ % 0.18/0.48 definitionFOFtoCNF_0 $X1 % 0.18/0.48 |- ~c1_0 \/ ~c2_2 $X1 $X2 \/ ~c4_1 $X1 \/ ~ndr1_0 \/ ~ndr1_1 $X1 \/ % 0.18/0.48 c1_2 $X1 $X2 \/ c4_2 $X1 $X2 \/ definitionFOFtoCNF_0 $X1 \/ ndr1_1 a112 % 0.18/0.48 |- ~c1_0 \/ ~c2_2 $X1 $X2 \/ ~c4_1 $X1 \/ ~ndr1_0 \/ ~ndr1_1 $X1 \/ % 0.18/0.48 ~ndr1_1 a112 \/ c1_2 $X1 $X2 \/ c1_2 a112 $X3 \/ c4_2 $X1 $X2 \/ % 0.18/0.48 c5_2 a112 $X3 \/ definitionFOFtoCNF_0 $X1 % 0.18/0.48 |- ~c2_0 \/ ~c4_2 $X19 a138 \/ ~ndr1_0 \/ ~ndr1_1 $X19 \/ c2_2 $X19 $X20 \/ % 0.18/0.48 c3_2 $X19 $X20 \/ c5_1 $X19 \/ c5_2 $X19 $X20 % 0.18/0.48 |- ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $X19 \/ c2_2 $X19 $X20 \/ c3_2 $X19 $X20 \/ % 0.18/0.48 c5_1 $X19 \/ c5_2 $X19 $X20 \/ c5_2 $X19 a138 % 0.18/0.48 |- ~c3_0 \/ c1_1 a137 % 0.18/0.48 |- ~c3_0 \/ c4_1 a137 % 0.18/0.48 |- ~c3_0 \/ ndr1_0 % 0.18/0.48 |- ~c2_2 $X9 a116 \/ ~definitionFOFtoCNF_1 $X9 % 0.18/0.48 |- ~definitionFOFtoCNF_1 $X9 \/ c1_2 $X9 a116 % 0.18/0.48 |- ~definitionFOFtoCNF_1 $X9 \/ c5_2 $X9 a116 % 0.18/0.48 |- ~definitionFOFtoCNF_1 $X9 \/ ndr1_1 $X9 % 0.18/0.48 |- ~c1_2 $X9 a116 \/ ~c5_2 $X9 a116 \/ ~ndr1_1 $X9 \/ c2_2 $X9 a116 \/ % 0.18/0.48 definitionFOFtoCNF_1 $X9 % 0.18/0.48 |- ~c4_2 $X9 a115 \/ ~definitionFOFtoCNF_2 $X9 % 0.18/0.48 |- ~definitionFOFtoCNF_2 $X9 \/ c2_2 $X9 a115 % 0.18/0.48 |- ~definitionFOFtoCNF_2 $X9 \/ c5_2 $X9 a115 % 0.18/0.48 |- ~definitionFOFtoCNF_2 $X9 \/ ndr1_1 $X9 % 0.18/0.48 |- ~c2_2 $X9 a115 \/ ~c5_2 $X9 a115 \/ ~ndr1_1 $X9 \/ c4_2 $X9 a115 \/ % 0.18/0.48 definitionFOFtoCNF_2 $X9 % 0.18/0.48 |- ~c3_0 \/ ~c4_1 $X10 \/ ~c5_2 $X9 a117 \/ ~ndr1_0 \/ c2_1 $X10 \/ % 0.18/0.48 definitionFOFtoCNF_1 $X9 \/ definitionFOFtoCNF_2 $X9 % 0.18/0.48 |- ~c3_0 \/ ~c4_1 $X10 \/ ~ndr1_0 \/ c2_1 $X10 \/ c3_2 $X9 a117 \/ % 0.18/0.48 definitionFOFtoCNF_1 $X9 \/ definitionFOFtoCNF_2 $X9 % 0.18/0.48 |- ~c3_0 \/ ~c4_1 $X10 \/ ~ndr1_0 \/ c2_1 $X10 \/ c4_2 $X9 a117 \/ % 0.18/0.48 definitionFOFtoCNF_1 $X9 \/ definitionFOFtoCNF_2 $X9 % 0.18/0.48 |- ~c3_0 \/ ~c4_1 $X10 \/ ~ndr1_0 \/ c2_1 $X10 \/ % 0.18/0.48 definitionFOFtoCNF_1 $X9 \/ definitionFOFtoCNF_2 $X9 \/ ndr1_1 $X9 % 0.18/0.48 |- ~c1_2 $X11 a120 \/ ~definitionFOFtoCNF_3 $X11 % 0.18/0.48 |- ~definitionFOFtoCNF_3 $X11 \/ c2_2 $X11 a120 % 0.18/0.48 |- ~definitionFOFtoCNF_3 $X11 \/ c5_2 $X11 a120 % 0.18/0.48 |- ~definitionFOFtoCNF_3 $X11 \/ ndr1_1 $X11 % 0.18/0.48 |- ~c2_2 $X11 a120 \/ ~c5_2 $X11 a120 \/ ~ndr1_1 $X11 \/ c1_2 $X11 a120 \/ % 0.18/0.48 definitionFOFtoCNF_3 $X11 % 0.18/0.48 |- ~c2_2 $X11 a119 \/ ~ndr1_0 \/ c3_0 \/ c4_1 $X11 \/ % 0.18/0.48 definitionFOFtoCNF_3 $X11 % 0.18/0.48 |- ~c3_2 $X11 a119 \/ ~ndr1_0 \/ c3_0 \/ c4_1 $X11 \/ % 0.18/0.48 definitionFOFtoCNF_3 $X11 % 0.18/0.48 |- ~ndr1_0 \/ c3_0 \/ c4_1 $X11 \/ c4_2 $X11 a119 \/ % 0.18/0.48 definitionFOFtoCNF_3 $X11 % 0.18/0.48 |- ~ndr1_0 \/ c3_0 \/ c4_1 $X11 \/ definitionFOFtoCNF_3 $X11 \/ ndr1_1 $X11 % 0.18/0.48 |- ~definitionFOFtoCNF_4 $X16 \/ c1_2 $X16 a132 % 0.18/0.48 |- ~definitionFOFtoCNF_4 $X16 \/ c2_2 $X16 a132 % 0.18/0.48 |- ~definitionFOFtoCNF_4 $X16 \/ c5_2 $X16 a132 % 0.18/0.48 |- ~definitionFOFtoCNF_4 $X16 \/ ndr1_1 $X16 % 0.18/0.48 |- ~c1_2 $X16 a132 \/ ~c2_2 $X16 a132 \/ ~c5_2 $X16 a132 \/ ~ndr1_1 $X16 \/ % 0.18/0.48 definitionFOFtoCNF_4 $X16 % 0.18/0.48 |- ~c1_2 $X16 a131 \/ ~c2_1 a133 \/ ~ndr1_0 \/ c2_0 \/ c5_1 $X16 \/ % 0.18/0.48 definitionFOFtoCNF_4 $X16 % 0.18/0.48 |- ~c1_2 $X16 a131 \/ ~c5_1 a133 \/ ~ndr1_0 \/ c2_0 \/ c5_1 $X16 \/ % 0.18/0.48 definitionFOFtoCNF_4 $X16 % 0.18/0.48 |- ~c2_1 a133 \/ ~c4_2 $X16 a131 \/ ~ndr1_0 \/ c2_0 \/ c5_1 $X16 \/ % 0.18/0.48 definitionFOFtoCNF_4 $X16 % 0.18/0.48 |- ~c2_1 a133 \/ ~ndr1_0 \/ c2_0 \/ c5_1 $X16 \/ % 0.18/0.48 definitionFOFtoCNF_4 $X16 \/ ndr1_1 $X16 % 0.18/0.48 |- ~c4_2 $X16 a131 \/ ~c5_1 a133 \/ ~ndr1_0 \/ c2_0 \/ c5_1 $X16 \/ % 0.18/0.48 definitionFOFtoCNF_4 $X16 % 0.18/0.48 |- ~c5_1 a133 \/ ~ndr1_0 \/ c2_0 \/ c5_1 $X16 \/ % 0.18/0.48 definitionFOFtoCNF_4 $X16 \/ ndr1_1 $X16 % 0.18/0.48 |- ~c1_1 a109 \/ ~definitionFOFtoCNF_5 % 0.18/0.48 |- ~definitionFOFtoCNF_5 \/ c3_1 a109 % 0.18/0.48 |- ~definitionFOFtoCNF_5 \/ ndr1_0 % 0.18/0.48 |- ~c3_1 a109 \/ ~ndr1_0 \/ c1_1 a109 \/ definitionFOFtoCNF_5 % 0.18/0.48 |- ~c1_2 $Y $Z \/ ~c3_1 $Y \/ ~c3_1 a110 \/ ~c3_2 $Y $Z \/ ~c5_1 $Y \/ % 0.18/0.48 ~c5_2 $Y $Z \/ ~ndr1_0 \/ ~ndr1_1 $Y \/ definitionFOFtoCNF_5 % 0.18/0.48 |- ~c1_2 $Y $Z \/ ~c3_1 $Y \/ ~c3_2 $Y $Z \/ ~c4_1 a110 \/ ~c5_1 $Y \/ % 0.18/0.48 ~c5_2 $Y $Z \/ ~ndr1_0 \/ ~ndr1_1 $Y \/ definitionFOFtoCNF_5 % 0.18/0.48 |- ~c1_2 $Y $Z \/ ~c3_1 $Y \/ ~c3_2 $Y $Z \/ ~c5_1 $Y \/ ~c5_2 $Y $Z \/ % 0.18/0.48 ~ndr1_0 \/ ~ndr1_1 $Y \/ ~ndr1_1 a110 \/ c1_2 a110 $X \/ c5_2 a110 $X \/ % 0.18/0.48 definitionFOFtoCNF_5 % 0.18/0.48 |- ~c2_2 a125 a127 \/ ~definitionFOFtoCNF_6 % 0.18/0.48 |- ~c3_2 a125 a126 \/ ~definitionFOFtoCNF_6 % 0.18/0.48 |- ~c3_2 a125 a127 \/ ~definitionFOFtoCNF_6 % 0.18/0.48 |- ~c4_1 a125 \/ ~definitionFOFtoCNF_6 % 0.18/0.48 |- ~c4_2 a125 a127 \/ ~definitionFOFtoCNF_6 % 0.18/0.48 |- ~c5_2 a125 a126 \/ ~definitionFOFtoCNF_6 % 0.18/0.48 |- ~definitionFOFtoCNF_6 \/ c1_2 a125 a126 % 0.18/0.48 |- ~definitionFOFtoCNF_6 \/ ndr1_0 % 0.18/0.48 |- ~definitionFOFtoCNF_6 \/ ndr1_1 a125 % 0.18/0.48 |- ~c1_2 a125 a126 \/ ~ndr1_0 \/ ~ndr1_1 a125 \/ c2_2 a125 a127 \/ % 0.18/0.48 c3_2 a125 a126 \/ c3_2 a125 a127 \/ c4_1 a125 \/ c4_2 a125 a127 \/ % 0.18/0.48 c5_2 a125 a126 \/ definitionFOFtoCNF_6 % 0.18/0.48 |- ~c1_2 a128 a129 \/ ~definitionFOFtoCNF_7 % 0.18/0.48 |- ~c2_1 a128 \/ ~definitionFOFtoCNF_7 % 0.18/0.48 |- ~definitionFOFtoCNF_7 \/ c2_2 a128 a129 % 0.18/0.48 |- ~definitionFOFtoCNF_7 \/ c3_1 a128 % 0.18/0.48 |- ~definitionFOFtoCNF_7 \/ c4_2 a128 a129 % 0.18/0.48 |- ~definitionFOFtoCNF_7 \/ ndr1_0 % 0.18/0.48 |- ~definitionFOFtoCNF_7 \/ ndr1_1 a128 % 0.18/0.48 |- ~c2_2 a128 a129 \/ ~c3_1 a128 \/ ~c4_2 a128 a129 \/ ~ndr1_0 \/ % 0.18/0.48 ~ndr1_1 a128 \/ c1_2 a128 a129 \/ c2_1 a128 \/ definitionFOFtoCNF_7 % 0.18/0.48 |- ~c1_1 a130 \/ definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 % 0.18/0.48 |- definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ ndr1_0 % 0.18/0.48 |- ~ndr1_1 a130 \/ c2_2 a130 $X15 \/ c5_2 a130 $X15 \/ % 0.18/0.48 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 % 0.18/0.48 |- ~c2_2 a130 $X14 \/ ~c3_2 a130 $X14 \/ ~c4_2 a130 $X14 \/ ~ndr1_1 a130 \/ % 0.18/0.48 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 % 0.18/0.48 |- ~c3_2 $U a105 \/ definitionFOFtoCNF_9 $U % 0.18/0.48 |- ~c4_2 $U a105 \/ definitionFOFtoCNF_9 $U % 0.18/0.48 |- c2_2 $U a105 \/ definitionFOFtoCNF_9 $U % 0.18/0.48 |- definitionFOFtoCNF_9 $U \/ ndr1_1 $U % 0.18/0.48 |- ~c2_2 $U a105 \/ ~definitionFOFtoCNF_9 $U \/ ~ndr1_1 $U \/ % 0.18/0.48 c3_2 $U a105 \/ c4_2 $U a105 % 0.18/0.48 |- definitionFOFtoCNF_8 $U \/ definitionFOFtoCNF_9 $U % 0.18/0.48 |- ~c1_2 $U a104 \/ ~definitionFOFtoCNF_8 $U \/ ~definitionFOFtoCNF_9 $U % 0.18/0.48 |- ~definitionFOFtoCNF_8 $U \/ ~definitionFOFtoCNF_9 $U \/ c3_2 $U a104 % 0.18/0.48 |- ~definitionFOFtoCNF_8 $U \/ ~definitionFOFtoCNF_9 $U \/ c4_2 $U a104 % 0.18/0.48 |- ~definitionFOFtoCNF_8 $U \/ ~definitionFOFtoCNF_9 $U \/ ndr1_1 $U % 0.18/0.48 |- ~c3_2 $U a104 \/ ~c4_2 $U a104 \/ ~ndr1_1 $U \/ c1_2 $U a104 \/ % 0.18/0.48 definitionFOFtoCNF_8 $U % 0.18/0.48 |- ~c5_1 a106 \/ ~definitionFOFtoCNF_10 % 0.18/0.48 |- ~definitionFOFtoCNF_10 \/ c1_2 a106 a107 % 0.18/0.48 |- ~definitionFOFtoCNF_10 \/ c2_2 a106 a107 % 0.18/0.48 |- ~definitionFOFtoCNF_10 \/ c4_2 a106 a107 % 0.18/0.48 |- ~definitionFOFtoCNF_10 \/ ndr1_0 % 0.18/0.49 |- ~definitionFOFtoCNF_10 \/ ndr1_1 a106 % 0.18/0.49 |- ~c1_2 a106 a107 \/ ~c2_2 a106 a107 \/ ~c4_2 a106 a107 \/ ~ndr1_0 \/ % 0.18/0.49 ~ndr1_1 a106 \/ c5_1 a106 \/ definitionFOFtoCNF_10 % 0.18/0.49 |- ~c4_1 a108 \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c2_2 $U $V \/ % 0.18/0.49 c3_2 $U $V \/ definitionFOFtoCNF_10 \/ definitionFOFtoCNF_8 $U % 0.18/0.49 |- ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c3_1 a108 \/ % 0.18/0.49 c3_2 $U $V \/ definitionFOFtoCNF_10 \/ definitionFOFtoCNF_8 $U % 0.18/0.49 |- ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ndr1_1 a108 \/ c1_2 a108 $W \/ % 0.18/0.49 c2_2 $U $V \/ c2_2 a108 $W \/ c3_2 $U $V \/ c4_2 a108 $W \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_8 $U % 0.18/0.49 |- ~c4_1 $X21 \/ ~c5_1 $X21 \/ ~ndr1_0 \/ ~ndr1_1 $X21 \/ c1_2 $X21 $X22 \/ % 0.18/0.49 c2_2 $X21 $X22 \/ c3_2 $X21 $X22 % 0.18/0.49 |- c3_0 \/ c4_1 $_30 \/ definitionFOFtoCNF_3 $_30 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ ndr1_1 $_30 % 0.18/0.49 |- c2_0 \/ c3_0 \/ c4_1 $_30 \/ definitionFOFtoCNF_3 $_30 \/ ndr1_1 $_30 % 0.18/0.49 |- c1_0 \/ c3_0 \/ c4_1 $_30 \/ definitionFOFtoCNF_3 $_30 \/ ndr1_1 $_30 % 0.18/0.49 |- c3_0 \/ c4_1 $_33 \/ c4_2 $_33 a119 \/ definitionFOFtoCNF_3 $_33 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 % 0.18/0.49 |- c2_0 \/ c3_0 \/ c4_1 $_33 \/ c4_2 $_33 a119 \/ definitionFOFtoCNF_3 $_33 % 0.18/0.49 |- c1_0 \/ c3_0 \/ c4_1 $_33 \/ c4_2 $_33 a119 \/ definitionFOFtoCNF_3 $_33 % 0.18/0.49 |- c2_2 a130 $_36 \/ c5_2 a130 $_36 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_9 a130 % 0.18/0.49 |- ~c1_0 \/ ~c1_2 a121 a119 \/ ~ndr1_1 a121 \/ c2_0 \/ c3_0 \/ % 0.18/0.49 c3_2 a121 a119 \/ c4_1 a121 \/ definitionFOFtoCNF_3 a121 % 0.18/0.49 |- c1_2 a114 $_41 \/ c2_0 \/ c3_0 \/ c4_1 a114 \/ c4_2 a114 $_41 \/ % 0.18/0.49 c5_2 a114 $_41 \/ definitionFOFtoCNF_3 a114 % 0.18/0.49 |- c1_2 a114 $_41 \/ c2_0 \/ c4_2 a114 $_41 \/ c5_2 a114 $_41 \/ % 0.18/0.49 definitionFOFtoCNF_9 a114 % 0.18/0.49 |- ~c1_2 a130 a116 \/ ~ndr1_1 a130 \/ c2_2 a130 a116 \/ % 0.18/0.49 definitionFOFtoCNF_1 a130 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_9 a130 % 0.18/0.49 |- c2_2 a130 $X15 \/ c3_0 \/ c4_1 a130 \/ c5_2 a130 $X15 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 % 0.18/0.49 |- ~c2_2 a114 a111 \/ ~ndr1_1 a114 \/ c1_2 a114 a111 \/ c2_0 \/ % 0.18/0.49 c3_2 a114 a111 \/ c4_2 a114 a111 \/ definitionFOFtoCNF_0 a114 \/ % 0.18/0.49 definitionFOFtoCNF_9 a114 % 0.18/0.49 |- ~c2_2 a114 a115 \/ ~ndr1_1 a114 \/ c1_2 a114 a115 \/ c2_0 \/ % 0.18/0.49 c4_2 a114 a115 \/ definitionFOFtoCNF_2 a114 \/ definitionFOFtoCNF_9 a114 % 0.18/0.49 |- ~c2_2 a114 a120 \/ ~ndr1_1 a114 \/ c1_2 a114 a120 \/ c2_0 \/ % 0.18/0.49 c4_2 a114 a120 \/ definitionFOFtoCNF_3 a114 \/ definitionFOFtoCNF_9 a114 % 0.18/0.49 |- ~c1_0 \/ ~c1_2 a121 a119 \/ ~ndr1_1 a121 \/ c3_0 \/ c3_2 a121 a119 \/ % 0.18/0.49 c4_1 a121 \/ definitionFOFtoCNF_3 a121 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 % 0.18/0.49 |- ~c2_2 a130 a119 \/ ~c3_2 a130 a119 \/ ~ndr1_1 a130 \/ c3_0 \/ % 0.18/0.49 c4_1 a130 \/ definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 % 0.18/0.49 |- ~c2_2 a114 a111 \/ ~ndr1_1 a114 \/ c1_2 a114 a111 \/ c2_0 \/ c3_0 \/ % 0.18/0.49 c3_2 a114 a111 \/ c4_1 a114 \/ c4_2 a114 a111 \/ % 0.18/0.49 definitionFOFtoCNF_0 a114 \/ definitionFOFtoCNF_3 a114 % 0.18/0.49 |- ~c2_2 a114 a115 \/ ~ndr1_1 a114 \/ c1_2 a114 a115 \/ c2_0 \/ c3_0 \/ % 0.18/0.49 c4_1 a114 \/ c4_2 a114 a115 \/ definitionFOFtoCNF_2 a114 \/ % 0.18/0.49 definitionFOFtoCNF_3 a114 % 0.18/0.49 |- ~c2_2 a114 a120 \/ ~ndr1_1 a114 \/ c1_2 a114 a120 \/ c2_0 \/ c3_0 \/ % 0.18/0.49 c4_1 a114 \/ c4_2 a114 a120 \/ definitionFOFtoCNF_3 a114 % 0.18/0.49 |- ~c1_2 a130 a116 \/ ~ndr1_1 a130 \/ c2_2 a130 a116 \/ c3_0 \/ % 0.18/0.49 c4_1 a130 \/ definitionFOFtoCNF_1 a130 \/ definitionFOFtoCNF_3 a130 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 % 0.18/0.49 |- ~c3_0 \/ ~c4_1 $_64 \/ ~ndr1_0 \/ c2_1 $_64 \/ c2_2 a130 a117 \/ % 0.18/0.49 definitionFOFtoCNF_1 a130 \/ definitionFOFtoCNF_2 a130 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_9 a130 % 0.18/0.49 |- ~c4_1 $_70 \/ ~c5_1 $_70 \/ ~ndr1_0 \/ c1_2 $_70 $_71 \/ % 0.18/0.49 c2_2 $_70 $_71 \/ c3_2 $_70 $_71 \/ definitionFOFtoCNF_9 $_70 % 0.18/0.49 |- ~c4_1 a118 \/ ~ndr1_0 \/ c1_0 \/ c1_2 a118 $_73 \/ c2_2 a118 $_73 \/ % 0.18/0.49 c3_2 a118 $_73 \/ definitionFOFtoCNF_9 a118 % 0.18/0.49 |- ~c1_0 \/ ~c3_1 $_75 \/ ~c4_1 $_75 \/ ~ndr1_0 \/ c4_2 $_75 $_76 \/ % 0.18/0.49 c5_0 \/ c5_2 $_75 $_76 \/ definitionFOFtoCNF_9 $_75 % 0.18/0.49 |- ~c2_0 \/ ~ndr1_0 \/ c2_2 $_86 $_87 \/ c3_2 $_86 $_87 \/ c5_1 $_86 \/ % 0.18/0.49 c5_2 $_86 $_87 \/ c5_2 $_86 a138 \/ definitionFOFtoCNF_9 $_86 % 0.18/0.49 |- ~c1_0 \/ ~c4_1 $_90 \/ ~ndr1_0 \/ c1_2 $_90 a105 \/ c4_2 $_90 a105 \/ % 0.18/0.49 definitionFOFtoCNF_0 $_90 \/ definitionFOFtoCNF_9 $_90 \/ ndr1_1 a112 % 0.18/0.49 |- ~c1_2 a130 $_93 \/ ~c3_1 a110 \/ ~c3_1 a130 \/ ~c3_2 a130 $_93 \/ % 0.18/0.49 ~c5_1 a130 \/ ~ndr1_0 \/ ~ndr1_1 a130 \/ c2_2 a130 $_93 \/ c3_0 \/ % 0.18/0.49 c4_1 a130 \/ definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_5 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 % 0.18/0.49 |- ~c1_2 a130 $_93 \/ ~c3_1 a110 \/ ~c3_1 a130 \/ ~c3_2 a130 $_93 \/ % 0.18/0.49 ~c5_1 a130 \/ ~ndr1_0 \/ ~ndr1_1 a130 \/ c2_2 a130 $_93 \/ % 0.18/0.49 definitionFOFtoCNF_5 \/ definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_9 a130 % 0.18/0.49 |- ~c1_2 a130 $_95 \/ ~c3_1 a130 \/ ~c3_2 a130 $_95 \/ ~c4_1 a110 \/ % 0.18/0.49 ~c5_1 a130 \/ ~ndr1_0 \/ ~ndr1_1 a130 \/ c2_2 a130 $_95 \/ c3_0 \/ % 0.18/0.49 c4_1 a130 \/ definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_5 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 % 0.18/0.49 |- ~c1_2 a130 $_95 \/ ~c3_1 a130 \/ ~c3_2 a130 $_95 \/ ~c4_1 a110 \/ % 0.18/0.49 ~c5_1 a130 \/ ~ndr1_0 \/ ~ndr1_1 a130 \/ c2_2 a130 $_95 \/ % 0.18/0.49 definitionFOFtoCNF_5 \/ definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_9 a130 % 0.18/0.49 |- ~c2_0 \/ c2_2 $_96 $_97 \/ c3_2 $_96 $_97 \/ c5_1 $_96 \/ % 0.18/0.49 c5_2 $_96 $_97 \/ c5_2 $_96 a138 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_9 $_96 % 0.18/0.49 |- ~c2_0 \/ c1_0 \/ c2_2 $_96 $_97 \/ c3_2 $_96 $_97 \/ c5_1 $_96 \/ % 0.18/0.49 c5_2 $_96 $_97 \/ c5_2 $_96 a138 \/ definitionFOFtoCNF_9 $_96 % 0.18/0.49 |- ~c1_0 \/ ~c3_2 a112 a113 \/ ~c4_1 $_100 \/ ~ndr1_0 \/ c1_2 $_100 a105 \/ % 0.18/0.49 c4_2 $_100 a105 \/ definitionFOFtoCNF_0 $_100 \/ % 0.18/0.49 definitionFOFtoCNF_9 $_100 % 0.18/0.49 |- ~c1_0 \/ ~c4_1 $_104 \/ ~c5_2 a112 a113 \/ ~ndr1_0 \/ c1_2 $_104 a105 \/ % 0.18/0.49 c4_2 $_104 a105 \/ definitionFOFtoCNF_0 $_104 \/ % 0.18/0.49 definitionFOFtoCNF_9 $_104 % 0.18/0.49 |- ~c1_0 \/ ~c4_1 $_108 \/ ~ndr1_0 \/ c1_2 $_108 a105 \/ c2_2 a112 a113 \/ % 0.18/0.49 c4_2 $_108 a105 \/ definitionFOFtoCNF_0 $_108 \/ % 0.18/0.49 definitionFOFtoCNF_9 $_108 % 0.18/0.49 |- ~c4_1 a108 \/ ~ndr1_0 \/ c2_2 a130 $_110 \/ c3_0 \/ c3_2 a130 $_110 \/ % 0.18/0.49 c4_1 a130 \/ definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a130 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 % 0.18/0.49 |- c3_0 \/ c3_1 a108 \/ c4_1 a130 \/ definitionFOFtoCNF_10 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 a130 % 0.18/0.49 |- ~c4_1 a108 \/ ~ndr1_0 \/ c1_2 a114 $_121 \/ c2_0 \/ c2_2 a114 $_121 \/ % 0.18/0.49 c3_0 \/ c3_2 a114 $_121 \/ c4_1 a114 \/ c4_2 a114 $_121 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a114 \/ % 0.18/0.49 definitionFOFtoCNF_8 a114 % 0.18/0.49 |- c1_2 a114 $_124 \/ c2_0 \/ c2_2 a114 $_124 \/ c3_0 \/ c3_1 a108 \/ % 0.18/0.49 c3_2 a114 $_124 \/ c4_1 a114 \/ c4_2 a114 $_124 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a114 \/ % 0.18/0.49 definitionFOFtoCNF_8 a114 % 0.18/0.49 |- ~c5_1 a133 \/ ~ndr1_0 \/ c1_2 a114 a131 \/ c2_0 \/ c2_2 a114 a131 \/ % 0.18/0.49 c3_0 \/ c3_1 a108 \/ c3_2 a114 a131 \/ c4_1 a114 \/ c5_1 a114 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a114 \/ % 0.18/0.49 definitionFOFtoCNF_4 a114 \/ definitionFOFtoCNF_8 a114 % 0.18/0.49 |- ~c2_1 a133 \/ ~ndr1_0 \/ c1_2 a114 a131 \/ c2_0 \/ c2_2 a114 a131 \/ % 0.18/0.49 c3_0 \/ c3_1 a108 \/ c3_2 a114 a131 \/ c4_1 a114 \/ c5_1 a114 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a114 \/ % 0.18/0.49 definitionFOFtoCNF_4 a114 \/ definitionFOFtoCNF_8 a114 % 0.18/0.49 |- ~c2_0 \/ c1_0 \/ c2_2 $_128 $_129 \/ c3_0 \/ c3_2 $_128 $_129 \/ % 0.18/0.49 c4_1 $_128 \/ c5_1 $_128 \/ c5_2 $_128 $_129 \/ c5_2 $_128 a138 \/ % 0.18/0.49 definitionFOFtoCNF_3 $_128 % 0.18/0.49 |- ~c2_0 \/ c2_2 $_132 $_133 \/ c3_0 \/ c3_2 $_132 $_133 \/ c4_1 $_132 \/ % 0.18/0.49 c5_1 $_132 \/ c5_2 $_132 $_133 \/ c5_2 $_132 a138 \/ % 0.18/0.49 definitionFOFtoCNF_3 $_132 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 % 0.18/0.49 |- ~c1_0 \/ ~c4_1 a112 \/ ~ndr1_0 \/ c1_2 a112 $_139 \/ c1_2 a112 a105 \/ % 0.18/0.49 c4_2 a112 a105 \/ c5_2 a112 $_139 \/ definitionFOFtoCNF_0 a112 \/ % 0.18/0.49 definitionFOFtoCNF_9 a112 % 0.18/0.49 |- ~c1_0 \/ ~c4_1 $_141 \/ ~ndr1_0 \/ ~ndr1_1 a112 \/ c1_2 $_141 a105 \/ % 0.18/0.49 c1_2 a112 $_142 \/ c4_2 $_141 a105 \/ c5_2 a112 $_142 \/ % 0.18/0.49 definitionFOFtoCNF_0 $_141 \/ definitionFOFtoCNF_9 $_141 % 0.18/0.49 |- ~c1_0 \/ ~c4_1 $_143 \/ ~ndr1_0 \/ c1_2 $_143 a105 \/ c1_2 a112 $_144 \/ % 0.18/0.49 c4_2 $_143 a105 \/ c5_2 a112 $_144 \/ definitionFOFtoCNF_0 $_143 \/ % 0.18/0.49 definitionFOFtoCNF_9 $_143 \/ definitionFOFtoCNF_9 a112 % 0.18/0.49 |- ~c1_2 a130 $_147 \/ ~c3_1 a130 \/ ~c3_2 a130 $_147 \/ ~c5_1 a130 \/ % 0.18/0.49 ~ndr1_0 \/ ~ndr1_1 a110 \/ ~ndr1_1 a130 \/ c1_2 a110 $_145 \/ % 0.18/0.49 c2_2 a130 $_147 \/ c3_0 \/ c4_1 a130 \/ c5_2 a110 $_145 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_5 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 % 0.18/0.49 |- ~c1_2 a130 $_147 \/ ~c3_1 a130 \/ ~c3_2 a130 $_147 \/ ~c5_1 a130 \/ % 0.18/0.49 ~ndr1_0 \/ ~ndr1_1 a110 \/ ~ndr1_1 a130 \/ c1_2 a110 $_145 \/ % 0.18/0.49 c2_2 a130 $_147 \/ c5_2 a110 $_145 \/ definitionFOFtoCNF_5 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_9 a130 % 0.18/0.49 |- ~ndr1_0 \/ ~ndr1_1 a108 \/ c1_2 a108 $_156 \/ c2_2 a108 $_156 \/ % 0.18/0.49 c2_2 a130 $_155 \/ c3_0 \/ c3_2 a130 $_155 \/ c4_1 a130 \/ % 0.18/0.49 c4_2 a108 $_156 \/ definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a130 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 % 0.18/0.49 |- c1_2 a108 $_160 \/ c2_2 a108 $_160 \/ c2_2 a130 $_159 \/ c3_0 \/ % 0.18/0.49 c3_2 a130 $_159 \/ c4_1 a130 \/ c4_2 a108 $_160 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a130 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 \/ definitionFOFtoCNF_9 a108 % 0.18/0.49 |- ~c1_2 a130 $_161 \/ ~c3_1 a130 \/ ~c4_1 a110 \/ ~c5_1 a130 \/ ~ndr1_0 \/ % 0.18/0.49 ~ndr1_1 a130 \/ c1_2 a108 $_162 \/ c2_2 a108 $_162 \/ c2_2 a130 $_161 \/ % 0.18/0.49 c3_0 \/ c4_1 a130 \/ c4_2 a108 $_162 \/ definitionFOFtoCNF_10 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_5 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 \/ definitionFOFtoCNF_9 a108 % 0.18/0.49 |- ~c1_2 a130 $_161 \/ ~c3_1 a110 \/ ~c3_1 a130 \/ ~c5_1 a130 \/ ~ndr1_0 \/ % 0.18/0.49 ~ndr1_1 a130 \/ c1_2 a108 $_162 \/ c2_2 a108 $_162 \/ c2_2 a130 $_161 \/ % 0.18/0.49 c3_0 \/ c4_1 a130 \/ c4_2 a108 $_162 \/ definitionFOFtoCNF_10 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_5 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 \/ definitionFOFtoCNF_9 a108 % 0.18/0.49 |- ~c5_1 a133 \/ ~ndr1_0 \/ c1_2 a108 a131 \/ c2_0 \/ c2_2 a108 a131 \/ % 0.18/0.49 c2_2 a130 $_161 \/ c3_0 \/ c3_2 a130 $_161 \/ c4_1 a130 \/ c5_1 a108 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a130 \/ % 0.18/0.49 definitionFOFtoCNF_4 a108 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 a130 \/ % 0.18/0.49 definitionFOFtoCNF_9 a108 % 0.18/0.49 |- ~c2_1 a133 \/ ~ndr1_0 \/ c1_2 a108 a131 \/ c2_0 \/ c2_2 a108 a131 \/ % 0.18/0.49 c2_2 a130 $_161 \/ c3_0 \/ c3_2 a130 $_161 \/ c4_1 a130 \/ c5_1 a108 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a130 \/ % 0.18/0.49 definitionFOFtoCNF_4 a108 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 a130 \/ % 0.18/0.49 definitionFOFtoCNF_9 a108 % 0.18/0.49 |- ~c1_0 \/ ~c4_1 $_163 \/ ~ndr1_0 \/ c1_2 $_163 a105 \/ c1_2 a112 $_164 \/ % 0.18/0.49 c2_0 \/ c3_0 \/ c4_1 a112 \/ c4_2 $_163 a105 \/ c5_2 a112 $_164 \/ % 0.18/0.49 definitionFOFtoCNF_0 $_163 \/ definitionFOFtoCNF_3 a112 \/ % 0.18/0.49 definitionFOFtoCNF_9 $_163 % 0.18/0.49 |- c1_2 a108 $_168 \/ c2_2 a108 $_168 \/ c2_2 a130 $_167 \/ c3_0 \/ % 0.18/0.49 c3_2 a130 $_167 \/ c4_1 a108 \/ c4_1 a130 \/ c4_2 a108 $_168 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a108 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 a130 % 0.18/0.49 |- ~c1_2 a130 $_169 \/ ~c3_1 a130 \/ ~c4_1 a110 \/ ~c5_1 a130 \/ ~ndr1_0 \/ % 0.18/0.49 ~ndr1_1 a130 \/ c1_2 a108 $_170 \/ c2_2 a108 $_170 \/ c2_2 a130 $_169 \/ % 0.18/0.49 c3_0 \/ c4_1 a108 \/ c4_1 a130 \/ c4_2 a108 $_170 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a108 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_5 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 % 0.18/0.49 |- ~c1_2 a130 $_169 \/ ~c3_1 a110 \/ ~c3_1 a130 \/ ~c5_1 a130 \/ ~ndr1_0 \/ % 0.18/0.49 ~ndr1_1 a130 \/ c1_2 a108 $_170 \/ c2_2 a108 $_170 \/ c2_2 a130 $_169 \/ % 0.18/0.49 c3_0 \/ c4_1 a108 \/ c4_1 a130 \/ c4_2 a108 $_170 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a108 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_5 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 % 0.18/0.49 |- ~c3_2 a108 a104 \/ ~ndr1_1 a108 \/ c1_2 a108 a104 \/ c2_2 a108 a104 \/ % 0.18/0.49 c2_2 a130 $_169 \/ c3_0 \/ c3_2 a130 $_169 \/ c4_1 a108 \/ c4_1 a130 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a108 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 a108 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 % 0.18/0.49 |- ~c5_1 a133 \/ ~ndr1_0 \/ c1_2 a108 a131 \/ c2_0 \/ c2_2 a108 a131 \/ % 0.18/0.49 c2_2 a130 $_169 \/ c3_0 \/ c3_2 a130 $_169 \/ c4_1 a108 \/ c4_1 a130 \/ % 0.18/0.49 c5_1 a108 \/ definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a108 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_4 a108 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 % 0.18/0.49 |- ~c2_1 a133 \/ ~ndr1_0 \/ c1_2 a108 a131 \/ c2_0 \/ c2_2 a108 a131 \/ % 0.18/0.49 c2_2 a130 $_169 \/ c3_0 \/ c3_2 a130 $_169 \/ c4_1 a108 \/ c4_1 a130 \/ % 0.18/0.49 c5_1 a108 \/ definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a108 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_4 a108 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 % 0.18/0.49 |- ~c1_2 a130 $_172 \/ ~c3_1 a130 \/ ~c5_1 a130 \/ ~ndr1_0 \/ % 0.18/0.49 ~ndr1_1 a110 \/ ~ndr1_1 a130 \/ c1_2 a108 $_168 \/ c1_2 a110 $_171 \/ % 0.18/0.49 c2_2 a108 $_168 \/ c2_2 a130 $_172 \/ c3_0 \/ c4_1 a108 \/ c4_1 a130 \/ % 0.18/0.49 c4_2 a108 $_168 \/ c5_2 a110 $_171 \/ definitionFOFtoCNF_10 \/ % 0.18/0.49 definitionFOFtoCNF_3 a108 \/ definitionFOFtoCNF_3 a130 \/ % 0.18/0.49 definitionFOFtoCNF_5 \/ definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 % 0.18/0.49 |- ~c1_2 a130 $_172 \/ ~c3_1 a130 \/ ~c5_1 a130 \/ ~ndr1_0 \/ % 0.18/0.49 ~ndr1_1 a110 \/ ~ndr1_1 a130 \/ c1_2 a108 $_160 \/ c1_2 a110 $_171 \/ % 0.18/0.49 c2_2 a108 $_160 \/ c2_2 a130 $_172 \/ c3_0 \/ c4_1 a130 \/ % 0.18/0.49 c4_2 a108 $_160 \/ c5_2 a110 $_171 \/ definitionFOFtoCNF_10 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_5 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_8 a130 \/ definitionFOFtoCNF_9 a108 % 0.18/0.49 |- ~c1_0 \/ ~c4_1 $_176 \/ ~ndr1_0 \/ c1_2 $_176 a105 \/ c1_2 a112 $_177 \/ % 0.18/0.49 c3_0 \/ c4_1 a112 \/ c4_2 $_176 a105 \/ c5_2 a112 $_177 \/ % 0.18/0.49 definitionFOFtoCNF_0 $_176 \/ definitionFOFtoCNF_3 a112 \/ % 0.18/0.49 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 \/ % 0.18/0.49 definitionFOFtoCNF_9 $_176 % 0.18/0.49 |- ~ndr1_0 \/ ~ndr1_1 a108 \/ c1_2 a108 $_181 \/ c1_2 a114 $_180 \/ c2_0 \/ % 0.18/0.49 c2_2 a108 $_181 \/ c2_2 a114 $_180 \/ c3_0 \/ c3_2 a114 $_180 \/ % 0.18/0.49 c4_1 a114 \/ c4_2 a108 $_181 \/ c4_2 a114 $_180 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a114 \/ % 0.18/0.49 definitionFOFtoCNF_8 a114 % 0.18/0.49 |- c1_2 a108 $_185 \/ c1_2 a114 $_184 \/ c2_0 \/ c2_2 a108 $_185 \/ % 0.18/0.49 c2_2 a114 $_184 \/ c3_0 \/ c3_2 a114 $_184 \/ c4_1 a114 \/ % 0.18/0.49 c4_2 a108 $_185 \/ c4_2 a114 $_184 \/ definitionFOFtoCNF_10 \/ % 0.18/0.49 definitionFOFtoCNF_3 a114 \/ definitionFOFtoCNF_8 a114 \/ % 0.18/0.49 definitionFOFtoCNF_9 a108 % 0.18/0.49 |- ~c5_1 a133 \/ ~ndr1_0 \/ c1_2 a108 $_187 \/ c1_2 a114 a131 \/ c2_0 \/ % 0.18/0.49 c2_2 a108 $_187 \/ c2_2 a114 a131 \/ c3_0 \/ c3_2 a114 a131 \/ % 0.18/0.49 c4_1 a114 \/ c4_2 a108 $_187 \/ c5_1 a114 \/ definitionFOFtoCNF_10 \/ % 0.18/0.49 definitionFOFtoCNF_3 a114 \/ definitionFOFtoCNF_4 a114 \/ % 0.18/0.49 definitionFOFtoCNF_8 a114 \/ definitionFOFtoCNF_9 a108 % 0.18/0.49 |- ~c2_1 a133 \/ ~ndr1_0 \/ c1_2 a108 $_187 \/ c1_2 a114 a131 \/ c2_0 \/ % 0.18/0.49 c2_2 a108 $_187 \/ c2_2 a114 a131 \/ c3_0 \/ c3_2 a114 a131 \/ % 0.18/0.49 c4_1 a114 \/ c4_2 a108 $_187 \/ c5_1 a114 \/ definitionFOFtoCNF_10 \/ % 0.18/0.49 definitionFOFtoCNF_3 a114 \/ definitionFOFtoCNF_4 a114 \/ % 0.18/0.49 definitionFOFtoCNF_8 a114 \/ definitionFOFtoCNF_9 a108 % 0.18/0.49 |- c1_2 a108 $_193 \/ c1_2 a114 $_192 \/ c2_0 \/ c2_2 a108 $_193 \/ % 0.18/0.49 c2_2 a114 $_192 \/ c3_0 \/ c3_2 a114 $_192 \/ c4_1 a108 \/ c4_1 a114 \/ % 0.18/0.49 c4_2 a108 $_193 \/ c4_2 a114 $_192 \/ definitionFOFtoCNF_10 \/ % 0.18/0.49 definitionFOFtoCNF_3 a108 \/ definitionFOFtoCNF_3 a114 \/ % 0.18/0.49 definitionFOFtoCNF_8 a114 % 0.18/0.49 |- ~c5_1 a133 \/ ~ndr1_0 \/ c1_2 a108 $_195 \/ c1_2 a114 a131 \/ c2_0 \/ % 0.18/0.49 c2_2 a108 $_195 \/ c2_2 a114 a131 \/ c3_0 \/ c3_2 a114 a131 \/ % 0.18/0.49 c4_1 a108 \/ c4_1 a114 \/ c4_2 a108 $_195 \/ c5_1 a114 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a108 \/ % 0.18/0.49 definitionFOFtoCNF_3 a114 \/ definitionFOFtoCNF_4 a114 \/ % 0.18/0.49 definitionFOFtoCNF_8 a114 % 0.18/0.49 |- ~c2_1 a133 \/ ~ndr1_0 \/ c1_2 a108 $_195 \/ c1_2 a114 a131 \/ c2_0 \/ % 0.18/0.49 c2_2 a108 $_195 \/ c2_2 a114 a131 \/ c3_0 \/ c3_2 a114 a131 \/ % 0.18/0.49 c4_1 a108 \/ c4_1 a114 \/ c4_2 a108 $_195 \/ c5_1 a114 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a108 \/ % 0.18/0.49 definitionFOFtoCNF_3 a114 \/ definitionFOFtoCNF_4 a114 \/ % 0.18/0.49 definitionFOFtoCNF_8 a114 % 0.18/0.49 |- ~c2_0 \/ c1_2 a108 a138 \/ c2_2 a108 $_204 \/ c2_2 a108 a138 \/ % 0.18/0.49 c2_2 a130 $_205 \/ c3_0 \/ c3_2 a108 $_204 \/ c3_2 a130 $_205 \/ % 0.18/0.49 c4_1 a130 \/ c5_1 a108 \/ c5_2 a108 $_204 \/ definitionFOFtoCNF_10 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 a130 \/ % 0.18/0.49 definitionFOFtoCNF_9 a108 % 0.18/0.49 |- ~c2_0 \/ c1_2 a108 a138 \/ c2_2 a108 $_214 \/ c2_2 a108 a138 \/ % 0.18/0.49 c2_2 a130 $_215 \/ c3_0 \/ c3_2 a108 $_214 \/ c3_2 a130 $_215 \/ % 0.18/0.49 c4_1 a108 \/ c4_1 a130 \/ c5_1 a108 \/ c5_2 a108 $_214 \/ % 0.18/0.49 definitionFOFtoCNF_10 \/ definitionFOFtoCNF_3 a108 \/ % 0.18/0.49 definitionFOFtoCNF_3 a130 \/ definitionFOFtoCNF_6 \/ % 0.18/0.49 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 a130 % 0.18/0.49 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.49 %------------------------------------------------------------------------------