↑ Up

Metis---2.4.CSA-Sat.s

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

% Computer : n005.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:42 EDT 2022

% Result   : CounterSatisfiable 0.20s 0.50s
% Output   : Saturation 0.20s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : SYN529+1 : TPTP v8.1.0. Released v2.1.0.
% 0.13/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.34  % Computer : n005.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 600
% 0.13/0.34  % DateTime : Tue Jul 12 01:01:07 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.20/0.35  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.20/0.50  % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.50  
% 0.20/0.50  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.50  |- ~c3_1 a355
% 0.20/0.50  |- ~c4_2 a355 a356
% 0.20/0.50  |- ~c5_2 a355 a356
% 0.20/0.50  |- ndr1_0
% 0.20/0.50  |- ndr1_1 a355
% 0.20/0.50  |- ~c3_0 \/ c2_0
% 0.20/0.50  |- ~c5_0 \/ c2_0
% 0.20/0.51  |- c1_0 \/ c2_2 $X7 a334 \/ c3_1 $X7 \/ c5_1 $X7
% 0.20/0.51  |- c1_0 \/ c3_1 $X7 \/ c4_2 $X7 a334 \/ c5_1 $X7
% 0.20/0.51  |- c1_0 \/ c3_1 $X7 \/ c5_1 $X7 \/ ndr1_1 $X7
% 0.20/0.51  |- ~c1_1 a343 \/ c3_0
% 0.20/0.51  |- c2_1 a343 \/ c3_0
% 0.20/0.51  |- ~c4_1 $X10 \/ c2_2 $X10 a342 \/ c4_0 \/ c5_1 $X10
% 0.20/0.51  |- ~c4_1 $X10 \/ c4_0 \/ c5_1 $X10 \/ c5_2 $X10 a342
% 0.20/0.51  |- ~c4_1 $X10 \/ c4_0 \/ c5_1 $X10 \/ ndr1_1 $X10
% 0.20/0.51  |- ~c2_1 $X11 \/ ~ndr1_1 $X11 \/ c2_2 $X11 $X12 \/ c3_1 $X11 \/
% 0.20/0.51     c3_2 $X11 $X12 \/ c4_2 $X11 $X12 \/ c5_0
% 0.20/0.51  |- ~c1_2 $X15 a350 \/ ~definitionFOFtoCNF_0 $X15
% 0.20/0.51  |- ~c3_2 $X15 a350 \/ ~definitionFOFtoCNF_0 $X15
% 0.20/0.51  |- ~definitionFOFtoCNF_0 $X15 \/ c2_2 $X15 a350
% 0.20/0.51  |- ~definitionFOFtoCNF_0 $X15 \/ ndr1_1 $X15
% 0.20/0.51  |- ~c2_2 $X15 a350 \/ ~ndr1_1 $X15 \/ c1_2 $X15 a350 \/ c3_2 $X15 a350 \/
% 0.20/0.51     definitionFOFtoCNF_0 $X15
% 0.20/0.51  |- ~c3_1 $X15 \/ ~c3_1 a348 \/ ~c4_2 $X15 $X16 \/ ~ndr1_1 $X15 \/
% 0.20/0.51     c1_2 $X15 $X16 \/ c5_2 $X15 $X16 \/ definitionFOFtoCNF_0 $X15
% 0.20/0.51  |- ~c3_1 $X15 \/ ~c4_2 $X15 $X16 \/ ~c5_2 a348 a349 \/ ~ndr1_1 $X15 \/
% 0.20/0.51     c1_2 $X15 $X16 \/ c5_2 $X15 $X16 \/ definitionFOFtoCNF_0 $X15
% 0.20/0.51  |- ~c3_1 $X15 \/ ~c4_2 $X15 $X16 \/ ~ndr1_1 $X15 \/ c1_2 $X15 $X16 \/
% 0.20/0.51     c2_2 a348 a349 \/ c5_2 $X15 $X16 \/ definitionFOFtoCNF_0 $X15
% 0.20/0.51  |- ~c3_1 $X15 \/ ~c4_2 $X15 $X16 \/ ~ndr1_1 $X15 \/ c1_2 $X15 $X16 \/
% 0.20/0.51     c5_2 $X15 $X16 \/ definitionFOFtoCNF_0 $X15 \/ ndr1_1 a348
% 0.20/0.51  |- ~c2_2 a348 $X14 \/ ~c3_1 $X15 \/ ~c4_2 $X15 $X16 \/ ~c4_2 a348 $X14 \/
% 0.20/0.51     ~ndr1_1 $X15 \/ ~ndr1_1 a348 \/ c1_2 $X15 $X16 \/ c5_2 $X15 $X16 \/
% 0.20/0.51     c5_2 a348 $X14 \/ definitionFOFtoCNF_0 $X15
% 0.20/0.51  |- ~c1_0 \/ ~c5_0 \/ c4_0
% 0.20/0.51  |- ~c1_0 \/ c3_0 \/ c5_0
% 0.20/0.51  |- ~c2_0 \/ ~c3_0 \/ ~c4_0
% 0.20/0.51  |- ~c3_0 \/ ~c5_0 \/ c4_0
% 0.20/0.51  |- ~c3_1 a333 \/ ~c4_0 \/ ~c5_2 a331 a332
% 0.20/0.51  |- ~c3_1 a333 \/ ~c4_0 \/ c1_2 a331 a332
% 0.20/0.51  |- ~c3_1 a333 \/ ~c4_0 \/ c2_2 a331 a332
% 0.20/0.51  |- ~c3_1 a333 \/ ~c4_0 \/ c3_1 a331
% 0.20/0.51  |- ~c3_1 a333 \/ ~c4_0 \/ c5_1 a331
% 0.20/0.51  |- ~c3_1 a333 \/ ~c4_0 \/ ndr1_1 a331
% 0.20/0.51  |- ~c4_2 a318 a320 \/ ~definitionFOFtoCNF_1
% 0.20/0.51  |- ~definitionFOFtoCNF_1 \/ c2_2 a318 a319
% 0.20/0.51  |- ~definitionFOFtoCNF_1 \/ c2_2 a318 a320
% 0.20/0.51  |- ~definitionFOFtoCNF_1 \/ c4_2 a318 a319
% 0.20/0.51  |- ~definitionFOFtoCNF_1 \/ ndr1_1 a318
% 0.20/0.51  |- ~c2_2 a318 a319 \/ ~c2_2 a318 a320 \/ ~c4_2 a318 a319 \/ ~ndr1_1 a318 \/
% 0.20/0.51     c4_2 a318 a320 \/ definitionFOFtoCNF_1
% 0.20/0.51  |- ~c4_0 \/ ~c4_1 a316 \/ definitionFOFtoCNF_1
% 0.20/0.51  |- ~c4_0 \/ ~c4_2 a316 a317 \/ definitionFOFtoCNF_1
% 0.20/0.51  |- ~c4_0 \/ c1_1 a316 \/ definitionFOFtoCNF_1
% 0.20/0.51  |- ~c4_0 \/ c2_2 a316 a317 \/ definitionFOFtoCNF_1
% 0.20/0.51  |- ~c4_0 \/ c3_2 a316 a317 \/ definitionFOFtoCNF_1
% 0.20/0.51  |- ~c4_0 \/ definitionFOFtoCNF_1 \/ ndr1_1 a316
% 0.20/0.51  |- ~c3_2 a338 a339 \/ ~definitionFOFtoCNF_2
% 0.20/0.51  |- ~c4_2 a338 a339 \/ ~definitionFOFtoCNF_2
% 0.20/0.51  |- ~definitionFOFtoCNF_2 \/ c1_1 a338
% 0.20/0.51  |- ~definitionFOFtoCNF_2 \/ c1_2 a338 a339
% 0.20/0.51  |- ~definitionFOFtoCNF_2 \/ c4_1 a338
% 0.20/0.51  |- ~definitionFOFtoCNF_2 \/ ndr1_1 a338
% 0.20/0.51  |- ~c1_1 a338 \/ ~c1_2 a338 a339 \/ ~c4_1 a338 \/ ~ndr1_1 a338 \/
% 0.20/0.51     c3_2 a338 a339 \/ c4_2 a338 a339 \/ definitionFOFtoCNF_2
% 0.20/0.51  |- ~c1_2 $X8 a340 \/ ~definitionFOFtoCNF_3 $X8
% 0.20/0.51  |- ~c4_2 $X8 a340 \/ ~definitionFOFtoCNF_3 $X8
% 0.20/0.51  |- ~definitionFOFtoCNF_3 $X8 \/ c2_2 $X8 a340
% 0.20/0.51  |- ~definitionFOFtoCNF_3 $X8 \/ ndr1_1 $X8
% 0.20/0.51  |- ~c2_2 $X8 a340 \/ ~ndr1_1 $X8 \/ c1_2 $X8 a340 \/ c4_2 $X8 a340 \/
% 0.20/0.51     definitionFOFtoCNF_3 $X8
% 0.20/0.51  |- ~c3_2 $X8 $X9 \/ ~c5_0 \/ ~ndr1_1 $X8 \/ c1_2 $X8 $X9 \/ c2_2 $X8 $X9 \/
% 0.20/0.51     c2_2 $X8 a341 \/ definitionFOFtoCNF_2 \/ definitionFOFtoCNF_3 $X8
% 0.20/0.51  |- ~c3_2 $X8 $X9 \/ ~c5_0 \/ ~ndr1_1 $X8 \/ c1_2 $X8 $X9 \/ c2_2 $X8 $X9 \/
% 0.20/0.51     c3_2 $X8 a341 \/ definitionFOFtoCNF_2 \/ definitionFOFtoCNF_3 $X8
% 0.20/0.51  |- ~c3_2 $X8 $X9 \/ ~c5_0 \/ ~ndr1_1 $X8 \/ c1_2 $X8 $X9 \/ c2_2 $X8 $X9 \/
% 0.20/0.51     c4_2 $X8 a341 \/ definitionFOFtoCNF_2 \/ definitionFOFtoCNF_3 $X8
% 0.20/0.51  |- ~c1_1 a351 \/ ~definitionFOFtoCNF_4
% 0.20/0.51  |- ~c1_2 a351 a352 \/ ~definitionFOFtoCNF_4
% 0.20/0.51  |- ~c4_2 a351 a352 \/ ~definitionFOFtoCNF_4
% 0.20/0.51  |- ~definitionFOFtoCNF_4 \/ c2_2 a351 a352
% 0.20/0.51  |- ~definitionFOFtoCNF_4 \/ c4_1 a351
% 0.20/0.51  |- ~definitionFOFtoCNF_4 \/ ndr1_1 a351
% 0.20/0.51  |- ~c2_2 a351 a352 \/ ~c4_1 a351 \/ ~ndr1_1 a351 \/ c1_1 a351 \/
% 0.20/0.51     c1_2 a351 a352 \/ c4_2 a351 a352 \/ definitionFOFtoCNF_4
% 0.20/0.51  |- c2_2 a353 a354 \/ c3_0 \/ definitionFOFtoCNF_4
% 0.20/0.51  |- c3_0 \/ c3_2 a353 a354 \/ definitionFOFtoCNF_4
% 0.20/0.51  |- c3_0 \/ definitionFOFtoCNF_4 \/ ndr1_1 a353
% 0.20/0.51  |- ~c1_2 a353 $X18 \/ ~c4_2 a353 $X18 \/ ~ndr1_1 a353 \/ c3_0 \/
% 0.20/0.51     c3_2 a353 $X18 \/ definitionFOFtoCNF_4
% 0.20/0.51  |- ~c2_2 a353 $X17 \/ ~c5_2 a353 $X17 \/ ~ndr1_1 a353 \/ c3_0 \/
% 0.20/0.51     c3_2 a353 $X17 \/ definitionFOFtoCNF_4
% 0.20/0.51  |- ~c3_2 a335 a337 \/ c4_0 \/ c5_0
% 0.20/0.51  |- c1_2 a335 a337 \/ c4_0 \/ c5_0
% 0.20/0.51  |- c2_2 a335 a336 \/ c4_0 \/ c5_0
% 0.20/0.51  |- c4_0 \/ c4_2 a335 a336 \/ c5_0
% 0.20/0.51  |- c4_0 \/ c5_0 \/ c5_2 a335 a336
% 0.20/0.51  |- c4_0 \/ c5_0 \/ c5_2 a335 a337
% 0.20/0.51  |- c4_0 \/ c5_0 \/ ndr1_1 a335
% 0.20/0.51  |- ~c2_1 a328 \/ ~c2_2 a329 a330 \/ c4_0
% 0.20/0.51  |- ~c2_1 a328 \/ c1_1 a329 \/ c4_0
% 0.20/0.51  |- ~c2_1 a328 \/ c4_0 \/ ndr1_1 a329
% 0.20/0.51  |- ~c2_2 a329 a330 \/ c4_0 \/ c5_1 a328
% 0.20/0.51  |- c1_1 a329 \/ c4_0 \/ c5_1 a328
% 0.20/0.51  |- c4_0 \/ c5_1 a328 \/ ndr1_1 a329
% 0.20/0.51  |- ~c2_1 a328 \/ ~c4_2 a329 $X6 \/ ~c5_2 a329 $X6 \/ ~ndr1_1 a329 \/
% 0.20/0.51     c1_2 a329 $X6 \/ c4_0
% 0.20/0.51  |- ~c4_2 a329 $X6 \/ ~c5_2 a329 $X6 \/ ~ndr1_1 a329 \/ c1_2 a329 $X6 \/
% 0.20/0.51     c4_0 \/ c5_1 a328
% 0.20/0.51  |- ~c1_2 $X a321 \/ ~definitionFOFtoCNF_5 $X
% 0.20/0.51  |- ~c2_2 $X a321 \/ ~definitionFOFtoCNF_5 $X
% 0.20/0.51  |- ~definitionFOFtoCNF_5 $X \/ c5_2 $X a321
% 0.20/0.51  |- ~definitionFOFtoCNF_5 $X \/ ndr1_1 $X
% 0.20/0.51  |- ~c5_2 $X a321 \/ ~ndr1_1 $X \/ c1_2 $X a321 \/ c2_2 $X a321 \/
% 0.20/0.51     definitionFOFtoCNF_5 $X
% 0.20/0.51  |- ~c1_2 a322 a323 \/ ~c2_1 $X \/ ~c3_2 $X $Y \/ ~c4_2 $X $Y \/
% 0.20/0.51     ~ndr1_1 $X \/ c2_2 $X $Y \/ c4_0 \/ definitionFOFtoCNF_5 $X
% 0.20/0.51  |- ~c2_1 $X \/ ~c3_2 $X $Y \/ ~c4_2 $X $Y \/ ~c4_2 a322 a323 \/
% 0.20/0.51     ~ndr1_1 $X \/ c2_2 $X $Y \/ c4_0 \/ definitionFOFtoCNF_5 $X
% 0.20/0.51  |- ~c2_1 $X \/ ~c3_2 $X $Y \/ ~c4_2 $X $Y \/ ~ndr1_1 $X \/ c2_2 $X $Y \/
% 0.20/0.51     c3_1 a322 \/ c4_0 \/ definitionFOFtoCNF_5 $X
% 0.20/0.51  |- ~c2_1 $X \/ ~c3_2 $X $Y \/ ~c4_2 $X $Y \/ ~ndr1_1 $X \/ c2_2 $X $Y \/
% 0.20/0.51     c4_0 \/ c5_2 a322 a323 \/ definitionFOFtoCNF_5 $X
% 0.20/0.51  |- ~c2_1 $X \/ ~c3_2 $X $Y \/ ~c4_2 $X $Y \/ ~ndr1_1 $X \/ c2_2 $X $Y \/
% 0.20/0.51     c4_0 \/ definitionFOFtoCNF_5 $X \/ ndr1_1 a322
% 0.20/0.51  |- ~c1_2 a314 a315 \/ ~c4_1 $V \/ ~ndr1_1 $V \/ c1_2 $V $W \/ c3_2 $V $W \/
% 0.20/0.51     c4_0 \/ c4_2 $V $W \/ c5_1 $V
% 0.20/0.51  |- ~c2_2 a314 a315 \/ ~c4_1 $V \/ ~ndr1_1 $V \/ c1_2 $V $W \/ c3_2 $V $W \/
% 0.20/0.51     c4_0 \/ c4_2 $V $W \/ c5_1 $V
% 0.20/0.51  |- ~c3_2 a314 a315 \/ ~c4_1 $V \/ ~ndr1_1 $V \/ c1_2 $V $W \/ c3_2 $V $W \/
% 0.20/0.51     c4_0 \/ c4_2 $V $W \/ c5_1 $V
% 0.20/0.51  |- ~c4_1 $V \/ ~ndr1_1 $V \/ c1_2 $V $W \/ c3_2 $V $W \/ c4_0 \/
% 0.20/0.51     c4_1 a314 \/ c4_2 $V $W \/ c5_1 $V
% 0.20/0.51  |- ~c4_1 $V \/ ~ndr1_1 $V \/ c1_2 $V $W \/ c3_2 $V $W \/ c4_0 \/
% 0.20/0.51     c4_2 $V $W \/ c5_1 $V \/ ndr1_1 a314
% 0.20/0.51  |- ~c1_2 a314 $U \/ ~c4_1 $V \/ ~ndr1_1 $V \/ ~ndr1_1 a314 \/ c1_2 $V $W \/
% 0.20/0.51     c3_2 $V $W \/ c3_2 a314 $U \/ c4_0 \/ c4_2 $V $W \/ c4_2 a314 $U \/
% 0.20/0.51     c5_1 $V
% 0.20/0.51  |- ~c5_2 a346 a347 \/ ~definitionFOFtoCNF_6
% 0.20/0.51  |- ~definitionFOFtoCNF_6 \/ c1_2 a346 a347
% 0.20/0.51  |- ~definitionFOFtoCNF_6 \/ c3_1 a346
% 0.20/0.51  |- ~definitionFOFtoCNF_6 \/ c4_1 a346
% 0.20/0.51  |- ~definitionFOFtoCNF_6 \/ ndr1_1 a346
% 0.20/0.51  |- ~c1_2 a346 a347 \/ ~c3_1 a346 \/ ~c4_1 a346 \/ ~ndr1_1 a346 \/
% 0.20/0.51     c5_2 a346 a347 \/ definitionFOFtoCNF_6
% 0.20/0.51  |- ~c1_2 a344 a345 \/ c5_0 \/ definitionFOFtoCNF_6
% 0.20/0.51  |- ~c2_1 a344 \/ c5_0 \/ definitionFOFtoCNF_6
% 0.20/0.51  |- c3_2 a344 a345 \/ c5_0 \/ definitionFOFtoCNF_6
% 0.20/0.51  |- c5_0 \/ definitionFOFtoCNF_6 \/ ndr1_1 a344
% 0.20/0.51  |- ~c1_2 a344 $X13 \/ ~c2_2 a344 $X13 \/ ~c5_2 a344 $X13 \/ ~ndr1_1 a344 \/
% 0.20/0.51     c5_0 \/ definitionFOFtoCNF_6
% 0.20/0.51  |- ~c2_2 a326 a327 \/ ~definitionFOFtoCNF_7
% 0.20/0.51  |- ~c5_2 a326 a327 \/ ~definitionFOFtoCNF_7
% 0.20/0.51  |- ~definitionFOFtoCNF_7 \/ c2_1 a326
% 0.20/0.51  |- ~definitionFOFtoCNF_7 \/ c3_2 a326 a327
% 0.20/0.51  |- ~definitionFOFtoCNF_7 \/ c4_1 a326
% 0.20/0.51  |- ~definitionFOFtoCNF_7 \/ ndr1_1 a326
% 0.20/0.51  |- ~c2_1 a326 \/ ~c3_2 a326 a327 \/ ~c4_1 a326 \/ ~ndr1_1 a326 \/
% 0.20/0.51     c2_2 a326 a327 \/ c5_2 a326 a327 \/ definitionFOFtoCNF_7
% 0.20/0.51  |- c1_2 a324 a325 \/ c5_0 \/ definitionFOFtoCNF_7
% 0.20/0.51  |- c5_0 \/ c5_2 a324 a325 \/ definitionFOFtoCNF_7
% 0.20/0.51  |- c5_0 \/ definitionFOFtoCNF_7 \/ ndr1_1 a324
% 0.20/0.51  |- ~c4_2 a324 $X4 \/ ~ndr1_1 a324 \/ c2_2 a324 $X4 \/ c3_2 a324 $X4 \/
% 0.20/0.51     c5_0 \/ definitionFOFtoCNF_7
% 0.20/0.51  |- ~c2_1 $X1 \/ ~ndr1_1 $X2 \/ c1_1 $Z \/ c2_1 $X2 \/ c4_1 $X1 \/
% 0.20/0.51     c4_1 $X2 \/ c4_2 $X2 $X3 \/ c5_1 $Z \/ c5_2 $X2 $X3
% 0.20/0.51  |- ~c1_2 a355 $X19 \/ c3_2 a355 $X19
% 0.20/0.51  |- ~c2_1 a322 \/ ~c3_2 a322 a323 \/ ~c4_2 a322 a323 \/ ~ndr1_1 a322 \/
% 0.20/0.51     c2_2 a322 a323 \/ c4_0 \/ definitionFOFtoCNF_5 a322
% 0.20/0.51  |- c1_2 a324 $_19 \/ c3_2 a324 $_19 \/ c5_0 \/ definitionFOFtoCNF_7
% 0.20/0.51  |- ~definitionFOFtoCNF_0 a324 \/ c1_2 a324 a350 \/ c5_0 \/
% 0.20/0.51     definitionFOFtoCNF_7
% 0.20/0.51  |- ~c1_2 a353 a334 \/ ~ndr1_1 a353 \/ c1_0 \/ c3_0 \/ c3_1 a353 \/
% 0.20/0.51     c3_2 a353 a334 \/ c5_1 a353 \/ definitionFOFtoCNF_4
% 0.20/0.51  |- ~c2_1 a324 \/ c2_2 a324 $_31 \/ c3_1 a324 \/ c3_2 a324 $_31 \/
% 0.20/0.51     c4_2 a324 $_31 \/ c5_0 \/ definitionFOFtoCNF_7
% 0.20/0.51  |- ~c2_1 a329 \/ c2_2 a329 $_31 \/ c3_1 a329 \/ c3_2 a329 $_31 \/ c4_0 \/
% 0.20/0.51     c4_2 a329 $_31 \/ c5_0 \/ c5_1 a328
% 0.20/0.51  |- ~c2_1 a335 \/ c2_2 a335 $_31 \/ c3_1 a335 \/ c3_2 a335 $_31 \/ c4_0 \/
% 0.20/0.51     c4_2 a335 $_31 \/ c5_0
% 0.20/0.51  |- ~c2_1 a353 \/ c2_2 a353 $_31 \/ c3_0 \/ c3_1 a353 \/ c3_2 a353 $_31 \/
% 0.20/0.51     c4_2 a353 $_31 \/ c5_0 \/ definitionFOFtoCNF_4
% 0.20/0.51  |- ~c2_1 a355 \/ c2_2 a355 $_31 \/ c3_2 a355 $_31 \/ c4_2 a355 $_31 \/ c5_0
% 0.20/0.51  |- ~c2_1 $_30 \/ c1_0 \/ c2_2 $_30 $_31 \/ c3_1 $_30 \/ c3_2 $_30 $_31 \/
% 0.20/0.51     c4_2 $_30 $_31 \/ c5_0 \/ c5_1 $_30
% 0.20/0.51  |- ~c4_1 a329 \/ c1_2 a329 $_56 \/ c3_2 a329 $_56 \/ c4_0 \/ c4_1 a314 \/
% 0.20/0.51     c4_2 a329 $_56 \/ c5_1 a328 \/ c5_1 a329
% 0.20/0.51  |- ~c4_1 a335 \/ c1_2 a335 $_56 \/ c3_2 a335 $_56 \/ c4_0 \/ c4_1 a314 \/
% 0.20/0.51     c4_2 a335 $_56 \/ c5_0 \/ c5_1 a335
% 0.20/0.51  |- ~c4_1 a344 \/ c1_2 a344 $_56 \/ c3_2 a344 $_56 \/ c4_0 \/ c4_1 a314 \/
% 0.20/0.51     c4_2 a344 $_56 \/ c5_0 \/ c5_1 a344 \/ definitionFOFtoCNF_6
% 0.20/0.51  |- ~c4_1 a353 \/ c1_2 a353 $_56 \/ c3_0 \/ c3_2 a353 $_56 \/ c4_0 \/
% 0.20/0.51     c4_1 a314 \/ c4_2 a353 $_56 \/ c5_1 a353 \/ definitionFOFtoCNF_4
% 0.20/0.51  |- ~c4_1 a355 \/ c1_2 a355 $_56 \/ c3_2 a355 $_56 \/ c4_0 \/ c4_1 a314 \/
% 0.20/0.51     c4_2 a355 $_56 \/ c5_1 a355
% 0.20/0.51  |- ~c4_1 $_55 \/ c1_0 \/ c1_2 $_55 $_56 \/ c3_1 $_55 \/ c3_2 $_55 $_56 \/
% 0.20/0.51     c4_0 \/ c4_1 a314 \/ c4_2 $_55 $_56 \/ c5_1 $_55
% 0.20/0.51  |- ~c4_1 a329 \/ c1_2 a329 $_61 \/ c3_2 a329 $_61 \/ c4_0 \/
% 0.20/0.51     c4_2 a329 $_61 \/ c5_1 a328 \/ c5_1 a329 \/ ndr1_1 a314
% 0.20/0.51  |- ~c4_1 a335 \/ c1_2 a335 $_61 \/ c3_2 a335 $_61 \/ c4_0 \/
% 0.20/0.51     c4_2 a335 $_61 \/ c5_0 \/ c5_1 a335 \/ ndr1_1 a314
% 0.20/0.51  |- ~c4_1 a344 \/ c1_2 a344 $_61 \/ c3_2 a344 $_61 \/ c4_0 \/
% 0.20/0.51     c4_2 a344 $_61 \/ c5_0 \/ c5_1 a344 \/ definitionFOFtoCNF_6 \/
% 0.20/0.51     ndr1_1 a314
% 0.20/0.51  |- ~c4_1 a353 \/ c1_2 a353 $_61 \/ c3_0 \/ c3_2 a353 $_61 \/ c4_0 \/
% 0.20/0.51     c4_2 a353 $_61 \/ c5_1 a353 \/ definitionFOFtoCNF_4 \/ ndr1_1 a314
% 0.20/0.51  |- ~c4_1 a355 \/ c1_2 a355 $_61 \/ c3_2 a355 $_61 \/ c4_0 \/
% 0.20/0.51     c4_2 a355 $_61 \/ c5_1 a355 \/ ndr1_1 a314
% 0.20/0.51  |- ~c4_1 $_60 \/ c1_0 \/ c1_2 $_60 $_61 \/ c3_1 $_60 \/ c3_2 $_60 $_61 \/
% 0.20/0.51     c4_0 \/ c4_2 $_60 $_61 \/ c5_1 $_60 \/ ndr1_1 a314
% 0.20/0.51  |- ~c1_2 a314 a315 \/ ~c4_1 $_75 \/ c1_0 \/ c1_2 $_75 $_76 \/ c3_1 $_75 \/
% 0.20/0.51     c3_2 $_75 $_76 \/ c4_0 \/ c4_2 $_75 $_76 \/ c5_1 $_75
% 0.20/0.52  |- ~c2_2 a314 a315 \/ ~c4_1 $_77 \/ c1_0 \/ c1_2 $_77 $_78 \/ c3_1 $_77 \/
% 0.20/0.52     c3_2 $_77 $_78 \/ c4_0 \/ c4_2 $_77 $_78 \/ c5_1 $_77
% 0.20/0.52  |- ~c3_2 a314 a315 \/ ~c4_1 $_79 \/ c1_0 \/ c1_2 $_79 $_80 \/ c3_1 $_79 \/
% 0.20/0.52     c3_2 $_79 $_80 \/ c4_0 \/ c4_2 $_79 $_80 \/ c5_1 $_79
% 0.20/0.52  |- c1_0 \/ c2_2 a343 $_88 \/ c3_0 \/ c3_1 a343 \/ c3_2 a343 $_88 \/
% 0.20/0.52     c4_2 a343 $_88 \/ c5_0 \/ c5_1 a343
% 0.20/0.52  |- ~c2_1 $_94 \/ c1_1 $_97 \/ c2_1 a324 \/ c4_1 $_94 \/ c4_1 a324 \/
% 0.20/0.52     c4_2 a324 $_96 \/ c5_0 \/ c5_1 $_97 \/ c5_2 a324 $_96 \/
% 0.20/0.52     definitionFOFtoCNF_7
% 0.20/0.52  |- ~c2_1 $_94 \/ c1_1 $_97 \/ c2_1 a329 \/ c4_0 \/ c4_1 $_94 \/
% 0.20/0.52     c4_1 a329 \/ c4_2 a329 $_96 \/ c5_1 $_97 \/ c5_1 a328 \/ c5_2 a329 $_96
% 0.20/0.52  |- ~c2_1 $_94 \/ c1_1 $_97 \/ c2_1 a335 \/ c4_0 \/ c4_1 $_94 \/
% 0.20/0.52     c4_1 a335 \/ c4_2 a335 $_96 \/ c5_0 \/ c5_1 $_97 \/ c5_2 a335 $_96
% 0.20/0.52  |- ~c2_1 $_94 \/ c1_1 $_97 \/ c2_1 a344 \/ c4_1 $_94 \/ c4_1 a344 \/
% 0.20/0.52     c4_2 a344 $_96 \/ c5_0 \/ c5_1 $_97 \/ c5_2 a344 $_96 \/
% 0.20/0.52     definitionFOFtoCNF_6
% 0.20/0.52  |- ~c2_1 $_94 \/ c1_1 $_97 \/ c2_1 a353 \/ c3_0 \/ c4_1 $_94 \/
% 0.20/0.52     c4_1 a353 \/ c4_2 a353 $_96 \/ c5_1 $_97 \/ c5_2 a353 $_96 \/
% 0.20/0.52     definitionFOFtoCNF_4
% 0.20/0.52  |- ~c2_1 $_94 \/ c1_1 $_97 \/ c2_1 a355 \/ c4_1 $_94 \/ c4_1 a355 \/
% 0.20/0.52     c4_2 a355 $_96 \/ c5_1 $_97 \/ c5_2 a355 $_96
% 0.20/0.52  |- ~c2_1 $_94 \/ c1_0 \/ c1_1 $_97 \/ c2_1 $_95 \/ c3_1 $_95 \/
% 0.20/0.52     c4_1 $_94 \/ c4_1 $_95 \/ c4_2 $_95 $_96 \/ c5_1 $_95 \/ c5_1 $_97 \/
% 0.20/0.52     c5_2 $_95 $_96
% 0.20/0.52  |- c1_1 $_101 \/ c2_1 a355 \/ c3_0 \/ c4_1 a343 \/ c4_1 a355 \/ c5_1 $_101
% 0.20/0.52  |- ~c2_2 a348 a334 \/ ~c3_1 $_105 \/ ~c4_2 $_105 $_106 \/ ~ndr1_1 $_105 \/
% 0.20/0.52     ~ndr1_1 a348 \/ c1_0 \/ c1_2 $_105 $_106 \/ c3_1 a348 \/ c5_1 a348 \/
% 0.20/0.52     c5_2 $_105 $_106 \/ c5_2 a348 a334 \/ definitionFOFtoCNF_0 $_105
% 0.20/0.52  |- c1_1 $_111 \/ c2_1 a324 \/ c3_0 \/ c4_1 a324 \/ c4_1 a343 \/
% 0.20/0.52     c4_2 a324 $_110 \/ c5_0 \/ c5_1 $_111 \/ c5_2 a324 $_110 \/
% 0.20/0.52     definitionFOFtoCNF_7
% 0.20/0.52  |- c1_1 $_114 \/ c1_2 a324 a321 \/ c2_1 a324 \/ c2_2 a324 a321 \/ c3_0 \/
% 0.20/0.52     c4_1 a324 \/ c4_1 a343 \/ c4_2 a324 a321 \/ c5_0 \/ c5_1 $_114 \/
% 0.20/0.52     definitionFOFtoCNF_5 a324 \/ definitionFOFtoCNF_7
% 0.20/0.52  |- c1_1 $_118 \/ c2_1 a344 \/ c3_0 \/ c4_1 a343 \/ c4_1 a344 \/
% 0.20/0.52     c4_2 a344 $_117 \/ c5_0 \/ c5_1 $_118 \/ c5_2 a344 $_117 \/
% 0.20/0.52     definitionFOFtoCNF_6
% 0.20/0.52  |- ~c1_2 a344 $_119 \/ ~c2_2 a344 $_119 \/ ~ndr1_1 a344 \/ c1_1 $_120 \/
% 0.20/0.52     c2_1 a344 \/ c3_0 \/ c4_1 a343 \/ c4_1 a344 \/ c4_2 a344 $_119 \/
% 0.20/0.52     c5_0 \/ c5_1 $_120 \/ definitionFOFtoCNF_6
% 0.20/0.52  |- c1_1 $_121 \/ c1_2 a344 a321 \/ c2_1 a344 \/ c2_2 a344 a321 \/ c3_0 \/
% 0.20/0.52     c4_1 a343 \/ c4_1 a344 \/ c4_2 a344 a321 \/ c5_0 \/ c5_1 $_121 \/
% 0.20/0.52     definitionFOFtoCNF_5 a344 \/ definitionFOFtoCNF_6
% 0.20/0.52  |- c1_1 $_125 \/ c2_1 a335 \/ c3_0 \/ c4_0 \/ c4_1 a335 \/ c4_1 a343 \/
% 0.20/0.52     c4_2 a335 $_124 \/ c5_0 \/ c5_1 $_125 \/ c5_2 a335 $_124
% 0.20/0.52  |- c1_1 $_128 \/ c1_2 a335 a321 \/ c2_1 a335 \/ c2_2 a335 a321 \/ c3_0 \/
% 0.20/0.52     c4_0 \/ c4_1 a335 \/ c4_1 a343 \/ c4_2 a335 a321 \/ c5_0 \/
% 0.20/0.52     c5_1 $_128 \/ definitionFOFtoCNF_5 a335
% 0.20/0.52  |- c1_1 $_132 \/ c2_1 a353 \/ c3_0 \/ c4_1 a343 \/ c4_1 a353 \/
% 0.20/0.52     c4_2 a353 $_131 \/ c5_1 $_132 \/ c5_2 a353 $_131 \/ definitionFOFtoCNF_4
% 0.20/0.52  |- ~c2_2 a353 $_133 \/ ~ndr1_1 a353 \/ c1_1 $_134 \/ c2_1 a353 \/ c3_0 \/
% 0.20/0.52     c3_2 a353 $_133 \/ c4_1 a343 \/ c4_1 a353 \/ c4_2 a353 $_133 \/
% 0.20/0.52     c5_1 $_134 \/ definitionFOFtoCNF_4
% 0.20/0.52  |- c1_1 $_135 \/ c1_2 a353 a321 \/ c2_1 a353 \/ c2_2 a353 a321 \/ c3_0 \/
% 0.20/0.52     c4_1 a343 \/ c4_1 a353 \/ c4_2 a353 a321 \/ c5_1 $_135 \/
% 0.20/0.52     definitionFOFtoCNF_4 \/ definitionFOFtoCNF_5 a353
% 0.20/0.52  |- ~c2_2 a348 $X14 \/ ~c3_1 a353 \/ ~c4_2 a348 $X14 \/ ~ndr1_1 a348 \/
% 0.20/0.52     ~ndr1_1 a353 \/ c1_1 $_136 \/ c1_2 a353 a321 \/ c2_1 a353 \/
% 0.20/0.52     c2_2 a353 a321 \/ c3_0 \/ c4_1 a343 \/ c4_1 a353 \/ c5_1 $_136 \/
% 0.20/0.52     c5_2 a348 $X14 \/ c5_2 a353 a321 \/ definitionFOFtoCNF_0 a353 \/
% 0.20/0.52     definitionFOFtoCNF_4 \/ definitionFOFtoCNF_5 a353
% 0.20/0.52  |- c1_1 $_141 \/ c2_1 a329 \/ c3_0 \/ c4_0 \/ c4_1 a329 \/ c4_1 a343 \/
% 0.20/0.52     c4_2 a329 $_140 \/ c5_1 $_141 \/ c5_1 a328 \/ c5_2 a329 $_140
% 0.20/0.52  |- c1_1 $_144 \/ c1_2 a329 a321 \/ c2_1 a329 \/ c2_2 a329 a321 \/ c3_0 \/
% 0.20/0.52     c4_0 \/ c4_1 a329 \/ c4_1 a343 \/ c4_2 a329 a321 \/ c5_1 $_144 \/
% 0.20/0.52     c5_1 a328 \/ definitionFOFtoCNF_5 a329
% 0.20/0.52  |- ~c1_2 a314 $_146 \/ ~c4_1 $_147 \/ ~ndr1_1 a314 \/ c1_0 \/
% 0.20/0.52     c1_2 $_147 $_148 \/ c3_1 $_147 \/ c3_2 $_147 $_148 \/ c3_2 a314 $_146 \/
% 0.20/0.52     c4_0 \/ c4_2 $_147 $_148 \/ c4_2 a314 $_146 \/ c5_1 $_147
% 0.20/0.52  |- ~c3_1 a324 \/ ~c3_1 a348 \/ c1_1 $_154 \/ c1_2 a324 a321 \/ c2_1 a324 \/
% 0.20/0.52     c2_2 a324 a321 \/ c3_0 \/ c4_1 a324 \/ c4_1 a343 \/ c5_0 \/
% 0.20/0.52     c5_1 $_154 \/ c5_2 a324 a321 \/ definitionFOFtoCNF_0 a324 \/
% 0.20/0.52     definitionFOFtoCNF_5 a324 \/ definitionFOFtoCNF_7
% 0.20/0.52  |- ~c3_1 a324 \/ c1_1 $_156 \/ c1_2 a324 a321 \/ c2_1 a324 \/
% 0.20/0.52     c2_2 a324 a321 \/ c3_0 \/ c4_1 a324 \/ c4_1 a343 \/ c5_0 \/
% 0.20/0.52     c5_1 $_156 \/ c5_2 a324 a321 \/ definitionFOFtoCNF_0 a324 \/
% 0.20/0.52     definitionFOFtoCNF_5 a324 \/ definitionFOFtoCNF_7 \/ ndr1_1 a348
% 0.20/0.52  |- ~c3_1 a335 \/ ~c3_1 a348 \/ c1_1 $_158 \/ c1_2 a335 a321 \/ c2_1 a335 \/
% 0.20/0.52     c2_2 a335 a321 \/ c3_0 \/ c4_0 \/ c4_1 a335 \/ c4_1 a343 \/ c5_0 \/
% 0.20/0.52     c5_1 $_158 \/ c5_2 a335 a321 \/ definitionFOFtoCNF_0 a335 \/
% 0.20/0.52     definitionFOFtoCNF_5 a335
% 0.20/0.52  |- ~c3_1 a335 \/ c1_1 $_160 \/ c1_2 a335 a321 \/ c2_1 a335 \/
% 0.20/0.52     c2_2 a335 a321 \/ c3_0 \/ c4_0 \/ c4_1 a335 \/ c4_1 a343 \/ c5_0 \/
% 0.20/0.52     c5_1 $_160 \/ c5_2 a335 a321 \/ definitionFOFtoCNF_0 a335 \/
% 0.20/0.52     definitionFOFtoCNF_5 a335 \/ ndr1_1 a348
% 0.20/0.52  |- ~c3_1 a348 \/ ~c3_1 a353 \/ c1_1 $_162 \/ c1_2 a353 a321 \/ c2_1 a353 \/
% 0.20/0.52     c2_2 a353 a321 \/ c3_0 \/ c4_1 a343 \/ c4_1 a353 \/ c5_1 $_162 \/
% 0.20/0.52     c5_2 a353 a321 \/ definitionFOFtoCNF_0 a353 \/ definitionFOFtoCNF_4 \/
% 0.20/0.52     definitionFOFtoCNF_5 a353
% 0.20/0.52  |- ~c3_1 a353 \/ c1_1 $_164 \/ c1_2 a353 a321 \/ c2_1 a353 \/
% 0.20/0.52     c2_2 a353 a321 \/ c3_0 \/ c4_1 a343 \/ c4_1 a353 \/ c5_1 $_164 \/
% 0.20/0.52     c5_2 a353 a321 \/ definitionFOFtoCNF_0 a353 \/ definitionFOFtoCNF_4 \/
% 0.20/0.52     definitionFOFtoCNF_5 a353 \/ ndr1_1 a348
% 0.20/0.52  |- c1_0 \/ c1_1 $_169 \/ c2_1 $_167 \/ c3_0 \/ c3_1 $_167 \/ c4_1 $_167 \/
% 0.20/0.52     c4_1 a343 \/ c4_2 $_167 $_168 \/ c5_1 $_167 \/ c5_1 $_169 \/
% 0.20/0.52     c5_2 $_167 $_168
% 0.20/0.52  |- ~c3_1 $X15 \/ ~c4_2 $X15 $X16 \/ ~ndr1_1 $X15 \/ c1_0 \/ c1_1 $_172 \/
% 0.20/0.52     c1_2 $X15 $X16 \/ c2_1 a348 \/ c3_0 \/ c3_1 a348 \/ c4_1 a343 \/
% 0.20/0.52     c4_1 a348 \/ c4_2 a348 a349 \/ c5_1 $_172 \/ c5_1 a348 \/
% 0.20/0.52     c5_2 $X15 $X16 \/ definitionFOFtoCNF_0 $X15
% 0.20/0.52  |- ~c3_1 a324 \/ c1_1 $_173 \/ c1_2 a324 a321 \/ c2_1 a324 \/
% 0.20/0.52     c2_2 a324 a321 \/ c2_2 a348 a349 \/ c3_0 \/ c4_1 a324 \/ c4_1 a343 \/
% 0.20/0.52     c5_0 \/ c5_1 $_173 \/ c5_2 a324 a321 \/ definitionFOFtoCNF_0 a324 \/
% 0.20/0.52     definitionFOFtoCNF_5 a324 \/ definitionFOFtoCNF_7
% 0.20/0.52  |- ~c3_1 a335 \/ c1_1 $_175 \/ c1_2 a335 a321 \/ c2_1 a335 \/
% 0.20/0.52     c2_2 a335 a321 \/ c2_2 a348 a349 \/ c3_0 \/ c4_0 \/ c4_1 a335 \/
% 0.20/0.52     c4_1 a343 \/ c5_0 \/ c5_1 $_175 \/ c5_2 a335 a321 \/
% 0.20/0.52     definitionFOFtoCNF_0 a335 \/ definitionFOFtoCNF_5 a335
% 0.20/0.52  |- ~c3_1 a329 \/ ~c3_1 a348 \/ c1_1 $_177 \/ c1_2 a329 a321 \/ c2_1 a329 \/
% 0.20/0.52     c2_2 a329 a321 \/ c3_0 \/ c4_0 \/ c4_1 a329 \/ c4_1 a343 \/
% 0.20/0.52     c5_1 $_177 \/ c5_1 a328 \/ c5_2 a329 a321 \/
% 0.20/0.52     definitionFOFtoCNF_0 a329 \/ definitionFOFtoCNF_5 a329
% 0.20/0.52  |- ~c3_1 a329 \/ c1_1 $_179 \/ c1_2 a329 a321 \/ c2_1 a329 \/
% 0.20/0.52     c2_2 a329 a321 \/ c3_0 \/ c4_0 \/ c4_1 a329 \/ c4_1 a343 \/
% 0.20/0.52     c5_1 $_179 \/ c5_1 a328 \/ c5_2 a329 a321 \/
% 0.20/0.52     definitionFOFtoCNF_0 a329 \/ definitionFOFtoCNF_5 a329 \/ ndr1_1 a348
% 0.20/0.52  |- ~c3_1 a353 \/ c1_1 $_181 \/ c1_2 a353 a321 \/ c2_1 a353 \/
% 0.20/0.52     c2_2 a348 a349 \/ c2_2 a353 a321 \/ c3_0 \/ c4_1 a343 \/ c4_1 a353 \/
% 0.20/0.52     c5_1 $_181 \/ c5_2 a353 a321 \/ definitionFOFtoCNF_0 a353 \/
% 0.20/0.52     definitionFOFtoCNF_4 \/ definitionFOFtoCNF_5 a353
% 0.20/0.52  |- ~c3_1 a329 \/ c1_1 $_183 \/ c1_2 a329 a321 \/ c2_1 a329 \/
% 0.20/0.52     c2_2 a329 a321 \/ c2_2 a348 a349 \/ c3_0 \/ c4_0 \/ c4_1 a329 \/
% 0.20/0.52     c4_1 a343 \/ c5_1 $_183 \/ c5_1 a328 \/ c5_2 a329 a321 \/
% 0.20/0.52     definitionFOFtoCNF_0 a329 \/ definitionFOFtoCNF_5 a329
% 0.20/0.52  |- ~c3_1 a344 \/ c1_1 $_185 \/ c1_2 a344 a321 \/ c2_1 a344 \/
% 0.20/0.52     c2_2 a344 a321 \/ c3_0 \/ c4_1 a343 \/ c4_1 a344 \/ c5_0 \/
% 0.20/0.52     c5_1 $_185 \/ c5_2 a344 a321 \/ definitionFOFtoCNF_0 a344 \/
% 0.20/0.52     definitionFOFtoCNF_5 a344 \/ definitionFOFtoCNF_6 \/ ndr1_1 a348
% 0.20/0.52  |- ~c3_1 a344 \/ ~c3_1 a348 \/ c1_1 $_187 \/ c1_2 a344 a321 \/ c2_1 a344 \/
% 0.20/0.52     c2_2 a344 a321 \/ c3_0 \/ c4_1 a343 \/ c4_1 a344 \/ c5_0 \/
% 0.20/0.52     c5_1 $_187 \/ c5_2 a344 a321 \/ definitionFOFtoCNF_0 a344 \/
% 0.20/0.52     definitionFOFtoCNF_5 a344 \/ definitionFOFtoCNF_6
% 0.20/0.52  |- c1_0 \/ c1_1 $_190 \/ c1_2 $_189 a321 \/ c2_1 $_189 \/
% 0.20/0.52     c2_2 $_189 a321 \/ c3_0 \/ c3_1 $_189 \/ c4_1 $_189 \/ c4_1 a343 \/
% 0.20/0.52     c4_2 $_189 a321 \/ c5_1 $_189 \/ c5_1 $_190 \/
% 0.20/0.52     definitionFOFtoCNF_5 $_189
% 0.20/0.52  |- ~c3_1 a344 \/ c1_1 $_193 \/ c1_2 a344 a321 \/ c2_1 a344 \/
% 0.20/0.52     c2_2 a344 a321 \/ c2_2 a348 a349 \/ c3_0 \/ c4_1 a343 \/ c4_1 a344 \/
% 0.20/0.52     c5_0 \/ c5_1 $_193 \/ c5_2 a344 a321 \/ definitionFOFtoCNF_0 a344 \/
% 0.20/0.52     definitionFOFtoCNF_5 a344 \/ definitionFOFtoCNF_6
% 0.20/0.52  |- ~c3_1 a324 \/ c1_0 \/ c1_1 $_197 \/ c1_2 a324 a321 \/ c2_1 a324 \/
% 0.20/0.52     c2_2 a324 a321 \/ c3_0 \/ c3_1 a348 \/ c4_1 a324 \/ c4_1 a343 \/ c5_0 \/
% 0.20/0.52     c5_1 $_197 \/ c5_1 a348 \/ c5_2 a324 a321 \/ c5_2 a348 a334 \/
% 0.20/0.52     definitionFOFtoCNF_0 a324 \/ definitionFOFtoCNF_5 a324 \/
% 0.20/0.52     definitionFOFtoCNF_7
% 0.20/0.52  |- ~c3_1 a335 \/ c1_0 \/ c1_1 $_201 \/ c1_2 a335 a321 \/ c2_1 a335 \/
% 0.20/0.52     c2_2 a335 a321 \/ c3_0 \/ c3_1 a348 \/ c4_0 \/ c4_1 a335 \/ c4_1 a343 \/
% 0.20/0.52     c5_0 \/ c5_1 $_201 \/ c5_1 a348 \/ c5_2 a335 a321 \/ c5_2 a348 a334 \/
% 0.20/0.52     definitionFOFtoCNF_0 a335 \/ definitionFOFtoCNF_5 a335
% 0.20/0.52  |- ~c3_1 a329 \/ c1_0 \/ c1_1 $_205 \/ c1_2 a329 a321 \/ c2_1 a329 \/
% 0.20/0.52     c2_2 a329 a321 \/ c3_0 \/ c3_1 a348 \/ c4_0 \/ c4_1 a329 \/ c4_1 a343 \/
% 0.20/0.52     c5_1 $_205 \/ c5_1 a328 \/ c5_1 a348 \/ c5_2 a329 a321 \/
% 0.20/0.52     c5_2 a348 a334 \/ definitionFOFtoCNF_0 a329 \/ definitionFOFtoCNF_5 a329
% 0.20/0.52  |- ~c3_1 a353 \/ c1_0 \/ c1_1 $_209 \/ c1_2 a353 a321 \/ c2_1 a353 \/
% 0.20/0.52     c2_2 a353 a321 \/ c3_0 \/ c3_1 a348 \/ c4_1 a343 \/ c4_1 a353 \/
% 0.20/0.52     c5_1 $_209 \/ c5_1 a348 \/ c5_2 a348 a334 \/ c5_2 a353 a321 \/
% 0.20/0.52     definitionFOFtoCNF_0 a353 \/ definitionFOFtoCNF_4 \/
% 0.20/0.52     definitionFOFtoCNF_5 a353
% 0.20/0.52  |- ~c3_1 a344 \/ c1_0 \/ c1_1 $_213 \/ c1_2 a344 a321 \/ c2_1 a344 \/
% 0.20/0.52     c2_2 a344 a321 \/ c3_0 \/ c3_1 a348 \/ c4_1 a343 \/ c4_1 a344 \/ c5_0 \/
% 0.20/0.52     c5_1 $_213 \/ c5_1 a348 \/ c5_2 a344 a321 \/ c5_2 a348 a334 \/
% 0.20/0.52     definitionFOFtoCNF_0 a344 \/ definitionFOFtoCNF_5 a344 \/
% 0.20/0.52     definitionFOFtoCNF_6
% 0.20/0.52  |- ~c3_1 a353 \/ c1_0 \/ c1_1 $_220 \/ c1_1 $_221 \/ c1_2 a353 a321 \/
% 0.20/0.52     c2_1 a348 \/ c2_1 a353 \/ c2_2 a353 a321 \/ c3_0 \/ c3_1 a348 \/
% 0.20/0.52     c4_1 a343 \/ c4_1 a348 \/ c4_1 a353 \/ c4_2 a348 a349 \/ c5_1 $_220 \/
% 0.20/0.52     c5_1 $_221 \/ c5_1 a348 \/ c5_2 a353 a321 \/
% 0.20/0.52     definitionFOFtoCNF_0 a353 \/ definitionFOFtoCNF_4 \/
% 0.20/0.52     definitionFOFtoCNF_5 a353
% 0.20/0.52  |- ~c3_1 a324 \/ c1_0 \/ c1_1 $_224 \/ c1_1 $_225 \/ c1_2 a324 a321 \/
% 0.20/0.52     c2_1 a324 \/ c2_1 a348 \/ c2_2 a324 a321 \/ c3_0 \/ c3_1 a348 \/
% 0.20/0.52     c4_1 a324 \/ c4_1 a343 \/ c4_1 a348 \/ c4_2 a348 a349 \/ c5_0 \/
% 0.20/0.52     c5_1 $_224 \/ c5_1 $_225 \/ c5_1 a348 \/ c5_2 a324 a321 \/
% 0.20/0.52     definitionFOFtoCNF_0 a324 \/ definitionFOFtoCNF_5 a324 \/
% 0.20/0.52     definitionFOFtoCNF_7
% 0.20/0.52  |- ~c3_1 a335 \/ c1_0 \/ c1_1 $_228 \/ c1_1 $_229 \/ c1_2 a335 a321 \/
% 0.20/0.52     c2_1 a335 \/ c2_1 a348 \/ c2_2 a335 a321 \/ c3_0 \/ c3_1 a348 \/ c4_0 \/
% 0.20/0.52     c4_1 a335 \/ c4_1 a343 \/ c4_1 a348 \/ c4_2 a348 a349 \/ c5_0 \/
% 0.20/0.52     c5_1 $_228 \/ c5_1 $_229 \/ c5_1 a348 \/ c5_2 a335 a321 \/
% 0.20/0.52     definitionFOFtoCNF_0 a335 \/ definitionFOFtoCNF_5 a335
% 0.20/0.52  |- ~c3_1 a344 \/ c1_0 \/ c1_1 $_232 \/ c1_1 $_233 \/ c1_2 a344 a321 \/
% 0.20/0.52     c2_1 a344 \/ c2_1 a348 \/ c2_2 a344 a321 \/ c3_0 \/ c3_1 a348 \/
% 0.20/0.52     c4_1 a343 \/ c4_1 a344 \/ c4_1 a348 \/ c4_2 a348 a349 \/ c5_0 \/
% 0.20/0.52     c5_1 $_232 \/ c5_1 $_233 \/ c5_1 a348 \/ c5_2 a344 a321 \/
% 0.20/0.52     definitionFOFtoCNF_0 a344 \/ definitionFOFtoCNF_5 a344 \/
% 0.20/0.52     definitionFOFtoCNF_6
% 0.20/0.52  |- ~c3_1 a329 \/ c1_0 \/ c1_1 $_236 \/ c1_1 $_237 \/ c1_2 a329 a321 \/
% 0.20/0.52     c2_1 a329 \/ c2_1 a348 \/ c2_2 a329 a321 \/ c3_0 \/ c3_1 a348 \/ c4_0 \/
% 0.20/0.52     c4_1 a329 \/ c4_1 a343 \/ c4_1 a348 \/ c4_2 a348 a349 \/ c5_1 $_236 \/
% 0.20/0.52     c5_1 $_237 \/ c5_1 a328 \/ c5_1 a348 \/ c5_2 a329 a321 \/
% 0.20/0.52     definitionFOFtoCNF_0 a329 \/ definitionFOFtoCNF_5 a329
% 0.20/0.52  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.52  
%------------------------------------------------------------------------------