%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN539+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n021.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:50 EDT 2022 % Result : CounterSatisfiable 0.47s 0.64s % Output : Saturation 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN539+1 : TPTP v8.1.0. Released v2.1.0. % 0.06/0.13 % Command : metis --show proof --show saturation %s % 0.13/0.33 % Computer : n021.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Tue Jul 12 08:52:24 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.47/0.64 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.47/0.64 % 0.47/0.64 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.47/0.64 |- c5_0 % 0.47/0.64 |- ~c1_2 $X25 $X26 \/ ~c1_2 $X25 a617 \/ ~c2_0 \/ ~c5_2 $X25 $X26 \/ % 0.47/0.64 ~ndr1_0 \/ ~ndr1_1 $X25 \/ c1_1 $X25 \/ c2_2 $X25 $X26 % 0.47/0.64 |- ~c1_2 $X25 $X26 \/ ~c2_0 \/ ~c5_2 $X25 $X26 \/ ~ndr1_0 \/ % 0.47/0.64 ~ndr1_1 $X25 \/ c1_1 $X25 \/ c2_2 $X25 $X26 \/ c4_2 $X25 a617 % 0.47/0.64 |- ~c3_1 a631 \/ ~c4_0 % 0.47/0.64 |- ~c4_0 \/ c1_1 a631 % 0.47/0.64 |- ~c4_0 \/ ndr1_0 % 0.47/0.64 |- ~c1_1 $X \/ ~c1_2 $X a595 \/ ~c5_2 $X $Y \/ ~ndr1_0 \/ ~ndr1_1 $X \/ % 0.47/0.64 c2_2 $X $Y % 0.47/0.64 |- ~c1_1 $X \/ ~c4_2 $X a595 \/ ~c5_2 $X $Y \/ ~ndr1_0 \/ ~ndr1_1 $X \/ % 0.47/0.64 c2_2 $X $Y % 0.47/0.64 |- ~c2_1 a637 \/ c3_0 % 0.47/0.64 |- ~c3_1 a637 \/ c3_0 % 0.47/0.64 |- ~c4_2 a637 a638 \/ c3_0 % 0.47/0.64 |- c1_2 a637 a638 \/ c3_0 % 0.47/0.64 |- c3_0 \/ ndr1_0 % 0.47/0.64 |- c3_0 \/ ndr1_1 a637 % 0.47/0.64 |- c2_1 a587 \/ c4_0 % 0.47/0.64 |- c3_1 a587 \/ c4_0 % 0.47/0.64 |- c4_0 \/ c5_1 a587 % 0.47/0.64 |- c4_0 \/ ndr1_0 % 0.47/0.64 |- ~c1_0 \/ ~c3_0 \/ ~c4_0 % 0.47/0.64 |- ~c1_0 \/ ~c1_1 a615 \/ ~c3_0 % 0.47/0.64 |- ~c1_0 \/ ~c2_2 a615 $X23 \/ ~c3_0 \/ ~c3_2 a615 $X23 \/ % 0.47/0.64 ~c5_2 a615 $X23 \/ ~ndr1_1 a615 % 0.47/0.64 |- ~c1_0 \/ ~c2_2 a615 $X24 \/ ~c3_0 \/ ~ndr1_1 a615 \/ c1_2 a615 $X24 \/ % 0.47/0.64 c3_2 a615 $X24 % 0.47/0.64 |- ~c1_0 \/ ~c2_2 $X32 $X33 \/ ~c3_1 $X32 \/ ~c3_2 $X32 a623 \/ ~c4_0 \/ % 0.47/0.64 ~c4_2 $X32 $X33 \/ ~ndr1_0 \/ ~ndr1_1 $X32 \/ c1_2 $X32 $X33 % 0.47/0.64 |- ~c1_0 \/ ~c4_1 a620 % 0.47/0.64 |- ~c1_0 \/ ndr1_0 % 0.47/0.64 |- ~c1_0 \/ ~c3_2 a605 $X8 \/ ~ndr1_0 \/ ~ndr1_1 $X10 \/ ~ndr1_1 a605 \/ % 0.47/0.64 c2_2 a605 $X8 \/ c3_1 $X10 \/ c4_2 $X10 $X11 \/ c5_2 $X10 $X11 % 0.47/0.64 |- ~c1_0 \/ ~c1_2 a605 $X9 \/ ~ndr1_0 \/ ~ndr1_1 $X10 \/ ~ndr1_1 a605 \/ % 0.47/0.64 c3_1 $X10 \/ c3_2 a605 $X9 \/ c4_2 $X10 $X11 \/ c5_2 $X10 $X11 \/ % 0.47/0.64 c5_2 a605 $X9 % 0.47/0.64 |- ~c1_1 a611 \/ ~c2_0 \/ ~c4_0 % 0.47/0.64 |- ~c1_2 a611 a612 \/ ~c2_0 \/ ~c4_0 % 0.47/0.64 |- ~c2_0 \/ ~c4_0 \/ c5_2 a611 a612 % 0.47/0.64 |- ~c2_0 \/ ~c4_0 \/ ndr1_1 a611 % 0.47/0.64 |- ~c2_0 \/ ~c3_2 a611 $X20 \/ ~c4_0 \/ ~ndr1_1 a611 \/ c2_2 a611 $X20 \/ % 0.47/0.64 c5_2 a611 $X20 % 0.47/0.64 |- ~c2_0 \/ ~c2_2 $X44 $X45 \/ ~c2_2 $X44 $X46 \/ ~c3_2 $X44 a636 \/ % 0.47/0.64 ~ndr1_0 \/ ~ndr1_1 $X44 \/ c1_2 $X44 $X45 \/ c4_2 $X44 $X46 % 0.47/0.64 |- ~c2_0 \/ ~c2_2 $X44 $X45 \/ ~c2_2 $X44 $X46 \/ ~ndr1_0 \/ % 0.47/0.64 ~ndr1_1 $X44 \/ c1_2 $X44 $X45 \/ c2_2 $X44 a636 \/ c4_2 $X44 $X46 % 0.47/0.64 |- ~c1_2 a588 a589 \/ ~c2_0 \/ ~c3_1 $U \/ ~ndr1_0 \/ c2_1 $U \/ c5_1 $U % 0.47/0.64 |- ~c2_0 \/ ~c2_2 a588 a591 \/ ~c3_1 $U \/ ~ndr1_0 \/ c2_1 $U \/ c5_1 $U % 0.47/0.64 |- ~c2_0 \/ ~c3_1 $U \/ ~c4_2 a588 a590 \/ ~ndr1_0 \/ c2_1 $U \/ c5_1 $U % 0.47/0.64 |- ~c2_0 \/ ~c3_1 $U \/ ~ndr1_0 \/ c1_2 a588 a590 \/ c2_1 $U \/ c5_1 $U % 0.47/0.64 |- ~c2_0 \/ ~c3_1 $U \/ ~ndr1_0 \/ c2_1 $U \/ c2_2 a588 a589 \/ c5_1 $U % 0.47/0.64 |- ~c2_0 \/ ~c3_1 $U \/ ~ndr1_0 \/ c2_1 $U \/ c2_2 a588 a590 \/ c5_1 $U % 0.47/0.64 |- ~c2_0 \/ ~c3_1 $U \/ ~ndr1_0 \/ c2_1 $U \/ c3_2 a588 a589 \/ c5_1 $U % 0.47/0.64 |- ~c2_0 \/ ~c3_1 $U \/ ~ndr1_0 \/ c2_1 $U \/ c5_1 $U \/ c5_2 a588 a591 % 0.47/0.64 |- ~c2_0 \/ ~c3_1 $U \/ ~ndr1_0 \/ c2_1 $U \/ c5_1 $U \/ ndr1_1 a588 % 0.47/0.64 |- ~c1_2 $X30 $X31 \/ ~c2_1 $X30 \/ ~c3_0 \/ ~c4_0 \/ ~c4_2 $X30 $X31 \/ % 0.47/0.64 ~ndr1_0 \/ ~ndr1_1 $X30 \/ c2_2 $X30 $X31 \/ c4_1 $X30 % 0.47/0.64 |- ~c3_0 \/ c1_0 \/ c4_0 % 0.47/0.64 |- ~c1_2 $X37 a628 \/ ~definitionFOFtoCNF_0 $X37 % 0.47/0.64 |- ~c5_2 $X37 a628 \/ ~definitionFOFtoCNF_0 $X37 % 0.47/0.64 |- ~definitionFOFtoCNF_0 $X37 \/ c4_2 $X37 a628 % 0.47/0.64 |- ~definitionFOFtoCNF_0 $X37 \/ ndr1_1 $X37 % 0.47/0.64 |- ~c4_2 $X37 a628 \/ ~ndr1_1 $X37 \/ c1_2 $X37 a628 \/ c5_2 $X37 a628 \/ % 0.47/0.64 definitionFOFtoCNF_0 $X37 % 0.47/0.64 |- ~c1_2 $X37 $X38 \/ ~c2_1 a629 \/ ~c3_0 \/ ~c4_1 $X37 \/ ~ndr1_0 \/ % 0.47/0.64 ~ndr1_1 $X37 \/ c2_2 $X37 $X38 \/ c3_2 $X37 $X38 \/ % 0.47/0.64 definitionFOFtoCNF_0 $X37 % 0.47/0.64 |- ~c1_2 $X37 $X38 \/ ~c2_2 a629 a630 \/ ~c3_0 \/ ~c4_1 $X37 \/ ~ndr1_0 \/ % 0.47/0.64 ~ndr1_1 $X37 \/ c2_2 $X37 $X38 \/ c3_2 $X37 $X38 \/ % 0.47/0.64 definitionFOFtoCNF_0 $X37 % 0.47/0.64 |- ~c1_2 $X37 $X38 \/ ~c3_0 \/ ~c4_1 $X37 \/ ~c5_2 a629 a630 \/ ~ndr1_0 \/ % 0.47/0.64 ~ndr1_1 $X37 \/ c2_2 $X37 $X38 \/ c3_2 $X37 $X38 \/ % 0.47/0.64 definitionFOFtoCNF_0 $X37 % 0.47/0.64 |- ~c1_2 $X37 $X38 \/ ~c3_0 \/ ~c4_1 $X37 \/ ~ndr1_0 \/ ~ndr1_1 $X37 \/ % 0.47/0.64 c2_2 $X37 $X38 \/ c3_1 a629 \/ c3_2 $X37 $X38 \/ % 0.47/0.64 definitionFOFtoCNF_0 $X37 % 0.47/0.64 |- ~c1_2 $X37 $X38 \/ ~c3_0 \/ ~c4_1 $X37 \/ ~ndr1_0 \/ ~ndr1_1 $X37 \/ % 0.47/0.64 c2_2 $X37 $X38 \/ c3_2 $X37 $X38 \/ definitionFOFtoCNF_0 $X37 \/ % 0.47/0.64 ndr1_1 a629 % 0.47/0.64 |- ~c3_0 \/ ~c3_1 $X21 \/ ~c3_1 a613 \/ ~ndr1_0 \/ c5_1 $X21 % 0.47/0.64 |- ~c3_0 \/ ~c3_1 $X21 \/ ~c3_2 a613 a614 \/ ~ndr1_0 \/ c5_1 $X21 % 0.47/0.64 |- ~c3_0 \/ ~c3_1 $X21 \/ ~c4_2 a613 a614 \/ ~ndr1_0 \/ c5_1 $X21 % 0.47/0.64 |- ~c3_0 \/ ~c3_1 $X21 \/ ~ndr1_0 \/ c1_2 a613 a614 \/ c5_1 $X21 % 0.47/0.64 |- ~c3_0 \/ ~c3_1 $X21 \/ ~ndr1_0 \/ c5_1 $X21 \/ ndr1_1 a613 % 0.47/0.64 |- ~c2_2 a613 $X22 \/ ~c3_0 \/ ~c3_1 $X21 \/ ~ndr1_0 \/ ~ndr1_1 a613 \/ % 0.47/0.64 c1_2 a613 $X22 \/ c5_1 $X21 % 0.47/0.64 |- c1_0 \/ c1_1 a619 % 0.47/0.64 |- c1_0 \/ c4_1 a619 % 0.47/0.64 |- c1_0 \/ c5_1 a619 % 0.47/0.64 |- c1_0 \/ ndr1_0 % 0.47/0.64 |- ~c2_1 a616 \/ c4_0 % 0.47/0.64 |- ~c3_1 a616 \/ c4_0 % 0.47/0.64 |- c1_1 a616 \/ c4_0 % 0.47/0.64 |- ~c1_2 $X42 $X43 \/ ~c2_1 a634 \/ ~c2_2 $X42 a635 \/ ~c5_1 $X42 \/ % 0.47/0.64 ~ndr1_0 \/ ~ndr1_1 $X42 \/ c1_0 \/ c2_2 $X42 $X43 % 0.47/0.64 |- ~c1_2 $X5 a604 \/ ~definitionFOFtoCNF_1 $X5 % 0.47/0.64 |- ~definitionFOFtoCNF_1 $X5 \/ c3_2 $X5 a604 % 0.47/0.64 |- ~definitionFOFtoCNF_1 $X5 \/ c4_2 $X5 a604 % 0.47/0.64 |- ~definitionFOFtoCNF_1 $X5 \/ ndr1_1 $X5 % 0.47/0.64 |- ~c3_2 $X5 a604 \/ ~c4_2 $X5 a604 \/ ~ndr1_1 $X5 \/ c1_2 $X5 a604 \/ % 0.47/0.64 definitionFOFtoCNF_1 $X5 % 0.47/0.64 |- ~c2_2 $X5 a602 \/ ~definitionFOFtoCNF_2 $X5 % 0.47/0.64 |- ~definitionFOFtoCNF_2 $X5 \/ c3_2 $X5 a602 % 0.47/0.64 |- ~definitionFOFtoCNF_2 $X5 \/ ndr1_1 $X5 % 0.47/0.64 |- ~c3_2 $X5 a602 \/ ~ndr1_1 $X5 \/ c2_2 $X5 a602 \/ % 0.47/0.64 definitionFOFtoCNF_2 $X5 % 0.47/0.65 |- ~c1_1 $X6 \/ ~c4_2 $X5 a603 \/ ~c5_2 $X6 $X7 \/ ~ndr1_0 \/ % 0.47/0.65 ~ndr1_1 $X6 \/ c1_0 \/ c1_2 $X6 $X7 \/ c4_2 $X6 $X7 \/ % 0.47/0.65 definitionFOFtoCNF_1 $X5 \/ definitionFOFtoCNF_2 $X5 % 0.47/0.65 |- ~c1_1 $X6 \/ ~c5_2 $X6 $X7 \/ ~ndr1_0 \/ ~ndr1_1 $X6 \/ c1_0 \/ % 0.47/0.65 c1_2 $X6 $X7 \/ c3_2 $X5 a603 \/ c4_2 $X6 $X7 \/ % 0.47/0.65 definitionFOFtoCNF_1 $X5 \/ definitionFOFtoCNF_2 $X5 % 0.47/0.65 |- ~c1_1 $X6 \/ ~c5_2 $X6 $X7 \/ ~ndr1_0 \/ ~ndr1_1 $X6 \/ c1_0 \/ % 0.47/0.65 c1_2 $X6 $X7 \/ c4_2 $X6 $X7 \/ c5_2 $X5 a603 \/ % 0.47/0.65 definitionFOFtoCNF_1 $X5 \/ definitionFOFtoCNF_2 $X5 % 0.47/0.65 |- ~c1_1 $X6 \/ ~c5_2 $X6 $X7 \/ ~ndr1_0 \/ ~ndr1_1 $X6 \/ c1_0 \/ % 0.47/0.65 c1_2 $X6 $X7 \/ c4_2 $X6 $X7 \/ definitionFOFtoCNF_1 $X5 \/ % 0.47/0.65 definitionFOFtoCNF_2 $X5 \/ ndr1_1 $X5 % 0.47/0.65 |- ~c2_1 $X27 \/ ~c2_2 $X27 a618 \/ ~ndr1_0 \/ c1_1 $X27 \/ c2_0 \/ c4_0 % 0.47/0.65 |- ~c2_1 $X27 \/ ~c3_2 $X27 a618 \/ ~ndr1_0 \/ c1_1 $X27 \/ c2_0 \/ c4_0 % 0.47/0.65 |- ~c2_1 $X27 \/ ~c4_2 $X27 a618 \/ ~ndr1_0 \/ c1_1 $X27 \/ c2_0 \/ c4_0 % 0.47/0.65 |- ~c2_1 $X27 \/ ~ndr1_0 \/ c1_1 $X27 \/ c2_0 \/ c4_0 \/ ndr1_1 $X27 % 0.47/0.65 |- ~c1_2 a596 a597 \/ ~c2_2 $Z $X1 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/ % 0.47/0.65 c2_0 \/ c2_1 $Z \/ c3_2 $Z $X1 % 0.47/0.65 |- ~c2_2 $Z $X1 \/ ~c2_2 a596 a597 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/ % 0.47/0.65 c2_0 \/ c2_1 $Z \/ c3_2 $Z $X1 % 0.47/0.65 |- ~c2_2 $Z $X1 \/ ~c4_2 a596 a598 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/ % 0.47/0.65 c2_0 \/ c2_1 $Z \/ c3_2 $Z $X1 % 0.47/0.65 |- ~c2_2 $Z $X1 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/ c1_2 a596 a598 \/ % 0.47/0.65 c2_0 \/ c2_1 $Z \/ c3_2 $Z $X1 % 0.47/0.65 |- ~c2_2 $Z $X1 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/ c2_0 \/ c2_1 $Z \/ % 0.47/0.65 c2_2 a596 a598 \/ c3_2 $Z $X1 % 0.47/0.65 |- ~c2_2 $Z $X1 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/ c2_0 \/ c2_1 $Z \/ % 0.47/0.65 c3_2 $Z $X1 \/ c5_2 a596 a597 % 0.47/0.65 |- ~c2_2 $Z $X1 \/ ~ndr1_0 \/ ~ndr1_1 $Z \/ c1_1 $Z \/ c2_0 \/ c2_1 $Z \/ % 0.47/0.65 c3_2 $Z $X1 \/ ndr1_1 a596 % 0.47/0.65 |- ~c1_2 a596 $X2 \/ ~c2_2 $Z $X1 \/ ~c4_2 a596 $X2 \/ ~ndr1_0 \/ % 0.47/0.65 ~ndr1_1 $Z \/ ~ndr1_1 a596 \/ c1_1 $Z \/ c2_0 \/ c2_1 $Z \/ % 0.47/0.65 c3_2 $Z $X1 \/ c3_2 a596 $X2 % 0.47/0.65 |- ~c2_2 $X35 a627 \/ ~definitionFOFtoCNF_3 $X35 % 0.47/0.65 |- ~definitionFOFtoCNF_3 $X35 \/ c1_2 $X35 a627 % 0.47/0.65 |- ~definitionFOFtoCNF_3 $X35 \/ ndr1_1 $X35 % 0.47/0.65 |- ~c1_2 $X35 a627 \/ ~ndr1_1 $X35 \/ c2_2 $X35 a627 \/ % 0.47/0.65 definitionFOFtoCNF_3 $X35 % 0.47/0.65 |- ~c1_2 $X35 $X36 \/ ~c1_2 a624 a625 \/ ~c3_1 $X35 \/ ~c3_2 $X35 $X36 \/ % 0.47/0.65 ~c5_2 $X35 $X36 \/ ~ndr1_0 \/ ~ndr1_1 $X35 \/ c2_0 \/ % 0.47/0.65 definitionFOFtoCNF_3 $X35 % 0.47/0.65 |- ~c1_2 $X35 $X36 \/ ~c2_2 a624 a625 \/ ~c3_1 $X35 \/ ~c3_2 $X35 $X36 \/ % 0.47/0.65 ~c5_2 $X35 $X36 \/ ~ndr1_0 \/ ~ndr1_1 $X35 \/ c2_0 \/ % 0.47/0.65 definitionFOFtoCNF_3 $X35 % 0.47/0.65 |- ~c1_2 $X35 $X36 \/ ~c3_1 $X35 \/ ~c3_2 $X35 $X36 \/ ~c3_2 a624 a626 \/ % 0.47/0.65 ~c5_2 $X35 $X36 \/ ~ndr1_0 \/ ~ndr1_1 $X35 \/ c2_0 \/ % 0.47/0.65 definitionFOFtoCNF_3 $X35 % 0.47/0.65 |- ~c1_2 $X35 $X36 \/ ~c3_1 $X35 \/ ~c3_2 $X35 $X36 \/ ~c5_2 $X35 $X36 \/ % 0.47/0.65 ~ndr1_0 \/ ~ndr1_1 $X35 \/ c2_0 \/ c3_2 a624 a625 \/ % 0.47/0.65 definitionFOFtoCNF_3 $X35 % 0.47/0.65 |- ~c1_2 $X35 $X36 \/ ~c3_1 $X35 \/ ~c3_2 $X35 $X36 \/ ~c5_2 $X35 $X36 \/ % 0.47/0.65 ~ndr1_0 \/ ~ndr1_1 $X35 \/ c2_0 \/ c4_2 a624 a626 \/ % 0.47/0.65 definitionFOFtoCNF_3 $X35 % 0.47/0.65 |- ~c1_2 $X35 $X36 \/ ~c3_1 $X35 \/ ~c3_2 $X35 $X36 \/ ~c5_2 $X35 $X36 \/ % 0.47/0.65 ~ndr1_0 \/ ~ndr1_1 $X35 \/ c2_0 \/ c5_2 a624 a626 \/ % 0.47/0.65 definitionFOFtoCNF_3 $X35 % 0.47/0.65 |- ~c1_2 $X35 $X36 \/ ~c3_1 $X35 \/ ~c3_2 $X35 $X36 \/ ~c5_2 $X35 $X36 \/ % 0.47/0.65 ~ndr1_0 \/ ~ndr1_1 $X35 \/ c2_0 \/ definitionFOFtoCNF_3 $X35 \/ % 0.47/0.65 ndr1_1 a624 % 0.47/0.65 |- ~c1_2 $X35 $X36 \/ ~c3_1 $X35 \/ ~c3_2 $X35 $X36 \/ ~c5_2 $X35 $X36 \/ % 0.47/0.65 ~ndr1_0 \/ ~ndr1_1 $X35 \/ ~ndr1_1 a624 \/ c2_0 \/ c2_2 a624 $X34 \/ % 0.47/0.65 c3_2 a624 $X34 \/ c5_2 a624 $X34 \/ definitionFOFtoCNF_3 $X35 % 0.47/0.65 |- ~c3_2 $X3 a599 \/ ~definitionFOFtoCNF_4 $X3 % 0.47/0.65 |- ~c5_2 $X3 a599 \/ ~definitionFOFtoCNF_4 $X3 % 0.47/0.65 |- ~definitionFOFtoCNF_4 $X3 \/ c2_2 $X3 a599 % 0.47/0.65 |- ~definitionFOFtoCNF_4 $X3 \/ ndr1_1 $X3 % 0.47/0.65 |- ~c2_2 $X3 a599 \/ ~ndr1_1 $X3 \/ c3_2 $X3 a599 \/ c5_2 $X3 a599 \/ % 0.47/0.65 definitionFOFtoCNF_4 $X3 % 0.47/0.65 |- ~c3_2 $X3 a600 \/ ~definitionFOFtoCNF_5 $X3 % 0.47/0.65 |- ~definitionFOFtoCNF_5 $X3 \/ c1_2 $X3 a600 % 0.47/0.65 |- ~definitionFOFtoCNF_5 $X3 \/ c2_2 $X3 a600 % 0.47/0.65 |- ~definitionFOFtoCNF_5 $X3 \/ ndr1_1 $X3 % 0.47/0.65 |- ~c1_2 $X3 a600 \/ ~c2_2 $X3 a600 \/ ~ndr1_1 $X3 \/ c3_2 $X3 a600 \/ % 0.47/0.65 definitionFOFtoCNF_5 $X3 % 0.47/0.65 |- ~c3_1 $X4 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $X3 \/ c2_1 $X4 \/ c2_2 $X4 a601 \/ % 0.47/0.65 definitionFOFtoCNF_4 $X3 \/ definitionFOFtoCNF_5 $X3 % 0.47/0.65 |- ~c3_1 $X4 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $X3 \/ c2_1 $X4 \/ c4_2 $X4 a601 \/ % 0.47/0.65 definitionFOFtoCNF_4 $X3 \/ definitionFOFtoCNF_5 $X3 % 0.47/0.65 |- ~c3_1 $X4 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $X3 \/ c2_1 $X4 \/ c5_2 $X4 a601 \/ % 0.47/0.65 definitionFOFtoCNF_4 $X3 \/ definitionFOFtoCNF_5 $X3 % 0.47/0.65 |- ~c3_1 $X4 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $X3 \/ c2_1 $X4 \/ % 0.47/0.65 definitionFOFtoCNF_4 $X3 \/ definitionFOFtoCNF_5 $X3 \/ ndr1_1 $X4 % 0.47/0.65 |- ~c2_2 $X39 a632 \/ ~definitionFOFtoCNF_6 $X39 % 0.47/0.65 |- ~c3_2 $X39 a632 \/ ~definitionFOFtoCNF_6 $X39 % 0.47/0.65 |- ~definitionFOFtoCNF_6 $X39 \/ ndr1_1 $X39 % 0.47/0.65 |- ~ndr1_1 $X39 \/ c2_2 $X39 a632 \/ c3_2 $X39 a632 \/ % 0.47/0.65 definitionFOFtoCNF_6 $X39 % 0.47/0.65 |- ~c1_1 a633 \/ ~c1_2 $X39 $X40 \/ ~ndr1_0 \/ ~ndr1_1 $X39 \/ c2_1 $X39 \/ % 0.47/0.65 c3_0 \/ c3_2 $X39 $X40 \/ c5_2 $X39 $X40 \/ definitionFOFtoCNF_6 $X39 % 0.47/0.65 |- ~c1_2 $X39 $X40 \/ ~c3_1 a633 \/ ~ndr1_0 \/ ~ndr1_1 $X39 \/ c2_1 $X39 \/ % 0.47/0.65 c3_0 \/ c3_2 $X39 $X40 \/ c5_2 $X39 $X40 \/ definitionFOFtoCNF_6 $X39 % 0.47/0.65 |- ~c1_2 $X39 $X40 \/ ~c3_2 a633 $X41 \/ ~ndr1_0 \/ ~ndr1_1 $X39 \/ % 0.47/0.65 ~ndr1_1 a633 \/ c1_2 a633 $X41 \/ c2_1 $X39 \/ c3_0 \/ c3_2 $X39 $X40 \/ % 0.47/0.65 c5_2 $X39 $X40 \/ definitionFOFtoCNF_6 $X39 % 0.47/0.65 |- ~definitionFOFtoCNF_7 \/ c1_1 a594 % 0.47/0.65 |- ~definitionFOFtoCNF_7 \/ c4_1 a594 % 0.47/0.65 |- ~definitionFOFtoCNF_7 \/ ndr1_0 % 0.47/0.65 |- ~c1_1 a594 \/ ~c4_1 a594 \/ ~ndr1_0 \/ definitionFOFtoCNF_7 % 0.47/0.65 |- ~c3_1 a592 \/ ~definitionFOFtoCNF_8 % 0.47/0.65 |- ~c4_1 a592 \/ ~definitionFOFtoCNF_8 % 0.47/0.65 |- ~definitionFOFtoCNF_8 \/ ndr1_0 % 0.47/0.65 |- ~ndr1_0 \/ c3_1 a592 \/ c4_1 a592 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- ~c5_1 a593 \/ definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- c2_1 a593 \/ definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_0 % 0.47/0.65 |- ~c1_2 a592 $V \/ ~c5_1 a593 \/ ~ndr1_1 a592 \/ c4_2 a592 $V \/ % 0.47/0.65 c5_2 a592 $V \/ definitionFOFtoCNF_7 % 0.47/0.65 |- ~c1_2 a592 $V \/ ~ndr1_1 a592 \/ c2_1 a593 \/ c4_2 a592 $V \/ % 0.47/0.65 c5_2 a592 $V \/ definitionFOFtoCNF_7 % 0.47/0.65 |- ~c1_2 a592 $V \/ ~ndr1_1 a592 \/ c4_2 a592 $V \/ c5_2 a592 $V \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ ndr1_0 % 0.47/0.65 |- ~c1_2 a593 $W \/ ~c4_2 a593 $W \/ ~ndr1_1 a593 \/ c5_2 a593 $W \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- ~c1_2 a592 $V \/ ~c1_2 a593 $W \/ ~c4_2 a593 $W \/ ~ndr1_1 a592 \/ % 0.47/0.65 ~ndr1_1 a593 \/ c4_2 a592 $V \/ c5_2 a592 $V \/ c5_2 a593 $W \/ % 0.47/0.65 definitionFOFtoCNF_7 % 0.47/0.65 |- ~c1_2 $X19 a610 \/ ~definitionFOFtoCNF_9 $X19 % 0.47/0.65 |- ~definitionFOFtoCNF_9 $X19 \/ c2_2 $X19 a610 % 0.47/0.65 |- ~definitionFOFtoCNF_9 $X19 \/ c3_2 $X19 a610 % 0.47/0.65 |- ~definitionFOFtoCNF_9 $X19 \/ ndr1_1 $X19 % 0.47/0.65 |- ~c2_2 $X19 a610 \/ ~c3_2 $X19 a610 \/ ~ndr1_1 $X19 \/ c1_2 $X19 a610 \/ % 0.47/0.65 definitionFOFtoCNF_9 $X19 % 0.47/0.65 |- ~c1_1 $X15 \/ ~c3_1 $X15 \/ ~c4_2 a608 a609 \/ ~ndr1_0 \/ % 0.47/0.65 ~ndr1_1 $X15 \/ c1_1 $X19 \/ c4_2 $X15 $X16 \/ c5_1 $X19 \/ % 0.47/0.65 c5_2 $X15 $X16 \/ definitionFOFtoCNF_9 $X19 % 0.47/0.65 |- ~c1_1 $X15 \/ ~c3_1 $X15 \/ ~ndr1_0 \/ ~ndr1_1 $X15 \/ c1_1 $X19 \/ % 0.47/0.65 c4_2 $X15 $X16 \/ c5_1 $X19 \/ c5_2 $X15 $X16 \/ c5_2 a608 a609 \/ % 0.47/0.65 definitionFOFtoCNF_9 $X19 % 0.47/0.65 |- ~c1_1 $X15 \/ ~c3_1 $X15 \/ ~ndr1_0 \/ ~ndr1_1 $X15 \/ c1_1 $X19 \/ % 0.47/0.65 c4_2 $X15 $X16 \/ c5_1 $X19 \/ c5_2 $X15 $X16 \/ % 0.47/0.65 definitionFOFtoCNF_9 $X19 \/ ndr1_1 a608 % 0.47/0.65 |- ~c1_1 $X15 \/ ~c2_2 a608 $X18 \/ ~c3_1 $X15 \/ ~c5_2 a608 $X18 \/ % 0.47/0.65 ~ndr1_0 \/ ~ndr1_1 $X15 \/ ~ndr1_1 a608 \/ c1_1 $X19 \/ % 0.47/0.65 c4_2 $X15 $X16 \/ c5_1 $X19 \/ c5_2 $X15 $X16 \/ % 0.47/0.65 definitionFOFtoCNF_9 $X19 % 0.47/0.65 |- ~c1_1 $X15 \/ ~c3_1 $X15 \/ ~c3_2 a608 $X17 \/ ~ndr1_0 \/ % 0.47/0.65 ~ndr1_1 $X15 \/ ~ndr1_1 a608 \/ c1_1 $X19 \/ c2_2 a608 $X17 \/ % 0.47/0.65 c4_2 $X15 $X16 \/ c5_1 $X19 \/ c5_2 $X15 $X16 \/ % 0.47/0.65 definitionFOFtoCNF_9 $X19 % 0.47/0.65 |- ~c1_2 $X29 a622 \/ ~definitionFOFtoCNF_10 $X29 % 0.47/0.65 |- ~definitionFOFtoCNF_10 $X29 \/ c5_2 $X29 a622 % 0.47/0.65 |- ~definitionFOFtoCNF_10 $X29 \/ ndr1_1 $X29 % 0.47/0.65 |- ~c5_2 $X29 a622 \/ ~ndr1_1 $X29 \/ c1_2 $X29 a622 \/ % 0.47/0.65 definitionFOFtoCNF_10 $X29 % 0.47/0.65 |- ~c2_1 $X29 \/ ~c2_2 $X29 a621 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $X28 \/ % 0.47/0.65 definitionFOFtoCNF_10 $X29 % 0.47/0.65 |- ~c2_1 $X29 \/ ~ndr1_0 \/ c1_2 $X29 a621 \/ c2_0 \/ c2_1 $X28 \/ % 0.47/0.65 definitionFOFtoCNF_10 $X29 % 0.47/0.65 |- ~c2_1 $X29 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $X28 \/ c4_2 $X29 a621 \/ % 0.47/0.65 definitionFOFtoCNF_10 $X29 % 0.47/0.65 |- ~c2_1 $X29 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $X28 \/ % 0.47/0.65 definitionFOFtoCNF_10 $X29 \/ ndr1_1 $X29 % 0.47/0.65 |- ~c1_2 $X47 a639 \/ ~c5_1 $X47 \/ ~ndr1_0 \/ c3_1 $X47 % 0.47/0.65 |- ~c2_2 $X47 a639 \/ ~c5_1 $X47 \/ ~ndr1_0 \/ c3_1 $X47 % 0.47/0.65 |- ~c5_1 $X47 \/ ~ndr1_0 \/ c3_1 $X47 \/ c5_2 $X47 a639 % 0.47/0.65 |- ~c5_1 $X47 \/ ~ndr1_0 \/ c3_1 $X47 \/ ndr1_1 $X47 % 0.47/0.65 |- ~c3_0 \/ ~c3_1 a613 \/ ~ndr1_0 \/ c5_1 a613 % 0.47/0.65 |- ~c2_0 \/ ~c2_2 $X44 $X46 \/ ~c3_2 $X44 a636 \/ ~ndr1_0 \/ % 0.47/0.65 ~ndr1_1 $X44 \/ c1_2 $X44 $X46 \/ c4_2 $X44 $X46 % 0.47/0.65 |- ~c2_0 \/ ~c2_2 $X44 $X46 \/ ~ndr1_0 \/ ~ndr1_1 $X44 \/ c1_2 $X44 $X46 \/ % 0.47/0.65 c2_2 $X44 a636 \/ c4_2 $X44 $X46 % 0.47/0.65 |- ~c2_2 a596 a597 \/ ~ndr1_0 \/ ~ndr1_1 a596 \/ c1_1 a596 \/ c2_0 \/ % 0.47/0.65 c2_1 a596 \/ c3_2 a596 a597 % 0.47/0.65 |- c3_1 a592 \/ c4_1 a592 \/ definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- c1_0 \/ c3_1 a592 \/ c4_1 a592 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- c3_1 a592 \/ c4_0 \/ c4_1 a592 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- c3_0 \/ c3_1 a592 \/ c4_1 a592 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- c1_0 \/ c3_1 a619 \/ ndr1_1 a619 % 0.47/0.65 |- c1_0 \/ c3_1 a619 \/ c5_2 a619 a639 % 0.47/0.65 |- c1_0 \/ c2_2 a619 a632 \/ c3_1 a619 \/ c3_2 a619 a632 \/ % 0.47/0.65 definitionFOFtoCNF_6 a619 % 0.47/0.65 |- c2_2 a637 a632 \/ c3_0 \/ c3_2 a637 a632 \/ definitionFOFtoCNF_6 a637 % 0.47/0.65 |- c1_1 a587 \/ c2_0 \/ c4_0 \/ ndr1_1 a587 % 0.47/0.65 |- c1_1 a587 \/ c2_0 \/ c2_2 a587 a632 \/ c3_2 a587 a632 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_6 a587 % 0.47/0.65 |- c1_1 a593 \/ c2_0 \/ c4_0 \/ definitionFOFtoCNF_7 \/ % 0.47/0.65 definitionFOFtoCNF_8 \/ ndr1_1 a593 % 0.47/0.65 |- c1_1 a593 \/ c2_0 \/ c2_2 a593 a632 \/ c3_2 a593 a632 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_6 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.65 definitionFOFtoCNF_8 % 0.47/0.65 |- c2_0 \/ c2_1 $_72 \/ c4_0 \/ definitionFOFtoCNF_10 a587 \/ ndr1_1 a587 % 0.47/0.65 |- c2_0 \/ c2_1 $_73 \/ c2_2 a587 a632 \/ c3_2 a587 a632 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_6 a587 % 0.47/0.65 |- c2_0 \/ c2_1 $_74 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 a593 % 0.47/0.65 |- c2_0 \/ c2_1 $_75 \/ c2_2 a593 a632 \/ c3_2 a593 a632 \/ % 0.47/0.65 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_6 a593 \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- c1_1 $_76 \/ c2_0 \/ c4_0 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.65 ndr1_1 $_76 \/ ndr1_1 a587 % 0.47/0.65 |- c1_1 $_77 \/ c2_0 \/ c2_2 $_77 a632 \/ c3_2 $_77 a632 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_6 $_77 \/ ndr1_1 a587 % 0.47/0.65 |- c1_1 $_77 \/ c2_0 \/ c2_2 a587 a632 \/ c3_2 a587 a632 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_6 a587 \/ ndr1_1 $_77 % 0.47/0.65 |- c1_2 a587 a621 \/ c2_0 \/ c2_1 $_82 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a587 % 0.47/0.65 |- c1_2 a593 a621 \/ c2_0 \/ c2_1 $_84 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- c1_1 $_86 \/ c1_2 a587 a621 \/ c2_0 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a587 \/ ndr1_1 $_86 % 0.47/0.65 |- c1_1 $_87 \/ c1_2 a587 a621 \/ c2_0 \/ c2_2 $_87 a632 \/ % 0.47/0.65 c3_2 $_87 a632 \/ c4_0 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.65 definitionFOFtoCNF_6 $_87 % 0.47/0.65 |- c2_0 \/ c2_1 $_90 \/ c4_0 \/ c4_2 a587 a621 \/ % 0.47/0.65 definitionFOFtoCNF_10 a587 % 0.47/0.65 |- c2_0 \/ c2_1 $_92 \/ c4_2 a593 a621 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- c1_1 $_94 \/ c2_0 \/ c4_0 \/ c4_2 a587 a621 \/ % 0.47/0.65 definitionFOFtoCNF_10 a587 \/ ndr1_1 $_94 % 0.47/0.65 |- c1_1 $_95 \/ c2_0 \/ c2_2 $_95 a632 \/ c3_2 $_95 a632 \/ c4_0 \/ % 0.47/0.65 c4_2 a587 a621 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.65 definitionFOFtoCNF_6 $_95 % 0.47/0.65 |- ~c1_1 a619 \/ ~c1_2 a619 a595 \/ ~ndr1_0 \/ ~ndr1_1 a619 \/ c1_0 \/ % 0.47/0.65 c2_2 a619 a639 \/ c3_1 a619 % 0.47/0.65 |- ~c1_1 a619 \/ ~c4_2 a619 a595 \/ ~ndr1_0 \/ ~ndr1_1 a619 \/ c1_0 \/ % 0.47/0.65 c2_2 a619 a639 \/ c3_1 a619 % 0.47/0.65 |- c1_1 $_101 \/ c1_2 a593 a621 \/ c2_0 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.65 definitionFOFtoCNF_8 \/ ndr1_1 $_101 % 0.47/0.65 |- c1_1 $_102 \/ c1_2 a593 a621 \/ c2_0 \/ c2_2 $_102 a632 \/ % 0.47/0.65 c3_2 $_102 a632 \/ c4_0 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.65 definitionFOFtoCNF_6 $_102 \/ definitionFOFtoCNF_7 \/ % 0.47/0.65 definitionFOFtoCNF_8 % 0.47/0.65 |- c1_1 $_105 \/ c2_0 \/ c4_0 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_105 \/ % 0.47/0.65 ndr1_1 a593 % 0.47/0.65 |- c1_1 $_106 \/ c2_0 \/ c2_2 $_106 a632 \/ c3_2 $_106 a632 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_6 $_106 \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 a593 % 0.47/0.65 |- c1_1 $_106 \/ c2_0 \/ c2_2 a593 a632 \/ c3_2 a593 a632 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_6 a593 \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_106 % 0.47/0.65 |- c1_1 $_111 \/ c2_0 \/ c4_0 \/ c4_2 a593 a621 \/ % 0.47/0.65 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.65 definitionFOFtoCNF_8 \/ ndr1_1 $_111 % 0.47/0.65 |- c1_1 $_112 \/ c2_0 \/ c2_2 $_112 a632 \/ c3_2 $_112 a632 \/ c4_0 \/ % 0.47/0.65 c4_2 a593 a621 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.65 definitionFOFtoCNF_6 $_112 \/ definitionFOFtoCNF_7 \/ % 0.47/0.65 definitionFOFtoCNF_8 % 0.47/0.65 |- c1_1 $_120 \/ c2_0 \/ c2_2 $_120 a632 \/ c2_2 a587 a632 \/ % 0.47/0.65 c3_2 $_120 a632 \/ c3_2 a587 a632 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_6 $_120 \/ % 0.47/0.65 definitionFOFtoCNF_6 a587 % 0.47/0.65 |- c2_0 \/ c2_1 $_74 \/ c5_2 a593 a621 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- ~c1_1 a593 \/ ~c4_2 a593 a595 \/ ~ndr1_0 \/ ~ndr1_1 a593 \/ c2_0 \/ % 0.47/0.65 c2_1 $_145 \/ c2_2 a593 a621 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- ~c1_1 a593 \/ ~c1_2 a593 a595 \/ ~ndr1_0 \/ ~ndr1_1 a593 \/ c2_0 \/ % 0.47/0.65 c2_1 $_145 \/ c2_2 a593 a621 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.65 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.65 |- c1_1 $_146 \/ c2_0 \/ c4_0 \/ c5_2 a593 a621 \/ % 0.47/0.65 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.65 definitionFOFtoCNF_8 \/ ndr1_1 $_146 % 0.47/0.65 |- ~c1_1 a593 \/ ~c4_2 a593 a595 \/ ~ndr1_0 \/ ~ndr1_1 a593 \/ % 0.47/0.65 c1_1 $_147 \/ c2_0 \/ c2_2 a593 a621 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.65 definitionFOFtoCNF_8 \/ ndr1_1 $_147 % 0.47/0.65 |- ~c1_1 a593 \/ ~c1_2 a593 a595 \/ ~ndr1_0 \/ ~ndr1_1 a593 \/ % 0.47/0.65 c1_1 $_147 \/ c2_0 \/ c2_2 a593 a621 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.65 definitionFOFtoCNF_8 \/ ndr1_1 $_147 % 0.47/0.65 |- c1_1 $_147 \/ c2_0 \/ c2_2 $_147 a632 \/ c3_2 $_147 a632 \/ c4_0 \/ % 0.47/0.65 c5_2 a593 a621 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.65 definitionFOFtoCNF_6 $_147 \/ definitionFOFtoCNF_7 \/ % 0.47/0.65 definitionFOFtoCNF_8 % 0.47/0.65 |- c1_1 $_156 \/ c2_0 \/ c2_2 $_156 a632 \/ c2_2 a593 a632 \/ % 0.47/0.65 c3_2 $_156 a632 \/ c3_2 a593 a632 \/ c4_0 \/ % 0.47/0.65 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_6 $_156 \/ % 0.47/0.65 definitionFOFtoCNF_6 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.65 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c2_1 a629 \/ ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ ~ndr1_1 a587 \/ % 0.47/0.66 c1_1 $_86 \/ c2_0 \/ c2_2 a587 a621 \/ c3_2 a587 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a587 \/ definitionFOFtoCNF_10 a587 \/ ndr1_1 $_86 % 0.47/0.66 |- ~c2_1 a629 \/ ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ ~ndr1_1 a593 \/ % 0.47/0.66 c1_1 $_101 \/ c2_0 \/ c2_2 a593 a621 \/ c3_2 a593 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a593 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_101 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ ~ndr1_1 a587 \/ c1_1 $_86 \/ c2_0 \/ % 0.47/0.66 c2_2 a587 a621 \/ c3_1 a629 \/ c3_2 a587 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a587 \/ definitionFOFtoCNF_10 a587 \/ ndr1_1 $_86 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ ~ndr1_1 a593 \/ c1_1 $_101 \/ c2_0 \/ % 0.47/0.66 c2_2 a593 a621 \/ c3_1 a629 \/ c3_2 a593 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a593 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_101 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ ~ndr1_1 a587 \/ c1_1 $_86 \/ c2_0 \/ % 0.47/0.66 c2_2 a587 a621 \/ c3_2 a587 a621 \/ c4_0 \/ definitionFOFtoCNF_0 a587 \/ % 0.47/0.66 definitionFOFtoCNF_10 a587 \/ ndr1_1 $_86 \/ ndr1_1 a629 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ ~ndr1_1 a593 \/ c1_1 $_101 \/ c2_0 \/ % 0.47/0.66 c2_2 a593 a621 \/ c3_2 a593 a621 \/ c4_0 \/ definitionFOFtoCNF_0 a593 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 \/ ndr1_1 $_101 \/ ndr1_1 a629 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c1_1 $_146 \/ c2_0 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_146 \/ % 0.47/0.66 ndr1_1 a624 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c2_0 \/ c2_1 $_74 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_3 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 \/ ndr1_1 a624 % 0.47/0.66 |- ~c1_1 a633 \/ ~ndr1_0 \/ c2_1 a637 \/ c3_0 \/ c3_2 a637 a638 \/ % 0.47/0.66 c5_2 a637 a638 \/ definitionFOFtoCNF_6 a637 % 0.47/0.66 |- ~c3_1 a633 \/ ~ndr1_0 \/ c2_1 a637 \/ c3_0 \/ c3_2 a637 a638 \/ % 0.47/0.66 c5_2 a637 a638 \/ definitionFOFtoCNF_6 a637 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c1_2 a624 a625 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ % 0.47/0.66 ~ndr1_0 \/ ~ndr1_1 a593 \/ c1_1 $_146 \/ c2_0 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_146 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c1_2 a624 a625 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ % 0.47/0.66 ~ndr1_0 \/ ~ndr1_1 a593 \/ c2_0 \/ c2_1 $_74 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c2_2 a624 a625 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ % 0.47/0.66 ~ndr1_0 \/ ~ndr1_1 a593 \/ c1_1 $_146 \/ c2_0 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_146 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c2_2 a624 a625 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ % 0.47/0.66 ~ndr1_0 \/ ~ndr1_1 a593 \/ c2_0 \/ c2_1 $_74 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~c3_2 a624 a626 \/ % 0.47/0.66 ~ndr1_0 \/ ~ndr1_1 a593 \/ c1_1 $_146 \/ c2_0 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_146 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~c3_2 a624 a626 \/ % 0.47/0.66 ~ndr1_0 \/ ~ndr1_1 a593 \/ c2_0 \/ c2_1 $_74 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c1_1 $_146 \/ c2_0 \/ c3_2 a624 a625 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_146 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c2_0 \/ c2_1 $_74 \/ c3_2 a624 a625 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c1_1 $_146 \/ c2_0 \/ c4_0 \/ c4_2 a624 a626 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_146 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c2_0 \/ c2_1 $_74 \/ c4_2 a624 a626 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c1_1 $_146 \/ c2_0 \/ c4_0 \/ c5_2 a624 a626 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_146 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c2_0 \/ c2_1 $_74 \/ c5_2 a624 a626 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c1_1 $_207 \/ c2_0 \/ c2_2 $_207 a632 \/ % 0.47/0.66 c3_2 $_207 a632 \/ c4_0 \/ c5_2 a624 a626 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_6 $_207 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c1_1 $_207 \/ c2_0 \/ c2_2 $_207 a632 \/ % 0.47/0.66 c3_2 $_207 a632 \/ c4_0 \/ c4_2 a624 a626 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_6 $_207 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c1_1 $_207 \/ c2_0 \/ c2_2 $_207 a632 \/ % 0.47/0.66 c3_2 $_207 a632 \/ c3_2 a624 a625 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.66 definitionFOFtoCNF_6 $_207 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~c3_2 a624 a626 \/ % 0.47/0.66 ~ndr1_0 \/ ~ndr1_1 a593 \/ c1_1 $_207 \/ c2_0 \/ c2_2 $_207 a632 \/ % 0.47/0.66 c3_2 $_207 a632 \/ c4_0 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_3 a593 \/ definitionFOFtoCNF_6 $_207 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c2_2 a624 a625 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ % 0.47/0.66 ~ndr1_0 \/ ~ndr1_1 a593 \/ c1_1 $_207 \/ c2_0 \/ c2_2 $_207 a632 \/ % 0.47/0.66 c3_2 $_207 a632 \/ c4_0 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_3 a593 \/ definitionFOFtoCNF_6 $_207 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c1_2 a624 a625 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ % 0.47/0.66 ~ndr1_0 \/ ~ndr1_1 a593 \/ c1_1 $_207 \/ c2_0 \/ c2_2 $_207 a632 \/ % 0.47/0.66 c3_2 $_207 a632 \/ c4_0 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_3 a593 \/ definitionFOFtoCNF_6 $_207 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 a593 \/ c1_1 $_207 \/ c2_0 \/ c2_2 $_207 a632 \/ % 0.47/0.66 c3_2 $_207 a632 \/ c4_0 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_3 a593 \/ definitionFOFtoCNF_6 $_207 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 a624 % 0.47/0.66 |- ~c1_1 a593 \/ ~c4_2 a593 a595 \/ ~ndr1_0 \/ ~ndr1_1 a593 \/ % 0.47/0.66 c1_1 $_207 \/ c2_0 \/ c2_2 $_207 a632 \/ c2_2 a593 a621 \/ % 0.47/0.66 c3_2 $_207 a632 \/ c4_0 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_6 $_207 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_1 a593 \/ ~c1_2 a593 a595 \/ ~ndr1_0 \/ ~ndr1_1 a593 \/ % 0.47/0.66 c1_1 $_207 \/ c2_0 \/ c2_2 $_207 a632 \/ c2_2 a593 a621 \/ % 0.47/0.66 c3_2 $_207 a632 \/ c4_0 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_6 $_207 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c2_1 a629 \/ ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $_208 \/ % 0.47/0.66 c2_1 $_72 \/ c2_2 a587 a621 \/ c3_2 a587 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a587 \/ definitionFOFtoCNF_10 a587 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $_209 \/ c2_1 $_72 \/ % 0.47/0.66 c2_2 a587 a621 \/ c3_1 a629 \/ c3_2 a587 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a587 \/ definitionFOFtoCNF_10 a587 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $_210 \/ c2_1 $_72 \/ % 0.47/0.66 c2_2 a587 a621 \/ c3_2 a587 a621 \/ c4_0 \/ definitionFOFtoCNF_0 a587 \/ % 0.47/0.66 definitionFOFtoCNF_10 a587 \/ ndr1_1 a629 % 0.47/0.66 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 $_211 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ % 0.47/0.66 c2_0 \/ c2_2 a587 a632 \/ c2_2 a605 a632 \/ c3_1 $_211 \/ % 0.47/0.66 c3_2 a587 a632 \/ c4_0 \/ c4_2 $_211 $_212 \/ c5_2 $_211 $_212 \/ % 0.47/0.66 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_6 a587 \/ % 0.47/0.66 definitionFOFtoCNF_6 a605 % 0.47/0.66 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 $_211 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ % 0.47/0.66 c1_2 a593 a621 \/ c2_0 \/ c2_2 a605 a632 \/ c3_1 $_211 \/ c4_0 \/ % 0.47/0.66 c4_2 $_211 $_212 \/ c5_2 $_211 $_212 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_6 a605 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 $_211 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ % 0.47/0.66 c1_2 a587 a621 \/ c2_0 \/ c2_2 a605 a632 \/ c3_1 $_211 \/ c4_0 \/ % 0.47/0.66 c4_2 $_211 $_212 \/ c5_2 $_211 $_212 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.66 definitionFOFtoCNF_6 a605 % 0.47/0.66 |- ~c1_0 \/ ~c3_2 a605 $_213 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_211 \/ % 0.47/0.66 c2_0 \/ c2_2 a593 a632 \/ c2_2 a605 $_213 \/ c3_1 $_211 \/ % 0.47/0.66 c3_2 a593 a632 \/ c4_0 \/ c4_2 $_211 $_212 \/ c5_2 $_211 $_212 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_6 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_0 \/ ~c3_2 a605 $_213 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_211 \/ % 0.47/0.66 c2_0 \/ c2_2 a605 $_213 \/ c3_1 $_211 \/ c4_0 \/ c4_2 $_211 $_212 \/ % 0.47/0.66 c5_2 $_211 $_212 \/ c5_2 a593 a621 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_0 \/ ~c3_2 a605 $_213 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_211 \/ % 0.47/0.66 c2_0 \/ c2_2 a587 a632 \/ c2_2 a605 $_213 \/ c3_1 $_211 \/ % 0.47/0.66 c3_2 a587 a632 \/ c4_0 \/ c4_2 $_211 $_212 \/ c5_2 $_211 $_212 \/ % 0.47/0.66 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_6 a587 % 0.47/0.66 |- ~c1_0 \/ ~c3_2 a605 $_213 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_211 \/ % 0.47/0.66 c2_0 \/ c2_2 a605 $_213 \/ c3_1 $_211 \/ c4_0 \/ c4_2 $_211 $_212 \/ % 0.47/0.66 c4_2 a593 a621 \/ c5_2 $_211 $_212 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_0 \/ ~c3_2 a605 $_213 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_211 \/ % 0.47/0.66 c2_0 \/ c2_2 a605 $_213 \/ c3_1 $_211 \/ c4_0 \/ c4_2 $_211 $_212 \/ % 0.47/0.66 c5_2 $_211 $_212 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 a593 % 0.47/0.66 |- ~c1_0 \/ ~c3_2 a605 $_213 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_211 \/ % 0.47/0.66 c1_2 a593 a621 \/ c2_0 \/ c2_2 a605 $_213 \/ c3_1 $_211 \/ c4_0 \/ % 0.47/0.66 c4_2 $_211 $_212 \/ c5_2 $_211 $_212 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_0 \/ ~c3_2 a605 $_213 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_211 \/ % 0.47/0.66 c2_0 \/ c2_2 a605 $_213 \/ c3_1 $_211 \/ c4_0 \/ c4_2 $_211 $_212 \/ % 0.47/0.66 c4_2 a587 a621 \/ c5_2 $_211 $_212 \/ definitionFOFtoCNF_10 a587 % 0.47/0.66 |- ~c1_0 \/ ~c3_2 a605 $_213 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_211 \/ % 0.47/0.66 c1_2 a587 a621 \/ c2_0 \/ c2_2 a605 $_213 \/ c3_1 $_211 \/ c4_0 \/ % 0.47/0.66 c4_2 $_211 $_212 \/ c5_2 $_211 $_212 \/ definitionFOFtoCNF_10 a587 % 0.47/0.66 |- ~c1_0 \/ ~c3_2 a605 $_213 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_211 \/ % 0.47/0.66 c2_0 \/ c2_2 a605 $_213 \/ c3_1 $_211 \/ c4_0 \/ c4_2 $_211 $_212 \/ % 0.47/0.66 c5_2 $_211 $_212 \/ definitionFOFtoCNF_10 a587 \/ ndr1_1 a587 % 0.47/0.66 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ c1_2 a587 a621 \/ % 0.47/0.66 c2_0 \/ c2_2 a605 a632 \/ c3_1 a605 \/ c4_0 \/ c4_2 a605 $_212 \/ % 0.47/0.66 c5_2 a605 $_212 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.66 definitionFOFtoCNF_6 a605 % 0.47/0.66 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ c2_0 \/ % 0.47/0.66 c2_2 a587 a632 \/ c2_2 a605 a632 \/ c3_1 a605 \/ c3_2 a587 a632 \/ % 0.47/0.66 c4_0 \/ c4_2 a605 $_212 \/ c5_2 a605 $_212 \/ % 0.47/0.66 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_6 a587 \/ % 0.47/0.66 definitionFOFtoCNF_6 a605 % 0.47/0.66 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ c1_2 a593 a621 \/ % 0.47/0.66 c2_0 \/ c2_2 a605 a632 \/ c3_1 a605 \/ c4_0 \/ c4_2 a605 $_212 \/ % 0.47/0.66 c5_2 a605 $_212 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_6 a605 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c2_1 a629 \/ ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $_217 \/ % 0.47/0.66 c2_1 $_74 \/ c2_2 a593 a621 \/ c3_2 a593 a621 \/ % 0.47/0.66 definitionFOFtoCNF_0 a593 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $_218 \/ c2_1 $_74 \/ % 0.47/0.66 c2_2 a593 a621 \/ c3_1 a629 \/ c3_2 a593 a621 \/ % 0.47/0.66 definitionFOFtoCNF_0 a593 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ c2_0 \/ c2_1 $_219 \/ c2_1 $_74 \/ % 0.47/0.66 c2_2 a593 a621 \/ c3_2 a593 a621 \/ definitionFOFtoCNF_0 a593 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 \/ ndr1_1 a629 % 0.47/0.66 |- ~c2_1 a629 \/ ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ c1_1 $_220 \/ % 0.47/0.66 c1_1 a587 \/ c2_0 \/ c2_2 a587 a621 \/ c3_2 a587 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a587 \/ definitionFOFtoCNF_10 a587 \/ ndr1_1 $_220 % 0.47/0.66 |- ~c2_1 a629 \/ ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ c1_1 $_220 \/ % 0.47/0.66 c1_1 $_76 \/ c2_0 \/ c2_2 a587 a621 \/ c3_2 a587 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a587 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.66 ndr1_1 $_220 \/ ndr1_1 $_76 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ c1_1 $_221 \/ c1_1 a587 \/ c2_0 \/ % 0.47/0.66 c2_2 a587 a621 \/ c3_1 a629 \/ c3_2 a587 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a587 \/ definitionFOFtoCNF_10 a587 \/ ndr1_1 $_221 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ c1_1 $_221 \/ c1_1 $_76 \/ c2_0 \/ % 0.47/0.66 c2_2 a587 a621 \/ c3_1 a629 \/ c3_2 a587 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a587 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.66 ndr1_1 $_221 \/ ndr1_1 $_76 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ c1_1 $_222 \/ c1_1 a587 \/ c2_0 \/ % 0.47/0.66 c2_2 a587 a621 \/ c3_2 a587 a621 \/ c4_0 \/ definitionFOFtoCNF_0 a587 \/ % 0.47/0.66 definitionFOFtoCNF_10 a587 \/ ndr1_1 $_222 \/ ndr1_1 a629 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a587 \/ ~ndr1_0 \/ c1_1 $_222 \/ c1_1 $_76 \/ c2_0 \/ % 0.47/0.66 c2_2 a587 a621 \/ c3_2 a587 a621 \/ c4_0 \/ definitionFOFtoCNF_0 a587 \/ % 0.47/0.66 definitionFOFtoCNF_10 a587 \/ ndr1_1 $_222 \/ ndr1_1 $_76 \/ ndr1_1 a629 % 0.47/0.66 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 $X10 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ c2_0 \/ % 0.47/0.66 c2_2 a593 a632 \/ c2_2 a605 a632 \/ c3_1 $X10 \/ c3_2 a593 a632 \/ % 0.47/0.66 c4_0 \/ c4_2 $X10 $X11 \/ c5_2 $X10 $X11 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_6 a593 \/ % 0.47/0.66 definitionFOFtoCNF_6 a605 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ c2_0 \/ % 0.47/0.66 c2_2 a593 a632 \/ c2_2 a605 a632 \/ c3_1 a605 \/ c3_2 a593 a632 \/ % 0.47/0.66 c4_0 \/ c4_2 a605 $X11 \/ c5_2 a605 $X11 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_6 a593 \/ % 0.47/0.66 definitionFOFtoCNF_6 a605 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- c1_0 \/ c1_2 a619 a639 \/ c3_1 a619 \/ c4_2 a619 a639 \/ % 0.47/0.66 definitionFOFtoCNF_1 $_238 \/ definitionFOFtoCNF_2 $_238 \/ ndr1_1 $_238 % 0.47/0.66 |- c1_0 \/ c1_2 a619 a639 \/ c2_2 $_239 a632 \/ c3_1 a619 \/ % 0.47/0.66 c3_2 $_239 a632 \/ c4_2 a619 a639 \/ definitionFOFtoCNF_1 $_239 \/ % 0.47/0.66 definitionFOFtoCNF_2 $_239 \/ definitionFOFtoCNF_6 $_239 % 0.47/0.66 |- ~c1_1 a593 \/ ~c3_1 a593 \/ ~ndr1_0 \/ c1_1 $_105 \/ c1_1 $_243 \/ % 0.47/0.66 c2_0 \/ c4_0 \/ c4_2 a593 $_242 \/ c5_1 $_243 \/ c5_2 a593 $_242 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 \/ definitionFOFtoCNF_9 $_243 \/ ndr1_1 $_105 \/ % 0.47/0.66 ndr1_1 a608 % 0.47/0.66 |- ~c1_1 a593 \/ ~c3_1 a593 \/ ~ndr1_0 \/ c1_1 $_243 \/ c2_0 \/ % 0.47/0.66 c2_1 $_74 \/ c4_2 a593 $_242 \/ c5_1 $_243 \/ c5_2 a593 $_242 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 \/ definitionFOFtoCNF_9 $_243 \/ ndr1_1 a608 % 0.47/0.66 |- ~c1_1 $_241 \/ ~c3_1 $_241 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_243 \/ % 0.47/0.66 c1_2 a619 a639 \/ c3_1 a619 \/ c4_2 $_241 $_242 \/ c4_2 a619 a639 \/ % 0.47/0.66 c5_1 $_243 \/ c5_2 $_241 $_242 \/ definitionFOFtoCNF_1 $_241 \/ % 0.47/0.66 definitionFOFtoCNF_2 $_241 \/ definitionFOFtoCNF_9 $_243 \/ ndr1_1 a608 % 0.47/0.66 |- c1_0 \/ c1_2 a619 a639 \/ c3_1 a619 \/ c3_2 $_251 a603 \/ % 0.47/0.66 c4_2 a619 a639 \/ definitionFOFtoCNF_1 $_251 \/ % 0.47/0.66 definitionFOFtoCNF_2 $_251 % 0.47/0.66 |- ~c1_1 a619 \/ ~c4_2 $_253 a603 \/ ~ndr1_0 \/ ~ndr1_1 a619 \/ c1_0 \/ % 0.47/0.66 c1_2 a619 a639 \/ c3_1 a619 \/ c4_2 a619 a639 \/ % 0.47/0.66 definitionFOFtoCNF_1 $_253 \/ definitionFOFtoCNF_2 $_253 % 0.47/0.66 |- c1_0 \/ c1_2 a619 a639 \/ c3_1 a619 \/ c4_2 a619 a639 \/ % 0.47/0.66 c5_2 $_262 a603 \/ definitionFOFtoCNF_1 $_262 \/ % 0.47/0.66 definitionFOFtoCNF_2 $_262 % 0.47/0.66 |- ~c1_2 $_263 a603 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_263 \/ c1_0 \/ % 0.47/0.66 c1_1 $_263 \/ c1_2 a619 a639 \/ c2_2 $_263 a603 \/ c3_1 a619 \/ % 0.47/0.66 c4_2 $_263 a617 \/ c4_2 a619 a639 \/ definitionFOFtoCNF_1 $_263 \/ % 0.47/0.66 definitionFOFtoCNF_2 $_263 % 0.47/0.66 |- ~c1_2 $_263 a603 \/ ~c1_2 $_263 a617 \/ ~c2_0 \/ ~ndr1_0 \/ % 0.47/0.66 ~ndr1_1 $_263 \/ c1_0 \/ c1_1 $_263 \/ c1_2 a619 a639 \/ % 0.47/0.66 c2_2 $_263 a603 \/ c3_1 a619 \/ c4_2 a619 a639 \/ % 0.47/0.66 definitionFOFtoCNF_1 $_263 \/ definitionFOFtoCNF_2 $_263 % 0.47/0.66 |- ~c1_1 $_263 \/ ~c4_2 $_263 a595 \/ ~ndr1_0 \/ ~ndr1_1 $_263 \/ c1_0 \/ % 0.47/0.66 c1_2 a619 a639 \/ c2_2 $_263 a603 \/ c3_1 a619 \/ c4_2 a619 a639 \/ % 0.47/0.66 definitionFOFtoCNF_1 $_263 \/ definitionFOFtoCNF_2 $_263 % 0.47/0.66 |- ~c1_1 $_263 \/ ~c1_2 $_263 a595 \/ ~ndr1_0 \/ ~ndr1_1 $_263 \/ c1_0 \/ % 0.47/0.66 c1_2 a619 a639 \/ c2_2 $_263 a603 \/ c3_1 a619 \/ c4_2 a619 a639 \/ % 0.47/0.66 definitionFOFtoCNF_1 $_263 \/ definitionFOFtoCNF_2 $_263 % 0.47/0.66 |- ~c1_1 $_266 \/ ~c3_1 $_266 \/ ~c4_2 a608 a609 \/ ~ndr1_0 \/ c1_0 \/ % 0.47/0.66 c1_1 $_268 \/ c1_2 a619 a639 \/ c3_1 a619 \/ c4_2 $_266 $_267 \/ % 0.47/0.66 c4_2 a619 a639 \/ c5_1 $_268 \/ c5_2 $_266 $_267 \/ % 0.47/0.66 definitionFOFtoCNF_1 $_266 \/ definitionFOFtoCNF_2 $_266 \/ % 0.47/0.66 definitionFOFtoCNF_9 $_268 % 0.47/0.66 |- ~c1_1 a593 \/ ~c3_1 a593 \/ ~ndr1_0 \/ c1_1 $_105 \/ c1_1 $_271 \/ % 0.47/0.66 c2_0 \/ c4_0 \/ c4_2 a593 $_270 \/ c5_1 $_271 \/ c5_2 a593 $_270 \/ % 0.47/0.66 c5_2 a608 a609 \/ definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 \/ definitionFOFtoCNF_9 $_271 \/ ndr1_1 $_105 % 0.47/0.66 |- ~c1_1 a593 \/ ~c3_1 a593 \/ ~ndr1_0 \/ c1_1 $_271 \/ c2_0 \/ % 0.47/0.66 c2_1 $_74 \/ c4_2 a593 $_270 \/ c5_1 $_271 \/ c5_2 a593 $_270 \/ % 0.47/0.66 c5_2 a608 a609 \/ definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 \/ definitionFOFtoCNF_9 $_271 % 0.47/0.66 |- ~c1_1 $_269 \/ ~c3_1 $_269 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_271 \/ % 0.47/0.66 c1_2 a619 a639 \/ c3_1 a619 \/ c4_2 $_269 $_270 \/ c4_2 a619 a639 \/ % 0.47/0.66 c5_1 $_271 \/ c5_2 $_269 $_270 \/ c5_2 a608 a609 \/ % 0.47/0.66 definitionFOFtoCNF_1 $_269 \/ definitionFOFtoCNF_2 $_269 \/ % 0.47/0.66 definitionFOFtoCNF_9 $_271 % 0.47/0.66 |- ~c1_0 \/ ~c1_2 a605 $_274 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_272 \/ % 0.47/0.66 c2_0 \/ c2_2 a593 a632 \/ c3_1 $_272 \/ c3_2 a593 a632 \/ % 0.47/0.66 c3_2 a605 $_274 \/ c4_0 \/ c4_2 $_272 $_273 \/ c5_2 $_272 $_273 \/ % 0.47/0.66 c5_2 a605 $_274 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_6 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_0 \/ ~c1_2 a605 $_274 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_272 \/ % 0.47/0.66 c2_0 \/ c3_1 $_272 \/ c3_2 a605 $_274 \/ c4_0 \/ c4_2 $_272 $_273 \/ % 0.47/0.66 c5_2 $_272 $_273 \/ c5_2 a593 a621 \/ c5_2 a605 $_274 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_0 \/ ~c1_2 a605 $_274 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_272 \/ % 0.47/0.66 c2_0 \/ c2_2 a587 a632 \/ c3_1 $_272 \/ c3_2 a587 a632 \/ % 0.47/0.66 c3_2 a605 $_274 \/ c4_0 \/ c4_2 $_272 $_273 \/ c5_2 $_272 $_273 \/ % 0.47/0.66 c5_2 a605 $_274 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.66 definitionFOFtoCNF_6 a587 % 0.47/0.66 |- ~c1_0 \/ ~c1_2 a605 $_274 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_272 \/ % 0.47/0.66 c2_0 \/ c3_1 $_272 \/ c3_2 a605 $_274 \/ c4_0 \/ c4_2 $_272 $_273 \/ % 0.47/0.66 c4_2 a593 a621 \/ c5_2 $_272 $_273 \/ c5_2 a605 $_274 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_0 \/ ~c1_2 a605 $_274 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_272 \/ % 0.47/0.66 c2_0 \/ c3_1 $_272 \/ c3_2 a605 $_274 \/ c4_0 \/ c4_2 $_272 $_273 \/ % 0.47/0.66 c5_2 $_272 $_273 \/ c5_2 a605 $_274 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 a593 % 0.47/0.66 |- ~c1_0 \/ ~c1_2 a605 $_274 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_272 \/ % 0.47/0.66 c1_2 a593 a621 \/ c2_0 \/ c3_1 $_272 \/ c3_2 a605 $_274 \/ c4_0 \/ % 0.47/0.66 c4_2 $_272 $_273 \/ c5_2 $_272 $_273 \/ c5_2 a605 $_274 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 % 0.47/0.66 |- ~c1_0 \/ ~c1_2 a605 $_274 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_272 \/ % 0.47/0.66 c2_0 \/ c3_1 $_272 \/ c3_2 a605 $_274 \/ c4_0 \/ c4_2 $_272 $_273 \/ % 0.47/0.66 c4_2 a587 a621 \/ c5_2 $_272 $_273 \/ c5_2 a605 $_274 \/ % 0.47/0.66 definitionFOFtoCNF_10 a587 % 0.47/0.66 |- ~c1_0 \/ ~c1_2 a605 $_274 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_272 \/ % 0.47/0.66 c1_2 a587 a621 \/ c2_0 \/ c3_1 $_272 \/ c3_2 a605 $_274 \/ c4_0 \/ % 0.47/0.66 c4_2 $_272 $_273 \/ c5_2 $_272 $_273 \/ c5_2 a605 $_274 \/ % 0.47/0.66 definitionFOFtoCNF_10 a587 % 0.47/0.66 |- ~c1_0 \/ ~c1_2 a605 $_274 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_272 \/ % 0.47/0.66 c2_0 \/ c3_1 $_272 \/ c3_2 a605 $_274 \/ c4_0 \/ c4_2 $_272 $_273 \/ % 0.47/0.66 c5_2 $_272 $_273 \/ c5_2 a605 $_274 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.66 ndr1_1 a587 % 0.47/0.66 |- ~c2_1 a629 \/ ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ c1_1 $_278 \/ % 0.47/0.66 c1_1 a593 \/ c2_0 \/ c2_2 a593 a621 \/ c3_2 a593 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a593 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_278 % 0.47/0.66 |- ~c2_1 a629 \/ ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ c1_1 $_105 \/ % 0.47/0.66 c1_1 $_278 \/ c2_0 \/ c2_2 a593 a621 \/ c3_2 a593 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a593 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_105 \/ % 0.47/0.66 ndr1_1 $_278 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ c1_1 $_279 \/ c1_1 a593 \/ c2_0 \/ % 0.47/0.66 c2_2 a593 a621 \/ c3_1 a629 \/ c3_2 a593 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a593 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_279 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ c1_1 $_105 \/ c1_1 $_279 \/ c2_0 \/ % 0.47/0.66 c2_2 a593 a621 \/ c3_1 a629 \/ c3_2 a593 a621 \/ c4_0 \/ % 0.47/0.66 definitionFOFtoCNF_0 a593 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.66 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_105 \/ % 0.47/0.66 ndr1_1 $_279 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ c1_1 $_280 \/ c1_1 a593 \/ c2_0 \/ % 0.47/0.66 c2_2 a593 a621 \/ c3_2 a593 a621 \/ c4_0 \/ definitionFOFtoCNF_0 a593 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 \/ ndr1_1 $_280 \/ ndr1_1 a629 % 0.47/0.66 |- ~c3_0 \/ ~c4_1 a593 \/ ~ndr1_0 \/ c1_1 $_105 \/ c1_1 $_280 \/ c2_0 \/ % 0.47/0.66 c2_2 a593 a621 \/ c3_2 a593 a621 \/ c4_0 \/ definitionFOFtoCNF_0 a593 \/ % 0.47/0.66 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.66 definitionFOFtoCNF_8 \/ ndr1_1 $_105 \/ ndr1_1 $_280 \/ ndr1_1 a629 % 0.47/0.67 |- ~c1_0 \/ c1_1 a605 \/ c2_0 \/ c2_2 a605 a632 \/ c3_1 a605 \/ c4_0 \/ % 0.47/0.67 c4_2 a605 $_282 \/ c5_2 a605 $_282 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 \/ ndr1_1 a587 % 0.47/0.67 |- ~c3_0 \/ ~c4_0 \/ c2_0 \/ c2_1 $_290 \/ c2_1 $_291 \/ c2_1 $_292 \/ % 0.47/0.67 c2_2 a593 a621 \/ c4_1 a593 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.67 |- ~c1_2 $_317 a603 \/ ~c3_1 $_317 \/ ~ndr1_0 \/ ~ndr1_1 $_317 \/ c1_0 \/ % 0.47/0.67 c1_2 a619 a639 \/ c2_0 \/ c3_1 a619 \/ c4_2 a619 a639 \/ % 0.47/0.67 definitionFOFtoCNF_1 $_317 \/ definitionFOFtoCNF_2 $_317 \/ % 0.47/0.67 definitionFOFtoCNF_3 $_317 \/ ndr1_1 a624 % 0.47/0.67 |- ~c1_2 $_319 a603 \/ ~c3_1 $_319 \/ ~ndr1_0 \/ ~ndr1_1 $_319 \/ c1_0 \/ % 0.47/0.67 c1_2 a619 a639 \/ c2_0 \/ c3_1 a619 \/ c4_2 a619 a639 \/ % 0.47/0.67 c5_2 a624 a626 \/ definitionFOFtoCNF_1 $_319 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_319 \/ definitionFOFtoCNF_3 $_319 % 0.47/0.67 |- ~c1_2 $_321 a603 \/ ~c3_1 $_321 \/ ~ndr1_0 \/ ~ndr1_1 $_321 \/ c1_0 \/ % 0.47/0.67 c1_2 a619 a639 \/ c2_0 \/ c3_1 a619 \/ c4_2 a619 a639 \/ % 0.47/0.67 c4_2 a624 a626 \/ definitionFOFtoCNF_1 $_321 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_321 \/ definitionFOFtoCNF_3 $_321 % 0.47/0.67 |- ~c1_2 $_323 a603 \/ ~c3_1 $_323 \/ ~ndr1_0 \/ ~ndr1_1 $_323 \/ c1_0 \/ % 0.47/0.67 c1_2 a619 a639 \/ c2_0 \/ c3_1 a619 \/ c3_2 a624 a625 \/ % 0.47/0.67 c4_2 a619 a639 \/ definitionFOFtoCNF_1 $_323 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_323 \/ definitionFOFtoCNF_3 $_323 % 0.47/0.67 |- ~c1_2 $_325 a603 \/ ~c3_1 $_325 \/ ~c3_2 a624 a626 \/ ~ndr1_0 \/ % 0.47/0.67 ~ndr1_1 $_325 \/ c1_0 \/ c1_2 a619 a639 \/ c2_0 \/ c3_1 a619 \/ % 0.47/0.67 c4_2 a619 a639 \/ definitionFOFtoCNF_1 $_325 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_325 \/ definitionFOFtoCNF_3 $_325 % 0.47/0.67 |- ~c1_2 $_327 a603 \/ ~c2_2 a624 a625 \/ ~c3_1 $_327 \/ ~ndr1_0 \/ % 0.47/0.67 ~ndr1_1 $_327 \/ c1_0 \/ c1_2 a619 a639 \/ c2_0 \/ c3_1 a619 \/ % 0.47/0.67 c4_2 a619 a639 \/ definitionFOFtoCNF_1 $_327 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_327 \/ definitionFOFtoCNF_3 $_327 % 0.47/0.67 |- ~c1_2 $_329 a603 \/ ~c1_2 a624 a625 \/ ~c3_1 $_329 \/ ~ndr1_0 \/ % 0.47/0.67 ~ndr1_1 $_329 \/ c1_0 \/ c1_2 a619 a639 \/ c2_0 \/ c3_1 a619 \/ % 0.47/0.67 c4_2 a619 a639 \/ definitionFOFtoCNF_1 $_329 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_329 \/ definitionFOFtoCNF_3 $_329 % 0.47/0.67 |- ~c1_0 \/ c1_1 a605 \/ c2_0 \/ c2_2 a605 a632 \/ c3_1 a605 \/ c4_0 \/ % 0.47/0.67 c4_2 a605 $_332 \/ c5_2 a605 $_332 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 \/ definitionFOFtoCNF_7 \/ % 0.47/0.67 definitionFOFtoCNF_8 \/ ndr1_1 a593 % 0.47/0.67 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.67 ~ndr1_1 a593 \/ ~ndr1_1 a624 \/ c1_1 $_147 \/ c2_0 \/ c2_2 $_147 a632 \/ % 0.47/0.67 c2_2 a624 $_335 \/ c3_2 $_147 a632 \/ c3_2 a624 $_335 \/ c4_0 \/ % 0.47/0.67 c5_2 a624 $_335 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_3 a593 \/ definitionFOFtoCNF_6 $_147 \/ % 0.47/0.67 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 % 0.47/0.67 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.67 ~ndr1_1 a593 \/ ~ndr1_1 a624 \/ c1_1 $_146 \/ c2_0 \/ c2_2 a624 $_335 \/ % 0.47/0.67 c3_2 a624 $_335 \/ c4_0 \/ c5_2 a624 $_335 \/ % 0.47/0.67 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_3 a593 \/ % 0.47/0.67 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 $_146 % 0.47/0.67 |- ~c1_2 a593 a621 \/ ~c3_1 a593 \/ ~c3_2 a593 a621 \/ ~ndr1_0 \/ % 0.47/0.67 ~ndr1_1 a593 \/ ~ndr1_1 a624 \/ c2_0 \/ c2_1 $_74 \/ c2_2 a624 $_335 \/ % 0.47/0.67 c3_2 a624 $_335 \/ c5_2 a624 $_335 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_3 a593 \/ definitionFOFtoCNF_7 \/ % 0.47/0.67 definitionFOFtoCNF_8 % 0.47/0.67 |- ~c1_1 $_341 \/ ~c2_2 a608 a603 \/ ~c3_1 $_341 \/ ~ndr1_0 \/ % 0.47/0.67 ~ndr1_1 $_341 \/ ~ndr1_1 a608 \/ c1_0 \/ c1_1 $_344 \/ c1_2 a619 a639 \/ % 0.47/0.67 c3_1 a619 \/ c4_2 $_341 $_342 \/ c4_2 a619 a639 \/ c5_1 $_344 \/ % 0.47/0.67 c5_2 $_341 $_342 \/ definitionFOFtoCNF_1 a608 \/ % 0.47/0.67 definitionFOFtoCNF_2 a608 \/ definitionFOFtoCNF_9 $_344 % 0.47/0.67 |- ~c1_1 $_341 \/ ~c2_2 a608 $_343 \/ ~c3_1 $_341 \/ ~c5_2 a608 $_343 \/ % 0.47/0.67 ~ndr1_0 \/ ~ndr1_1 a608 \/ c1_0 \/ c1_1 $_344 \/ c1_2 a619 a639 \/ % 0.47/0.67 c3_1 a619 \/ c4_2 $_341 $_342 \/ c4_2 a619 a639 \/ c5_1 $_344 \/ % 0.47/0.67 c5_2 $_341 $_342 \/ definitionFOFtoCNF_1 $_341 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_341 \/ definitionFOFtoCNF_9 $_344 % 0.47/0.67 |- ~c1_1 $_345 \/ ~c3_1 $_345 \/ ~ndr1_0 \/ ~ndr1_1 $_345 \/ % 0.47/0.67 ~ndr1_1 a608 \/ c1_1 $_348 \/ c1_1 a608 \/ c2_0 \/ c2_2 a593 a632 \/ % 0.47/0.67 c2_2 a608 a632 \/ c3_2 a593 a632 \/ c4_0 \/ c4_2 $_345 $_346 \/ % 0.47/0.67 c5_1 $_348 \/ c5_2 $_345 $_346 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_6 a593 \/ definitionFOFtoCNF_6 a608 \/ % 0.47/0.67 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ % 0.47/0.67 definitionFOFtoCNF_9 $_348 % 0.47/0.67 |- ~c1_1 $_345 \/ ~c3_1 $_345 \/ ~ndr1_0 \/ ~ndr1_1 $_345 \/ % 0.47/0.67 ~ndr1_1 a608 \/ c1_1 $_348 \/ c1_1 a608 \/ c2_0 \/ c2_2 a587 a632 \/ % 0.47/0.67 c2_2 a608 a632 \/ c3_2 a587 a632 \/ c4_0 \/ c4_2 $_345 $_346 \/ % 0.47/0.67 c5_1 $_348 \/ c5_2 $_345 $_346 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.67 definitionFOFtoCNF_6 a587 \/ definitionFOFtoCNF_6 a608 \/ % 0.47/0.67 definitionFOFtoCNF_9 $_348 % 0.47/0.67 |- ~c1_1 $_345 \/ ~c3_1 $_345 \/ ~ndr1_0 \/ ~ndr1_1 $_345 \/ % 0.47/0.67 ~ndr1_1 a608 \/ c1_1 $_348 \/ c1_1 a608 \/ c1_2 a593 a621 \/ c2_0 \/ % 0.47/0.67 c2_2 a608 a632 \/ c4_0 \/ c4_2 $_345 $_346 \/ c5_1 $_348 \/ % 0.47/0.67 c5_2 $_345 $_346 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_6 a608 \/ definitionFOFtoCNF_7 \/ % 0.47/0.67 definitionFOFtoCNF_8 \/ definitionFOFtoCNF_9 $_348 % 0.47/0.67 |- ~c1_1 $_345 \/ ~c3_1 $_345 \/ ~ndr1_0 \/ ~ndr1_1 $_345 \/ % 0.47/0.67 ~ndr1_1 a608 \/ c1_1 $_348 \/ c1_1 a608 \/ c1_2 a587 a621 \/ c2_0 \/ % 0.47/0.67 c2_2 a608 a632 \/ c4_0 \/ c4_2 $_345 $_346 \/ c5_1 $_348 \/ % 0.47/0.67 c5_2 $_345 $_346 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.67 definitionFOFtoCNF_6 a608 \/ definitionFOFtoCNF_9 $_348 % 0.47/0.67 |- ~c1_1 $_345 \/ ~c3_1 $_345 \/ ~c3_2 a608 $_347 \/ ~ndr1_0 \/ % 0.47/0.67 ~ndr1_1 a608 \/ c1_0 \/ c1_1 $_348 \/ c1_2 a619 a639 \/ % 0.47/0.67 c2_2 a608 $_347 \/ c3_1 a619 \/ c4_2 $_345 $_346 \/ c4_2 a619 a639 \/ % 0.47/0.67 c5_1 $_348 \/ c5_2 $_345 $_346 \/ definitionFOFtoCNF_1 $_345 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_345 \/ definitionFOFtoCNF_9 $_348 % 0.47/0.67 |- ~c1_1 a587 \/ ~ndr1_0 \/ c1_1 $_356 \/ c2_0 \/ c2_1 $_357 \/ c4_0 \/ % 0.47/0.67 c4_2 a587 $_355 \/ c5_1 $_356 \/ c5_2 a587 $_355 \/ % 0.47/0.67 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_9 $_356 \/ ndr1_1 a608 % 0.47/0.67 |- ~c1_1 a587 \/ ~ndr1_0 \/ c1_1 $_365 \/ c2_0 \/ c2_1 $_366 \/ c4_0 \/ % 0.47/0.67 c4_2 a587 $_364 \/ c5_1 $_365 \/ c5_2 a587 $_364 \/ c5_2 a608 a609 \/ % 0.47/0.67 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_9 $_365 % 0.47/0.67 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 $_370 \/ c1_1 a605 \/ c2_0 \/ % 0.47/0.67 c2_2 a605 a632 \/ c3_1 $_370 \/ c4_0 \/ c4_2 $_370 $_371 \/ % 0.47/0.67 c5_2 $_370 $_371 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 \/ ndr1_1 a587 % 0.47/0.67 |- ~c1_0 \/ c1_1 a605 \/ c2_0 \/ c2_2 a605 a632 \/ c3_0 \/ c3_1 a637 \/ % 0.47/0.67 c4_0 \/ c4_2 a637 $_373 \/ c5_2 a637 $_373 \/ % 0.47/0.67 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_6 a605 \/ ndr1_1 a587 % 0.47/0.67 |- ~c1_0 \/ c1_1 $_377 \/ c1_1 a605 \/ c2_0 \/ c2_2 a605 a632 \/ % 0.47/0.67 c3_1 $_377 \/ c4_0 \/ c4_2 $_377 $_378 \/ c5_2 $_377 $_378 \/ % 0.47/0.67 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_6 a605 \/ ndr1_1 a587 % 0.47/0.67 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ c1_2 a587 a621 \/ % 0.47/0.67 c2_0 \/ c2_2 a605 a632 \/ c3_0 \/ c3_1 a637 \/ c4_0 \/ % 0.47/0.67 c4_2 a637 $_382 \/ c5_2 a637 $_382 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 % 0.47/0.67 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_381 \/ c1_1 a605 \/ % 0.47/0.67 c1_2 a587 a621 \/ c2_0 \/ c2_2 a605 a632 \/ c3_1 $_381 \/ c4_0 \/ % 0.47/0.67 c4_2 $_381 $_382 \/ c5_2 $_381 $_382 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 % 0.47/0.67 |- ~c1_1 $_390 \/ ~c4_2 $_389 a603 \/ ~ndr1_0 \/ c1_0 \/ c1_2 $_390 a603 \/ % 0.47/0.67 c1_2 a619 a639 \/ c3_1 a619 \/ c4_2 $_390 a603 \/ c4_2 a619 a639 \/ % 0.47/0.67 definitionFOFtoCNF_1 $_389 \/ definitionFOFtoCNF_1 $_390 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_389 \/ definitionFOFtoCNF_2 $_390 % 0.47/0.67 |- ~c1_1 a587 \/ ~ndr1_0 \/ c1_1 $_397 \/ c1_1 $_398 \/ c2_0 \/ c4_0 \/ % 0.47/0.67 c4_2 a587 $_396 \/ c5_1 $_397 \/ c5_2 a587 $_396 \/ % 0.47/0.67 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_9 $_397 \/ % 0.47/0.67 ndr1_1 $_398 \/ ndr1_1 a608 % 0.47/0.67 |- ~c1_1 a587 \/ ~ndr1_0 \/ c1_1 $_412 \/ c1_1 $_413 \/ c2_0 \/ c4_0 \/ % 0.47/0.67 c4_2 a587 $_411 \/ c5_1 $_412 \/ c5_2 a587 $_411 \/ c5_2 a608 a609 \/ % 0.47/0.67 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_9 $_412 \/ ndr1_1 $_413 % 0.47/0.67 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 $_429 \/ c1_1 a605 \/ c2_0 \/ % 0.47/0.67 c2_2 a605 a632 \/ c3_1 $_429 \/ c4_0 \/ c4_2 $_429 $_430 \/ % 0.47/0.67 c5_2 $_429 $_430 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 \/ definitionFOFtoCNF_7 \/ % 0.47/0.67 definitionFOFtoCNF_8 \/ ndr1_1 a593 % 0.47/0.67 |- ~c1_0 \/ c1_1 a605 \/ c2_0 \/ c2_2 a605 a632 \/ c3_0 \/ c3_1 a637 \/ % 0.47/0.67 c4_0 \/ c4_2 a637 $_432 \/ c5_2 a637 $_432 \/ % 0.47/0.67 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_6 a605 \/ % 0.47/0.67 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 a593 % 0.47/0.67 |- ~c1_0 \/ c1_1 $_436 \/ c1_1 a605 \/ c2_0 \/ c2_2 a605 a632 \/ % 0.47/0.67 c3_1 $_436 \/ c4_0 \/ c4_2 $_436 $_437 \/ c5_2 $_436 $_437 \/ % 0.47/0.67 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_6 a605 \/ % 0.47/0.67 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ ndr1_1 a593 % 0.47/0.67 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ c1_2 a593 a621 \/ % 0.47/0.67 c2_0 \/ c2_2 a605 a632 \/ c3_0 \/ c3_1 a637 \/ c4_0 \/ % 0.47/0.67 c4_2 a637 $_449 \/ c5_2 a637 $_449 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 \/ definitionFOFtoCNF_7 \/ % 0.47/0.67 definitionFOFtoCNF_8 % 0.47/0.67 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_448 \/ c1_1 a605 \/ % 0.47/0.67 c1_2 a593 a621 \/ c2_0 \/ c2_2 a605 a632 \/ c3_1 $_448 \/ c4_0 \/ % 0.47/0.67 c4_2 $_448 $_449 \/ c5_2 $_448 $_449 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 \/ definitionFOFtoCNF_7 \/ % 0.47/0.67 definitionFOFtoCNF_8 % 0.47/0.67 |- ~c1_2 $_466 a603 \/ ~c3_1 $_466 \/ ~ndr1_0 \/ ~ndr1_1 $_466 \/ % 0.47/0.67 ~ndr1_1 a624 \/ c1_0 \/ c1_2 a619 a639 \/ c2_0 \/ c2_2 a624 $_465 \/ % 0.47/0.67 c3_1 a619 \/ c3_2 a624 $_465 \/ c4_2 a619 a639 \/ c5_2 a624 $_465 \/ % 0.47/0.67 definitionFOFtoCNF_1 $_466 \/ definitionFOFtoCNF_2 $_466 \/ % 0.47/0.67 definitionFOFtoCNF_3 $_466 % 0.47/0.67 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ c2_0 \/ % 0.47/0.67 c2_2 a587 a632 \/ c2_2 a605 a632 \/ c3_0 \/ c3_1 a637 \/ % 0.47/0.67 c3_2 a587 a632 \/ c4_0 \/ c4_2 a637 $_470 \/ c5_2 a637 $_470 \/ % 0.47/0.67 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_6 a587 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 % 0.47/0.67 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_469 \/ c1_1 a605 \/ c2_0 \/ % 0.47/0.67 c2_2 a587 a632 \/ c2_2 a605 a632 \/ c3_1 $_469 \/ c3_2 a587 a632 \/ % 0.47/0.67 c4_0 \/ c4_2 $_469 $_470 \/ c5_2 $_469 $_470 \/ % 0.47/0.67 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_6 a587 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 % 0.47/0.67 |- ~c1_1 a587 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_474 \/ c1_2 a619 a639 \/ % 0.47/0.67 c3_1 a619 \/ c4_0 \/ c4_2 a587 $_473 \/ c4_2 a619 a639 \/ c5_1 $_474 \/ % 0.47/0.67 c5_2 a587 $_473 \/ definitionFOFtoCNF_1 a587 \/ % 0.47/0.67 definitionFOFtoCNF_2 a587 \/ definitionFOFtoCNF_9 $_474 \/ ndr1_1 a608 % 0.47/0.67 |- ~c1_1 a587 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_482 \/ c1_2 a619 a639 \/ % 0.47/0.67 c3_1 a619 \/ c4_0 \/ c4_2 a587 $_481 \/ c4_2 a619 a639 \/ c5_1 $_482 \/ % 0.47/0.67 c5_2 a587 $_481 \/ c5_2 a608 a609 \/ definitionFOFtoCNF_1 a587 \/ % 0.47/0.67 definitionFOFtoCNF_2 a587 \/ definitionFOFtoCNF_9 $_482 % 0.47/0.67 |- ~c1_1 $_502 \/ ~c2_2 a608 a603 \/ ~c3_1 $_502 \/ ~ndr1_0 \/ % 0.47/0.67 ~ndr1_1 a608 \/ c1_0 \/ c1_1 $_504 \/ c1_2 a619 a639 \/ c3_1 a619 \/ % 0.47/0.67 c4_2 $_502 $_503 \/ c4_2 a619 a639 \/ c5_1 $_504 \/ c5_2 $_502 $_503 \/ % 0.47/0.67 definitionFOFtoCNF_1 $_502 \/ definitionFOFtoCNF_1 a608 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_502 \/ definitionFOFtoCNF_2 a608 \/ % 0.47/0.67 definitionFOFtoCNF_9 $_504 % 0.47/0.67 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 a605 \/ c2_0 \/ % 0.47/0.67 c2_2 a593 a632 \/ c2_2 a605 a632 \/ c3_0 \/ c3_1 a637 \/ % 0.47/0.67 c3_2 a593 a632 \/ c4_0 \/ c4_2 a637 $_508 \/ c5_2 a637 $_508 \/ % 0.47/0.67 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_6 a593 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 \/ definitionFOFtoCNF_7 \/ % 0.47/0.67 definitionFOFtoCNF_8 % 0.47/0.67 |- ~c1_0 \/ ~ndr1_0 \/ ~ndr1_1 a605 \/ c1_1 $_507 \/ c1_1 a605 \/ c2_0 \/ % 0.47/0.67 c2_2 a593 a632 \/ c2_2 a605 a632 \/ c3_1 $_507 \/ c3_2 a593 a632 \/ % 0.47/0.67 c4_0 \/ c4_2 $_507 $_508 \/ c5_2 $_507 $_508 \/ % 0.47/0.67 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_6 a593 \/ % 0.47/0.67 definitionFOFtoCNF_6 a605 \/ definitionFOFtoCNF_7 \/ % 0.47/0.67 definitionFOFtoCNF_8 % 0.47/0.67 |- ~c1_1 $_527 \/ ~c3_1 $_527 \/ ~ndr1_0 \/ ~ndr1_1 $_527 \/ c1_1 $_529 \/ % 0.47/0.67 c1_1 a608 \/ c2_0 \/ c2_2 a608 a632 \/ c4_0 \/ c4_2 $_527 $_528 \/ % 0.47/0.67 c5_1 $_529 \/ c5_2 $_527 $_528 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.67 definitionFOFtoCNF_6 a608 \/ definitionFOFtoCNF_9 $_529 \/ ndr1_1 a587 % 0.47/0.67 |- ~c1_1 $_530 \/ ~c3_1 $_530 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_532 \/ % 0.47/0.67 c1_1 a608 \/ c1_2 a619 a639 \/ c2_0 \/ c2_2 a608 a632 \/ c3_1 a619 \/ % 0.47/0.67 c4_0 \/ c4_2 $_530 $_531 \/ c4_2 a619 a639 \/ c5_1 $_532 \/ % 0.47/0.67 c5_2 $_530 $_531 \/ definitionFOFtoCNF_1 $_530 \/ % 0.47/0.67 definitionFOFtoCNF_10 a587 \/ definitionFOFtoCNF_2 $_530 \/ % 0.47/0.67 definitionFOFtoCNF_6 a608 \/ definitionFOFtoCNF_9 $_532 \/ ndr1_1 a587 % 0.47/0.67 |- ~c1_1 $_536 \/ ~c3_1 $_536 \/ ~ndr1_0 \/ ~ndr1_1 a608 \/ c1_0 \/ % 0.47/0.67 c1_1 $_538 \/ c1_1 a608 \/ c1_2 a587 a621 \/ c1_2 a619 a639 \/ c2_0 \/ % 0.47/0.67 c2_2 a608 a632 \/ c3_1 a619 \/ c4_0 \/ c4_2 $_536 $_537 \/ % 0.47/0.67 c4_2 a619 a639 \/ c5_1 $_538 \/ c5_2 $_536 $_537 \/ % 0.47/0.67 definitionFOFtoCNF_1 $_536 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_536 \/ definitionFOFtoCNF_6 a608 \/ % 0.47/0.67 definitionFOFtoCNF_9 $_538 % 0.47/0.67 |- ~c1_1 $_546 \/ ~c3_1 $_546 \/ ~ndr1_0 \/ ~ndr1_1 $_546 \/ c1_1 $_548 \/ % 0.47/0.67 c1_1 a608 \/ c2_0 \/ c2_2 a608 a632 \/ c4_0 \/ c4_2 $_546 $_547 \/ % 0.47/0.67 c5_1 $_548 \/ c5_2 $_546 $_547 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_6 a608 \/ definitionFOFtoCNF_7 \/ % 0.47/0.67 definitionFOFtoCNF_8 \/ definitionFOFtoCNF_9 $_548 \/ ndr1_1 a593 % 0.47/0.67 |- ~c1_1 $_549 \/ ~c3_1 $_549 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_551 \/ % 0.47/0.67 c1_1 a608 \/ c1_2 a619 a639 \/ c2_0 \/ c2_2 a608 a632 \/ c3_1 a619 \/ % 0.47/0.67 c4_0 \/ c4_2 $_549 $_550 \/ c4_2 a619 a639 \/ c5_1 $_551 \/ % 0.47/0.67 c5_2 $_549 $_550 \/ definitionFOFtoCNF_1 $_549 \/ % 0.47/0.67 definitionFOFtoCNF_10 a593 \/ definitionFOFtoCNF_2 $_549 \/ % 0.47/0.67 definitionFOFtoCNF_6 a608 \/ definitionFOFtoCNF_7 \/ % 0.47/0.67 definitionFOFtoCNF_8 \/ definitionFOFtoCNF_9 $_551 \/ ndr1_1 a593 % 0.47/0.67 |- ~c1_1 $_555 \/ ~c3_1 $_555 \/ ~ndr1_0 \/ ~ndr1_1 a608 \/ c1_0 \/ % 0.47/0.67 c1_1 $_557 \/ c1_1 a608 \/ c1_2 a593 a621 \/ c1_2 a619 a639 \/ c2_0 \/ % 0.47/0.67 c2_2 a608 a632 \/ c3_1 a619 \/ c4_0 \/ c4_2 $_555 $_556 \/ % 0.47/0.67 c4_2 a619 a639 \/ c5_1 $_557 \/ c5_2 $_555 $_556 \/ % 0.47/0.67 definitionFOFtoCNF_1 $_555 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_555 \/ definitionFOFtoCNF_6 a608 \/ % 0.47/0.67 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ % 0.47/0.67 definitionFOFtoCNF_9 $_557 % 0.47/0.67 |- ~c1_1 $_558 \/ ~c3_1 $_558 \/ ~ndr1_0 \/ ~ndr1_1 a608 \/ c1_0 \/ % 0.47/0.67 c1_1 $_560 \/ c1_1 a608 \/ c1_2 a619 a639 \/ c2_0 \/ c2_2 a587 a632 \/ % 0.47/0.67 c2_2 a608 a632 \/ c3_1 a619 \/ c3_2 a587 a632 \/ c4_0 \/ % 0.47/0.67 c4_2 $_558 $_559 \/ c4_2 a619 a639 \/ c5_1 $_560 \/ c5_2 $_558 $_559 \/ % 0.47/0.67 definitionFOFtoCNF_1 $_558 \/ definitionFOFtoCNF_10 a587 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_558 \/ definitionFOFtoCNF_6 a587 \/ % 0.47/0.67 definitionFOFtoCNF_6 a608 \/ definitionFOFtoCNF_9 $_560 % 0.47/0.67 |- ~c1_1 $_565 \/ ~c3_1 $_565 \/ ~ndr1_0 \/ ~ndr1_1 a608 \/ c1_0 \/ % 0.47/0.67 c1_1 $_567 \/ c1_1 a608 \/ c1_2 a619 a639 \/ c2_0 \/ c2_2 a593 a632 \/ % 0.47/0.67 c2_2 a608 a632 \/ c3_1 a619 \/ c3_2 a593 a632 \/ c4_0 \/ % 0.47/0.67 c4_2 $_565 $_566 \/ c4_2 a619 a639 \/ c5_1 $_567 \/ c5_2 $_565 $_566 \/ % 0.47/0.67 definitionFOFtoCNF_1 $_565 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_2 $_565 \/ definitionFOFtoCNF_6 a593 \/ % 0.47/0.67 definitionFOFtoCNF_6 a608 \/ definitionFOFtoCNF_7 \/ % 0.47/0.67 definitionFOFtoCNF_8 \/ definitionFOFtoCNF_9 $_567 % 0.47/0.67 |- ~c1_1 a587 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_576 \/ c1_1 a608 \/ % 0.47/0.67 c1_2 a619 a639 \/ c2_0 \/ c2_2 a608 a632 \/ c3_1 a619 \/ c4_0 \/ % 0.47/0.67 c4_2 a587 $_575 \/ c4_2 a619 a639 \/ c5_1 $_576 \/ c5_2 a587 $_575 \/ % 0.47/0.67 definitionFOFtoCNF_1 a587 \/ definitionFOFtoCNF_10 a593 \/ % 0.47/0.67 definitionFOFtoCNF_2 a587 \/ definitionFOFtoCNF_6 a608 \/ % 0.47/0.67 definitionFOFtoCNF_7 \/ definitionFOFtoCNF_8 \/ % 0.47/0.67 definitionFOFtoCNF_9 $_576 \/ ndr1_1 a593 % 0.47/0.67 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.47/0.67 %------------------------------------------------------------------------------