%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : LCL665+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 12:43:11 PM UTC 2026 % Result : CounterSatisfiable 0.39s 0.64s % Output : Saturation 0.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL665+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : metis --show proof --show saturation %s % 0.08/0.35 % Computer : n011.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sat Sep 5 03:02:43 UTC 2026 % 0.08/0.35 % CPUTime : % 0.08/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.39/0.64 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.64 % 0.39/0.64 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.64 |- r1 $X $X % 0.39/0.64 |- ~p11 skolemFOFtoCNF_Y % 0.39/0.64 |- r1 skolemFOFtoCNF_X skolemFOFtoCNF_Y % 0.39/0.64 |- ~p12 skolemFOFtoCNF_Y_1 % 0.39/0.64 |- r1 skolemFOFtoCNF_X skolemFOFtoCNF_Y_1 % 0.39/0.64 |- ~p13 skolemFOFtoCNF_Y_2 % 0.39/0.64 |- r1 skolemFOFtoCNF_X skolemFOFtoCNF_Y_2 % 0.39/0.64 |- ~p15 skolemFOFtoCNF_Y_3 % 0.39/0.65 |- r1 skolemFOFtoCNF_X skolemFOFtoCNF_Y_3 % 0.39/0.65 |- ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ p22 $X % 0.39/0.65 |- ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ p24 $X % 0.39/0.65 |- ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ p25 $X % 0.39/0.65 |- ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ p26 $X % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_1 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p11 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p11 $Y \/ r1 $Y (skolemFOFtoCNF_X_1 $Y) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_2 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p11 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p11 $Y \/ r1 $Y (skolemFOFtoCNF_X_2 $Y) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_3 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p13 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p13 $Y \/ r1 $Y (skolemFOFtoCNF_X_3 $Y) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_4 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p13 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p13 $Y \/ r1 $Y (skolemFOFtoCNF_X_4 $Y) % 0.39/0.65 |- ~p22 (skolemFOFtoCNF_X_5 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p14 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p14 $Y \/ r1 $Y (skolemFOFtoCNF_X_5 $Y) % 0.39/0.65 |- ~p24 (skolemFOFtoCNF_X_6 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p14 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p14 $Y \/ r1 $Y (skolemFOFtoCNF_X_6 $Y) % 0.39/0.65 |- ~p26 (skolemFOFtoCNF_X_7 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p14 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p14 $Y \/ r1 $Y (skolemFOFtoCNF_X_7 $Y) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_8 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p15 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p15 $Y \/ r1 $Y (skolemFOFtoCNF_X_8 $Y) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_9 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p15 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p15 $Y \/ r1 $Y (skolemFOFtoCNF_X_9 $Y) % 0.39/0.65 |- ~p22 (skolemFOFtoCNF_X_10 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p16 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p16 $Y \/ r1 $Y (skolemFOFtoCNF_X_10 $Y) % 0.39/0.65 |- ~p24 (skolemFOFtoCNF_X_11 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p16 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p16 $Y \/ r1 $Y (skolemFOFtoCNF_X_11 $Y) % 0.39/0.65 |- ~p26 (skolemFOFtoCNF_X_12 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ p16 $Y % 0.39/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p16 $Y \/ r1 $Y (skolemFOFtoCNF_X_12 $Y) % 0.39/0.65 |- p22 skolemFOFtoCNF_X % 0.39/0.65 |- p24 skolemFOFtoCNF_X % 0.39/0.65 |- p25 skolemFOFtoCNF_X % 0.39/0.65 |- p26 skolemFOFtoCNF_X % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ p11 skolemFOFtoCNF_X % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_1) \/ p11 skolemFOFtoCNF_Y_1 % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_2) \/ p11 skolemFOFtoCNF_Y_2 % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_3) \/ p11 skolemFOFtoCNF_Y_3 % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ p11 skolemFOFtoCNF_X % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_1) \/ p11 skolemFOFtoCNF_Y_1 % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_2) \/ p11 skolemFOFtoCNF_Y_2 % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_3) \/ p11 skolemFOFtoCNF_Y_3 % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ p13 skolemFOFtoCNF_Y % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_1) \/ p13 skolemFOFtoCNF_Y_1 % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_2) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_3) \/ p13 skolemFOFtoCNF_Y_3 % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y) \/ p15 skolemFOFtoCNF_Y % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_1) \/ p15 skolemFOFtoCNF_Y_1 % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_2) \/ p15 skolemFOFtoCNF_Y_2 % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_3) % 0.39/0.65 |- p11 skolemFOFtoCNF_X \/ % 0.39/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.65 |- r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y) % 0.39/0.65 |- p11 skolemFOFtoCNF_Y_1 \/ % 0.39/0.65 r1 skolemFOFtoCNF_Y_1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_1) % 0.39/0.65 |- p11 skolemFOFtoCNF_Y_2 \/ % 0.39/0.65 r1 skolemFOFtoCNF_Y_2 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_2) % 0.39/0.65 |- p11 skolemFOFtoCNF_Y_3 \/ % 0.39/0.65 r1 skolemFOFtoCNF_Y_3 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_3) % 0.39/0.65 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.65 r1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.65 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ p13 skolemFOFtoCNF_Y % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_1) \/ p13 skolemFOFtoCNF_Y_1 % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_2) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_3) \/ p13 skolemFOFtoCNF_Y_3 % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ p15 skolemFOFtoCNF_Y % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_1) \/ p15 skolemFOFtoCNF_Y_1 % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_2) \/ p15 skolemFOFtoCNF_Y_2 % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_3) % 0.39/0.65 |- p11 skolemFOFtoCNF_X \/ % 0.39/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.65 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.65 r1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.65 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.65 |- r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y) % 0.39/0.65 |- p11 skolemFOFtoCNF_Y_1 \/ % 0.39/0.65 r1 skolemFOFtoCNF_Y_1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_1) % 0.39/0.65 |- p11 skolemFOFtoCNF_Y_2 \/ % 0.39/0.65 r1 skolemFOFtoCNF_Y_2 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_2) % 0.39/0.65 |- p11 skolemFOFtoCNF_Y_3 \/ % 0.39/0.65 r1 skolemFOFtoCNF_Y_3 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_3) % 0.39/0.65 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.65 r1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.65 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.65 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.65 r1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.65 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.65 |- p13 skolemFOFtoCNF_X \/ % 0.39/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.65 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.65 r1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.65 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.65 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.65 r1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.65 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.65 |- p13 skolemFOFtoCNF_Y \/ % 0.39/0.65 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.39/0.65 |- p13 skolemFOFtoCNF_Y_1 \/ % 0.39/0.65 r1 skolemFOFtoCNF_Y_1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_1) % 0.39/0.65 |- r1 skolemFOFtoCNF_Y_2 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_2) % 0.39/0.65 |- p13 skolemFOFtoCNF_Y_3 \/ % 0.39/0.65 r1 skolemFOFtoCNF_Y_3 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_3) % 0.39/0.65 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.65 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.65 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.65 |- p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.65 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.65 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p23 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.65 |- p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.65 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.65 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.65 |- ~p21 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) \/ % 0.39/0.65 p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.66 |- ~p23 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X % 0.39/0.66 |- ~p21 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X % 0.39/0.66 |- p13 skolemFOFtoCNF_X \/ % 0.39/0.66 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.66 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.66 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y \/ % 0.39/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y_1 \/ % 0.39/0.66 r1 skolemFOFtoCNF_Y_1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- r1 skolemFOFtoCNF_Y_2 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y_3 \/ % 0.39/0.66 r1 skolemFOFtoCNF_Y_3 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.66 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.66 |- p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.66 |- ~p23 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 |- ~p23 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 |- p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.66 |- ~p21 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 |- ~p21 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 |- ~p23 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X % 0.39/0.66 |- ~p21 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X % 0.39/0.66 |- p11 skolemFOFtoCNF_X \/ p24 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.66 |- p11 skolemFOFtoCNF_X \/ p24 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.66 |- p13 skolemFOFtoCNF_X \/ p24 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.66 |- p13 skolemFOFtoCNF_X \/ p24 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 |- p24 skolemFOFtoCNF_Y % 0.39/0.66 |- p24 skolemFOFtoCNF_Y_1 % 0.39/0.66 |- p24 skolemFOFtoCNF_Y_2 % 0.39/0.66 |- p24 skolemFOFtoCNF_Y_3 % 0.39/0.66 |- p24 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y) % 0.39/0.66 |- p24 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y \/ p24 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y \/ p24 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_1 \/ p24 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_1 \/ p24 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y_1 \/ p24 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y_1 \/ p24 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_2 \/ p24 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_2 \/ p24 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- p24 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- p24 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_3 \/ p24 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_3 \/ p24 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y_3 \/ p24 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y_3 \/ p24 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- ~r1 skolemFOFtoCNF_X $_19 \/ p24 $_19 % 0.39/0.66 |- p11 skolemFOFtoCNF_X \/ p26 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.66 |- p11 skolemFOFtoCNF_X \/ p26 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.66 |- p13 skolemFOFtoCNF_X \/ p26 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.66 |- p13 skolemFOFtoCNF_X \/ p26 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 |- p26 skolemFOFtoCNF_Y % 0.39/0.66 |- p26 skolemFOFtoCNF_Y_1 % 0.39/0.66 |- p26 skolemFOFtoCNF_Y_2 % 0.39/0.66 |- p26 skolemFOFtoCNF_Y_3 % 0.39/0.66 |- p26 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y) % 0.39/0.66 |- p26 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y \/ p26 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y \/ p26 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_1 \/ p26 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_1 \/ p26 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y_1 \/ p26 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y_1 \/ p26 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_2 \/ p26 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_2 \/ p26 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- p26 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- p26 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_3 \/ p26 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- p11 skolemFOFtoCNF_Y_3 \/ p26 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y_3 \/ p26 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- p13 skolemFOFtoCNF_Y_3 \/ p26 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- ~r1 skolemFOFtoCNF_X $_22 \/ p26 $_22 % 0.39/0.66 |- p14 skolemFOFtoCNF_X % 0.39/0.66 |- p14 skolemFOFtoCNF_Y % 0.39/0.66 |- p14 skolemFOFtoCNF_Y_1 % 0.39/0.66 |- p14 skolemFOFtoCNF_Y_2 % 0.39/0.66 |- p14 skolemFOFtoCNF_Y_3 % 0.39/0.66 |- p15 skolemFOFtoCNF_X \/ % 0.39/0.66 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.66 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.66 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.66 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.66 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.66 |- p15 skolemFOFtoCNF_Y \/ % 0.39/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y) % 0.39/0.66 |- p15 skolemFOFtoCNF_Y_1 \/ % 0.39/0.66 r1 skolemFOFtoCNF_Y_1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- p15 skolemFOFtoCNF_Y_2 \/ % 0.39/0.66 r1 skolemFOFtoCNF_Y_2 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- r1 skolemFOFtoCNF_Y_3 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- p26 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- p24 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_3) % 0.39/0.66 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.66 |- p15 skolemFOFtoCNF_X \/ p26 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.66 |- p15 skolemFOFtoCNF_X \/ p24 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.66 |- p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.66 |- p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.66 |- p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.66 |- ~p23 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.66 |- ~p23 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.66 |- p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.66 |- ~p21 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.66 |- ~p21 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.66 |- ~p23 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.66 |- ~p21 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) \/ % 0.39/0.66 p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.66 |- p15 skolemFOFtoCNF_Y \/ p26 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y) % 0.39/0.66 |- p15 skolemFOFtoCNF_Y \/ p24 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y) % 0.39/0.66 |- p15 skolemFOFtoCNF_Y_1 \/ p26 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- p15 skolemFOFtoCNF_Y_1 \/ p24 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_1) % 0.39/0.66 |- p15 skolemFOFtoCNF_Y_2 \/ p26 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- p15 skolemFOFtoCNF_Y_2 \/ p24 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_2) % 0.39/0.66 |- p15 skolemFOFtoCNF_X \/ % 0.39/0.66 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.66 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.66 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.66 r1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.66 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.67 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.67 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.67 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.67 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.67 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.67 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.67 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ % 0.39/0.67 r1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.67 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y \/ % 0.39/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_1 \/ % 0.39/0.67 r1 skolemFOFtoCNF_Y_1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_2 \/ % 0.39/0.67 r1 skolemFOFtoCNF_Y_2 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- r1 skolemFOFtoCNF_Y_3 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p26 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p24 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.39/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.67 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.39/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.67 |- p15 skolemFOFtoCNF_X \/ p26 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 |- p15 skolemFOFtoCNF_X \/ p24 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 |- p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.67 |- p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.67 |- p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.67 |- ~p23 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) \/ % 0.39/0.67 p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 |- ~p23 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) \/ % 0.39/0.67 p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.67 |- p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.67 |- ~p21 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) \/ % 0.39/0.67 p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 |- ~p21 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) \/ % 0.39/0.67 p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.67 |- ~p23 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) \/ % 0.39/0.67 p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.67 |- ~p21 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) \/ % 0.39/0.67 p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.67 |- p15 skolemFOFtoCNF_Y \/ p26 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y \/ p24 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_1 \/ p26 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_1 \/ p24 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_2 \/ p26 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_2 \/ p24 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p16 skolemFOFtoCNF_Y % 0.39/0.67 |- p16 skolemFOFtoCNF_Y_1 % 0.39/0.67 |- p16 skolemFOFtoCNF_Y_2 % 0.39/0.67 |- p16 skolemFOFtoCNF_Y_3 % 0.39/0.67 |- p16 skolemFOFtoCNF_X % 0.39/0.67 |- p11 skolemFOFtoCNF_X \/ p22 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.67 |- p11 skolemFOFtoCNF_X \/ p22 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.67 |- p13 skolemFOFtoCNF_X \/ p22 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.67 |- p13 skolemFOFtoCNF_X \/ p22 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.67 |- p15 skolemFOFtoCNF_X \/ p22 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.67 |- p15 skolemFOFtoCNF_X \/ p22 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 |- p22 skolemFOFtoCNF_Y % 0.39/0.67 |- p22 skolemFOFtoCNF_Y_1 % 0.39/0.67 |- p22 skolemFOFtoCNF_Y_2 % 0.39/0.67 |- p22 skolemFOFtoCNF_Y_3 % 0.39/0.67 |- p22 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y) % 0.39/0.67 |- p22 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y \/ p22 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y \/ p22 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y \/ p22 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y \/ p22 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_1 \/ p22 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_1 \/ p22 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y_1 \/ p22 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y_1 \/ p22 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_1 \/ p22 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_1 \/ p22 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_2 \/ p22 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_2 \/ p22 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p22 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p22 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_2 \/ p22 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_2 \/ p22 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_3 \/ p22 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_3 \/ p22 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y_3 \/ p22 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y_3 \/ p22 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p22 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p22 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- ~r1 skolemFOFtoCNF_X $_31 \/ p22 $_31 % 0.39/0.67 |- p11 skolemFOFtoCNF_X \/ p25 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.67 |- p11 skolemFOFtoCNF_X \/ p25 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.67 |- p13 skolemFOFtoCNF_X \/ p25 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.67 |- p13 skolemFOFtoCNF_X \/ p25 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.67 |- p15 skolemFOFtoCNF_X \/ p25 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.67 |- p15 skolemFOFtoCNF_X \/ p25 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.67 |- p25 skolemFOFtoCNF_Y % 0.39/0.67 |- p25 skolemFOFtoCNF_Y_1 % 0.39/0.67 |- p25 skolemFOFtoCNF_Y_2 % 0.39/0.67 |- p25 skolemFOFtoCNF_Y_3 % 0.39/0.67 |- p25 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y) % 0.39/0.67 |- p25 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y \/ p25 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y \/ p25 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y \/ p25 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y \/ p25 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_1 \/ p25 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_1 \/ p25 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y_1 \/ p25 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y_1 \/ p25 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_1 \/ p25 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_1 \/ p25 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_1) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_2 \/ p25 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_2 \/ p25 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p25 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p25 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_2 \/ p25 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p15 skolemFOFtoCNF_Y_2 \/ p25 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_2) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_3 \/ p25 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p11 skolemFOFtoCNF_Y_3 \/ p25 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y_3 \/ p25 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p13 skolemFOFtoCNF_Y_3 \/ p25 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p25 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- p25 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y_3) % 0.39/0.67 |- ~r1 skolemFOFtoCNF_X $_34 \/ p25 $_34 % 0.39/0.67 |- p11 skolemFOFtoCNF_X \/ p14 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.67 |- p11 skolemFOFtoCNF_X \/ p14 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.67 |- p13 skolemFOFtoCNF_X \/ p14 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.67 |- p13 skolemFOFtoCNF_X \/ p14 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.67 |- p11 skolemFOFtoCNF_X \/ p16 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) % 0.39/0.67 |- p11 skolemFOFtoCNF_X \/ p16 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) % 0.39/0.67 |- p13 skolemFOFtoCNF_X \/ p16 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p16 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) % 0.39/0.68 |- p15 skolemFOFtoCNF_X \/ p16 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.39/0.68 |- p15 skolemFOFtoCNF_X \/ p16 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.68 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_2 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 skolemFOFtoCNF_X \/ p11 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_1 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p25 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p22 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p26 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.68 |- p13 skolemFOFtoCNF_X \/ p13 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ % 0.39/0.68 p24 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X) \/ p13 skolemFOFtoCNF_X \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p14 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_9 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p15 skolemFOFtoCNF_X \/ p15 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p14 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_4 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p13 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_3 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p25 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p22 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p26 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 |- p11 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ p15 skolemFOFtoCNF_X \/ % 0.39/0.69 p24 (skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X)) % 0.39/0.69 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.69 %------------------------------------------------------------------------------