%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN348+1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n004.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:01:37 EDT 2022 % Result : CounterSatisfiable 0.61s 0.82s % Output : Saturation 0.61s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYN348+1 : TPTP v8.1.0. Released v2.0.0. % 0.10/0.12 % Command : metis --show proof --show saturation %s % 0.13/0.33 % Computer : n004.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 07:44:37 EDT 2022 % 0.13/0.33 % CPUTime : % 0.13/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.61/0.82 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.61/0.82 % 0.61/0.82 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.61/0.82 |- ~big_f $X1 $X4 \/ ~big_f $X3 $X4 \/ ~definitionFOFtoCNF_1 $X1 $X3 $X4 % 0.61/0.82 |- ~big_f $X1 $X4 \/ big_f $X3 $X4 \/ definitionFOFtoCNF_1 $X1 $X3 $X4 % 0.61/0.82 |- ~big_f $X3 $X4 \/ big_f $X1 $X4 \/ definitionFOFtoCNF_1 $X1 $X3 $X4 % 0.61/0.82 |- ~definitionFOFtoCNF_1 $X1 $X3 $X4 \/ big_f $X1 $X4 \/ big_f $X3 $X4 % 0.61/0.82 |- ~big_f $X4 $X1 \/ ~big_f $X4 $X3 \/ ~definitionFOFtoCNF_0 $X1 $X3 $X4 \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 $X3 $X4 % 0.61/0.82 |- ~big_f $X4 $X1 \/ ~big_f $X4 $X3 \/ ~definitionFOFtoCNF_1 $X1 $X3 $X4 \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 $X3 $X4 % 0.61/0.82 |- ~big_f $X4 $X1 \/ ~definitionFOFtoCNF_0 $X1 $X3 $X4 \/ % 0.61/0.82 ~definitionFOFtoCNF_1 $X1 $X3 $X4 \/ big_f $X4 $X3 % 0.61/0.82 |- ~big_f $X4 $X1 \/ big_f $X4 $X3 \/ definitionFOFtoCNF_0 $X1 $X3 $X4 \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 $X3 $X4 % 0.61/0.82 |- ~big_f $X4 $X3 \/ ~definitionFOFtoCNF_0 $X1 $X3 $X4 \/ % 0.61/0.82 ~definitionFOFtoCNF_1 $X1 $X3 $X4 \/ big_f $X4 $X1 % 0.61/0.82 |- ~big_f $X4 $X3 \/ big_f $X4 $X1 \/ definitionFOFtoCNF_0 $X1 $X3 $X4 \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 $X3 $X4 % 0.61/0.82 |- ~definitionFOFtoCNF_0 $X1 $X3 $X4 \/ big_f $X4 $X1 \/ big_f $X4 $X3 \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 $X3 $X4 % 0.61/0.82 |- ~definitionFOFtoCNF_1 $X1 $X3 $X4 \/ big_f $X4 $X1 \/ big_f $X4 $X3 \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 $X3 $X4 % 0.61/0.82 |- ~big_f $X3 (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 ~big_f (skolemFOFtoCNF_X2 $X1) (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 ~big_f (skolemFOFtoCNF_X4_1 $X1 $X3) $X3 \/ % 0.61/0.82 ~big_f (skolemFOFtoCNF_X4_1 $X1 $X3) (skolemFOFtoCNF_X2 $X1) \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 $X3 (skolemFOFtoCNF_X4 $X1 $X3) % 0.61/0.82 |- ~big_f $X3 (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 ~big_f (skolemFOFtoCNF_X2 $X1) (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $X1 $X3) $X3 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $X1 $X3) (skolemFOFtoCNF_X2 $X1) \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 $X3 (skolemFOFtoCNF_X4 $X1 $X3) % 0.61/0.82 |- ~big_f $X3 (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 ~big_f (skolemFOFtoCNF_X4_1 $X1 $X3) $X3 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $X1) (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $X1 $X3) (skolemFOFtoCNF_X2 $X1) \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 $X3 (skolemFOFtoCNF_X4 $X1 $X3) % 0.61/0.82 |- ~big_f $X3 (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 ~big_f (skolemFOFtoCNF_X4_1 $X1 $X3) (skolemFOFtoCNF_X2 $X1) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $X1) (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $X1 $X3) $X3 \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 $X3 (skolemFOFtoCNF_X4 $X1 $X3) % 0.61/0.82 |- ~big_f (skolemFOFtoCNF_X2 $X1) (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 ~big_f (skolemFOFtoCNF_X4_1 $X1 $X3) $X3 \/ % 0.61/0.82 big_f $X3 (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $X1 $X3) (skolemFOFtoCNF_X2 $X1) \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 $X3 (skolemFOFtoCNF_X4 $X1 $X3) % 0.61/0.82 |- ~big_f (skolemFOFtoCNF_X2 $X1) (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 ~big_f (skolemFOFtoCNF_X4_1 $X1 $X3) (skolemFOFtoCNF_X2 $X1) \/ % 0.61/0.82 big_f $X3 (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $X1 $X3) $X3 \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 $X3 (skolemFOFtoCNF_X4 $X1 $X3) % 0.61/0.82 |- ~big_f (skolemFOFtoCNF_X4_1 $X1 $X3) $X3 \/ % 0.61/0.82 ~big_f (skolemFOFtoCNF_X4_1 $X1 $X3) (skolemFOFtoCNF_X2 $X1) \/ % 0.61/0.82 big_f $X3 (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $X1) (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 $X3 (skolemFOFtoCNF_X4 $X1 $X3) % 0.61/0.82 |- big_f $X3 (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $X1) (skolemFOFtoCNF_X4_1 $X1 $X3) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $X1 $X3) $X3 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $X1 $X3) (skolemFOFtoCNF_X2 $X1) \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 $X3 (skolemFOFtoCNF_X4 $X1 $X3) % 0.61/0.82 |- ~big_f (skolemFOFtoCNF_X2 $X1) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $X1 (skolemFOFtoCNF_X2 $X1)) \/ % 0.61/0.82 ~big_f (skolemFOFtoCNF_X4_1 $X1 (skolemFOFtoCNF_X2 $X1)) % 0.61/0.82 (skolemFOFtoCNF_X2 $X1) \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 (skolemFOFtoCNF_X2 $X1) % 0.61/0.82 (skolemFOFtoCNF_X4 $X1 (skolemFOFtoCNF_X2 $X1)) % 0.61/0.82 |- ~big_f (skolemFOFtoCNF_X2 $X1) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $X1 (skolemFOFtoCNF_X2 $X1)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $X1 (skolemFOFtoCNF_X2 $X1)) % 0.61/0.82 (skolemFOFtoCNF_X2 $X1) \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 (skolemFOFtoCNF_X2 $X1) % 0.61/0.82 (skolemFOFtoCNF_X4 $X1 (skolemFOFtoCNF_X2 $X1)) % 0.61/0.82 |- ~big_f (skolemFOFtoCNF_X4_1 $X1 (skolemFOFtoCNF_X2 $X1)) % 0.61/0.82 (skolemFOFtoCNF_X2 $X1) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $X1) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $X1 (skolemFOFtoCNF_X2 $X1)) \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 (skolemFOFtoCNF_X2 $X1) % 0.61/0.82 (skolemFOFtoCNF_X4 $X1 (skolemFOFtoCNF_X2 $X1)) % 0.61/0.82 |- big_f $_54 (skolemFOFtoCNF_X4_1 $_53 $_54) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_53) (skolemFOFtoCNF_X4_1 $_53 $_54) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_53 $_54) $_53 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_53 $_54) $_54 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_53 $_54) $_54 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_53 $_54) (skolemFOFtoCNF_X2 $_53) \/ % 0.61/0.82 definitionFOFtoCNF_1 $_53 $_54 (skolemFOFtoCNF_X4 $_53 $_54) % 0.61/0.82 |- ~big_f (skolemFOFtoCNF_X4 $_53 $_54) $_53 \/ % 0.61/0.82 ~big_f (skolemFOFtoCNF_X4 $_53 $_54) $_54 \/ % 0.61/0.82 big_f $_54 (skolemFOFtoCNF_X4_1 $_53 $_54) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_53) (skolemFOFtoCNF_X4_1 $_53 $_54) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_53 $_54) $_54 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_53 $_54) (skolemFOFtoCNF_X2 $_53) \/ % 0.61/0.82 definitionFOFtoCNF_1 $_53 $_54 (skolemFOFtoCNF_X4 $_53 $_54) % 0.61/0.82 |- ~big_f (skolemFOFtoCNF_X4 $_54 $_54) $_54 \/ % 0.61/0.82 big_f $_54 (skolemFOFtoCNF_X4_1 $_54 $_54) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_54) (skolemFOFtoCNF_X4_1 $_54 $_54) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_54 $_54) $_54 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_54 $_54) (skolemFOFtoCNF_X2 $_54) \/ % 0.61/0.82 definitionFOFtoCNF_1 $_54 $_54 (skolemFOFtoCNF_X4 $_54 $_54) % 0.61/0.82 |- big_f $_56 (skolemFOFtoCNF_X4 $_56 $_57) \/ % 0.61/0.82 big_f $_57 (skolemFOFtoCNF_X4 $_56 $_57) \/ % 0.61/0.82 big_f $_57 (skolemFOFtoCNF_X4_1 $_56 $_57) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_56) (skolemFOFtoCNF_X4_1 $_56 $_57) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_56 $_57) $_56 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_56 $_57) $_57 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_56 $_57) $_57 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_56 $_57) (skolemFOFtoCNF_X2 $_56) % 0.61/0.82 |- ~big_f $_56 (skolemFOFtoCNF_X4 $_56 $_57) \/ % 0.61/0.82 ~big_f $_57 (skolemFOFtoCNF_X4 $_56 $_57) \/ % 0.61/0.82 big_f $_57 (skolemFOFtoCNF_X4_1 $_56 $_57) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_56) (skolemFOFtoCNF_X4_1 $_56 $_57) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_56 $_57) $_56 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_56 $_57) $_57 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_56 $_57) $_57 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_56 $_57) (skolemFOFtoCNF_X2 $_56) % 0.61/0.82 |- ~big_f $_57 (skolemFOFtoCNF_X4 $_57 $_57) \/ % 0.61/0.82 big_f $_57 (skolemFOFtoCNF_X4_1 $_57 $_57) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_57) (skolemFOFtoCNF_X4_1 $_57 $_57) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_57 $_57) $_57 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_57 $_57) $_57 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_57 $_57) (skolemFOFtoCNF_X2 $_57) % 0.61/0.82 |- big_f $_63 (skolemFOFtoCNF_X4 $_63 (skolemFOFtoCNF_X2 $_63)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_63) % 0.61/0.82 (skolemFOFtoCNF_X4 $_63 (skolemFOFtoCNF_X2 $_63)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_63) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_63 (skolemFOFtoCNF_X2 $_63)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_63 (skolemFOFtoCNF_X2 $_63)) $_63 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_63 (skolemFOFtoCNF_X2 $_63)) % 0.61/0.82 (skolemFOFtoCNF_X2 $_63) % 0.61/0.82 |- big_f $_64 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) $X1 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) $_64 \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) % 0.61/0.82 |- big_f $_64 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) $X3 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) $_64 \/ % 0.61/0.82 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_64) $X3 % 0.61/0.82 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_64) $X3 % 0.61/0.82 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) % 0.61/0.82 |- big_f $X1 (skolemFOFtoCNF_X2 $_64) \/ % 0.61/0.82 big_f $_64 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) $_64 \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 % 0.61/0.82 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) % 0.61/0.82 (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 |- big_f $X3 (skolemFOFtoCNF_X2 $_64) \/ % 0.61/0.82 big_f $_64 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_64 (skolemFOFtoCNF_X2 $_64)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) $_64 \/ % 0.61/0.82 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4 $_64 (skolemFOFtoCNF_X2 $_64)) % 0.61/0.82 $X3 (skolemFOFtoCNF_X2 $_64) % 0.61/0.82 |- big_f $_65 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_65) (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_65 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_66 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) $X1 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) (skolemFOFtoCNF_X2 $_65) \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 $_66 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 $_66 (skolemFOFtoCNF_X4_1 $_65 $_66) % 0.61/0.82 |- big_f $_65 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_65) (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_65 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_66 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) $X3 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) (skolemFOFtoCNF_X2 $_65) \/ % 0.61/0.82 definitionFOFtoCNF_0 $_66 $X3 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 definitionFOFtoCNF_1 $_66 $X3 (skolemFOFtoCNF_X4_1 $_65 $_66) % 0.61/0.82 |- big_f $X1 $_66 \/ big_f $_65 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_65) (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_65 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_66 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) (skolemFOFtoCNF_X2 $_65) \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X4_1 $_65 $_66) $_66 % 0.61/0.82 |- big_f $X3 $_66 \/ big_f $_65 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_65) (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_65 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_66 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) (skolemFOFtoCNF_X2 $_65) \/ % 0.61/0.82 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_65 $_66) $X3 $_66 % 0.61/0.82 |- big_f $_65 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_65) (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_65 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_66 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) $X1 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) $_66 \/ % 0.61/0.82 definitionFOFtoCNF_0 $X1 (skolemFOFtoCNF_X2 $_65) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X2 $_65) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_65 $_66) % 0.61/0.82 |- big_f $_65 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_65) (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_65 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_66 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) $X3 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) $_66 \/ % 0.61/0.82 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_65) $X3 % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_65) $X3 % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_65 $_66) % 0.61/0.82 |- big_f $X1 (skolemFOFtoCNF_X2 $_65) \/ % 0.61/0.82 big_f $_65 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_65) (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_65 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_66 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) $_66 \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X4_1 $_65 $_66) % 0.61/0.82 (skolemFOFtoCNF_X2 $_65) % 0.61/0.82 |- big_f $X3 (skolemFOFtoCNF_X2 $_65) \/ % 0.61/0.82 big_f $_65 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4 $_65 $_66) \/ % 0.61/0.82 big_f $_66 (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_65) (skolemFOFtoCNF_X4_1 $_65 $_66) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_65 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_65 $_66) $_66 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_65 $_66) $_66 \/ % 0.61/0.82 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_65 $_66) $X3 % 0.61/0.82 (skolemFOFtoCNF_X2 $_65) % 0.61/0.82 |- big_f $_69 (skolemFOFtoCNF_X2 $_70) \/ % 0.61/0.82 big_f $_70 (skolemFOFtoCNF_X4 $_70 (skolemFOFtoCNF_X2 $_70)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_70) $_69 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_70) % 0.61/0.82 (skolemFOFtoCNF_X4 $_70 (skolemFOFtoCNF_X2 $_70)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_70) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_70 (skolemFOFtoCNF_X2 $_70)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_70 (skolemFOFtoCNF_X2 $_70)) $_70 \/ % 0.61/0.82 definitionFOFtoCNF_0 $_69 % 0.61/0.82 (skolemFOFtoCNF_X4 $_70 (skolemFOFtoCNF_X2 $_70)) % 0.61/0.82 (skolemFOFtoCNF_X2 $_70) % 0.61/0.82 |- ~big_f (skolemFOFtoCNF_X2 $_70) $_69 \/ % 0.61/0.82 ~definitionFOFtoCNF_0 $_69 % 0.61/0.82 (skolemFOFtoCNF_X4 $_70 (skolemFOFtoCNF_X2 $_70)) % 0.61/0.82 (skolemFOFtoCNF_X2 $_70) \/ big_f $_69 (skolemFOFtoCNF_X2 $_70) \/ % 0.61/0.82 big_f $_70 (skolemFOFtoCNF_X4 $_70 (skolemFOFtoCNF_X2 $_70)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_70) % 0.61/0.82 (skolemFOFtoCNF_X4 $_70 (skolemFOFtoCNF_X2 $_70)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_70) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_70 (skolemFOFtoCNF_X2 $_70)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_70 (skolemFOFtoCNF_X2 $_70)) $_70 % 0.61/0.82 |- big_f $_71 (skolemFOFtoCNF_X2 $_72) \/ % 0.61/0.82 big_f $_72 (skolemFOFtoCNF_X4 $_72 (skolemFOFtoCNF_X2 $_72)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_72) $_71 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_72) % 0.61/0.82 (skolemFOFtoCNF_X4 $_72 (skolemFOFtoCNF_X2 $_72)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_72) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_72 (skolemFOFtoCNF_X2 $_72)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_72 (skolemFOFtoCNF_X2 $_72)) $_72 \/ % 0.61/0.82 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4 $_72 (skolemFOFtoCNF_X2 $_72)) % 0.61/0.82 $_71 (skolemFOFtoCNF_X2 $_72) % 0.61/0.82 |- ~big_f (skolemFOFtoCNF_X2 $_72) $_71 \/ % 0.61/0.82 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4 $_72 (skolemFOFtoCNF_X2 $_72)) % 0.61/0.82 $_71 (skolemFOFtoCNF_X2 $_72) \/ % 0.61/0.82 big_f $_71 (skolemFOFtoCNF_X2 $_72) \/ % 0.61/0.82 big_f $_72 (skolemFOFtoCNF_X4 $_72 (skolemFOFtoCNF_X2 $_72)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_72) % 0.61/0.82 (skolemFOFtoCNF_X4 $_72 (skolemFOFtoCNF_X2 $_72)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_72) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_72 (skolemFOFtoCNF_X2 $_72)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_72 (skolemFOFtoCNF_X2 $_72)) $_72 % 0.61/0.82 |- big_f $_81 (skolemFOFtoCNF_X4 $_82 (skolemFOFtoCNF_X2 $_82)) \/ % 0.61/0.82 big_f $_82 (skolemFOFtoCNF_X4 $_82 (skolemFOFtoCNF_X2 $_82)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_82) % 0.61/0.82 (skolemFOFtoCNF_X4 $_82 (skolemFOFtoCNF_X2 $_82)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_82) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_82 (skolemFOFtoCNF_X2 $_82)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_82 (skolemFOFtoCNF_X2 $_82)) $_81 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_82 (skolemFOFtoCNF_X2 $_82)) $_82 \/ % 0.61/0.82 definitionFOFtoCNF_0 $_81 (skolemFOFtoCNF_X2 $_82) % 0.61/0.82 (skolemFOFtoCNF_X4 $_82 (skolemFOFtoCNF_X2 $_82)) % 0.61/0.82 |- big_f $_85 (skolemFOFtoCNF_X4 $_86 (skolemFOFtoCNF_X2 $_86)) \/ % 0.61/0.82 big_f $_86 (skolemFOFtoCNF_X4 $_86 (skolemFOFtoCNF_X2 $_86)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_86) % 0.61/0.82 (skolemFOFtoCNF_X4 $_86 (skolemFOFtoCNF_X2 $_86)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_86) % 0.61/0.82 (skolemFOFtoCNF_X4_1 $_86 (skolemFOFtoCNF_X2 $_86)) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_86 (skolemFOFtoCNF_X2 $_86)) $_85 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_86 (skolemFOFtoCNF_X2 $_86)) $_86 \/ % 0.61/0.82 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_86) $_85 % 0.61/0.82 (skolemFOFtoCNF_X4 $_86 (skolemFOFtoCNF_X2 $_86)) % 0.61/0.82 |- big_f $X1 (skolemFOFtoCNF_X2 $_90) \/ big_f $_89 $_91 \/ % 0.61/0.82 big_f $_90 (skolemFOFtoCNF_X4 $_90 $_91) \/ % 0.61/0.82 big_f $_91 (skolemFOFtoCNF_X4 $_90 $_91) \/ % 0.61/0.82 big_f $_91 (skolemFOFtoCNF_X4_1 $_90 $_91) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_90) (skolemFOFtoCNF_X4_1 $_90 $_91) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_90 $_91) $_90 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_90 $_91) $_91 \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X4_1 $_90 $_91) % 0.61/0.82 (skolemFOFtoCNF_X2 $_90) \/ % 0.61/0.82 definitionFOFtoCNF_1 $_89 (skolemFOFtoCNF_X4_1 $_90 $_91) $_91 % 0.61/0.82 |- big_f $X3 (skolemFOFtoCNF_X2 $_90) \/ big_f $_89 $_91 \/ % 0.61/0.82 big_f $_90 (skolemFOFtoCNF_X4 $_90 $_91) \/ % 0.61/0.82 big_f $_91 (skolemFOFtoCNF_X4 $_90 $_91) \/ % 0.61/0.82 big_f $_91 (skolemFOFtoCNF_X4_1 $_90 $_91) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_90) (skolemFOFtoCNF_X4_1 $_90 $_91) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_90 $_91) $_90 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_90 $_91) $_91 \/ % 0.61/0.82 definitionFOFtoCNF_1 $_89 (skolemFOFtoCNF_X4_1 $_90 $_91) $_91 \/ % 0.61/0.82 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_90 $_91) $X3 % 0.61/0.82 (skolemFOFtoCNF_X2 $_90) % 0.61/0.82 |- big_f $_89 $_91 \/ big_f $_90 (skolemFOFtoCNF_X4 $_90 $_91) \/ % 0.61/0.82 big_f $_91 $_89 \/ big_f $_91 (skolemFOFtoCNF_X4 $_90 $_91) \/ % 0.61/0.82 big_f $_91 (skolemFOFtoCNF_X4_1 $_90 $_91) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_90) (skolemFOFtoCNF_X4_1 $_90 $_91) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_90 $_91) $_90 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_90 $_91) $_91 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_90 $_91) (skolemFOFtoCNF_X2 $_90) \/ % 0.61/0.82 definitionFOFtoCNF_0 $_89 (skolemFOFtoCNF_X4_1 $_90 $_91) $_91 % 0.61/0.82 |- ~big_f $_91 $_89 \/ % 0.61/0.82 ~definitionFOFtoCNF_0 $_89 (skolemFOFtoCNF_X4_1 $_90 $_91) $_91 \/ % 0.61/0.82 big_f $_89 $_91 \/ big_f $_90 (skolemFOFtoCNF_X4 $_90 $_91) \/ % 0.61/0.82 big_f $_91 (skolemFOFtoCNF_X4 $_90 $_91) \/ % 0.61/0.82 big_f $_91 (skolemFOFtoCNF_X4_1 $_90 $_91) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_90) (skolemFOFtoCNF_X4_1 $_90 $_91) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_90 $_91) $_90 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_90 $_91) $_91 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4_1 $_90 $_91) (skolemFOFtoCNF_X2 $_90) % 0.61/0.82 |- big_f $X1 (skolemFOFtoCNF_X2 $_93) \/ big_f $_92 $_94 \/ % 0.61/0.82 big_f $_93 (skolemFOFtoCNF_X4 $_93 $_94) \/ % 0.61/0.82 big_f $_94 (skolemFOFtoCNF_X4 $_93 $_94) \/ % 0.61/0.82 big_f $_94 (skolemFOFtoCNF_X4_1 $_93 $_94) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_93) (skolemFOFtoCNF_X4_1 $_93 $_94) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_93 $_94) $_93 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_93 $_94) $_94 \/ % 0.61/0.82 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X4_1 $_93 $_94) % 0.61/0.82 (skolemFOFtoCNF_X2 $_93) \/ % 0.61/0.82 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_93 $_94) $_92 $_94 % 0.61/0.82 |- big_f $X3 (skolemFOFtoCNF_X2 $_93) \/ big_f $_92 $_94 \/ % 0.61/0.82 big_f $_93 (skolemFOFtoCNF_X4 $_93 $_94) \/ % 0.61/0.82 big_f $_94 (skolemFOFtoCNF_X4 $_93 $_94) \/ % 0.61/0.82 big_f $_94 (skolemFOFtoCNF_X4_1 $_93 $_94) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X2 $_93) (skolemFOFtoCNF_X4_1 $_93 $_94) \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_93 $_94) $_93 \/ % 0.61/0.82 big_f (skolemFOFtoCNF_X4 $_93 $_94) $_94 \/ % 0.61/0.82 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_93 $_94) $X3 % 0.61/0.82 (skolemFOFtoCNF_X2 $_93) \/ % 0.61/0.82 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_93 $_94) $_92 $_94 % 0.61/0.83 |- big_f $_92 $_94 \/ big_f $_93 (skolemFOFtoCNF_X4 $_93 $_94) \/ % 0.61/0.83 big_f $_94 $_92 \/ big_f $_94 (skolemFOFtoCNF_X4 $_93 $_94) \/ % 0.61/0.83 big_f $_94 (skolemFOFtoCNF_X4_1 $_93 $_94) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_93) (skolemFOFtoCNF_X4_1 $_93 $_94) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_93 $_94) $_93 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_93 $_94) $_94 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_93 $_94) (skolemFOFtoCNF_X2 $_93) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_93 $_94) $_92 $_94 % 0.61/0.83 |- ~big_f $_94 $_92 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_93 $_94) $_92 $_94 \/ % 0.61/0.83 big_f $_92 $_94 \/ big_f $_93 (skolemFOFtoCNF_X4 $_93 $_94) \/ % 0.61/0.83 big_f $_94 (skolemFOFtoCNF_X4 $_93 $_94) \/ % 0.61/0.83 big_f $_94 (skolemFOFtoCNF_X4_1 $_93 $_94) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_93) (skolemFOFtoCNF_X4_1 $_93 $_94) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_93 $_94) $_93 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_93 $_94) $_94 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_93 $_94) (skolemFOFtoCNF_X2 $_93) % 0.61/0.83 |- big_f $_95 (skolemFOFtoCNF_X2 $_96) \/ % 0.61/0.83 big_f $_96 (skolemFOFtoCNF_X4 $_96 $_97) \/ % 0.61/0.83 big_f $_97 (skolemFOFtoCNF_X4 $_96 $_97) \/ % 0.61/0.83 big_f $_97 (skolemFOFtoCNF_X4_1 $_96 $_97) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_96) $_95 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_96) (skolemFOFtoCNF_X4_1 $_96 $_97) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_96 $_97) $_96 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_96 $_97) $_97 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_96 $_97) $_97 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_95 (skolemFOFtoCNF_X4_1 $_96 $_97) % 0.61/0.83 (skolemFOFtoCNF_X2 $_96) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_96) $_95 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_95 (skolemFOFtoCNF_X4_1 $_96 $_97) % 0.61/0.83 (skolemFOFtoCNF_X2 $_96) \/ big_f $_95 (skolemFOFtoCNF_X2 $_96) \/ % 0.61/0.83 big_f $_96 (skolemFOFtoCNF_X4 $_96 $_97) \/ % 0.61/0.83 big_f $_97 (skolemFOFtoCNF_X4 $_96 $_97) \/ % 0.61/0.83 big_f $_97 (skolemFOFtoCNF_X4_1 $_96 $_97) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_96) (skolemFOFtoCNF_X4_1 $_96 $_97) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_96 $_97) $_96 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_96 $_97) $_97 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_96 $_97) $_97 % 0.61/0.83 |- big_f $_100 (skolemFOFtoCNF_X4 $_99 $_100) \/ % 0.61/0.83 big_f $_100 (skolemFOFtoCNF_X4_1 $_99 $_100) \/ % 0.61/0.83 big_f $_98 (skolemFOFtoCNF_X2 $_99) \/ % 0.61/0.83 big_f $_99 (skolemFOFtoCNF_X4 $_99 $_100) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_99) $_98 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_99) (skolemFOFtoCNF_X4_1 $_99 $_100) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_99 $_100) $_100 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_99 $_100) $_99 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_99 $_100) $_100 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_99 $_100) $_98 % 0.61/0.83 (skolemFOFtoCNF_X2 $_99) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_99) $_98 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_99 $_100) $_98 % 0.61/0.83 (skolemFOFtoCNF_X2 $_99) \/ % 0.61/0.83 big_f $_100 (skolemFOFtoCNF_X4 $_99 $_100) \/ % 0.61/0.83 big_f $_100 (skolemFOFtoCNF_X4_1 $_99 $_100) \/ % 0.61/0.83 big_f $_98 (skolemFOFtoCNF_X2 $_99) \/ % 0.61/0.83 big_f $_99 (skolemFOFtoCNF_X4 $_99 $_100) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_99) (skolemFOFtoCNF_X4_1 $_99 $_100) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_99 $_100) $_100 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_99 $_100) $_99 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_99 $_100) $_100 % 0.61/0.83 |- big_f $_102 (skolemFOFtoCNF_X4 $_102 $_103) \/ % 0.61/0.83 big_f $_103 (skolemFOFtoCNF_X4 $_102 $_103) \/ % 0.61/0.83 big_f $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_102) (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_102 $_103) $_102 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_102 $_103) $_103 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_102 $_103) $X1 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_102 $_103) $_101 \/ % 0.61/0.83 definitionFOFtoCNF_0 $X1 (skolemFOFtoCNF_X2 $_102) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 definitionFOFtoCNF_0 $_101 $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X2 $_102) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_101 $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) % 0.61/0.83 |- big_f $_102 (skolemFOFtoCNF_X4 $_102 $_103) \/ % 0.61/0.83 big_f $_103 (skolemFOFtoCNF_X4 $_102 $_103) \/ % 0.61/0.83 big_f $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_102) (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_102 $_103) $_102 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_102 $_103) $_103 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_102 $_103) $X3 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_102 $_103) $_101 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_101 $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_102) $X3 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_101 $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_102) $X3 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_102 $_103) % 0.61/0.83 |- big_f $X1 (skolemFOFtoCNF_X2 $_102) \/ % 0.61/0.83 big_f $_102 (skolemFOFtoCNF_X4 $_102 $_103) \/ % 0.61/0.83 big_f $_103 (skolemFOFtoCNF_X4 $_102 $_103) \/ % 0.61/0.83 big_f $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_102) (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_102 $_103) $_102 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_102 $_103) $_103 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_102 $_103) $_101 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_101 $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X4_1 $_102 $_103) % 0.61/0.83 (skolemFOFtoCNF_X2 $_102) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_101 $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) % 0.61/0.83 |- big_f $X3 (skolemFOFtoCNF_X2 $_102) \/ % 0.61/0.83 big_f $_102 (skolemFOFtoCNF_X4 $_102 $_103) \/ % 0.61/0.83 big_f $_103 (skolemFOFtoCNF_X4 $_102 $_103) \/ % 0.61/0.83 big_f $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_102) (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_102 $_103) $_102 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_102 $_103) $_103 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_102 $_103) $_101 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_101 $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_101 $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_102 $_103) $X3 % 0.61/0.83 (skolemFOFtoCNF_X2 $_102) % 0.61/0.83 |- big_f $_101 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 big_f $_102 (skolemFOFtoCNF_X4 $_102 $_103) \/ % 0.61/0.83 big_f $_103 (skolemFOFtoCNF_X4 $_102 $_103) \/ % 0.61/0.83 big_f $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_102) (skolemFOFtoCNF_X4_1 $_102 $_103) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_102 $_103) $_102 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_102 $_103) $_103 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_102 $_103) $_101 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_102 $_103) (skolemFOFtoCNF_X2 $_102) \/ % 0.61/0.83 definitionFOFtoCNF_0 $_101 $_103 (skolemFOFtoCNF_X4_1 $_102 $_103) % 0.61/0.83 |- big_f $_105 (skolemFOFtoCNF_X4 $_105 $_106) \/ % 0.61/0.83 big_f $_106 (skolemFOFtoCNF_X4 $_105 $_106) \/ % 0.61/0.83 big_f $_106 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_105) (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_105 $_106) $_105 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_105 $_106) $_106 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_105 $_106) $X1 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_105 $_106) $_104 \/ % 0.61/0.83 definitionFOFtoCNF_0 $X1 (skolemFOFtoCNF_X2 $_105) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 definitionFOFtoCNF_0 $_106 $_104 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X2 $_105) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_106 $_104 (skolemFOFtoCNF_X4_1 $_105 $_106) % 0.61/0.83 |- big_f $_105 (skolemFOFtoCNF_X4 $_105 $_106) \/ % 0.61/0.83 big_f $_106 (skolemFOFtoCNF_X4 $_105 $_106) \/ % 0.61/0.83 big_f $_106 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_105) (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_105 $_106) $_105 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_105 $_106) $_106 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_105 $_106) $X3 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_105 $_106) $_104 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_106 $_104 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_105) $X3 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_106 $_104 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_105) $X3 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_105 $_106) % 0.61/0.83 |- big_f $X1 (skolemFOFtoCNF_X2 $_105) \/ % 0.61/0.83 big_f $_105 (skolemFOFtoCNF_X4 $_105 $_106) \/ % 0.61/0.83 big_f $_106 (skolemFOFtoCNF_X4 $_105 $_106) \/ % 0.61/0.83 big_f $_106 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_105) (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_105 $_106) $_105 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_105 $_106) $_106 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_105 $_106) $_104 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_106 $_104 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X4_1 $_105 $_106) % 0.61/0.83 (skolemFOFtoCNF_X2 $_105) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_106 $_104 (skolemFOFtoCNF_X4_1 $_105 $_106) % 0.61/0.83 |- big_f $X3 (skolemFOFtoCNF_X2 $_105) \/ % 0.61/0.83 big_f $_105 (skolemFOFtoCNF_X4 $_105 $_106) \/ % 0.61/0.83 big_f $_106 (skolemFOFtoCNF_X4 $_105 $_106) \/ % 0.61/0.83 big_f $_106 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_105) (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_105 $_106) $_105 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_105 $_106) $_106 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_105 $_106) $_104 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_106 $_104 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_106 $_104 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_105 $_106) $X3 % 0.61/0.83 (skolemFOFtoCNF_X2 $_105) % 0.61/0.83 |- big_f $_104 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 big_f $_105 (skolemFOFtoCNF_X4 $_105 $_106) \/ % 0.61/0.83 big_f $_106 (skolemFOFtoCNF_X4 $_105 $_106) \/ % 0.61/0.83 big_f $_106 (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_105) (skolemFOFtoCNF_X4_1 $_105 $_106) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_105 $_106) $_105 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_105 $_106) $_106 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_105 $_106) $_104 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_105 $_106) (skolemFOFtoCNF_X2 $_105) \/ % 0.61/0.83 definitionFOFtoCNF_0 $_106 $_104 (skolemFOFtoCNF_X4_1 $_105 $_106) % 0.61/0.83 |- big_f $X1 $_109 \/ big_f $_108 (skolemFOFtoCNF_X4 $_108 $_109) \/ % 0.61/0.83 big_f $_109 (skolemFOFtoCNF_X4 $_108 $_109) \/ % 0.61/0.83 big_f $_109 (skolemFOFtoCNF_X4_1 $_108 $_109) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_108) (skolemFOFtoCNF_X4_1 $_108 $_109) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_108 $_109) $_108 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_108 $_109) $_109 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_108 $_109) $_107 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_108) $_107 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_108 $_109) \/ % 0.61/0.83 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X4_1 $_108 $_109) $_109 \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_108) $_107 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_108 $_109) % 0.61/0.83 |- big_f $X3 $_109 \/ big_f $_108 (skolemFOFtoCNF_X4 $_108 $_109) \/ % 0.61/0.83 big_f $_109 (skolemFOFtoCNF_X4 $_108 $_109) \/ % 0.61/0.83 big_f $_109 (skolemFOFtoCNF_X4_1 $_108 $_109) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_108) (skolemFOFtoCNF_X4_1 $_108 $_109) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_108 $_109) $_108 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_108 $_109) $_109 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_108 $_109) $_107 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_108) $_107 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_108 $_109) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_108) $_107 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_108 $_109) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_108 $_109) $X3 $_109 % 0.61/0.83 |- big_f $_107 (skolemFOFtoCNF_X4_1 $_108 $_109) \/ % 0.61/0.83 big_f $_108 (skolemFOFtoCNF_X4 $_108 $_109) \/ % 0.61/0.83 big_f $_109 (skolemFOFtoCNF_X4 $_108 $_109) \/ % 0.61/0.83 big_f $_109 (skolemFOFtoCNF_X4_1 $_108 $_109) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_108) (skolemFOFtoCNF_X4_1 $_108 $_109) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_108 $_109) $_108 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_108 $_109) $_109 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_108 $_109) $_107 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_108 $_109) $_109 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_108) $_107 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_108 $_109) % 0.61/0.83 |- big_f $X1 $_112 \/ big_f $_111 (skolemFOFtoCNF_X4 $_111 $_112) \/ % 0.61/0.83 big_f $_112 (skolemFOFtoCNF_X4 $_111 $_112) \/ % 0.61/0.83 big_f $_112 (skolemFOFtoCNF_X4_1 $_111 $_112) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_111) (skolemFOFtoCNF_X4_1 $_111 $_112) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_111 $_112) $_111 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_111 $_112) $_112 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_111 $_112) $_110 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_110 (skolemFOFtoCNF_X2 $_111) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_111 $_112) \/ % 0.61/0.83 definitionFOFtoCNF_1 $X1 (skolemFOFtoCNF_X4_1 $_111 $_112) $_112 \/ % 0.61/0.83 definitionFOFtoCNF_1 $_110 (skolemFOFtoCNF_X2 $_111) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_111 $_112) % 0.61/0.83 |- big_f $X3 $_112 \/ big_f $_111 (skolemFOFtoCNF_X4 $_111 $_112) \/ % 0.61/0.83 big_f $_112 (skolemFOFtoCNF_X4 $_111 $_112) \/ % 0.61/0.83 big_f $_112 (skolemFOFtoCNF_X4_1 $_111 $_112) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_111) (skolemFOFtoCNF_X4_1 $_111 $_112) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_111 $_112) $_111 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_111 $_112) $_112 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_111 $_112) $_110 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_110 (skolemFOFtoCNF_X2 $_111) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_111 $_112) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_110 (skolemFOFtoCNF_X2 $_111) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_111 $_112) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_111 $_112) $X3 $_112 % 0.61/0.83 |- big_f $_110 (skolemFOFtoCNF_X4_1 $_111 $_112) \/ % 0.61/0.83 big_f $_111 (skolemFOFtoCNF_X4 $_111 $_112) \/ % 0.61/0.83 big_f $_112 (skolemFOFtoCNF_X4 $_111 $_112) \/ % 0.61/0.83 big_f $_112 (skolemFOFtoCNF_X4_1 $_111 $_112) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_111) (skolemFOFtoCNF_X4_1 $_111 $_112) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_111 $_112) $_111 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_111 $_112) $_112 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_111 $_112) $_110 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_111 $_112) $_112 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_110 (skolemFOFtoCNF_X2 $_111) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_111 $_112) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X4_1 $_114 $_115) $_115 \/ big_f $_113 $_115 \/ % 0.61/0.83 big_f $_114 (skolemFOFtoCNF_X4 $_114 $_115) \/ big_f $_115 $_113 \/ % 0.61/0.83 big_f $_115 (skolemFOFtoCNF_X4 $_114 $_115) \/ % 0.61/0.83 big_f $_115 (skolemFOFtoCNF_X4_1 $_114 $_115) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_114) (skolemFOFtoCNF_X4_1 $_114 $_115) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_114 $_115) $_114 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_114 $_115) $_115 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_113 (skolemFOFtoCNF_X4_1 $_114 $_115) $_115 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_114 $_115 (skolemFOFtoCNF_X4 $_114 $_115) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X4_1 $_120 $_121) $_121 \/ big_f $_119 $_121 \/ % 0.61/0.83 big_f $_120 (skolemFOFtoCNF_X4 $_120 $_121) \/ big_f $_121 $_119 \/ % 0.61/0.83 big_f $_121 (skolemFOFtoCNF_X4 $_120 $_121) \/ % 0.61/0.83 big_f $_121 (skolemFOFtoCNF_X4_1 $_120 $_121) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_120) (skolemFOFtoCNF_X4_1 $_120 $_121) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_120 $_121) $_120 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_120 $_121) $_121 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_120 $_121 (skolemFOFtoCNF_X4 $_120 $_121) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_120 $_121) $_119 $_121 % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X4_1 $_129 $_130) (skolemFOFtoCNF_X2 $_129) \/ % 0.61/0.83 big_f $_128 (skolemFOFtoCNF_X2 $_129) \/ % 0.61/0.83 big_f $_129 (skolemFOFtoCNF_X4 $_129 $_130) \/ % 0.61/0.83 big_f $_130 (skolemFOFtoCNF_X4 $_129 $_130) \/ % 0.61/0.83 big_f $_130 (skolemFOFtoCNF_X4_1 $_129 $_130) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_129) $_128 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_129) (skolemFOFtoCNF_X4_1 $_129 $_130) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_129 $_130) $_129 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_129 $_130) $_130 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_128 (skolemFOFtoCNF_X4_1 $_129 $_130) % 0.61/0.83 (skolemFOFtoCNF_X2 $_129) \/ % 0.61/0.83 definitionFOFtoCNF_0 $_129 $_130 (skolemFOFtoCNF_X4 $_129 $_130) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X4_1 $_136 $_134) (skolemFOFtoCNF_X2 $_136) \/ % 0.61/0.83 big_f $_134 (skolemFOFtoCNF_X4 $_136 $_134) \/ % 0.61/0.83 big_f $_134 (skolemFOFtoCNF_X4_1 $_136 $_134) \/ % 0.61/0.83 big_f $_135 (skolemFOFtoCNF_X2 $_136) \/ % 0.61/0.83 big_f $_136 (skolemFOFtoCNF_X4 $_136 $_134) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_136) $_135 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_136) (skolemFOFtoCNF_X4_1 $_136 $_134) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_136 $_134) $_134 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_136 $_134) $_136 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_136 $_134 (skolemFOFtoCNF_X4 $_136 $_134) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_136 $_134) $_135 % 0.61/0.83 (skolemFOFtoCNF_X2 $_136) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X4_1 $_138 $_139) $_139 \/ % 0.61/0.83 big_f $_137 (skolemFOFtoCNF_X4_1 $_138 $_139) \/ % 0.61/0.83 big_f $_138 (skolemFOFtoCNF_X4 $_138 $_139) \/ % 0.61/0.83 big_f $_139 (skolemFOFtoCNF_X4 $_138 $_139) \/ % 0.61/0.83 big_f $_139 (skolemFOFtoCNF_X4_1 $_138 $_139) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_138) (skolemFOFtoCNF_X4_1 $_138 $_139) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_138 $_139) $_138 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_138 $_139) $_139 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_138 $_139) $_137 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_137 $_139 (skolemFOFtoCNF_X4_1 $_138 $_139) \/ % 0.61/0.83 definitionFOFtoCNF_0 $_138 $_139 (skolemFOFtoCNF_X4 $_138 $_139) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X4_1 $_141 $_142) $_142 \/ % 0.61/0.83 big_f $_140 (skolemFOFtoCNF_X4_1 $_141 $_142) \/ % 0.61/0.83 big_f $_141 (skolemFOFtoCNF_X4 $_141 $_142) \/ % 0.61/0.83 big_f $_142 (skolemFOFtoCNF_X4 $_141 $_142) \/ % 0.61/0.83 big_f $_142 (skolemFOFtoCNF_X4_1 $_141 $_142) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_141) (skolemFOFtoCNF_X4_1 $_141 $_142) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_141 $_142) $_141 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_141 $_142) $_142 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_141 $_142) $_140 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_141 $_142 (skolemFOFtoCNF_X4 $_141 $_142) \/ % 0.61/0.83 definitionFOFtoCNF_0 $_142 $_140 (skolemFOFtoCNF_X4_1 $_141 $_142) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X4_1 $_144 $_145) (skolemFOFtoCNF_X2 $_144) \/ % 0.61/0.83 big_f $_143 (skolemFOFtoCNF_X4_1 $_144 $_145) \/ % 0.61/0.83 big_f $_144 (skolemFOFtoCNF_X4 $_144 $_145) \/ % 0.61/0.83 big_f $_145 (skolemFOFtoCNF_X4 $_144 $_145) \/ % 0.61/0.83 big_f $_145 (skolemFOFtoCNF_X4_1 $_144 $_145) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_144) (skolemFOFtoCNF_X4_1 $_144 $_145) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_144 $_145) $_144 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_144 $_145) $_145 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_144 $_145) $_143 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_144 $_145 (skolemFOFtoCNF_X4 $_144 $_145) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_144) $_143 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_144 $_145) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X4_1 $_147 $_148) (skolemFOFtoCNF_X2 $_147) \/ % 0.61/0.83 big_f $_146 (skolemFOFtoCNF_X4_1 $_147 $_148) \/ % 0.61/0.83 big_f $_147 (skolemFOFtoCNF_X4 $_147 $_148) \/ % 0.61/0.83 big_f $_148 (skolemFOFtoCNF_X4 $_147 $_148) \/ % 0.61/0.83 big_f $_148 (skolemFOFtoCNF_X4_1 $_147 $_148) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_147) (skolemFOFtoCNF_X4_1 $_147 $_148) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_147 $_148) $_147 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_147 $_148) $_148 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_147 $_148) $_146 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_146 (skolemFOFtoCNF_X2 $_147) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_147 $_148) \/ % 0.61/0.83 definitionFOFtoCNF_0 $_147 $_148 (skolemFOFtoCNF_X4 $_147 $_148) % 0.61/0.83 |- big_f $_149 (skolemFOFtoCNF_X2 $_151) \/ big_f $_150 $_152 \/ % 0.61/0.83 big_f $_151 (skolemFOFtoCNF_X4 $_151 $_152) \/ % 0.61/0.83 big_f $_152 (skolemFOFtoCNF_X4 $_151 $_152) \/ % 0.61/0.83 big_f $_152 (skolemFOFtoCNF_X4_1 $_151 $_152) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_151) $_149 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_151) (skolemFOFtoCNF_X4_1 $_151 $_152) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_151 $_152) $_151 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_151 $_152) $_152 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_149 (skolemFOFtoCNF_X4_1 $_151 $_152) % 0.61/0.83 (skolemFOFtoCNF_X2 $_151) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_150 (skolemFOFtoCNF_X4_1 $_151 $_152) $_152 % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_151) $_149 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_149 (skolemFOFtoCNF_X4_1 $_151 $_152) % 0.61/0.83 (skolemFOFtoCNF_X2 $_151) \/ big_f $_149 (skolemFOFtoCNF_X2 $_151) \/ % 0.61/0.83 big_f $_150 $_152 \/ big_f $_151 (skolemFOFtoCNF_X4 $_151 $_152) \/ % 0.61/0.83 big_f $_152 (skolemFOFtoCNF_X4 $_151 $_152) \/ % 0.61/0.83 big_f $_152 (skolemFOFtoCNF_X4_1 $_151 $_152) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_151) (skolemFOFtoCNF_X4_1 $_151 $_152) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_151 $_152) $_151 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_151 $_152) $_152 \/ % 0.61/0.83 definitionFOFtoCNF_1 $_150 (skolemFOFtoCNF_X4_1 $_151 $_152) $_152 % 0.61/0.83 |- big_f $_149 (skolemFOFtoCNF_X2 $_151) \/ big_f $_150 $_152 \/ % 0.61/0.83 big_f $_151 (skolemFOFtoCNF_X4 $_151 $_152) \/ big_f $_152 $_150 \/ % 0.61/0.83 big_f $_152 (skolemFOFtoCNF_X4 $_151 $_152) \/ % 0.61/0.83 big_f $_152 (skolemFOFtoCNF_X4_1 $_151 $_152) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_151) (skolemFOFtoCNF_X4_1 $_151 $_152) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_151 $_152) $_151 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_151 $_152) $_152 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_150 (skolemFOFtoCNF_X4_1 $_151 $_152) $_152 \/ % 0.61/0.83 definitionFOFtoCNF_1 $_149 (skolemFOFtoCNF_X4_1 $_151 $_152) % 0.61/0.83 (skolemFOFtoCNF_X2 $_151) % 0.61/0.83 |- ~big_f $_152 $_150 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_150 (skolemFOFtoCNF_X4_1 $_151 $_152) $_152 \/ % 0.61/0.83 big_f $_149 (skolemFOFtoCNF_X2 $_151) \/ big_f $_150 $_152 \/ % 0.61/0.83 big_f $_151 (skolemFOFtoCNF_X4 $_151 $_152) \/ % 0.61/0.83 big_f $_152 (skolemFOFtoCNF_X4 $_151 $_152) \/ % 0.61/0.83 big_f $_152 (skolemFOFtoCNF_X4_1 $_151 $_152) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_151) (skolemFOFtoCNF_X4_1 $_151 $_152) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_151 $_152) $_151 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_151 $_152) $_152 \/ % 0.61/0.83 definitionFOFtoCNF_1 $_149 (skolemFOFtoCNF_X4_1 $_151 $_152) % 0.61/0.83 (skolemFOFtoCNF_X2 $_151) % 0.61/0.83 |- big_f $_153 (skolemFOFtoCNF_X2 $_155) \/ big_f $_154 $_156 \/ % 0.61/0.83 big_f $_155 (skolemFOFtoCNF_X4 $_155 $_156) \/ big_f $_156 $_154 \/ % 0.61/0.83 big_f $_156 (skolemFOFtoCNF_X4 $_155 $_156) \/ % 0.61/0.83 big_f $_156 (skolemFOFtoCNF_X4_1 $_155 $_156) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_155) (skolemFOFtoCNF_X4_1 $_155 $_156) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_155 $_156) $_155 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_155 $_156) $_156 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_154 (skolemFOFtoCNF_X4_1 $_155 $_156) $_156 \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_155 $_156) $_153 % 0.61/0.83 (skolemFOFtoCNF_X2 $_155) % 0.61/0.83 |- ~big_f $_156 $_154 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_154 (skolemFOFtoCNF_X4_1 $_155 $_156) $_156 \/ % 0.61/0.83 big_f $_153 (skolemFOFtoCNF_X2 $_155) \/ big_f $_154 $_156 \/ % 0.61/0.83 big_f $_155 (skolemFOFtoCNF_X4 $_155 $_156) \/ % 0.61/0.83 big_f $_156 (skolemFOFtoCNF_X4 $_155 $_156) \/ % 0.61/0.83 big_f $_156 (skolemFOFtoCNF_X4_1 $_155 $_156) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_155) (skolemFOFtoCNF_X4_1 $_155 $_156) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_155 $_156) $_155 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_155 $_156) $_156 \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_155 $_156) $_153 % 0.61/0.83 (skolemFOFtoCNF_X2 $_155) % 0.61/0.83 |- big_f $_153 (skolemFOFtoCNF_X2 $_155) \/ big_f $_154 $_156 \/ % 0.61/0.83 big_f $_155 (skolemFOFtoCNF_X4 $_155 $_156) \/ % 0.61/0.83 big_f $_156 (skolemFOFtoCNF_X4 $_155 $_156) \/ % 0.61/0.83 big_f $_156 (skolemFOFtoCNF_X4_1 $_155 $_156) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_155) $_153 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_155) (skolemFOFtoCNF_X4_1 $_155 $_156) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_155 $_156) $_155 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_155 $_156) $_156 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_155 $_156) $_153 % 0.61/0.83 (skolemFOFtoCNF_X2 $_155) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_154 (skolemFOFtoCNF_X4_1 $_155 $_156) $_156 % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_155) $_153 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_155 $_156) $_153 % 0.61/0.83 (skolemFOFtoCNF_X2 $_155) \/ big_f $_153 (skolemFOFtoCNF_X2 $_155) \/ % 0.61/0.83 big_f $_154 $_156 \/ big_f $_155 (skolemFOFtoCNF_X4 $_155 $_156) \/ % 0.61/0.83 big_f $_156 (skolemFOFtoCNF_X4 $_155 $_156) \/ % 0.61/0.83 big_f $_156 (skolemFOFtoCNF_X4_1 $_155 $_156) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_155) (skolemFOFtoCNF_X4_1 $_155 $_156) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_155 $_156) $_155 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_155 $_156) $_156 \/ % 0.61/0.83 definitionFOFtoCNF_1 $_154 (skolemFOFtoCNF_X4_1 $_155 $_156) $_156 % 0.61/0.83 |- big_f $_157 (skolemFOFtoCNF_X2 $_159) \/ big_f $_158 $_160 \/ % 0.61/0.83 big_f $_159 (skolemFOFtoCNF_X4 $_159 $_160) \/ % 0.61/0.83 big_f $_160 (skolemFOFtoCNF_X4 $_159 $_160) \/ % 0.61/0.83 big_f $_160 (skolemFOFtoCNF_X4_1 $_159 $_160) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_159) $_157 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_159) (skolemFOFtoCNF_X4_1 $_159 $_160) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_159 $_160) $_159 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_159 $_160) $_160 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_159 $_160) $_157 % 0.61/0.83 (skolemFOFtoCNF_X2 $_159) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_159 $_160) $_158 $_160 % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_159) $_157 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_159 $_160) $_157 % 0.61/0.83 (skolemFOFtoCNF_X2 $_159) \/ big_f $_157 (skolemFOFtoCNF_X2 $_159) \/ % 0.61/0.83 big_f $_158 $_160 \/ big_f $_159 (skolemFOFtoCNF_X4 $_159 $_160) \/ % 0.61/0.83 big_f $_160 (skolemFOFtoCNF_X4 $_159 $_160) \/ % 0.61/0.83 big_f $_160 (skolemFOFtoCNF_X4_1 $_159 $_160) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_159) (skolemFOFtoCNF_X4_1 $_159 $_160) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_159 $_160) $_159 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_159 $_160) $_160 \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_159 $_160) $_158 $_160 % 0.61/0.83 |- big_f $_157 (skolemFOFtoCNF_X2 $_159) \/ big_f $_158 $_160 \/ % 0.61/0.83 big_f $_159 (skolemFOFtoCNF_X4 $_159 $_160) \/ big_f $_160 $_158 \/ % 0.61/0.83 big_f $_160 (skolemFOFtoCNF_X4 $_159 $_160) \/ % 0.61/0.83 big_f $_160 (skolemFOFtoCNF_X4_1 $_159 $_160) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_159) (skolemFOFtoCNF_X4_1 $_159 $_160) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_159 $_160) $_159 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_159 $_160) $_160 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_159 $_160) $_158 $_160 \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_159 $_160) $_157 % 0.61/0.83 (skolemFOFtoCNF_X2 $_159) % 0.61/0.83 |- ~big_f $_160 $_158 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_159 $_160) $_158 $_160 \/ % 0.61/0.83 big_f $_157 (skolemFOFtoCNF_X2 $_159) \/ big_f $_158 $_160 \/ % 0.61/0.83 big_f $_159 (skolemFOFtoCNF_X4 $_159 $_160) \/ % 0.61/0.83 big_f $_160 (skolemFOFtoCNF_X4 $_159 $_160) \/ % 0.61/0.83 big_f $_160 (skolemFOFtoCNF_X4_1 $_159 $_160) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_159) (skolemFOFtoCNF_X4_1 $_159 $_160) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_159 $_160) $_159 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_159 $_160) $_160 \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_159 $_160) $_157 % 0.61/0.83 (skolemFOFtoCNF_X2 $_159) % 0.61/0.83 |- big_f $_161 (skolemFOFtoCNF_X2 $_163) \/ big_f $_162 $_164 \/ % 0.61/0.83 big_f $_163 (skolemFOFtoCNF_X4 $_163 $_164) \/ % 0.61/0.83 big_f $_164 (skolemFOFtoCNF_X4 $_163 $_164) \/ % 0.61/0.83 big_f $_164 (skolemFOFtoCNF_X4_1 $_163 $_164) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_163) $_161 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_163) (skolemFOFtoCNF_X4_1 $_163 $_164) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_163 $_164) $_163 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_163 $_164) $_164 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_161 (skolemFOFtoCNF_X4_1 $_163 $_164) % 0.61/0.83 (skolemFOFtoCNF_X2 $_163) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_163 $_164) $_162 $_164 % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_163) $_161 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_161 (skolemFOFtoCNF_X4_1 $_163 $_164) % 0.61/0.83 (skolemFOFtoCNF_X2 $_163) \/ big_f $_161 (skolemFOFtoCNF_X2 $_163) \/ % 0.61/0.83 big_f $_162 $_164 \/ big_f $_163 (skolemFOFtoCNF_X4 $_163 $_164) \/ % 0.61/0.83 big_f $_164 (skolemFOFtoCNF_X4 $_163 $_164) \/ % 0.61/0.83 big_f $_164 (skolemFOFtoCNF_X4_1 $_163 $_164) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_163) (skolemFOFtoCNF_X4_1 $_163 $_164) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_163 $_164) $_163 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_163 $_164) $_164 \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_163 $_164) $_162 $_164 % 0.61/0.83 |- big_f $_161 (skolemFOFtoCNF_X2 $_163) \/ big_f $_162 $_164 \/ % 0.61/0.83 big_f $_163 (skolemFOFtoCNF_X4 $_163 $_164) \/ big_f $_164 $_162 \/ % 0.61/0.83 big_f $_164 (skolemFOFtoCNF_X4 $_163 $_164) \/ % 0.61/0.83 big_f $_164 (skolemFOFtoCNF_X4_1 $_163 $_164) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_163) (skolemFOFtoCNF_X4_1 $_163 $_164) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_163 $_164) $_163 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_163 $_164) $_164 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_163 $_164) $_162 $_164 \/ % 0.61/0.83 definitionFOFtoCNF_1 $_161 (skolemFOFtoCNF_X4_1 $_163 $_164) % 0.61/0.83 (skolemFOFtoCNF_X2 $_163) % 0.61/0.83 |- ~big_f $_164 $_162 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_163 $_164) $_162 $_164 \/ % 0.61/0.83 big_f $_161 (skolemFOFtoCNF_X2 $_163) \/ big_f $_162 $_164 \/ % 0.61/0.83 big_f $_163 (skolemFOFtoCNF_X4 $_163 $_164) \/ % 0.61/0.83 big_f $_164 (skolemFOFtoCNF_X4 $_163 $_164) \/ % 0.61/0.83 big_f $_164 (skolemFOFtoCNF_X4_1 $_163 $_164) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_163) (skolemFOFtoCNF_X4_1 $_163 $_164) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_163 $_164) $_163 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_163 $_164) $_164 \/ % 0.61/0.83 definitionFOFtoCNF_1 $_161 (skolemFOFtoCNF_X4_1 $_163 $_164) % 0.61/0.83 (skolemFOFtoCNF_X2 $_163) % 0.61/0.83 |- big_f $_189 (skolemFOFtoCNF_X2 $_191) \/ % 0.61/0.83 big_f $_190 (skolemFOFtoCNF_X4_1 $_191 $_192) \/ % 0.61/0.83 big_f $_191 (skolemFOFtoCNF_X4 $_191 $_192) \/ % 0.61/0.83 big_f $_192 (skolemFOFtoCNF_X4 $_191 $_192) \/ % 0.61/0.83 big_f $_192 (skolemFOFtoCNF_X4_1 $_191 $_192) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_191) (skolemFOFtoCNF_X4_1 $_191 $_192) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_191 $_192) $_191 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_191 $_192) $_192 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_191 $_192) $_190 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_190 $_192 (skolemFOFtoCNF_X4_1 $_191 $_192) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_191 $_192) $_189 % 0.61/0.83 (skolemFOFtoCNF_X2 $_191) % 0.61/0.83 |- big_f $_189 (skolemFOFtoCNF_X2 $_191) \/ % 0.61/0.83 big_f $_191 (skolemFOFtoCNF_X4 $_191 $_192) \/ % 0.61/0.83 big_f $_192 (skolemFOFtoCNF_X4 $_191 $_192) \/ % 0.61/0.83 big_f $_192 (skolemFOFtoCNF_X4_1 $_191 $_192) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_191) $_189 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_191) (skolemFOFtoCNF_X4_1 $_191 $_192) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_191 $_192) $_191 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_191 $_192) $_192 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_191 $_192) $_190 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_190 $_192 (skolemFOFtoCNF_X4_1 $_191 $_192) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_191 $_192) $_189 % 0.61/0.83 (skolemFOFtoCNF_X2 $_191) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_190 $_192 (skolemFOFtoCNF_X4_1 $_191 $_192) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_191) $_189 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_191 $_192) $_189 % 0.61/0.83 (skolemFOFtoCNF_X2 $_191) \/ big_f $_189 (skolemFOFtoCNF_X2 $_191) \/ % 0.61/0.83 big_f $_191 (skolemFOFtoCNF_X4 $_191 $_192) \/ % 0.61/0.83 big_f $_192 (skolemFOFtoCNF_X4 $_191 $_192) \/ % 0.61/0.83 big_f $_192 (skolemFOFtoCNF_X4_1 $_191 $_192) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_191) (skolemFOFtoCNF_X4_1 $_191 $_192) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_191 $_192) $_191 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_191 $_192) $_192 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_191 $_192) $_190 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_190 $_192 (skolemFOFtoCNF_X4_1 $_191 $_192) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_190 $_192 (skolemFOFtoCNF_X4_1 $_191 $_192) % 0.61/0.83 |- big_f $_193 (skolemFOFtoCNF_X2 $_195) \/ % 0.61/0.83 big_f $_195 (skolemFOFtoCNF_X4 $_195 $_196) \/ % 0.61/0.83 big_f $_196 (skolemFOFtoCNF_X4 $_195 $_196) \/ % 0.61/0.83 big_f $_196 (skolemFOFtoCNF_X4_1 $_195 $_196) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_195) $_193 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_195) (skolemFOFtoCNF_X4_1 $_195 $_196) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_195 $_196) $_195 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_195 $_196) $_196 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_195 $_196) $_194 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_193 (skolemFOFtoCNF_X4_1 $_195 $_196) % 0.61/0.83 (skolemFOFtoCNF_X2 $_195) \/ % 0.61/0.83 definitionFOFtoCNF_0 $_194 $_196 (skolemFOFtoCNF_X4_1 $_195 $_196) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_194 $_196 (skolemFOFtoCNF_X4_1 $_195 $_196) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_195) $_193 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_193 (skolemFOFtoCNF_X4_1 $_195 $_196) % 0.61/0.83 (skolemFOFtoCNF_X2 $_195) \/ big_f $_193 (skolemFOFtoCNF_X2 $_195) \/ % 0.61/0.83 big_f $_195 (skolemFOFtoCNF_X4 $_195 $_196) \/ % 0.61/0.83 big_f $_196 (skolemFOFtoCNF_X4 $_195 $_196) \/ % 0.61/0.83 big_f $_196 (skolemFOFtoCNF_X4_1 $_195 $_196) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_195) (skolemFOFtoCNF_X4_1 $_195 $_196) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_195 $_196) $_195 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_195 $_196) $_196 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_195 $_196) $_194 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_194 $_196 (skolemFOFtoCNF_X4_1 $_195 $_196) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_194 $_196 (skolemFOFtoCNF_X4_1 $_195 $_196) % 0.61/0.83 |- big_f $_193 (skolemFOFtoCNF_X2 $_195) \/ % 0.61/0.83 big_f $_194 (skolemFOFtoCNF_X4_1 $_195 $_196) \/ % 0.61/0.83 big_f $_195 (skolemFOFtoCNF_X4 $_195 $_196) \/ % 0.61/0.83 big_f $_196 (skolemFOFtoCNF_X4 $_195 $_196) \/ % 0.61/0.83 big_f $_196 (skolemFOFtoCNF_X4_1 $_195 $_196) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_195) (skolemFOFtoCNF_X4_1 $_195 $_196) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_195 $_196) $_195 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_195 $_196) $_196 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_195 $_196) $_194 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_194 $_196 (skolemFOFtoCNF_X4_1 $_195 $_196) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_193 (skolemFOFtoCNF_X4_1 $_195 $_196) % 0.61/0.83 (skolemFOFtoCNF_X2 $_195) % 0.61/0.83 |- big_f $_197 (skolemFOFtoCNF_X2 $_199) \/ % 0.61/0.83 big_f $_199 (skolemFOFtoCNF_X4 $_199 $_200) \/ % 0.61/0.83 big_f $_200 (skolemFOFtoCNF_X4 $_199 $_200) \/ % 0.61/0.83 big_f $_200 (skolemFOFtoCNF_X4_1 $_199 $_200) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_199) $_197 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_199) (skolemFOFtoCNF_X4_1 $_199 $_200) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_199 $_200) $_199 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_199 $_200) $_200 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_199 $_200) $_198 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_197 (skolemFOFtoCNF_X4_1 $_199 $_200) % 0.61/0.83 (skolemFOFtoCNF_X2 $_199) \/ % 0.61/0.83 definitionFOFtoCNF_0 $_200 $_198 (skolemFOFtoCNF_X4_1 $_199 $_200) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_200 $_198 (skolemFOFtoCNF_X4_1 $_199 $_200) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_199) $_197 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_197 (skolemFOFtoCNF_X4_1 $_199 $_200) % 0.61/0.83 (skolemFOFtoCNF_X2 $_199) \/ big_f $_197 (skolemFOFtoCNF_X2 $_199) \/ % 0.61/0.83 big_f $_199 (skolemFOFtoCNF_X4 $_199 $_200) \/ % 0.61/0.83 big_f $_200 (skolemFOFtoCNF_X4 $_199 $_200) \/ % 0.61/0.83 big_f $_200 (skolemFOFtoCNF_X4_1 $_199 $_200) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_199) (skolemFOFtoCNF_X4_1 $_199 $_200) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_199 $_200) $_199 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_199 $_200) $_200 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_199 $_200) $_198 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_200 $_198 (skolemFOFtoCNF_X4_1 $_199 $_200) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_200 $_198 (skolemFOFtoCNF_X4_1 $_199 $_200) % 0.61/0.83 |- big_f $_197 (skolemFOFtoCNF_X2 $_199) \/ % 0.61/0.83 big_f $_198 (skolemFOFtoCNF_X4_1 $_199 $_200) \/ % 0.61/0.83 big_f $_199 (skolemFOFtoCNF_X4 $_199 $_200) \/ % 0.61/0.83 big_f $_200 (skolemFOFtoCNF_X4 $_199 $_200) \/ % 0.61/0.83 big_f $_200 (skolemFOFtoCNF_X4_1 $_199 $_200) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_199) (skolemFOFtoCNF_X4_1 $_199 $_200) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_199 $_200) $_199 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_199 $_200) $_200 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_199 $_200) $_198 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_200 $_198 (skolemFOFtoCNF_X4_1 $_199 $_200) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_197 (skolemFOFtoCNF_X4_1 $_199 $_200) % 0.61/0.83 (skolemFOFtoCNF_X2 $_199) % 0.61/0.83 |- big_f $_201 (skolemFOFtoCNF_X2 $_203) \/ % 0.61/0.83 big_f $_202 (skolemFOFtoCNF_X4_1 $_203 $_204) \/ % 0.61/0.83 big_f $_203 (skolemFOFtoCNF_X4 $_203 $_204) \/ % 0.61/0.83 big_f $_204 (skolemFOFtoCNF_X4 $_203 $_204) \/ % 0.61/0.83 big_f $_204 (skolemFOFtoCNF_X4_1 $_203 $_204) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_203) (skolemFOFtoCNF_X4_1 $_203 $_204) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_203 $_204) $_203 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_203 $_204) $_204 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_203 $_204) $_202 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_204 $_202 (skolemFOFtoCNF_X4_1 $_203 $_204) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_203 $_204) $_201 % 0.61/0.83 (skolemFOFtoCNF_X2 $_203) % 0.61/0.83 |- big_f $_201 (skolemFOFtoCNF_X2 $_203) \/ % 0.61/0.83 big_f $_203 (skolemFOFtoCNF_X4 $_203 $_204) \/ % 0.61/0.83 big_f $_204 (skolemFOFtoCNF_X4 $_203 $_204) \/ % 0.61/0.83 big_f $_204 (skolemFOFtoCNF_X4_1 $_203 $_204) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_203) $_201 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_203) (skolemFOFtoCNF_X4_1 $_203 $_204) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_203 $_204) $_203 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_203 $_204) $_204 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_203 $_204) $_202 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_204 $_202 (skolemFOFtoCNF_X4_1 $_203 $_204) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_203 $_204) $_201 % 0.61/0.83 (skolemFOFtoCNF_X2 $_203) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_204 $_202 (skolemFOFtoCNF_X4_1 $_203 $_204) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_203) $_201 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_203 $_204) $_201 % 0.61/0.83 (skolemFOFtoCNF_X2 $_203) \/ big_f $_201 (skolemFOFtoCNF_X2 $_203) \/ % 0.61/0.83 big_f $_203 (skolemFOFtoCNF_X4 $_203 $_204) \/ % 0.61/0.83 big_f $_204 (skolemFOFtoCNF_X4 $_203 $_204) \/ % 0.61/0.83 big_f $_204 (skolemFOFtoCNF_X4_1 $_203 $_204) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_203) (skolemFOFtoCNF_X4_1 $_203 $_204) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_203 $_204) $_203 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_203 $_204) $_204 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_203 $_204) $_202 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_204 $_202 (skolemFOFtoCNF_X4_1 $_203 $_204) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_204 $_202 (skolemFOFtoCNF_X4_1 $_203 $_204) % 0.61/0.83 |- big_f $_205 $_208 \/ big_f $_206 (skolemFOFtoCNF_X4_1 $_207 $_208) \/ % 0.61/0.83 big_f $_207 (skolemFOFtoCNF_X4 $_207 $_208) \/ % 0.61/0.83 big_f $_208 (skolemFOFtoCNF_X4 $_207 $_208) \/ % 0.61/0.83 big_f $_208 (skolemFOFtoCNF_X4_1 $_207 $_208) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_207) (skolemFOFtoCNF_X4_1 $_207 $_208) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_207 $_208) $_207 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_207 $_208) $_208 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_207 $_208) $_206 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_207) $_206 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_207 $_208) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_207 $_208) $_205 $_208 % 0.61/0.83 |- big_f $_205 $_208 \/ big_f $_207 (skolemFOFtoCNF_X4 $_207 $_208) \/ % 0.61/0.83 big_f $_208 $_205 \/ big_f $_208 (skolemFOFtoCNF_X4 $_207 $_208) \/ % 0.61/0.83 big_f $_208 (skolemFOFtoCNF_X4_1 $_207 $_208) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_207) (skolemFOFtoCNF_X4_1 $_207 $_208) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_207 $_208) $_207 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_207 $_208) $_208 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_207 $_208) $_206 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_207) $_206 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_207 $_208) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_207 $_208) $_205 $_208 \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_207) $_206 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_207 $_208) % 0.61/0.83 |- ~big_f $_208 $_205 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_207 $_208) $_205 $_208 \/ % 0.61/0.83 big_f $_205 $_208 \/ big_f $_207 (skolemFOFtoCNF_X4 $_207 $_208) \/ % 0.61/0.83 big_f $_208 (skolemFOFtoCNF_X4 $_207 $_208) \/ % 0.61/0.83 big_f $_208 (skolemFOFtoCNF_X4_1 $_207 $_208) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_207) (skolemFOFtoCNF_X4_1 $_207 $_208) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_207 $_208) $_207 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_207 $_208) $_208 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_207 $_208) $_206 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_207) $_206 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_207 $_208) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_207) $_206 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_207 $_208) % 0.61/0.83 |- big_f $_209 $_212 \/ big_f $_211 (skolemFOFtoCNF_X4 $_211 $_212) \/ % 0.61/0.83 big_f $_212 $_209 \/ big_f $_212 (skolemFOFtoCNF_X4 $_211 $_212) \/ % 0.61/0.83 big_f $_212 (skolemFOFtoCNF_X4_1 $_211 $_212) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_211) (skolemFOFtoCNF_X4_1 $_211 $_212) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_211 $_212) $_211 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_211 $_212) $_212 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_211 $_212) $_210 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_209 (skolemFOFtoCNF_X4_1 $_211 $_212) $_212 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_211) $_210 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_211 $_212) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_211) $_210 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_211 $_212) % 0.61/0.83 |- ~big_f $_212 $_209 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_209 (skolemFOFtoCNF_X4_1 $_211 $_212) $_212 \/ % 0.61/0.83 big_f $_209 $_212 \/ big_f $_211 (skolemFOFtoCNF_X4 $_211 $_212) \/ % 0.61/0.83 big_f $_212 (skolemFOFtoCNF_X4 $_211 $_212) \/ % 0.61/0.83 big_f $_212 (skolemFOFtoCNF_X4_1 $_211 $_212) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_211) (skolemFOFtoCNF_X4_1 $_211 $_212) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_211 $_212) $_211 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_211 $_212) $_212 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_211 $_212) $_210 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_211) $_210 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_211 $_212) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_211) $_210 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_211 $_212) % 0.61/0.83 |- big_f $_209 $_212 \/ big_f $_210 (skolemFOFtoCNF_X4_1 $_211 $_212) \/ % 0.61/0.83 big_f $_211 (skolemFOFtoCNF_X4 $_211 $_212) \/ % 0.61/0.83 big_f $_212 (skolemFOFtoCNF_X4 $_211 $_212) \/ % 0.61/0.83 big_f $_212 (skolemFOFtoCNF_X4_1 $_211 $_212) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_211) (skolemFOFtoCNF_X4_1 $_211 $_212) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_211 $_212) $_211 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_211 $_212) $_212 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_211 $_212) $_210 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_211) $_210 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_211 $_212) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_209 (skolemFOFtoCNF_X4_1 $_211 $_212) $_212 % 0.61/0.83 |- big_f $_213 $_216 \/ big_f $_214 (skolemFOFtoCNF_X4_1 $_215 $_216) \/ % 0.61/0.83 big_f $_215 (skolemFOFtoCNF_X4 $_215 $_216) \/ % 0.61/0.83 big_f $_216 (skolemFOFtoCNF_X4 $_215 $_216) \/ % 0.61/0.83 big_f $_216 (skolemFOFtoCNF_X4_1 $_215 $_216) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_215) (skolemFOFtoCNF_X4_1 $_215 $_216) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_215 $_216) $_215 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_215 $_216) $_216 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_215 $_216) $_214 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_214 (skolemFOFtoCNF_X2 $_215) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_215 $_216) \/ % 0.61/0.83 definitionFOFtoCNF_1 (skolemFOFtoCNF_X4_1 $_215 $_216) $_213 $_216 % 0.61/0.83 |- big_f $_213 $_216 \/ big_f $_215 (skolemFOFtoCNF_X4 $_215 $_216) \/ % 0.61/0.83 big_f $_216 $_213 \/ big_f $_216 (skolemFOFtoCNF_X4 $_215 $_216) \/ % 0.61/0.83 big_f $_216 (skolemFOFtoCNF_X4_1 $_215 $_216) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_215) (skolemFOFtoCNF_X4_1 $_215 $_216) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_215 $_216) $_215 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_215 $_216) $_216 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_215 $_216) $_214 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_214 (skolemFOFtoCNF_X2 $_215) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_215 $_216) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_215 $_216) $_213 $_216 \/ % 0.61/0.83 definitionFOFtoCNF_1 $_214 (skolemFOFtoCNF_X2 $_215) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_215 $_216) % 0.61/0.83 |- ~big_f $_216 $_213 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_215 $_216) $_213 $_216 \/ % 0.61/0.83 big_f $_213 $_216 \/ big_f $_215 (skolemFOFtoCNF_X4 $_215 $_216) \/ % 0.61/0.83 big_f $_216 (skolemFOFtoCNF_X4 $_215 $_216) \/ % 0.61/0.83 big_f $_216 (skolemFOFtoCNF_X4_1 $_215 $_216) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_215) (skolemFOFtoCNF_X4_1 $_215 $_216) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_215 $_216) $_215 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_215 $_216) $_216 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_215 $_216) $_214 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_214 (skolemFOFtoCNF_X2 $_215) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_215 $_216) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_214 (skolemFOFtoCNF_X2 $_215) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_215 $_216) % 0.61/0.83 |- big_f $_217 $_220 \/ big_f $_219 (skolemFOFtoCNF_X4 $_219 $_220) \/ % 0.61/0.83 big_f $_220 $_217 \/ big_f $_220 (skolemFOFtoCNF_X4 $_219 $_220) \/ % 0.61/0.83 big_f $_220 (skolemFOFtoCNF_X4_1 $_219 $_220) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_219) (skolemFOFtoCNF_X4_1 $_219 $_220) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_219 $_220) $_219 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_219 $_220) $_220 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_219 $_220) $_218 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_217 (skolemFOFtoCNF_X4_1 $_219 $_220) $_220 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_218 (skolemFOFtoCNF_X2 $_219) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_219 $_220) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_218 (skolemFOFtoCNF_X2 $_219) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_219 $_220) % 0.61/0.83 |- ~big_f $_220 $_217 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_217 (skolemFOFtoCNF_X4_1 $_219 $_220) $_220 \/ % 0.61/0.83 big_f $_217 $_220 \/ big_f $_219 (skolemFOFtoCNF_X4 $_219 $_220) \/ % 0.61/0.83 big_f $_220 (skolemFOFtoCNF_X4 $_219 $_220) \/ % 0.61/0.83 big_f $_220 (skolemFOFtoCNF_X4_1 $_219 $_220) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_219) (skolemFOFtoCNF_X4_1 $_219 $_220) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_219 $_220) $_219 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_219 $_220) $_220 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_219 $_220) $_218 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_218 (skolemFOFtoCNF_X2 $_219) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_219 $_220) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_218 (skolemFOFtoCNF_X2 $_219) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_219 $_220) % 0.61/0.83 |- big_f $_217 $_220 \/ big_f $_218 (skolemFOFtoCNF_X4_1 $_219 $_220) \/ % 0.61/0.83 big_f $_219 (skolemFOFtoCNF_X4 $_219 $_220) \/ % 0.61/0.83 big_f $_220 (skolemFOFtoCNF_X4 $_219 $_220) \/ % 0.61/0.83 big_f $_220 (skolemFOFtoCNF_X4_1 $_219 $_220) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_219) (skolemFOFtoCNF_X4_1 $_219 $_220) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_219 $_220) $_219 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_219 $_220) $_220 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_219 $_220) $_218 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_218 (skolemFOFtoCNF_X2 $_219) % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_219 $_220) \/ % 0.61/0.83 definitionFOFtoCNF_1 $_217 (skolemFOFtoCNF_X4_1 $_219 $_220) $_220 % 0.61/0.83 |- big_f $_225 (skolemFOFtoCNF_X2 $_227) \/ big_f $_226 $_228 \/ % 0.61/0.83 big_f $_227 (skolemFOFtoCNF_X4 $_227 $_228) \/ big_f $_228 $_226 \/ % 0.61/0.83 big_f $_228 (skolemFOFtoCNF_X4 $_227 $_228) \/ % 0.61/0.83 big_f $_228 (skolemFOFtoCNF_X4_1 $_227 $_228) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_227) $_225 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_227) (skolemFOFtoCNF_X4_1 $_227 $_228) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_227 $_228) $_227 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_227 $_228) $_228 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_225 (skolemFOFtoCNF_X4_1 $_227 $_228) % 0.61/0.83 (skolemFOFtoCNF_X2 $_227) \/ % 0.61/0.83 definitionFOFtoCNF_0 $_226 (skolemFOFtoCNF_X4_1 $_227 $_228) $_228 % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_227) $_225 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_225 (skolemFOFtoCNF_X4_1 $_227 $_228) % 0.61/0.83 (skolemFOFtoCNF_X2 $_227) \/ big_f $_225 (skolemFOFtoCNF_X2 $_227) \/ % 0.61/0.83 big_f $_226 $_228 \/ big_f $_227 (skolemFOFtoCNF_X4 $_227 $_228) \/ % 0.61/0.83 big_f $_228 $_226 \/ big_f $_228 (skolemFOFtoCNF_X4 $_227 $_228) \/ % 0.61/0.83 big_f $_228 (skolemFOFtoCNF_X4_1 $_227 $_228) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_227) (skolemFOFtoCNF_X4_1 $_227 $_228) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_227 $_228) $_227 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_227 $_228) $_228 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_226 (skolemFOFtoCNF_X4_1 $_227 $_228) $_228 % 0.61/0.83 |- big_f $_233 (skolemFOFtoCNF_X2 $_235) \/ big_f $_234 $_236 \/ % 0.61/0.83 big_f $_235 (skolemFOFtoCNF_X4 $_235 $_236) \/ big_f $_236 $_234 \/ % 0.61/0.83 big_f $_236 (skolemFOFtoCNF_X4 $_235 $_236) \/ % 0.61/0.83 big_f $_236 (skolemFOFtoCNF_X4_1 $_235 $_236) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_235) $_233 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_235) (skolemFOFtoCNF_X4_1 $_235 $_236) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_235 $_236) $_235 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_235 $_236) $_236 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_234 (skolemFOFtoCNF_X4_1 $_235 $_236) $_236 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_235 $_236) $_233 % 0.61/0.83 (skolemFOFtoCNF_X2 $_235) % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_235) $_233 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_235 $_236) $_233 % 0.61/0.83 (skolemFOFtoCNF_X2 $_235) \/ big_f $_233 (skolemFOFtoCNF_X2 $_235) \/ % 0.61/0.83 big_f $_234 $_236 \/ big_f $_235 (skolemFOFtoCNF_X4 $_235 $_236) \/ % 0.61/0.83 big_f $_236 $_234 \/ big_f $_236 (skolemFOFtoCNF_X4 $_235 $_236) \/ % 0.61/0.83 big_f $_236 (skolemFOFtoCNF_X4_1 $_235 $_236) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_235) (skolemFOFtoCNF_X4_1 $_235 $_236) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_235 $_236) $_235 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_235 $_236) $_236 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_234 (skolemFOFtoCNF_X4_1 $_235 $_236) $_236 % 0.61/0.83 |- big_f $_241 (skolemFOFtoCNF_X2 $_243) \/ big_f $_242 $_244 \/ % 0.61/0.83 big_f $_243 (skolemFOFtoCNF_X4 $_243 $_244) \/ big_f $_244 $_242 \/ % 0.61/0.83 big_f $_244 (skolemFOFtoCNF_X4 $_243 $_244) \/ % 0.61/0.83 big_f $_244 (skolemFOFtoCNF_X4_1 $_243 $_244) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_243) $_241 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_243) (skolemFOFtoCNF_X4_1 $_243 $_244) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_243 $_244) $_243 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_243 $_244) $_244 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_243 $_244) $_241 % 0.61/0.83 (skolemFOFtoCNF_X2 $_243) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_243 $_244) $_242 $_244 % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_243) $_241 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_243 $_244) $_241 % 0.61/0.83 (skolemFOFtoCNF_X2 $_243) \/ big_f $_241 (skolemFOFtoCNF_X2 $_243) \/ % 0.61/0.83 big_f $_242 $_244 \/ big_f $_243 (skolemFOFtoCNF_X4 $_243 $_244) \/ % 0.61/0.83 big_f $_244 $_242 \/ big_f $_244 (skolemFOFtoCNF_X4 $_243 $_244) \/ % 0.61/0.83 big_f $_244 (skolemFOFtoCNF_X4_1 $_243 $_244) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_243) (skolemFOFtoCNF_X4_1 $_243 $_244) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_243 $_244) $_243 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_243 $_244) $_244 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_243 $_244) $_242 $_244 % 0.61/0.83 |- big_f $_249 (skolemFOFtoCNF_X2 $_251) \/ big_f $_250 $_252 \/ % 0.61/0.83 big_f $_251 (skolemFOFtoCNF_X4 $_251 $_252) \/ big_f $_252 $_250 \/ % 0.61/0.83 big_f $_252 (skolemFOFtoCNF_X4 $_251 $_252) \/ % 0.61/0.83 big_f $_252 (skolemFOFtoCNF_X4_1 $_251 $_252) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_251) $_249 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_251) (skolemFOFtoCNF_X4_1 $_251 $_252) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_251 $_252) $_251 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_251 $_252) $_252 \/ % 0.61/0.83 definitionFOFtoCNF_0 $_249 (skolemFOFtoCNF_X4_1 $_251 $_252) % 0.61/0.83 (skolemFOFtoCNF_X2 $_251) \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_251 $_252) $_250 $_252 % 0.61/0.83 |- ~big_f (skolemFOFtoCNF_X2 $_251) $_249 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_249 (skolemFOFtoCNF_X4_1 $_251 $_252) % 0.61/0.83 (skolemFOFtoCNF_X2 $_251) \/ big_f $_249 (skolemFOFtoCNF_X2 $_251) \/ % 0.61/0.83 big_f $_250 $_252 \/ big_f $_251 (skolemFOFtoCNF_X4 $_251 $_252) \/ % 0.61/0.83 big_f $_252 $_250 \/ big_f $_252 (skolemFOFtoCNF_X4 $_251 $_252) \/ % 0.61/0.83 big_f $_252 (skolemFOFtoCNF_X4_1 $_251 $_252) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_251) (skolemFOFtoCNF_X4_1 $_251 $_252) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_251 $_252) $_251 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_251 $_252) $_252 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_251 $_252) $_250 $_252 % 0.61/0.83 |- ~big_f $_256 $_253 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_255 $_256) $_253 $_256 \/ % 0.61/0.83 big_f $_253 $_256 \/ big_f $_254 (skolemFOFtoCNF_X4_1 $_255 $_256) \/ % 0.61/0.83 big_f $_255 (skolemFOFtoCNF_X4 $_255 $_256) \/ % 0.61/0.83 big_f $_256 (skolemFOFtoCNF_X4 $_255 $_256) \/ % 0.61/0.83 big_f $_256 (skolemFOFtoCNF_X4_1 $_255 $_256) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_255) (skolemFOFtoCNF_X4_1 $_255 $_256) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_255 $_256) $_255 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_255 $_256) $_256 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_255 $_256) $_254 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_255) $_254 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_255 $_256) % 0.61/0.83 |- ~big_f $_260 $_257 \/ % 0.61/0.83 ~definitionFOFtoCNF_0 $_257 (skolemFOFtoCNF_X4_1 $_259 $_260) $_260 \/ % 0.61/0.83 big_f $_257 $_260 \/ big_f $_258 (skolemFOFtoCNF_X4_1 $_259 $_260) \/ % 0.61/0.83 big_f $_259 (skolemFOFtoCNF_X4 $_259 $_260) \/ % 0.61/0.83 big_f $_260 (skolemFOFtoCNF_X4 $_259 $_260) \/ % 0.61/0.83 big_f $_260 (skolemFOFtoCNF_X4_1 $_259 $_260) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X2 $_259) (skolemFOFtoCNF_X4_1 $_259 $_260) \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_259 $_260) $_259 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4 $_259 $_260) $_260 \/ % 0.61/0.83 big_f (skolemFOFtoCNF_X4_1 $_259 $_260) $_258 \/ % 0.61/0.83 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_259) $_258 % 0.61/0.83 (skolemFOFtoCNF_X4_1 $_259 $_260) % 0.61/0.84 |- ~big_f $_264 $_261 \/ % 0.61/0.84 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_263 $_264) $_261 $_264 \/ % 0.61/0.84 big_f $_261 $_264 \/ big_f $_262 (skolemFOFtoCNF_X4_1 $_263 $_264) \/ % 0.61/0.84 big_f $_263 (skolemFOFtoCNF_X4 $_263 $_264) \/ % 0.61/0.84 big_f $_264 (skolemFOFtoCNF_X4 $_263 $_264) \/ % 0.61/0.84 big_f $_264 (skolemFOFtoCNF_X4_1 $_263 $_264) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_263) (skolemFOFtoCNF_X4_1 $_263 $_264) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_263 $_264) $_263 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_263 $_264) $_264 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_263 $_264) $_262 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_262 (skolemFOFtoCNF_X2 $_263) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_263 $_264) % 0.61/0.84 |- ~big_f $_268 $_265 \/ % 0.61/0.84 ~definitionFOFtoCNF_0 $_265 (skolemFOFtoCNF_X4_1 $_267 $_268) $_268 \/ % 0.61/0.84 big_f $_265 $_268 \/ big_f $_266 (skolemFOFtoCNF_X4_1 $_267 $_268) \/ % 0.61/0.84 big_f $_267 (skolemFOFtoCNF_X4 $_267 $_268) \/ % 0.61/0.84 big_f $_268 (skolemFOFtoCNF_X4 $_267 $_268) \/ % 0.61/0.84 big_f $_268 (skolemFOFtoCNF_X4_1 $_267 $_268) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_267) (skolemFOFtoCNF_X4_1 $_267 $_268) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_267 $_268) $_267 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_267 $_268) $_268 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_267 $_268) $_266 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_266 (skolemFOFtoCNF_X2 $_267) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_267 $_268) % 0.61/0.84 |- ~big_f $_276 $_274 \/ % 0.61/0.84 ~definitionFOFtoCNF_0 $_274 (skolemFOFtoCNF_X4_1 $_275 $_276) $_276 \/ % 0.61/0.84 big_f $_273 (skolemFOFtoCNF_X2 $_275) \/ big_f $_274 $_276 \/ % 0.61/0.84 big_f $_275 (skolemFOFtoCNF_X4 $_275 $_276) \/ % 0.61/0.84 big_f $_276 (skolemFOFtoCNF_X4 $_275 $_276) \/ % 0.61/0.84 big_f $_276 (skolemFOFtoCNF_X4_1 $_275 $_276) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_275) $_273 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_275) (skolemFOFtoCNF_X4_1 $_275 $_276) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_275 $_276) $_275 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_275 $_276) $_276 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_273 (skolemFOFtoCNF_X4_1 $_275 $_276) % 0.61/0.84 (skolemFOFtoCNF_X2 $_275) % 0.61/0.84 |- ~big_f $_284 $_282 \/ % 0.61/0.84 ~definitionFOFtoCNF_0 $_282 (skolemFOFtoCNF_X4_1 $_283 $_284) $_284 \/ % 0.61/0.84 big_f $_281 (skolemFOFtoCNF_X2 $_283) \/ big_f $_282 $_284 \/ % 0.61/0.84 big_f $_283 (skolemFOFtoCNF_X4 $_283 $_284) \/ % 0.61/0.84 big_f $_284 (skolemFOFtoCNF_X4 $_283 $_284) \/ % 0.61/0.84 big_f $_284 (skolemFOFtoCNF_X4_1 $_283 $_284) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_283) $_281 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_283) (skolemFOFtoCNF_X4_1 $_283 $_284) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_283 $_284) $_283 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_283 $_284) $_284 \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_283 $_284) $_281 % 0.61/0.84 (skolemFOFtoCNF_X2 $_283) % 0.61/0.84 |- ~big_f $_292 $_290 \/ % 0.61/0.84 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_291 $_292) $_290 $_292 \/ % 0.61/0.84 big_f $_289 (skolemFOFtoCNF_X2 $_291) \/ big_f $_290 $_292 \/ % 0.61/0.84 big_f $_291 (skolemFOFtoCNF_X4 $_291 $_292) \/ % 0.61/0.84 big_f $_292 (skolemFOFtoCNF_X4 $_291 $_292) \/ % 0.61/0.84 big_f $_292 (skolemFOFtoCNF_X4_1 $_291 $_292) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_291) $_289 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_291) (skolemFOFtoCNF_X4_1 $_291 $_292) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_291 $_292) $_291 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_291 $_292) $_292 \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_291 $_292) $_289 % 0.61/0.84 (skolemFOFtoCNF_X2 $_291) % 0.61/0.84 |- ~big_f $_296 $_294 \/ % 0.61/0.84 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_295 $_296) $_294 $_296 \/ % 0.61/0.84 big_f $_293 (skolemFOFtoCNF_X2 $_295) \/ big_f $_294 $_296 \/ % 0.61/0.84 big_f $_295 (skolemFOFtoCNF_X4 $_295 $_296) \/ % 0.61/0.84 big_f $_296 (skolemFOFtoCNF_X4 $_295 $_296) \/ % 0.61/0.84 big_f $_296 (skolemFOFtoCNF_X4_1 $_295 $_296) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_295) $_293 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_295) (skolemFOFtoCNF_X4_1 $_295 $_296) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_295 $_296) $_295 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_295 $_296) $_296 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_293 (skolemFOFtoCNF_X4_1 $_295 $_296) % 0.61/0.84 (skolemFOFtoCNF_X2 $_295) % 0.61/0.84 |- ~big_f (skolemFOFtoCNF_X2 $_303) $_301 \/ % 0.61/0.84 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_303 $_304) $_301 % 0.61/0.84 (skolemFOFtoCNF_X2 $_303) \/ big_f $_301 (skolemFOFtoCNF_X2 $_303) \/ % 0.61/0.84 big_f $_302 (skolemFOFtoCNF_X4_1 $_303 $_304) \/ % 0.61/0.84 big_f $_303 (skolemFOFtoCNF_X4 $_303 $_304) \/ % 0.61/0.84 big_f $_304 (skolemFOFtoCNF_X4 $_303 $_304) \/ % 0.61/0.84 big_f $_304 (skolemFOFtoCNF_X4_1 $_303 $_304) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_303) (skolemFOFtoCNF_X4_1 $_303 $_304) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_303 $_304) $_303 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_303 $_304) $_304 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_303 $_304) $_302 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_302 $_304 (skolemFOFtoCNF_X4_1 $_303 $_304) % 0.61/0.84 |- ~big_f (skolemFOFtoCNF_X2 $_307) $_305 \/ % 0.61/0.84 ~definitionFOFtoCNF_0 $_305 (skolemFOFtoCNF_X4_1 $_307 $_308) % 0.61/0.84 (skolemFOFtoCNF_X2 $_307) \/ big_f $_305 (skolemFOFtoCNF_X2 $_307) \/ % 0.61/0.84 big_f $_306 (skolemFOFtoCNF_X4_1 $_307 $_308) \/ % 0.61/0.84 big_f $_307 (skolemFOFtoCNF_X4 $_307 $_308) \/ % 0.61/0.84 big_f $_308 (skolemFOFtoCNF_X4 $_307 $_308) \/ % 0.61/0.84 big_f $_308 (skolemFOFtoCNF_X4_1 $_307 $_308) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_307) (skolemFOFtoCNF_X4_1 $_307 $_308) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_307 $_308) $_307 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_307 $_308) $_308 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_307 $_308) $_306 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_306 $_308 (skolemFOFtoCNF_X4_1 $_307 $_308) % 0.61/0.84 |- ~big_f (skolemFOFtoCNF_X2 $_311) $_309 \/ % 0.61/0.84 ~definitionFOFtoCNF_0 $_309 (skolemFOFtoCNF_X4_1 $_311 $_312) % 0.61/0.84 (skolemFOFtoCNF_X2 $_311) \/ big_f $_309 (skolemFOFtoCNF_X2 $_311) \/ % 0.61/0.84 big_f $_310 (skolemFOFtoCNF_X4_1 $_311 $_312) \/ % 0.61/0.84 big_f $_311 (skolemFOFtoCNF_X4 $_311 $_312) \/ % 0.61/0.84 big_f $_312 (skolemFOFtoCNF_X4 $_311 $_312) \/ % 0.61/0.84 big_f $_312 (skolemFOFtoCNF_X4_1 $_311 $_312) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_311) (skolemFOFtoCNF_X4_1 $_311 $_312) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_311 $_312) $_311 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_311 $_312) $_312 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_311 $_312) $_310 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_312 $_310 (skolemFOFtoCNF_X4_1 $_311 $_312) % 0.61/0.84 |- ~big_f (skolemFOFtoCNF_X2 $_315) $_313 \/ % 0.61/0.84 ~definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_315 $_316) $_313 % 0.61/0.84 (skolemFOFtoCNF_X2 $_315) \/ big_f $_313 (skolemFOFtoCNF_X2 $_315) \/ % 0.61/0.84 big_f $_314 (skolemFOFtoCNF_X4_1 $_315 $_316) \/ % 0.61/0.84 big_f $_315 (skolemFOFtoCNF_X4 $_315 $_316) \/ % 0.61/0.84 big_f $_316 (skolemFOFtoCNF_X4 $_315 $_316) \/ % 0.61/0.84 big_f $_316 (skolemFOFtoCNF_X4_1 $_315 $_316) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_315) (skolemFOFtoCNF_X4_1 $_315 $_316) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_315 $_316) $_315 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_315 $_316) $_316 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_315 $_316) $_314 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_316 $_314 (skolemFOFtoCNF_X4_1 $_315 $_316) % 0.61/0.84 |- big_f $_318 (skolemFOFtoCNF_X4_1 $_319 $_320) \/ % 0.61/0.84 big_f $_319 (skolemFOFtoCNF_X4 $_319 $_320) \/ % 0.61/0.84 big_f $_320 (skolemFOFtoCNF_X4 $_319 $_320) \/ % 0.61/0.84 big_f $_320 (skolemFOFtoCNF_X4_1 $_319 $_320) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_319) (skolemFOFtoCNF_X4_1 $_319 $_320) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_319 $_320) $_319 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_319 $_320) $_320 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_319 $_320) $_317 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_319 $_320) $_318 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_318 $_320 (skolemFOFtoCNF_X4_1 $_319 $_320) \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_319) $_317 % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_319 $_320) \/ % 0.61/0.84 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_319) $_317 % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_319 $_320) % 0.61/0.84 |- big_f $_317 (skolemFOFtoCNF_X4_1 $_319 $_320) \/ % 0.61/0.84 big_f $_319 (skolemFOFtoCNF_X4 $_319 $_320) \/ % 0.61/0.84 big_f $_320 (skolemFOFtoCNF_X4 $_319 $_320) \/ % 0.61/0.84 big_f $_320 (skolemFOFtoCNF_X4_1 $_319 $_320) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_319) (skolemFOFtoCNF_X4_1 $_319 $_320) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_319 $_320) $_319 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_319 $_320) $_320 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_319 $_320) $_317 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_319 $_320) $_318 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_318 $_320 (skolemFOFtoCNF_X4_1 $_319 $_320) \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_319) $_317 % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_319 $_320) \/ % 0.61/0.84 definitionFOFtoCNF_1 $_318 $_320 (skolemFOFtoCNF_X4_1 $_319 $_320) % 0.61/0.84 |- big_f $_321 (skolemFOFtoCNF_X4_1 $_323 $_324) \/ % 0.61/0.84 big_f $_323 (skolemFOFtoCNF_X4 $_323 $_324) \/ % 0.61/0.84 big_f $_324 (skolemFOFtoCNF_X4 $_323 $_324) \/ % 0.61/0.84 big_f $_324 (skolemFOFtoCNF_X4_1 $_323 $_324) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_323) (skolemFOFtoCNF_X4_1 $_323 $_324) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_323 $_324) $_323 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_323 $_324) $_324 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_323 $_324) $_321 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_323 $_324) $_322 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_321 (skolemFOFtoCNF_X2 $_323) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_323 $_324) \/ % 0.61/0.84 definitionFOFtoCNF_0 $_322 $_324 (skolemFOFtoCNF_X4_1 $_323 $_324) \/ % 0.61/0.84 definitionFOFtoCNF_1 $_322 $_324 (skolemFOFtoCNF_X4_1 $_323 $_324) % 0.61/0.84 |- big_f $_322 (skolemFOFtoCNF_X4_1 $_323 $_324) \/ % 0.61/0.84 big_f $_323 (skolemFOFtoCNF_X4 $_323 $_324) \/ % 0.61/0.84 big_f $_324 (skolemFOFtoCNF_X4 $_323 $_324) \/ % 0.61/0.84 big_f $_324 (skolemFOFtoCNF_X4_1 $_323 $_324) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_323) (skolemFOFtoCNF_X4_1 $_323 $_324) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_323 $_324) $_323 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_323 $_324) $_324 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_323 $_324) $_321 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_323 $_324) $_322 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_321 (skolemFOFtoCNF_X2 $_323) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_323 $_324) \/ % 0.61/0.84 definitionFOFtoCNF_0 $_322 $_324 (skolemFOFtoCNF_X4_1 $_323 $_324) \/ % 0.61/0.84 definitionFOFtoCNF_1 $_321 (skolemFOFtoCNF_X2 $_323) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_323 $_324) % 0.61/0.84 |- big_f $_325 (skolemFOFtoCNF_X4_1 $_327 $_328) \/ % 0.61/0.84 big_f $_327 (skolemFOFtoCNF_X4 $_327 $_328) \/ % 0.61/0.84 big_f $_328 (skolemFOFtoCNF_X4 $_327 $_328) \/ % 0.61/0.84 big_f $_328 (skolemFOFtoCNF_X4_1 $_327 $_328) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_327) (skolemFOFtoCNF_X4_1 $_327 $_328) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_327 $_328) $_327 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_327 $_328) $_328 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_327 $_328) $_325 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_327 $_328) $_326 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_325 (skolemFOFtoCNF_X2 $_327) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_327 $_328) \/ % 0.61/0.84 definitionFOFtoCNF_0 $_328 $_326 (skolemFOFtoCNF_X4_1 $_327 $_328) \/ % 0.61/0.84 definitionFOFtoCNF_1 $_328 $_326 (skolemFOFtoCNF_X4_1 $_327 $_328) % 0.61/0.84 |- big_f $_326 (skolemFOFtoCNF_X4_1 $_327 $_328) \/ % 0.61/0.84 big_f $_327 (skolemFOFtoCNF_X4 $_327 $_328) \/ % 0.61/0.84 big_f $_328 (skolemFOFtoCNF_X4 $_327 $_328) \/ % 0.61/0.84 big_f $_328 (skolemFOFtoCNF_X4_1 $_327 $_328) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_327) (skolemFOFtoCNF_X4_1 $_327 $_328) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_327 $_328) $_327 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_327 $_328) $_328 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_327 $_328) $_325 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_327 $_328) $_326 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_325 (skolemFOFtoCNF_X2 $_327) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_327 $_328) \/ % 0.61/0.84 definitionFOFtoCNF_0 $_328 $_326 (skolemFOFtoCNF_X4_1 $_327 $_328) \/ % 0.61/0.84 definitionFOFtoCNF_1 $_325 (skolemFOFtoCNF_X2 $_327) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_327 $_328) % 0.61/0.84 |- big_f $_330 (skolemFOFtoCNF_X4_1 $_331 $_332) \/ % 0.61/0.84 big_f $_331 (skolemFOFtoCNF_X4 $_331 $_332) \/ % 0.61/0.84 big_f $_332 (skolemFOFtoCNF_X4 $_331 $_332) \/ % 0.61/0.84 big_f $_332 (skolemFOFtoCNF_X4_1 $_331 $_332) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_331) (skolemFOFtoCNF_X4_1 $_331 $_332) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_331 $_332) $_331 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_331 $_332) $_332 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_331 $_332) $_329 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_331 $_332) $_330 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_332 $_330 (skolemFOFtoCNF_X4_1 $_331 $_332) \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_331) $_329 % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_331 $_332) \/ % 0.61/0.84 definitionFOFtoCNF_1 (skolemFOFtoCNF_X2 $_331) $_329 % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_331 $_332) % 0.61/0.84 |- big_f $_329 (skolemFOFtoCNF_X4_1 $_331 $_332) \/ % 0.61/0.84 big_f $_331 (skolemFOFtoCNF_X4 $_331 $_332) \/ % 0.61/0.84 big_f $_332 (skolemFOFtoCNF_X4 $_331 $_332) \/ % 0.61/0.84 big_f $_332 (skolemFOFtoCNF_X4_1 $_331 $_332) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_331) (skolemFOFtoCNF_X4_1 $_331 $_332) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_331 $_332) $_331 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_331 $_332) $_332 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_331 $_332) $_329 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_331 $_332) $_330 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_332 $_330 (skolemFOFtoCNF_X4_1 $_331 $_332) \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_331) $_329 % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_331 $_332) \/ % 0.61/0.84 definitionFOFtoCNF_1 $_332 $_330 (skolemFOFtoCNF_X4_1 $_331 $_332) % 0.61/0.84 |- big_f $_337 $_340 \/ big_f $_338 (skolemFOFtoCNF_X4_1 $_339 $_340) \/ % 0.61/0.84 big_f $_339 (skolemFOFtoCNF_X4 $_339 $_340) \/ big_f $_340 $_337 \/ % 0.61/0.84 big_f $_340 (skolemFOFtoCNF_X4 $_339 $_340) \/ % 0.61/0.84 big_f $_340 (skolemFOFtoCNF_X4_1 $_339 $_340) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_339) (skolemFOFtoCNF_X4_1 $_339 $_340) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_339 $_340) $_339 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_339 $_340) $_340 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_339 $_340) $_338 \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_339) $_338 % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_339 $_340) \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_339 $_340) $_337 $_340 % 0.61/0.84 |- big_f $_345 $_348 \/ big_f $_346 (skolemFOFtoCNF_X4_1 $_347 $_348) \/ % 0.61/0.84 big_f $_347 (skolemFOFtoCNF_X4 $_347 $_348) \/ big_f $_348 $_345 \/ % 0.61/0.84 big_f $_348 (skolemFOFtoCNF_X4 $_347 $_348) \/ % 0.61/0.84 big_f $_348 (skolemFOFtoCNF_X4_1 $_347 $_348) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_347) (skolemFOFtoCNF_X4_1 $_347 $_348) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_347 $_348) $_347 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_347 $_348) $_348 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_347 $_348) $_346 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_345 (skolemFOFtoCNF_X4_1 $_347 $_348) $_348 \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_347) $_346 % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_347 $_348) % 0.61/0.84 |- big_f $_361 $_364 \/ big_f $_362 (skolemFOFtoCNF_X4_1 $_363 $_364) \/ % 0.61/0.84 big_f $_363 (skolemFOFtoCNF_X4 $_363 $_364) \/ big_f $_364 $_361 \/ % 0.61/0.84 big_f $_364 (skolemFOFtoCNF_X4 $_363 $_364) \/ % 0.61/0.84 big_f $_364 (skolemFOFtoCNF_X4_1 $_363 $_364) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_363) (skolemFOFtoCNF_X4_1 $_363 $_364) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_363 $_364) $_363 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_363 $_364) $_364 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_363 $_364) $_362 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_361 (skolemFOFtoCNF_X4_1 $_363 $_364) $_364 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_362 (skolemFOFtoCNF_X2 $_363) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_363 $_364) % 0.61/0.84 |- big_f $_373 $_376 \/ big_f $_374 (skolemFOFtoCNF_X4_1 $_375 $_376) \/ % 0.61/0.84 big_f $_375 (skolemFOFtoCNF_X4 $_375 $_376) \/ big_f $_376 $_373 \/ % 0.61/0.84 big_f $_376 (skolemFOFtoCNF_X4 $_375 $_376) \/ % 0.61/0.84 big_f $_376 (skolemFOFtoCNF_X4_1 $_375 $_376) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_375) (skolemFOFtoCNF_X4_1 $_375 $_376) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_375 $_376) $_375 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_375 $_376) $_376 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_375 $_376) $_374 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_374 (skolemFOFtoCNF_X2 $_375) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_375 $_376) \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_375 $_376) $_373 $_376 % 0.61/0.84 |- big_f $_381 (skolemFOFtoCNF_X4_1 $_383 $_384) \/ % 0.61/0.84 big_f $_382 (skolemFOFtoCNF_X4_1 $_383 $_384) \/ % 0.61/0.84 big_f $_383 (skolemFOFtoCNF_X4 $_383 $_384) \/ % 0.61/0.84 big_f $_384 (skolemFOFtoCNF_X4 $_383 $_384) \/ % 0.61/0.84 big_f $_384 (skolemFOFtoCNF_X4_1 $_383 $_384) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_383) (skolemFOFtoCNF_X4_1 $_383 $_384) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_383 $_384) $_383 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_383 $_384) $_384 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_383 $_384) $_381 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_383 $_384) $_382 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_382 $_384 (skolemFOFtoCNF_X4_1 $_383 $_384) \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_383) $_381 % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_383 $_384) % 0.61/0.84 |- big_f $_389 (skolemFOFtoCNF_X4_1 $_391 $_392) \/ % 0.61/0.84 big_f $_390 (skolemFOFtoCNF_X4_1 $_391 $_392) \/ % 0.61/0.84 big_f $_391 (skolemFOFtoCNF_X4 $_391 $_392) \/ % 0.61/0.84 big_f $_392 (skolemFOFtoCNF_X4 $_391 $_392) \/ % 0.61/0.84 big_f $_392 (skolemFOFtoCNF_X4_1 $_391 $_392) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_391) (skolemFOFtoCNF_X4_1 $_391 $_392) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_391 $_392) $_391 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_391 $_392) $_392 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_391 $_392) $_389 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_391 $_392) $_390 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_389 (skolemFOFtoCNF_X2 $_391) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_391 $_392) \/ % 0.61/0.84 definitionFOFtoCNF_0 $_390 $_392 (skolemFOFtoCNF_X4_1 $_391 $_392) % 0.61/0.84 |- big_f $_397 (skolemFOFtoCNF_X4_1 $_399 $_400) \/ % 0.61/0.84 big_f $_398 (skolemFOFtoCNF_X4_1 $_399 $_400) \/ % 0.61/0.84 big_f $_399 (skolemFOFtoCNF_X4 $_399 $_400) \/ % 0.61/0.84 big_f $_400 (skolemFOFtoCNF_X4 $_399 $_400) \/ % 0.61/0.84 big_f $_400 (skolemFOFtoCNF_X4_1 $_399 $_400) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_399) (skolemFOFtoCNF_X4_1 $_399 $_400) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_399 $_400) $_399 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_399 $_400) $_400 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_399 $_400) $_397 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_399 $_400) $_398 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_397 (skolemFOFtoCNF_X2 $_399) % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_399 $_400) \/ % 0.61/0.84 definitionFOFtoCNF_0 $_400 $_398 (skolemFOFtoCNF_X4_1 $_399 $_400) % 0.61/0.84 |- big_f $_405 (skolemFOFtoCNF_X4_1 $_407 $_408) \/ % 0.61/0.84 big_f $_406 (skolemFOFtoCNF_X4_1 $_407 $_408) \/ % 0.61/0.84 big_f $_407 (skolemFOFtoCNF_X4 $_407 $_408) \/ % 0.61/0.84 big_f $_408 (skolemFOFtoCNF_X4 $_407 $_408) \/ % 0.61/0.84 big_f $_408 (skolemFOFtoCNF_X4_1 $_407 $_408) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_407) (skolemFOFtoCNF_X4_1 $_407 $_408) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_407 $_408) $_407 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_407 $_408) $_408 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_407 $_408) $_405 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_407 $_408) $_406 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_408 $_406 (skolemFOFtoCNF_X4_1 $_407 $_408) \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X2 $_407) $_405 % 0.61/0.84 (skolemFOFtoCNF_X4_1 $_407 $_408) % 0.61/0.84 |- big_f $_417 (skolemFOFtoCNF_X2 $_419) \/ % 0.61/0.84 big_f $_418 (skolemFOFtoCNF_X4_1 $_419 $_420) \/ % 0.61/0.84 big_f $_419 (skolemFOFtoCNF_X4 $_419 $_420) \/ % 0.61/0.84 big_f $_420 (skolemFOFtoCNF_X4 $_419 $_420) \/ % 0.61/0.84 big_f $_420 (skolemFOFtoCNF_X4_1 $_419 $_420) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_419) $_417 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_419) (skolemFOFtoCNF_X4_1 $_419 $_420) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_419 $_420) $_419 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_419 $_420) $_420 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_419 $_420) $_418 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_417 (skolemFOFtoCNF_X4_1 $_419 $_420) % 0.61/0.84 (skolemFOFtoCNF_X2 $_419) \/ % 0.61/0.84 definitionFOFtoCNF_0 $_418 $_420 (skolemFOFtoCNF_X4_1 $_419 $_420) % 0.61/0.84 |- big_f $_425 (skolemFOFtoCNF_X2 $_427) \/ % 0.61/0.84 big_f $_426 (skolemFOFtoCNF_X4_1 $_427 $_428) \/ % 0.61/0.84 big_f $_427 (skolemFOFtoCNF_X4 $_427 $_428) \/ % 0.61/0.84 big_f $_428 (skolemFOFtoCNF_X4 $_427 $_428) \/ % 0.61/0.84 big_f $_428 (skolemFOFtoCNF_X4_1 $_427 $_428) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_427) $_425 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_427) (skolemFOFtoCNF_X4_1 $_427 $_428) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_427 $_428) $_427 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_427 $_428) $_428 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_427 $_428) $_426 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_426 $_428 (skolemFOFtoCNF_X4_1 $_427 $_428) \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_427 $_428) $_425 % 0.61/0.84 (skolemFOFtoCNF_X2 $_427) % 0.61/0.84 |- big_f $_437 (skolemFOFtoCNF_X2 $_439) \/ % 0.61/0.84 big_f $_438 (skolemFOFtoCNF_X4_1 $_439 $_440) \/ % 0.61/0.84 big_f $_439 (skolemFOFtoCNF_X4 $_439 $_440) \/ % 0.61/0.84 big_f $_440 (skolemFOFtoCNF_X4 $_439 $_440) \/ % 0.61/0.84 big_f $_440 (skolemFOFtoCNF_X4_1 $_439 $_440) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_439) $_437 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_439) (skolemFOFtoCNF_X4_1 $_439 $_440) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_439 $_440) $_439 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_439 $_440) $_440 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_439 $_440) $_438 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_437 (skolemFOFtoCNF_X4_1 $_439 $_440) % 0.61/0.84 (skolemFOFtoCNF_X2 $_439) \/ % 0.61/0.84 definitionFOFtoCNF_0 $_440 $_438 (skolemFOFtoCNF_X4_1 $_439 $_440) % 0.61/0.84 |- big_f $_453 (skolemFOFtoCNF_X2 $_455) \/ % 0.61/0.84 big_f $_454 (skolemFOFtoCNF_X4_1 $_455 $_456) \/ % 0.61/0.84 big_f $_455 (skolemFOFtoCNF_X4 $_455 $_456) \/ % 0.61/0.84 big_f $_456 (skolemFOFtoCNF_X4 $_455 $_456) \/ % 0.61/0.84 big_f $_456 (skolemFOFtoCNF_X4_1 $_455 $_456) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_455) $_453 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X2 $_455) (skolemFOFtoCNF_X4_1 $_455 $_456) \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_455 $_456) $_455 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4 $_455 $_456) $_456 \/ % 0.61/0.84 big_f (skolemFOFtoCNF_X4_1 $_455 $_456) $_454 \/ % 0.61/0.84 definitionFOFtoCNF_0 $_456 $_454 (skolemFOFtoCNF_X4_1 $_455 $_456) \/ % 0.61/0.84 definitionFOFtoCNF_0 (skolemFOFtoCNF_X4_1 $_455 $_456) $_453 % 0.61/0.84 (skolemFOFtoCNF_X2 $_455) % 0.61/0.84 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.61/0.84 %------------------------------------------------------------------------------