↑ Up

Metis---2.4.CSA-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : SYN524+1 : TPTP v8.1.0. Released v2.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n009.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:38 EDT 2022

% Result   : CounterSatisfiable 0.10s 0.32s
% Output   : Saturation 0.10s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07  % Problem  : SYN524+1 : TPTP v8.1.0. Released v2.1.0.
% 0.00/0.07  % Command  : metis --show proof --show saturation %s
% 0.07/0.26  % Computer : n009.cluster.edu
% 0.07/0.26  % Model    : x86_64 x86_64
% 0.07/0.26  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.26  % Memory   : 8042.1875MB
% 0.07/0.26  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.07/0.26  % CPULimit : 300
% 0.07/0.26  % WCLimit  : 600
% 0.07/0.26  % DateTime : Tue Jul 12 03:20:21 EDT 2022
% 0.07/0.26  % CPUTime  : 
% 0.07/0.26  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.10/0.32  % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.32  
% 0.10/0.32  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.32  |- ~c3_0 \/ c2_1 a180
% 0.10/0.32  |- ~c3_0 \/ c3_1 a180
% 0.10/0.32  |- ~c3_0 \/ ndr1_0
% 0.10/0.32  |- ~c1_2 a180 $X17 \/ ~c3_0 \/ ~c5_2 a180 $X17 \/ ~ndr1_1 a180 \/
% 0.10/0.32     c4_2 a180 $X17
% 0.10/0.32  |- ~c5_0 \/ ~c5_2 a165 a166
% 0.10/0.32  |- ~c5_0 \/ c1_1 a165
% 0.10/0.32  |- ~c5_0 \/ c1_2 a165 a166
% 0.10/0.32  |- ~c5_0 \/ c3_2 a165 a166
% 0.10/0.32  |- ~c5_0 \/ ndr1_0
% 0.10/0.32  |- ~c5_0 \/ ndr1_1 a165
% 0.10/0.32  |- ~c3_2 a165 $X2 \/ ~c5_0 \/ ~ndr1_1 a165 \/ c4_2 a165 $X2 \/
% 0.10/0.32     c5_2 a165 $X2
% 0.10/0.32  |- ~c3_1 $X24 \/ ~ndr1_0 \/ c3_0 \/ ndr1_1 $X24
% 0.10/0.32  |- ~c1_2 $X24 a186 \/ ~c2_2 $X24 a185 \/ ~c3_1 $X24 \/ ~ndr1_0 \/ c3_0
% 0.10/0.32  |- ~c1_2 $X24 a186 \/ ~c3_1 $X24 \/ ~c3_2 $X24 a185 \/ ~ndr1_0 \/ c3_0
% 0.10/0.32  |- ~c2_2 $X24 a185 \/ ~c3_1 $X24 \/ ~ndr1_0 \/ c3_0 \/ c4_2 $X24 a186
% 0.10/0.32  |- ~c3_1 $X24 \/ ~c3_2 $X24 a185 \/ ~ndr1_0 \/ c3_0 \/ c4_2 $X24 a186
% 0.10/0.32  |- ~c1_0 \/ ~c2_1 a159 \/ ~c5_2 $X $Y \/ ~ndr1_0 \/ ~ndr1_1 $X \/
% 0.10/0.32     c1_1 $X \/ c2_2 $X $Y \/ c3_1 $X
% 0.10/0.32  |- ~c1_0 \/ ~c3_1 a159 \/ ~c5_2 $X $Y \/ ~ndr1_0 \/ ~ndr1_1 $X \/
% 0.10/0.32     c1_1 $X \/ c2_2 $X $Y \/ c3_1 $X
% 0.10/0.32  |- ~c1_0 \/ ~c3_2 a159 a160 \/ ~c5_2 $X $Y \/ ~ndr1_0 \/ ~ndr1_1 $X \/
% 0.10/0.32     c1_1 $X \/ c2_2 $X $Y \/ c3_1 $X
% 0.10/0.32  |- ~c1_0 \/ ~c5_2 $X $Y \/ ~c5_2 a159 a160 \/ ~ndr1_0 \/ ~ndr1_1 $X \/
% 0.10/0.32     c1_1 $X \/ c2_2 $X $Y \/ c3_1 $X
% 0.10/0.32  |- ~c1_0 \/ ~c5_2 $X $Y \/ ~ndr1_0 \/ ~ndr1_1 $X \/ c1_1 $X \/
% 0.10/0.32     c2_2 $X $Y \/ c3_1 $X \/ ndr1_1 a159
% 0.10/0.32  |- ~c2_0 \/ ~c3_0 \/ ~c4_2 a178 a179
% 0.10/0.32  |- ~c2_0 \/ ~c3_0 \/ c4_1 a178
% 0.10/0.32  |- ~c2_0 \/ ~c3_0 \/ c5_2 a178 a179
% 0.10/0.32  |- ~c2_0 \/ ~c3_0 \/ ndr1_1 a178
% 0.10/0.32  |- ~c2_0 \/ ~c3_0 \/ ~ndr1_1 a178 \/ c3_2 a178 $X15 \/ c4_2 a178 $X15
% 0.10/0.32  |- ~c2_0 \/ ~c3_0 \/ ~c3_1 $X16 \/ ~c4_1 $X16 \/ ~c5_1 $X16 \/ ~ndr1_0
% 0.10/0.32  |- ~c2_0 \/ ~c2_1 $X3 \/ ~c5_1 $X3 \/ ~ndr1_0 \/ c1_1 $X3 \/ c2_2 a167 a168
% 0.10/0.32  |- ~c2_0 \/ ~c2_1 $X3 \/ ~c5_1 $X3 \/ ~ndr1_0 \/ c1_1 $X3 \/ c3_2 a167 a168
% 0.10/0.32  |- ~c2_0 \/ ~c2_1 $X3 \/ ~c5_1 $X3 \/ ~ndr1_0 \/ c1_1 $X3 \/ c4_2 a167 a168
% 0.10/0.32  |- ~c2_0 \/ ~c2_1 $X3 \/ ~c5_1 $X3 \/ ~ndr1_0 \/ c1_1 $X3 \/ ndr1_1 a167
% 0.10/0.32  |- ~c1_2 a167 $X5 \/ ~c2_0 \/ ~c2_1 $X3 \/ ~c3_2 a167 $X5 \/ ~c5_1 $X3 \/
% 0.10/0.32     ~ndr1_0 \/ ~ndr1_1 a167 \/ c1_1 $X3
% 0.10/0.32  |- ~c1_2 a167 $X4 \/ ~c2_0 \/ ~c2_1 $X3 \/ ~c2_2 a167 $X4 \/ ~c5_1 $X3 \/
% 0.10/0.32     ~ndr1_0 \/ ~ndr1_1 a167 \/ c1_1 $X3 \/ c4_2 a167 $X4
% 0.10/0.32  |- ~c4_0 \/ c2_0 \/ c3_0
% 0.10/0.32  |- ~c1_2 $X11 a174 \/ ~definitionFOFtoCNF_0 $X11
% 0.10/0.32  |- ~c2_2 $X11 a174 \/ ~definitionFOFtoCNF_0 $X11
% 0.10/0.32  |- ~c5_2 $X11 a174 \/ ~definitionFOFtoCNF_0 $X11
% 0.10/0.32  |- ~definitionFOFtoCNF_0 $X11 \/ ndr1_1 $X11
% 0.10/0.32  |- ~ndr1_1 $X11 \/ c1_2 $X11 a174 \/ c2_2 $X11 a174 \/ c5_2 $X11 a174 \/
% 0.10/0.32     definitionFOFtoCNF_0 $X11
% 0.10/0.32  |- ~c3_1 $X11 \/ ~c4_0 \/ ~ndr1_0 \/ c1_1 $X11 \/ c1_1 a175 \/
% 0.10/0.32     definitionFOFtoCNF_0 $X11
% 0.10/0.32  |- ~c3_1 $X11 \/ ~c4_0 \/ ~ndr1_0 \/ c1_1 $X11 \/ c2_1 a175 \/
% 0.10/0.32     definitionFOFtoCNF_0 $X11
% 0.10/0.32  |- ~c3_1 $X11 \/ ~c3_2 a175 $X12 \/ ~c4_0 \/ ~ndr1_0 \/ ~ndr1_1 a175 \/
% 0.10/0.32     c1_1 $X11 \/ c2_2 a175 $X12 \/ c4_2 a175 $X12 \/
% 0.10/0.32     definitionFOFtoCNF_0 $X11
% 0.10/0.32  |- ~c5_2 a183 a184 \/ c1_0 \/ c5_0
% 0.10/0.32  |- c1_0 \/ c1_2 a183 a184 \/ c5_0
% 0.10/0.32  |- c1_0 \/ c2_1 a183 \/ c5_0
% 0.10/0.32  |- c1_0 \/ c5_0 \/ ndr1_0
% 0.10/0.32  |- c1_0 \/ c5_0 \/ ndr1_1 a183
% 0.10/0.32  |- ~c3_2 $U a157 \/ ~definitionFOFtoCNF_1 $U
% 0.10/0.32  |- ~definitionFOFtoCNF_1 $U \/ c2_2 $U a157
% 0.10/0.32  |- ~definitionFOFtoCNF_1 $U \/ ndr1_1 $U
% 0.10/0.32  |- ~c2_2 $U a157 \/ ~ndr1_1 $U \/ c3_2 $U a157 \/ definitionFOFtoCNF_1 $U
% 0.10/0.32  |- ~c5_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_0 \/ c1_2 $U $V \/ c3_1 a158 \/
% 0.10/0.32     c5_2 $U $V \/ definitionFOFtoCNF_1 $U
% 0.10/0.32  |- ~c5_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_0 \/ c1_2 $U $V \/ c5_1 a158 \/
% 0.10/0.32     c5_2 $U $V \/ definitionFOFtoCNF_1 $U
% 0.10/0.32  |- ~c5_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ndr1_1 a158 \/ c1_0 \/
% 0.10/0.32     c1_2 $U $V \/ c1_2 a158 $W \/ c4_2 a158 $W \/ c5_2 $U $V \/
% 0.10/0.32     c5_2 a158 $W \/ definitionFOFtoCNF_1 $U
% 0.10/0.32  |- ~c4_1 a181 \/ c2_0 \/ c4_0
% 0.10/0.32  |- c1_1 a181 \/ c2_0 \/ c4_0
% 0.10/0.32  |- c2_0 \/ c4_0 \/ ndr1_0
% 0.10/0.32  |- ~c1_2 a181 $X18 \/ ~ndr1_1 a181 \/ c2_0 \/ c3_2 a181 $X18 \/ c4_0 \/
% 0.10/0.32     c5_2 a181 $X18
% 0.10/0.32  |- ~c4_2 $X14 a176 \/ ~definitionFOFtoCNF_2 $X14
% 0.10/0.32  |- ~definitionFOFtoCNF_2 $X14 \/ c2_2 $X14 a176
% 0.10/0.32  |- ~definitionFOFtoCNF_2 $X14 \/ ndr1_1 $X14
% 0.10/0.32  |- ~c2_2 $X14 a176 \/ ~ndr1_1 $X14 \/ c4_2 $X14 a176 \/
% 0.10/0.32     definitionFOFtoCNF_2 $X14
% 0.10/0.32  |- ~c1_1 $X14 \/ ~c2_1 $X13 \/ ~c5_1 $X13 \/ ~ndr1_0 \/ c2_2 $X14 a177 \/
% 0.10/0.32     c3_0 \/ c4_1 $X13 \/ definitionFOFtoCNF_2 $X14
% 0.10/0.32  |- ~c1_1 $X14 \/ ~c2_1 $X13 \/ ~c5_1 $X13 \/ ~ndr1_0 \/ c3_0 \/
% 0.10/0.32     c3_2 $X14 a177 \/ c4_1 $X13 \/ definitionFOFtoCNF_2 $X14
% 0.10/0.32  |- ~c1_1 $X14 \/ ~c2_1 $X13 \/ ~c5_1 $X13 \/ ~ndr1_0 \/ c3_0 \/
% 0.10/0.32     c4_1 $X13 \/ c4_2 $X14 a177 \/ definitionFOFtoCNF_2 $X14
% 0.10/0.32  |- ~c1_1 $X14 \/ ~c2_1 $X13 \/ ~c5_1 $X13 \/ ~ndr1_0 \/ c3_0 \/
% 0.10/0.32     c4_1 $X13 \/ definitionFOFtoCNF_2 $X14 \/ ndr1_1 $X14
% 0.10/0.32  |- ~c1_1 $X19 \/ ~c1_2 $X19 $X20 \/ ~c2_2 $X21 a182 \/ ~c3_2 $X19 $X20 \/
% 0.10/0.32     ~c3_2 $X21 $X22 \/ ~c4_1 $X19 \/ ~c4_2 $X19 $X20 \/ ~ndr1_0 \/
% 0.10/0.32     ~ndr1_1 $X19 \/ ~ndr1_1 $X21 \/ c1_1 $X21 \/ c1_2 $X21 $X22 \/
% 0.10/0.32     c2_2 $X21 $X22 \/ c3_0
% 0.10/0.32  |- ~c1_1 $X19 \/ ~c1_2 $X19 $X20 \/ ~c3_2 $X19 $X20 \/ ~c3_2 $X21 $X22 \/
% 0.10/0.32     ~c3_2 $X21 a182 \/ ~c4_1 $X19 \/ ~c4_2 $X19 $X20 \/ ~ndr1_0 \/
% 0.10/0.32     ~ndr1_1 $X19 \/ ~ndr1_1 $X21 \/ c1_1 $X21 \/ c1_2 $X21 $X22 \/
% 0.10/0.32     c2_2 $X21 $X22 \/ c3_0
% 0.10/0.32  |- ~c1_1 $X19 \/ ~c1_2 $X19 $X20 \/ ~c3_2 $X19 $X20 \/ ~c3_2 $X21 $X22 \/
% 0.10/0.32     ~c4_1 $X19 \/ ~c4_2 $X19 $X20 \/ ~ndr1_0 \/ ~ndr1_1 $X19 \/
% 0.10/0.32     ~ndr1_1 $X21 \/ c1_1 $X21 \/ c1_2 $X21 $X22 \/ c2_2 $X21 $X22 \/ c3_0 \/
% 0.10/0.32     c5_2 $X21 a182
% 0.10/0.32  |- ~c1_1 a170 \/ ~definitionFOFtoCNF_3
% 0.10/0.32  |- ~c3_1 a170 \/ ~definitionFOFtoCNF_3
% 0.10/0.32  |- ~definitionFOFtoCNF_3 \/ ndr1_0
% 0.10/0.32  |- ~ndr1_0 \/ c1_1 a170 \/ c3_1 a170 \/ definitionFOFtoCNF_3
% 0.10/0.32  |- ~definitionFOFtoCNF_4 \/ c3_1 a169
% 0.10/0.32  |- ~definitionFOFtoCNF_4 \/ ndr1_0
% 0.10/0.32  |- ~c3_1 a169 \/ ~ndr1_0 \/ definitionFOFtoCNF_4
% 0.10/0.32  |- ~c1_2 a171 a172 \/ definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.32  |- ~c4_1 a171 \/ definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.32  |- c3_2 a171 a172 \/ definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.32  |- definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4 \/ ndr1_0
% 0.10/0.32  |- definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4 \/ ndr1_1 a171
% 0.10/0.32  |- ~c4_2 a171 $X7 \/ ~c5_2 a171 $X7 \/ ~ndr1_1 a171 \/
% 0.10/0.32     definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.32  |- ~c1_2 a171 a172 \/ ~ndr1_1 a169 \/ c2_2 a169 $X6 \/ c3_2 a169 $X6 \/
% 0.10/0.32     c5_2 a169 $X6 \/ definitionFOFtoCNF_3
% 0.10/0.32  |- ~c4_1 a171 \/ ~ndr1_1 a169 \/ c2_2 a169 $X6 \/ c3_2 a169 $X6 \/
% 0.10/0.32     c5_2 a169 $X6 \/ definitionFOFtoCNF_3
% 0.10/0.32  |- ~ndr1_1 a169 \/ c2_2 a169 $X6 \/ c3_2 a169 $X6 \/ c3_2 a171 a172 \/
% 0.10/0.32     c5_2 a169 $X6 \/ definitionFOFtoCNF_3
% 0.10/0.32  |- ~ndr1_1 a169 \/ c2_2 a169 $X6 \/ c3_2 a169 $X6 \/ c5_2 a169 $X6 \/
% 0.10/0.32     definitionFOFtoCNF_3 \/ ndr1_0
% 0.10/0.32  |- ~ndr1_1 a169 \/ c2_2 a169 $X6 \/ c3_2 a169 $X6 \/ c5_2 a169 $X6 \/
% 0.10/0.32     definitionFOFtoCNF_3 \/ ndr1_1 a171
% 0.10/0.32  |- ~c4_2 a171 $X7 \/ ~c5_2 a171 $X7 \/ ~ndr1_1 a169 \/ ~ndr1_1 a171 \/
% 0.10/0.32     c2_2 a169 $X6 \/ c3_2 a169 $X6 \/ c5_2 a169 $X6 \/ definitionFOFtoCNF_3
% 0.10/0.32  |- ~c1_2 a163 a164 \/ ~definitionFOFtoCNF_5
% 0.10/0.32  |- ~c2_1 a163 \/ ~definitionFOFtoCNF_5
% 0.10/0.32  |- ~c3_2 a163 a164 \/ ~definitionFOFtoCNF_5
% 0.10/0.32  |- ~definitionFOFtoCNF_5 \/ c3_1 a163
% 0.10/0.32  |- ~definitionFOFtoCNF_5 \/ c5_2 a163 a164
% 0.10/0.32  |- ~definitionFOFtoCNF_5 \/ ndr1_0
% 0.10/0.32  |- ~definitionFOFtoCNF_5 \/ ndr1_1 a163
% 0.10/0.32  |- ~c3_1 a163 \/ ~c5_2 a163 a164 \/ ~ndr1_0 \/ ~ndr1_1 a163 \/
% 0.10/0.32     c1_2 a163 a164 \/ c2_1 a163 \/ c3_2 a163 a164 \/ definitionFOFtoCNF_5
% 0.10/0.32  |- ~c1_2 $Z $X1 \/ ~c3_1 a161 \/ ~c4_2 $Z $X1 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/
% 0.10/0.32     c1_1 $Z \/ c2_1 $Z \/ definitionFOFtoCNF_5
% 0.10/0.32  |- ~c1_2 $Z $X1 \/ ~c4_2 $Z $X1 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/
% 0.10/0.32     c1_2 a161 a162 \/ c2_1 $Z \/ definitionFOFtoCNF_5
% 0.10/0.32  |- ~c1_2 $Z $X1 \/ ~c4_2 $Z $X1 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/
% 0.10/0.32     c2_1 $Z \/ c3_2 a161 a162 \/ definitionFOFtoCNF_5
% 0.10/0.32  |- ~c1_2 $Z $X1 \/ ~c4_2 $Z $X1 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/
% 0.10/0.32     c2_1 $Z \/ c4_1 a161 \/ definitionFOFtoCNF_5
% 0.10/0.32  |- ~c1_2 $Z $X1 \/ ~c4_2 $Z $X1 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/
% 0.10/0.32     c2_1 $Z \/ c5_2 a161 a162 \/ definitionFOFtoCNF_5
% 0.10/0.32  |- ~c1_2 $Z $X1 \/ ~c4_2 $Z $X1 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/
% 0.10/0.32     c2_1 $Z \/ definitionFOFtoCNF_5 \/ ndr1_1 a161
% 0.10/0.32  |- ~c2_1 $X9 \/ ~c3_2 $X8 a173 \/ ~c5_0 \/ ~c5_1 $X9 \/ ~ndr1_0 \/
% 0.10/0.32     ~ndr1_1 $X9 \/ c2_2 $X9 $X10 \/ c4_2 $X9 $X10 \/ c5_2 $X9 $X10
% 0.10/0.32  |- ~c2_1 $X9 \/ ~c5_0 \/ ~c5_1 $X9 \/ ~c5_2 $X8 a173 \/ ~ndr1_0 \/
% 0.10/0.32     ~ndr1_1 $X9 \/ c2_2 $X9 $X10 \/ c4_2 $X9 $X10 \/ c5_2 $X9 $X10
% 0.10/0.32  |- ~c2_1 $X9 \/ ~c5_0 \/ ~c5_1 $X9 \/ ~ndr1_0 \/ ~ndr1_1 $X9 \/
% 0.10/0.32     c2_2 $X9 $X10 \/ c4_2 $X9 $X10 \/ c5_2 $X9 $X10 \/ ndr1_1 $X8
% 0.10/0.32  |- ~c2_1 $X25 \/ ~c5_2 $X25 a187 \/ ~ndr1_0
% 0.10/0.32  |- ~c2_1 $X25 \/ ~ndr1_0 \/ c1_2 $X25 a187
% 0.10/0.32  |- ~c2_1 $X25 \/ ~ndr1_0 \/ c2_2 $X25 a187
% 0.10/0.32  |- ~c2_1 $X25 \/ ~ndr1_0 \/ ndr1_1 $X25
% 0.10/0.32  |- ~c1_0 \/ ~c5_2 a159 a160 \/ ~ndr1_0 \/ ~ndr1_1 a159 \/ c1_1 a159 \/
% 0.10/0.32     c2_2 a159 a160 \/ c3_1 a159
% 0.10/0.32  |- ~c5_1 a158 \/ ~ndr1_0 \/ ~ndr1_1 a158 \/ c1_0 \/ c1_2 a158 $V \/
% 0.10/0.32     c1_2 a158 $W \/ c4_2 a158 $W \/ c5_2 a158 $V \/ c5_2 a158 $W \/
% 0.10/0.32     definitionFOFtoCNF_1 a158
% 0.10/0.32  |- ~c1_1 $X19 \/ ~c1_2 $X19 $X20 \/ ~c3_2 $X19 $X20 \/ ~c3_2 $X21 a182 \/
% 0.10/0.32     ~c4_1 $X19 \/ ~c4_2 $X19 $X20 \/ ~ndr1_0 \/ ~ndr1_1 $X19 \/
% 0.10/0.32     ~ndr1_1 $X21 \/ c1_1 $X21 \/ c1_2 $X21 a182 \/ c2_2 $X21 a182 \/ c3_0
% 0.10/0.32  |- c1_1 a170 \/ c3_1 a170 \/ definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.32  |- c1_1 a170 \/ c2_0 \/ c3_1 a170 \/ c4_0 \/ definitionFOFtoCNF_3
% 0.10/0.32  |- c1_0 \/ c1_1 a170 \/ c3_1 a170 \/ c5_0 \/ definitionFOFtoCNF_3
% 0.10/0.32  |- c1_0 \/ c1_2 a183 a187 \/ c5_0
% 0.10/0.32  |- c1_0 \/ c2_2 a183 a187 \/ c5_0
% 0.10/0.32  |- c1_1 a170 \/ c3_0 \/ definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4 \/
% 0.10/0.32     ndr1_1 a170
% 0.10/0.32  |- c1_0 \/ c1_1 a170 \/ c3_0 \/ c5_0 \/ definitionFOFtoCNF_3 \/ ndr1_1 a170
% 0.10/0.32  |- c1_1 a170 \/ c2_0 \/ c3_0 \/ c4_0 \/ definitionFOFtoCNF_3 \/ ndr1_1 a170
% 0.10/0.32  |- c1_0 \/ c2_2 a183 $_22 \/ c3_2 a183 $_22 \/ c5_0
% 0.10/0.32  |- ~c1_2 a183 a186 \/ ~c3_1 a183 \/ ~ndr1_0 \/ c1_0 \/ c2_2 a183 a185 \/
% 0.10/0.32     c3_0 \/ c5_0
% 0.10/0.32  |- ~c3_1 a183 \/ ~ndr1_0 \/ c1_0 \/ c2_2 a183 a185 \/ c3_0 \/
% 0.10/0.32     c4_2 a183 a186 \/ c5_0
% 0.10/0.32  |- ~c4_0 \/ c1_1 a170 \/ c1_1 a175 \/ definitionFOFtoCNF_0 a170 \/
% 0.10/0.32     definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.32  |- ~c4_0 \/ c1_0 \/ c1_1 a170 \/ c1_1 a175 \/ c5_0 \/
% 0.10/0.32     definitionFOFtoCNF_0 a170 \/ definitionFOFtoCNF_3
% 0.10/0.32  |- ~c4_0 \/ c1_1 a170 \/ c2_1 a175 \/ definitionFOFtoCNF_0 a170 \/
% 0.10/0.32     definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.32  |- ~c4_0 \/ c1_0 \/ c1_1 a170 \/ c2_1 a175 \/ c5_0 \/
% 0.10/0.32     definitionFOFtoCNF_0 a170 \/ definitionFOFtoCNF_3
% 0.10/0.32  |- c1_1 a170 \/ c1_2 a170 a174 \/ c2_0 \/ c2_2 a170 a174 \/ c3_0 \/ c4_0 \/
% 0.10/0.32     c5_2 a170 a174 \/ definitionFOFtoCNF_0 a170 \/ definitionFOFtoCNF_3
% 0.10/0.32  |- c1_0 \/ c1_1 a170 \/ c1_2 a170 a174 \/ c2_2 a170 a174 \/ c3_0 \/ c5_0 \/
% 0.10/0.32     c5_2 a170 a174 \/ definitionFOFtoCNF_0 a170 \/ definitionFOFtoCNF_3
% 0.10/0.32  |- c1_1 a170 \/ c1_2 a170 a174 \/ c2_2 a170 a174 \/ c3_0 \/
% 0.10/0.32     c5_2 a170 a174 \/ definitionFOFtoCNF_0 a170 \/ definitionFOFtoCNF_3 \/
% 0.10/0.32     definitionFOFtoCNF_4
% 0.10/0.33  |- c1_2 a171 a174 \/ c2_2 a171 a174 \/ c5_2 a171 a174 \/
% 0.10/0.33     definitionFOFtoCNF_0 a171 \/ definitionFOFtoCNF_3 \/
% 0.10/0.33     definitionFOFtoCNF_4
% 0.10/0.33  |- c1_0 \/ c1_2 a183 a174 \/ c2_2 a183 a174 \/ c5_0 \/ c5_2 a183 a174 \/
% 0.10/0.33     definitionFOFtoCNF_0 a183
% 0.10/0.33  |- ~c4_2 a171 a174 \/ ~ndr1_1 a171 \/ c1_2 a171 a174 \/ c2_2 a171 a174 \/
% 0.10/0.33     definitionFOFtoCNF_0 a171 \/ definitionFOFtoCNF_3 \/
% 0.10/0.33     definitionFOFtoCNF_4
% 0.10/0.33  |- ~c1_0 \/ ~c2_1 a159 \/ ~ndr1_0 \/ c1_1 a171 \/ c1_2 a171 a174 \/
% 0.10/0.33     c2_2 a171 a174 \/ c3_1 a171 \/ definitionFOFtoCNF_0 a171 \/
% 0.10/0.33     definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.33  |- ~c1_0 \/ ~c3_1 a159 \/ ~ndr1_0 \/ c1_1 a171 \/ c1_2 a171 a174 \/
% 0.10/0.33     c2_2 a171 a174 \/ c3_1 a171 \/ definitionFOFtoCNF_0 a171 \/
% 0.10/0.33     definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.33  |- ~c1_0 \/ c1_1 a171 \/ c1_2 a171 a174 \/ c2_2 a171 a174 \/ c3_1 a171 \/
% 0.10/0.33     definitionFOFtoCNF_0 a171 \/ definitionFOFtoCNF_3 \/
% 0.10/0.33     definitionFOFtoCNF_4 \/ ndr1_1 a159
% 0.10/0.33  |- ~c5_1 a170 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a170 \/ c1_2 a170 $_58 \/ c2_0 \/
% 0.10/0.33     c3_0 \/ c3_1 a158 \/ c4_0 \/ c5_2 a170 $_58 \/
% 0.10/0.33     definitionFOFtoCNF_1 a170 \/ definitionFOFtoCNF_3
% 0.10/0.33  |- ~c5_1 a170 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a170 \/ c1_2 a170 $_58 \/ c3_0 \/
% 0.10/0.33     c3_1 a158 \/ c5_0 \/ c5_2 a170 $_58 \/ definitionFOFtoCNF_1 a170 \/
% 0.10/0.33     definitionFOFtoCNF_3
% 0.10/0.33  |- ~c5_1 a170 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a170 \/ c1_2 a170 $_58 \/ c3_0 \/
% 0.10/0.33     c3_1 a158 \/ c5_2 a170 $_58 \/ definitionFOFtoCNF_1 a170 \/
% 0.10/0.33     definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.33  |- ~c5_1 a171 \/ ~ndr1_0 \/ c1_0 \/ c1_2 a171 $_58 \/ c3_1 a158 \/
% 0.10/0.33     c5_2 a171 $_58 \/ definitionFOFtoCNF_1 a171 \/ definitionFOFtoCNF_3 \/
% 0.10/0.33     definitionFOFtoCNF_4
% 0.10/0.33  |- ~c5_1 a183 \/ ~ndr1_0 \/ c1_0 \/ c1_2 a183 $_58 \/ c3_1 a158 \/ c5_0 \/
% 0.10/0.33     c5_2 a183 $_58 \/ definitionFOFtoCNF_1 a183
% 0.10/0.33  |- ~c5_1 a170 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a170 \/ c1_2 a170 $_61 \/ c2_0 \/
% 0.10/0.33     c3_0 \/ c4_0 \/ c5_1 a158 \/ c5_2 a170 $_61 \/
% 0.10/0.33     definitionFOFtoCNF_1 a170 \/ definitionFOFtoCNF_3
% 0.10/0.33  |- ~c5_1 a170 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a170 \/ c1_2 a170 $_61 \/ c3_0 \/
% 0.10/0.33     c5_0 \/ c5_1 a158 \/ c5_2 a170 $_61 \/ definitionFOFtoCNF_1 a170 \/
% 0.10/0.33     definitionFOFtoCNF_3
% 0.10/0.33  |- ~c5_1 a170 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a170 \/ c1_2 a170 $_61 \/ c3_0 \/
% 0.10/0.33     c5_1 a158 \/ c5_2 a170 $_61 \/ definitionFOFtoCNF_1 a170 \/
% 0.10/0.33     definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.33  |- ~c5_1 a171 \/ ~ndr1_0 \/ c1_0 \/ c1_2 a171 $_61 \/ c5_1 a158 \/
% 0.10/0.33     c5_2 a171 $_61 \/ definitionFOFtoCNF_1 a171 \/ definitionFOFtoCNF_3 \/
% 0.10/0.33     definitionFOFtoCNF_4
% 0.10/0.33  |- ~c5_1 a183 \/ ~ndr1_0 \/ c1_0 \/ c1_2 a183 $_61 \/ c5_0 \/ c5_1 a158 \/
% 0.10/0.33     c5_2 a183 $_61 \/ definitionFOFtoCNF_1 a183
% 0.10/0.33  |- ~c1_0 \/ ~c3_2 a159 a160 \/ ~ndr1_0 \/ ~ndr1_1 a171 \/ c1_1 a171 \/
% 0.10/0.33     c1_2 a171 a174 \/ c2_2 a171 a174 \/ c3_1 a171 \/
% 0.10/0.33     definitionFOFtoCNF_0 a171 \/ definitionFOFtoCNF_3 \/
% 0.10/0.33     definitionFOFtoCNF_4
% 0.10/0.33  |- ~c1_0 \/ ~c5_2 a159 a160 \/ ~ndr1_0 \/ ~ndr1_1 a171 \/ c1_1 a171 \/
% 0.10/0.33     c1_2 a171 a174 \/ c2_2 a171 a174 \/ c3_1 a171 \/
% 0.10/0.33     definitionFOFtoCNF_0 a171 \/ definitionFOFtoCNF_3 \/
% 0.10/0.33     definitionFOFtoCNF_4
% 0.10/0.33  |- ~c2_1 a170 \/ ~c5_0 \/ ~c5_1 a170 \/ ~ndr1_0 \/ c1_1 a170 \/ c2_0 \/
% 0.10/0.33     c2_2 a170 $_93 \/ c3_0 \/ c4_0 \/ c4_2 a170 $_93 \/ c5_2 a170 $_93 \/
% 0.10/0.33     definitionFOFtoCNF_3 \/ ndr1_1 $_94
% 0.10/0.33  |- ~c2_1 a170 \/ ~c5_0 \/ ~c5_1 a170 \/ ~ndr1_0 \/ c1_1 a170 \/
% 0.10/0.33     c2_2 a170 $_93 \/ c3_0 \/ c4_2 a170 $_93 \/ c5_2 a170 $_93 \/
% 0.10/0.33     definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4 \/ ndr1_1 $_94
% 0.10/0.33  |- ~c2_1 a171 \/ ~c5_0 \/ ~c5_1 a171 \/ ~ndr1_0 \/ c2_2 a171 $_93 \/
% 0.10/0.33     c4_2 a171 $_93 \/ c5_2 a171 $_93 \/ definitionFOFtoCNF_3 \/
% 0.10/0.33     definitionFOFtoCNF_4 \/ ndr1_1 $_94
% 0.10/0.33  |- ~c5_1 a170 \/ ~ndr1_0 \/ ~ndr1_1 a158 \/ c1_0 \/ c1_1 a170 \/
% 0.10/0.33     c1_2 a158 $_110 \/ c1_2 a170 $_109 \/ c2_0 \/ c3_0 \/ c4_0 \/
% 0.10/0.33     c4_2 a158 $_110 \/ c5_2 a158 $_110 \/ c5_2 a170 $_109 \/
% 0.10/0.33     definitionFOFtoCNF_1 a170 \/ definitionFOFtoCNF_3
% 0.10/0.33  |- ~c5_1 a170 \/ ~ndr1_0 \/ ~ndr1_1 a158 \/ c1_0 \/ c1_1 a170 \/
% 0.10/0.33     c1_2 a158 $_110 \/ c1_2 a170 $_109 \/ c3_0 \/ c4_2 a158 $_110 \/ c5_0 \/
% 0.10/0.33     c5_2 a158 $_110 \/ c5_2 a170 $_109 \/ definitionFOFtoCNF_1 a170 \/
% 0.10/0.33     definitionFOFtoCNF_3
% 0.10/0.33  |- ~c5_1 a170 \/ ~ndr1_0 \/ ~ndr1_1 a158 \/ c1_0 \/ c1_1 a170 \/
% 0.10/0.33     c1_2 a158 $_110 \/ c1_2 a170 $_109 \/ c3_0 \/ c4_2 a158 $_110 \/
% 0.10/0.33     c5_2 a158 $_110 \/ c5_2 a170 $_109 \/ definitionFOFtoCNF_1 a170 \/
% 0.10/0.33     definitionFOFtoCNF_3 \/ definitionFOFtoCNF_4
% 0.10/0.33  |- ~c5_1 a171 \/ ~ndr1_0 \/ ~ndr1_1 a158 \/ c1_0 \/ c1_2 a158 $_110 \/
% 0.10/0.33     c1_2 a171 $_109 \/ c4_2 a158 $_110 \/ c5_2 a158 $_110 \/
% 0.10/0.33     c5_2 a171 $_109 \/ definitionFOFtoCNF_1 a171 \/ definitionFOFtoCNF_3 \/
% 0.10/0.33     definitionFOFtoCNF_4
% 0.10/0.33  |- ~c5_1 a183 \/ ~ndr1_0 \/ ~ndr1_1 a158 \/ c1_0 \/ c1_2 a158 $_110 \/
% 0.10/0.33     c1_2 a183 $_109 \/ c4_2 a158 $_110 \/ c5_0 \/ c5_2 a158 $_110 \/
% 0.10/0.33     c5_2 a183 $_109 \/ definitionFOFtoCNF_1 a183
% 0.10/0.33  |- ~c1_1 $_126 \/ ~c1_2 $_126 $_127 \/ ~c2_2 a183 a182 \/
% 0.10/0.33     ~c3_2 $_126 $_127 \/ ~c4_1 $_126 \/ ~c4_2 $_126 $_127 \/ ~ndr1_0 \/
% 0.10/0.33     ~ndr1_1 $_126 \/ ~ndr1_1 a183 \/ c1_0 \/ c1_1 a183 \/ c1_2 a183 $_129 \/
% 0.10/0.33     c2_2 a183 $_129 \/ c3_0 \/ c5_0
% 0.10/0.33  |- ~c1_1 $_133 \/ ~c1_2 $_133 $_134 \/ ~c3_2 $_133 $_134 \/
% 0.10/0.33     ~c3_2 a183 a182 \/ ~c4_1 $_133 \/ ~c4_2 $_133 $_134 \/ ~ndr1_0 \/
% 0.10/0.33     ~ndr1_1 $_133 \/ ~ndr1_1 a183 \/ c1_0 \/ c1_1 a183 \/ c1_2 a183 $_136 \/
% 0.10/0.33     c2_2 a183 $_136 \/ c3_0 \/ c5_0
% 0.10/0.33  |- ~c1_1 $_140 \/ ~c1_2 $_140 $_141 \/ ~c3_2 $_140 $_141 \/ ~c4_1 $_140 \/
% 0.10/0.33     ~c4_2 $_140 $_141 \/ ~ndr1_0 \/ ~ndr1_1 $_140 \/ ~ndr1_1 a183 \/ c1_0 \/
% 0.10/0.33     c1_1 a183 \/ c1_2 a183 $_143 \/ c2_2 a183 $_143 \/ c3_0 \/ c5_0 \/
% 0.10/0.33     c5_2 a183 a182
% 0.10/0.33  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.33  
%------------------------------------------------------------------------------