↑ Up

Metis---2.4.SAT-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : HAL007+1 : TPTP v8.1.0. Released v6.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n027.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 600s
% DateTime : Sat Jul 16 12:45:43 EDT 2022

% Result   : Satisfiable 0.17s 0.41s
% Output   : Saturation 0.17s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11  % Problem  : HAL007+1 : TPTP v8.1.0. Released v6.4.0.
% 0.11/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.32  % Computer : n027.cluster.edu
% 0.12/0.32  % Model    : x86_64 x86_64
% 0.12/0.32  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32  % Memory   : 8042.1875MB
% 0.12/0.32  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32  % CPULimit : 300
% 0.12/0.32  % WCLimit  : 600
% 0.12/0.32  % DateTime : Tue Jun  7 21:14:25 EDT 2022
% 0.12/0.32  % CPUTime  : 
% 0.12/0.32  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.17/0.41  % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.41  
% 0.17/0.41  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.41  |- ~morphism $Morphism $Dom $Cod \/ $Morphism . zero $Dom = zero $Cod
% 0.17/0.41  |- ~element $El $Dom \/ ~morphism $Morphism $Dom $Cod \/
% 0.17/0.41     element ($Morphism . $El) $Cod
% 0.17/0.41  |- ~($Morphism . $El1 = $Morphism . $El2) \/ ~element $El1 $Dom \/
% 0.17/0.41     ~element $El2 $Dom \/ ~injection $Morphism \/
% 0.17/0.41     ~morphism $Morphism $Dom $Cod \/ $El1 = $El2
% 0.17/0.41  |- ~(skolemFOFtoCNF_El1 $Dom $Morphism =
% 0.17/0.41       skolemFOFtoCNF_El2 $Dom $Morphism) \/ ~morphism $Morphism $Dom $Cod \/
% 0.17/0.41     injection $Morphism
% 0.17/0.41  |- ~morphism $Morphism $Dom $Cod \/
% 0.17/0.41     $Morphism . skolemFOFtoCNF_El1 $Dom $Morphism =
% 0.17/0.41     $Morphism . skolemFOFtoCNF_El2 $Dom $Morphism \/ injection $Morphism
% 0.17/0.41  |- ~morphism $Morphism $Dom $Cod \/
% 0.17/0.41     element (skolemFOFtoCNF_El1 $Dom $Morphism) $Dom \/ injection $Morphism
% 0.17/0.41  |- ~morphism $Morphism $Dom $Cod \/
% 0.17/0.41     element (skolemFOFtoCNF_El2 $Dom $Morphism) $Dom \/ injection $Morphism
% 0.17/0.41  |- ~element $ElCod $Cod \/ ~morphism $Morphism $Dom $Cod \/
% 0.17/0.41     ~surjection $Morphism \/
% 0.17/0.41     $Morphism . skolemFOFtoCNF_ElDom $Dom $ElCod $Morphism = $ElCod
% 0.17/0.41  |- ~element $ElCod $Cod \/ ~morphism $Morphism $Dom $Cod \/
% 0.17/0.41     ~surjection $Morphism \/
% 0.17/0.41     element (skolemFOFtoCNF_ElDom $Dom $ElCod $Morphism) $Dom
% 0.17/0.41  |- ~morphism $Morphism $Dom $Cod \/
% 0.17/0.41     element (skolemFOFtoCNF_ElCod $Cod $Dom $Morphism) $Cod \/
% 0.17/0.41     surjection $Morphism
% 0.17/0.41  |- ~($Morphism . $ElDom = skolemFOFtoCNF_ElCod $Cod $Dom $Morphism) \/
% 0.17/0.41     ~element $ElDom $Dom \/ ~morphism $Morphism $Dom $Cod \/
% 0.17/0.41     surjection $Morphism
% 0.17/0.41  |- ~element $ElDom $Dom \/ ~exact $Morphism1 $Morphism2 \/
% 0.17/0.41     ~morphism $Morphism1 $Dom $CodDom \/
% 0.17/0.41     ~morphism $Morphism2 $CodDom $Cod \/
% 0.17/0.41     $Morphism2 . ($Morphism1 . $ElDom) = zero $Cod
% 0.17/0.41  |- ~($Morphism2 . $ElCodDom = zero $Cod) \/ ~element $ElCodDom $CodDom \/
% 0.17/0.41     ~exact $Morphism1 $Morphism2 \/ ~morphism $Morphism1 $Dom $CodDom \/
% 0.17/0.41     ~morphism $Morphism2 $CodDom $Cod \/
% 0.17/0.41     $Morphism1 . skolemFOFtoCNF_ElDom_1 $Dom $ElCodDom $Morphism1 =
% 0.17/0.41     $ElCodDom
% 0.17/0.41  |- ~($Morphism2 . $ElCodDom = zero $Cod) \/ ~element $ElCodDom $CodDom \/
% 0.17/0.41     ~exact $Morphism1 $Morphism2 \/ ~morphism $Morphism1 $Dom $CodDom \/
% 0.17/0.41     ~morphism $Morphism2 $CodDom $Cod \/
% 0.17/0.41     element (skolemFOFtoCNF_ElDom_1 $Dom $ElCodDom $Morphism1) $Dom
% 0.17/0.41  |- ~morphism $Morphism1 $Dom $CodDom \/
% 0.17/0.41     ~morphism $Morphism2 $CodDom $Cod \/
% 0.17/0.41     $Morphism1 .
% 0.17/0.41     skolemFOFtoCNF_ElDom_2 $Cod $CodDom $Dom $Morphism1 $Morphism2 =
% 0.17/0.41     skolemFOFtoCNF_ElCodDom $Cod $CodDom $Dom $Morphism1 $Morphism2 \/
% 0.17/0.41     $Morphism2 .
% 0.17/0.41     skolemFOFtoCNF_ElCodDom $Cod $CodDom $Dom $Morphism1 $Morphism2 =
% 0.17/0.41     zero $Cod \/ exact $Morphism1 $Morphism2
% 0.17/0.41  |- ~morphism $Morphism1 $Dom $CodDom \/
% 0.17/0.41     ~morphism $Morphism2 $CodDom $Cod \/
% 0.17/0.41     $Morphism1 .
% 0.17/0.41     skolemFOFtoCNF_ElDom_2 $Cod $CodDom $Dom $Morphism1 $Morphism2 =
% 0.17/0.41     skolemFOFtoCNF_ElCodDom $Cod $CodDom $Dom $Morphism1 $Morphism2 \/
% 0.17/0.41     element
% 0.17/0.41       (skolemFOFtoCNF_ElCodDom $Cod $CodDom $Dom $Morphism1 $Morphism2)
% 0.17/0.41       $CodDom \/ exact $Morphism1 $Morphism2
% 0.17/0.41  |- ~morphism $Morphism1 $Dom $CodDom \/
% 0.17/0.41     ~morphism $Morphism2 $CodDom $Cod \/
% 0.17/0.41     $Morphism2 .
% 0.17/0.41     skolemFOFtoCNF_ElCodDom $Cod $CodDom $Dom $Morphism1 $Morphism2 =
% 0.17/0.41     zero $Cod \/
% 0.17/0.41     element (skolemFOFtoCNF_ElDom_2 $Cod $CodDom $Dom $Morphism1 $Morphism2)
% 0.17/0.41       $Dom \/ exact $Morphism1 $Morphism2
% 0.17/0.41  |- ~morphism $Morphism1 $Dom $CodDom \/
% 0.17/0.41     ~morphism $Morphism2 $CodDom $Cod \/
% 0.17/0.41     element
% 0.17/0.41       (skolemFOFtoCNF_ElCodDom $Cod $CodDom $Dom $Morphism1 $Morphism2)
% 0.17/0.41       $CodDom \/
% 0.17/0.41     element (skolemFOFtoCNF_ElDom_2 $Cod $CodDom $Dom $Morphism1 $Morphism2)
% 0.17/0.41       $Dom \/ exact $Morphism1 $Morphism2
% 0.17/0.41  |- ~($Morphism1 . $ElDom =
% 0.17/0.41       skolemFOFtoCNF_ElCodDom $Cod $CodDom $Dom $Morphism1 $Morphism2) \/
% 0.17/0.41     ~($Morphism2 .
% 0.17/0.41       skolemFOFtoCNF_ElCodDom $Cod $CodDom $Dom $Morphism1 $Morphism2 =
% 0.17/0.41       zero $Cod) \/ ~element $ElDom $Dom \/
% 0.17/0.41     ~element
% 0.17/0.41        (skolemFOFtoCNF_ElCodDom $Cod $CodDom $Dom $Morphism1 $Morphism2)
% 0.17/0.41        $CodDom \/ ~morphism $Morphism1 $Dom $CodDom \/
% 0.17/0.41     ~morphism $Morphism2 $CodDom $Cod \/ exact $Morphism1 $Morphism2
% 0.17/0.41  |- ~commute $M1 $M2 $M3 $M4 \/ ~element $ElDom $Dom \/
% 0.17/0.41     ~morphism $M1 $Dom $DomCod1 \/ ~morphism $M2 $DomCod1 $Cod \/
% 0.17/0.41     ~morphism $M3 $Dom $DomCod2 \/ ~morphism $M4 $DomCod2 $Cod \/
% 0.17/0.41     $M2 . ($M1 . $ElDom) = $M4 . ($M3 . $ElDom)
% 0.17/0.41  |- ~($M2 . ($M1 . skolemFOFtoCNF_ElDom_3 $Dom $M1 $M2 $M3 $M4) =
% 0.17/0.41       $M4 . ($M3 . skolemFOFtoCNF_ElDom_3 $Dom $M1 $M2 $M3 $M4)) \/
% 0.17/0.41     ~morphism $M1 $Dom $DomCod1 \/ ~morphism $M2 $DomCod1 $Cod \/
% 0.17/0.41     ~morphism $M3 $Dom $DomCod2 \/ ~morphism $M4 $DomCod2 $Cod \/
% 0.17/0.41     commute $M1 $M2 $M3 $M4
% 0.17/0.41  |- ~morphism $M1 $Dom $DomCod1 \/ ~morphism $M2 $DomCod1 $Cod \/
% 0.17/0.41     ~morphism $M3 $Dom $DomCod2 \/ ~morphism $M4 $DomCod2 $Cod \/
% 0.17/0.41     commute $M1 $M2 $M3 $M4 \/
% 0.17/0.41     element (skolemFOFtoCNF_ElDom_3 $Dom $M1 $M2 $M3 $M4) $Dom
% 0.17/0.41  |- ~element $El1 $Dom \/ ~element $El2 $Dom \/
% 0.17/0.41     element (subtract $Dom $El1 $El2) $Dom
% 0.17/0.41  |- ~element $El $Dom \/ subtract $Dom $El $El = zero $Dom
% 0.17/0.41  |- ~element $El1 $Dom \/ ~element $El2 $Dom \/
% 0.17/0.41     subtract $Dom $El1 (subtract $Dom $El1 $El2) = $El2
% 0.17/0.41  |- ~element $El1 $Dom \/ ~element $El2 $Dom \/
% 0.17/0.41     ~morphism $Morphism $Dom $Cod \/
% 0.17/0.41     $Morphism . subtract $Dom $El1 $El2 =
% 0.17/0.41     subtract $Cod ($Morphism . $El1) ($Morphism . $El2)
% 0.17/0.41  |- ~element $El2 $Dom \/ element (subtract $Dom $El2 $El2) $Dom
% 0.17/0.41  |- ~element $El2 $Dom \/
% 0.17/0.41     subtract $Dom $El2 (subtract $Dom $El2 $El2) = $El2
% 0.17/0.41  |- ~element $El2 $Dom \/ ~morphism $Morphism $Dom $Cod \/
% 0.17/0.41     $Morphism . subtract $Dom $El2 $El2 =
% 0.17/0.41     subtract $Cod ($Morphism . $El2) ($Morphism . $El2)
% 0.17/0.41  |- ~morphism $Morphism2 $Cod $Cod \/
% 0.17/0.41     $Morphism2 .
% 0.17/0.41     skolemFOFtoCNF_ElCodDom $Cod $Cod $Cod $Morphism2 $Morphism2 =
% 0.17/0.41     zero $Cod \/
% 0.17/0.41     $Morphism2 .
% 0.17/0.41     skolemFOFtoCNF_ElDom_2 $Cod $Cod $Cod $Morphism2 $Morphism2 =
% 0.17/0.41     skolemFOFtoCNF_ElCodDom $Cod $Cod $Cod $Morphism2 $Morphism2 \/
% 0.17/0.41     exact $Morphism2 $Morphism2
% 0.17/0.41  |- ~morphism $Morphism2 $Cod $Cod \/
% 0.17/0.41     $Morphism2 .
% 0.17/0.41     skolemFOFtoCNF_ElDom_2 $Cod $Cod $Cod $Morphism2 $Morphism2 =
% 0.17/0.41     skolemFOFtoCNF_ElCodDom $Cod $Cod $Cod $Morphism2 $Morphism2 \/
% 0.17/0.41     element (skolemFOFtoCNF_ElCodDom $Cod $Cod $Cod $Morphism2 $Morphism2)
% 0.17/0.41       $Cod \/ exact $Morphism2 $Morphism2
% 0.17/0.41  |- ~morphism $Morphism2 $Cod $Cod \/
% 0.17/0.41     $Morphism2 .
% 0.17/0.41     skolemFOFtoCNF_ElCodDom $Cod $Cod $Cod $Morphism2 $Morphism2 =
% 0.17/0.41     zero $Cod \/
% 0.17/0.41     element (skolemFOFtoCNF_ElDom_2 $Cod $Cod $Cod $Morphism2 $Morphism2)
% 0.17/0.41       $Cod \/ exact $Morphism2 $Morphism2
% 0.17/0.41  |- ~morphism $Morphism2 $Cod $Cod \/
% 0.17/0.41     element (skolemFOFtoCNF_ElCodDom $Cod $Cod $Cod $Morphism2 $Morphism2)
% 0.17/0.41       $Cod \/
% 0.17/0.41     element (skolemFOFtoCNF_ElDom_2 $Cod $Cod $Cod $Morphism2 $Morphism2)
% 0.17/0.41       $Cod \/ exact $Morphism2 $Morphism2
% 0.17/0.41  |- ~element $ElDom $Cod \/ ~exact $Morphism2 $Morphism2 \/
% 0.17/0.41     ~morphism $Morphism2 $Cod $Cod \/
% 0.17/0.41     $Morphism2 . ($Morphism2 . $ElDom) = zero $Cod
% 0.17/0.41  |- ~($Morphism2 . $ElCodDom = zero $Cod) \/ ~element $ElCodDom $Cod \/
% 0.17/0.41     ~exact $Morphism2 $Morphism2 \/ ~morphism $Morphism2 $Cod $Cod \/
% 0.17/0.41     $Morphism2 . skolemFOFtoCNF_ElDom_1 $Cod $ElCodDom $Morphism2 =
% 0.17/0.41     $ElCodDom
% 0.17/0.41  |- ~($Morphism2 . $ElCodDom = zero $Cod) \/ ~element $ElCodDom $Cod \/
% 0.17/0.41     ~exact $Morphism2 $Morphism2 \/ ~morphism $Morphism2 $Cod $Cod \/
% 0.17/0.41     element (skolemFOFtoCNF_ElDom_1 $Cod $ElCodDom $Morphism2) $Cod
% 0.17/0.41  |- ~($M2 . ($M2 . skolemFOFtoCNF_ElDom_3 $Cod $M2 $M2 $M3 $M4) =
% 0.17/0.41       $M4 . ($M3 . skolemFOFtoCNF_ElDom_3 $Cod $M2 $M2 $M3 $M4)) \/
% 0.17/0.41     ~morphism $M2 $Cod $Cod \/ ~morphism $M3 $Cod $DomCod2 \/
% 0.17/0.41     ~morphism $M4 $DomCod2 $Cod \/ commute $M2 $M2 $M3 $M4
% 0.17/0.41  |- ~($M2 . ($M3 . skolemFOFtoCNF_ElDom_3 $Dom $M3 $M2 $M3 $M4) =
% 0.17/0.41       $M4 . ($M3 . skolemFOFtoCNF_ElDom_3 $Dom $M3 $M2 $M3 $M4)) \/
% 0.17/0.41     ~morphism $M2 $DomCod2 $Cod \/ ~morphism $M3 $Dom $DomCod2 \/
% 0.17/0.41     ~morphism $M4 $DomCod2 $Cod \/ commute $M3 $M2 $M3 $M4
% 0.17/0.41  |- ~($M2 . ($M4 . skolemFOFtoCNF_ElDom_3 $DomCod2 $M4 $M2 $M3 $M4) =
% 0.17/0.41       $M4 . ($M3 . skolemFOFtoCNF_ElDom_3 $DomCod2 $M4 $M2 $M3 $M4)) \/
% 0.17/0.41     ~morphism $M2 $Cod $Cod \/ ~morphism $M3 $DomCod2 $DomCod2 \/
% 0.17/0.41     ~morphism $M4 $DomCod2 $Cod \/ commute $M4 $M2 $M3 $M4
% 0.17/0.41  |- ~($M3 . ($M1 . skolemFOFtoCNF_ElDom_3 $Dom $M1 $M3 $M3 $M4) =
% 0.17/0.41       $M4 . ($M3 . skolemFOFtoCNF_ElDom_3 $Dom $M1 $M3 $M3 $M4)) \/
% 0.17/0.41     ~morphism $M1 $Dom $Dom \/ ~morphism $M3 $Dom $DomCod2 \/
% 0.17/0.41     ~morphism $M4 $DomCod2 $DomCod2 \/ commute $M1 $M3 $M3 $M4
% 0.17/0.41  |- ~($M3 . ($M3 . skolemFOFtoCNF_ElDom_3 $DomCod2 $M3 $M3 $M3 $M4) =
% 0.17/0.41       $M4 . ($M3 . skolemFOFtoCNF_ElDom_3 $DomCod2 $M3 $M3 $M3 $M4)) \/
% 0.17/0.41     ~morphism $M3 $DomCod2 $DomCod2 \/ ~morphism $M4 $DomCod2 $DomCod2 \/
% 0.17/0.41     commute $M3 $M3 $M3 $M4
% 0.17/0.41  |- ~($M3 . ($M4 . skolemFOFtoCNF_ElDom_3 $DomCod2 $M4 $M3 $M3 $M4) =
% 0.17/0.41       $M4 . ($M3 . skolemFOFtoCNF_ElDom_3 $DomCod2 $M4 $M3 $M3 $M4)) \/
% 0.17/0.41     ~morphism $M3 $DomCod2 $DomCod2 \/ ~morphism $M4 $DomCod2 $DomCod2 \/
% 0.17/0.41     commute $M4 $M3 $M3 $M4
% 0.17/0.41  |- ~($M4 . ($M1 . skolemFOFtoCNF_ElDom_3 $Dom $M1 $M4 $M3 $M4) =
% 0.17/0.41       $M4 . ($M3 . skolemFOFtoCNF_ElDom_3 $Dom $M1 $M4 $M3 $M4)) \/
% 0.17/0.41     ~morphism $M1 $Dom $DomCod2 \/ ~morphism $M3 $Dom $DomCod2 \/
% 0.17/0.41     ~morphism $M4 $DomCod2 $Cod \/ commute $M1 $M4 $M3 $M4
% 0.17/0.41  |- ~morphism $M3 $Dom $DomCod2 \/ ~morphism $M4 $DomCod2 $Cod \/
% 0.17/0.41     commute $M3 $M4 $M3 $M4
% 0.17/0.41  |- ~($M4 . ($M4 . skolemFOFtoCNF_ElDom_3 $Cod $M4 $M4 $M3 $M4) =
% 0.17/0.41       $M4 . ($M3 . skolemFOFtoCNF_ElDom_3 $Cod $M4 $M4 $M3 $M4)) \/
% 0.17/0.41     ~morphism $M3 $Cod $Cod \/ ~morphism $M4 $Cod $Cod \/
% 0.17/0.41     commute $M4 $M4 $M3 $M4
% 0.17/0.41  |- ~($M2 . ($M1 . skolemFOFtoCNF_ElDom_3 $Cod $M1 $M2 $M4 $M4) =
% 0.17/0.41       $M4 . ($M4 . skolemFOFtoCNF_ElDom_3 $Cod $M1 $M2 $M4 $M4)) \/
% 0.17/0.41     ~morphism $M1 $Cod $DomCod1 \/ ~morphism $M2 $DomCod1 $Cod \/
% 0.17/0.41     ~morphism $M4 $Cod $Cod \/ commute $M1 $M2 $M4 $M4
% 0.17/0.41  |- ~($M2 . ($M2 . skolemFOFtoCNF_ElDom_3 $DomCod1 $M2 $M2 $M4 $M4) =
% 0.17/0.41       $M4 . ($M4 . skolemFOFtoCNF_ElDom_3 $DomCod1 $M2 $M2 $M4 $M4)) \/
% 0.17/0.41     ~morphism $M2 $DomCod1 $DomCod1 \/ ~morphism $M4 $DomCod1 $DomCod1 \/
% 0.17/0.41     commute $M2 $M2 $M4 $M4
% 0.17/0.41  |- ~($M2 . ($M4 . skolemFOFtoCNF_ElDom_3 $Cod $M4 $M2 $M4 $M4) =
% 0.17/0.41       $M4 . ($M4 . skolemFOFtoCNF_ElDom_3 $Cod $M4 $M2 $M4 $M4)) \/
% 0.17/0.41     ~morphism $M2 $Cod $Cod \/ ~morphism $M4 $Cod $Cod \/
% 0.17/0.41     commute $M4 $M2 $M4 $M4
% 0.17/0.42  |- ~($M4 . ($M1 . skolemFOFtoCNF_ElDom_3 $Cod $M1 $M4 $M4 $M4) =
% 0.17/0.42       $M4 . ($M4 . skolemFOFtoCNF_ElDom_3 $Cod $M1 $M4 $M4 $M4)) \/
% 0.17/0.42     ~morphism $M1 $Cod $Cod \/ ~morphism $M4 $Cod $Cod \/
% 0.17/0.42     commute $M1 $M4 $M4 $M4
% 0.17/0.42  |- ~morphism $M4 $Cod $Cod \/ commute $M4 $M4 $M4 $M4
% 0.17/0.42  |- ~morphism $M2 $Cod $Cod \/ ~morphism $M3 $Cod $DomCod2 \/
% 0.17/0.42     ~morphism $M4 $DomCod2 $Cod \/ commute $M2 $M2 $M3 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $Cod $M2 $M2 $M3 $M4) $Cod
% 0.17/0.42  |- ~morphism $M2 $DomCod2 $Cod \/ ~morphism $M3 $Dom $DomCod2 \/
% 0.17/0.42     ~morphism $M4 $DomCod2 $Cod \/ commute $M3 $M2 $M3 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $Dom $M3 $M2 $M3 $M4) $Dom
% 0.17/0.42  |- ~morphism $M2 $Cod $Cod \/ ~morphism $M3 $DomCod2 $DomCod2 \/
% 0.17/0.42     ~morphism $M4 $DomCod2 $Cod \/ commute $M4 $M2 $M3 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $DomCod2 $M4 $M2 $M3 $M4) $DomCod2
% 0.17/0.42  |- ~morphism $M1 $Dom $Dom \/ ~morphism $M3 $Dom $DomCod2 \/
% 0.17/0.42     ~morphism $M4 $DomCod2 $DomCod2 \/ commute $M1 $M3 $M3 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $Dom $M1 $M3 $M3 $M4) $Dom
% 0.17/0.42  |- ~morphism $M3 $DomCod2 $DomCod2 \/ ~morphism $M4 $DomCod2 $DomCod2 \/
% 0.17/0.42     commute $M3 $M3 $M3 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $DomCod2 $M3 $M3 $M3 $M4) $DomCod2
% 0.17/0.42  |- ~morphism $M3 $DomCod2 $DomCod2 \/ ~morphism $M4 $DomCod2 $DomCod2 \/
% 0.17/0.42     commute $M4 $M3 $M3 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $DomCod2 $M4 $M3 $M3 $M4) $DomCod2
% 0.17/0.42  |- ~morphism $M1 $Dom $DomCod2 \/ ~morphism $M3 $Dom $DomCod2 \/
% 0.17/0.42     ~morphism $M4 $DomCod2 $Cod \/ commute $M1 $M4 $M3 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $Dom $M1 $M4 $M3 $M4) $Dom
% 0.17/0.42  |- ~morphism $M3 $Cod $Cod \/ ~morphism $M4 $Cod $Cod \/
% 0.17/0.42     commute $M4 $M4 $M3 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $Cod $M4 $M4 $M3 $M4) $Cod
% 0.17/0.42  |- ~morphism $M1 $Cod $DomCod1 \/ ~morphism $M2 $DomCod1 $Cod \/
% 0.17/0.42     ~morphism $M4 $Cod $Cod \/ commute $M1 $M2 $M4 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $Cod $M1 $M2 $M4 $M4) $Cod
% 0.17/0.42  |- ~morphism $M2 $DomCod1 $DomCod1 \/ ~morphism $M4 $DomCod1 $DomCod1 \/
% 0.17/0.42     commute $M2 $M2 $M4 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $DomCod1 $M2 $M2 $M4 $M4) $DomCod1
% 0.17/0.42  |- ~morphism $M2 $Cod $Cod \/ ~morphism $M4 $Cod $Cod \/
% 0.17/0.42     commute $M4 $M2 $M4 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $Cod $M4 $M2 $M4 $M4) $Cod
% 0.17/0.42  |- ~morphism $M1 $Cod $Cod \/ ~morphism $M4 $Cod $Cod \/
% 0.17/0.42     commute $M1 $M4 $M4 $M4 \/
% 0.17/0.42     element (skolemFOFtoCNF_ElDom_3 $Cod $M1 $M4 $M4 $M4) $Cod
% 0.17/0.42  |- ~($Morphism1 .
% 0.17/0.42       skolemFOFtoCNF_ElCodDom $Cod $CodDom $CodDom $Morphism1 $Morphism2 =
% 0.17/0.42       skolemFOFtoCNF_ElCodDom $Cod $CodDom $CodDom $Morphism1 $Morphism2) \/
% 0.17/0.42     ~($Morphism2 .
% 0.17/0.42       skolemFOFtoCNF_ElCodDom $Cod $CodDom $CodDom $Morphism1 $Morphism2 =
% 0.17/0.42       zero $Cod) \/
% 0.17/0.42     ~element
% 0.17/0.42        (skolemFOFtoCNF_ElCodDom $Cod $CodDom $CodDom $Morphism1 $Morphism2)
% 0.17/0.42        $CodDom \/ ~morphism $Morphism1 $CodDom $CodDom \/
% 0.17/0.42     ~morphism $Morphism2 $CodDom $Cod \/ exact $Morphism1 $Morphism2
% 0.17/0.42  |- ~commute $M2 $M2 $M3 $M4 \/ ~element $ElDom $Cod \/
% 0.17/0.42     ~morphism $M2 $Cod $Cod \/ ~morphism $M3 $Cod $DomCod2 \/
% 0.17/0.42     ~morphism $M4 $DomCod2 $Cod \/
% 0.17/0.42     $M2 . ($M2 . $ElDom) = $M4 . ($M3 . $ElDom)
% 0.17/0.42  |- ~commute $M3 $M2 $M3 $M4 \/ ~element $ElDom $Dom \/
% 0.17/0.42     ~morphism $M2 $DomCod2 $Cod \/ ~morphism $M3 $Dom $DomCod2 \/
% 0.17/0.42     ~morphism $M4 $DomCod2 $Cod \/
% 0.17/0.42     $M2 . ($M3 . $ElDom) = $M4 . ($M3 . $ElDom)
% 0.17/0.42  |- ~commute $M4 $M2 $M3 $M4 \/ ~element $ElDom $DomCod2 \/
% 0.17/0.42     ~morphism $M2 $Cod $Cod \/ ~morphism $M3 $DomCod2 $DomCod2 \/
% 0.17/0.42     ~morphism $M4 $DomCod2 $Cod \/
% 0.17/0.42     $M2 . ($M4 . $ElDom) = $M4 . ($M3 . $ElDom)
% 0.17/0.42  |- ~commute $M1 $M3 $M3 $M4 \/ ~element $ElDom $Dom \/
% 0.17/0.42     ~morphism $M1 $Dom $Dom \/ ~morphism $M3 $Dom $DomCod2 \/
% 0.17/0.42     ~morphism $M4 $DomCod2 $DomCod2 \/
% 0.17/0.42     $M3 . ($M1 . $ElDom) = $M4 . ($M3 . $ElDom)
% 0.17/0.42  |- ~commute $M3 $M3 $M3 $M4 \/ ~element $ElDom $DomCod2 \/
% 0.17/0.42     ~morphism $M3 $DomCod2 $DomCod2 \/ ~morphism $M4 $DomCod2 $DomCod2 \/
% 0.17/0.42     $M3 . ($M3 . $ElDom) = $M4 . ($M3 . $ElDom)
% 0.17/0.42  |- ~commute $M4 $M3 $M3 $M4 \/ ~element $ElDom $DomCod2 \/
% 0.17/0.42     ~morphism $M3 $DomCod2 $DomCod2 \/ ~morphism $M4 $DomCod2 $DomCod2 \/
% 0.17/0.42     $M3 . ($M4 . $ElDom) = $M4 . ($M3 . $ElDom)
% 0.17/0.42  |- ~commute $M1 $M4 $M3 $M4 \/ ~element $ElDom $Dom \/
% 0.17/0.42     ~morphism $M1 $Dom $DomCod2 \/ ~morphism $M3 $Dom $DomCod2 \/
% 0.17/0.42     ~morphism $M4 $DomCod2 $Cod \/
% 0.17/0.42     $M4 . ($M1 . $ElDom) = $M4 . ($M3 . $ElDom)
% 0.17/0.42  |- ~commute $M4 $M4 $M3 $M4 \/ ~element $ElDom $Cod \/
% 0.17/0.42     ~morphism $M3 $Cod $Cod \/ ~morphism $M4 $Cod $Cod \/
% 0.17/0.42     $M4 . ($M4 . $ElDom) = $M4 . ($M3 . $ElDom)
% 0.17/0.42  |- ~commute $M1 $M2 $M4 $M4 \/ ~element $ElDom $Cod \/
% 0.17/0.42     ~morphism $M1 $Cod $DomCod1 \/ ~morphism $M2 $DomCod1 $Cod \/
% 0.17/0.42     ~morphism $M4 $Cod $Cod \/ $M2 . ($M1 . $ElDom) = $M4 . ($M4 . $ElDom)
% 0.17/0.42  |- ~commute $M2 $M2 $M4 $M4 \/ ~element $ElDom $DomCod1 \/
% 0.17/0.42     ~morphism $M2 $DomCod1 $DomCod1 \/ ~morphism $M4 $DomCod1 $DomCod1 \/
% 0.17/0.42     $M2 . ($M2 . $ElDom) = $M4 . ($M4 . $ElDom)
% 0.17/0.42  |- ~commute $M4 $M2 $M4 $M4 \/ ~element $ElDom $Cod \/
% 0.17/0.42     ~morphism $M2 $Cod $Cod \/ ~morphism $M4 $Cod $Cod \/
% 0.17/0.42     $M2 . ($M4 . $ElDom) = $M4 . ($M4 . $ElDom)
% 0.17/0.42  |- ~commute $M1 $M4 $M4 $M4 \/ ~element $ElDom $Cod \/
% 0.17/0.42     ~morphism $M1 $Cod $Cod \/ ~morphism $M4 $Cod $Cod \/
% 0.17/0.42     $M4 . ($M1 . $ElDom) = $M4 . ($M4 . $ElDom)
% 0.17/0.42  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42  
%------------------------------------------------------------------------------