↑ Up

Metis---2.4.CSA-Sat.s

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

% Computer : n014.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:41 EDT 2022

% Result   : CounterSatisfiable 0.47s 0.69s
% Output   : Saturation 0.47s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SYN528+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 : n014.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:36:34 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 0.12/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.47/0.69  % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.47/0.69  
% 0.47/0.69  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.47/0.69  |- c4_0
% 0.47/0.69  |- ~c2_2 $X19 a306 \/ ~definitionFOFtoCNF_0 $X19
% 0.47/0.69  |- ~definitionFOFtoCNF_0 $X19 \/ c4_2 $X19 a306
% 0.47/0.69  |- ~definitionFOFtoCNF_0 $X19 \/ ndr1_1 $X19
% 0.47/0.69  |- ~c4_2 $X19 a306 \/ ~ndr1_1 $X19 \/ c2_2 $X19 a306 \/
% 0.47/0.69     definitionFOFtoCNF_0 $X19
% 0.47/0.69  |- ~c3_0 \/ ~c4_1 $X19 \/ ~ndr1_0 \/ c3_2 $X19 a305 \/
% 0.47/0.69     definitionFOFtoCNF_0 $X19
% 0.47/0.69  |- ~c3_0 \/ ~c4_1 $X19 \/ ~ndr1_0 \/ c4_2 $X19 a305 \/
% 0.47/0.69     definitionFOFtoCNF_0 $X19
% 0.47/0.69  |- ~c3_0 \/ ~c4_1 $X19 \/ ~ndr1_0 \/ c5_2 $X19 a305 \/
% 0.47/0.69     definitionFOFtoCNF_0 $X19
% 0.47/0.69  |- ~c3_0 \/ ~c4_1 $X19 \/ ~ndr1_0 \/ definitionFOFtoCNF_0 $X19 \/
% 0.47/0.69     ndr1_1 $X19
% 0.47/0.69  |- ~c4_2 $X6 a290 \/ ~definitionFOFtoCNF_1 $X6
% 0.47/0.69  |- ~c5_2 $X6 a290 \/ ~definitionFOFtoCNF_1 $X6
% 0.47/0.69  |- ~definitionFOFtoCNF_1 $X6 \/ ndr1_1 $X6
% 0.47/0.69  |- ~ndr1_1 $X6 \/ c4_2 $X6 a290 \/ c5_2 $X6 a290 \/
% 0.47/0.69     definitionFOFtoCNF_1 $X6
% 0.47/0.69  |- ~c2_2 $X6 a289 \/ ~ndr1_0 \/ c1_0 \/ definitionFOFtoCNF_1 $X6
% 0.47/0.69  |- ~c5_2 $X6 a289 \/ ~ndr1_0 \/ c1_0 \/ definitionFOFtoCNF_1 $X6
% 0.47/0.69  |- ~c1_1 $X1 \/ ~c2_2 $X1 $X2 \/ ~c2_2 a281 a282 \/ ~c4_1 $X1 \/
% 0.47/0.69     ~c4_2 $X1 $X2 \/ ~ndr1_0 \/ ~ndr1_1 $X1
% 0.47/0.69  |- ~c1_1 $X1 \/ ~c2_2 $X1 $X2 \/ ~c4_1 $X1 \/ ~c4_1 a281 \/
% 0.47/0.69     ~c4_2 $X1 $X2 \/ ~ndr1_0 \/ ~ndr1_1 $X1
% 0.47/0.69  |- ~c1_1 $X1 \/ ~c2_2 $X1 $X2 \/ ~c4_1 $X1 \/ ~c4_2 $X1 $X2 \/
% 0.47/0.69     ~c5_2 a281 a282 \/ ~ndr1_0 \/ ~ndr1_1 $X1
% 0.47/0.69  |- ~c1_1 $X1 \/ ~c2_2 $X1 $X2 \/ ~c4_1 $X1 \/ ~c4_2 $X1 $X2 \/ ~ndr1_0 \/
% 0.47/0.69     ~ndr1_1 $X1 \/ c3_2 a281 a282
% 0.47/0.69  |- ~c1_1 $X1 \/ ~c2_2 $X1 $X2 \/ ~c4_1 $X1 \/ ~c4_2 $X1 $X2 \/ ~ndr1_0 \/
% 0.47/0.69     ~ndr1_1 $X1 \/ c5_1 a281
% 0.47/0.69  |- ~c1_1 $X1 \/ ~c2_2 $X1 $X2 \/ ~c4_1 $X1 \/ ~c4_2 $X1 $X2 \/ ~ndr1_0 \/
% 0.47/0.69     ~ndr1_1 $X1 \/ ndr1_1 a281
% 0.47/0.69  |- ~c1_0 \/ ~c1_2 a297 a298 \/ c3_0
% 0.47/0.69  |- ~c1_0 \/ ~c2_2 a297 a299 \/ c3_0
% 0.47/0.69  |- ~c1_0 \/ ~c3_2 a297 a299 \/ c3_0
% 0.47/0.69  |- ~c1_0 \/ ~c4_2 a297 a299 \/ c3_0
% 0.47/0.69  |- ~c1_0 \/ c2_1 a297 \/ c3_0
% 0.47/0.69  |- ~c1_0 \/ c2_2 a297 a298 \/ c3_0
% 0.47/0.69  |- ~c1_0 \/ c3_0 \/ c3_2 a297 a298
% 0.47/0.69  |- ~c1_0 \/ c3_0 \/ ndr1_0
% 0.47/0.69  |- ~c1_0 \/ c3_0 \/ ndr1_1 a297
% 0.47/0.69  |- ~c1_0 \/ ~c4_1 a277 \/ c5_0
% 0.47/0.69  |- ~c1_0 \/ c2_1 a277 \/ c5_0
% 0.47/0.69  |- ~c1_0 \/ c5_0 \/ ndr1_0
% 0.47/0.69  |- ~c1_0 \/ ~c2_1 $X7 \/ ~c2_1 $X9 \/ ~c2_2 $X9 a291 \/ ~c4_2 $X7 $X8 \/
% 0.47/0.69     ~c5_1 $X7 \/ ~ndr1_0 \/ ~ndr1_1 $X7 \/ c5_2 $X7 $X8
% 0.47/0.69  |- ~c1_0 \/ ~c2_1 $X7 \/ ~c2_1 $X9 \/ ~c4_2 $X7 $X8 \/ ~c5_1 $X7 \/
% 0.47/0.69     ~c5_2 $X9 a291 \/ ~ndr1_0 \/ ~ndr1_1 $X7 \/ c5_2 $X7 $X8
% 0.47/0.69  |- ~c1_0 \/ ~c2_1 $X7 \/ ~c2_1 $X9 \/ ~c4_2 $X7 $X8 \/ ~c5_1 $X7 \/
% 0.47/0.69     ~ndr1_0 \/ ~ndr1_1 $X7 \/ c1_2 $X9 a291 \/ c5_2 $X7 $X8
% 0.47/0.69  |- ~c1_0 \/ ~c2_1 $X7 \/ ~c2_1 $X9 \/ ~c4_2 $X7 $X8 \/ ~c5_1 $X7 \/
% 0.47/0.69     ~ndr1_0 \/ ~ndr1_1 $X7 \/ c5_2 $X7 $X8 \/ ndr1_1 $X9
% 0.47/0.69  |- ~c3_2 $X a279 \/ ~definitionFOFtoCNF_2 $X
% 0.47/0.69  |- ~definitionFOFtoCNF_2 $X \/ c4_2 $X a279
% 0.47/0.69  |- ~definitionFOFtoCNF_2 $X \/ ndr1_1 $X
% 0.47/0.69  |- ~c4_2 $X a279 \/ ~ndr1_1 $X \/ c3_2 $X a279 \/ definitionFOFtoCNF_2 $X
% 0.47/0.69  |- ~c1_2 $U $W \/ ~c2_0 \/ ~c2_1 $X \/ ~c2_2 $U a278 \/ ~c4_2 $U $V \/
% 0.47/0.69     ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c2_2 $U $W \/
% 0.47/0.69     definitionFOFtoCNF_2 $X
% 0.47/0.69  |- ~c1_2 $U $W \/ ~c2_0 \/ ~c2_1 $X \/ ~c4_2 $U $V \/ ~c4_2 $U a278 \/
% 0.47/0.69     ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c2_2 $U $W \/
% 0.47/0.69     definitionFOFtoCNF_2 $X
% 0.47/0.69  |- ~c1_2 $U $W \/ ~c2_0 \/ ~c2_1 $X \/ ~c4_2 $U $V \/ ~c5_2 $U $V \/
% 0.47/0.69     ~c5_2 $U a278 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c2_2 $U $W \/
% 0.47/0.69     definitionFOFtoCNF_2 $X
% 0.47/0.69  |- ~c1_2 $Y $Z \/ ~c3_0 \/ ~c5_1 $Y \/ ~ndr1_0 \/ ~ndr1_1 $Y \/
% 0.47/0.69     c3_2 $Y $Z \/ c4_2 $Y a280 \/ c5_0 \/ c5_2 $Y $Z
% 0.47/0.69  |- ~c1_2 $Y $Z \/ ~c3_0 \/ ~c5_1 $Y \/ ~ndr1_0 \/ ~ndr1_1 $Y \/
% 0.47/0.69     c3_2 $Y $Z \/ c5_0 \/ c5_2 $Y $Z \/ c5_2 $Y a280
% 0.47/0.69  |- ~c3_0 \/ ~c3_1 a292 \/ ~c4_1 $X12 \/ ~ndr1_0 \/ c1_1 $X12 \/ c3_1 $X12
% 0.47/0.69  |- ~c2_2 a292 $X11 \/ ~c3_0 \/ ~c4_1 $X12 \/ ~ndr1_0 \/ ~ndr1_1 a292 \/
% 0.47/0.69     c1_1 $X12 \/ c3_1 $X12 \/ c3_2 a292 $X11 \/ c4_2 a292 $X11
% 0.47/0.69  |- ~c3_0 \/ ~c3_2 a292 $X10 \/ ~c4_1 $X12 \/ ~c5_2 a292 $X10 \/ ~ndr1_0 \/
% 0.47/0.69     ~ndr1_1 a292 \/ c1_1 $X12 \/ c2_2 a292 $X10 \/ c3_1 $X12
% 0.47/0.69  |- c1_0 \/ c2_1 a302
% 0.47/0.69  |- c1_0 \/ c5_1 a302
% 0.47/0.69  |- c1_0 \/ ndr1_0
% 0.47/0.69  |- ~c2_2 a302 $X16 \/ ~c5_2 a302 $X16 \/ ~ndr1_1 a302 \/ c1_0
% 0.47/0.69  |- ~c1_2 $X14 $X15 \/ ~c1_2 a300 a301 \/ ~c2_2 $X14 $X15 \/ ~ndr1_0 \/
% 0.47/0.69     ~ndr1_1 $X14 \/ c1_1 $X14 \/ c4_1 $X14
% 0.47/0.69  |- ~c1_2 $X14 $X15 \/ ~c2_2 $X14 $X15 \/ ~c3_2 a300 a301 \/ ~ndr1_0 \/
% 0.47/0.69     ~ndr1_1 $X14 \/ c1_1 $X14 \/ c4_1 $X14
% 0.47/0.69  |- ~c1_2 $X14 $X15 \/ ~c2_2 $X14 $X15 \/ ~c4_2 a300 a301 \/ ~ndr1_0 \/
% 0.47/0.69     ~ndr1_1 $X14 \/ c1_1 $X14 \/ c4_1 $X14
% 0.47/0.69  |- ~c1_2 $X14 $X15 \/ ~c2_2 $X14 $X15 \/ ~ndr1_0 \/ ~ndr1_1 $X14 \/
% 0.47/0.69     c1_1 $X14 \/ c4_1 $X14 \/ c5_1 a300
% 0.47/0.69  |- ~c1_2 $X14 $X15 \/ ~c2_2 $X14 $X15 \/ ~ndr1_0 \/ ~ndr1_1 $X14 \/
% 0.47/0.69     c1_1 $X14 \/ c4_1 $X14 \/ ndr1_1 a300
% 0.47/0.69  |- ~c1_1 a288 \/ ~c5_0 \/ c3_0
% 0.47/0.69  |- ~c5_0 \/ c3_0 \/ ndr1_0
% 0.47/0.69  |- ~c5_0 \/ ~ndr1_1 a288 \/ c1_2 a288 $X5 \/ c2_2 a288 $X5 \/ c3_0 \/
% 0.47/0.69     c4_2 a288 $X5
% 0.47/0.69  |- ~c5_2 $X17 a303 \/ ~definitionFOFtoCNF_3 $X17
% 0.47/0.69  |- ~definitionFOFtoCNF_3 $X17 \/ c2_2 $X17 a303
% 0.47/0.69  |- ~definitionFOFtoCNF_3 $X17 \/ c4_2 $X17 a303
% 0.47/0.69  |- ~definitionFOFtoCNF_3 $X17 \/ ndr1_1 $X17
% 0.47/0.69  |- ~c2_2 $X17 a303 \/ ~c4_2 $X17 a303 \/ ~ndr1_1 $X17 \/ c5_2 $X17 a303 \/
% 0.47/0.69     definitionFOFtoCNF_3 $X17
% 0.47/0.69  |- ~c2_1 $X17 \/ ~c5_0 \/ ~c5_1 $X17 \/ ~ndr1_0 \/ c5_1 a304 \/
% 0.47/0.69     definitionFOFtoCNF_3 $X17
% 0.47/0.69  |- ~c2_1 $X17 \/ ~c4_2 a304 $X18 \/ ~c5_0 \/ ~c5_1 $X17 \/
% 0.47/0.69     ~c5_2 a304 $X18 \/ ~ndr1_0 \/ ~ndr1_1 a304 \/ c1_2 a304 $X18 \/
% 0.47/0.69     definitionFOFtoCNF_3 $X17
% 0.47/0.69  |- ~c2_2 $X3 a285 \/ definitionFOFtoCNF_5 $X3
% 0.47/0.69  |- c1_2 $X3 a285 \/ definitionFOFtoCNF_5 $X3
% 0.47/0.69  |- c3_2 $X3 a285 \/ definitionFOFtoCNF_5 $X3
% 0.47/0.69  |- definitionFOFtoCNF_5 $X3 \/ ndr1_1 $X3
% 0.47/0.69  |- ~c1_2 $X3 a285 \/ ~c3_2 $X3 a285 \/ ~definitionFOFtoCNF_5 $X3 \/
% 0.47/0.69     ~ndr1_1 $X3 \/ c2_2 $X3 a285
% 0.47/0.69  |- definitionFOFtoCNF_4 $X3 \/ definitionFOFtoCNF_5 $X3
% 0.47/0.69  |- ~c1_2 $X3 a284 \/ ~definitionFOFtoCNF_4 $X3 \/ ~definitionFOFtoCNF_5 $X3
% 0.47/0.69  |- ~c3_2 $X3 a284 \/ ~definitionFOFtoCNF_4 $X3 \/ ~definitionFOFtoCNF_5 $X3
% 0.47/0.69  |- ~definitionFOFtoCNF_4 $X3 \/ ~definitionFOFtoCNF_5 $X3 \/ c4_2 $X3 a284
% 0.47/0.69  |- ~definitionFOFtoCNF_4 $X3 \/ ~definitionFOFtoCNF_5 $X3 \/ ndr1_1 $X3
% 0.47/0.69  |- ~c4_2 $X3 a284 \/ ~ndr1_1 $X3 \/ c1_2 $X3 a284 \/ c3_2 $X3 a284 \/
% 0.47/0.69     definitionFOFtoCNF_4 $X3
% 0.47/0.69  |- ~c2_2 $X3 a283 \/ ~definitionFOFtoCNF_6 $X3
% 0.47/0.69  |- ~c4_2 $X3 a283 \/ ~definitionFOFtoCNF_6 $X3
% 0.47/0.69  |- ~definitionFOFtoCNF_6 $X3 \/ ndr1_1 $X3
% 0.47/0.69  |- ~ndr1_1 $X3 \/ c2_2 $X3 a283 \/ c4_2 $X3 a283 \/
% 0.47/0.69     definitionFOFtoCNF_6 $X3
% 0.47/0.69  |- ~c1_2 a286 a287 \/ ~ndr1_0 \/ c5_0 \/ definitionFOFtoCNF_4 $X3 \/
% 0.47/0.69     definitionFOFtoCNF_6 $X3
% 0.47/0.69  |- ~c2_1 a286 \/ ~ndr1_0 \/ c5_0 \/ definitionFOFtoCNF_4 $X3 \/
% 0.47/0.69     definitionFOFtoCNF_6 $X3
% 0.47/0.69  |- ~c4_2 a286 a287 \/ ~ndr1_0 \/ c5_0 \/ definitionFOFtoCNF_4 $X3 \/
% 0.47/0.69     definitionFOFtoCNF_6 $X3
% 0.47/0.69  |- ~ndr1_0 \/ c5_0 \/ definitionFOFtoCNF_4 $X3 \/
% 0.47/0.69     definitionFOFtoCNF_6 $X3 \/ ndr1_1 a286
% 0.47/0.69  |- ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $X4 \/ c5_0 \/ c5_2 a286 $X4 \/
% 0.47/0.69     definitionFOFtoCNF_4 $X3 \/ definitionFOFtoCNF_6 $X3
% 0.47/0.69  |- ~c1_1 a294 \/ ~definitionFOFtoCNF_7
% 0.47/0.69  |- ~c4_1 a294 \/ ~definitionFOFtoCNF_7
% 0.47/0.69  |- ~definitionFOFtoCNF_7 \/ c3_1 a294
% 0.47/0.69  |- ~definitionFOFtoCNF_7 \/ ndr1_0
% 0.47/0.69  |- ~c3_1 a294 \/ ~ndr1_0 \/ c1_1 a294 \/ c4_1 a294 \/ definitionFOFtoCNF_7
% 0.47/0.69  |- ~definitionFOFtoCNF_8 \/ c3_1 a296
% 0.47/0.69  |- ~definitionFOFtoCNF_8 \/ c4_1 a296
% 0.47/0.69  |- ~definitionFOFtoCNF_8 \/ ndr1_0
% 0.47/0.69  |- ~c3_1 a296 \/ ~c4_1 a296 \/ ~ndr1_0 \/ definitionFOFtoCNF_8
% 0.47/0.69  |- ~c1_1 a295 \/ definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.69  |- ~c2_1 a295 \/ definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.69  |- definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_0
% 0.47/0.69  |- ~ndr1_1 a295 \/ c4_2 a295 $X13 \/ c5_2 a295 $X13 \/
% 0.47/0.69     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 $U $W \/ ~c2_0 \/ ~c2_1 $X \/ ~c4_2 $U a278 \/ ~c5_2 $U a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 $U \/ c2_2 $U $W \/ definitionFOFtoCNF_2 $X
% 0.47/0.70  |- c1_0 \/ definitionFOFtoCNF_1 $_25 \/ ndr1_1 $_25
% 0.47/0.70  |- c1_0 \/ c4_2 $_29 a289 \/ definitionFOFtoCNF_1 $_29
% 0.47/0.70  |- c1_0 \/ c4_2 $_33 a290 \/ c5_2 $_33 a290 \/ definitionFOFtoCNF_1 $_33
% 0.47/0.70  |- c4_2 $_33 a290 \/ c5_2 $_33 a290 \/ definitionFOFtoCNF_1 $_33 \/
% 0.47/0.70     definitionFOFtoCNF_5 $_33
% 0.47/0.70  |- c1_0 \/ c2_2 $_36 a283 \/ c4_2 $_36 a283 \/ definitionFOFtoCNF_1 $_36 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_36
% 0.47/0.70  |- c2_2 $_36 a283 \/ c4_2 $_36 a283 \/ definitionFOFtoCNF_5 $_36 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_36
% 0.47/0.70  |- c5_0 \/ definitionFOFtoCNF_4 $_38 \/ definitionFOFtoCNF_6 $_38 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 a286
% 0.47/0.70  |- c1_0 \/ c5_0 \/ definitionFOFtoCNF_4 $_38 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_38 \/ ndr1_1 a286
% 0.47/0.70  |- ~c2_2 a302 a290 \/ ~ndr1_1 a302 \/ c1_0 \/ c4_2 a302 a290 \/
% 0.47/0.70     definitionFOFtoCNF_1 a302
% 0.47/0.70  |- c1_0 \/ c5_0 \/ definitionFOFtoCNF_4 $_47 \/ ndr1_1 $_47 \/ ndr1_1 a286
% 0.47/0.70  |- c1_0 \/ c2_2 a286 a283 \/ c4_2 a286 a283 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_47 \/ definitionFOFtoCNF_6 $_47 \/
% 0.47/0.70     definitionFOFtoCNF_6 a286
% 0.47/0.70  |- c1_0 \/ c5_0 \/ definitionFOFtoCNF_4 a286 \/ ndr1_1 a286
% 0.47/0.70  |- c1_0 \/ c2_2 a286 a283 \/ c4_2 a286 a283 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_4 a286 \/ definitionFOFtoCNF_6 a286
% 0.47/0.70  |- c1_0 \/ c4_2 a295 $_48 \/ c5_2 a295 $_48 \/ definitionFOFtoCNF_1 a295 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- c4_2 a295 $_48 \/ c5_2 a295 $_48 \/ definitionFOFtoCNF_5 a295 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~definitionFOFtoCNF_1 a295 \/ c4_2 a295 a290 \/
% 0.47/0.70     definitionFOFtoCNF_5 a295 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c5_0 \/ c1_0 \/ c5_1 a304 \/ definitionFOFtoCNF_3 a302
% 0.47/0.70  |- c5_0 \/ definitionFOFtoCNF_4 $_53 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 $_53 \/ ndr1_1 a286
% 0.47/0.70  |- c2_2 a286 a283 \/ c4_2 a286 a283 \/ c5_0 \/ definitionFOFtoCNF_4 $_53 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_53 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- c4_2 a286 a290 \/ c5_0 \/ c5_2 a286 a290 \/ definitionFOFtoCNF_1 a286 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_53 \/ definitionFOFtoCNF_6 $_53 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- c5_0 \/ definitionFOFtoCNF_4 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 a286
% 0.47/0.70  |- c2_2 a286 a283 \/ c4_2 a286 a283 \/ c5_0 \/ definitionFOFtoCNF_4 a286 \/
% 0.47/0.70     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- c4_2 a286 a290 \/ c5_0 \/ c5_2 a286 a290 \/ definitionFOFtoCNF_1 a286 \/
% 0.47/0.70     definitionFOFtoCNF_4 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c5_0 \/ c1_0 \/ c1_2 a288 $_59 \/ c2_2 a288 $_59 \/ c3_0 \/
% 0.47/0.70     c4_2 a288 $_59 \/ definitionFOFtoCNF_1 a288
% 0.47/0.70  |- ~c5_0 \/ c1_2 a288 $_59 \/ c2_2 a288 $_59 \/ c3_0 \/ c4_2 a288 $_59 \/
% 0.47/0.70     definitionFOFtoCNF_5 a288
% 0.47/0.70  |- c4_2 a295 $X13 \/ c5_0 \/ c5_2 a295 $X13 \/ definitionFOFtoCNF_4 a295 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 a286
% 0.47/0.70  |- c4_2 $_60 a290 \/ c5_0 \/ c5_2 $_60 a290 \/ definitionFOFtoCNF_1 $_60 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_60 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 a286
% 0.47/0.70  |- c1_0 \/ c2_2 a286 a283 \/ c4_2 a286 a283 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_63 \/ definitionFOFtoCNF_6 a286 \/ ndr1_1 $_63
% 0.47/0.70  |- ~ndr1_0 \/ c2_2 a286 $_66 \/ c5_0 \/ c5_2 a286 $_66 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_65 \/ definitionFOFtoCNF_5 a286 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_65
% 0.47/0.70  |- ~definitionFOFtoCNF_1 a295 \/ c4_2 a295 a290 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_4 a295 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 a286
% 0.47/0.70  |- c2_2 a286 a283 \/ c4_2 a286 a283 \/ c5_0 \/ definitionFOFtoCNF_4 $_90 \/
% 0.47/0.70     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 $_90
% 0.47/0.70  |- c4_2 a286 a290 \/ c5_0 \/ c5_2 a286 a290 \/ definitionFOFtoCNF_1 a286 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_91 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 $_91
% 0.47/0.70  |- c2_2 a286 a283 \/ c4_2 $_92 a290 \/ c4_2 a286 a283 \/ c5_0 \/
% 0.47/0.70     c5_2 $_92 a290 \/ definitionFOFtoCNF_1 $_92 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_92 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- c4_2 $_93 a290 \/ c4_2 a286 a290 \/ c5_0 \/ c5_2 $_93 a290 \/
% 0.47/0.70     c5_2 a286 a290 \/ definitionFOFtoCNF_1 $_93 \/
% 0.47/0.70     definitionFOFtoCNF_1 a286 \/ definitionFOFtoCNF_4 $_93 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~c3_0 \/ ~c3_2 a292 a290 \/ ~c4_1 $_112 \/ ~ndr1_0 \/ ~ndr1_1 a292 \/
% 0.47/0.70     c1_1 $_112 \/ c2_2 a292 a290 \/ c3_1 $_112 \/ c4_2 a292 a290 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_1 a292 \/ definitionFOFtoCNF_4 a292 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 a286
% 0.47/0.70  |- ~c3_0 \/ ~c3_2 a292 a290 \/ ~c4_1 $_112 \/ ~ndr1_0 \/ ~ndr1_1 a292 \/
% 0.47/0.70     c1_1 $_112 \/ c2_2 a292 a290 \/ c3_1 $_112 \/ c4_2 a292 a290 \/
% 0.47/0.70     definitionFOFtoCNF_1 a292 \/ definitionFOFtoCNF_5 a292
% 0.47/0.70  |- ~c3_0 \/ ~c3_2 a292 a290 \/ ~c4_1 $_112 \/ ~ndr1_0 \/ ~ndr1_1 a292 \/
% 0.47/0.70     c1_0 \/ c1_1 $_112 \/ c2_2 a292 a290 \/ c3_1 $_112 \/ c4_2 a292 a290 \/
% 0.47/0.70     definitionFOFtoCNF_1 a292
% 0.47/0.70  |- c1_0 \/ c5_0 \/ definitionFOFtoCNF_1 a286 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_134 \/ definitionFOFtoCNF_6 $_134
% 0.47/0.70  |- c1_0 \/ c5_0 \/ definitionFOFtoCNF_1 a286 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_135 \/ ndr1_1 $_135
% 0.47/0.70  |- c1_0 \/ c4_2 a295 $X13 \/ c5_0 \/ c5_2 a295 $X13 \/
% 0.47/0.70     definitionFOFtoCNF_1 a286 \/ definitionFOFtoCNF_4 a295 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~definitionFOFtoCNF_1 a295 \/ c1_0 \/ c4_2 a295 a290 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_1 a286 \/ definitionFOFtoCNF_4 a295 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~c3_0 \/ ~c3_2 a292 a290 \/ ~c4_1 $X12 \/ ~ndr1_0 \/ ~ndr1_1 a292 \/
% 0.47/0.70     c1_1 $X12 \/ c2_2 a286 a283 \/ c2_2 a292 a290 \/ c3_1 $X12 \/
% 0.47/0.70     c4_2 a286 a283 \/ c4_2 a292 a290 \/ c5_0 \/ definitionFOFtoCNF_1 a292 \/
% 0.47/0.70     definitionFOFtoCNF_4 a292 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~c3_0 \/ ~c3_2 a292 a290 \/ ~c4_1 $X12 \/ ~ndr1_0 \/ ~ndr1_1 a292 \/
% 0.47/0.70     c1_1 $X12 \/ c2_2 a292 a290 \/ c3_1 $X12 \/ c4_2 a286 a290 \/
% 0.47/0.70     c4_2 a292 a290 \/ c5_0 \/ c5_2 a286 a290 \/ definitionFOFtoCNF_1 a286 \/
% 0.47/0.70     definitionFOFtoCNF_1 a292 \/ definitionFOFtoCNF_4 a292 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_0 \/ ~c2_1 $_174 \/ ~c2_1 $_175 \/ ~c5_1 $_174 \/ ~ndr1_0 \/
% 0.47/0.70     c2_2 $_174 a283 \/ c5_2 $_174 a283 \/ definitionFOFtoCNF_5 $_174 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_174 \/ ndr1_1 $_175
% 0.47/0.70  |- ~c1_0 \/ ~c2_1 $_178 \/ ~c2_1 $_179 \/ ~c2_2 $_179 a291 \/
% 0.47/0.70     ~c5_1 $_178 \/ ~ndr1_0 \/ c2_2 $_178 a283 \/ c5_2 $_178 a283 \/
% 0.47/0.70     definitionFOFtoCNF_5 $_178 \/ definitionFOFtoCNF_6 $_178
% 0.47/0.70  |- ~c1_0 \/ ~c2_1 $_182 \/ ~c2_1 $_183 \/ ~c5_1 $_182 \/ ~ndr1_0 \/
% 0.47/0.70     c1_2 $_183 a291 \/ c2_2 $_182 a283 \/ c5_2 $_182 a283 \/
% 0.47/0.70     definitionFOFtoCNF_5 $_182 \/ definitionFOFtoCNF_6 $_182
% 0.47/0.70  |- c1_0 \/ c2_2 a286 $_191 \/ c5_0 \/ c5_2 a286 $_191 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_190 \/ ndr1_1 $_190
% 0.47/0.70  |- ~definitionFOFtoCNF_1 a286 \/ c1_0 \/ c2_2 a286 a290 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_192 \/ ndr1_1 $_192
% 0.47/0.70  |- c1_0 \/ c2_2 a286 $_200 \/ c5_0 \/ c5_2 a286 $_200 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_199 \/ definitionFOFtoCNF_6 $_199
% 0.47/0.70  |- ~definitionFOFtoCNF_1 a286 \/ c1_0 \/ c2_2 a286 a290 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_201 \/ definitionFOFtoCNF_6 $_201
% 0.47/0.70  |- ~c1_0 \/ ~c2_1 $_204 \/ ~c2_1 $_205 \/ ~c5_1 $_204 \/
% 0.47/0.70     ~c5_2 $_205 a291 \/ ~ndr1_0 \/ c2_2 $_204 a283 \/ c5_2 $_204 a283 \/
% 0.47/0.70     definitionFOFtoCNF_5 $_204 \/ definitionFOFtoCNF_6 $_204
% 0.47/0.70  |- c2_2 a286 $_214 \/ c5_0 \/ c5_2 a286 $_214 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_213 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 $_213
% 0.47/0.70  |- ~definitionFOFtoCNF_1 a286 \/ c2_2 a286 a290 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_215 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 $_215
% 0.47/0.70  |- ~c1_0 \/ ~c2_1 $_204 \/ ~c2_1 a286 \/ ~c5_1 $_204 \/ ~ndr1_0 \/
% 0.47/0.70     c2_2 $_204 a283 \/ c2_2 a286 a291 \/ c5_0 \/ c5_2 $_204 a283 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_215 \/ definitionFOFtoCNF_5 $_204 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_204 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 $_215
% 0.47/0.70  |- ~c1_0 \/ ~c2_1 $X7 \/ ~c2_1 a286 \/ ~c4_2 $X7 $X8 \/ ~c5_1 $X7 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 $X7 \/ c2_2 a286 a291 \/ c5_0 \/ c5_2 $X7 $X8 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_215 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 $_215
% 0.47/0.70  |- c2_2 a286 $_216 \/ c4_2 $_215 a290 \/ c5_0 \/ c5_2 $_215 a290 \/
% 0.47/0.70     c5_2 a286 $_216 \/ definitionFOFtoCNF_1 $_215 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_215 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- c2_2 a286 $_220 \/ c5_0 \/ c5_2 a286 $_220 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_219 \/ definitionFOFtoCNF_6 $_219 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~definitionFOFtoCNF_1 a286 \/ c2_2 a286 a290 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_221 \/ definitionFOFtoCNF_6 $_221 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~c3_0 \/ ~c3_2 a292 a290 \/ ~c4_1 $X12 \/ ~ndr1_0 \/ ~ndr1_1 a292 \/
% 0.47/0.70     c1_1 $X12 \/ c2_2 a286 $_228 \/ c2_2 a292 a290 \/ c3_1 $X12 \/
% 0.47/0.70     c4_2 a292 a290 \/ c5_0 \/ c5_2 a286 $_228 \/
% 0.47/0.70     definitionFOFtoCNF_1 a292 \/ definitionFOFtoCNF_4 a292 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~definitionFOFtoCNF_1 a286 \/ c2_2 a286 a290 \/ c4_2 $_227 a290 \/
% 0.47/0.70     c5_0 \/ c5_2 $_227 a290 \/ definitionFOFtoCNF_1 $_227 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_227 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_0 \/ ~c2_1 $_204 \/ ~c2_1 a286 \/ ~c5_1 $_204 \/ ~ndr1_0 \/
% 0.47/0.70     c2_2 $_204 a283 \/ c2_2 a286 a291 \/ c4_2 $_227 a290 \/ c5_0 \/
% 0.47/0.70     c5_2 $_204 a283 \/ c5_2 $_227 a290 \/ definitionFOFtoCNF_1 $_227 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_227 \/ definitionFOFtoCNF_5 $_204 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_204 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_0 \/ ~c2_1 $X7 \/ ~c2_1 a286 \/ ~c4_2 $X7 $X8 \/ ~c5_1 $X7 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 $X7 \/ c2_2 a286 a291 \/ c4_2 $_227 a290 \/ c5_0 \/
% 0.47/0.70     c5_2 $X7 $X8 \/ c5_2 $_227 a290 \/ definitionFOFtoCNF_1 $_227 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_227 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_232 \/ ~c2_0 \/ ~c2_1 $_233 \/ ~c4_2 a286 $_231 \/
% 0.47/0.70     ~c4_2 a286 a278 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_231 \/
% 0.47/0.70     c2_2 a286 $_232 \/ c4_2 $_215 a290 \/ c5_0 \/ c5_2 $_215 a290 \/
% 0.47/0.70     definitionFOFtoCNF_1 $_215 \/ definitionFOFtoCNF_2 $_233 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_215 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_232 \/ ~c2_0 \/ ~c2_1 $_233 \/ ~c4_2 a286 $_231 \/
% 0.47/0.70     ~c4_2 a286 a278 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_231 \/
% 0.47/0.70     c2_2 a286 $_232 \/ c5_0 \/ definitionFOFtoCNF_2 $_233 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_219 \/ definitionFOFtoCNF_6 $_219 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_232 \/ ~c2_0 \/ ~c2_1 $_233 \/ ~c4_2 a286 $_231 \/
% 0.47/0.70     ~c4_2 a286 a278 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_231 \/
% 0.47/0.70     c2_2 a286 $_232 \/ c5_0 \/ definitionFOFtoCNF_2 $_233 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_213 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 $_213
% 0.47/0.70  |- ~c1_2 a286 $_232 \/ ~c2_0 \/ ~c2_1 $_233 \/ ~c4_2 a286 $_231 \/
% 0.47/0.70     ~c4_2 a286 a278 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_231 \/
% 0.47/0.70     c2_2 a286 $_232 \/ c5_0 \/ definitionFOFtoCNF_2 $_233 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_199 \/ definitionFOFtoCNF_6 $_199
% 0.47/0.70  |- ~c1_2 a286 $_232 \/ ~c2_0 \/ ~c2_1 $_233 \/ ~c4_2 a286 $_231 \/
% 0.47/0.70     ~c4_2 a286 a278 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_231 \/
% 0.47/0.70     c2_2 a286 $_232 \/ c5_0 \/ definitionFOFtoCNF_2 $_233 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_190 \/ ndr1_1 $_190
% 0.47/0.70  |- ~c1_2 a286 $_232 \/ ~c2_0 \/ ~c2_1 $_233 \/ ~c4_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_232 \/ c2_2 a286 a278 \/
% 0.47/0.70     c5_0 \/ definitionFOFtoCNF_2 $_233 \/ definitionFOFtoCNF_4 $_199 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_199
% 0.47/0.70  |- ~c1_2 a286 $_232 \/ ~c2_0 \/ ~c2_1 $_233 \/ ~c4_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_232 \/ c2_2 a286 a278 \/
% 0.47/0.70     c5_0 \/ definitionFOFtoCNF_2 $_233 \/ definitionFOFtoCNF_4 $_190 \/
% 0.47/0.70     ndr1_1 $_190
% 0.47/0.70  |- ~c1_2 a286 $_232 \/ ~c2_0 \/ ~c2_1 $_233 \/ ~c4_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_232 \/ c2_2 a286 a278 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_233 \/ definitionFOFtoCNF_4 $_219 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_219 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_232 \/ ~c2_0 \/ ~c2_1 $_233 \/ ~c4_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_232 \/ c2_2 a286 a278 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_233 \/ definitionFOFtoCNF_4 $_213 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_213
% 0.47/0.70  |- ~c1_2 a286 $_232 \/ ~c2_0 \/ ~c2_1 $_233 \/ ~c4_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_232 \/ c2_2 a286 a278 \/
% 0.47/0.70     c4_2 $_215 a290 \/ c5_0 \/ c5_2 $_215 a290 \/
% 0.47/0.70     definitionFOFtoCNF_1 $_215 \/ definitionFOFtoCNF_2 $_233 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_215 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_236 \/ ~c2_0 \/ ~c2_1 $_237 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~c4_2 a286 $_235 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_235 \/
% 0.47/0.70     c2_2 a286 $_236 \/ c4_2 $_215 a290 \/ c5_0 \/ c5_2 $_215 a290 \/
% 0.47/0.70     definitionFOFtoCNF_1 $_215 \/ definitionFOFtoCNF_2 $_237 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_215 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_236 \/ ~c2_0 \/ ~c2_1 $_237 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~c4_2 a286 $_235 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_235 \/
% 0.47/0.70     c2_2 a286 $_236 \/ c5_0 \/ definitionFOFtoCNF_2 $_237 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_219 \/ definitionFOFtoCNF_6 $_219 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_236 \/ ~c2_0 \/ ~c2_1 $_237 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~c4_2 a286 $_235 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_235 \/
% 0.47/0.70     c2_2 a286 $_236 \/ c5_0 \/ definitionFOFtoCNF_2 $_237 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_213 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 $_213
% 0.47/0.70  |- ~c1_2 a286 $_236 \/ ~c2_0 \/ ~c2_1 $_237 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~c4_2 a286 $_235 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/
% 0.47/0.70     c2_2 a286 $_235 \/ c2_2 a286 $_236 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_237 \/ definitionFOFtoCNF_4 $_199 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_199
% 0.47/0.70  |- ~c1_2 a286 $_236 \/ ~c2_0 \/ ~c2_1 $_237 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~c4_2 a286 $_235 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/
% 0.47/0.70     c2_2 a286 $_235 \/ c2_2 a286 $_236 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_237 \/ definitionFOFtoCNF_4 $_190 \/ ndr1_1 $_190
% 0.47/0.70  |- ~c1_2 a286 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a286 $_239 \/
% 0.47/0.70     ~c5_2 a286 a278 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_239 \/
% 0.47/0.70     c2_2 a286 $_240 \/ c4_2 $_215 a290 \/ c5_0 \/ c5_2 $_215 a290 \/
% 0.47/0.70     definitionFOFtoCNF_1 $_215 \/ definitionFOFtoCNF_2 $_241 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_215 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a286 $_239 \/
% 0.47/0.70     ~c5_2 a286 a278 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_239 \/
% 0.47/0.70     c2_2 a286 $_240 \/ c5_0 \/ definitionFOFtoCNF_2 $_241 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_219 \/ definitionFOFtoCNF_6 $_219 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a286 $_239 \/
% 0.47/0.70     ~c5_2 a286 a278 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_239 \/
% 0.47/0.70     c2_2 a286 $_240 \/ c5_0 \/ definitionFOFtoCNF_2 $_241 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_213 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 $_213
% 0.47/0.70  |- ~c1_2 a286 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a286 $_239 \/
% 0.47/0.70     ~c5_2 a286 a278 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_239 \/
% 0.47/0.70     c2_2 a286 $_240 \/ c5_0 \/ definitionFOFtoCNF_2 $_241 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_199 \/ definitionFOFtoCNF_6 $_199
% 0.47/0.70  |- ~c1_2 a286 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a286 $_239 \/
% 0.47/0.70     ~c5_2 a286 a278 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_239 \/
% 0.47/0.70     c2_2 a286 $_240 \/ c5_0 \/ definitionFOFtoCNF_2 $_241 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_190 \/ ndr1_1 $_190
% 0.47/0.70  |- ~c1_2 a286 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a286 $_239 \/
% 0.47/0.70     ~c5_2 a286 $_239 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_240 \/
% 0.47/0.70     c2_2 a286 a278 \/ c4_2 $_215 a290 \/ c5_0 \/ c5_2 $_215 a290 \/
% 0.47/0.70     definitionFOFtoCNF_1 $_215 \/ definitionFOFtoCNF_2 $_241 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_215 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a286 $_239 \/
% 0.47/0.70     ~c5_2 a286 $_239 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_240 \/
% 0.47/0.70     c2_2 a286 a278 \/ c5_0 \/ definitionFOFtoCNF_2 $_241 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_219 \/ definitionFOFtoCNF_6 $_219 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a286 $_239 \/
% 0.47/0.70     ~c5_2 a286 $_239 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_240 \/
% 0.47/0.70     c2_2 a286 a278 \/ c5_0 \/ definitionFOFtoCNF_2 $_241 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_213 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 $_213
% 0.47/0.70  |- ~c1_2 a286 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a286 $_239 \/
% 0.47/0.70     ~c5_2 a286 $_239 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/
% 0.47/0.70     c2_2 a286 $_240 \/ c2_2 a286 a278 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_241 \/ definitionFOFtoCNF_4 $_199 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_199
% 0.47/0.70  |- ~c1_2 a286 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a286 $_239 \/
% 0.47/0.70     ~c5_2 a286 $_239 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/
% 0.47/0.70     c2_2 a286 $_240 \/ c2_2 a286 a278 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_241 \/ definitionFOFtoCNF_4 $_190 \/ ndr1_1 $_190
% 0.47/0.70  |- ~c1_2 a295 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a295 $_239 \/
% 0.47/0.70     ~c5_2 a295 $_239 \/ ~ndr1_0 \/ ~ndr1_1 a295 \/ c1_0 \/
% 0.47/0.70     c2_2 a295 $_240 \/ c4_2 a295 a278 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_1 a286 \/ definitionFOFtoCNF_2 $_241 \/
% 0.47/0.70     definitionFOFtoCNF_4 a295 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a295 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a295 $_239 \/
% 0.47/0.70     ~c5_2 a295 $_239 \/ ~ndr1_0 \/ ~ndr1_1 a295 \/ c2_2 a295 $_240 \/
% 0.47/0.70     c4_2 a295 a278 \/ c5_0 \/ definitionFOFtoCNF_2 $_241 \/
% 0.47/0.70     definitionFOFtoCNF_4 a295 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8 \/ ndr1_1 a286
% 0.47/0.70  |- ~c1_2 a295 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a295 $_239 \/
% 0.47/0.70     ~c5_2 a295 $_239 \/ ~ndr1_0 \/ ~ndr1_1 a295 \/ c1_0 \/
% 0.47/0.70     c2_2 a295 $_240 \/ c4_2 a295 a278 \/ definitionFOFtoCNF_1 a295 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_241 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a295 $_240 \/ ~c2_0 \/ ~c2_1 $_241 \/ ~c4_2 a295 $_239 \/
% 0.47/0.70     ~c5_2 a295 $_239 \/ ~ndr1_0 \/ ~ndr1_1 a295 \/ c2_2 a295 $_240 \/
% 0.47/0.70     c4_2 a295 a278 \/ definitionFOFtoCNF_2 $_241 \/
% 0.47/0.70     definitionFOFtoCNF_5 a295 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_278 \/ ~c2_0 \/ ~c2_1 $_279 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_278 \/ c2_2 a286 a283 \/
% 0.47/0.70     c5_0 \/ definitionFOFtoCNF_2 $_279 \/ definitionFOFtoCNF_4 $_276 \/
% 0.47/0.70     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 $_276 \/
% 0.47/0.70     definitionFOFtoCNF_6 a286
% 0.47/0.70  |- ~c1_2 a286 $_278 \/ ~c2_0 \/ ~c2_1 $_279 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_278 \/ c2_2 a286 a283 \/
% 0.47/0.70     c5_0 \/ definitionFOFtoCNF_2 $_279 \/ definitionFOFtoCNF_4 $_276 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_47 \/ definitionFOFtoCNF_6 $_276 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_47 \/ definitionFOFtoCNF_6 a286
% 0.47/0.70  |- ~c1_2 a286 $_278 \/ ~c2_0 \/ ~c2_1 $_279 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_278 \/ c2_2 a286 a283 \/
% 0.47/0.70     c5_0 \/ definitionFOFtoCNF_2 $_279 \/ definitionFOFtoCNF_4 $_276 \/
% 0.47/0.70     definitionFOFtoCNF_4 a286 \/ definitionFOFtoCNF_6 $_276 \/
% 0.47/0.70     definitionFOFtoCNF_6 a286
% 0.47/0.70  |- ~c1_2 a286 $_282 \/ ~c2_0 \/ ~c2_1 $_283 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_282 \/ c2_2 a286 a283 \/
% 0.47/0.70     c5_0 \/ definitionFOFtoCNF_2 $_283 \/ definitionFOFtoCNF_4 $_280 \/
% 0.47/0.70     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 a286 \/ ndr1_1 $_280
% 0.47/0.70  |- ~c1_2 a286 $_282 \/ ~c2_0 \/ ~c2_1 $_283 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_282 \/ c2_2 a286 a283 \/
% 0.47/0.70     c5_0 \/ definitionFOFtoCNF_2 $_283 \/ definitionFOFtoCNF_4 $_280 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_63 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.70     ndr1_1 $_280 \/ ndr1_1 $_63
% 0.47/0.70  |- ~c1_2 a286 $_303 \/ ~c2_0 \/ ~c2_1 $_304 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_303 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_304 \/ definitionFOFtoCNF_4 $_301 \/
% 0.47/0.70     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 $_301 \/
% 0.47/0.70     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_303 \/ ~c2_0 \/ ~c2_1 $_304 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_303 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_304 \/ definitionFOFtoCNF_4 $_301 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_53 \/ definitionFOFtoCNF_6 $_301 \/
% 0.47/0.70     definitionFOFtoCNF_6 $_53 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_303 \/ ~c2_0 \/ ~c2_1 $_304 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_303 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_304 \/ definitionFOFtoCNF_4 $_301 \/
% 0.47/0.70     definitionFOFtoCNF_4 a286 \/ definitionFOFtoCNF_6 $_301 \/
% 0.47/0.70     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.70     definitionFOFtoCNF_8
% 0.47/0.70  |- ~c1_2 a286 $_307 \/ ~c2_0 \/ ~c2_1 $_308 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_307 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_308 \/ definitionFOFtoCNF_4 $_305 \/
% 0.47/0.70     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_305
% 0.47/0.70  |- ~c1_2 a286 $_307 \/ ~c2_0 \/ ~c2_1 $_308 \/ ~c2_2 a286 a278 \/
% 0.47/0.70     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_307 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.70     definitionFOFtoCNF_2 $_308 \/ definitionFOFtoCNF_4 $_305 \/
% 0.47/0.70     definitionFOFtoCNF_4 $_90 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.70     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_305 \/
% 0.47/0.70     ndr1_1 $_90
% 0.47/0.71  |- ~c1_2 a286 $_311 \/ ~c2_0 \/ ~c2_1 $_312 \/ ~c4_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_311 \/ c2_2 a286 a283 \/
% 0.47/0.71     c5_0 \/ definitionFOFtoCNF_2 $_312 \/ definitionFOFtoCNF_4 $_309 \/
% 0.47/0.71     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 a286 \/ ndr1_1 $_309
% 0.47/0.71  |- ~c1_2 a286 $_311 \/ ~c2_0 \/ ~c2_1 $_312 \/ ~c4_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_311 \/ c2_2 a286 a283 \/
% 0.47/0.71     c5_0 \/ definitionFOFtoCNF_2 $_312 \/ definitionFOFtoCNF_4 $_309 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_63 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.71     ndr1_1 $_309 \/ ndr1_1 $_63
% 0.47/0.71  |- ~c1_2 a286 $_315 \/ ~c2_0 \/ ~c2_1 $_316 \/ ~c4_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_315 \/ c2_2 a286 a283 \/
% 0.47/0.71     c5_0 \/ definitionFOFtoCNF_2 $_316 \/ definitionFOFtoCNF_4 $_313 \/
% 0.47/0.71     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 $_313 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286
% 0.47/0.71  |- ~c1_2 a286 $_315 \/ ~c2_0 \/ ~c2_1 $_316 \/ ~c4_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_315 \/ c2_2 a286 a283 \/
% 0.47/0.71     c5_0 \/ definitionFOFtoCNF_2 $_316 \/ definitionFOFtoCNF_4 $_313 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_47 \/ definitionFOFtoCNF_6 $_313 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_47 \/ definitionFOFtoCNF_6 a286
% 0.47/0.71  |- ~c1_2 a286 $_315 \/ ~c2_0 \/ ~c2_1 $_316 \/ ~c4_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_315 \/ c2_2 a286 a283 \/
% 0.47/0.71     c5_0 \/ definitionFOFtoCNF_2 $_316 \/ definitionFOFtoCNF_4 $_313 \/
% 0.47/0.71     definitionFOFtoCNF_4 a286 \/ definitionFOFtoCNF_6 $_313 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286
% 0.47/0.71  |- ~c1_2 a286 $_340 \/ ~c2_0 \/ ~c2_1 $_341 \/ ~c4_2 a286 $_339 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_339 \/ c2_2 a286 $_340 \/
% 0.47/0.71     c2_2 a286 a278 \/ c5_0 \/ definitionFOFtoCNF_2 $_341 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_199 \/ definitionFOFtoCNF_4 $_338 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_199 \/ definitionFOFtoCNF_6 $_338
% 0.47/0.71  |- ~c1_2 a286 $_344 \/ ~c2_0 \/ ~c2_1 $_345 \/ ~c4_2 a286 $_343 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c1_0 \/ c2_2 a286 $_343 \/ c2_2 a286 $_344 \/
% 0.47/0.71     c2_2 a286 a278 \/ c5_0 \/ definitionFOFtoCNF_2 $_345 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_190 \/ definitionFOFtoCNF_4 $_342 \/
% 0.47/0.71     ndr1_1 $_190 \/ ndr1_1 $_342
% 0.47/0.71  |- ~c1_2 a286 $_368 \/ ~c2_0 \/ ~c2_1 $_369 \/ ~c4_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_368 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_369 \/ definitionFOFtoCNF_4 $_366 \/
% 0.47/0.71     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.71     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_366
% 0.47/0.71  |- ~c1_2 a286 $_368 \/ ~c2_0 \/ ~c2_1 $_369 \/ ~c4_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_368 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_369 \/ definitionFOFtoCNF_4 $_366 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_90 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.71     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_366 \/
% 0.47/0.71     ndr1_1 $_90
% 0.47/0.71  |- ~c1_2 a286 $_372 \/ ~c2_0 \/ ~c2_1 $_373 \/ ~c4_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_372 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_373 \/ definitionFOFtoCNF_4 $_370 \/
% 0.47/0.71     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 $_370 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.71     definitionFOFtoCNF_8
% 0.47/0.71  |- ~c1_2 a286 $_372 \/ ~c2_0 \/ ~c2_1 $_373 \/ ~c4_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_372 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_373 \/ definitionFOFtoCNF_4 $_370 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_53 \/ definitionFOFtoCNF_6 $_370 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_53 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.71     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.71  |- ~c1_2 a286 $_372 \/ ~c2_0 \/ ~c2_1 $_373 \/ ~c4_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_372 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_373 \/ definitionFOFtoCNF_4 $_370 \/
% 0.47/0.71     definitionFOFtoCNF_4 a286 \/ definitionFOFtoCNF_6 $_370 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.71     definitionFOFtoCNF_8
% 0.47/0.71  |- ~c1_2 a286 $_382 \/ ~c2_0 \/ ~c2_1 $_383 \/ ~c4_2 a286 $_381 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_381 \/ c2_2 a286 $_382 \/
% 0.47/0.71     c2_2 a286 a278 \/ c5_0 \/ definitionFOFtoCNF_2 $_383 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_213 \/ definitionFOFtoCNF_4 $_380 \/
% 0.47/0.71     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_213 \/
% 0.47/0.71     ndr1_1 $_380
% 0.47/0.71  |- ~c1_2 a286 $_386 \/ ~c2_0 \/ ~c2_1 $_387 \/ ~c4_2 a286 $_385 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_385 \/ c2_2 a286 $_386 \/
% 0.47/0.71     c2_2 a286 a278 \/ c5_0 \/ definitionFOFtoCNF_2 $_387 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_219 \/ definitionFOFtoCNF_4 $_384 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_219 \/ definitionFOFtoCNF_6 $_384 \/
% 0.47/0.71     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.71  |- ~c1_2 a286 $_414 \/ ~c2_0 \/ ~c2_1 $_415 \/ ~c2_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_414 \/ c2_2 a286 a283 \/
% 0.47/0.71     c4_2 $_412 a290 \/ c5_0 \/ c5_2 $_412 a290 \/
% 0.47/0.71     definitionFOFtoCNF_1 $_412 \/ definitionFOFtoCNF_2 $_415 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_412 \/ definitionFOFtoCNF_5 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.71     definitionFOFtoCNF_8
% 0.47/0.71  |- ~c1_2 a286 $_435 \/ ~c2_0 \/ ~c2_1 $_436 \/ ~c4_2 a286 a278 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_435 \/ c2_2 a286 a283 \/
% 0.47/0.71     c4_2 $_433 a290 \/ c5_0 \/ c5_2 $_433 a290 \/
% 0.47/0.71     definitionFOFtoCNF_1 $_433 \/ definitionFOFtoCNF_2 $_436 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_433 \/ definitionFOFtoCNF_5 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.71     definitionFOFtoCNF_8
% 0.47/0.71  |- ~c1_2 a286 $_450 \/ ~c2_0 \/ ~c2_1 $_451 \/ ~c4_2 a286 $_449 \/
% 0.47/0.71     ~ndr1_0 \/ ~ndr1_1 a286 \/ c2_2 a286 $_449 \/ c2_2 a286 $_450 \/
% 0.47/0.71     c2_2 a286 a278 \/ c4_2 $_215 a290 \/ c4_2 $_448 a290 \/ c5_0 \/
% 0.47/0.71     c5_2 $_215 a290 \/ c5_2 $_448 a290 \/ definitionFOFtoCNF_1 $_215 \/
% 0.47/0.71     definitionFOFtoCNF_1 $_448 \/ definitionFOFtoCNF_2 $_451 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_215 \/ definitionFOFtoCNF_4 $_448 \/
% 0.47/0.71     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.71  |- ~c1_2 a286 $_466 \/ ~c2_0 \/ ~c2_1 $_467 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/
% 0.47/0.71     c1_0 \/ c2_2 a286 $_466 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_467 \/ definitionFOFtoCNF_4 $_463 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_464 \/ definitionFOFtoCNF_5 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_463 \/ definitionFOFtoCNF_6 $_464 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286
% 0.47/0.71  |- ~c1_2 a286 $_466 \/ ~c2_0 \/ ~c2_1 $_467 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/
% 0.47/0.71     c1_0 \/ c2_2 a286 $_466 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_467 \/ definitionFOFtoCNF_4 $_463 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_464 \/ definitionFOFtoCNF_4 $_47 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_463 \/ definitionFOFtoCNF_6 $_464 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_47 \/ definitionFOFtoCNF_6 a286
% 0.47/0.71  |- ~c1_2 a286 $_466 \/ ~c2_0 \/ ~c2_1 $_467 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/
% 0.47/0.71     c1_0 \/ c2_2 a286 $_466 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_467 \/ definitionFOFtoCNF_4 $_463 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_464 \/ definitionFOFtoCNF_4 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_463 \/ definitionFOFtoCNF_6 $_464 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286
% 0.47/0.71  |- ~c2_0 \/ ~c2_1 $_481 \/ ~ndr1_0 \/ c1_0 \/ c2_2 a286 a278 \/
% 0.47/0.71     c2_2 a286 a283 \/ c2_2 a286 a285 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_481 \/ definitionFOFtoCNF_4 $_479 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_480 \/ definitionFOFtoCNF_5 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_479 \/ definitionFOFtoCNF_6 $_480 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286
% 0.47/0.71  |- ~c2_0 \/ c1_0 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c2_2 a286 a285 \/
% 0.47/0.71     c5_0 \/ definitionFOFtoCNF_2 a302 \/ definitionFOFtoCNF_4 $_485 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_486 \/ definitionFOFtoCNF_5 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_485 \/ definitionFOFtoCNF_6 $_486 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286
% 0.47/0.71  |- ~c1_2 a286 $_496 \/ ~c2_0 \/ ~c2_1 $_497 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/
% 0.47/0.71     c2_2 a286 $_496 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_497 \/ definitionFOFtoCNF_4 $_493 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_494 \/ definitionFOFtoCNF_5 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_493 \/ definitionFOFtoCNF_6 $_494 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.71     definitionFOFtoCNF_8
% 0.47/0.71  |- ~c1_2 a286 $_496 \/ ~c2_0 \/ ~c2_1 $_497 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/
% 0.47/0.71     c2_2 a286 $_496 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_497 \/ definitionFOFtoCNF_4 $_493 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_494 \/ definitionFOFtoCNF_4 $_53 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_493 \/ definitionFOFtoCNF_6 $_494 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_53 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.71     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.71  |- ~c1_2 a286 $_496 \/ ~c2_0 \/ ~c2_1 $_497 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/
% 0.47/0.71     c2_2 a286 $_496 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_497 \/ definitionFOFtoCNF_4 $_493 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_494 \/ definitionFOFtoCNF_4 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_493 \/ definitionFOFtoCNF_6 $_494 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.71     definitionFOFtoCNF_8
% 0.47/0.71  |- ~c1_2 a286 $_501 \/ ~c2_0 \/ ~c2_1 $_502 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/
% 0.47/0.71     c1_0 \/ c2_2 a286 $_501 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_502 \/ definitionFOFtoCNF_4 $_498 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_499 \/ definitionFOFtoCNF_5 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ ndr1_1 $_498 \/ ndr1_1 $_499
% 0.47/0.71  |- ~c1_2 a286 $_501 \/ ~c2_0 \/ ~c2_1 $_502 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/
% 0.47/0.71     c1_0 \/ c2_2 a286 $_501 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_502 \/ definitionFOFtoCNF_4 $_498 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_499 \/ definitionFOFtoCNF_4 $_63 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ ndr1_1 $_498 \/ ndr1_1 $_499 \/ ndr1_1 $_63
% 0.47/0.71  |- ~c2_0 \/ ~c2_1 $_509 \/ ~ndr1_0 \/ c1_0 \/ c2_2 a286 a278 \/
% 0.47/0.71     c2_2 a286 a283 \/ c2_2 a286 a285 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_509 \/ definitionFOFtoCNF_4 $_507 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_508 \/ definitionFOFtoCNF_5 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ ndr1_1 $_507 \/ ndr1_1 $_508
% 0.47/0.71  |- ~c2_0 \/ c1_0 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c2_2 a286 a285 \/
% 0.47/0.71     c5_0 \/ definitionFOFtoCNF_2 a302 \/ definitionFOFtoCNF_4 $_513 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_514 \/ definitionFOFtoCNF_5 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ ndr1_1 $_513 \/ ndr1_1 $_514
% 0.47/0.71  |- ~c2_0 \/ ~c2_1 $_523 \/ ~ndr1_0 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/
% 0.47/0.71     c2_2 a286 a285 \/ c5_0 \/ definitionFOFtoCNF_2 $_523 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_521 \/ definitionFOFtoCNF_4 $_522 \/
% 0.47/0.71     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 $_521 \/
% 0.47/0.71     definitionFOFtoCNF_6 $_522 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.71     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.71  |- ~c1_2 a286 $_534 \/ ~c2_0 \/ ~c2_1 $_535 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/
% 0.47/0.71     c2_2 a286 $_534 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_535 \/ definitionFOFtoCNF_4 $_531 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_532 \/ definitionFOFtoCNF_5 a286 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.71     definitionFOFtoCNF_8 \/ ndr1_1 $_531 \/ ndr1_1 $_532
% 0.47/0.71  |- ~c1_2 a286 $_534 \/ ~c2_0 \/ ~c2_1 $_535 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/
% 0.47/0.71     c2_2 a286 $_534 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/ c5_0 \/
% 0.47/0.71     definitionFOFtoCNF_2 $_535 \/ definitionFOFtoCNF_4 $_531 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_532 \/ definitionFOFtoCNF_4 $_90 \/
% 0.47/0.71     definitionFOFtoCNF_6 a286 \/ definitionFOFtoCNF_7 \/
% 0.47/0.71     definitionFOFtoCNF_8 \/ ndr1_1 $_531 \/ ndr1_1 $_532 \/ ndr1_1 $_90
% 0.47/0.71  |- ~c2_0 \/ ~c2_1 $_542 \/ ~ndr1_0 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/
% 0.47/0.71     c2_2 a286 a285 \/ c5_0 \/ definitionFOFtoCNF_2 $_542 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_540 \/ definitionFOFtoCNF_4 $_541 \/
% 0.47/0.71     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.71     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_540 \/
% 0.47/0.71     ndr1_1 $_541
% 0.47/0.71  |- ~c1_2 a286 $_574 \/ ~c2_0 \/ ~c2_1 $_575 \/ ~ndr1_0 \/ ~ndr1_1 a286 \/
% 0.47/0.71     c2_2 a286 $_574 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/
% 0.47/0.71     c4_2 $_571 a290 \/ c4_2 $_572 a290 \/ c5_0 \/ c5_2 $_571 a290 \/
% 0.47/0.71     c5_2 $_572 a290 \/ definitionFOFtoCNF_1 $_571 \/
% 0.47/0.71     definitionFOFtoCNF_1 $_572 \/ definitionFOFtoCNF_2 $_575 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_571 \/ definitionFOFtoCNF_4 $_572 \/
% 0.47/0.71     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.71     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.71  |- ~c2_0 \/ ~c2_1 $_582 \/ ~ndr1_0 \/ c2_2 a286 a278 \/ c2_2 a286 a283 \/
% 0.47/0.71     c2_2 a286 a285 \/ c4_2 $_580 a290 \/ c4_2 $_581 a290 \/ c5_0 \/
% 0.47/0.71     c5_2 $_580 a290 \/ c5_2 $_581 a290 \/ definitionFOFtoCNF_1 $_580 \/
% 0.47/0.71     definitionFOFtoCNF_1 $_581 \/ definitionFOFtoCNF_2 $_582 \/
% 0.47/0.71     definitionFOFtoCNF_4 $_580 \/ definitionFOFtoCNF_4 $_581 \/
% 0.47/0.71     definitionFOFtoCNF_5 a286 \/ definitionFOFtoCNF_6 a286 \/
% 0.47/0.71     definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8
% 0.47/0.71  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.47/0.71  
%------------------------------------------------------------------------------