%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : LCL639+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n027.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:00 PM UTC 2026 % Result : CounterSatisfiable 0.40s 0.65s % Output : Saturation 0.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL639+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : metis --show proof --show saturation %s % 0.12/0.38 % Computer : n027.cluster.edu % 0.12/0.38 % Model : x86_64 x86_64 % 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.38 % Memory : 8046.5625MB % 0.12/0.38 % OS : Linux 6.8.0-71-generic % 0.12/0.38 % CPULimit : 300 % 0.12/0.38 % WCLimit : 300 % 0.12/0.38 % DateTime : Sat Sep 5 02:43:42 UTC 2026 % 0.12/0.38 % CPUTime : % 0.12/0.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.40/0.65 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.65 % 0.40/0.65 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.65 |- r1 skolemFOFtoCNF_X skolemFOFtoCNF_Y % 0.40/0.65 |- ~p1 skolemFOFtoCNF_X_1 % 0.40/0.65 |- r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X_1 % 0.40/0.65 |- r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X_2 % 0.40/0.65 |- ~r1 skolemFOFtoCNF_X_2 $Y \/ p1 $Y % 0.40/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ r1 $Y (skolemFOFtoCNF_X_3 $Y) % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_4 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 p1 (skolemFOFtoCNF_X_5 $Y) % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_4 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_5 $Y) % 0.40/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ p1 (skolemFOFtoCNF_X_5 $Y) \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_4 $Y) % 0.40/0.65 |- ~r1 skolemFOFtoCNF_X $Y \/ r1 $Y (skolemFOFtoCNF_X_4 $Y) \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_5 $Y) % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_6 $Y) \/ ~r1 $X $Y' \/ ~r1 $Y $X \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y' % 0.40/0.65 |- ~r1 $X $Y' \/ ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y' \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_6 $Y) % 0.40/0.65 |- ~r1 $X $Y'' \/ ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 p1 (skolemFOFtoCNF_X_8 $Y'') \/ r1 $Y (skolemFOFtoCNF_X_7 $Y) % 0.40/0.65 |- ~r1 $X $Y'' \/ ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_7 $Y) \/ r1 $Y'' (skolemFOFtoCNF_X_8 $Y'') % 0.40/0.65 |- ~p1 $Y' \/ ~r1 $X $Y'' \/ ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 ~r1 (skolemFOFtoCNF_X_7 $Y) $Y' \/ p1 (skolemFOFtoCNF_X_8 $Y'') % 0.40/0.65 |- ~p1 $Y' \/ ~r1 $X $Y'' \/ ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 ~r1 (skolemFOFtoCNF_X_7 $Y) $Y' \/ r1 $Y'' (skolemFOFtoCNF_X_8 $Y'') % 0.40/0.65 |- ~p1 $X' \/ ~p1 (skolemFOFtoCNF_X_9 $Y) \/ ~r1 $X $Y' \/ ~r1 $Y $X \/ % 0.40/0.65 ~r1 $Y' $X' \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y' % 0.40/0.65 |- ~p1 $X' \/ ~r1 $X $Y' \/ ~r1 $Y $X \/ ~r1 $Y' $X' \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y' \/ p1 (skolemFOFtoCNF_Y' $Y) % 0.40/0.65 |- ~p1 $X' \/ ~r1 $X $Y' \/ ~r1 $Y $X \/ ~r1 $Y' $X' \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y' \/ r1 $Y (skolemFOFtoCNF_X_9 $Y) % 0.40/0.65 |- ~p1 $X' \/ ~r1 $X $Y' \/ ~r1 $Y $X \/ ~r1 $Y' $X' \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y' \/ % 0.40/0.65 r1 (skolemFOFtoCNF_X_9 $Y) (skolemFOFtoCNF_Y' $Y) % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_10 $Y) \/ ~p1 (skolemFOFtoCNF_X_11 $Y'') \/ % 0.40/0.65 ~r1 $X $Y'' \/ ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y'' % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_10 $Y) \/ ~r1 $X $Y'' \/ ~r1 $Y $X \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y'' \/ r1 $Y'' (skolemFOFtoCNF_X_11 $Y'') % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_11 $Y'') \/ ~r1 $X $Y'' \/ ~r1 $Y $X \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y'' \/ r1 $Y (skolemFOFtoCNF_X_10 $Y) % 0.40/0.65 |- ~r1 $X $Y'' \/ ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y'' \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_10 $Y) \/ r1 $Y'' (skolemFOFtoCNF_X_11 $Y'') % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_11 $Y'') \/ ~r1 $X $Y'' \/ ~r1 $Y $X \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ ~r1 (skolemFOFtoCNF_X_10 $Y) $Y' \/ p1 $Y' \/ % 0.40/0.65 p1 $Y'' % 0.40/0.65 |- ~r1 $X $Y'' \/ ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 ~r1 (skolemFOFtoCNF_X_10 $Y) $Y' \/ p1 $Y' \/ p1 $Y'' \/ % 0.40/0.65 r1 $Y'' (skolemFOFtoCNF_X_11 $Y'') % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_6 $Y) \/ ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 p1 $Y % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_6 $Y) \/ ~r1 $Y skolemFOFtoCNF_X \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y % 0.40/0.65 |- ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_6 $Y) % 0.40/0.65 |- ~r1 $Y skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_6 $Y) % 0.40/0.65 |- ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 (skolemFOFtoCNF_X_8 $Y) \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_7 $Y) % 0.40/0.65 |- ~r1 $Y skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 p1 (skolemFOFtoCNF_X_8 $Y) \/ r1 $Y (skolemFOFtoCNF_X_7 $Y) % 0.40/0.65 |- ~r1 skolemFOFtoCNF_X $Y'' \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.65 p1 (skolemFOFtoCNF_X_8 $Y'') \/ % 0.40/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) % 0.40/0.65 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.65 p1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) \/ % 0.40/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) % 0.40/0.65 |- ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ r1 $Y (skolemFOFtoCNF_X_7 $Y) \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_8 $Y) % 0.40/0.65 |- ~r1 $Y skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_7 $Y) \/ r1 $Y (skolemFOFtoCNF_X_8 $Y) % 0.40/0.65 |- ~r1 skolemFOFtoCNF_X $Y'' \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.65 r1 $Y'' (skolemFOFtoCNF_X_8 $Y'') \/ % 0.40/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) % 0.40/0.65 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) \/ % 0.40/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X) % 0.40/0.65 |- ~p1 $Y' \/ ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 ~r1 (skolemFOFtoCNF_X_7 $Y) $Y' \/ p1 (skolemFOFtoCNF_X_8 $Y) % 0.40/0.65 |- ~p1 $Y' \/ ~r1 $Y (skolemFOFtoCNF_X_7 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 ~r1 (skolemFOFtoCNF_X_7 $Y) $Y' \/ p1 (skolemFOFtoCNF_X_8 $Y') % 0.40/0.65 |- ~p1 $Y' \/ ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 ~r1 (skolemFOFtoCNF_X_7 $Y) $Y' \/ r1 $Y (skolemFOFtoCNF_X_8 $Y) % 0.40/0.65 |- ~p1 $Y' \/ ~r1 $Y (skolemFOFtoCNF_X_7 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 ~r1 (skolemFOFtoCNF_X_7 $Y) $Y' \/ r1 $Y' (skolemFOFtoCNF_X_8 $Y') % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_10 $Y) \/ ~p1 (skolemFOFtoCNF_X_11 $Y) \/ % 0.40/0.65 ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_10 $Y) \/ ~p1 (skolemFOFtoCNF_X_11 $Y) \/ % 0.40/0.65 ~r1 $Y skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.65 ~p1 (skolemFOFtoCNF_X_11 $Y'') \/ ~r1 skolemFOFtoCNF_X $Y'' \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 $Y'' % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.65 ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X) \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_10 $Y) \/ ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 p1 $Y \/ r1 $Y (skolemFOFtoCNF_X_11 $Y) % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_10 $Y) \/ ~r1 $Y skolemFOFtoCNF_X \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y \/ r1 $Y (skolemFOFtoCNF_X_11 $Y) % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y'' \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.65 p1 $Y'' \/ r1 $Y'' (skolemFOFtoCNF_X_11 $Y'') % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X) % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_11 $Y) \/ ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 p1 $Y \/ r1 $Y (skolemFOFtoCNF_X_10 $Y) % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_11 $Y) \/ ~r1 $Y skolemFOFtoCNF_X \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y \/ r1 $Y (skolemFOFtoCNF_X_10 $Y) % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_11 $Y'') \/ ~r1 skolemFOFtoCNF_X $Y'' \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 $Y'' \/ % 0.40/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) % 0.40/0.65 |- ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X) \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) % 0.40/0.65 |- ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_10 $Y) \/ r1 $Y (skolemFOFtoCNF_X_11 $Y) % 0.40/0.65 |- ~r1 $Y skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y \/ % 0.40/0.65 r1 $Y (skolemFOFtoCNF_X_10 $Y) \/ r1 $Y (skolemFOFtoCNF_X_11 $Y) % 0.40/0.65 |- ~r1 skolemFOFtoCNF_X $Y'' \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.65 p1 $Y'' \/ r1 $Y'' (skolemFOFtoCNF_X_11 $Y'') \/ % 0.40/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) % 0.40/0.65 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.65 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X) % 0.40/0.65 |- ~p1 $X' \/ ~p1 (skolemFOFtoCNF_X_9 $Y) \/ ~r1 $Y $X' \/ ~r1 $Y $Y \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y % 0.40/0.65 |- ~p1 $X' \/ ~p1 (skolemFOFtoCNF_X_9 $Y) \/ ~r1 $Y $X' \/ % 0.40/0.65 ~r1 $Y skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y % 0.40/0.65 |- ~p1 $X' \/ ~p1 (skolemFOFtoCNF_X_9 $Y') \/ ~r1 $X' $Y' \/ ~r1 $Y' $X' \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y' \/ p1 $Y' % 0.40/0.65 |- ~p1 skolemFOFtoCNF_X \/ ~p1 (skolemFOFtoCNF_X_9 $Y') \/ % 0.40/0.65 ~r1 $Y' skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $Y' \/ p1 $Y' % 0.40/0.65 |- ~p1 $X' \/ ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ ~r1 $Y' $X' \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y' \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.65 p1 $Y' % 0.40/0.65 |- ~p1 $X' \/ ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $X' \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.65 p1 skolemFOFtoCNF_X % 0.40/0.65 |- ~p1 $Y \/ ~p1 (skolemFOFtoCNF_X_9 $Y) \/ ~r1 $X skolemFOFtoCNF_X \/ % 0.40/0.65 ~r1 $Y $X \/ ~r1 skolemFOFtoCNF_X $Y \/ p1 skolemFOFtoCNF_X % 0.40/0.65 |- ~p1 $X' \/ ~r1 $Y $X' \/ ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.65 p1 $Y \/ p1 (skolemFOFtoCNF_Y' $Y) % 0.40/0.65 |- ~p1 $X' \/ ~r1 $Y $X' \/ ~r1 $Y skolemFOFtoCNF_X \/ % 0.40/0.65 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y \/ p1 (skolemFOFtoCNF_Y' $Y) % 0.40/0.66 |- ~p1 $X' \/ ~r1 $X' $Y' \/ ~r1 $Y' $X' \/ ~r1 skolemFOFtoCNF_X $Y' \/ % 0.40/0.66 p1 $Y' \/ p1 (skolemFOFtoCNF_Y' $Y') % 0.40/0.66 |- ~p1 skolemFOFtoCNF_X \/ ~r1 $Y' skolemFOFtoCNF_X \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X $Y' \/ p1 $Y' \/ p1 (skolemFOFtoCNF_Y' $Y') % 0.40/0.66 |- ~p1 $X' \/ ~r1 $Y' $X' \/ ~r1 skolemFOFtoCNF_X $Y' \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 $Y' \/ % 0.40/0.66 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 $X' \/ ~r1 skolemFOFtoCNF_X $X' \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.66 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 $Y \/ ~r1 $X skolemFOFtoCNF_X \/ ~r1 $Y $X \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X $Y \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.66 p1 (skolemFOFtoCNF_Y' $Y) % 0.40/0.66 |- ~p1 $X' \/ ~r1 $Y $X' \/ ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.66 p1 $Y \/ r1 $Y (skolemFOFtoCNF_X_9 $Y) % 0.40/0.66 |- ~p1 $X' \/ ~r1 $Y $X' \/ ~r1 $Y skolemFOFtoCNF_X \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y \/ r1 $Y (skolemFOFtoCNF_X_9 $Y) % 0.40/0.66 |- ~p1 $X' \/ ~r1 $X' $Y' \/ ~r1 $Y' $X' \/ ~r1 skolemFOFtoCNF_X $Y' \/ % 0.40/0.66 p1 $Y' \/ r1 $Y' (skolemFOFtoCNF_X_9 $Y') % 0.40/0.66 |- ~p1 skolemFOFtoCNF_X \/ ~r1 $Y' skolemFOFtoCNF_X \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X $Y' \/ p1 $Y' \/ r1 $Y' (skolemFOFtoCNF_X_9 $Y') % 0.40/0.66 |- ~p1 $X' \/ ~r1 $Y' $X' \/ ~r1 skolemFOFtoCNF_X $Y' \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 $Y' \/ % 0.40/0.66 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 $X' \/ ~r1 skolemFOFtoCNF_X $X' \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.66 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 $Y \/ ~r1 $X skolemFOFtoCNF_X \/ ~r1 $Y $X \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X $Y \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.66 r1 $Y (skolemFOFtoCNF_X_9 $Y) % 0.40/0.66 |- ~p1 $X' \/ ~r1 $Y $X' \/ ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.66 p1 $Y \/ r1 (skolemFOFtoCNF_X_9 $Y) (skolemFOFtoCNF_Y' $Y) % 0.40/0.66 |- ~p1 $X' \/ ~r1 $Y $X' \/ ~r1 $Y skolemFOFtoCNF_X \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X $Y \/ p1 $Y \/ % 0.40/0.66 r1 (skolemFOFtoCNF_X_9 $Y) (skolemFOFtoCNF_Y' $Y) % 0.40/0.66 |- ~p1 $X' \/ ~r1 $X' $Y' \/ ~r1 $Y' $X' \/ ~r1 skolemFOFtoCNF_X $Y' \/ % 0.40/0.66 p1 $Y' \/ r1 (skolemFOFtoCNF_X_9 $Y') (skolemFOFtoCNF_Y' $Y') % 0.40/0.66 |- ~p1 skolemFOFtoCNF_X \/ ~r1 $Y' skolemFOFtoCNF_X \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X $Y' \/ p1 $Y' \/ % 0.40/0.66 r1 (skolemFOFtoCNF_X_9 $Y') (skolemFOFtoCNF_Y' $Y') % 0.40/0.66 |- ~p1 $X' \/ ~r1 $Y' $X' \/ ~r1 skolemFOFtoCNF_X $Y' \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 $Y' \/ % 0.40/0.66 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.40/0.66 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 $X' \/ ~r1 skolemFOFtoCNF_X $X' \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.66 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.40/0.66 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 $Y \/ ~r1 $X skolemFOFtoCNF_X \/ ~r1 $Y $X \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X $Y \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.66 r1 (skolemFOFtoCNF_X_9 $Y) (skolemFOFtoCNF_Y' $Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_11 $Y) \/ ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.66 ~r1 (skolemFOFtoCNF_X_10 $Y) $Y' \/ p1 $Y \/ p1 $Y' % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_11 $Y') \/ ~r1 $Y (skolemFOFtoCNF_X_10 $Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X $Y \/ ~r1 (skolemFOFtoCNF_X_10 $Y) $Y' \/ p1 $Y' % 0.40/0.66 |- ~r1 $Y $Y \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.66 ~r1 (skolemFOFtoCNF_X_10 $Y) $Y' \/ p1 $Y \/ p1 $Y' \/ % 0.40/0.66 r1 $Y (skolemFOFtoCNF_X_11 $Y) % 0.40/0.66 |- ~r1 $Y (skolemFOFtoCNF_X_10 $Y) \/ ~r1 skolemFOFtoCNF_X $Y \/ % 0.40/0.66 ~r1 (skolemFOFtoCNF_X_10 $Y) $Y' \/ p1 $Y' \/ % 0.40/0.66 r1 $Y' (skolemFOFtoCNF_X_11 $Y') % 0.40/0.66 |- r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.66 p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) % 0.40/0.66 |- p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.66 |- r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.66 p1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y) \/ % 0.40/0.66 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) % 0.40/0.66 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.66 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ ~p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X % 0.40/0.66 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.66 p1 skolemFOFtoCNF_X \/ p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.66 ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y % 0.40/0.66 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.66 p1 skolemFOFtoCNF_X \/ % 0.40/0.66 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_11 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.66 p1 skolemFOFtoCNF_X \/ % 0.40/0.66 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.40/0.66 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) % 0.40/0.66 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_11 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_6 $_51) \/ ~r1 $_51 skolemFOFtoCNF_X \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X $_51 \/ p1 skolemFOFtoCNF_Y % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_6 $_51) \/ ~r1 $_51 skolemFOFtoCNF_Y \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X $_51 % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_6 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X_1 $_52 \/ p1 $_52 % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_6 skolemFOFtoCNF_X) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 skolemFOFtoCNF_X_2 \/ ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X_1) \/ ~p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X_1 \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X_2) \/ ~p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X_2 \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_X_2 % 0.40/0.66 |- ~p1 skolemFOFtoCNF_X_2 \/ ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ ~p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ % 0.40/0.66 p1 skolemFOFtoCNF_Y \/ p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X_1 \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ % 0.40/0.66 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X_1) % 0.40/0.66 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X_2 \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_X_2 \/ % 0.40/0.66 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X_2) % 0.40/0.66 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.66 p1 skolemFOFtoCNF_Y \/ p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_X \/ % 0.40/0.66 p1 skolemFOFtoCNF_X \/ p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.66 |- ~r1 $_77 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_77 \/ % 0.40/0.66 p1 skolemFOFtoCNF_Y \/ r1 $_77 (skolemFOFtoCNF_X_6 $_77) % 0.40/0.66 |- ~r1 $_77 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_77 \/ % 0.40/0.66 r1 $_77 (skolemFOFtoCNF_X_6 $_77) % 0.40/0.66 |- ~r1 skolemFOFtoCNF_X_1 $_78 \/ p1 $_78 \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_6 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.66 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_6 skolemFOFtoCNF_X) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ % 0.40/0.66 p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.66 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.66 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X_1 \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ % 0.40/0.66 r1 skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X_1) % 0.40/0.66 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X_2 \/ % 0.40/0.66 ~r1 skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_X_2 \/ % 0.40/0.66 r1 skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X_2) % 0.40/0.67 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_X \/ % 0.40/0.67 p1 skolemFOFtoCNF_X \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~r1 $_95 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_95 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 $_95 (skolemFOFtoCNF_X_7 $_95) % 0.40/0.67 |- ~r1 $_95 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_95 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X_1) \/ % 0.40/0.67 r1 $_95 (skolemFOFtoCNF_X_7 $_95) % 0.40/0.67 |- ~r1 $_95 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_95 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X_2) \/ % 0.40/0.67 r1 $_95 (skolemFOFtoCNF_X_7 $_95) % 0.40/0.67 |- ~r1 $_95 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_95 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 r1 $_95 (skolemFOFtoCNF_X_7 $_95) % 0.40/0.67 |- ~r1 $_95 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_95 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 r1 $_95 (skolemFOFtoCNF_X_7 $_95) % 0.40/0.67 |- ~r1 $_95 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_95 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 r1 $_95 (skolemFOFtoCNF_X_7 $_95) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X_1 $_96 \/ p1 (skolemFOFtoCNF_X_8 $_96) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_7 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X_2 $_96 \/ p1 (skolemFOFtoCNF_X_8 $_96) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_7 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X_1) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X_2) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ % 0.40/0.67 p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X_1 \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X_1) % 0.40/0.67 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X_1) % 0.40/0.67 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X_2 \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X_2 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_X_2 \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X_2) % 0.40/0.67 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X_2) % 0.40/0.67 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.40/0.67 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.40/0.67 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_X) % 0.40/0.67 (skolemFOFtoCNF_Y' skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_X \/ % 0.40/0.67 p1 skolemFOFtoCNF_X \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.67 |- ~r1 $_118 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_118 \/ % 0.40/0.67 r1 $_118 (skolemFOFtoCNF_X_7 $_118) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_8 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~r1 $_118 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_118 \/ % 0.40/0.67 r1 $_118 (skolemFOFtoCNF_X_7 $_118) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X_1) % 0.40/0.67 |- ~r1 $_118 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_118 \/ % 0.40/0.67 r1 $_118 (skolemFOFtoCNF_X_7 $_118) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X_2) % 0.40/0.67 |- ~r1 $_118 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_118 \/ % 0.40/0.67 r1 $_118 (skolemFOFtoCNF_X_7 $_118) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y)) % 0.40/0.67 |- ~r1 $_118 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_118 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 $_118 (skolemFOFtoCNF_X_7 $_118) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y)) % 0.40/0.67 |- ~r1 $_118 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_118 \/ % 0.40/0.67 r1 $_118 (skolemFOFtoCNF_X_7 $_118) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X_1 $_119 \/ r1 $_119 (skolemFOFtoCNF_X_8 $_119) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_7 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X_2 $_119 \/ r1 $_119 (skolemFOFtoCNF_X_8 $_119) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_7 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X_1) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_8 skolemFOFtoCNF_X_2) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y)) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y)) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_7 skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_8 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 $_129) \/ % 0.40/0.67 ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~r1 $_129 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_129 \/ % 0.40/0.67 p1 skolemFOFtoCNF_Y % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 $_129) \/ % 0.40/0.67 ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_1) \/ % 0.40/0.67 ~r1 $_129 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_129 % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 $_129) \/ % 0.40/0.67 ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_2) \/ % 0.40/0.67 ~r1 $_129 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_129 \/ % 0.40/0.67 p1 skolemFOFtoCNF_X_2 % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 $_129) \/ % 0.40/0.67 ~p1 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 ~r1 $_129 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_129 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 $_129) \/ % 0.40/0.67 ~p1 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 ~r1 $_129 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_129 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~p1 (skolemFOFtoCNF_X_11 $_130) \/ ~r1 skolemFOFtoCNF_X_1 $_130 \/ % 0.40/0.67 p1 $_130 % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.67 ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_1) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.67 ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_2) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X_2 % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 $_138) \/ ~r1 $_138 skolemFOFtoCNF_X \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X $_138 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_11 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 $_138) \/ ~r1 $_138 skolemFOFtoCNF_Y \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X $_138 \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_1) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 $_138) \/ ~r1 $_138 skolemFOFtoCNF_Y \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X $_138 \/ p1 skolemFOFtoCNF_X_2 \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_2) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 $_138) \/ ~r1 $_138 skolemFOFtoCNF_Y \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X $_138 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y)) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 $_138) \/ ~r1 $_138 skolemFOFtoCNF_Y \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X $_138 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y)) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X_1 $_139 \/ p1 $_139 \/ % 0.40/0.67 r1 $_139 (skolemFOFtoCNF_X_11 $_139) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_1) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X_2 \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_2) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y)) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y)) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_Y) \/ % 0.40/0.67 ~r1 $_147 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_147 \/ % 0.40/0.67 p1 skolemFOFtoCNF_Y \/ r1 $_147 (skolemFOFtoCNF_X_10 $_147) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_1) \/ % 0.40/0.67 ~r1 $_147 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_147 \/ % 0.40/0.67 r1 $_147 (skolemFOFtoCNF_X_10 $_147) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_2) \/ % 0.40/0.67 ~r1 $_147 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_147 \/ % 0.40/0.67 p1 skolemFOFtoCNF_X_2 \/ r1 $_147 (skolemFOFtoCNF_X_10 $_147) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 ~r1 $_147 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_147 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 $_147 (skolemFOFtoCNF_X_10 $_147) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y)) \/ % 0.40/0.67 ~r1 $_147 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_147 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 $_147 (skolemFOFtoCNF_X_10 $_147) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_11 $_148) \/ ~r1 skolemFOFtoCNF_X_1 $_148 \/ % 0.40/0.67 p1 $_148 \/ r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_10 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_1) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) % 0.40/0.67 |- ~p1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_2) \/ % 0.40/0.67 ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X_2 \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) % 0.40/0.67 |- ~r1 $_156 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_156 \/ % 0.40/0.67 p1 skolemFOFtoCNF_Y \/ r1 $_156 (skolemFOFtoCNF_X_10 $_156) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_11 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~r1 $_156 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_156 \/ % 0.40/0.67 r1 $_156 (skolemFOFtoCNF_X_10 $_156) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_1) % 0.40/0.67 |- ~r1 $_156 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_156 \/ % 0.40/0.67 p1 skolemFOFtoCNF_X_2 \/ r1 $_156 (skolemFOFtoCNF_X_10 $_156) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_2) % 0.40/0.67 |- ~r1 $_156 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_156 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 $_156 (skolemFOFtoCNF_X_10 $_156) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y)) % 0.40/0.67 |- ~r1 $_156 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_156 \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 $_156 (skolemFOFtoCNF_X_10 $_156) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y)) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X_1 $_157 \/ p1 $_157 \/ % 0.40/0.67 r1 $_157 (skolemFOFtoCNF_X_11 $_157) \/ % 0.40/0.67 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_10 skolemFOFtoCNF_Y) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_1 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_1) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ p1 skolemFOFtoCNF_X_2 \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X_2 (skolemFOFtoCNF_X_11 skolemFOFtoCNF_X_2) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y)) % 0.40/0.67 |- ~r1 skolemFOFtoCNF_X skolemFOFtoCNF_X \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.67 p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.67 r1 skolemFOFtoCNF_X (skolemFOFtoCNF_X_10 skolemFOFtoCNF_X) \/ % 0.40/0.67 r1 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.67 (skolemFOFtoCNF_X_11 (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y)) % 0.40/0.68 |- ~p1 $_173 \/ ~p1 (skolemFOFtoCNF_X_9 $_174) \/ % 0.40/0.68 ~r1 $_174 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_174 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 $_173 % 0.40/0.68 |- ~p1 $_173 \/ ~p1 (skolemFOFtoCNF_X_9 $_174) \/ % 0.40/0.68 ~r1 $_174 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_174 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_2 $_173 \/ p1 skolemFOFtoCNF_X_2 % 0.40/0.68 |- ~p1 $_173 \/ ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_175 $_173 \/ ~r1 skolemFOFtoCNF_X_1 $_175 \/ p1 $_175 % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_9 $_174) \/ ~p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 ~r1 $_172 skolemFOFtoCNF_X \/ ~r1 $_174 $_172 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_174 \/ p1 skolemFOFtoCNF_X % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~p1 (skolemFOFtoCNF_X_9 $_174) \/ % 0.40/0.68 ~r1 $_172 skolemFOFtoCNF_Y \/ ~r1 $_174 $_172 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_174 \/ p1 skolemFOFtoCNF_Y % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~p1 (skolemFOFtoCNF_X_9 $_174) \/ ~r1 $_172 skolemFOFtoCNF_Y \/ % 0.40/0.68 ~r1 $_174 $_172 \/ ~r1 skolemFOFtoCNF_X $_174 \/ p1 skolemFOFtoCNF_Y % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~p1 (skolemFOFtoCNF_X_9 $_174) \/ ~r1 $_172 skolemFOFtoCNF_Y \/ % 0.40/0.68 ~r1 $_174 $_172 \/ ~r1 skolemFOFtoCNF_X $_174 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~p1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~p1 (skolemFOFtoCNF_X_9 $_185) \/ % 0.40/0.68 ~r1 $_185 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_185 \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~p1 (skolemFOFtoCNF_X_9 $_188) \/ ~r1 $_188 skolemFOFtoCNF_X \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_188 \/ p1 skolemFOFtoCNF_Y % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~p1 (skolemFOFtoCNF_X_9 $_191) \/ ~r1 $_191 skolemFOFtoCNF_X \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_191 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 $_194 \/ ~r1 $_195 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_195 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 $_194 \/ p1 (skolemFOFtoCNF_Y' $_195) % 0.40/0.68 |- ~p1 $_194 \/ ~r1 $_195 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_195 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_2 $_194 \/ p1 skolemFOFtoCNF_X_2 \/ % 0.40/0.68 p1 (skolemFOFtoCNF_Y' $_195) % 0.40/0.68 |- ~p1 $_194 \/ ~r1 $_196 $_194 \/ ~r1 skolemFOFtoCNF_X_1 $_196 \/ % 0.40/0.68 p1 $_196 \/ p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 $_193 skolemFOFtoCNF_X \/ ~r1 $_195 $_193 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_195 \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.68 p1 (skolemFOFtoCNF_Y' $_195) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 $_193 skolemFOFtoCNF_Y \/ % 0.40/0.68 ~r1 $_195 $_193 \/ ~r1 skolemFOFtoCNF_X $_195 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 (skolemFOFtoCNF_Y' $_195) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_193 skolemFOFtoCNF_Y \/ ~r1 $_195 $_193 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_195 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 (skolemFOFtoCNF_Y' $_195) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_193 skolemFOFtoCNF_Y \/ ~r1 $_195 $_193 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_195 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 (skolemFOFtoCNF_Y' $_195) \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 $_206 skolemFOFtoCNF_X \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_206 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 (skolemFOFtoCNF_Y' $_206) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_209 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_209 \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ p1 (skolemFOFtoCNF_Y' $_209) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_212 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_212 \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ p1 (skolemFOFtoCNF_Y' $_212) \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 $_215 \/ ~r1 $_216 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_216 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 $_215 \/ r1 $_216 (skolemFOFtoCNF_X_9 $_216) % 0.40/0.68 |- ~p1 $_215 \/ ~r1 $_216 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_216 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_2 $_215 \/ p1 skolemFOFtoCNF_X_2 \/ % 0.40/0.68 r1 $_216 (skolemFOFtoCNF_X_9 $_216) % 0.40/0.68 |- ~p1 $_215 \/ ~r1 $_217 $_215 \/ ~r1 skolemFOFtoCNF_X_1 $_217 \/ % 0.40/0.68 p1 $_217 \/ r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 $_214 skolemFOFtoCNF_X \/ ~r1 $_216 $_214 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_216 \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.68 r1 $_216 (skolemFOFtoCNF_X_9 $_216) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 $_214 skolemFOFtoCNF_Y \/ % 0.40/0.68 ~r1 $_216 $_214 \/ ~r1 skolemFOFtoCNF_X $_216 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 $_216 (skolemFOFtoCNF_X_9 $_216) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_214 skolemFOFtoCNF_Y \/ ~r1 $_216 $_214 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_216 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 $_216 (skolemFOFtoCNF_X_9 $_216) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_214 skolemFOFtoCNF_Y \/ ~r1 $_216 $_214 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_216 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 $_216 (skolemFOFtoCNF_X_9 $_216) \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 $_227 skolemFOFtoCNF_X \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_227 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 $_227 (skolemFOFtoCNF_X_9 $_227) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_230 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_230 \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ r1 $_230 (skolemFOFtoCNF_X_9 $_230) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_233 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_233 \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ r1 $_233 (skolemFOFtoCNF_X_9 $_233) \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 $_240 \/ ~r1 $_241 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_241 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 $_240 \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 $_241) (skolemFOFtoCNF_Y' $_241) % 0.40/0.68 |- ~p1 $_240 \/ ~r1 $_241 skolemFOFtoCNF_Y \/ ~r1 skolemFOFtoCNF_X $_241 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_2 $_240 \/ p1 skolemFOFtoCNF_X_2 \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 $_241) (skolemFOFtoCNF_Y' $_241) % 0.40/0.68 |- ~p1 $_240 \/ ~r1 $_242 $_240 \/ ~r1 skolemFOFtoCNF_X_1 $_242 \/ % 0.40/0.68 p1 $_242 \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.68 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_Y \/ ~r1 $_239 skolemFOFtoCNF_X \/ ~r1 $_241 $_239 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_241 \/ p1 skolemFOFtoCNF_X \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 $_241) (skolemFOFtoCNF_Y' $_241) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 $_239 skolemFOFtoCNF_Y \/ % 0.40/0.68 ~r1 $_241 $_239 \/ ~r1 skolemFOFtoCNF_X $_241 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 $_241) (skolemFOFtoCNF_Y' $_241) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_239 skolemFOFtoCNF_Y \/ ~r1 $_241 $_239 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_241 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 $_241) (skolemFOFtoCNF_Y' $_241) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_239 skolemFOFtoCNF_Y \/ ~r1 $_241 $_239 \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_241 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 $_241) (skolemFOFtoCNF_Y' $_241) \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_Y skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.68 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.68 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.68 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X_1 skolemFOFtoCNF_Y \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 skolemFOFtoCNF_Y) % 0.40/0.68 (skolemFOFtoCNF_Y' skolemFOFtoCNF_Y) \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.68 |- ~p1 skolemFOFtoCNF_X_2 \/ ~r1 $_252 skolemFOFtoCNF_X \/ % 0.40/0.68 ~r1 skolemFOFtoCNF_X $_252 \/ p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 $_252) (skolemFOFtoCNF_Y' $_252) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_3 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_255 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_255 \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 $_255) (skolemFOFtoCNF_Y' $_255) % 0.40/0.68 |- ~p1 (skolemFOFtoCNF_X_5 skolemFOFtoCNF_Y) \/ % 0.40/0.68 ~r1 $_258 skolemFOFtoCNF_X \/ ~r1 skolemFOFtoCNF_X $_258 \/ % 0.40/0.68 p1 skolemFOFtoCNF_Y \/ % 0.40/0.68 r1 (skolemFOFtoCNF_X_9 $_258) (skolemFOFtoCNF_Y' $_258) \/ % 0.40/0.68 r1 skolemFOFtoCNF_Y (skolemFOFtoCNF_X_4 skolemFOFtoCNF_Y) % 0.40/0.68 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.68 %------------------------------------------------------------------------------