%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN533+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n025.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:45 EDT 2022 % Result : CounterSatisfiable 0.18s 0.40s % Output : Saturation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SYN533+1 : TPTP v8.1.0. Released v2.1.0. % 0.06/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n025.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 : Tue Jul 12 00:31:32 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.18/0.40 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.40 % 0.18/0.40 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.40 |- c4_0 % 0.18/0.40 |- ~c3_1 a467 \/ c1_0 % 0.18/0.40 |- c1_0 \/ c4_1 a467 % 0.18/0.40 |- c1_0 \/ c5_1 a467 % 0.18/0.40 |- c1_0 \/ ndr1_0 % 0.18/0.40 |- ~c2_1 a464 \/ c2_0 % 0.18/0.40 |- ~c5_1 a464 \/ c2_0 % 0.18/0.40 |- c2_0 \/ c3_1 a464 % 0.18/0.40 |- c2_0 \/ ndr1_0 % 0.18/0.40 |- ~c4_2 a465 a466 \/ c2_0 % 0.18/0.40 |- ~c5_1 a465 \/ c2_0 % 0.18/0.40 |- ~c5_2 a465 a466 \/ c2_0 % 0.18/0.40 |- c1_2 a465 a466 \/ c2_0 % 0.18/0.40 |- c2_0 \/ ndr1_1 a465 % 0.18/0.40 |- ~c2_2 a445 a446 \/ c3_0 % 0.18/0.40 |- ~c4_2 a445 a446 \/ c3_0 % 0.18/0.40 |- c3_0 \/ c3_1 a445 % 0.18/0.40 |- c3_0 \/ ndr1_0 % 0.18/0.40 |- c3_0 \/ ndr1_1 a445 % 0.18/0.40 |- ~c1_1 $X7 \/ ~c3_1 $X9 \/ ~c4_1 $X7 \/ ~ndr1_0 \/ ~ndr1_1 $X7 \/ % 0.18/0.40 c2_1 $X9 \/ c2_2 $X7 $X8 \/ c4_2 $X7 $X8 \/ c5_2 $X7 $X8 % 0.18/0.40 |- ~c1_0 \/ ~c2_2 $U $V \/ ~c3_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c2_0 \/ % 0.18/0.40 c2_1 $U \/ c5_2 $U $V % 0.18/0.40 |- ~c1_2 a453 a454 \/ ~definitionFOFtoCNF_0 % 0.18/0.40 |- ~c3_2 a453 a454 \/ ~definitionFOFtoCNF_0 % 0.18/0.40 |- ~c4_1 a453 \/ ~definitionFOFtoCNF_0 % 0.18/0.40 |- ~definitionFOFtoCNF_0 \/ c5_2 a453 a454 % 0.18/0.40 |- ~definitionFOFtoCNF_0 \/ ndr1_0 % 0.18/0.40 |- ~definitionFOFtoCNF_0 \/ ndr1_1 a453 % 0.18/0.40 |- ~c5_2 a453 a454 \/ ~ndr1_0 \/ ~ndr1_1 a453 \/ c1_2 a453 a454 \/ % 0.18/0.40 c3_2 a453 a454 \/ c4_1 a453 \/ definitionFOFtoCNF_0 % 0.18/0.40 |- ~c1_0 \/ ~c1_1 a455 \/ definitionFOFtoCNF_0 % 0.18/0.40 |- ~c1_0 \/ ~c4_2 a455 a456 \/ definitionFOFtoCNF_0 % 0.18/0.40 |- ~c1_0 \/ ~c4_2 a455 a457 \/ definitionFOFtoCNF_0 % 0.18/0.40 |- ~c1_0 \/ c1_2 a455 a457 \/ definitionFOFtoCNF_0 % 0.18/0.40 |- ~c1_0 \/ c2_2 a455 a456 \/ definitionFOFtoCNF_0 % 0.18/0.40 |- ~c1_0 \/ c2_2 a455 a457 \/ definitionFOFtoCNF_0 % 0.18/0.40 |- ~c1_0 \/ c3_2 a455 a456 \/ definitionFOFtoCNF_0 % 0.18/0.40 |- ~c1_0 \/ definitionFOFtoCNF_0 \/ ndr1_0 % 0.18/0.40 |- ~c1_0 \/ definitionFOFtoCNF_0 \/ ndr1_1 a455 % 0.18/0.40 |- ~c2_0 \/ ~c4_2 a461 a462 \/ c1_0 % 0.18/0.40 |- ~c2_0 \/ ~c5_2 a461 a462 \/ c1_0 % 0.18/0.40 |- ~c1_1 a460 \/ ~definitionFOFtoCNF_1 % 0.18/0.40 |- ~definitionFOFtoCNF_1 \/ c2_1 a460 % 0.18/0.40 |- ~definitionFOFtoCNF_1 \/ ndr1_0 % 0.18/0.40 |- ~definitionFOFtoCNF_1 \/ ~ndr1_1 a460 \/ c3_2 a460 $X6 % 0.18/0.40 |- ~c2_1 a460 \/ ~c3_2 a460 skolemFOFtoCNF_X6 \/ ~ndr1_0 \/ c1_1 a460 \/ % 0.18/0.40 definitionFOFtoCNF_1 % 0.18/0.40 |- ~c2_1 a460 \/ ~ndr1_0 \/ c1_1 a460 \/ definitionFOFtoCNF_1 \/ % 0.18/0.40 ndr1_1 a460 % 0.18/0.40 |- ~c1_2 a458 a459 \/ ~c3_0 \/ definitionFOFtoCNF_1 % 0.18/0.40 |- ~c3_0 \/ ~c3_2 a458 a459 \/ definitionFOFtoCNF_1 % 0.18/0.40 |- ~c3_0 \/ ~c5_1 a458 \/ definitionFOFtoCNF_1 % 0.18/0.40 |- ~c3_0 \/ c1_1 a458 \/ definitionFOFtoCNF_1 % 0.18/0.40 |- ~c3_0 \/ c5_2 a458 a459 \/ definitionFOFtoCNF_1 % 0.18/0.40 |- ~c3_0 \/ definitionFOFtoCNF_1 \/ ndr1_0 % 0.18/0.40 |- ~c3_0 \/ definitionFOFtoCNF_1 \/ ndr1_1 a458 % 0.18/0.40 |- ~c2_2 a451 a452 \/ ~c5_0 \/ c2_0 % 0.18/0.40 |- ~c4_1 a451 \/ ~c5_0 \/ c2_0 % 0.18/0.40 |- ~c5_0 \/ c2_0 \/ c3_1 a451 % 0.18/0.40 |- ~c5_0 \/ c2_0 \/ c3_2 a451 a452 % 0.18/0.40 |- ~c5_0 \/ c2_0 \/ ndr1_1 a451 % 0.18/0.40 |- ~c1_1 $X1 \/ ~c3_2 $X1 $X2 \/ ~ndr1_0 \/ ~ndr1_1 $X1 \/ c1_0 \/ c3_0 \/ % 0.18/0.40 c4_2 $X1 $X2 \/ c5_2 $X1 $X2 % 0.18/0.40 |- ~c2_1 $W \/ ~c3_2 $X $Z \/ ~c5_2 $X $Y \/ ~ndr1_0 \/ ~ndr1_1 $X \/ % 0.18/0.40 c1_0 \/ c1_2 $X $Z \/ c3_2 $X $Y \/ c4_2 $X $Z \/ ndr1_1 $W % 0.18/0.40 |- ~c1_2 $W a443 \/ ~c2_1 $W \/ ~c3_2 $W a444 \/ ~c3_2 $X $Z \/ % 0.18/0.40 ~c5_2 $X $Y \/ ~ndr1_0 \/ ~ndr1_1 $X \/ c1_0 \/ c1_2 $X $Z \/ % 0.18/0.40 c3_2 $X $Y \/ c4_2 $X $Z % 0.18/0.40 |- ~c1_2 $W a443 \/ ~c2_1 $W \/ ~c3_2 $X $Z \/ ~c5_2 $W a444 \/ % 0.18/0.40 ~c5_2 $X $Y \/ ~ndr1_0 \/ ~ndr1_1 $X \/ c1_0 \/ c1_2 $X $Z \/ % 0.18/0.40 c3_2 $X $Y \/ c4_2 $X $Z % 0.18/0.40 |- ~c2_1 $W \/ ~c3_2 $W a444 \/ ~c3_2 $X $Z \/ ~c5_2 $X $Y \/ ~ndr1_0 \/ % 0.18/0.40 ~ndr1_1 $X \/ c1_0 \/ c1_2 $X $Z \/ c3_2 $W a443 \/ c3_2 $X $Y \/ % 0.18/0.40 c4_2 $X $Z % 0.18/0.40 |- ~c2_1 $W \/ ~c3_2 $X $Z \/ ~c5_2 $W a444 \/ ~c5_2 $X $Y \/ ~ndr1_0 \/ % 0.18/0.40 ~ndr1_1 $X \/ c1_0 \/ c1_2 $X $Z \/ c3_2 $W a443 \/ c3_2 $X $Y \/ % 0.18/0.40 c4_2 $X $Z % 0.18/0.40 |- ~c2_2 a449 a450 \/ ~definitionFOFtoCNF_2 % 0.18/0.40 |- ~c3_2 a449 a450 \/ ~definitionFOFtoCNF_2 % 0.18/0.40 |- ~definitionFOFtoCNF_2 \/ c1_1 a449 % 0.18/0.40 |- ~definitionFOFtoCNF_2 \/ c2_1 a449 % 0.18/0.40 |- ~definitionFOFtoCNF_2 \/ c5_2 a449 a450 % 0.18/0.40 |- ~definitionFOFtoCNF_2 \/ ndr1_0 % 0.18/0.41 |- ~definitionFOFtoCNF_2 \/ ndr1_1 a449 % 0.18/0.41 |- ~c1_1 a449 \/ ~c2_1 a449 \/ ~c5_2 a449 a450 \/ ~ndr1_0 \/ % 0.18/0.41 ~ndr1_1 a449 \/ c2_2 a449 a450 \/ c3_2 a449 a450 \/ definitionFOFtoCNF_2 % 0.18/0.41 |- ~c1_2 a447 a448 \/ c2_0 \/ definitionFOFtoCNF_2 % 0.18/0.41 |- ~c2_2 a447 a448 \/ c2_0 \/ definitionFOFtoCNF_2 % 0.18/0.41 |- ~c4_2 a447 a448 \/ c2_0 \/ definitionFOFtoCNF_2 % 0.18/0.41 |- c2_0 \/ definitionFOFtoCNF_2 \/ ndr1_1 a447 % 0.18/0.41 |- ~c5_2 a447 $X3 \/ ~ndr1_1 a447 \/ c1_2 a447 $X3 \/ c2_0 \/ % 0.18/0.41 c3_2 a447 $X3 \/ definitionFOFtoCNF_2 % 0.18/0.41 |- ~c1_2 $X10 a468 \/ ~definitionFOFtoCNF_3 $X10 % 0.18/0.41 |- ~definitionFOFtoCNF_3 $X10 \/ c2_2 $X10 a468 % 0.18/0.41 |- ~definitionFOFtoCNF_3 $X10 \/ c5_2 $X10 a468 % 0.18/0.41 |- ~definitionFOFtoCNF_3 $X10 \/ ndr1_1 $X10 % 0.18/0.41 |- ~c2_2 $X10 a468 \/ ~c5_2 $X10 a468 \/ ~ndr1_1 $X10 \/ c1_2 $X10 a468 \/ % 0.18/0.41 definitionFOFtoCNF_3 $X10 % 0.18/0.41 |- ~ndr1_0 \/ c1_1 $X10 \/ c2_2 $X10 a469 \/ definitionFOFtoCNF_3 $X10 % 0.18/0.41 |- ~ndr1_0 \/ c1_1 $X10 \/ c4_2 $X10 a469 \/ definitionFOFtoCNF_3 $X10 % 0.18/0.41 |- ~ndr1_0 \/ c1_1 $X10 \/ c5_2 $X10 a469 \/ definitionFOFtoCNF_3 $X10 % 0.18/0.41 |- ~ndr1_0 \/ c1_1 $X10 \/ definitionFOFtoCNF_3 $X10 \/ ndr1_1 $X10 % 0.18/0.41 |- ~c1_2 $X a443 \/ ~c2_1 $X \/ ~c3_2 $X a444 \/ ~c5_2 $X $Y \/ ~ndr1_0 \/ % 0.18/0.41 ~ndr1_1 $X \/ c1_0 \/ c1_2 $X a444 \/ c3_2 $X $Y \/ c4_2 $X a444 % 0.18/0.41 |- ~c1_2 $X a443 \/ ~c2_1 $X \/ ~c3_2 $X $Z \/ ~c5_2 $X a444 \/ ~ndr1_0 \/ % 0.18/0.41 ~ndr1_1 $X \/ c1_0 \/ c1_2 $X $Z \/ c3_2 $X a444 \/ c4_2 $X $Z % 0.18/0.41 |- ~c2_1 $X \/ ~c3_2 $X a444 \/ ~c5_2 $X $Y \/ ~ndr1_0 \/ ~ndr1_1 $X \/ % 0.18/0.41 c1_0 \/ c1_2 $X a444 \/ c3_2 $X $Y \/ c3_2 $X a443 \/ c4_2 $X a444 % 0.18/0.41 |- ~c2_1 $X \/ ~c3_2 $X $Z \/ ~c5_2 $X a444 \/ ~ndr1_0 \/ ~ndr1_1 $X \/ % 0.18/0.41 c1_0 \/ c1_2 $X $Z \/ c3_2 $X a443 \/ c3_2 $X a444 \/ c4_2 $X $Z % 0.18/0.41 |- c1_0 \/ c2_1 $_5 \/ c3_1 $_5 % 0.18/0.41 |- c1_0 \/ c2_1 a467 % 0.18/0.41 |- c1_1 $_7 \/ c3_0 \/ definitionFOFtoCNF_3 $_7 \/ ndr1_1 $_7 % 0.18/0.41 |- c1_1 $_7 \/ c2_0 \/ definitionFOFtoCNF_3 $_7 \/ ndr1_1 $_7 % 0.18/0.41 |- c1_0 \/ c1_1 $_7 \/ definitionFOFtoCNF_3 $_7 \/ ndr1_1 $_7 % 0.18/0.41 |- c1_1 $_8 \/ c2_2 $_8 a469 \/ c3_0 \/ definitionFOFtoCNF_3 $_8 % 0.18/0.41 |- c1_1 $_8 \/ c2_0 \/ c2_2 $_8 a469 \/ definitionFOFtoCNF_3 $_8 % 0.18/0.41 |- c1_0 \/ c1_1 $_8 \/ c2_2 $_8 a469 \/ definitionFOFtoCNF_3 $_8 % 0.18/0.41 |- c1_1 $_9 \/ c3_0 \/ c4_2 $_9 a469 \/ definitionFOFtoCNF_3 $_9 % 0.18/0.41 |- c1_1 $_9 \/ c2_0 \/ c4_2 $_9 a469 \/ definitionFOFtoCNF_3 $_9 % 0.18/0.41 |- c1_0 \/ c1_1 $_9 \/ c4_2 $_9 a469 \/ definitionFOFtoCNF_3 $_9 % 0.18/0.41 |- c1_1 $_10 \/ c3_0 \/ c5_2 $_10 a469 \/ definitionFOFtoCNF_3 $_10 % 0.18/0.41 |- c1_1 $_10 \/ c2_0 \/ c5_2 $_10 a469 \/ definitionFOFtoCNF_3 $_10 % 0.18/0.41 |- c1_0 \/ c1_1 $_10 \/ c5_2 $_10 a469 \/ definitionFOFtoCNF_3 $_10 % 0.18/0.41 |- ~definitionFOFtoCNF_1 \/ c1_1 a460 \/ c3_0 \/ c3_2 a460 $X6 \/ % 0.18/0.41 definitionFOFtoCNF_3 a460 % 0.18/0.41 |- ~definitionFOFtoCNF_1 \/ c1_1 a460 \/ c2_0 \/ c3_2 a460 $X6 \/ % 0.18/0.41 definitionFOFtoCNF_3 a460 % 0.18/0.41 |- ~definitionFOFtoCNF_1 \/ c1_0 \/ c1_1 a460 \/ c3_2 a460 $X6 \/ % 0.18/0.41 definitionFOFtoCNF_3 a460 % 0.18/0.41 |- c2_0 \/ c3_0 % 0.18/0.41 |- c2_0 \/ c5_2 a458 a459 \/ definitionFOFtoCNF_1 % 0.18/0.41 |- c2_0 \/ definitionFOFtoCNF_1 \/ ndr1_1 a458 % 0.18/0.41 |- c1_1 a458 \/ c2_0 \/ definitionFOFtoCNF_1 % 0.18/0.41 |- c1_0 \/ c2_0 % 0.18/0.41 |- c1_0 \/ c2_2 a461 a463 % 0.18/0.41 |- c1_0 \/ c1_2 a461 a463 % 0.18/0.41 |- c1_0 \/ c1_2 a461 a462 % 0.18/0.41 |- c1_0 \/ ndr1_1 a461 % 0.18/0.41 |- c1_0 \/ c1_1 a461 % 0.18/0.41 |- c1_1 a447 \/ c1_2 a447 a469 \/ c2_0 \/ c3_2 a447 a469 \/ % 0.18/0.41 definitionFOFtoCNF_2 \/ definitionFOFtoCNF_3 a447 % 0.18/0.41 |- ~c1_1 $_33 \/ ~c4_1 $_33 \/ ~ndr1_0 \/ ~ndr1_1 $_33 \/ c1_0 \/ % 0.18/0.41 c2_1 $_35 \/ c2_2 $_33 $_34 \/ c4_2 $_33 $_34 \/ c5_2 $_33 $_34 % 0.18/0.41 |- ~c1_1 a445 \/ ~c3_1 $_35 \/ ~c4_1 a445 \/ ~ndr1_0 \/ c2_1 $_35 \/ % 0.18/0.41 c2_2 a445 $_34 \/ c3_0 \/ c4_2 a445 $_34 \/ c5_2 a445 $_34 % 0.18/0.41 |- ~c1_1 a447 \/ ~c3_1 $_35 \/ ~c4_1 a447 \/ ~ndr1_0 \/ c2_0 \/ % 0.18/0.41 c2_1 $_35 \/ c2_2 a447 $_34 \/ c4_2 a447 $_34 \/ c5_2 a447 $_34 \/ % 0.18/0.41 definitionFOFtoCNF_2 % 0.18/0.41 |- ~c1_1 a458 \/ ~c3_1 $_35 \/ ~c4_1 a458 \/ ~ndr1_0 \/ c2_0 \/ % 0.18/0.41 c2_1 $_35 \/ c2_2 a458 $_34 \/ c4_2 a458 $_34 \/ c5_2 a458 $_34 \/ % 0.18/0.41 definitionFOFtoCNF_1 % 0.18/0.41 |- ~c1_1 a465 \/ ~c3_1 $_35 \/ ~c4_1 a465 \/ ~ndr1_0 \/ c2_0 \/ % 0.18/0.41 c2_1 $_35 \/ c2_2 a465 $_34 \/ c4_2 a465 $_34 \/ c5_2 a465 $_34 % 0.18/0.41 |- ~c1_1 a445 \/ ~c4_1 a445 \/ ~ndr1_0 \/ c1_0 \/ c2_1 $_37 \/ % 0.18/0.41 c2_2 a445 $_36 \/ c3_0 \/ c4_2 a445 $_36 \/ c5_2 a445 $_36 % 0.18/0.41 |- ~c1_1 a461 \/ ~c4_1 a461 \/ ~ndr1_0 \/ c1_0 \/ c2_1 $_41 \/ % 0.18/0.41 c2_2 a461 $_40 \/ c4_2 a461 $_40 \/ c5_2 a461 $_40 % 0.18/0.41 |- ~c1_2 $_46 a443 \/ ~c2_1 $_46 \/ ~c3_2 $_46 a444 \/ ~ndr1_0 \/ % 0.18/0.41 ~ndr1_1 $_46 \/ c1_0 \/ c1_1 $_46 \/ c1_2 $_46 a444 \/ c3_2 $_46 a469 \/ % 0.18/0.41 c4_2 $_46 a444 \/ definitionFOFtoCNF_3 $_46 % 0.18/0.41 |- ~c2_1 $_51 \/ ~c3_2 $_51 a444 \/ ~ndr1_0 \/ ~ndr1_1 $_51 \/ c1_0 \/ % 0.18/0.41 c1_1 $_51 \/ c1_2 $_51 a444 \/ c3_2 $_51 a443 \/ c3_2 $_51 a469 \/ % 0.18/0.41 c4_2 $_51 a444 \/ definitionFOFtoCNF_3 $_51 % 0.18/0.41 |- ~c2_1 $_63 \/ ~c3_2 $_64 $_66 \/ ~ndr1_0 \/ ~ndr1_1 $_64 \/ c1_0 \/ % 0.18/0.41 c1_1 $_64 \/ c1_2 $_64 $_66 \/ c3_2 $_64 a469 \/ c4_2 $_64 $_66 \/ % 0.18/0.41 definitionFOFtoCNF_3 $_64 \/ ndr1_1 $_63 % 0.18/0.41 |- ~c1_2 $_70 a443 \/ ~c2_1 $_70 \/ ~c3_2 $_70 a444 \/ ~c3_2 $_71 $_73 \/ % 0.18/0.41 ~ndr1_0 \/ ~ndr1_1 $_71 \/ c1_0 \/ c1_1 $_71 \/ c1_2 $_71 $_73 \/ % 0.18/0.41 c3_2 $_71 a469 \/ c4_2 $_71 $_73 \/ definitionFOFtoCNF_3 $_71 % 0.18/0.41 |- ~c1_2 $_77 a443 \/ ~c2_1 $_77 \/ ~c3_2 $_78 $_80 \/ ~c5_2 $_77 a444 \/ % 0.18/0.41 ~ndr1_0 \/ ~ndr1_1 $_78 \/ c1_0 \/ c1_1 $_78 \/ c1_2 $_78 $_80 \/ % 0.18/0.41 c3_2 $_78 a469 \/ c4_2 $_78 $_80 \/ definitionFOFtoCNF_3 $_78 % 0.18/0.41 |- ~c2_1 $_84 \/ ~c3_2 $_84 a444 \/ ~c3_2 $_85 $_87 \/ ~ndr1_0 \/ % 0.18/0.41 ~ndr1_1 $_85 \/ c1_0 \/ c1_1 $_85 \/ c1_2 $_85 $_87 \/ c3_2 $_84 a443 \/ % 0.18/0.41 c3_2 $_85 a469 \/ c4_2 $_85 $_87 \/ definitionFOFtoCNF_3 $_85 % 0.18/0.41 |- ~c2_1 $_91 \/ ~c3_2 $_92 $_94 \/ ~c5_2 $_91 a444 \/ ~ndr1_0 \/ % 0.18/0.41 ~ndr1_1 $_92 \/ c1_0 \/ c1_1 $_92 \/ c1_2 $_92 $_94 \/ c3_2 $_91 a443 \/ % 0.18/0.41 c3_2 $_92 a469 \/ c4_2 $_92 $_94 \/ definitionFOFtoCNF_3 $_92 % 0.18/0.41 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.41 %------------------------------------------------------------------------------