%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN538+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:49 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.07/0.12 % Problem : SYN538+1 : TPTP v8.1.0. Released v2.1.0. % 0.07/0.13 % Command : metis --show proof --show saturation %s % 0.14/0.34 % Computer : n005.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Mon Jul 11 16:33:22 EDT 2022 % 0.14/0.34 % CPUTime : % 0.14/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.20/0.50 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.50 % 0.20/0.50 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.50 |- ~c1_0 \/ c3_0 % 0.20/0.50 |- ~c2_0 \/ ~c4_0 % 0.20/0.50 |- ~c2_2 $X17 $X18 \/ ~c3_0 \/ ~c4_1 $X17 \/ ~ndr1_0 \/ ~ndr1_1 $X17 \/ % 0.20/0.50 c1_2 $X17 $X18 \/ c3_2 $X17 $X18 \/ c5_1 $X17 % 0.20/0.50 |- c1_0 \/ c4_0 % 0.20/0.50 |- ~c2_1 $X42 \/ ~c4_1 $X42 \/ ~ndr1_0 \/ c3_0 \/ c3_1 $X42 % 0.20/0.50 |- ~c1_1 $X15 \/ ~c4_2 $X15 $X16 \/ ~c5_2 $X15 $X16 \/ ~ndr1_0 \/ % 0.20/0.50 ~ndr1_1 $X15 \/ c1_2 $X15 $X16 \/ c2_1 $X15 \/ c5_0 % 0.20/0.50 |- ~c2_2 a552 a554 \/ ~c3_1 $X2 \/ ~c3_2 $X2 $X3 \/ ~ndr1_0 \/ % 0.20/0.50 ~ndr1_1 $X2 \/ c1_2 $X2 $X3 \/ c4_1 $X2 \/ c4_2 $X2 $X3 % 0.20/0.50 |- ~c3_1 $X2 \/ ~c3_2 $X2 $X3 \/ ~c3_2 a552 a553 \/ ~ndr1_0 \/ % 0.20/0.50 ~ndr1_1 $X2 \/ c1_2 $X2 $X3 \/ c4_1 $X2 \/ c4_2 $X2 $X3 % 0.20/0.50 |- ~c3_1 $X2 \/ ~c3_2 $X2 $X3 \/ ~c4_2 a552 a554 \/ ~ndr1_0 \/ % 0.20/0.50 ~ndr1_1 $X2 \/ c1_2 $X2 $X3 \/ c4_1 $X2 \/ c4_2 $X2 $X3 % 0.20/0.50 |- ~c3_1 $X2 \/ ~c3_2 $X2 $X3 \/ ~ndr1_0 \/ ~ndr1_1 $X2 \/ c1_2 $X2 $X3 \/ % 0.20/0.50 c1_2 a552 a553 \/ c4_1 $X2 \/ c4_2 $X2 $X3 % 0.20/0.50 |- ~c3_1 $X2 \/ ~c3_2 $X2 $X3 \/ ~ndr1_0 \/ ~ndr1_1 $X2 \/ c1_2 $X2 $X3 \/ % 0.20/0.50 c2_2 a552 a553 \/ c4_1 $X2 \/ c4_2 $X2 $X3 % 0.20/0.50 |- ~c3_1 $X2 \/ ~c3_2 $X2 $X3 \/ ~ndr1_0 \/ ~ndr1_1 $X2 \/ c1_2 $X2 $X3 \/ % 0.20/0.50 c4_1 $X2 \/ c4_2 $X2 $X3 \/ ndr1_1 a552 % 0.20/0.50 |- ~c1_1 $X20 \/ ~c2_1 $X22 \/ ~c2_2 $X20 $X21 \/ ~c2_2 $X20 a566 \/ % 0.20/0.50 ~c4_2 $X20 $X21 \/ ~c5_1 $X22 \/ ~ndr1_0 \/ ~ndr1_1 $X20 \/ % 0.20/0.50 c3_2 $X20 $X21 % 0.20/0.50 |- ~c1_1 $X20 \/ ~c2_1 $X22 \/ ~c2_2 $X20 $X21 \/ ~c3_2 $X20 a566 \/ % 0.20/0.50 ~c4_2 $X20 $X21 \/ ~c5_1 $X22 \/ ~ndr1_0 \/ ~ndr1_1 $X20 \/ % 0.20/0.50 c3_2 $X20 $X21 % 0.20/0.50 |- ~c1_1 $X20 \/ ~c2_1 $X22 \/ ~c2_2 $X20 $X21 \/ ~c4_2 $X20 $X21 \/ % 0.20/0.50 ~c5_1 $X22 \/ ~ndr1_0 \/ ~ndr1_1 $X20 \/ c3_2 $X20 $X21 \/ % 0.20/0.50 c4_2 $X20 a566 % 0.20/0.50 |- ~c3_1 $X34 \/ ~c3_2 $X33 a575 \/ ~c4_1 $X33 \/ ~ndr1_0 \/ c2_1 $X33 \/ % 0.20/0.50 c4_1 $X34 % 0.20/0.50 |- ~c3_1 $X34 \/ ~c4_1 $X33 \/ ~ndr1_0 \/ c1_2 $X33 a575 \/ c2_1 $X33 \/ % 0.20/0.50 c4_1 $X34 % 0.20/0.50 |- ~c3_1 $X34 \/ ~c4_1 $X33 \/ ~ndr1_0 \/ c2_1 $X33 \/ c2_2 $X33 a575 \/ % 0.20/0.50 c4_1 $X34 % 0.20/0.50 |- ~c3_1 $X34 \/ ~c4_1 $X33 \/ ~ndr1_0 \/ c2_1 $X33 \/ c4_1 $X34 \/ % 0.20/0.50 ndr1_1 $X33 % 0.20/0.50 |- ~c1_0 \/ ~c1_1 a585 \/ ~c4_0 % 0.20/0.50 |- ~c1_0 \/ ~c4_0 \/ c2_1 a585 % 0.20/0.50 |- ~c1_0 \/ ~c4_0 \/ c5_1 a585 % 0.20/0.50 |- ~c1_0 \/ ~c4_0 \/ ndr1_0 % 0.20/0.51 |- ~c2_0 \/ ~c2_2 $X24 a570 \/ ~c5_1 $X24 \/ ~c5_2 $X24 $X25 \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 $X24 \/ c2_2 $X24 $X25 \/ c5_0 % 0.20/0.51 |- ~c2_0 \/ ~c3_2 $X24 a570 \/ ~c5_1 $X24 \/ ~c5_2 $X24 $X25 \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 $X24 \/ c2_2 $X24 $X25 \/ c5_0 % 0.20/0.51 |- ~c2_0 \/ ~c4_2 $X24 a570 \/ ~c5_1 $X24 \/ ~c5_2 $X24 $X25 \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 $X24 \/ c2_2 $X24 $X25 \/ c5_0 % 0.20/0.51 |- ~c1_2 $X43 $X44 \/ ~c2_0 \/ ~c2_1 a581 \/ ~c5_2 $X43 $X44 \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 $X43 \/ c4_1 $X43 \/ c4_2 $X43 $X44 \/ c5_1 $X43 % 0.20/0.51 |- ~c1_2 $X43 $X44 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~c5_2 $X43 $X44 \/ % 0.20/0.51 ~ndr1_0 \/ ~ndr1_1 $X43 \/ c4_1 $X43 \/ c4_2 $X43 $X44 \/ c5_1 $X43 % 0.20/0.51 |- ~c1_2 $X43 $X44 \/ ~c2_0 \/ ~c5_2 $X43 $X44 \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 $X43 \/ c1_2 a581 a582 \/ c4_1 $X43 \/ c4_2 $X43 $X44 \/ % 0.20/0.51 c5_1 $X43 % 0.20/0.51 |- ~c1_2 $X43 $X44 \/ ~c2_0 \/ ~c5_2 $X43 $X44 \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 $X43 \/ c3_1 a581 \/ c4_1 $X43 \/ c4_2 $X43 $X44 \/ c5_1 $X43 % 0.20/0.51 |- ~c1_2 $X43 $X44 \/ ~c2_0 \/ ~c5_2 $X43 $X44 \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 $X43 \/ c4_1 $X43 \/ c4_2 $X43 $X44 \/ c5_1 $X43 \/ % 0.20/0.51 c5_2 a581 a582 % 0.20/0.51 |- ~c1_2 $X43 $X44 \/ ~c2_0 \/ ~c5_2 $X43 $X44 \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 $X43 \/ c4_1 $X43 \/ c4_2 $X43 $X44 \/ c5_1 $X43 \/ ndr1_1 a581 % 0.20/0.51 |- ~c1_2 a571 a572 \/ ~c2_0 \/ ~c2_1 $X26 \/ ~c4_1 $X26 \/ ~ndr1_0 \/ % 0.20/0.51 c1_1 $X26 % 0.20/0.51 |- ~c2_0 \/ ~c2_1 $X26 \/ ~c3_2 a571 a572 \/ ~c4_1 $X26 \/ ~ndr1_0 \/ % 0.20/0.51 c1_1 $X26 % 0.20/0.51 |- ~c2_0 \/ ~c2_1 $X26 \/ ~c4_1 $X26 \/ ~c4_2 a571 a573 \/ ~ndr1_0 \/ % 0.20/0.51 c1_1 $X26 % 0.20/0.51 |- ~c2_0 \/ ~c2_1 $X26 \/ ~c4_1 $X26 \/ ~ndr1_0 \/ c1_1 $X26 \/ c1_1 a571 % 0.20/0.51 |- ~c2_0 \/ ~c2_1 $X26 \/ ~c4_1 $X26 \/ ~ndr1_0 \/ c1_1 $X26 \/ % 0.20/0.51 c1_2 a571 a573 % 0.20/0.51 |- ~c2_0 \/ ~c2_1 $X26 \/ ~c4_1 $X26 \/ ~ndr1_0 \/ c1_1 $X26 \/ % 0.20/0.51 c3_2 a571 a573 % 0.20/0.51 |- ~c2_0 \/ ~c2_1 $X26 \/ ~c4_1 $X26 \/ ~ndr1_0 \/ c1_1 $X26 \/ % 0.20/0.51 c5_2 a571 a572 % 0.20/0.51 |- ~c2_0 \/ ~c2_1 $X26 \/ ~c4_1 $X26 \/ ~ndr1_0 \/ c1_1 $X26 \/ ndr1_1 a571 % 0.20/0.51 |- ~c1_1 a565 \/ ~c3_0 \/ ~c5_0 % 0.20/0.51 |- ~c3_0 \/ ~c5_0 \/ ndr1_0 % 0.20/0.51 |- ~c1_2 a565 $X19 \/ ~c2_2 a565 $X19 \/ ~c3_0 \/ ~c5_0 \/ ~ndr1_1 a565 % 0.20/0.51 |- ~c3_0 \/ ~c3_1 $X5 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $X5 \/ c4_1 $X5 % 0.20/0.51 |- ~c3_0 \/ c4_0 \/ c5_0 % 0.20/0.51 |- ~c4_0 \/ ~c5_1 a550 \/ c3_0 % 0.20/0.51 |- ~c4_0 \/ c3_0 \/ ndr1_0 % 0.20/0.51 |- ~c2_1 a578 \/ ~c4_0 \/ c3_0 % 0.20/0.51 |- ~c4_0 \/ c3_0 \/ c5_1 a578 % 0.20/0.51 |- ~c4_0 \/ ~c5_2 a578 $X37 \/ ~ndr1_1 a578 \/ c3_0 \/ c4_2 a578 $X37 % 0.20/0.51 |- ~c1_1 a551 \/ ~c3_1 $Y \/ ~c4_0 \/ ~c4_1 $Y \/ ~ndr1_0 % 0.20/0.51 |- ~c2_2 a551 $X1 \/ ~c3_1 $Y \/ ~c4_0 \/ ~c4_1 $Y \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 a551 \/ c4_2 a551 $X1 \/ c5_2 a551 $X1 % 0.20/0.51 |- ~c3_1 $Y \/ ~c3_2 a551 $Z \/ ~c4_0 \/ ~c4_1 $Y \/ ~c4_2 a551 $Z \/ % 0.20/0.51 ~ndr1_0 \/ ~ndr1_1 a551 \/ c1_2 a551 $Z % 0.20/0.51 |- ~c2_1 $X35 \/ ~ndr1_0 \/ c2_0 % 0.20/0.51 |- ~c1_2 $X4 a555 \/ ~c3_1 $X4 \/ ~ndr1_0 \/ c1_0 \/ c5_0 \/ c5_1 $X4 % 0.20/0.51 |- ~c3_1 $X4 \/ ~c4_2 $X4 a555 \/ ~ndr1_0 \/ c1_0 \/ c5_0 \/ c5_1 $X4 % 0.20/0.51 |- ~c3_1 $X4 \/ ~c5_2 $X4 a555 \/ ~ndr1_0 \/ c1_0 \/ c5_0 \/ c5_1 $X4 % 0.20/0.51 |- ~c3_1 $X4 \/ ~ndr1_0 \/ c1_0 \/ c5_0 \/ c5_1 $X4 \/ ndr1_1 $X4 % 0.20/0.51 |- ~c2_1 $X36 \/ ~c5_2 $X36 a576 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a577 \/ % 0.20/0.51 c3_1 $X36 % 0.20/0.51 |- ~c2_1 $X36 \/ ~c5_2 $X36 a576 \/ ~ndr1_0 \/ c1_0 \/ c3_1 $X36 \/ % 0.20/0.51 c4_1 a577 % 0.20/0.51 |- ~c2_1 $X36 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a577 \/ c2_2 $X36 a576 \/ % 0.20/0.51 c3_1 $X36 % 0.20/0.51 |- ~c2_1 $X36 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a577 \/ c3_1 $X36 \/ ndr1_1 $X36 % 0.20/0.51 |- ~c2_1 $X36 \/ ~ndr1_0 \/ c1_0 \/ c2_2 $X36 a576 \/ c3_1 $X36 \/ % 0.20/0.51 c4_1 a577 % 0.20/0.51 |- ~c2_1 $X36 \/ ~ndr1_0 \/ c1_0 \/ c3_1 $X36 \/ c4_1 a577 \/ ndr1_1 $X36 % 0.20/0.51 |- ~definitionFOFtoCNF_0 $X12 \/ c3_2 $X12 a560 % 0.20/0.51 |- ~definitionFOFtoCNF_0 $X12 \/ c5_2 $X12 a560 % 0.20/0.51 |- ~definitionFOFtoCNF_0 $X12 \/ ndr1_1 $X12 % 0.20/0.51 |- ~c3_2 $X12 a560 \/ ~c5_2 $X12 a560 \/ ~ndr1_1 $X12 \/ % 0.20/0.51 definitionFOFtoCNF_0 $X12 % 0.20/0.51 |- ~c1_2 $X9 a559 \/ ~c2_2 $X9 $X10 \/ ~c3_1 $X12 \/ ~c3_2 $X9 $X11 \/ % 0.20/0.51 ~c4_1 $X12 \/ ~ndr1_0 \/ ~ndr1_1 $X9 \/ c1_2 $X9 $X10 \/ c2_0 \/ % 0.20/0.51 c2_2 $X9 $X11 \/ c5_2 $X9 $X11 \/ definitionFOFtoCNF_0 $X12 % 0.20/0.51 |- ~c2_2 $X9 $X10 \/ ~c3_1 $X12 \/ ~c3_2 $X9 $X11 \/ ~c4_1 $X12 \/ % 0.20/0.51 ~ndr1_0 \/ ~ndr1_1 $X9 \/ c1_2 $X9 $X10 \/ c2_0 \/ c2_2 $X9 $X11 \/ % 0.20/0.51 c3_2 $X9 a559 \/ c5_2 $X9 $X11 \/ definitionFOFtoCNF_0 $X12 % 0.20/0.51 |- ~c2_2 $X9 $X10 \/ ~c3_1 $X12 \/ ~c3_2 $X9 $X11 \/ ~c4_1 $X12 \/ % 0.20/0.51 ~ndr1_0 \/ ~ndr1_1 $X9 \/ c1_2 $X9 $X10 \/ c2_0 \/ c2_2 $X9 $X11 \/ % 0.20/0.51 c4_2 $X9 a559 \/ c5_2 $X9 $X11 \/ definitionFOFtoCNF_0 $X12 % 0.20/0.51 |- ~c2_1 a584 \/ ~definitionFOFtoCNF_1 % 0.20/0.51 |- ~c5_1 a584 \/ ~definitionFOFtoCNF_1 % 0.20/0.51 |- ~definitionFOFtoCNF_1 \/ ndr1_0 % 0.20/0.51 |- ~ndr1_0 \/ c2_1 a584 \/ c5_1 a584 \/ definitionFOFtoCNF_1 % 0.20/0.51 |- ~c4_1 a583 \/ c4_0 \/ definitionFOFtoCNF_1 % 0.20/0.51 |- c3_1 a583 \/ c4_0 \/ definitionFOFtoCNF_1 % 0.20/0.51 |- c4_0 \/ c5_1 a583 \/ definitionFOFtoCNF_1 % 0.20/0.51 |- c4_0 \/ definitionFOFtoCNF_1 \/ ndr1_0 % 0.20/0.51 |- ~c3_2 $X8 a558 \/ ~definitionFOFtoCNF_2 $X8 % 0.20/0.51 |- ~c5_2 $X8 a558 \/ ~definitionFOFtoCNF_2 $X8 % 0.20/0.51 |- ~definitionFOFtoCNF_2 $X8 \/ c2_2 $X8 a558 % 0.20/0.51 |- ~definitionFOFtoCNF_2 $X8 \/ ndr1_1 $X8 % 0.20/0.51 |- ~c2_2 $X8 a558 \/ ~ndr1_1 $X8 \/ c3_2 $X8 a558 \/ c5_2 $X8 a558 \/ % 0.20/0.51 definitionFOFtoCNF_2 $X8 % 0.20/0.51 |- ~c3_2 $X8 a557 \/ ~c4_1 a556 \/ ~ndr1_0 \/ c2_1 $X8 \/ c5_0 \/ % 0.20/0.51 definitionFOFtoCNF_2 $X8 % 0.20/0.51 |- ~c3_2 $X8 a557 \/ ~ndr1_0 \/ c2_1 $X8 \/ c5_0 \/ c5_1 a556 \/ % 0.20/0.51 definitionFOFtoCNF_2 $X8 % 0.20/0.51 |- ~c4_1 a556 \/ ~ndr1_0 \/ c1_2 $X8 a557 \/ c2_1 $X8 \/ c5_0 \/ % 0.20/0.51 definitionFOFtoCNF_2 $X8 % 0.20/0.51 |- ~c4_1 a556 \/ ~ndr1_0 \/ c2_1 $X8 \/ c5_0 \/ definitionFOFtoCNF_2 $X8 \/ % 0.20/0.51 ndr1_1 $X8 % 0.20/0.51 |- ~ndr1_0 \/ c1_2 $X8 a557 \/ c2_1 $X8 \/ c5_0 \/ c5_1 a556 \/ % 0.20/0.51 definitionFOFtoCNF_2 $X8 % 0.20/0.51 |- ~ndr1_0 \/ c2_1 $X8 \/ c5_0 \/ c5_1 a556 \/ definitionFOFtoCNF_2 $X8 \/ % 0.20/0.51 ndr1_1 $X8 % 0.20/0.51 |- ~c1_2 a567 a568 \/ ~definitionFOFtoCNF_3 % 0.20/0.51 |- ~definitionFOFtoCNF_3 \/ c1_1 a567 % 0.20/0.51 |- ~definitionFOFtoCNF_3 \/ c2_1 a567 % 0.20/0.51 |- ~definitionFOFtoCNF_3 \/ c4_2 a567 a568 % 0.20/0.51 |- ~definitionFOFtoCNF_3 \/ ndr1_0 % 0.20/0.51 |- ~definitionFOFtoCNF_3 \/ ndr1_1 a567 % 0.20/0.51 |- ~c1_1 a567 \/ ~c2_1 a567 \/ ~c4_2 a567 a568 \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 a567 \/ c1_2 a567 a568 \/ definitionFOFtoCNF_3 % 0.20/0.51 |- ~c1_1 a569 \/ c5_0 \/ definitionFOFtoCNF_3 % 0.20/0.51 |- ~c2_1 a569 \/ c5_0 \/ definitionFOFtoCNF_3 % 0.20/0.51 |- c5_0 \/ definitionFOFtoCNF_3 \/ ndr1_0 % 0.20/0.51 |- ~c2_2 a569 $X23 \/ ~ndr1_1 a569 \/ c3_2 a569 $X23 \/ c5_0 \/ % 0.20/0.51 definitionFOFtoCNF_3 % 0.20/0.51 |- ~c1_1 a574 \/ ~c1_2 $X28 $X29 \/ ~c3_2 $X28 $X29 \/ ~c5_1 $X28 \/ % 0.20/0.51 ~ndr1_0 \/ ~ndr1_1 $X28 \/ c2_1 $X28 \/ c2_2 $X28 $X29 \/ c5_0 % 0.20/0.51 |- ~c1_2 $X28 $X29 \/ ~c3_2 $X28 $X29 \/ ~c5_1 $X28 \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 $X28 \/ c2_1 $X28 \/ c2_2 $X28 $X29 \/ c5_0 \/ c5_1 a574 % 0.20/0.51 |- ~c1_2 $X28 $X29 \/ ~c1_2 a574 $X27 \/ ~c3_2 $X28 $X29 \/ ~c5_1 $X28 \/ % 0.20/0.51 ~ndr1_0 \/ ~ndr1_1 $X28 \/ ~ndr1_1 a574 \/ c2_1 $X28 \/ % 0.20/0.51 c2_2 $X28 $X29 \/ c3_2 a574 $X27 \/ c4_2 a574 $X27 \/ c5_0 % 0.20/0.51 |- ~c2_2 $X14 a563 \/ definitionFOFtoCNF_5 $X14 % 0.20/0.51 |- c1_2 $X14 a563 \/ definitionFOFtoCNF_5 $X14 % 0.20/0.51 |- c4_2 $X14 a563 \/ definitionFOFtoCNF_5 $X14 % 0.20/0.51 |- definitionFOFtoCNF_5 $X14 \/ ndr1_1 $X14 % 0.20/0.51 |- ~c1_2 $X14 a563 \/ ~c4_2 $X14 a563 \/ ~definitionFOFtoCNF_5 $X14 \/ % 0.20/0.51 ~ndr1_1 $X14 \/ c2_2 $X14 a563 % 0.20/0.51 |- definitionFOFtoCNF_4 $X14 \/ definitionFOFtoCNF_5 $X14 % 0.20/0.51 |- ~c4_2 $X14 a562 \/ ~definitionFOFtoCNF_4 $X14 \/ % 0.20/0.51 ~definitionFOFtoCNF_5 $X14 % 0.20/0.51 |- ~definitionFOFtoCNF_4 $X14 \/ ~definitionFOFtoCNF_5 $X14 \/ % 0.20/0.51 c2_2 $X14 a562 % 0.20/0.51 |- ~definitionFOFtoCNF_4 $X14 \/ ~definitionFOFtoCNF_5 $X14 \/ % 0.20/0.51 c5_2 $X14 a562 % 0.20/0.51 |- ~definitionFOFtoCNF_4 $X14 \/ ~definitionFOFtoCNF_5 $X14 \/ ndr1_1 $X14 % 0.20/0.51 |- ~c2_2 $X14 a562 \/ ~c5_2 $X14 a562 \/ ~ndr1_1 $X14 \/ c4_2 $X14 a562 \/ % 0.20/0.51 definitionFOFtoCNF_4 $X14 % 0.20/0.51 |- ~c1_1 a561 \/ ~c1_1 a564 \/ ~ndr1_0 \/ c3_1 $X14 \/ % 0.20/0.51 definitionFOFtoCNF_4 $X14 % 0.20/0.51 |- ~c1_1 a561 \/ ~c3_1 a564 \/ ~ndr1_0 \/ c3_1 $X14 \/ % 0.20/0.51 definitionFOFtoCNF_4 $X14 % 0.20/0.51 |- ~c1_1 a564 \/ ~c2_2 a561 $X13 \/ ~c4_2 a561 $X13 \/ ~c5_2 a561 $X13 \/ % 0.20/0.51 ~ndr1_0 \/ ~ndr1_1 a561 \/ c3_1 $X14 \/ definitionFOFtoCNF_4 $X14 % 0.20/0.51 |- ~c2_2 a561 $X13 \/ ~c3_1 a564 \/ ~c4_2 a561 $X13 \/ ~c5_2 a561 $X13 \/ % 0.20/0.51 ~ndr1_0 \/ ~ndr1_1 a561 \/ c3_1 $X14 \/ definitionFOFtoCNF_4 $X14 % 0.20/0.51 |- ~c4_2 a546 a547 \/ ~definitionFOFtoCNF_6 % 0.20/0.51 |- ~definitionFOFtoCNF_6 \/ c2_1 a546 % 0.20/0.51 |- ~definitionFOFtoCNF_6 \/ c2_2 a546 a547 % 0.20/0.51 |- ~definitionFOFtoCNF_6 \/ c5_2 a546 a547 % 0.20/0.51 |- ~definitionFOFtoCNF_6 \/ ndr1_0 % 0.20/0.51 |- ~definitionFOFtoCNF_6 \/ ndr1_1 a546 % 0.20/0.51 |- ~c2_1 a546 \/ ~c2_2 a546 a547 \/ ~c5_2 a546 a547 \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 a546 \/ c4_2 a546 a547 \/ definitionFOFtoCNF_6 % 0.20/0.51 |- ~c1_2 $U a548 \/ ~definitionFOFtoCNF_7 $U % 0.20/0.51 |- ~definitionFOFtoCNF_7 $U \/ c2_2 $U a548 % 0.20/0.51 |- ~definitionFOFtoCNF_7 $U \/ c5_2 $U a548 % 0.20/0.51 |- ~definitionFOFtoCNF_7 $U \/ ndr1_1 $U % 0.20/0.51 |- ~c2_2 $U a548 \/ ~c5_2 $U a548 \/ ~ndr1_1 $U \/ c1_2 $U a548 \/ % 0.20/0.51 definitionFOFtoCNF_7 $U % 0.20/0.51 |- ~c1_1 $W \/ ~c2_2 $W $X \/ ~c3_2 $W $X \/ ~c4_2 $U a549 \/ % 0.20/0.51 ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ndr1_1 $W \/ c1_2 $U $V \/ % 0.20/0.51 c2_1 $W \/ definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 $U % 0.20/0.51 |- ~c1_1 $W \/ ~c2_2 $W $X \/ ~c3_2 $W $X \/ ~c5_2 $U $V \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 $U \/ ~ndr1_1 $W \/ c1_2 $U $V \/ c2_1 $W \/ c2_2 $U a549 \/ % 0.20/0.51 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 $U % 0.20/0.51 |- ~c1_1 $W \/ ~c2_2 $W $X \/ ~c3_2 $W $X \/ ~c5_2 $U $V \/ ~ndr1_0 \/ % 0.20/0.51 ~ndr1_1 $U \/ ~ndr1_1 $W \/ c1_2 $U $V \/ c2_1 $W \/ c5_2 $U a549 \/ % 0.20/0.51 definitionFOFtoCNF_6 \/ definitionFOFtoCNF_7 $U % 0.20/0.51 |- ~c1_2 $X38 $X39 \/ ~c1_2 $X41 a580 \/ ~c2_2 $X41 a579 \/ ~c3_1 $X40 \/ % 0.20/0.51 ~c3_1 $X41 \/ ~c4_1 $X38 \/ ~ndr1_0 \/ ~ndr1_1 $X38 \/ c5_1 $X38 \/ % 0.20/0.51 c5_2 $X38 $X39 % 0.20/0.51 |- ~c1_2 $X38 $X39 \/ ~c1_2 $X41 a580 \/ ~c3_1 $X40 \/ ~c3_1 $X41 \/ % 0.20/0.51 ~c4_1 $X38 \/ ~ndr1_0 \/ ~ndr1_1 $X38 \/ c3_2 $X41 a579 \/ c5_1 $X38 \/ % 0.20/0.51 c5_2 $X38 $X39 % 0.20/0.51 |- ~c1_2 $X38 $X39 \/ ~c2_2 $X41 a579 \/ ~c3_1 $X40 \/ ~c3_1 $X41 \/ % 0.20/0.51 ~c4_1 $X38 \/ ~ndr1_0 \/ ~ndr1_1 $X38 \/ c2_2 $X41 a580 \/ c5_1 $X38 \/ % 0.20/0.51 c5_2 $X38 $X39 % 0.20/0.51 |- ~ndr1_0 \/ c1_1 $X45 \/ c4_1 $X45 \/ c5_1 $X45 % 0.20/0.52 |- ~c3_1 a552 \/ ~c3_2 a552 a553 \/ ~ndr1_0 \/ ~ndr1_1 a552 \/ % 0.20/0.52 c1_2 a552 a553 \/ c4_1 a552 \/ c4_2 a552 a553 % 0.20/0.52 |- ~c1_2 $X38 $X39 \/ ~c3_1 $X41 \/ ~c4_1 $X38 \/ ~ndr1_0 \/ % 0.20/0.52 ~ndr1_1 $X38 \/ c5_1 $X38 \/ c5_2 $X38 $X39 \/ ndr1_1 $X41 % 0.20/0.52 |- ~c1_2 $X41 a580 \/ ~c3_1 $X40 \/ ~c3_1 $X41 \/ ~c4_1 $X41 \/ ~ndr1_0 \/ % 0.20/0.52 ~ndr1_1 $X41 \/ c3_2 $X41 a579 \/ c5_1 $X41 \/ c5_2 $X41 a580 % 0.20/0.52 |- ~c1_2 $X38 $X39 \/ ~c3_1 $X41 \/ ~c4_1 $X38 \/ ~ndr1_0 \/ % 0.20/0.52 ~ndr1_1 $X38 \/ c2_2 $X41 a580 \/ c3_2 $X41 a579 \/ c5_1 $X38 \/ % 0.20/0.52 c5_2 $X38 $X39 % 0.20/0.52 |- ~c2_0 \/ c1_0 % 0.20/0.52 |- c1_0 \/ c3_0 \/ ndr1_0 % 0.20/0.52 |- c1_0 \/ c3_0 \/ c5_1 a578 % 0.20/0.52 |- c1_0 \/ c2_1 a584 \/ c3_0 \/ c5_1 a584 \/ definitionFOFtoCNF_1 % 0.20/0.52 |- c2_1 a584 \/ c5_0 \/ c5_1 a584 \/ definitionFOFtoCNF_1 \/ % 0.20/0.52 definitionFOFtoCNF_3 % 0.20/0.52 |- c2_1 a584 \/ c4_0 \/ c5_1 a584 \/ definitionFOFtoCNF_1 % 0.20/0.52 |- c1_0 \/ c1_1 $_21 \/ c3_0 \/ c4_1 $_21 \/ c5_1 $_21 % 0.20/0.52 |- c1_1 $_21 \/ c4_1 $_21 \/ c5_0 \/ c5_1 $_21 \/ definitionFOFtoCNF_3 % 0.20/0.52 |- c1_1 $_21 \/ c4_0 \/ c4_1 $_21 \/ c5_1 $_21 \/ definitionFOFtoCNF_1 % 0.20/0.52 |- ~definitionFOFtoCNF_1 \/ c1_0 \/ c1_1 a584 \/ c3_0 \/ c4_1 a584 % 0.20/0.52 |- c1_0 \/ c1_1 a550 \/ c3_0 \/ c4_1 a550 % 0.20/0.52 |- ~c1_1 a551 \/ ~c3_1 a550 \/ ~c4_0 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a550 \/ % 0.20/0.52 c3_0 % 0.20/0.52 |- ~c2_1 a550 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a550 \/ c3_0 \/ c3_1 a550 % 0.20/0.52 |- ~c4_0 \/ c1_1 a550 \/ c3_0 \/ c4_1 a550 \/ c5_0 \/ definitionFOFtoCNF_3 % 0.20/0.52 |- ~definitionFOFtoCNF_1 \/ c1_1 a584 \/ c4_1 a584 \/ c5_0 \/ % 0.20/0.52 definitionFOFtoCNF_3 % 0.20/0.52 |- c1_0 \/ c2_1 $_43 \/ c3_0 \/ c5_0 \/ c5_1 a556 \/ % 0.20/0.52 definitionFOFtoCNF_2 $_43 \/ ndr1_1 $_43 % 0.20/0.52 |- c2_1 $_43 \/ c5_0 \/ c5_1 a556 \/ definitionFOFtoCNF_2 $_43 \/ % 0.20/0.52 definitionFOFtoCNF_3 \/ ndr1_1 $_43 % 0.20/0.52 |- c2_1 $_43 \/ c4_0 \/ c5_0 \/ c5_1 a556 \/ definitionFOFtoCNF_1 \/ % 0.20/0.52 definitionFOFtoCNF_2 $_43 \/ ndr1_1 $_43 % 0.20/0.52 |- c1_0 \/ c1_2 $_61 a557 \/ c2_1 $_61 \/ c3_0 \/ c5_0 \/ c5_1 a556 \/ % 0.20/0.52 definitionFOFtoCNF_2 $_61 % 0.20/0.52 |- c1_2 $_61 a557 \/ c2_1 $_61 \/ c5_0 \/ c5_1 a556 \/ % 0.20/0.52 definitionFOFtoCNF_2 $_61 \/ definitionFOFtoCNF_3 % 0.20/0.52 |- c1_2 $_61 a557 \/ c2_1 $_61 \/ c4_0 \/ c5_0 \/ c5_1 a556 \/ % 0.20/0.52 definitionFOFtoCNF_1 \/ definitionFOFtoCNF_2 $_61 % 0.20/0.52 |- ~c3_1 $_67 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a550 \/ c2_1 a550 \/ c3_0 \/ % 0.20/0.52 c4_1 $_67 \/ ndr1_1 a550 % 0.20/0.52 |- ~c3_1 $_74 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a550 \/ c1_2 a550 a575 \/ % 0.20/0.52 c2_1 a550 \/ c3_0 \/ c4_1 $_74 % 0.20/0.52 |- ~c3_1 $_76 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a550 \/ c2_1 a550 \/ % 0.20/0.52 c2_2 a550 a575 \/ c3_0 \/ c4_1 $_76 % 0.20/0.52 |- ~c3_1 $_131 \/ ~c4_1 $_130 \/ ~ndr1_0 \/ c5_1 $_130 \/ % 0.20/0.52 c5_2 $_130 a563 \/ definitionFOFtoCNF_5 $_130 \/ ndr1_1 $_131 % 0.20/0.52 |- ~c3_1 $_133 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a550 \/ c3_0 \/ c5_1 a550 \/ % 0.20/0.52 c5_2 a550 a563 \/ definitionFOFtoCNF_5 a550 \/ ndr1_1 $_133 % 0.20/0.52 |- ~c1_1 $_135 \/ ~c2_1 $_137 \/ ~c2_2 $_135 $_136 \/ ~c2_2 $_135 a566 \/ % 0.20/0.52 ~c4_2 $_135 $_136 \/ ~ndr1_0 \/ ~ndr1_1 $_135 \/ c1_1 $_137 \/ % 0.20/0.52 c3_2 $_135 $_136 \/ c4_0 \/ c4_1 $_137 \/ definitionFOFtoCNF_1 % 0.20/0.52 |- ~c1_1 $_135 \/ ~c2_1 $_137 \/ ~c2_2 $_135 $_136 \/ ~c2_2 $_135 a566 \/ % 0.20/0.52 ~c4_2 $_135 $_136 \/ ~ndr1_0 \/ ~ndr1_1 $_135 \/ c1_1 $_137 \/ % 0.20/0.52 c3_2 $_135 $_136 \/ c4_1 $_137 \/ c5_0 \/ definitionFOFtoCNF_3 % 0.20/0.52 |- ~c1_1 $_135 \/ ~c2_1 $_137 \/ ~c2_2 $_135 $_136 \/ ~c2_2 $_135 a566 \/ % 0.20/0.52 ~c4_2 $_135 $_136 \/ ~ndr1_0 \/ ~ndr1_1 $_135 \/ c1_0 \/ c1_1 $_137 \/ % 0.20/0.52 c3_0 \/ c3_2 $_135 $_136 \/ c4_1 $_137 % 0.20/0.52 |- ~c1_1 $_138 \/ ~c2_1 $_140 \/ ~c2_2 $_138 $_139 \/ ~c3_2 $_138 a566 \/ % 0.20/0.52 ~c4_2 $_138 $_139 \/ ~ndr1_0 \/ ~ndr1_1 $_138 \/ c1_1 $_140 \/ % 0.20/0.52 c3_2 $_138 $_139 \/ c4_0 \/ c4_1 $_140 \/ definitionFOFtoCNF_1 % 0.20/0.52 |- ~c1_1 $_138 \/ ~c2_1 $_140 \/ ~c2_2 $_138 $_139 \/ ~c3_2 $_138 a566 \/ % 0.20/0.52 ~c4_2 $_138 $_139 \/ ~ndr1_0 \/ ~ndr1_1 $_138 \/ c1_1 $_140 \/ % 0.20/0.52 c3_2 $_138 $_139 \/ c4_1 $_140 \/ c5_0 \/ definitionFOFtoCNF_3 % 0.20/0.52 |- ~c1_1 $_138 \/ ~c2_1 $_140 \/ ~c2_2 $_138 $_139 \/ ~c3_2 $_138 a566 \/ % 0.20/0.52 ~c4_2 $_138 $_139 \/ ~ndr1_0 \/ ~ndr1_1 $_138 \/ c1_0 \/ c1_1 $_140 \/ % 0.20/0.52 c3_0 \/ c3_2 $_138 $_139 \/ c4_1 $_140 % 0.20/0.52 |- ~c1_1 $_141 \/ ~c2_1 $_143 \/ ~c2_2 $_141 $_142 \/ ~c4_2 $_141 $_142 \/ % 0.20/0.52 ~ndr1_0 \/ ~ndr1_1 $_141 \/ c1_1 $_143 \/ c3_2 $_141 $_142 \/ c4_0 \/ % 0.20/0.52 c4_1 $_143 \/ c4_2 $_141 a566 \/ definitionFOFtoCNF_1 % 0.20/0.52 |- ~c1_1 $_141 \/ ~c2_1 $_143 \/ ~c2_2 $_141 $_142 \/ ~c4_2 $_141 $_142 \/ % 0.20/0.52 ~ndr1_0 \/ ~ndr1_1 $_141 \/ c1_1 $_143 \/ c3_2 $_141 $_142 \/ % 0.20/0.52 c4_1 $_143 \/ c4_2 $_141 a566 \/ c5_0 \/ definitionFOFtoCNF_3 % 0.20/0.52 |- ~c1_1 $_141 \/ ~c2_1 $_143 \/ ~c2_2 $_141 $_142 \/ ~c4_2 $_141 $_142 \/ % 0.20/0.52 ~ndr1_0 \/ ~ndr1_1 $_141 \/ c1_0 \/ c1_1 $_143 \/ c3_0 \/ % 0.20/0.52 c3_2 $_141 $_142 \/ c4_1 $_143 \/ c4_2 $_141 a566 % 0.20/0.52 |- ~c3_1 $_148 \/ ~c4_1 $_147 \/ ~ndr1_0 \/ c2_2 $_148 a580 \/ % 0.20/0.52 c3_2 $_148 a579 \/ c5_1 $_147 \/ c5_2 $_147 a563 \/ % 0.20/0.52 definitionFOFtoCNF_5 $_147 % 0.20/0.52 |- ~c3_1 $_150 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a550 \/ c2_2 $_150 a580 \/ % 0.20/0.52 c3_0 \/ c3_2 $_150 a579 \/ c5_1 a550 \/ c5_2 a550 a563 \/ % 0.20/0.52 definitionFOFtoCNF_5 a550 % 0.20/0.52 |- ~c3_1 $_153 \/ ~c4_1 $_152 \/ ~ndr1_0 \/ c2_1 $_152 \/ c5_0 \/ % 0.20/0.52 c5_1 $_152 \/ c5_1 a556 \/ c5_2 $_152 a557 \/ % 0.20/0.52 definitionFOFtoCNF_2 $_152 \/ definitionFOFtoCNF_3 \/ ndr1_1 $_153 % 0.20/0.52 |- ~c3_1 $_158 \/ ~c4_1 $_157 \/ ~ndr1_0 \/ c2_1 $_157 \/ c4_0 \/ c5_0 \/ % 0.20/0.52 c5_1 $_157 \/ c5_1 a556 \/ c5_2 $_157 a557 \/ definitionFOFtoCNF_1 \/ % 0.20/0.52 definitionFOFtoCNF_2 $_157 \/ ndr1_1 $_158 % 0.20/0.52 |- ~c3_1 $_162 \/ ~c4_1 $_161 \/ ~ndr1_0 \/ c1_0 \/ c2_1 $_161 \/ c3_0 \/ % 0.20/0.52 c5_0 \/ c5_1 $_161 \/ c5_1 a556 \/ c5_2 $_161 a557 \/ % 0.20/0.52 definitionFOFtoCNF_2 $_161 \/ ndr1_1 $_162 % 0.20/0.52 |- ~c3_1 $_164 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a550 \/ c2_1 a550 \/ c3_0 \/ % 0.20/0.52 c5_0 \/ c5_1 a550 \/ c5_1 a556 \/ c5_2 a550 a557 \/ % 0.20/0.52 definitionFOFtoCNF_2 a550 \/ ndr1_1 $_164 % 0.20/0.52 |- ~c1_2 $_172 a580 \/ ~c2_2 $_172 a579 \/ ~c3_1 $_171 \/ ~c3_1 $_172 \/ % 0.20/0.52 ~c4_1 $_170 \/ ~ndr1_0 \/ c5_1 $_170 \/ c5_2 $_170 a563 \/ % 0.20/0.52 definitionFOFtoCNF_5 $_170 % 0.20/0.52 |- ~c1_2 $_182 a580 \/ ~c3_1 $_181 \/ ~c3_1 $_182 \/ ~c4_1 $_180 \/ % 0.20/0.52 ~ndr1_0 \/ c3_2 $_182 a579 \/ c5_1 $_180 \/ c5_2 $_180 a563 \/ % 0.20/0.52 definitionFOFtoCNF_5 $_180 % 0.20/0.52 |- ~c2_2 $_192 a579 \/ ~c3_1 $_191 \/ ~c3_1 $_192 \/ ~c4_1 $_190 \/ % 0.20/0.52 ~ndr1_0 \/ c2_2 $_192 a580 \/ c5_1 $_190 \/ c5_2 $_190 a563 \/ % 0.20/0.52 definitionFOFtoCNF_5 $_190 % 0.20/0.52 |- ~c3_1 $_197 \/ ~c4_1 $_196 \/ ~ndr1_0 \/ c2_1 $_196 \/ % 0.20/0.52 c2_2 $_197 a580 \/ c3_2 $_197 a579 \/ c5_0 \/ c5_1 $_196 \/ c5_1 a556 \/ % 0.20/0.52 c5_2 $_196 a557 \/ definitionFOFtoCNF_2 $_196 \/ definitionFOFtoCNF_3 % 0.20/0.52 |- ~c3_1 $_205 \/ ~c4_1 $_204 \/ ~ndr1_0 \/ c2_1 $_204 \/ % 0.20/0.52 c2_2 $_205 a580 \/ c3_2 $_205 a579 \/ c4_0 \/ c5_0 \/ c5_1 $_204 \/ % 0.20/0.52 c5_1 a556 \/ c5_2 $_204 a557 \/ definitionFOFtoCNF_1 \/ % 0.20/0.52 definitionFOFtoCNF_2 $_204 % 0.20/0.52 |- ~c3_1 $_209 \/ ~c4_1 $_208 \/ ~ndr1_0 \/ c1_0 \/ c2_1 $_208 \/ % 0.20/0.52 c2_2 $_209 a580 \/ c3_0 \/ c3_2 $_209 a579 \/ c5_0 \/ c5_1 $_208 \/ % 0.20/0.52 c5_1 a556 \/ c5_2 $_208 a557 \/ definitionFOFtoCNF_2 $_208 % 0.20/0.52 |- ~c3_1 $_211 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a550 \/ c2_1 a550 \/ % 0.20/0.52 c2_2 $_211 a580 \/ c3_0 \/ c3_2 $_211 a579 \/ c5_0 \/ c5_1 a550 \/ % 0.20/0.52 c5_1 a556 \/ c5_2 a550 a557 \/ definitionFOFtoCNF_2 a550 % 0.20/0.52 |- ~c1_2 $_266 a580 \/ ~c2_2 $_266 a579 \/ ~c3_1 $_265 \/ ~c3_1 $_266 \/ % 0.20/0.52 ~c4_1 $_264 \/ ~ndr1_0 \/ c2_1 $_264 \/ c5_0 \/ c5_1 $_264 \/ % 0.20/0.52 c5_1 a556 \/ c5_2 $_264 a557 \/ definitionFOFtoCNF_2 $_264 \/ % 0.20/0.52 definitionFOFtoCNF_3 % 0.20/0.52 |- ~c1_2 $_272 a580 \/ ~c3_1 $_271 \/ ~c3_1 $_272 \/ ~c4_1 $_270 \/ % 0.20/0.52 ~ndr1_0 \/ c2_1 $_270 \/ c3_2 $_272 a579 \/ c5_0 \/ c5_1 $_270 \/ % 0.20/0.52 c5_1 a556 \/ c5_2 $_270 a557 \/ definitionFOFtoCNF_2 $_270 \/ % 0.20/0.52 definitionFOFtoCNF_3 % 0.20/0.52 |- ~c2_2 $_278 a579 \/ ~c3_1 $_277 \/ ~c3_1 $_278 \/ ~c4_1 $_276 \/ % 0.20/0.52 ~ndr1_0 \/ c2_1 $_276 \/ c2_2 $_278 a580 \/ c5_0 \/ c5_1 $_276 \/ % 0.20/0.52 c5_1 a556 \/ c5_2 $_276 a557 \/ definitionFOFtoCNF_2 $_276 \/ % 0.20/0.52 definitionFOFtoCNF_3 % 0.20/0.52 |- ~c1_2 $_284 a580 \/ ~c2_2 $_284 a579 \/ ~c3_1 $_283 \/ ~c3_1 $_284 \/ % 0.20/0.52 ~c4_1 $_282 \/ ~ndr1_0 \/ c2_1 $_282 \/ c4_0 \/ c5_0 \/ c5_1 $_282 \/ % 0.20/0.52 c5_1 a556 \/ c5_2 $_282 a557 \/ definitionFOFtoCNF_1 \/ % 0.20/0.52 definitionFOFtoCNF_2 $_282 % 0.20/0.52 |- ~c1_2 $_290 a580 \/ ~c2_2 $_290 a579 \/ ~c3_1 $_289 \/ ~c3_1 $_290 \/ % 0.20/0.52 ~c4_1 $_288 \/ ~ndr1_0 \/ c1_0 \/ c2_1 $_288 \/ c3_0 \/ c5_0 \/ % 0.20/0.52 c5_1 $_288 \/ c5_1 a556 \/ c5_2 $_288 a557 \/ definitionFOFtoCNF_2 $_288 % 0.20/0.52 |- ~c1_2 $_296 a580 \/ ~c3_1 $_295 \/ ~c3_1 $_296 \/ ~c4_1 $_294 \/ % 0.20/0.52 ~ndr1_0 \/ c2_1 $_294 \/ c3_2 $_296 a579 \/ c4_0 \/ c5_0 \/ % 0.20/0.52 c5_1 $_294 \/ c5_1 a556 \/ c5_2 $_294 a557 \/ definitionFOFtoCNF_1 \/ % 0.20/0.52 definitionFOFtoCNF_2 $_294 % 0.20/0.52 |- ~c1_2 $_302 a580 \/ ~c3_1 $_301 \/ ~c3_1 $_302 \/ ~c4_1 $_300 \/ % 0.20/0.52 ~ndr1_0 \/ c1_0 \/ c2_1 $_300 \/ c3_0 \/ c3_2 $_302 a579 \/ c5_0 \/ % 0.20/0.52 c5_1 $_300 \/ c5_1 a556 \/ c5_2 $_300 a557 \/ definitionFOFtoCNF_2 $_300 % 0.20/0.52 |- ~c2_2 $_308 a579 \/ ~c3_1 $_307 \/ ~c3_1 $_308 \/ ~c4_1 $_306 \/ % 0.20/0.52 ~ndr1_0 \/ c1_0 \/ c2_1 $_306 \/ c2_2 $_308 a580 \/ c3_0 \/ c5_0 \/ % 0.20/0.52 c5_1 $_306 \/ c5_1 a556 \/ c5_2 $_306 a557 \/ definitionFOFtoCNF_2 $_306 % 0.20/0.52 |- ~c2_2 $_314 a579 \/ ~c3_1 $_313 \/ ~c3_1 $_314 \/ ~c4_1 $_312 \/ % 0.20/0.52 ~ndr1_0 \/ c2_1 $_312 \/ c2_2 $_314 a580 \/ c4_0 \/ c5_0 \/ % 0.20/0.52 c5_1 $_312 \/ c5_1 a556 \/ c5_2 $_312 a557 \/ definitionFOFtoCNF_1 \/ % 0.20/0.52 definitionFOFtoCNF_2 $_312 % 0.20/0.52 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.52 %------------------------------------------------------------------------------