Metis---2.4.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : KRS033+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n017.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 600s
% DateTime : Sun Jul 17 03:18:29 EDT 2022

% Result   : Satisfiable 32.27s 32.49s
% Output   : Saturation 32.27s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : KRS033+1 : TPTP v8.1.0. Released v3.1.0.
% 0.07/0.13  % Command  : metis --show proof --show saturation %s
% 0.12/0.34  % Computer : n017.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 600
% 0.12/0.34  % DateTime : Tue Jun  7 18:47:32 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 0.12/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 32.27/32.49  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 32.27/32.49  
% 32.27/32.49  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 32.27/32.49  |- ~cowlNothing $X
% 32.27/32.49  |- cowlThing $X
% 32.27/32.49  |- ~xsd_integer $X \/ ~xsd_string $X
% 32.27/32.49  |- xsd_integer $X \/ xsd_string $X
% 32.27/32.49  |- ~cSatisfiable $X \/ cp (skolemFOFtoCNF_Y $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ cp (skolemFOFtoCNF_Y_1 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ cp (skolemFOFtoCNF_Y_2 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ cp (skolemFOFtoCNF_Y_3 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ cp1 (skolemFOFtoCNF_Y_3 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ cp1 (skolemFOFtoCNF_Y_7 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ cp2 (skolemFOFtoCNF_Y_2 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ cp2 (skolemFOFtoCNF_Y_6 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ cp3 (skolemFOFtoCNF_Y_1 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ cp3 (skolemFOFtoCNF_Y_5 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ cp4 (skolemFOFtoCNF_Y $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ cp4 (skolemFOFtoCNF_Y_4 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y_1 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y_2 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y_3 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y_4 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y_5 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y_6 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y_7 $X)
% 32.27/32.49  |- ~cSatisfiable $X \/ ~rr $X $Y0 \/ ~rr $X $Y1 \/ ~rr $X $Y2 \/
% 32.27/32.49     ~rr $X $Y3 \/ ~rr $X $Y4 \/ $Y0 = $Y1 \/ $Y0 = $Y2 \/ $Y0 = $Y3 \/
% 32.27/32.49     $Y0 = $Y4 \/ $Y1 = $Y2 \/ $Y1 = $Y3 \/ $Y1 = $Y4 \/ $Y2 = $Y3 \/
% 32.27/32.49     $Y2 = $Y4 \/ $Y3 = $Y4
% 32.27/32.49  |- ~cp1 $X \/ ~cp2 $X
% 32.27/32.49  |- ~cp1 $X \/ ~cp3 $X
% 32.27/32.49  |- ~cp1 $X \/ ~cp4 $X
% 32.27/32.49  |- ~cp1 $X \/ ~cp5 $X
% 32.27/32.49  |- ~cp2 $X \/ ~cp3 $X
% 32.27/32.49  |- ~cp2 $X \/ ~cp4 $X
% 32.27/32.49  |- ~cp2 $X \/ ~cp5 $X
% 32.27/32.49  |- ~cp3 $X \/ ~cp4 $X
% 32.27/32.49  |- ~cp3 $X \/ ~cp5 $X
% 32.27/32.49  |- ~cp4 $X \/ ~cp5 $X
% 32.27/32.49  |- cSatisfiable i2003_11_14_17_15_37698
% 32.27/32.49  |- ~(skolemFOFtoCNF_Y0 $X = skolemFOFtoCNF_Y1 $X) \/ ~cp $Y'''' \/
% 32.27/32.49     ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/ ~cp1 $Y'''' \/
% 32.27/32.49     ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/ ~rr $X $Y'''' \/
% 32.27/32.49     ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/ ~rr $X $Y''''''' \/ cSatisfiable $X
% 32.27/32.49  |- ~(skolemFOFtoCNF_Y0 $X = skolemFOFtoCNF_Y2 $X) \/ ~cp $Y'''' \/
% 32.27/32.49     ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/ ~cp1 $Y'''' \/
% 32.27/32.49     ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/ ~rr $X $Y'''' \/
% 32.27/32.49     ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/ ~rr $X $Y''''''' \/ cSatisfiable $X
% 32.27/32.49  |- ~(skolemFOFtoCNF_Y0 $X = skolemFOFtoCNF_Y3 $X) \/ ~cp $Y'''' \/
% 32.27/32.49     ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/ ~cp1 $Y'''' \/
% 32.27/32.49     ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/ ~rr $X $Y'''' \/
% 32.27/32.49     ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/ ~rr $X $Y''''''' \/ cSatisfiable $X
% 32.27/32.49  |- ~(skolemFOFtoCNF_Y0 $X = skolemFOFtoCNF_Y4 $X) \/ ~cp $Y'''' \/
% 32.27/32.49     ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/ ~cp1 $Y'''' \/
% 32.27/32.49     ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/ ~rr $X $Y'''' \/
% 32.27/32.49     ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/ ~rr $X $Y''''''' \/ cSatisfiable $X
% 32.27/32.49  |- ~(skolemFOFtoCNF_Y1 $X = skolemFOFtoCNF_Y2 $X) \/ ~cp $Y'''' \/
% 32.27/32.49     ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/ ~cp1 $Y'''' \/
% 32.27/32.49     ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/ ~rr $X $Y'''' \/
% 32.27/32.49     ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/ ~rr $X $Y''''''' \/ cSatisfiable $X
% 32.27/32.49  |- ~(skolemFOFtoCNF_Y1 $X = skolemFOFtoCNF_Y3 $X) \/ ~cp $Y'''' \/
% 32.27/32.49     ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/ ~cp1 $Y'''' \/
% 32.27/32.49     ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/ ~rr $X $Y'''' \/
% 32.27/32.49     ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/ ~rr $X $Y''''''' \/ cSatisfiable $X
% 32.27/32.49  |- ~(skolemFOFtoCNF_Y1 $X = skolemFOFtoCNF_Y4 $X) \/ ~cp $Y'''' \/
% 32.27/32.49     ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/ ~cp1 $Y'''' \/
% 32.27/32.49     ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/ ~rr $X $Y'''' \/
% 32.27/32.49     ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/ ~rr $X $Y''''''' \/ cSatisfiable $X
% 32.27/32.49  |- ~(skolemFOFtoCNF_Y2 $X = skolemFOFtoCNF_Y3 $X) \/ ~cp $Y'''' \/
% 32.27/32.49     ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/ ~cp1 $Y'''' \/
% 32.27/32.49     ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/ ~rr $X $Y'''' \/
% 32.27/32.49     ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/ ~rr $X $Y''''''' \/ cSatisfiable $X
% 32.27/32.49  |- ~(skolemFOFtoCNF_Y2 $X = skolemFOFtoCNF_Y4 $X) \/ ~cp $Y'''' \/
% 32.27/32.49     ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/ ~cp1 $Y'''' \/
% 32.27/32.49     ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/ ~rr $X $Y'''' \/
% 32.27/32.49     ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/ ~rr $X $Y''''''' \/ cSatisfiable $X
% 32.27/32.49  |- ~(skolemFOFtoCNF_Y3 $X = skolemFOFtoCNF_Y4 $X) \/ ~cp $Y'''' \/
% 32.27/32.49     ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/ ~cp1 $Y'''' \/
% 32.27/32.49     ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/ ~rr $X $Y'''' \/
% 32.27/32.49     ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/ ~rr $X $Y''''''' \/ cSatisfiable $X
% 32.27/32.49  |- ~cp $Y'''' \/ ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/
% 32.27/32.49     ~cp1 $Y'''' \/ ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/
% 32.27/32.49     ~rr $X $Y'''' \/ ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/
% 32.27/32.49     ~rr $X $Y''''''' \/ cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y0 $X)
% 32.27/32.50  |- ~cp $Y'''' \/ ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/
% 32.27/32.50     ~cp1 $Y'''' \/ ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/
% 32.27/32.50     ~rr $X $Y'''' \/ ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/
% 32.27/32.50     ~rr $X $Y''''''' \/ cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y1 $X)
% 32.27/32.50  |- ~cp $Y'''' \/ ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/
% 32.27/32.50     ~cp1 $Y'''' \/ ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/
% 32.27/32.50     ~rr $X $Y'''' \/ ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/
% 32.27/32.50     ~rr $X $Y''''''' \/ cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y2 $X)
% 32.27/32.50  |- ~cp $Y'''' \/ ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/
% 32.27/32.50     ~cp1 $Y'''' \/ ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/
% 32.27/32.50     ~rr $X $Y'''' \/ ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/
% 32.27/32.50     ~rr $X $Y''''''' \/ cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y3 $X)
% 32.27/32.50  |- ~cp $Y'''' \/ ~cp $Y''''' \/ ~cp $Y'''''' \/ ~cp $Y''''''' \/
% 32.27/32.50     ~cp1 $Y'''' \/ ~cp2 $Y''''' \/ ~cp3 $Y'''''' \/ ~cp4 $Y''''''' \/
% 32.27/32.50     ~rr $X $Y'''' \/ ~rr $X $Y''''' \/ ~rr $X $Y'''''' \/
% 32.27/32.50     ~rr $X $Y''''''' \/ cSatisfiable $X \/ rr $X (skolemFOFtoCNF_Y4 $X)
% 32.27/32.50  |- cp2 (skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698)
% 32.27/32.50  |- ~cp1 (skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698)
% 32.27/32.50  |- cp3 (skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698)
% 32.27/32.50  |- ~cp2 (skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698)
% 32.27/32.50  |- ~cp1 (skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698)
% 32.27/32.50  |- cp3 (skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698)
% 32.27/32.50  |- ~cp2 (skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698)
% 32.27/32.50  |- ~cp1 (skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698)
% 32.27/32.50  |- cp4 (skolemFOFtoCNF_Y i2003_11_14_17_15_37698)
% 32.27/32.50  |- ~cp3 (skolemFOFtoCNF_Y i2003_11_14_17_15_37698)
% 32.27/32.50  |- ~cp2 (skolemFOFtoCNF_Y i2003_11_14_17_15_37698)
% 32.27/32.50  |- ~cp1 (skolemFOFtoCNF_Y i2003_11_14_17_15_37698)
% 32.27/32.50  |- cp (skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698)
% 32.27/32.50  |- cp (skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698)
% 32.27/32.50  |- cp1 (skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698)
% 32.27/32.50  |- cp1 (skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698)
% 32.27/32.50  |- cp2 (skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698)
% 32.27/32.50  |- ~cp1 (skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698)
% 32.27/32.50  |- cp (skolemFOFtoCNF_Y i2003_11_14_17_15_37698)
% 32.27/32.50  |- cp (skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698)
% 32.27/32.50  |- rr i2003_11_14_17_15_37698 (skolemFOFtoCNF_Y i2003_11_14_17_15_37698)
% 32.27/32.50  |- rr i2003_11_14_17_15_37698 (skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698)
% 32.27/32.50  |- rr i2003_11_14_17_15_37698 (skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698)
% 32.27/32.50  |- rr i2003_11_14_17_15_37698 (skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698)
% 32.27/32.50  |- rr i2003_11_14_17_15_37698 (skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698)
% 32.27/32.50  |- rr i2003_11_14_17_15_37698 (skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698)
% 32.27/32.50  |- rr i2003_11_14_17_15_37698 (skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698)
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_111 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_112 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_113 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_114 \/ $_111 = $_112 \/ $_111 = $_113 \/
% 32.27/32.50     $_111 = $_114 \/ $_112 = $_113 \/ $_112 = $_114 \/ $_113 = $_114 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_111 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_112 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_113 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_114
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_111 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_112 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_113 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_114 \/ $_111 = $_112 \/ $_111 = $_113 \/
% 32.27/32.50     $_111 = $_114 \/ $_112 = $_113 \/ $_112 = $_114 \/ $_113 = $_114 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_111 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_112 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_113 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_114
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_111 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_112 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_113 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_114 \/ $_111 = $_112 \/ $_111 = $_113 \/
% 32.27/32.50     $_111 = $_114 \/ $_112 = $_113 \/ $_112 = $_114 \/ $_113 = $_114 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_111 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_112 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_113 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_114
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_111 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_112 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_113 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_114 \/ $_111 = $_112 \/ $_111 = $_113 \/
% 32.27/32.50     $_111 = $_114 \/ $_112 = $_113 \/ $_112 = $_114 \/ $_113 = $_114 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_111 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_112 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_113 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_114
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_111 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_112 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_113 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_114 \/ $_111 = $_112 \/ $_111 = $_113 \/
% 32.27/32.50     $_111 = $_114 \/ $_112 = $_113 \/ $_112 = $_114 \/ $_113 = $_114 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_111 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_112 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_113 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_114
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_111 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_112 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_113 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_114 \/ $_111 = $_112 \/ $_111 = $_113 \/
% 32.27/32.50     $_111 = $_114 \/ $_112 = $_113 \/ $_112 = $_114 \/ $_113 = $_114 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_111 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_112 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_113 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_114
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_111 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_112 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_113 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_114 \/ $_111 = $_112 \/ $_111 = $_113 \/
% 32.27/32.50     $_111 = $_114 \/ $_112 = $_113 \/ $_112 = $_114 \/ $_113 = $_114 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_111 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_112 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_113 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_114
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_116 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_117 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_118 \/ $_116 = $_117 \/ $_116 = $_118 \/
% 32.27/32.50     $_117 = $_118 \/ skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_118 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_118 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_116 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_117 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_118 \/ $_116 = $_117 \/ $_116 = $_118 \/
% 32.27/32.50     $_117 = $_118 \/ skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_118 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_118 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_116 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_117 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_118 \/ $_116 = $_117 \/ $_116 = $_118 \/
% 32.27/32.50     $_117 = $_118 \/ skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_118 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_118
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_116 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_117 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_118 \/ $_116 = $_117 \/ $_116 = $_118 \/
% 32.27/32.50     $_117 = $_118 \/ skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_118 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_118
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_116 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_117 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_118 \/ $_116 = $_117 \/ $_116 = $_118 \/
% 32.27/32.50     $_117 = $_118 \/ skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_118 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_118
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_116 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_117 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_118 \/ $_116 = $_117 \/ $_116 = $_118 \/
% 32.27/32.50     $_117 = $_118 \/ skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_118 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_116 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_117 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_118
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_120 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_121 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_122 \/ $_120 = $_121 \/ $_120 = $_122 \/
% 32.27/32.50     $_121 = $_122 \/ skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_120 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_121 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_122 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_120 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_121 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_122 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_120 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_121 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_122 \/ $_120 = $_121 \/ $_120 = $_122 \/
% 32.27/32.50     $_121 = $_122 \/ skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_120 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_121 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_122 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_120 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_121 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_122
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_120 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_121 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_122 \/ $_120 = $_121 \/ $_120 = $_122 \/
% 32.27/32.50     $_121 = $_122 \/ skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_120 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_121 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_122 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_120 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_121 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_122
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_120 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_121 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_122 \/ $_120 = $_121 \/ $_120 = $_122 \/
% 32.27/32.50     $_121 = $_122 \/ skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_120 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_121 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_122 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_120 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_121 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_122
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_120 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_121 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_122 \/ $_120 = $_121 \/ $_120 = $_122 \/
% 32.27/32.50     $_121 = $_122 \/ skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_120 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_121 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_122 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_120 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_121 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_122
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_124 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_125 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_126 \/ $_124 = $_125 \/ $_124 = $_126 \/
% 32.27/32.50     $_125 = $_126 \/ skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_124 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_125 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_126 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_124 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_125 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_126
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_124 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_125 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_126 \/ $_124 = $_125 \/ $_124 = $_126 \/
% 32.27/32.50     $_125 = $_126 \/ skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_124 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_125 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_126 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_124 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_125 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_126
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_124 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_125 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_126 \/ $_124 = $_125 \/ $_124 = $_126 \/
% 32.27/32.50     $_125 = $_126 \/ skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_124 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_125 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_126 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_124 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_125 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_126
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_124 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_125 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_126 \/ $_124 = $_125 \/ $_124 = $_126 \/
% 32.27/32.50     $_125 = $_126 \/ skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_124 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_125 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_126 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_124 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_125 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_126
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_128 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_129 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_130 \/ $_128 = $_129 \/ $_128 = $_130 \/
% 32.27/32.50     $_129 = $_130 \/ skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_128 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_129 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_130 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_128 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_129 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_130 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_128 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_129 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_130 \/ $_128 = $_129 \/ $_128 = $_130 \/
% 32.27/32.50     $_129 = $_130 \/ skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_128 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_129 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_130 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_128 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_129 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_130 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_128 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_129 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_130 \/ $_128 = $_129 \/ $_128 = $_130 \/
% 32.27/32.50     $_129 = $_130 \/ skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_128 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_129 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_130 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_128 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_129 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_130 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_132 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_133 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_134 \/ $_132 = $_133 \/ $_132 = $_134 \/
% 32.27/32.50     $_133 = $_134 \/ skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_132 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_133 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_134 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_132 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_133 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_134 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_132 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_133 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_134 \/ $_132 = $_133 \/ $_132 = $_134 \/
% 32.27/32.50     $_133 = $_134 \/ skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_132 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_133 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_134 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_132 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_133 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_134 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_136 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_137 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_138 \/ $_136 = $_137 \/ $_136 = $_138 \/
% 32.27/32.50     $_137 = $_138 \/ skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_136 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_137 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_138 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_136 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_137 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_138 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_148 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_149 \/ $_148 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_148 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_149 \/ $_148 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_149
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_148 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_149 \/ $_148 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_149
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_148 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_149 \/ $_148 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_149
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_148 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_149 \/ $_148 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_149 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_148 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_149
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_151
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_151
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_151 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_151
% 32.27/32.50  |- skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698
% 32.27/32.50  |- skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698
% 32.27/32.50  |- skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_158 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_158 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_158 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_158 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_158
% 32.27/32.50  |- skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_164 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_164 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_164 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_164 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_164 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_164 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_164 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_164 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_164 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_164 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.50  |- skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_173 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_174 \/ $_173 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_174
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_173 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_174 \/ $_173 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_174
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_173 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_174 \/ $_173 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_174
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_173 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_174 \/ $_173 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_174 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_173 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_174
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_176 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.50  |- skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_182 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_182 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_182 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_182 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_182 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_185 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_185 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_185 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_185 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_185 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_193 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_194 \/ $_193 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_193 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_193 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_193 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_193 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_194 \/ $_193 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_193 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_193 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_193 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_193 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_194 \/ $_193 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_193 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_193 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_193 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_194 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_196 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_196 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_196 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_196 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_196 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_196 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_196 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_196 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_196 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_196 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.50  |- skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_205 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_205 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_205 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_205 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_205 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_210 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_211 \/ $_210 = $_211 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_210 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_211 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_210 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_211 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_210 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_211 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_210 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_211 \/ $_210 = $_211 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_210 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_211 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_210 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_211 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_210 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_211 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_216 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_216 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_216 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_216 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_216 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_221 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_222 \/ $_221 = $_222 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_221 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 = $_222 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_2 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_221 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_222 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_221 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_222 \/
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_237 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_238 \/ $_237 = $_238 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_237 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_238 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_237 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_238 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_237 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_238
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_237 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_238 \/ $_237 = $_238 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_237 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_238 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_237 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_238 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_237 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_238
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_237 \/
% 32.27/32.50     ~rr i2003_11_14_17_15_37698 $_238 \/ $_237 = $_238 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_237 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_238 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_237 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_238 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_237 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_238
% 32.27/32.50  |- skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_248 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_248 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_248 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_248 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_248
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_248 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_248 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_248 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_248 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_248
% 32.27/32.50  |- skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698
% 32.27/32.50  |- ~rr i2003_11_14_17_15_37698 $_252 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_252 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_252 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_252 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_252 \/
% 32.27/32.50     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.50     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_257 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_258 \/ $_257 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_257 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_257 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_257 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_257 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_258 \/ $_257 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_257 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_257 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_257 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_257 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_258 \/ $_257 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_257 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_257 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_257 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_258 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_260 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_260 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_260 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_260 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_260 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_260 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_260 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_260 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_260 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_260 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.51  |- skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_268 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_268 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_268 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_268 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_268 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_273 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_274 \/ $_273 = $_274 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_273 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_274 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_273 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_274 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_273 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_274 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_273 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_274 \/ $_273 = $_274 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_273 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_274 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_273 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_274 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_273 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_274 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_276 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_276 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_276 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_276 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_276 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_284 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_285 \/ $_284 = $_285 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_284 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 = $_285 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_1 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_284 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_285 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_284 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_285 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_297 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_298 \/ $_297 = $_298 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_297 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_298 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_297 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_298 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_297 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_298 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_297 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_298 \/ $_297 = $_298 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_297 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_298 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_297 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_298 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_297 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_298 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_297 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_298 \/ $_297 = $_298 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_297 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_298 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_297 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_298 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_297 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_298
% 32.27/32.51  |- skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_4 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_303 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_303 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_303 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_303 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_303 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_303 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_303 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_303 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_303 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_303
% 32.27/32.51  |- skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_307 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_307 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_307 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_307 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_307 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_312 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_313 \/ $_312 = $_313 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_312 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_313 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_312 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_313 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_312 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_313 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_312 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_313 \/ $_312 = $_313 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_312 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_313 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_312 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_313 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_312 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_313
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_315 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_315 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_315 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_315 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_315
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_320 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_321 \/ $_320 = $_321 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_320 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 = $_321 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_320 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_321 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_320 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_321
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_328 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_329 \/ $_328 = $_329 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_328 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_329 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_328 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_329 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_328 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_329 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_328 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_329 \/ $_328 = $_329 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_328 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_329 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_328 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_329 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_328 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_329 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_331 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_331 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_331 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_331 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_331 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_336 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_337 \/ $_336 = $_337 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_336 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_337 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_336 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_337 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_336 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 = $_337 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_7 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698
% 32.27/32.51  |- ~rr i2003_11_14_17_15_37698 $_344 \/
% 32.27/32.51     ~rr i2003_11_14_17_15_37698 $_345 \/ $_344 = $_345 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_344 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 = $_345 \/
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_344 \/
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698 = $_345 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_344 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 = $_345 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_3 i2003_11_14_17_15_37698 \/
% 32.27/32.51     skolemFOFtoCNF_Y_6 i2003_11_14_17_15_37698 =
% 32.27/32.51     skolemFOFtoCNF_Y_5 i2003_11_14_17_15_37698
% 32.27/32.51  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 32.27/32.51  
%------------------------------------------------------------------------------