%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GEO659+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n022.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 : 0s
% DateTime : Sat Jul 16 02:55:25 EDT 2022
% Result : Theorem 214.21s 214.61s
% Output : Refutation 214.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GEO659+1 : TPTP v8.1.0. Released v7.5.0.
% 0.13/0.13 % Command : bliksem %s
% 0.13/0.35 % Computer : n022.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % DateTime : Sat Jun 18 07:43:32 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.77/1.22 *** allocated 10000 integers for termspace/termends
% 0.77/1.22 *** allocated 10000 integers for clauses
% 0.77/1.22 *** allocated 10000 integers for justifications
% 0.77/1.22 Bliksem 1.12
% 0.77/1.22
% 0.77/1.22
% 0.77/1.22 Automatic Strategy Selection
% 0.77/1.22
% 0.77/1.22 *** allocated 15000 integers for termspace/termends
% 0.77/1.22
% 0.77/1.22 Clauses:
% 0.77/1.22
% 0.77/1.22 { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 0.77/1.22 { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 0.77/1.22 { ! coll( X, T, Y ), ! coll( X, T, Z ), coll( Y, Z, X ) }.
% 0.77/1.22 { ! para( X, Y, Z, T ), para( X, Y, T, Z ) }.
% 0.77/1.22 { ! para( X, Y, Z, T ), para( Z, T, X, Y ) }.
% 0.77/1.22 { ! para( X, Y, U, W ), ! para( U, W, Z, T ), para( X, Y, Z, T ) }.
% 0.77/1.22 { ! perp( X, Y, Z, T ), perp( X, Y, T, Z ) }.
% 0.77/1.22 { ! perp( X, Y, Z, T ), perp( Z, T, X, Y ) }.
% 0.77/1.22 { ! perp( X, Y, U, W ), ! perp( U, W, Z, T ), para( X, Y, Z, T ) }.
% 0.77/1.22 { ! para( X, Y, U, W ), ! perp( U, W, Z, T ), perp( X, Y, Z, T ) }.
% 0.77/1.22 { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 0.77/1.22 { ! cong( T, X, T, Y ), ! cong( T, X, T, Z ), circle( T, X, Y, Z ) }.
% 0.77/1.22 { ! cong( U, X, U, Y ), ! cong( U, X, U, Z ), ! cong( U, X, U, T ), cyclic
% 0.77/1.22 ( X, Y, Z, T ) }.
% 0.77/1.22 { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z ) }.
% 0.77/1.22 { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T ) }.
% 0.77/1.22 { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T ) }.
% 0.77/1.22 { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 0.77/1.22 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( Y, X, Z, T, U, W, V0, V1
% 0.77/1.22 ) }.
% 0.77/1.22 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( Z, T, X, Y, V0, V1, U, W
% 0.77/1.22 ) }.
% 0.77/1.22 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( U, W, V0, V1, X, Y, Z, T
% 0.77/1.22 ) }.
% 0.77/1.22 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( X, Y, U, W, Z, T, V0, V1
% 0.77/1.22 ) }.
% 0.77/1.22 { ! eqangle( X, Y, Z, T, V2, V3, V4, V5 ), ! eqangle( V2, V3, V4, V5, U, W
% 0.77/1.22 , V0, V1 ), eqangle( X, Y, Z, T, U, W, V0, V1 ) }.
% 0.77/1.22 { ! cong( X, Y, Z, T ), cong( X, Y, T, Z ) }.
% 0.77/1.22 { ! cong( X, Y, Z, T ), cong( Z, T, X, Y ) }.
% 0.77/1.22 { ! cong( X, Y, U, W ), ! cong( U, W, Z, T ), cong( X, Y, Z, T ) }.
% 0.77/1.22 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( Y, X, Z, T, U, W, V0, V1
% 0.77/1.22 ) }.
% 0.77/1.22 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( Z, T, X, Y, V0, V1, U, W
% 0.77/1.22 ) }.
% 0.77/1.22 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( U, W, V0, V1, X, Y, Z, T
% 0.77/1.22 ) }.
% 0.77/1.22 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( X, Y, U, W, Z, T, V0, V1
% 0.77/1.22 ) }.
% 0.77/1.22 { ! eqratio( X, Y, Z, T, V2, V3, V4, V5 ), ! eqratio( V2, V3, V4, V5, U, W
% 0.77/1.22 , V0, V1 ), eqratio( X, Y, Z, T, U, W, V0, V1 ) }.
% 0.77/1.22 { ! simtri( X, Z, Y, T, W, U ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.22 { ! simtri( Y, X, Z, U, T, W ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.22 { ! simtri( T, U, W, X, Y, Z ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.22 { ! simtri( X, Y, Z, V0, V1, V2 ), ! simtri( V0, V1, V2, T, U, W ), simtri
% 0.77/1.22 ( X, Y, Z, T, U, W ) }.
% 0.77/1.22 { ! contri( X, Z, Y, T, W, U ), contri( X, Y, Z, T, U, W ) }.
% 0.77/1.22 { ! contri( Y, X, Z, U, T, W ), contri( X, Y, Z, T, U, W ) }.
% 0.77/1.22 { ! contri( T, U, W, X, Y, Z ), contri( X, Y, Z, T, U, W ) }.
% 0.77/1.22 { ! contri( X, Y, Z, V0, V1, V2 ), ! contri( V0, V1, V2, T, U, W ), contri
% 0.77/1.22 ( X, Y, Z, T, U, W ) }.
% 0.77/1.22 { ! eqangle( X, Y, U, W, Z, T, U, W ), para( X, Y, Z, T ) }.
% 0.77/1.22 { ! para( X, Y, Z, T ), eqangle( X, Y, U, W, Z, T, U, W ) }.
% 0.77/1.22 { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z, Y, T, X, T, Y ) }.
% 0.77/1.22 { ! eqangle( Z, X, Z, Y, T, X, T, Y ), coll( Z, T, X ), cyclic( X, Y, Z, T
% 0.77/1.22 ) }.
% 0.77/1.22 { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll( Z, T, Y ), cyclic( X, Y, Z,
% 0.77/1.22 T ) }.
% 0.77/1.22 { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U, T ), ! cyclic( X, Y, U, W ), !
% 0.77/1.22 eqangle( U, X, U, Y, W, Z, W, T ), cong( X, Y, Z, T ) }.
% 0.77/1.22 { ! midp( Z, U, X ), ! midp( T, U, Y ), para( Z, T, X, Y ) }.
% 0.77/1.22 { ! midp( U, X, T ), ! para( U, Z, T, Y ), ! coll( Z, X, Y ), midp( Z, X, Y
% 0.77/1.22 ) }.
% 0.77/1.22 { ! cong( Z, X, Z, Y ), eqangle( Z, X, X, Y, X, Y, Z, Y ) }.
% 0.77/1.22 { ! eqangle( Z, X, X, Y, X, Y, Z, Y ), coll( Z, X, Y ), cong( Z, X, Z, Y )
% 0.77/1.22 }.
% 0.77/1.22 { ! circle( U, X, Y, Z ), ! perp( U, X, X, T ), eqangle( X, T, X, Y, Z, X,
% 0.77/1.22 Z, Y ) }.
% 0.77/1.22 { ! circle( Y, X, T, U ), ! eqangle( X, Z, X, T, U, X, U, T ), perp( Y, X,
% 0.77/1.22 X, Z ) }.
% 0.77/1.22 { ! circle( T, X, Y, Z ), ! midp( U, Y, Z ), eqangle( X, Y, X, Z, T, Y, T,
% 0.77/1.22 U ) }.
% 0.77/1.22 { ! circle( U, T, X, Y ), ! coll( Z, X, Y ), ! eqangle( T, X, T, Y, U, X, U
% 0.77/1.22 , Z ), midp( Z, X, Y ) }.
% 0.77/1.22 { ! perp( X, Y, Y, T ), ! midp( Z, X, T ), cong( X, Z, Y, Z ) }.
% 0.77/1.22 { ! circle( T, X, Y, Z ), ! coll( T, X, Z ), perp( X, Y, Y, Z ) }.
% 0.77/1.22 { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T ), eqangle( X, T, Z, T, Z, T,
% 0.77/1.22 Z, Y ) }.
% 0.77/1.22 { ! midp( T, X, Y ), ! perp( Z, T, X, Y ), cong( Z, X, Z, Y ) }.
% 0.77/1.22 { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T ), perp( X, Y, Z, T ) }.
% 0.77/1.22 { ! cong( X, Y, T, Y ), ! cong( X, Z, T, Z ), ! cyclic( X, T, Y, Z ), perp
% 0.77/1.22 ( Y, X, X, Z ) }.
% 0.77/1.22 { ! eqangle( X, Y, Y, Z, T, U, U, W ), ! eqangle( X, Z, Y, Z, T, W, U, W )
% 0.77/1.22 , coll( X, Y, Z ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.22 { ! simtri( X, Y, Z, T, U, W ), eqratio( X, Y, X, Z, T, U, T, W ) }.
% 0.77/1.22 { ! simtri( X, Y, Z, T, U, W ), eqangle( X, Y, Y, Z, T, U, U, W ) }.
% 0.77/1.22 { ! simtri( X, Y, Z, T, U, W ), ! cong( X, Y, T, U ), contri( X, Y, Z, T, U
% 0.77/1.22 , W ) }.
% 0.77/1.22 { ! contri( X, Y, U, Z, T, W ), cong( X, Y, Z, T ) }.
% 0.77/1.22 { ! midp( U, X, Y ), ! midp( U, Z, T ), para( X, Z, Y, T ) }.
% 0.77/1.22 { ! midp( Z, T, U ), ! para( T, X, U, Y ), ! para( T, Y, U, X ), midp( Z, X
% 0.77/1.22 , Y ) }.
% 0.77/1.22 { ! para( X, Y, Z, T ), ! coll( U, X, Z ), ! coll( U, Y, T ), eqratio( U, X
% 0.77/1.22 , X, Z, U, Y, Y, T ) }.
% 0.77/1.22 { ! para( X, Y, X, Z ), coll( X, Y, Z ) }.
% 0.77/1.22 { ! cong( X, Y, X, Z ), ! coll( X, Y, Z ), midp( X, Y, Z ) }.
% 0.77/1.22 { ! midp( X, Y, Z ), cong( X, Y, X, Z ) }.
% 0.77/1.22 { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 0.77/1.22 { ! midp( U, X, Y ), ! midp( W, Z, T ), eqratio( U, X, X, Y, W, Z, Z, T ) }
% 0.77/1.22 .
% 0.77/1.22 { ! eqangle( X, Y, Z, T, Z, T, X, Y ), para( X, Y, Z, T ), perp( X, Y, Z, T
% 0.77/1.22 ) }.
% 0.77/1.22 { ! eqangle( X, Y, Z, T, Z, T, X, Y ), perp( X, Y, Z, T ), para( X, Y, Z, T
% 0.77/1.22 ) }.
% 0.77/1.22 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), ! para( U, W, V0, V1 ), para( X, Y
% 0.77/1.22 , Z, T ) }.
% 0.77/1.22 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), ! perp( U, W, V0, V1 ), perp( X, Y
% 0.77/1.22 , Z, T ) }.
% 0.77/1.22 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), ! cong( U, W, V0, V1 ), cong( X, Y
% 0.77/1.22 , Z, T ) }.
% 0.77/1.22 { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z, Y, Z, X, Z ), coll( skol1( U
% 0.77/1.22 , W, Z, T ), Z, T ) }.
% 0.77/1.22 { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z, Y, Z, X, Z ), coll( skol1( X
% 0.77/1.22 , Y, Z, T ), X, Y ) }.
% 0.77/1.22 { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( skol2( U
% 0.77/1.22 , W, Z, T ), Z, T ) }.
% 0.77/1.22 { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( Y, X,
% 0.77/1.22 skol2( X, Y, Z, T ) ) }.
% 0.77/1.22 { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( skol3( U
% 0.77/1.22 , W, Z, T ), Z, T ) }.
% 0.77/1.22 { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( Y, X,
% 0.77/1.22 skol3( X, Y, Z, T ) ) }.
% 0.77/1.22 { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y ), coll( skol4( U, W, Z, T ), Z
% 0.77/1.22 , T ) }.
% 0.77/1.22 { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y ), coll( Y, X, skol4( X, Y, Z, T
% 0.77/1.22 ) ) }.
% 0.77/1.22 { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll( X, Y, Z ), cyclic( T, Y, Z,
% 0.77/1.22 skol5( W, Y, Z, T ) ) }.
% 0.77/1.22 { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll( X, Y, Z ), eqangle( X, Z, Y, Z
% 0.77/1.22 , X, skol5( X, Y, Z, T ), Y, skol5( X, Y, Z, T ) ) }.
% 0.77/1.22 { ! midp( U, X, Y ), ! midp( W, Z, T ), midp( skol6( X, V0, V1, T, V2, V3 )
% 0.77/1.22 , X, T ) }.
% 0.77/1.22 { ! midp( U, X, Y ), ! midp( W, Z, T ), para( skol6( X, V0, Z, T, V1, W ),
% 0.77/1.22 W, X, Z ) }.
% 0.77/1.22 { ! midp( U, X, Y ), ! midp( W, Z, T ), para( skol6( X, Y, Z, T, U, W ), U
% 0.77/1.22 , Y, T ) }.
% 0.77/1.22 { ! midp( Z, X, Y ), ! midp( W, T, U ), ! coll( T, X, Y ), ! coll( U, X, Y
% 0.77/1.22 ), midp( skol7( X, V0 ), X, V0 ) }.
% 0.77/1.22 { ! midp( T, X, U ), ! para( X, W, Z, T ), ! para( X, W, U, Y ), ! coll( W
% 0.77/1.22 , Y, Z ), coll( skol8( V0, V1, Z, T ), T, Z ) }.
% 0.77/1.22 { ! midp( T, X, U ), ! para( X, W, Z, T ), ! para( X, W, U, Y ), ! coll( W
% 0.77/1.22 , Y, Z ), coll( skol8( X, Y, Z, T ), X, Y ) }.
% 0.77/1.22 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), cong( T, Z, T, skol9( W, V0,
% 0.77/1.22 Z, T ) ) }.
% 0.77/1.22 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), cong( Y, Z, Y, skol9( W, Y, Z
% 0.77/1.22 , T ) ) }.
% 0.77/1.22 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), para( skol9( X, Y, Z, T ), Z
% 0.77/1.22 , X, Y ) }.
% 0.77/1.22 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), coll( skol10( U, Y, Z ), Z, Y
% 0.77/1.22 ) }.
% 0.77/1.22 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), perp( X, skol10( X, Y, Z ), Z
% 0.77/1.22 , Y ) }.
% 0.77/1.22 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), alpha1( X, Y, Z ) }.
% 0.77/1.22 { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z ), Z, X ) }.
% 0.77/1.22 { ! alpha1( X, Y, Z ), perp( Y, skol11( X, Y, Z ), Z, X ) }.
% 0.77/1.22 { ! coll( T, Z, X ), ! perp( Y, T, Z, X ), alpha1( X, Y, Z ) }.
% 0.77/1.22 { ! circle( Y, X, Z, T ), perp( skol12( X, Y ), X, X, Y ) }.
% 3.28/3.69 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 3.28/3.69 , alpha2( X, Z, U, skol13( X, V0, Z, V1, U ) ) }.
% 3.28/3.69 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 3.28/3.69 , coll( skol21( V0, Y, T, V1 ), Y, T ) }.
% 3.28/3.69 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 3.28/3.69 , cong( skol21( X, Y, T, U ), U, U, X ) }.
% 3.28/3.69 { ! alpha2( X, Y, Z, T ), coll( T, X, Y ) }.
% 3.28/3.69 { ! alpha2( X, Y, Z, T ), cong( T, Z, Z, X ) }.
% 3.28/3.69 { ! coll( T, X, Y ), ! cong( T, Z, Z, X ), alpha2( X, Y, Z, T ) }.
% 3.28/3.69 { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T ), ! midp( U, X, Y ), circle(
% 3.28/3.69 skol14( X, Y, Z ), X, Y, Z ) }.
% 3.28/3.69 { ! perp( X, Z, Z, Y ), ! cyclic( X, Y, Z, T ), circle( skol15( X, Y, Z ),
% 3.28/3.69 X, Y, Z ) }.
% 3.28/3.69 { ! perp( X, U, U, T ), ! coll( T, Y, Z ), coll( skol16( W, Y, Z ), Y, Z )
% 3.28/3.69 }.
% 3.28/3.69 { ! perp( X, U, U, T ), ! coll( T, Y, Z ), perp( skol16( X, Y, Z ), X, Y, Z
% 3.28/3.69 ) }.
% 3.28/3.69 { ! perp( X, Z, X, Y ), ! perp( Y, X, Y, T ), ! midp( U, Z, T ), midp(
% 3.28/3.69 skol17( X, Y ), X, Y ) }.
% 3.28/3.69 { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z ), coll( X, Y, skol18( X, Y ) )
% 3.28/3.69 }.
% 3.28/3.69 { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z ), cong( Y, X, Y, skol18( X, Y )
% 3.28/3.69 ) }.
% 3.28/3.69 { ! para( U, W, X, Y ), ! coll( Z, U, X ), ! coll( Z, W, Y ), ! coll( T, U
% 3.28/3.69 , W ), coll( Z, T, skol19( V0, V1, Z, T ) ) }.
% 3.28/3.69 { ! para( U, W, X, Y ), ! coll( Z, U, X ), ! coll( Z, W, Y ), ! coll( T, U
% 3.28/3.69 , W ), coll( skol19( X, Y, Z, T ), X, Y ) }.
% 3.28/3.69 { perp( skol20, skol25, skol26, skol27 ) }.
% 3.28/3.69 { coll( skol20, skol26, skol27 ) }.
% 3.28/3.69 { perp( skol22, skol26, skol25, skol27 ) }.
% 3.28/3.69 { coll( skol22, skol25, skol27 ) }.
% 3.28/3.69 { midp( skol28, skol25, skol27 ) }.
% 3.28/3.69 { perp( skol25, skol27, skol28, skol29 ) }.
% 3.28/3.69 { midp( skol30, skol25, skol26 ) }.
% 3.28/3.69 { perp( skol25, skol26, skol30, skol29 ) }.
% 3.28/3.69 { midp( skol31, skol27, skol26 ) }.
% 3.28/3.69 { perp( skol27, skol26, skol31, skol29 ) }.
% 3.28/3.69 { coll( skol26, skol22, skol23 ) }.
% 3.28/3.69 { circle( skol29, skol26, skol23, skol32 ) }.
% 3.28/3.69 { coll( skol25, skol20, skol24 ) }.
% 3.28/3.69 { circle( skol29, skol25, skol24, skol33 ) }.
% 3.28/3.69 { ! para( skol20, skol22, skol23, skol24 ) }.
% 3.28/3.69
% 3.28/3.69 percentage equality = 0.008596, percentage horn = 0.931298
% 3.28/3.69 This is a problem with some equality
% 3.28/3.69
% 3.28/3.69
% 3.28/3.69
% 3.28/3.69 Options Used:
% 3.28/3.69
% 3.28/3.69 useres = 1
% 3.28/3.69 useparamod = 1
% 3.28/3.69 useeqrefl = 1
% 3.28/3.69 useeqfact = 1
% 3.28/3.69 usefactor = 1
% 3.28/3.69 usesimpsplitting = 0
% 3.28/3.69 usesimpdemod = 5
% 3.28/3.69 usesimpres = 3
% 3.28/3.69
% 3.28/3.69 resimpinuse = 1000
% 3.28/3.69 resimpclauses = 20000
% 3.28/3.69 substype = eqrewr
% 3.28/3.69 backwardsubs = 1
% 3.28/3.69 selectoldest = 5
% 3.28/3.69
% 3.28/3.69 litorderings [0] = split
% 3.28/3.69 litorderings [1] = extend the termordering, first sorting on arguments
% 3.28/3.69
% 3.28/3.69 termordering = kbo
% 3.28/3.69
% 3.28/3.69 litapriori = 0
% 3.28/3.69 termapriori = 1
% 3.28/3.69 litaposteriori = 0
% 3.28/3.69 termaposteriori = 0
% 3.28/3.69 demodaposteriori = 0
% 3.28/3.69 ordereqreflfact = 0
% 3.28/3.69
% 3.28/3.69 litselect = negord
% 3.28/3.69
% 3.28/3.69 maxweight = 15
% 3.28/3.69 maxdepth = 30000
% 3.28/3.69 maxlength = 115
% 3.28/3.69 maxnrvars = 195
% 3.28/3.69 excuselevel = 1
% 3.28/3.69 increasemaxweight = 1
% 3.28/3.69
% 3.28/3.69 maxselected = 10000000
% 3.28/3.69 maxnrclauses = 10000000
% 3.28/3.69
% 3.28/3.69 showgenerated = 0
% 3.28/3.69 showkept = 0
% 3.28/3.69 showselected = 0
% 3.28/3.69 showdeleted = 0
% 3.28/3.69 showresimp = 1
% 3.28/3.69 showstatus = 2000
% 3.28/3.69
% 3.28/3.69 prologoutput = 0
% 3.28/3.69 nrgoals = 5000000
% 3.28/3.69 totalproof = 1
% 3.28/3.69
% 3.28/3.69 Symbols occurring in the translation:
% 3.28/3.69
% 3.28/3.69 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 3.28/3.69 . [1, 2] (w:1, o:47, a:1, s:1, b:0),
% 3.28/3.69 ! [4, 1] (w:0, o:42, a:1, s:1, b:0),
% 3.28/3.69 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.28/3.69 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.28/3.69 coll [38, 3] (w:1, o:75, a:1, s:1, b:0),
% 3.28/3.69 para [40, 4] (w:1, o:83, a:1, s:1, b:0),
% 3.28/3.69 perp [43, 4] (w:1, o:84, a:1, s:1, b:0),
% 3.28/3.69 midp [45, 3] (w:1, o:76, a:1, s:1, b:0),
% 3.28/3.69 cong [47, 4] (w:1, o:85, a:1, s:1, b:0),
% 3.28/3.69 circle [48, 4] (w:1, o:86, a:1, s:1, b:0),
% 3.28/3.69 cyclic [49, 4] (w:1, o:87, a:1, s:1, b:0),
% 3.28/3.69 eqangle [54, 8] (w:1, o:102, a:1, s:1, b:0),
% 3.28/3.69 eqratio [57, 8] (w:1, o:103, a:1, s:1, b:0),
% 3.28/3.69 simtri [59, 6] (w:1, o:99, a:1, s:1, b:0),
% 3.28/3.69 contri [60, 6] (w:1, o:100, a:1, s:1, b:0),
% 3.28/3.69 alpha1 [69, 3] (w:1, o:77, a:1, s:1, b:1),
% 3.28/3.69 alpha2 [70, 4] (w:1, o:88, a:1, s:1, b:1),
% 3.28/3.69 skol1 [71, 4] (w:1, o:89, a:1, s:1, b:1),
% 3.28/3.69 skol2 [72, 4] (w:1, o:91, a:1, s:1, b:1),
% 28.20/28.58 skol3 [73, 4] (w:1, o:93, a:1, s:1, b:1),
% 28.20/28.58 skol4 [74, 4] (w:1, o:94, a:1, s:1, b:1),
% 28.20/28.58 skol5 [75, 4] (w:1, o:95, a:1, s:1, b:1),
% 28.20/28.58 skol6 [76, 6] (w:1, o:101, a:1, s:1, b:1),
% 28.20/28.58 skol7 [77, 2] (w:1, o:71, a:1, s:1, b:1),
% 28.20/28.58 skol8 [78, 4] (w:1, o:96, a:1, s:1, b:1),
% 28.20/28.58 skol9 [79, 4] (w:1, o:97, a:1, s:1, b:1),
% 28.20/28.58 skol10 [80, 3] (w:1, o:78, a:1, s:1, b:1),
% 28.20/28.58 skol11 [81, 3] (w:1, o:79, a:1, s:1, b:1),
% 28.20/28.58 skol12 [82, 2] (w:1, o:72, a:1, s:1, b:1),
% 28.20/28.58 skol13 [83, 5] (w:1, o:98, a:1, s:1, b:1),
% 28.20/28.58 skol14 [84, 3] (w:1, o:80, a:1, s:1, b:1),
% 28.20/28.58 skol15 [85, 3] (w:1, o:81, a:1, s:1, b:1),
% 28.20/28.58 skol16 [86, 3] (w:1, o:82, a:1, s:1, b:1),
% 28.20/28.58 skol17 [87, 2] (w:1, o:73, a:1, s:1, b:1),
% 28.20/28.58 skol18 [88, 2] (w:1, o:74, a:1, s:1, b:1),
% 28.20/28.58 skol19 [89, 4] (w:1, o:90, a:1, s:1, b:1),
% 28.20/28.58 skol20 [90, 0] (w:1, o:29, a:1, s:1, b:1),
% 28.20/28.58 skol21 [91, 4] (w:1, o:92, a:1, s:1, b:1),
% 28.20/28.58 skol22 [92, 0] (w:1, o:30, a:1, s:1, b:1),
% 28.20/28.58 skol23 [93, 0] (w:1, o:31, a:1, s:1, b:1),
% 28.20/28.58 skol24 [94, 0] (w:1, o:32, a:1, s:1, b:1),
% 28.20/28.58 skol25 [95, 0] (w:1, o:33, a:1, s:1, b:1),
% 28.20/28.58 skol26 [96, 0] (w:1, o:34, a:1, s:1, b:1),
% 28.20/28.58 skol27 [97, 0] (w:1, o:35, a:1, s:1, b:1),
% 28.20/28.58 skol28 [98, 0] (w:1, o:36, a:1, s:1, b:1),
% 28.20/28.58 skol29 [99, 0] (w:1, o:37, a:1, s:1, b:1),
% 28.20/28.58 skol30 [100, 0] (w:1, o:38, a:1, s:1, b:1),
% 28.20/28.58 skol31 [101, 0] (w:1, o:39, a:1, s:1, b:1),
% 28.20/28.58 skol32 [102, 0] (w:1, o:40, a:1, s:1, b:1),
% 28.20/28.58 skol33 [103, 0] (w:1, o:41, a:1, s:1, b:1).
% 28.20/28.58
% 28.20/28.58
% 28.20/28.58 Starting Search:
% 28.20/28.58
% 28.20/28.58 *** allocated 15000 integers for clauses
% 28.20/28.58 *** allocated 22500 integers for clauses
% 28.20/28.58 *** allocated 33750 integers for clauses
% 28.20/28.58 *** allocated 50625 integers for clauses
% 28.20/28.58 *** allocated 22500 integers for termspace/termends
% 28.20/28.58 *** allocated 75937 integers for clauses
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 *** allocated 33750 integers for termspace/termends
% 28.20/28.58 *** allocated 113905 integers for clauses
% 28.20/28.58 *** allocated 50625 integers for termspace/termends
% 28.20/28.58
% 28.20/28.58 Intermediate Status:
% 28.20/28.58 Generated: 7742
% 28.20/28.58 Kept: 2006
% 28.20/28.58 Inuse: 306
% 28.20/28.58 Deleted: 0
% 28.20/28.58 Deletedinuse: 0
% 28.20/28.58
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 *** allocated 170857 integers for clauses
% 28.20/28.58 *** allocated 75937 integers for termspace/termends
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 *** allocated 256285 integers for clauses
% 28.20/28.58
% 28.20/28.58 Intermediate Status:
% 28.20/28.58 Generated: 14417
% 28.20/28.58 Kept: 4025
% 28.20/28.58 Inuse: 446
% 28.20/28.58 Deleted: 0
% 28.20/28.58 Deletedinuse: 0
% 28.20/28.58
% 28.20/28.58 *** allocated 113905 integers for termspace/termends
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 *** allocated 384427 integers for clauses
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 *** allocated 170857 integers for termspace/termends
% 28.20/28.58
% 28.20/28.58 Intermediate Status:
% 28.20/28.58 Generated: 27551
% 28.20/28.58 Kept: 6293
% 28.20/28.58 Inuse: 531
% 28.20/28.58 Deleted: 0
% 28.20/28.58 Deletedinuse: 0
% 28.20/28.58
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 *** allocated 576640 integers for clauses
% 28.20/28.58
% 28.20/28.58 Intermediate Status:
% 28.20/28.58 Generated: 38230
% 28.20/28.58 Kept: 8294
% 28.20/28.58 Inuse: 660
% 28.20/28.58 Deleted: 1
% 28.20/28.58 Deletedinuse: 0
% 28.20/28.58
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 *** allocated 256285 integers for termspace/termends
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58
% 28.20/28.58 Intermediate Status:
% 28.20/28.58 Generated: 51763
% 28.20/28.58 Kept: 10294
% 28.20/28.58 Inuse: 781
% 28.20/28.58 Deleted: 3
% 28.20/28.58 Deletedinuse: 1
% 28.20/28.58
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 *** allocated 864960 integers for clauses
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58
% 28.20/28.58 Intermediate Status:
% 28.20/28.58 Generated: 64683
% 28.20/28.58 Kept: 12576
% 28.20/28.58 Inuse: 869
% 28.20/28.58 Deleted: 5
% 28.20/28.58 Deletedinuse: 3
% 28.20/28.58
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58
% 28.20/28.58 Intermediate Status:
% 28.20/28.58 Generated: 80778
% 28.20/28.58 Kept: 14621
% 28.20/28.58 Inuse: 1022
% 28.20/28.58 Deleted: 7
% 28.20/28.58 Deletedinuse: 3
% 28.20/28.58
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 *** allocated 384427 integers for termspace/termends
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58
% 28.20/28.58 Intermediate Status:
% 28.20/28.58 Generated: 94370
% 28.20/28.58 Kept: 16628
% 28.20/28.58 Inuse: 1166
% 28.20/28.58 Deleted: 7
% 28.20/28.58 Deletedinuse: 3
% 28.20/28.58
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 *** allocated 1297440 integers for clauses
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58
% 28.20/28.58 Intermediate Status:
% 28.20/28.58 Generated: 104661
% 28.20/28.58 Kept: 18723
% 28.20/28.58 Inuse: 1275
% 28.20/28.58 Deleted: 9
% 28.20/28.58 Deletedinuse: 3
% 28.20/28.58
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 Resimplifying inuse:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58 Resimplifying clauses:
% 28.20/28.58 Done
% 28.20/28.58
% 28.20/28.58
% 28.20/28.58 Intermediate Status:
% 102.54/102.95 Generated: 113555
% 102.54/102.95 Kept: 20727
% 102.54/102.95 Inuse: 1350
% 102.54/102.95 Deleted: 841
% 102.54/102.95 Deletedinuse: 3
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 121094
% 102.54/102.95 Kept: 22735
% 102.54/102.95 Inuse: 1471
% 102.54/102.95 Deleted: 1684
% 102.54/102.95 Deletedinuse: 842
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 127670
% 102.54/102.95 Kept: 24745
% 102.54/102.95 Inuse: 1568
% 102.54/102.95 Deleted: 1707
% 102.54/102.95 Deletedinuse: 842
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 *** allocated 576640 integers for termspace/termends
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 *** allocated 1946160 integers for clauses
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 133515
% 102.54/102.95 Kept: 26757
% 102.54/102.95 Inuse: 1645
% 102.54/102.95 Deleted: 1770
% 102.54/102.95 Deletedinuse: 842
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 142338
% 102.54/102.95 Kept: 28821
% 102.54/102.95 Inuse: 1759
% 102.54/102.95 Deleted: 1771
% 102.54/102.95 Deletedinuse: 842
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 147776
% 102.54/102.95 Kept: 30835
% 102.54/102.95 Inuse: 1818
% 102.54/102.95 Deleted: 1795
% 102.54/102.95 Deletedinuse: 842
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 154502
% 102.54/102.95 Kept: 32841
% 102.54/102.95 Inuse: 1911
% 102.54/102.95 Deleted: 1797
% 102.54/102.95 Deletedinuse: 842
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 163301
% 102.54/102.95 Kept: 34899
% 102.54/102.95 Inuse: 2019
% 102.54/102.95 Deleted: 1813
% 102.54/102.95 Deletedinuse: 842
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 171619
% 102.54/102.95 Kept: 36957
% 102.54/102.95 Inuse: 2113
% 102.54/102.95 Deleted: 1817
% 102.54/102.95 Deletedinuse: 842
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 179364
% 102.54/102.95 Kept: 38981
% 102.54/102.95 Inuse: 2229
% 102.54/102.95 Deleted: 1827
% 102.54/102.95 Deletedinuse: 842
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 *** allocated 864960 integers for termspace/termends
% 102.54/102.95 Resimplifying clauses:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 188447
% 102.54/102.95 Kept: 40992
% 102.54/102.95 Inuse: 2405
% 102.54/102.95 Deleted: 14752
% 102.54/102.95 Deletedinuse: 847
% 102.54/102.95
% 102.54/102.95 *** allocated 2919240 integers for clauses
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 196295
% 102.54/102.95 Kept: 43004
% 102.54/102.95 Inuse: 2523
% 102.54/102.95 Deleted: 14752
% 102.54/102.95 Deletedinuse: 847
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 203545
% 102.54/102.95 Kept: 45015
% 102.54/102.95 Inuse: 2597
% 102.54/102.95 Deleted: 14752
% 102.54/102.95 Deletedinuse: 847
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 212017
% 102.54/102.95 Kept: 47020
% 102.54/102.95 Inuse: 2671
% 102.54/102.95 Deleted: 14775
% 102.54/102.95 Deletedinuse: 870
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 242292
% 102.54/102.95 Kept: 49207
% 102.54/102.95 Inuse: 2836
% 102.54/102.95 Deleted: 14776
% 102.54/102.95 Deletedinuse: 870
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 246331
% 102.54/102.95 Kept: 51346
% 102.54/102.95 Inuse: 2871
% 102.54/102.95 Deleted: 14777
% 102.54/102.95 Deletedinuse: 871
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 252707
% 102.54/102.95 Kept: 53452
% 102.54/102.95 Inuse: 2906
% 102.54/102.95 Deleted: 14777
% 102.54/102.95 Deletedinuse: 871
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 257541
% 102.54/102.95 Kept: 56126
% 102.54/102.95 Inuse: 2921
% 102.54/102.95 Deleted: 14777
% 102.54/102.95 Deletedinuse: 871
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 261521
% 102.54/102.95 Kept: 58147
% 102.54/102.95 Inuse: 2971
% 102.54/102.95 Deleted: 14781
% 102.54/102.95 Deletedinuse: 871
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 269288
% 102.54/102.95 Kept: 60193
% 102.54/102.95 Inuse: 3036
% 102.54/102.95 Deleted: 14782
% 102.54/102.95 Deletedinuse: 871
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying clauses:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 *** allocated 4378860 integers for clauses
% 102.54/102.95 *** allocated 1297440 integers for termspace/termends
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 277196
% 102.54/102.95 Kept: 62198
% 102.54/102.95 Inuse: 3097
% 102.54/102.95 Deleted: 17276
% 102.54/102.95 Deletedinuse: 871
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 102.54/102.95 Done
% 102.54/102.95
% 102.54/102.95
% 102.54/102.95 Intermediate Status:
% 102.54/102.95 Generated: 283820
% 102.54/102.95 Kept: 64216
% 102.54/102.95 Inuse: 3149
% 102.54/102.95 Deleted: 17276
% 102.54/102.95 Deletedinuse: 871
% 102.54/102.95
% 102.54/102.95 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60
% 214.21/214.60 Intermediate Status:
% 214.21/214.60 Generated: 297288
% 214.21/214.60 Kept: 66225
% 214.21/214.60 Inuse: 3221
% 214.21/214.60 Deleted: 17276
% 214.21/214.60 Deletedinuse: 871
% 214.21/214.60
% 214.21/214.60 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60
% 214.21/214.60 Intermediate Status:
% 214.21/214.60 Generated: 307197
% 214.21/214.60 Kept: 68275
% 214.21/214.60 Inuse: 3306
% 214.21/214.60 Deleted: 17276
% 214.21/214.60 Deletedinuse: 871
% 214.21/214.60
% 214.21/214.60 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60
% 214.21/214.60 Intermediate Status:
% 214.21/214.60 Generated: 312264
% 214.21/214.60 Kept: 70335
% 214.21/214.60 Inuse: 3326
% 214.21/214.60 Deleted: 17276
% 214.21/214.60 Deletedinuse: 871
% 214.21/214.60
% 214.21/214.60 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60
% 214.21/214.60 Intermediate Status:
% 214.21/214.60 Generated: 323124
% 214.21/214.60 Kept: 72809
% 214.21/214.60 Inuse: 3371
% 214.21/214.60 Deleted: 17276
% 214.21/214.60 Deletedinuse: 871
% 214.21/214.60
% 214.21/214.60 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60
% 214.21/214.60 Intermediate Status:
% 214.21/214.60 Generated: 332333
% 214.21/214.60 Kept: 74827
% 214.21/214.60 Inuse: 3419
% 214.21/214.60 Deleted: 17276
% 214.21/214.60 Deletedinuse: 871
% 214.21/214.60
% 214.21/214.60 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60 Resimplifying inuse:
% 214.21/214.60 Done
% 214.21/214.60
% 214.21/214.60
% 214.21/214.60 Intermediate Status:
% 214.21/214.60 Generated: 339211
% 214.21/214.60 Kept: 76866
% 214.21/214.60 Inuse: 3446
% 214.21/214.60 Deleted: 17276
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 352329
% 214.21/214.61 Kept: 78881
% 214.21/214.61 Inuse: 3494
% 214.21/214.61 Deleted: 17276
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 357331
% 214.21/214.61 Kept: 81088
% 214.21/214.61 Inuse: 3506
% 214.21/214.61 Deleted: 17276
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying clauses:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 363346
% 214.21/214.61 Kept: 83090
% 214.21/214.61 Inuse: 3565
% 214.21/214.61 Deleted: 17716
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 376527
% 214.21/214.61 Kept: 85287
% 214.21/214.61 Inuse: 3641
% 214.21/214.61 Deleted: 17716
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 385444
% 214.21/214.61 Kept: 87412
% 214.21/214.61 Inuse: 3686
% 214.21/214.61 Deleted: 17716
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 396809
% 214.21/214.61 Kept: 89415
% 214.21/214.61 Inuse: 3743
% 214.21/214.61 Deleted: 17716
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 *** allocated 1946160 integers for termspace/termends
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 407963
% 214.21/214.61 Kept: 91472
% 214.21/214.61 Inuse: 3791
% 214.21/214.61 Deleted: 17716
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 *** allocated 6568290 integers for clauses
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 414397
% 214.21/214.61 Kept: 94146
% 214.21/214.61 Inuse: 3811
% 214.21/214.61 Deleted: 17716
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 421773
% 214.21/214.61 Kept: 96224
% 214.21/214.61 Inuse: 3841
% 214.21/214.61 Deleted: 17716
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 446441
% 214.21/214.61 Kept: 98300
% 214.21/214.61 Inuse: 3931
% 214.21/214.61 Deleted: 17716
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 468781
% 214.21/214.61 Kept: 100309
% 214.21/214.61 Inuse: 4055
% 214.21/214.61 Deleted: 17716
% 214.21/214.61 Deletedinuse: 871
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying clauses:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 478070
% 214.21/214.61 Kept: 102318
% 214.21/214.61 Inuse: 4124
% 214.21/214.61 Deleted: 18351
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 496011
% 214.21/214.61 Kept: 104319
% 214.21/214.61 Inuse: 4199
% 214.21/214.61 Deleted: 18351
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 508062
% 214.21/214.61 Kept: 106319
% 214.21/214.61 Inuse: 4270
% 214.21/214.61 Deleted: 18351
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 513480
% 214.21/214.61 Kept: 108327
% 214.21/214.61 Inuse: 4313
% 214.21/214.61 Deleted: 18351
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 521939
% 214.21/214.61 Kept: 110356
% 214.21/214.61 Inuse: 4368
% 214.21/214.61 Deleted: 18351
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 530186
% 214.21/214.61 Kept: 112363
% 214.21/214.61 Inuse: 4417
% 214.21/214.61 Deleted: 18351
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 546889
% 214.21/214.61 Kept: 114378
% 214.21/214.61 Inuse: 4522
% 214.21/214.61 Deleted: 18351
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 556692
% 214.21/214.61 Kept: 116410
% 214.21/214.61 Inuse: 4584
% 214.21/214.61 Deleted: 18351
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 565509
% 214.21/214.61 Kept: 118556
% 214.21/214.61 Inuse: 4621
% 214.21/214.61 Deleted: 18351
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 573182
% 214.21/214.61 Kept: 121562
% 214.21/214.61 Inuse: 4646
% 214.21/214.61 Deleted: 18351
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying clauses:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 578615
% 214.21/214.61 Kept: 123593
% 214.21/214.61 Inuse: 4656
% 214.21/214.61 Deleted: 19774
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 583091
% 214.21/214.61 Kept: 125634
% 214.21/214.61 Inuse: 4671
% 214.21/214.61 Deleted: 19774
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 588549
% 214.21/214.61 Kept: 127668
% 214.21/214.61 Inuse: 4708
% 214.21/214.61 Deleted: 19775
% 214.21/214.61 Deletedinuse: 872
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 593348
% 214.21/214.61 Kept: 129699
% 214.21/214.61 Inuse: 4733
% 214.21/214.61 Deleted: 19922
% 214.21/214.61 Deletedinuse: 1019
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 599437
% 214.21/214.61 Kept: 131712
% 214.21/214.61 Inuse: 4778
% 214.21/214.61 Deleted: 19922
% 214.21/214.61 Deletedinuse: 1019
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 612570
% 214.21/214.61 Kept: 133744
% 214.21/214.61 Inuse: 4821
% 214.21/214.61 Deleted: 19922
% 214.21/214.61 Deletedinuse: 1019
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 636039
% 214.21/214.61 Kept: 135760
% 214.21/214.61 Inuse: 4858
% 214.21/214.61 Deleted: 19923
% 214.21/214.61 Deletedinuse: 1020
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 *** allocated 2919240 integers for termspace/termends
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 652448
% 214.21/214.61 Kept: 137809
% 214.21/214.61 Inuse: 4891
% 214.21/214.61 Deleted: 19925
% 214.21/214.61 Deletedinuse: 1022
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 666089
% 214.21/214.61 Kept: 139878
% 214.21/214.61 Inuse: 4911
% 214.21/214.61 Deleted: 19932
% 214.21/214.61 Deletedinuse: 1029
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 *** allocated 9852435 integers for clauses
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying clauses:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 684686
% 214.21/214.61 Kept: 142411
% 214.21/214.61 Inuse: 4935
% 214.21/214.61 Deleted: 26319
% 214.21/214.61 Deletedinuse: 1033
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 691702
% 214.21/214.61 Kept: 144448
% 214.21/214.61 Inuse: 4958
% 214.21/214.61 Deleted: 26429
% 214.21/214.61 Deletedinuse: 1143
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Intermediate Status:
% 214.21/214.61 Generated: 697741
% 214.21/214.61 Kept: 146508
% 214.21/214.61 Inuse: 4982
% 214.21/214.61 Deleted: 26485
% 214.21/214.61 Deletedinuse: 1199
% 214.21/214.61
% 214.21/214.61 Resimplifying inuse:
% 214.21/214.61 Done
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Bliksems!, er is een bewijs:
% 214.21/214.61 % SZS status Theorem
% 214.21/214.61 % SZS output start Refutation
% 214.21/214.61
% 214.21/214.61 (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 214.21/214.61 (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 214.21/214.61 (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z ), coll( Y
% 214.21/214.61 , Z, X ) }.
% 214.21/214.61 (3) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( X, Y, T, Z ) }.
% 214.21/214.61 (4) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( Z, T, X, Y ) }.
% 214.21/214.61 (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T, X, Y ) }.
% 214.21/214.61 (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U, W, Z, T ),
% 214.21/214.61 para( X, Y, Z, T ) }.
% 214.21/214.61 (9) {G0,W15,D2,L3,V6,M3} I { ! para( X, Y, U, W ), ! perp( U, W, Z, T ),
% 214.21/214.61 perp( X, Y, Z, T ) }.
% 214.21/214.61 (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 214.21/214.61 (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T )
% 214.21/214.61 }.
% 214.21/214.61 (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T )
% 214.21/214.61 }.
% 214.21/214.61 (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X, Y, U, W, Z
% 214.21/214.61 , T, U, W ) }.
% 214.21/214.61 (40) {G0,W14,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z, Y,
% 214.21/214.61 T, X, T, Y ) }.
% 214.21/214.61 (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll(
% 214.21/214.61 Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 214.21/214.61 (43) {G0,W29,D2,L5,V6,M5} I { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U, T
% 214.21/214.61 ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T ), cong( X
% 214.21/214.61 , Y, Z, T ) }.
% 214.21/214.61 (56) {G0,W15,D2,L3,V4,M3} I { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T ),
% 214.21/214.61 perp( X, Y, Z, T ) }.
% 214.21/214.61 (63) {G0,W13,D2,L3,V5,M3} I { ! midp( U, X, Y ), ! midp( U, Z, T ), para( X
% 214.21/214.61 , Z, Y, T ) }.
% 214.21/214.61 (69) {G0,W8,D2,L2,V3,M2} I { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 214.21/214.61 (88) {G0,W22,D3,L5,V7,M5} I { ! midp( Z, X, Y ), ! midp( W, T, U ), ! coll
% 214.21/214.61 ( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0 ) }.
% 214.21/214.61 (117) {G0,W4,D2,L1,V0,M1} I { coll( skol20, skol26, skol27 ) }.
% 214.21/214.61 (119) {G0,W4,D2,L1,V0,M1} I { coll( skol22, skol25, skol27 ) }.
% 214.21/214.61 (120) {G0,W4,D2,L1,V0,M1} I { midp( skol28, skol25, skol27 ) }.
% 214.21/214.61 (124) {G0,W4,D2,L1,V0,M1} I { midp( skol31, skol27, skol26 ) }.
% 214.21/214.61 (130) {G0,W5,D2,L1,V0,M1} I { ! para( skol20, skol22, skol23, skol24 ) }.
% 214.21/214.61 (153) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y, Y, Z ), !
% 214.21/214.61 coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 214.21/214.61 (170) {G1,W4,D2,L1,V0,M1} R(119,0) { coll( skol22, skol27, skol25 ) }.
% 214.21/214.61 (171) {G2,W4,D2,L1,V0,M1} R(1,170) { coll( skol27, skol22, skol25 ) }.
% 214.21/214.61 (172) {G1,W4,D2,L1,V0,M1} R(1,119) { coll( skol25, skol22, skol27 ) }.
% 214.21/214.61 (203) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll( X, Y, T ),
% 214.21/214.61 coll( Z, X, T ) }.
% 214.21/214.61 (208) {G2,W8,D2,L2,V3,M2} F(203) { ! coll( X, Y, Z ), coll( Z, X, Z ) }.
% 214.21/214.61 (232) {G1,W10,D2,L2,V4,M2} R(4,3) { ! para( X, Y, Z, T ), para( Z, T, Y, X
% 214.21/214.61 ) }.
% 214.21/214.61 (235) {G1,W4,D2,L1,V0,M1} R(117,1) { coll( skol26, skol20, skol27 ) }.
% 214.21/214.61 (239) {G2,W4,D2,L1,V0,M1} R(235,0) { coll( skol26, skol27, skol20 ) }.
% 214.21/214.61 (242) {G3,W4,D2,L1,V0,M1} R(239,1) { coll( skol27, skol26, skol20 ) }.
% 214.21/214.61 (245) {G4,W4,D2,L1,V0,M1} R(242,0) { coll( skol27, skol20, skol26 ) }.
% 214.21/214.61 (286) {G1,W10,D2,L2,V2,M2} R(8,130) { ! perp( skol20, skol22, X, Y ), !
% 214.21/214.61 perp( X, Y, skol23, skol24 ) }.
% 214.21/214.61 (314) {G1,W15,D2,L3,V6,M3} R(9,7) { ! para( X, Y, Z, T ), perp( X, Y, U, W
% 214.21/214.61 ), ! perp( U, W, Z, T ) }.
% 214.21/214.61 (333) {G1,W4,D2,L1,V0,M1} R(10,120) { midp( skol28, skol27, skol25 ) }.
% 214.21/214.61 (335) {G1,W4,D2,L1,V0,M1} R(10,124) { midp( skol31, skol26, skol27 ) }.
% 214.21/214.61 (405) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), ! cyclic( Y, Z
% 214.21/214.61 , X, T ) }.
% 214.21/214.61 (406) {G1,W10,D2,L2,V4,M2} R(15,14) { ! cyclic( X, Y, Z, T ), cyclic( Y, Z
% 214.21/214.61 , X, T ) }.
% 214.21/214.61 (490) {G5,W4,D2,L1,V0,M1} R(208,245) { coll( skol26, skol27, skol26 ) }.
% 214.21/214.61 (493) {G3,W4,D2,L1,V0,M1} R(208,235) { coll( skol27, skol26, skol27 ) }.
% 214.21/214.61 (503) {G3,W12,D2,L3,V4,M3} R(208,2) { coll( X, Y, X ), ! coll( X, Z, Y ), !
% 214.21/214.61 coll( X, Z, T ) }.
% 214.21/214.61 (505) {G3,W4,D2,L1,V0,M1} R(208,172) { coll( skol27, skol25, skol27 ) }.
% 214.21/214.61 (508) {G3,W4,D2,L1,V0,M1} R(208,171) { coll( skol25, skol27, skol25 ) }.
% 214.21/214.61 (518) {G4,W8,D2,L2,V3,M2} F(503) { coll( X, Y, X ), ! coll( X, Z, Y ) }.
% 214.21/214.61 (534) {G6,W4,D2,L1,V0,M1} R(490,0) { coll( skol26, skol26, skol27 ) }.
% 214.21/214.61 (685) {G4,W4,D2,L1,V0,M1} R(505,0) { coll( skol27, skol27, skol25 ) }.
% 214.21/214.61 (813) {G5,W8,D2,L2,V3,M2} R(518,1) { ! coll( X, Y, Z ), coll( Z, X, X ) }.
% 214.21/214.61 (818) {G6,W8,D2,L2,V3,M2} R(813,1) { coll( X, Y, Y ), ! coll( Z, Y, X ) }.
% 214.21/214.61 (819) {G6,W8,D2,L2,V3,M2} R(813,0) { coll( X, Y, Y ), ! coll( Y, X, Z ) }.
% 214.21/214.61 (834) {G7,W8,D2,L2,V3,M2} R(819,819) { ! coll( X, Y, Z ), coll( X, Y, Y )
% 214.21/214.61 }.
% 214.21/214.61 (837) {G8,W12,D2,L3,V4,M3} R(834,2) { ! coll( X, Y, Z ), ! coll( X, Y, T )
% 214.21/214.61 , coll( T, Y, X ) }.
% 214.21/214.61 (838) {G9,W8,D2,L2,V3,M2} F(837) { ! coll( X, Y, Z ), coll( Z, Y, X ) }.
% 214.21/214.61 (857) {G10,W8,D2,L2,V3,M2} R(838,818) { coll( X, X, Y ), ! coll( Z, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 (869) {G1,W14,D2,L3,V3,M3} R(42,39) { ! coll( X, X, Y ), cyclic( Z, Y, X, X
% 214.21/214.61 ), ! para( X, Z, X, Z ) }.
% 214.21/214.61 (998) {G1,W20,D2,L4,V4,M4} R(43,40);f { ! cyclic( X, Y, Z, X ), ! cyclic( X
% 214.21/214.61 , Y, Z, Y ), ! cyclic( X, Y, Z, T ), cong( X, Y, X, Y ) }.
% 214.21/214.61 (1030) {G2,W15,D2,L3,V3,M3} F(998) { ! cyclic( X, Y, Z, X ), ! cyclic( X, Y
% 214.21/214.61 , Z, Y ), cong( X, Y, X, Y ) }.
% 214.21/214.61 (1073) {G11,W8,D2,L2,V3,M2} R(69,857) { ! midp( X, Y, Z ), coll( Y, Y, Z )
% 214.21/214.61 }.
% 214.21/214.61 (1846) {G1,W20,D2,L4,V6,M4} R(56,8) { ! cong( X, Y, Z, Y ), ! cong( X, T, Z
% 214.21/214.61 , T ), ! perp( U, W, X, Z ), para( U, W, Y, T ) }.
% 214.21/214.61 (1847) {G1,W15,D2,L3,V4,M3} R(56,7) { ! cong( X, Y, Z, Y ), ! cong( X, T, Z
% 214.21/214.61 , T ), perp( Y, T, X, Z ) }.
% 214.21/214.61 (1849) {G2,W15,D2,L3,V5,M3} F(1846) { ! cong( X, Y, Z, Y ), ! perp( T, U, X
% 214.21/214.61 , Z ), para( T, U, Y, Y ) }.
% 214.21/214.61 (2136) {G1,W13,D2,L3,V5,M3} R(63,10) { ! midp( X, Y, Z ), para( Y, T, Z, U
% 214.21/214.61 ), ! midp( X, U, T ) }.
% 214.21/214.61 (2156) {G2,W9,D2,L2,V3,M2} F(2136) { ! midp( X, Y, Z ), para( Y, Z, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 (8637) {G7,W10,D3,L2,V1,M2} R(153,335);r(534) { ! coll( skol27, skol26,
% 214.21/214.61 skol27 ), midp( skol7( skol26, X ), skol26, X ) }.
% 214.21/214.61 (8639) {G5,W10,D3,L2,V1,M2} R(153,333);r(685) { ! coll( skol25, skol27,
% 214.21/214.61 skol25 ), midp( skol7( skol27, X ), skol27, X ) }.
% 214.21/214.61 (20057) {G8,W6,D3,L1,V1,M1} S(8637);r(493) { midp( skol7( skol26, X ),
% 214.21/214.61 skol26, X ) }.
% 214.21/214.61 (20058) {G6,W6,D3,L1,V1,M1} S(8639);r(508) { midp( skol7( skol27, X ),
% 214.21/214.61 skol27, X ) }.
% 214.21/214.61 (20312) {G12,W4,D2,L1,V1,M1} R(20057,1073) { coll( skol26, skol26, X ) }.
% 214.21/214.61 (20425) {G13,W4,D2,L1,V2,M1} R(20312,203);r(20312) { coll( Y, skol26, X )
% 214.21/214.61 }.
% 214.21/214.61 (20444) {G14,W4,D2,L1,V3,M1} R(20425,203);r(20425) { coll( Z, X, Y ) }.
% 214.21/214.61 (20761) {G7,W6,D3,L1,V1,M1} R(20058,10) { midp( skol7( skol27, X ), X,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 (20838) {G15,W10,D3,L2,V2,M2} R(20761,153);r(20444) { ! coll( skol27, X,
% 214.21/214.61 skol27 ), midp( skol7( X, Y ), X, Y ) }.
% 214.21/214.61 (40106) {G16,W6,D3,L1,V2,M1} S(20838);r(20444) { midp( skol7( X, Y ), X, Y
% 214.21/214.61 ) }.
% 214.21/214.61 (40361) {G15,W10,D2,L2,V3,M2} S(869);r(20444) { cyclic( Z, Y, X, X ), !
% 214.21/214.61 para( X, Z, X, Z ) }.
% 214.21/214.61 (46475) {G17,W6,D3,L1,V2,M1} R(40106,10) { midp( skol7( X, Y ), Y, X ) }.
% 214.21/214.61 (127502) {G18,W5,D2,L1,V2,M1} R(2156,46475) { para( X, Y, Y, X ) }.
% 214.21/214.61 (127515) {G19,W5,D2,L1,V2,M1} R(127502,232) { para( X, Y, X, Y ) }.
% 214.21/214.61 (142307) {G20,W5,D2,L1,V3,M1} S(40361);r(127515) { cyclic( Z, Y, X, X ) }.
% 214.21/214.61 (147716) {G21,W5,D2,L1,V3,M1} R(142307,406) { cyclic( X, Y, Z, Y ) }.
% 214.21/214.61 (147717) {G21,W5,D2,L1,V3,M1} R(142307,405) { cyclic( X, Y, Z, X ) }.
% 214.21/214.61 (147733) {G22,W5,D2,L1,V2,M1} R(147716,1030);r(147717) { cong( X, Y, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 (148244) {G23,W5,D2,L1,V3,M1} R(147733,1847);r(147733) { perp( Z, Y, X, X )
% 214.21/214.61 }.
% 214.21/214.61 (148328) {G24,W5,D2,L1,V3,M1} R(148244,1849);r(147733) { para( Z, T, Y, Y )
% 214.21/214.61 }.
% 214.21/214.61 (148333) {G25,W5,D2,L1,V4,M1} R(148244,314);r(148328) { perp( X, Y, T, U )
% 214.21/214.61 }.
% 214.21/214.61 (148336) {G26,W0,D0,L0,V0,M0} R(148244,286);r(148333) { }.
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 % SZS output end Refutation
% 214.21/214.61 found a proof!
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Unprocessed initial clauses:
% 214.21/214.61
% 214.21/214.61 (148338) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 214.21/214.61 (148339) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 214.21/214.61 (148340) {G0,W12,D2,L3,V4,M3} { ! coll( X, T, Y ), ! coll( X, T, Z ), coll
% 214.21/214.61 ( Y, Z, X ) }.
% 214.21/214.61 (148341) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( X, Y, T, Z )
% 214.21/214.61 }.
% 214.21/214.61 (148342) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( Z, T, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 (148343) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! para( U, W, Z, T )
% 214.21/214.61 , para( X, Y, Z, T ) }.
% 214.21/214.61 (148344) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( X, Y, T, Z )
% 214.21/214.61 }.
% 214.21/214.61 (148345) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( Z, T, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 (148346) {G0,W15,D2,L3,V6,M3} { ! perp( X, Y, U, W ), ! perp( U, W, Z, T )
% 214.21/214.61 , para( X, Y, Z, T ) }.
% 214.21/214.61 (148347) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! perp( U, W, Z, T )
% 214.21/214.61 , perp( X, Y, Z, T ) }.
% 214.21/214.61 (148348) {G0,W8,D2,L2,V3,M2} { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 214.21/214.61 (148349) {G0,W15,D2,L3,V4,M3} { ! cong( T, X, T, Y ), ! cong( T, X, T, Z )
% 214.21/214.61 , circle( T, X, Y, Z ) }.
% 214.21/214.61 (148350) {G0,W20,D2,L4,V5,M4} { ! cong( U, X, U, Y ), ! cong( U, X, U, Z )
% 214.21/214.61 , ! cong( U, X, U, T ), cyclic( X, Y, Z, T ) }.
% 214.21/214.61 (148351) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z
% 214.21/214.61 ) }.
% 214.21/214.61 (148352) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T
% 214.21/214.61 ) }.
% 214.21/214.61 (148353) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T
% 214.21/214.61 ) }.
% 214.21/214.61 (148354) {G0,W15,D2,L3,V5,M3} { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y
% 214.21/214.61 , T ), cyclic( X, Y, Z, T ) }.
% 214.21/214.61 (148355) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 214.21/214.61 eqangle( Y, X, Z, T, U, W, V0, V1 ) }.
% 214.21/214.61 (148356) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 214.21/214.61 eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 214.21/214.61 (148357) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 214.21/214.61 eqangle( U, W, V0, V1, X, Y, Z, T ) }.
% 214.21/214.61 (148358) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 214.21/214.61 eqangle( X, Y, U, W, Z, T, V0, V1 ) }.
% 214.21/214.61 (148359) {G0,W27,D2,L3,V12,M3} { ! eqangle( X, Y, Z, T, V2, V3, V4, V5 ),
% 214.21/214.61 ! eqangle( V2, V3, V4, V5, U, W, V0, V1 ), eqangle( X, Y, Z, T, U, W, V0
% 214.21/214.61 , V1 ) }.
% 214.21/214.61 (148360) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( X, Y, T, Z )
% 214.21/214.61 }.
% 214.21/214.61 (148361) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( Z, T, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 (148362) {G0,W15,D2,L3,V6,M3} { ! cong( X, Y, U, W ), ! cong( U, W, Z, T )
% 214.21/214.61 , cong( X, Y, Z, T ) }.
% 214.21/214.61 (148363) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 214.21/214.61 eqratio( Y, X, Z, T, U, W, V0, V1 ) }.
% 214.21/214.61 (148364) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 214.21/214.61 eqratio( Z, T, X, Y, V0, V1, U, W ) }.
% 214.21/214.61 (148365) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 214.21/214.61 eqratio( U, W, V0, V1, X, Y, Z, T ) }.
% 214.21/214.61 (148366) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 214.21/214.61 eqratio( X, Y, U, W, Z, T, V0, V1 ) }.
% 214.21/214.61 (148367) {G0,W27,D2,L3,V12,M3} { ! eqratio( X, Y, Z, T, V2, V3, V4, V5 ),
% 214.21/214.61 ! eqratio( V2, V3, V4, V5, U, W, V0, V1 ), eqratio( X, Y, Z, T, U, W, V0
% 214.21/214.61 , V1 ) }.
% 214.21/214.61 (148368) {G0,W14,D2,L2,V6,M2} { ! simtri( X, Z, Y, T, W, U ), simtri( X, Y
% 214.21/214.61 , Z, T, U, W ) }.
% 214.21/214.61 (148369) {G0,W14,D2,L2,V6,M2} { ! simtri( Y, X, Z, U, T, W ), simtri( X, Y
% 214.21/214.61 , Z, T, U, W ) }.
% 214.21/214.61 (148370) {G0,W14,D2,L2,V6,M2} { ! simtri( T, U, W, X, Y, Z ), simtri( X, Y
% 214.21/214.61 , Z, T, U, W ) }.
% 214.21/214.61 (148371) {G0,W21,D2,L3,V9,M3} { ! simtri( X, Y, Z, V0, V1, V2 ), ! simtri
% 214.21/214.61 ( V0, V1, V2, T, U, W ), simtri( X, Y, Z, T, U, W ) }.
% 214.21/214.61 (148372) {G0,W14,D2,L2,V6,M2} { ! contri( X, Z, Y, T, W, U ), contri( X, Y
% 214.21/214.61 , Z, T, U, W ) }.
% 214.21/214.61 (148373) {G0,W14,D2,L2,V6,M2} { ! contri( Y, X, Z, U, T, W ), contri( X, Y
% 214.21/214.61 , Z, T, U, W ) }.
% 214.21/214.61 (148374) {G0,W14,D2,L2,V6,M2} { ! contri( T, U, W, X, Y, Z ), contri( X, Y
% 214.21/214.61 , Z, T, U, W ) }.
% 214.21/214.61 (148375) {G0,W21,D2,L3,V9,M3} { ! contri( X, Y, Z, V0, V1, V2 ), ! contri
% 214.21/214.61 ( V0, V1, V2, T, U, W ), contri( X, Y, Z, T, U, W ) }.
% 214.21/214.61 (148376) {G0,W14,D2,L2,V6,M2} { ! eqangle( X, Y, U, W, Z, T, U, W ), para
% 214.21/214.61 ( X, Y, Z, T ) }.
% 214.21/214.61 (148377) {G0,W14,D2,L2,V6,M2} { ! para( X, Y, Z, T ), eqangle( X, Y, U, W
% 214.21/214.61 , Z, T, U, W ) }.
% 214.21/214.61 (148378) {G0,W14,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z,
% 214.21/214.61 Y, T, X, T, Y ) }.
% 214.21/214.61 (148379) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y ), coll
% 214.21/214.61 ( Z, T, X ), cyclic( X, Y, Z, T ) }.
% 214.21/214.61 (148380) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y ), !
% 214.21/214.61 coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 214.21/214.61 (148381) {G0,W29,D2,L5,V6,M5} { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U
% 214.21/214.61 , T ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T ), cong
% 214.21/214.61 ( X, Y, Z, T ) }.
% 214.21/214.61 (148382) {G0,W13,D2,L3,V5,M3} { ! midp( Z, U, X ), ! midp( T, U, Y ), para
% 214.21/214.61 ( Z, T, X, Y ) }.
% 214.21/214.61 (148383) {G0,W17,D2,L4,V5,M4} { ! midp( U, X, T ), ! para( U, Z, T, Y ), !
% 214.21/214.61 coll( Z, X, Y ), midp( Z, X, Y ) }.
% 214.21/214.61 (148384) {G0,W14,D2,L2,V3,M2} { ! cong( Z, X, Z, Y ), eqangle( Z, X, X, Y
% 214.21/214.61 , X, Y, Z, Y ) }.
% 214.21/214.61 (148385) {G0,W18,D2,L3,V3,M3} { ! eqangle( Z, X, X, Y, X, Y, Z, Y ), coll
% 214.21/214.61 ( Z, X, Y ), cong( Z, X, Z, Y ) }.
% 214.21/214.61 (148386) {G0,W19,D2,L3,V5,M3} { ! circle( U, X, Y, Z ), ! perp( U, X, X, T
% 214.21/214.61 ), eqangle( X, T, X, Y, Z, X, Z, Y ) }.
% 214.21/214.61 (148387) {G0,W19,D2,L3,V5,M3} { ! circle( Y, X, T, U ), ! eqangle( X, Z, X
% 214.21/214.61 , T, U, X, U, T ), perp( Y, X, X, Z ) }.
% 214.21/214.61 (148388) {G0,W18,D2,L3,V5,M3} { ! circle( T, X, Y, Z ), ! midp( U, Y, Z )
% 214.21/214.61 , eqangle( X, Y, X, Z, T, Y, T, U ) }.
% 214.21/214.61 (148389) {G0,W22,D2,L4,V5,M4} { ! circle( U, T, X, Y ), ! coll( Z, X, Y )
% 214.21/214.61 , ! eqangle( T, X, T, Y, U, X, U, Z ), midp( Z, X, Y ) }.
% 214.21/214.61 (148390) {G0,W14,D2,L3,V4,M3} { ! perp( X, Y, Y, T ), ! midp( Z, X, T ),
% 214.21/214.61 cong( X, Z, Y, Z ) }.
% 214.21/214.61 (148391) {G0,W14,D2,L3,V4,M3} { ! circle( T, X, Y, Z ), ! coll( T, X, Z )
% 214.21/214.61 , perp( X, Y, Y, Z ) }.
% 214.21/214.61 (148392) {G0,W19,D2,L3,V4,M3} { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T
% 214.21/214.61 ), eqangle( X, T, Z, T, Z, T, Z, Y ) }.
% 214.21/214.61 (148393) {G0,W14,D2,L3,V4,M3} { ! midp( T, X, Y ), ! perp( Z, T, X, Y ),
% 214.21/214.61 cong( Z, X, Z, Y ) }.
% 214.21/214.61 (148394) {G0,W15,D2,L3,V4,M3} { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T )
% 214.21/214.61 , perp( X, Y, Z, T ) }.
% 214.21/214.61 (148395) {G0,W20,D2,L4,V4,M4} { ! cong( X, Y, T, Y ), ! cong( X, Z, T, Z )
% 214.21/214.61 , ! cyclic( X, T, Y, Z ), perp( Y, X, X, Z ) }.
% 214.21/214.61 (148396) {G0,W29,D2,L4,V6,M4} { ! eqangle( X, Y, Y, Z, T, U, U, W ), !
% 214.21/214.61 eqangle( X, Z, Y, Z, T, W, U, W ), coll( X, Y, Z ), simtri( X, Y, Z, T, U
% 214.21/214.61 , W ) }.
% 214.21/214.61 (148397) {G0,W16,D2,L2,V6,M2} { ! simtri( X, Y, Z, T, U, W ), eqratio( X,
% 214.21/214.61 Y, X, Z, T, U, T, W ) }.
% 214.21/214.61 (148398) {G0,W16,D2,L2,V6,M2} { ! simtri( X, Y, Z, T, U, W ), eqangle( X,
% 214.21/214.61 Y, Y, Z, T, U, U, W ) }.
% 214.21/214.61 (148399) {G0,W19,D2,L3,V6,M3} { ! simtri( X, Y, Z, T, U, W ), ! cong( X, Y
% 214.21/214.61 , T, U ), contri( X, Y, Z, T, U, W ) }.
% 214.21/214.61 (148400) {G0,W12,D2,L2,V6,M2} { ! contri( X, Y, U, Z, T, W ), cong( X, Y,
% 214.21/214.61 Z, T ) }.
% 214.21/214.61 (148401) {G0,W13,D2,L3,V5,M3} { ! midp( U, X, Y ), ! midp( U, Z, T ), para
% 214.21/214.61 ( X, Z, Y, T ) }.
% 214.21/214.61 (148402) {G0,W18,D2,L4,V5,M4} { ! midp( Z, T, U ), ! para( T, X, U, Y ), !
% 214.21/214.61 para( T, Y, U, X ), midp( Z, X, Y ) }.
% 214.21/214.61 (148403) {G0,W22,D2,L4,V5,M4} { ! para( X, Y, Z, T ), ! coll( U, X, Z ), !
% 214.21/214.61 coll( U, Y, T ), eqratio( U, X, X, Z, U, Y, Y, T ) }.
% 214.21/214.61 (148404) {G0,W9,D2,L2,V3,M2} { ! para( X, Y, X, Z ), coll( X, Y, Z ) }.
% 214.21/214.61 (148405) {G0,W13,D2,L3,V3,M3} { ! cong( X, Y, X, Z ), ! coll( X, Y, Z ),
% 214.21/214.61 midp( X, Y, Z ) }.
% 214.21/214.61 (148406) {G0,W9,D2,L2,V3,M2} { ! midp( X, Y, Z ), cong( X, Y, X, Z ) }.
% 214.21/214.61 (148407) {G0,W8,D2,L2,V3,M2} { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 214.21/214.61 (148408) {G0,W17,D2,L3,V6,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ),
% 214.21/214.61 eqratio( U, X, X, Y, W, Z, Z, T ) }.
% 214.21/214.61 (148409) {G0,W19,D2,L3,V4,M3} { ! eqangle( X, Y, Z, T, Z, T, X, Y ), para
% 214.21/214.61 ( X, Y, Z, T ), perp( X, Y, Z, T ) }.
% 214.21/214.61 (148410) {G0,W19,D2,L3,V4,M3} { ! eqangle( X, Y, Z, T, Z, T, X, Y ), perp
% 214.21/214.61 ( X, Y, Z, T ), para( X, Y, Z, T ) }.
% 214.21/214.61 (148411) {G0,W19,D2,L3,V8,M3} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), !
% 214.21/214.61 para( U, W, V0, V1 ), para( X, Y, Z, T ) }.
% 214.21/214.61 (148412) {G0,W19,D2,L3,V8,M3} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), !
% 214.21/214.61 perp( U, W, V0, V1 ), perp( X, Y, Z, T ) }.
% 214.21/214.61 (148413) {G0,W19,D2,L3,V8,M3} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), !
% 214.21/214.61 cong( U, W, V0, V1 ), cong( X, Y, Z, T ) }.
% 214.21/214.61 (148414) {G0,W22,D3,L3,V6,M3} { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y,
% 214.21/214.61 Z, Y, Z, X, Z ), coll( skol1( U, W, Z, T ), Z, T ) }.
% 214.21/214.61 (148415) {G0,W22,D3,L3,V4,M3} { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y,
% 214.21/214.61 Z, Y, Z, X, Z ), coll( skol1( X, Y, Z, T ), X, Y ) }.
% 214.21/214.61 (148416) {G0,W22,D3,L3,V6,M3} { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z,
% 214.21/214.61 T, Z, T, Z, Y ), coll( skol2( U, W, Z, T ), Z, T ) }.
% 214.21/214.61 (148417) {G0,W22,D3,L3,V4,M3} { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z,
% 214.21/214.61 T, Z, T, Z, Y ), coll( Y, X, skol2( X, Y, Z, T ) ) }.
% 214.21/214.61 (148418) {G0,W22,D3,L3,V6,M3} { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z,
% 214.21/214.61 T, Z, T, Z, Y ), coll( skol3( U, W, Z, T ), Z, T ) }.
% 214.21/214.61 (148419) {G0,W22,D3,L3,V4,M3} { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z,
% 214.21/214.61 T, Z, T, Z, Y ), coll( Y, X, skol3( X, Y, Z, T ) ) }.
% 214.21/214.61 (148420) {G0,W18,D3,L3,V6,M3} { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y )
% 214.21/214.61 , coll( skol4( U, W, Z, T ), Z, T ) }.
% 214.21/214.61 (148421) {G0,W18,D3,L3,V4,M3} { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y )
% 214.21/214.61 , coll( Y, X, skol4( X, Y, Z, T ) ) }.
% 214.21/214.61 (148422) {G0,W22,D3,L3,V6,M3} { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll
% 214.21/214.61 ( X, Y, Z ), cyclic( T, Y, Z, skol5( W, Y, Z, T ) ) }.
% 214.21/214.61 (148423) {G0,W30,D3,L3,V5,M3} { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll
% 214.21/214.61 ( X, Y, Z ), eqangle( X, Z, Y, Z, X, skol5( X, Y, Z, T ), Y, skol5( X, Y
% 214.21/214.61 , Z, T ) ) }.
% 214.21/214.61 (148424) {G0,W18,D3,L3,V10,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ),
% 214.21/214.61 midp( skol6( X, V0, V1, T, V2, V3 ), X, T ) }.
% 214.21/214.61 (148425) {G0,W19,D3,L3,V8,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), para
% 214.21/214.61 ( skol6( X, V0, Z, T, V1, W ), W, X, Z ) }.
% 214.21/214.61 (148426) {G0,W19,D3,L3,V6,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), para
% 214.21/214.61 ( skol6( X, Y, Z, T, U, W ), U, Y, T ) }.
% 214.21/214.61 (148427) {G0,W22,D3,L5,V7,M5} { ! midp( Z, X, Y ), ! midp( W, T, U ), !
% 214.21/214.61 coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0 ) }.
% 214.21/214.61 (148428) {G0,W26,D3,L5,V8,M5} { ! midp( T, X, U ), ! para( X, W, Z, T ), !
% 214.21/214.61 para( X, W, U, Y ), ! coll( W, Y, Z ), coll( skol8( V0, V1, Z, T ), T, Z
% 214.21/214.61 ) }.
% 214.21/214.61 (148429) {G0,W26,D3,L5,V6,M5} { ! midp( T, X, U ), ! para( X, W, Z, T ), !
% 214.21/214.61 para( X, W, U, Y ), ! coll( W, Y, Z ), coll( skol8( X, Y, Z, T ), X, Y )
% 214.21/214.61 }.
% 214.21/214.61 (148430) {G0,W19,D3,L3,V7,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 214.21/214.61 , cong( T, Z, T, skol9( W, V0, Z, T ) ) }.
% 214.21/214.61 (148431) {G0,W19,D3,L3,V6,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 214.21/214.61 , cong( Y, Z, Y, skol9( W, Y, Z, T ) ) }.
% 214.21/214.61 (148432) {G0,W19,D3,L3,V5,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 214.21/214.61 , para( skol9( X, Y, Z, T ), Z, X, Y ) }.
% 214.21/214.61 (148433) {G0,W17,D3,L3,V5,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 214.21/214.61 , coll( skol10( U, Y, Z ), Z, Y ) }.
% 214.21/214.61 (148434) {G0,W18,D3,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 214.21/214.61 , perp( X, skol10( X, Y, Z ), Z, Y ) }.
% 214.21/214.61 (148435) {G0,W14,D2,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 214.21/214.61 , alpha1( X, Y, Z ) }.
% 214.21/214.61 (148436) {G0,W11,D3,L2,V4,M2} { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z
% 214.21/214.61 ), Z, X ) }.
% 214.21/214.61 (148437) {G0,W12,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), perp( Y, skol11( X, Y
% 214.21/214.61 , Z ), Z, X ) }.
% 214.21/214.61 (148438) {G0,W13,D2,L3,V4,M3} { ! coll( T, Z, X ), ! perp( Y, T, Z, X ),
% 214.21/214.61 alpha1( X, Y, Z ) }.
% 214.21/214.61 (148439) {G0,W12,D3,L2,V4,M2} { ! circle( Y, X, Z, T ), perp( skol12( X, Y
% 214.21/214.61 ), X, X, Y ) }.
% 214.21/214.61 (148440) {G0,W28,D3,L5,V8,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 214.21/214.61 ), ! cong( U, X, U, Y ), W = U, alpha2( X, Z, U, skol13( X, V0, Z, V1, U
% 214.21/214.61 ) ) }.
% 214.21/214.61 (148441) {G0,W26,D3,L5,V8,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 214.21/214.61 ), ! cong( U, X, U, Y ), W = U, coll( skol21( V0, Y, T, V1 ), Y, T ) }.
% 214.21/214.61 (148442) {G0,W27,D3,L5,V6,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 214.21/214.61 ), ! cong( U, X, U, Y ), W = U, cong( skol21( X, Y, T, U ), U, U, X )
% 214.21/214.61 }.
% 214.21/214.61 (148443) {G0,W9,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), coll( T, X, Y ) }.
% 214.21/214.61 (148444) {G0,W10,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), cong( T, Z, Z, X )
% 214.21/214.61 }.
% 214.21/214.61 (148445) {G0,W14,D2,L3,V4,M3} { ! coll( T, X, Y ), ! cong( T, Z, Z, X ),
% 214.21/214.61 alpha2( X, Y, Z, T ) }.
% 214.21/214.61 (148446) {G0,W22,D3,L4,V5,M4} { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T
% 214.21/214.61 ), ! midp( U, X, Y ), circle( skol14( X, Y, Z ), X, Y, Z ) }.
% 214.21/214.61 (148447) {G0,W18,D3,L3,V4,M3} { ! perp( X, Z, Z, Y ), ! cyclic( X, Y, Z, T
% 214.21/214.61 ), circle( skol15( X, Y, Z ), X, Y, Z ) }.
% 214.21/214.61 (148448) {G0,W16,D3,L3,V6,M3} { ! perp( X, U, U, T ), ! coll( T, Y, Z ),
% 214.21/214.61 coll( skol16( W, Y, Z ), Y, Z ) }.
% 214.21/214.61 (148449) {G0,W17,D3,L3,V5,M3} { ! perp( X, U, U, T ), ! coll( T, Y, Z ),
% 214.21/214.61 perp( skol16( X, Y, Z ), X, Y, Z ) }.
% 214.21/214.61 (148450) {G0,W20,D3,L4,V5,M4} { ! perp( X, Z, X, Y ), ! perp( Y, X, Y, T )
% 214.21/214.61 , ! midp( U, Z, T ), midp( skol17( X, Y ), X, Y ) }.
% 214.21/214.61 (148451) {G0,W16,D3,L3,V3,M3} { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z )
% 214.21/214.61 , coll( X, Y, skol18( X, Y ) ) }.
% 214.21/214.61 (148452) {G0,W17,D3,L3,V3,M3} { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z )
% 214.21/214.61 , cong( Y, X, Y, skol18( X, Y ) ) }.
% 214.21/214.61 (148453) {G0,W25,D3,L5,V8,M5} { ! para( U, W, X, Y ), ! coll( Z, U, X ), !
% 214.21/214.61 coll( Z, W, Y ), ! coll( T, U, W ), coll( Z, T, skol19( V0, V1, Z, T ) )
% 214.21/214.61 }.
% 214.21/214.61 (148454) {G0,W25,D3,L5,V6,M5} { ! para( U, W, X, Y ), ! coll( Z, U, X ), !
% 214.21/214.61 coll( Z, W, Y ), ! coll( T, U, W ), coll( skol19( X, Y, Z, T ), X, Y )
% 214.21/214.61 }.
% 214.21/214.61 (148455) {G0,W5,D2,L1,V0,M1} { perp( skol20, skol25, skol26, skol27 ) }.
% 214.21/214.61 (148456) {G0,W4,D2,L1,V0,M1} { coll( skol20, skol26, skol27 ) }.
% 214.21/214.61 (148457) {G0,W5,D2,L1,V0,M1} { perp( skol22, skol26, skol25, skol27 ) }.
% 214.21/214.61 (148458) {G0,W4,D2,L1,V0,M1} { coll( skol22, skol25, skol27 ) }.
% 214.21/214.61 (148459) {G0,W4,D2,L1,V0,M1} { midp( skol28, skol25, skol27 ) }.
% 214.21/214.61 (148460) {G0,W5,D2,L1,V0,M1} { perp( skol25, skol27, skol28, skol29 ) }.
% 214.21/214.61 (148461) {G0,W4,D2,L1,V0,M1} { midp( skol30, skol25, skol26 ) }.
% 214.21/214.61 (148462) {G0,W5,D2,L1,V0,M1} { perp( skol25, skol26, skol30, skol29 ) }.
% 214.21/214.61 (148463) {G0,W4,D2,L1,V0,M1} { midp( skol31, skol27, skol26 ) }.
% 214.21/214.61 (148464) {G0,W5,D2,L1,V0,M1} { perp( skol27, skol26, skol31, skol29 ) }.
% 214.21/214.61 (148465) {G0,W4,D2,L1,V0,M1} { coll( skol26, skol22, skol23 ) }.
% 214.21/214.61 (148466) {G0,W5,D2,L1,V0,M1} { circle( skol29, skol26, skol23, skol32 )
% 214.21/214.61 }.
% 214.21/214.61 (148467) {G0,W4,D2,L1,V0,M1} { coll( skol25, skol20, skol24 ) }.
% 214.21/214.61 (148468) {G0,W5,D2,L1,V0,M1} { circle( skol29, skol25, skol24, skol33 )
% 214.21/214.61 }.
% 214.21/214.61 (148469) {G0,W5,D2,L1,V0,M1} { ! para( skol20, skol22, skol23, skol24 )
% 214.21/214.61 }.
% 214.21/214.61
% 214.21/214.61
% 214.21/214.61 Total Proof:
% 214.21/214.61
% 214.21/214.61 subsumption: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent0: (148338) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 214.21/214.61 }.
% 214.21/214.61 parent0: (148339) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Y, X, Z )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T,
% 214.21/214.61 Z ), coll( Y, Z, X ) }.
% 214.21/214.61 parent0: (148340) {G0,W12,D2,L3,V4,M3} { ! coll( X, T, Y ), ! coll( X, T,
% 214.21/214.61 Z ), coll( Y, Z, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (3) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( X, Y
% 214.21/214.61 , T, Z ) }.
% 214.21/214.61 parent0: (148341) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( X, Y
% 214.21/214.61 , T, Z ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (4) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( Z, T
% 214.21/214.61 , X, Y ) }.
% 214.21/214.61 parent0: (148342) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( Z, T
% 214.21/214.61 , X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T
% 214.21/214.61 , X, Y ) }.
% 214.21/214.61 parent0: (148345) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( Z, T
% 214.21/214.61 , X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U,
% 214.21/214.61 W, Z, T ), para( X, Y, Z, T ) }.
% 214.21/214.61 parent0: (148346) {G0,W15,D2,L3,V6,M3} { ! perp( X, Y, U, W ), ! perp( U,
% 214.21/214.61 W, Z, T ), para( X, Y, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 U := U
% 214.21/214.61 W := W
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (9) {G0,W15,D2,L3,V6,M3} I { ! para( X, Y, U, W ), ! perp( U,
% 214.21/214.61 W, Z, T ), perp( X, Y, Z, T ) }.
% 214.21/214.61 parent0: (148347) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! perp( U,
% 214.21/214.61 W, Z, T ), perp( X, Y, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 U := U
% 214.21/214.61 W := W
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y
% 214.21/214.61 ) }.
% 214.21/214.61 parent0: (148348) {G0,W8,D2,L2,V3,M2} { ! midp( Z, Y, X ), midp( Z, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 214.21/214.61 X, Z, Y, T ) }.
% 214.21/214.61 parent0: (148352) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X
% 214.21/214.61 , Z, Y, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 214.21/214.61 Y, X, Z, T ) }.
% 214.21/214.61 parent0: (148353) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Y
% 214.21/214.61 , X, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X
% 214.21/214.61 , Y, U, W, Z, T, U, W ) }.
% 214.21/214.61 parent0: (148377) {G0,W14,D2,L2,V6,M2} { ! para( X, Y, Z, T ), eqangle( X
% 214.21/214.61 , Y, U, W, Z, T, U, W ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 U := U
% 214.21/214.61 W := W
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (40) {G0,W14,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), eqangle
% 214.21/214.61 ( Z, X, Z, Y, T, X, T, Y ) }.
% 214.21/214.61 parent0: (148378) {G0,W14,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), eqangle(
% 214.21/214.61 Z, X, Z, Y, T, X, T, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T,
% 214.21/214.61 Y ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 214.21/214.61 parent0: (148380) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y
% 214.21/214.61 ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (43) {G0,W29,D2,L5,V6,M5} I { ! cyclic( X, Y, U, Z ), ! cyclic
% 214.21/214.61 ( X, Y, U, T ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T
% 214.21/214.61 ), cong( X, Y, Z, T ) }.
% 214.21/214.61 parent0: (148381) {G0,W29,D2,L5,V6,M5} { ! cyclic( X, Y, U, Z ), ! cyclic
% 214.21/214.61 ( X, Y, U, T ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T
% 214.21/214.61 ), cong( X, Y, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 U := U
% 214.21/214.61 W := W
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 3 ==> 3
% 214.21/214.61 4 ==> 4
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (56) {G0,W15,D2,L3,V4,M3} I { ! cong( X, Z, Y, Z ), ! cong( X
% 214.21/214.61 , T, Y, T ), perp( X, Y, Z, T ) }.
% 214.21/214.61 parent0: (148394) {G0,W15,D2,L3,V4,M3} { ! cong( X, Z, Y, Z ), ! cong( X,
% 214.21/214.61 T, Y, T ), perp( X, Y, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (63) {G0,W13,D2,L3,V5,M3} I { ! midp( U, X, Y ), ! midp( U, Z
% 214.21/214.61 , T ), para( X, Z, Y, T ) }.
% 214.21/214.61 parent0: (148401) {G0,W13,D2,L3,V5,M3} { ! midp( U, X, Y ), ! midp( U, Z,
% 214.21/214.61 T ), para( X, Z, Y, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 U := U
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (69) {G0,W8,D2,L2,V3,M2} I { ! midp( X, Y, Z ), coll( X, Y, Z
% 214.21/214.61 ) }.
% 214.21/214.61 parent0: (148407) {G0,W8,D2,L2,V3,M2} { ! midp( X, Y, Z ), coll( X, Y, Z )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (88) {G0,W22,D3,L5,V7,M5} I { ! midp( Z, X, Y ), ! midp( W, T
% 214.21/214.61 , U ), ! coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0
% 214.21/214.61 ) }.
% 214.21/214.61 parent0: (148427) {G0,W22,D3,L5,V7,M5} { ! midp( Z, X, Y ), ! midp( W, T,
% 214.21/214.61 U ), ! coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0 )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 U := U
% 214.21/214.61 W := W
% 214.21/214.61 V0 := V0
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 3 ==> 3
% 214.21/214.61 4 ==> 4
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (117) {G0,W4,D2,L1,V0,M1} I { coll( skol20, skol26, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 parent0: (148456) {G0,W4,D2,L1,V0,M1} { coll( skol20, skol26, skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (119) {G0,W4,D2,L1,V0,M1} I { coll( skol22, skol25, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 parent0: (148458) {G0,W4,D2,L1,V0,M1} { coll( skol22, skol25, skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (120) {G0,W4,D2,L1,V0,M1} I { midp( skol28, skol25, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 parent0: (148459) {G0,W4,D2,L1,V0,M1} { midp( skol28, skol25, skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (124) {G0,W4,D2,L1,V0,M1} I { midp( skol31, skol27, skol26 )
% 214.21/214.61 }.
% 214.21/214.61 parent0: (148463) {G0,W4,D2,L1,V0,M1} { midp( skol31, skol27, skol26 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (130) {G0,W5,D2,L1,V0,M1} I { ! para( skol20, skol22, skol23,
% 214.21/214.61 skol24 ) }.
% 214.21/214.61 parent0: (148469) {G0,W5,D2,L1,V0,M1} { ! para( skol20, skol22, skol23,
% 214.21/214.61 skol24 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 factor: (148920) {G0,W18,D3,L4,V4,M4} { ! midp( X, Y, Z ), ! coll( Y, Y, Z
% 214.21/214.61 ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 214.21/214.61 parent0[0, 1]: (88) {G0,W22,D3,L5,V7,M5} I { ! midp( Z, X, Y ), ! midp( W,
% 214.21/214.61 T, U ), ! coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0
% 214.21/214.61 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := X
% 214.21/214.61 T := Y
% 214.21/214.61 U := Z
% 214.21/214.61 W := X
% 214.21/214.61 V0 := T
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (153) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll(
% 214.21/214.61 Y, Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 214.21/214.61 parent0: (148920) {G0,W18,D3,L4,V4,M4} { ! midp( X, Y, Z ), ! coll( Y, Y,
% 214.21/214.61 Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 3 ==> 3
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148923) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol27, skol25 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (119) {G0,W4,D2,L1,V0,M1} I { coll( skol22, skol25, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol22
% 214.21/214.61 Y := skol25
% 214.21/214.61 Z := skol27
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (170) {G1,W4,D2,L1,V0,M1} R(119,0) { coll( skol22, skol27,
% 214.21/214.61 skol25 ) }.
% 214.21/214.61 parent0: (148923) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol27, skol25 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148924) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol22, skol25 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (170) {G1,W4,D2,L1,V0,M1} R(119,0) { coll( skol22, skol27,
% 214.21/214.61 skol25 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol22
% 214.21/214.61 Y := skol27
% 214.21/214.61 Z := skol25
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (171) {G2,W4,D2,L1,V0,M1} R(1,170) { coll( skol27, skol22,
% 214.21/214.61 skol25 ) }.
% 214.21/214.61 parent0: (148924) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol22, skol25 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148925) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol22, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (119) {G0,W4,D2,L1,V0,M1} I { coll( skol22, skol25, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol22
% 214.21/214.61 Y := skol25
% 214.21/214.61 Z := skol27
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (172) {G1,W4,D2,L1,V0,M1} R(1,119) { coll( skol25, skol22,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 parent0: (148925) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol22, skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148929) {G1,W12,D2,L3,V4,M3} { coll( X, Z, Y ), ! coll( Z, T
% 214.21/214.61 , X ), ! coll( Z, T, Y ) }.
% 214.21/214.61 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent1[2]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 214.21/214.61 ), coll( Y, Z, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := X
% 214.21/214.61 Z := Y
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (203) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll
% 214.21/214.61 ( X, Y, T ), coll( Z, X, T ) }.
% 214.21/214.61 parent0: (148929) {G1,W12,D2,L3,V4,M3} { coll( X, Z, Y ), ! coll( Z, T, X
% 214.21/214.61 ), ! coll( Z, T, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := T
% 214.21/214.61 Z := X
% 214.21/214.61 T := Y
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 2
% 214.21/214.61 1 ==> 0
% 214.21/214.61 2 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 factor: (148931) {G1,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, X, Z )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0, 1]: (203) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), !
% 214.21/214.61 coll( X, Y, T ), coll( Z, X, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := Z
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (208) {G2,W8,D2,L2,V3,M2} F(203) { ! coll( X, Y, Z ), coll( Z
% 214.21/214.61 , X, Z ) }.
% 214.21/214.61 parent0: (148931) {G1,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, X, Z )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148933) {G1,W10,D2,L2,V4,M2} { para( X, Y, T, Z ), ! para( Z
% 214.21/214.61 , T, X, Y ) }.
% 214.21/214.61 parent0[0]: (3) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( X, Y,
% 214.21/214.61 T, Z ) }.
% 214.21/214.61 parent1[1]: (4) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( Z, T,
% 214.21/214.61 X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := T
% 214.21/214.61 Z := X
% 214.21/214.61 T := Y
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (232) {G1,W10,D2,L2,V4,M2} R(4,3) { ! para( X, Y, Z, T ), para
% 214.21/214.61 ( Z, T, Y, X ) }.
% 214.21/214.61 parent0: (148933) {G1,W10,D2,L2,V4,M2} { para( X, Y, T, Z ), ! para( Z, T
% 214.21/214.61 , X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := T
% 214.21/214.61 Z := X
% 214.21/214.61 T := Y
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 1
% 214.21/214.61 1 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148934) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol20, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (117) {G0,W4,D2,L1,V0,M1} I { coll( skol20, skol26, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol20
% 214.21/214.61 Y := skol26
% 214.21/214.61 Z := skol27
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (235) {G1,W4,D2,L1,V0,M1} R(117,1) { coll( skol26, skol20,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 parent0: (148934) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol20, skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148935) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol27, skol20 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (235) {G1,W4,D2,L1,V0,M1} R(117,1) { coll( skol26, skol20,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol26
% 214.21/214.61 Y := skol20
% 214.21/214.61 Z := skol27
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (239) {G2,W4,D2,L1,V0,M1} R(235,0) { coll( skol26, skol27,
% 214.21/214.61 skol20 ) }.
% 214.21/214.61 parent0: (148935) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol27, skol20 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148936) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol26, skol20 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (239) {G2,W4,D2,L1,V0,M1} R(235,0) { coll( skol26, skol27,
% 214.21/214.61 skol20 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol26
% 214.21/214.61 Y := skol27
% 214.21/214.61 Z := skol20
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (242) {G3,W4,D2,L1,V0,M1} R(239,1) { coll( skol27, skol26,
% 214.21/214.61 skol20 ) }.
% 214.21/214.61 parent0: (148936) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol26, skol20 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148937) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol20, skol26 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (242) {G3,W4,D2,L1,V0,M1} R(239,1) { coll( skol27, skol26,
% 214.21/214.61 skol20 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol27
% 214.21/214.61 Y := skol26
% 214.21/214.61 Z := skol20
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (245) {G4,W4,D2,L1,V0,M1} R(242,0) { coll( skol27, skol20,
% 214.21/214.61 skol26 ) }.
% 214.21/214.61 parent0: (148937) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol20, skol26 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148938) {G1,W10,D2,L2,V2,M2} { ! perp( skol20, skol22, X, Y )
% 214.21/214.61 , ! perp( X, Y, skol23, skol24 ) }.
% 214.21/214.61 parent0[0]: (130) {G0,W5,D2,L1,V0,M1} I { ! para( skol20, skol22, skol23,
% 214.21/214.61 skol24 ) }.
% 214.21/214.61 parent1[2]: (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U, W
% 214.21/214.61 , Z, T ), para( X, Y, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := skol20
% 214.21/214.61 Y := skol22
% 214.21/214.61 Z := skol23
% 214.21/214.61 T := skol24
% 214.21/214.61 U := X
% 214.21/214.61 W := Y
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (286) {G1,W10,D2,L2,V2,M2} R(8,130) { ! perp( skol20, skol22,
% 214.21/214.61 X, Y ), ! perp( X, Y, skol23, skol24 ) }.
% 214.21/214.61 parent0: (148938) {G1,W10,D2,L2,V2,M2} { ! perp( skol20, skol22, X, Y ), !
% 214.21/214.61 perp( X, Y, skol23, skol24 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148939) {G1,W15,D2,L3,V6,M3} { ! para( X, Y, Z, T ), perp( X
% 214.21/214.61 , Y, U, W ), ! perp( U, W, Z, T ) }.
% 214.21/214.61 parent0[1]: (9) {G0,W15,D2,L3,V6,M3} I { ! para( X, Y, U, W ), ! perp( U, W
% 214.21/214.61 , Z, T ), perp( X, Y, Z, T ) }.
% 214.21/214.61 parent1[1]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 214.21/214.61 X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := U
% 214.21/214.61 T := W
% 214.21/214.61 U := Z
% 214.21/214.61 W := T
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := U
% 214.21/214.61 Y := W
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (314) {G1,W15,D2,L3,V6,M3} R(9,7) { ! para( X, Y, Z, T ), perp
% 214.21/214.61 ( X, Y, U, W ), ! perp( U, W, Z, T ) }.
% 214.21/214.61 parent0: (148939) {G1,W15,D2,L3,V6,M3} { ! para( X, Y, Z, T ), perp( X, Y
% 214.21/214.61 , U, W ), ! perp( U, W, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 U := U
% 214.21/214.61 W := W
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148940) {G1,W4,D2,L1,V0,M1} { midp( skol28, skol27, skol25 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (120) {G0,W4,D2,L1,V0,M1} I { midp( skol28, skol25, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol27
% 214.21/214.61 Y := skol25
% 214.21/214.61 Z := skol28
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (333) {G1,W4,D2,L1,V0,M1} R(10,120) { midp( skol28, skol27,
% 214.21/214.61 skol25 ) }.
% 214.21/214.61 parent0: (148940) {G1,W4,D2,L1,V0,M1} { midp( skol28, skol27, skol25 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148941) {G1,W4,D2,L1,V0,M1} { midp( skol31, skol26, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (124) {G0,W4,D2,L1,V0,M1} I { midp( skol31, skol27, skol26 )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol26
% 214.21/214.61 Y := skol27
% 214.21/214.61 Z := skol31
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (335) {G1,W4,D2,L1,V0,M1} R(10,124) { midp( skol31, skol26,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 parent0: (148941) {G1,W4,D2,L1,V0,M1} { midp( skol31, skol26, skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148942) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic
% 214.21/214.61 ( X, Z, Y, T ) }.
% 214.21/214.61 parent0[0]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 214.21/214.61 , X, Z, T ) }.
% 214.21/214.61 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 214.21/214.61 , Z, Y, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := Y
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (405) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), !
% 214.21/214.61 cyclic( Y, Z, X, T ) }.
% 214.21/214.61 parent0: (148942) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic( X
% 214.21/214.61 , Z, Y, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148944) {G1,W10,D2,L2,V4,M2} { cyclic( X, Z, Y, T ), ! cyclic
% 214.21/214.61 ( Y, X, Z, T ) }.
% 214.21/214.61 parent0[0]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 214.21/214.61 , Z, Y, T ) }.
% 214.21/214.61 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 214.21/214.61 , X, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (406) {G1,W10,D2,L2,V4,M2} R(15,14) { ! cyclic( X, Y, Z, T ),
% 214.21/214.61 cyclic( Y, Z, X, T ) }.
% 214.21/214.61 parent0: (148944) {G1,W10,D2,L2,V4,M2} { cyclic( X, Z, Y, T ), ! cyclic( Y
% 214.21/214.61 , X, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 1
% 214.21/214.61 1 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148945) {G3,W4,D2,L1,V0,M1} { coll( skol26, skol27, skol26 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (208) {G2,W8,D2,L2,V3,M2} F(203) { ! coll( X, Y, Z ), coll( Z,
% 214.21/214.61 X, Z ) }.
% 214.21/214.61 parent1[0]: (245) {G4,W4,D2,L1,V0,M1} R(242,0) { coll( skol27, skol20,
% 214.21/214.61 skol26 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol27
% 214.21/214.61 Y := skol20
% 214.21/214.61 Z := skol26
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (490) {G5,W4,D2,L1,V0,M1} R(208,245) { coll( skol26, skol27,
% 214.21/214.61 skol26 ) }.
% 214.21/214.61 parent0: (148945) {G3,W4,D2,L1,V0,M1} { coll( skol26, skol27, skol26 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148946) {G2,W4,D2,L1,V0,M1} { coll( skol27, skol26, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (208) {G2,W8,D2,L2,V3,M2} F(203) { ! coll( X, Y, Z ), coll( Z,
% 214.21/214.61 X, Z ) }.
% 214.21/214.61 parent1[0]: (235) {G1,W4,D2,L1,V0,M1} R(117,1) { coll( skol26, skol20,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol26
% 214.21/214.61 Y := skol20
% 214.21/214.61 Z := skol27
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (493) {G3,W4,D2,L1,V0,M1} R(208,235) { coll( skol27, skol26,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 parent0: (148946) {G2,W4,D2,L1,V0,M1} { coll( skol27, skol26, skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148947) {G1,W12,D2,L3,V4,M3} { coll( Z, X, Z ), ! coll( Z, T
% 214.21/214.61 , X ), ! coll( Z, T, Y ) }.
% 214.21/214.61 parent0[0]: (208) {G2,W8,D2,L2,V3,M2} F(203) { ! coll( X, Y, Z ), coll( Z,
% 214.21/214.61 X, Z ) }.
% 214.21/214.61 parent1[2]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 214.21/214.61 ), coll( Y, Z, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := X
% 214.21/214.61 Z := Y
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (503) {G3,W12,D2,L3,V4,M3} R(208,2) { coll( X, Y, X ), ! coll
% 214.21/214.61 ( X, Z, Y ), ! coll( X, Z, T ) }.
% 214.21/214.61 parent0: (148947) {G1,W12,D2,L3,V4,M3} { coll( Z, X, Z ), ! coll( Z, T, X
% 214.21/214.61 ), ! coll( Z, T, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := X
% 214.21/214.61 T := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148949) {G2,W4,D2,L1,V0,M1} { coll( skol27, skol25, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (208) {G2,W8,D2,L2,V3,M2} F(203) { ! coll( X, Y, Z ), coll( Z,
% 214.21/214.61 X, Z ) }.
% 214.21/214.61 parent1[0]: (172) {G1,W4,D2,L1,V0,M1} R(1,119) { coll( skol25, skol22,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol25
% 214.21/214.61 Y := skol22
% 214.21/214.61 Z := skol27
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (505) {G3,W4,D2,L1,V0,M1} R(208,172) { coll( skol27, skol25,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 parent0: (148949) {G2,W4,D2,L1,V0,M1} { coll( skol27, skol25, skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148950) {G3,W4,D2,L1,V0,M1} { coll( skol25, skol27, skol25 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (208) {G2,W8,D2,L2,V3,M2} F(203) { ! coll( X, Y, Z ), coll( Z,
% 214.21/214.61 X, Z ) }.
% 214.21/214.61 parent1[0]: (171) {G2,W4,D2,L1,V0,M1} R(1,170) { coll( skol27, skol22,
% 214.21/214.61 skol25 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol27
% 214.21/214.61 Y := skol22
% 214.21/214.61 Z := skol25
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (508) {G3,W4,D2,L1,V0,M1} R(208,171) { coll( skol25, skol27,
% 214.21/214.61 skol25 ) }.
% 214.21/214.61 parent0: (148950) {G3,W4,D2,L1,V0,M1} { coll( skol25, skol27, skol25 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 factor: (148951) {G3,W8,D2,L2,V3,M2} { coll( X, Y, X ), ! coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent0[1, 2]: (503) {G3,W12,D2,L3,V4,M3} R(208,2) { coll( X, Y, X ), !
% 214.21/214.61 coll( X, Z, Y ), ! coll( X, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := Y
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (518) {G4,W8,D2,L2,V3,M2} F(503) { coll( X, Y, X ), ! coll( X
% 214.21/214.61 , Z, Y ) }.
% 214.21/214.61 parent0: (148951) {G3,W8,D2,L2,V3,M2} { coll( X, Y, X ), ! coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148952) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol26, skol27 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (490) {G5,W4,D2,L1,V0,M1} R(208,245) { coll( skol26, skol27,
% 214.21/214.61 skol26 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol26
% 214.21/214.61 Y := skol27
% 214.21/214.61 Z := skol26
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (534) {G6,W4,D2,L1,V0,M1} R(490,0) { coll( skol26, skol26,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 parent0: (148952) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol26, skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148953) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol27, skol25 )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (505) {G3,W4,D2,L1,V0,M1} R(208,172) { coll( skol27, skol25,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol27
% 214.21/214.61 Y := skol25
% 214.21/214.61 Z := skol27
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (685) {G4,W4,D2,L1,V0,M1} R(505,0) { coll( skol27, skol27,
% 214.21/214.61 skol25 ) }.
% 214.21/214.61 parent0: (148953) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol27, skol25 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148955) {G1,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( X, Z,
% 214.21/214.61 Y ) }.
% 214.21/214.61 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (518) {G4,W8,D2,L2,V3,M2} F(503) { coll( X, Y, X ), ! coll( X,
% 214.21/214.61 Z, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (813) {G5,W8,D2,L2,V3,M2} R(518,1) { ! coll( X, Y, Z ), coll(
% 214.21/214.61 Z, X, X ) }.
% 214.21/214.61 parent0: (148955) {G1,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := Y
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 1
% 214.21/214.61 1 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148956) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( Y, X,
% 214.21/214.61 Z ) }.
% 214.21/214.61 parent0[0]: (813) {G5,W8,D2,L2,V3,M2} R(518,1) { ! coll( X, Y, Z ), coll( Z
% 214.21/214.61 , X, X ) }.
% 214.21/214.61 parent1[1]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (818) {G6,W8,D2,L2,V3,M2} R(813,1) { coll( X, Y, Y ), ! coll(
% 214.21/214.61 Z, Y, X ) }.
% 214.21/214.61 parent0: (148956) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( Y, X, Z )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148957) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( X, Z,
% 214.21/214.61 Y ) }.
% 214.21/214.61 parent0[0]: (813) {G5,W8,D2,L2,V3,M2} R(518,1) { ! coll( X, Y, Z ), coll( Z
% 214.21/214.61 , X, X ) }.
% 214.21/214.61 parent1[1]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := Y
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (819) {G6,W8,D2,L2,V3,M2} R(813,0) { coll( X, Y, Y ), ! coll(
% 214.21/214.61 Y, X, Z ) }.
% 214.21/214.61 parent0: (148957) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( X, Z, Y )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148958) {G7,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! coll( X, Y,
% 214.21/214.61 Z ) }.
% 214.21/214.61 parent0[1]: (819) {G6,W8,D2,L2,V3,M2} R(813,0) { coll( X, Y, Y ), ! coll( Y
% 214.21/214.61 , X, Z ) }.
% 214.21/214.61 parent1[0]: (819) {G6,W8,D2,L2,V3,M2} R(813,0) { coll( X, Y, Y ), ! coll( Y
% 214.21/214.61 , X, Z ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (834) {G7,W8,D2,L2,V3,M2} R(819,819) { ! coll( X, Y, Z ), coll
% 214.21/214.61 ( X, Y, Y ) }.
% 214.21/214.61 parent0: (148958) {G7,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! coll( X, Y, Z )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 1
% 214.21/214.61 1 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148962) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, Y
% 214.21/214.61 , X ), ! coll( X, Y, T ) }.
% 214.21/214.61 parent0[1]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 214.21/214.61 ), coll( Y, Z, X ) }.
% 214.21/214.61 parent1[1]: (834) {G7,W8,D2,L2,V3,M2} R(819,819) { ! coll( X, Y, Z ), coll
% 214.21/214.61 ( X, Y, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := Y
% 214.21/214.61 T := Y
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := T
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (837) {G8,W12,D2,L3,V4,M3} R(834,2) { ! coll( X, Y, Z ), !
% 214.21/214.61 coll( X, Y, T ), coll( T, Y, X ) }.
% 214.21/214.61 parent0: (148962) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, Y, X
% 214.21/214.61 ), ! coll( X, Y, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := T
% 214.21/214.61 T := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 1
% 214.21/214.61 1 ==> 2
% 214.21/214.61 2 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 factor: (148965) {G8,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0, 1]: (837) {G8,W12,D2,L3,V4,M3} R(834,2) { ! coll( X, Y, Z ), !
% 214.21/214.61 coll( X, Y, T ), coll( T, Y, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := Z
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (838) {G9,W8,D2,L2,V3,M2} F(837) { ! coll( X, Y, Z ), coll( Z
% 214.21/214.61 , Y, X ) }.
% 214.21/214.61 parent0: (148965) {G8,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148966) {G7,W8,D2,L2,V3,M2} { coll( Y, Y, X ), ! coll( Z, Y,
% 214.21/214.61 X ) }.
% 214.21/214.61 parent0[0]: (838) {G9,W8,D2,L2,V3,M2} F(837) { ! coll( X, Y, Z ), coll( Z,
% 214.21/214.61 Y, X ) }.
% 214.21/214.61 parent1[0]: (818) {G6,W8,D2,L2,V3,M2} R(813,1) { coll( X, Y, Y ), ! coll( Z
% 214.21/214.61 , Y, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Y
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (857) {G10,W8,D2,L2,V3,M2} R(838,818) { coll( X, X, Y ), !
% 214.21/214.61 coll( Z, X, Y ) }.
% 214.21/214.61 parent0: (148966) {G7,W8,D2,L2,V3,M2} { coll( Y, Y, X ), ! coll( Z, Y, X )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148967) {G1,W14,D2,L3,V3,M3} { ! coll( X, X, Z ), cyclic( Y,
% 214.21/214.61 Z, X, X ), ! para( X, Y, X, Y ) }.
% 214.21/214.61 parent0[0]: (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T, Y
% 214.21/214.61 ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 214.21/214.61 parent1[1]: (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X
% 214.21/214.61 , Y, U, W, Z, T, U, W ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := X
% 214.21/214.61 T := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := X
% 214.21/214.61 T := Y
% 214.21/214.61 U := X
% 214.21/214.61 W := Z
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (869) {G1,W14,D2,L3,V3,M3} R(42,39) { ! coll( X, X, Y ),
% 214.21/214.61 cyclic( Z, Y, X, X ), ! para( X, Z, X, Z ) }.
% 214.21/214.61 parent0: (148967) {G1,W14,D2,L3,V3,M3} { ! coll( X, X, Z ), cyclic( Y, Z,
% 214.21/214.61 X, X ), ! para( X, Y, X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := Y
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148968) {G1,W25,D2,L5,V4,M5} { ! cyclic( X, Y, Z, X ), !
% 214.21/214.61 cyclic( X, Y, Z, Y ), ! cyclic( X, Y, Z, T ), cong( X, Y, X, Y ), !
% 214.21/214.61 cyclic( X, Y, Z, T ) }.
% 214.21/214.61 parent0[3]: (43) {G0,W29,D2,L5,V6,M5} I { ! cyclic( X, Y, U, Z ), ! cyclic
% 214.21/214.61 ( X, Y, U, T ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T
% 214.21/214.61 ), cong( X, Y, Z, T ) }.
% 214.21/214.61 parent1[1]: (40) {G0,W14,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), eqangle(
% 214.21/214.61 Z, X, Z, Y, T, X, T, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := X
% 214.21/214.61 T := Y
% 214.21/214.61 U := Z
% 214.21/214.61 W := T
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 factor: (148970) {G1,W20,D2,L4,V3,M4} { ! cyclic( X, Y, Z, X ), ! cyclic(
% 214.21/214.61 X, Y, Z, Y ), cong( X, Y, X, Y ), ! cyclic( X, Y, Z, X ) }.
% 214.21/214.61 parent0[0, 2]: (148968) {G1,W25,D2,L5,V4,M5} { ! cyclic( X, Y, Z, X ), !
% 214.21/214.61 cyclic( X, Y, Z, Y ), ! cyclic( X, Y, Z, T ), cong( X, Y, X, Y ), !
% 214.21/214.61 cyclic( X, Y, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (998) {G1,W20,D2,L4,V4,M4} R(43,40);f { ! cyclic( X, Y, Z, X )
% 214.21/214.61 , ! cyclic( X, Y, Z, Y ), ! cyclic( X, Y, Z, T ), cong( X, Y, X, Y ) }.
% 214.21/214.61 parent0: (148970) {G1,W20,D2,L4,V3,M4} { ! cyclic( X, Y, Z, X ), ! cyclic
% 214.21/214.61 ( X, Y, Z, Y ), cong( X, Y, X, Y ), ! cyclic( X, Y, Z, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 3
% 214.21/214.61 3 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 factor: (148975) {G1,W15,D2,L3,V3,M3} { ! cyclic( X, Y, Z, X ), ! cyclic(
% 214.21/214.61 X, Y, Z, Y ), cong( X, Y, X, Y ) }.
% 214.21/214.61 parent0[0, 2]: (998) {G1,W20,D2,L4,V4,M4} R(43,40);f { ! cyclic( X, Y, Z, X
% 214.21/214.61 ), ! cyclic( X, Y, Z, Y ), ! cyclic( X, Y, Z, T ), cong( X, Y, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (1030) {G2,W15,D2,L3,V3,M3} F(998) { ! cyclic( X, Y, Z, X ), !
% 214.21/214.61 cyclic( X, Y, Z, Y ), cong( X, Y, X, Y ) }.
% 214.21/214.61 parent0: (148975) {G1,W15,D2,L3,V3,M3} { ! cyclic( X, Y, Z, X ), ! cyclic
% 214.21/214.61 ( X, Y, Z, Y ), cong( X, Y, X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148977) {G1,W8,D2,L2,V3,M2} { coll( X, X, Y ), ! midp( Z, X,
% 214.21/214.61 Y ) }.
% 214.21/214.61 parent0[1]: (857) {G10,W8,D2,L2,V3,M2} R(838,818) { coll( X, X, Y ), ! coll
% 214.21/214.61 ( Z, X, Y ) }.
% 214.21/214.61 parent1[1]: (69) {G0,W8,D2,L2,V3,M2} I { ! midp( X, Y, Z ), coll( X, Y, Z )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := X
% 214.21/214.61 Z := Y
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (1073) {G11,W8,D2,L2,V3,M2} R(69,857) { ! midp( X, Y, Z ),
% 214.21/214.61 coll( Y, Y, Z ) }.
% 214.21/214.61 parent0: (148977) {G1,W8,D2,L2,V3,M2} { coll( X, X, Y ), ! midp( Z, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 1
% 214.21/214.61 1 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148979) {G1,W20,D2,L4,V6,M4} { ! perp( X, Y, Z, T ), para( X
% 214.21/214.61 , Y, U, W ), ! cong( Z, U, T, U ), ! cong( Z, W, T, W ) }.
% 214.21/214.61 parent0[1]: (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U, W
% 214.21/214.61 , Z, T ), para( X, Y, Z, T ) }.
% 214.21/214.61 parent1[2]: (56) {G0,W15,D2,L3,V4,M3} I { ! cong( X, Z, Y, Z ), ! cong( X,
% 214.21/214.61 T, Y, T ), perp( X, Y, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := U
% 214.21/214.61 T := W
% 214.21/214.61 U := Z
% 214.21/214.61 W := T
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := T
% 214.21/214.61 Z := U
% 214.21/214.61 T := W
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (1846) {G1,W20,D2,L4,V6,M4} R(56,8) { ! cong( X, Y, Z, Y ), !
% 214.21/214.61 cong( X, T, Z, T ), ! perp( U, W, X, Z ), para( U, W, Y, T ) }.
% 214.21/214.61 parent0: (148979) {G1,W20,D2,L4,V6,M4} { ! perp( X, Y, Z, T ), para( X, Y
% 214.21/214.61 , U, W ), ! cong( Z, U, T, U ), ! cong( Z, W, T, W ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := U
% 214.21/214.61 Y := W
% 214.21/214.61 Z := X
% 214.21/214.61 T := Z
% 214.21/214.61 U := Y
% 214.21/214.61 W := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 2
% 214.21/214.61 1 ==> 3
% 214.21/214.61 2 ==> 0
% 214.21/214.61 3 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148982) {G1,W15,D2,L3,V4,M3} { perp( Z, T, X, Y ), ! cong( X
% 214.21/214.61 , Z, Y, Z ), ! cong( X, T, Y, T ) }.
% 214.21/214.61 parent0[0]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 214.21/214.61 X, Y ) }.
% 214.21/214.61 parent1[2]: (56) {G0,W15,D2,L3,V4,M3} I { ! cong( X, Z, Y, Z ), ! cong( X,
% 214.21/214.61 T, Y, T ), perp( X, Y, Z, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (1847) {G1,W15,D2,L3,V4,M3} R(56,7) { ! cong( X, Y, Z, Y ), !
% 214.21/214.61 cong( X, T, Z, T ), perp( Y, T, X, Z ) }.
% 214.21/214.61 parent0: (148982) {G1,W15,D2,L3,V4,M3} { perp( Z, T, X, Y ), ! cong( X, Z
% 214.21/214.61 , Y, Z ), ! cong( X, T, Y, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := Y
% 214.21/214.61 T := T
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 2
% 214.21/214.61 1 ==> 0
% 214.21/214.61 2 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 factor: (148984) {G1,W15,D2,L3,V5,M3} { ! cong( X, Y, Z, Y ), ! perp( T, U
% 214.21/214.61 , X, Z ), para( T, U, Y, Y ) }.
% 214.21/214.61 parent0[0, 1]: (1846) {G1,W20,D2,L4,V6,M4} R(56,8) { ! cong( X, Y, Z, Y ),
% 214.21/214.61 ! cong( X, T, Z, T ), ! perp( U, W, X, Z ), para( U, W, Y, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := Y
% 214.21/214.61 U := T
% 214.21/214.61 W := U
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (1849) {G2,W15,D2,L3,V5,M3} F(1846) { ! cong( X, Y, Z, Y ), !
% 214.21/214.61 perp( T, U, X, Z ), para( T, U, Y, Y ) }.
% 214.21/214.61 parent0: (148984) {G1,W15,D2,L3,V5,M3} { ! cong( X, Y, Z, Y ), ! perp( T,
% 214.21/214.61 U, X, Z ), para( T, U, Y, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 U := U
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148986) {G1,W13,D2,L3,V5,M3} { ! midp( X, Y, Z ), para( Y, T
% 214.21/214.61 , Z, U ), ! midp( X, U, T ) }.
% 214.21/214.61 parent0[1]: (63) {G0,W13,D2,L3,V5,M3} I { ! midp( U, X, Y ), ! midp( U, Z,
% 214.21/214.61 T ), para( X, Z, Y, T ) }.
% 214.21/214.61 parent1[1]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := T
% 214.21/214.61 T := U
% 214.21/214.61 U := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := T
% 214.21/214.61 Y := U
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (2136) {G1,W13,D2,L3,V5,M3} R(63,10) { ! midp( X, Y, Z ), para
% 214.21/214.61 ( Y, T, Z, U ), ! midp( X, U, T ) }.
% 214.21/214.61 parent0: (148986) {G1,W13,D2,L3,V5,M3} { ! midp( X, Y, Z ), para( Y, T, Z
% 214.21/214.61 , U ), ! midp( X, U, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := T
% 214.21/214.61 U := U
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 2 ==> 2
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 factor: (148989) {G1,W9,D2,L2,V3,M2} { ! midp( X, Y, Z ), para( Y, Z, Z, Y
% 214.21/214.61 ) }.
% 214.21/214.61 parent0[0, 2]: (2136) {G1,W13,D2,L3,V5,M3} R(63,10) { ! midp( X, Y, Z ),
% 214.21/214.61 para( Y, T, Z, U ), ! midp( X, U, T ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := Z
% 214.21/214.61 U := Y
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (2156) {G2,W9,D2,L2,V3,M2} F(2136) { ! midp( X, Y, Z ), para(
% 214.21/214.61 Y, Z, Z, Y ) }.
% 214.21/214.61 parent0: (148989) {G1,W9,D2,L2,V3,M2} { ! midp( X, Y, Z ), para( Y, Z, Z,
% 214.21/214.61 Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148990) {G2,W14,D3,L3,V1,M3} { ! coll( skol26, skol26, skol27
% 214.21/214.61 ), ! coll( skol27, skol26, skol27 ), midp( skol7( skol26, X ), skol26, X
% 214.21/214.61 ) }.
% 214.21/214.61 parent0[0]: (153) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y
% 214.21/214.61 , Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 214.21/214.61 parent1[0]: (335) {G1,W4,D2,L1,V0,M1} R(10,124) { midp( skol31, skol26,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol31
% 214.21/214.61 Y := skol26
% 214.21/214.61 Z := skol27
% 214.21/214.61 T := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148991) {G3,W10,D3,L2,V1,M2} { ! coll( skol27, skol26, skol27
% 214.21/214.61 ), midp( skol7( skol26, X ), skol26, X ) }.
% 214.21/214.61 parent0[0]: (148990) {G2,W14,D3,L3,V1,M3} { ! coll( skol26, skol26, skol27
% 214.21/214.61 ), ! coll( skol27, skol26, skol27 ), midp( skol7( skol26, X ), skol26, X
% 214.21/214.61 ) }.
% 214.21/214.61 parent1[0]: (534) {G6,W4,D2,L1,V0,M1} R(490,0) { coll( skol26, skol26,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (8637) {G7,W10,D3,L2,V1,M2} R(153,335);r(534) { ! coll( skol27
% 214.21/214.61 , skol26, skol27 ), midp( skol7( skol26, X ), skol26, X ) }.
% 214.21/214.61 parent0: (148991) {G3,W10,D3,L2,V1,M2} { ! coll( skol27, skol26, skol27 )
% 214.21/214.61 , midp( skol7( skol26, X ), skol26, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148992) {G2,W14,D3,L3,V1,M3} { ! coll( skol27, skol27, skol25
% 214.21/214.61 ), ! coll( skol25, skol27, skol25 ), midp( skol7( skol27, X ), skol27, X
% 214.21/214.61 ) }.
% 214.21/214.61 parent0[0]: (153) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y
% 214.21/214.61 , Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 214.21/214.61 parent1[0]: (333) {G1,W4,D2,L1,V0,M1} R(10,120) { midp( skol28, skol27,
% 214.21/214.61 skol25 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol28
% 214.21/214.61 Y := skol27
% 214.21/214.61 Z := skol25
% 214.21/214.61 T := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148993) {G3,W10,D3,L2,V1,M2} { ! coll( skol25, skol27, skol25
% 214.21/214.61 ), midp( skol7( skol27, X ), skol27, X ) }.
% 214.21/214.61 parent0[0]: (148992) {G2,W14,D3,L3,V1,M3} { ! coll( skol27, skol27, skol25
% 214.21/214.61 ), ! coll( skol25, skol27, skol25 ), midp( skol7( skol27, X ), skol27, X
% 214.21/214.61 ) }.
% 214.21/214.61 parent1[0]: (685) {G4,W4,D2,L1,V0,M1} R(505,0) { coll( skol27, skol27,
% 214.21/214.61 skol25 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (8639) {G5,W10,D3,L2,V1,M2} R(153,333);r(685) { ! coll( skol25
% 214.21/214.61 , skol27, skol25 ), midp( skol7( skol27, X ), skol27, X ) }.
% 214.21/214.61 parent0: (148993) {G3,W10,D3,L2,V1,M2} { ! coll( skol25, skol27, skol25 )
% 214.21/214.61 , midp( skol7( skol27, X ), skol27, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148994) {G4,W6,D3,L1,V1,M1} { midp( skol7( skol26, X ),
% 214.21/214.61 skol26, X ) }.
% 214.21/214.61 parent0[0]: (8637) {G7,W10,D3,L2,V1,M2} R(153,335);r(534) { ! coll( skol27
% 214.21/214.61 , skol26, skol27 ), midp( skol7( skol26, X ), skol26, X ) }.
% 214.21/214.61 parent1[0]: (493) {G3,W4,D2,L1,V0,M1} R(208,235) { coll( skol27, skol26,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (20057) {G8,W6,D3,L1,V1,M1} S(8637);r(493) { midp( skol7(
% 214.21/214.61 skol26, X ), skol26, X ) }.
% 214.21/214.61 parent0: (148994) {G4,W6,D3,L1,V1,M1} { midp( skol7( skol26, X ), skol26,
% 214.21/214.61 X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148995) {G4,W6,D3,L1,V1,M1} { midp( skol7( skol27, X ),
% 214.21/214.61 skol27, X ) }.
% 214.21/214.61 parent0[0]: (8639) {G5,W10,D3,L2,V1,M2} R(153,333);r(685) { ! coll( skol25
% 214.21/214.61 , skol27, skol25 ), midp( skol7( skol27, X ), skol27, X ) }.
% 214.21/214.61 parent1[0]: (508) {G3,W4,D2,L1,V0,M1} R(208,171) { coll( skol25, skol27,
% 214.21/214.61 skol25 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (20058) {G6,W6,D3,L1,V1,M1} S(8639);r(508) { midp( skol7(
% 214.21/214.61 skol27, X ), skol27, X ) }.
% 214.21/214.61 parent0: (148995) {G4,W6,D3,L1,V1,M1} { midp( skol7( skol27, X ), skol27,
% 214.21/214.61 X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148996) {G9,W4,D2,L1,V1,M1} { coll( skol26, skol26, X ) }.
% 214.21/214.61 parent0[0]: (1073) {G11,W8,D2,L2,V3,M2} R(69,857) { ! midp( X, Y, Z ), coll
% 214.21/214.61 ( Y, Y, Z ) }.
% 214.21/214.61 parent1[0]: (20057) {G8,W6,D3,L1,V1,M1} S(8637);r(493) { midp( skol7(
% 214.21/214.61 skol26, X ), skol26, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol7( skol26, X )
% 214.21/214.61 Y := skol26
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (20312) {G12,W4,D2,L1,V1,M1} R(20057,1073) { coll( skol26,
% 214.21/214.61 skol26, X ) }.
% 214.21/214.61 parent0: (148996) {G9,W4,D2,L1,V1,M1} { coll( skol26, skol26, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148997) {G2,W8,D2,L2,V2,M2} { ! coll( skol26, skol26, Y ),
% 214.21/214.61 coll( X, skol26, Y ) }.
% 214.21/214.61 parent0[0]: (203) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll(
% 214.21/214.61 X, Y, T ), coll( Z, X, T ) }.
% 214.21/214.61 parent1[0]: (20312) {G12,W4,D2,L1,V1,M1} R(20057,1073) { coll( skol26,
% 214.21/214.61 skol26, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol26
% 214.21/214.61 Y := skol26
% 214.21/214.61 Z := X
% 214.21/214.61 T := Y
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (148999) {G3,W4,D2,L1,V2,M1} { coll( Y, skol26, X ) }.
% 214.21/214.61 parent0[0]: (148997) {G2,W8,D2,L2,V2,M2} { ! coll( skol26, skol26, Y ),
% 214.21/214.61 coll( X, skol26, Y ) }.
% 214.21/214.61 parent1[0]: (20312) {G12,W4,D2,L1,V1,M1} R(20057,1073) { coll( skol26,
% 214.21/214.61 skol26, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (20425) {G13,W4,D2,L1,V2,M1} R(20312,203);r(20312) { coll( Y,
% 214.21/214.61 skol26, X ) }.
% 214.21/214.61 parent0: (148999) {G3,W4,D2,L1,V2,M1} { coll( Y, skol26, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149000) {G2,W8,D2,L2,V3,M2} { ! coll( X, skol26, Z ), coll( Y
% 214.21/214.61 , X, Z ) }.
% 214.21/214.61 parent0[0]: (203) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll(
% 214.21/214.61 X, Y, T ), coll( Z, X, T ) }.
% 214.21/214.61 parent1[0]: (20425) {G13,W4,D2,L1,V2,M1} R(20312,203);r(20312) { coll( Y,
% 214.21/214.61 skol26, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := skol26
% 214.21/214.61 Z := Y
% 214.21/214.61 T := Z
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149002) {G3,W4,D2,L1,V3,M1} { coll( Z, X, Y ) }.
% 214.21/214.61 parent0[0]: (149000) {G2,W8,D2,L2,V3,M2} { ! coll( X, skol26, Z ), coll( Y
% 214.21/214.61 , X, Z ) }.
% 214.21/214.61 parent1[0]: (20425) {G13,W4,D2,L1,V2,M1} R(20312,203);r(20312) { coll( Y,
% 214.21/214.61 skol26, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := Y
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (20444) {G14,W4,D2,L1,V3,M1} R(20425,203);r(20425) { coll( Z,
% 214.21/214.61 X, Y ) }.
% 214.21/214.61 parent0: (149002) {G3,W4,D2,L1,V3,M1} { coll( Z, X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149003) {G1,W6,D3,L1,V1,M1} { midp( skol7( skol27, X ), X,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 parent0[0]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (20058) {G6,W6,D3,L1,V1,M1} S(8639);r(508) { midp( skol7(
% 214.21/214.61 skol27, X ), skol27, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := skol27
% 214.21/214.61 Z := skol7( skol27, X )
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (20761) {G7,W6,D3,L1,V1,M1} R(20058,10) { midp( skol7( skol27
% 214.21/214.61 , X ), X, skol27 ) }.
% 214.21/214.61 parent0: (149003) {G1,W6,D3,L1,V1,M1} { midp( skol7( skol27, X ), X,
% 214.21/214.61 skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149004) {G2,W14,D3,L3,V2,M3} { ! coll( X, X, skol27 ), ! coll
% 214.21/214.61 ( skol27, X, skol27 ), midp( skol7( X, Y ), X, Y ) }.
% 214.21/214.61 parent0[0]: (153) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y
% 214.21/214.61 , Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 214.21/214.61 parent1[0]: (20761) {G7,W6,D3,L1,V1,M1} R(20058,10) { midp( skol7( skol27,
% 214.21/214.61 X ), X, skol27 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol7( skol27, X )
% 214.21/214.61 Y := X
% 214.21/214.61 Z := skol27
% 214.21/214.61 T := Y
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149007) {G3,W10,D3,L2,V2,M2} { ! coll( skol27, X, skol27 ),
% 214.21/214.61 midp( skol7( X, Y ), X, Y ) }.
% 214.21/214.61 parent0[0]: (149004) {G2,W14,D3,L3,V2,M3} { ! coll( X, X, skol27 ), ! coll
% 214.21/214.61 ( skol27, X, skol27 ), midp( skol7( X, Y ), X, Y ) }.
% 214.21/214.61 parent1[0]: (20444) {G14,W4,D2,L1,V3,M1} R(20425,203);r(20425) { coll( Z, X
% 214.21/214.61 , Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := skol27
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (20838) {G15,W10,D3,L2,V2,M2} R(20761,153);r(20444) { ! coll(
% 214.21/214.61 skol27, X, skol27 ), midp( skol7( X, Y ), X, Y ) }.
% 214.21/214.61 parent0: (149007) {G3,W10,D3,L2,V2,M2} { ! coll( skol27, X, skol27 ), midp
% 214.21/214.61 ( skol7( X, Y ), X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149009) {G15,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), X, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent0[0]: (20838) {G15,W10,D3,L2,V2,M2} R(20761,153);r(20444) { ! coll(
% 214.21/214.61 skol27, X, skol27 ), midp( skol7( X, Y ), X, Y ) }.
% 214.21/214.61 parent1[0]: (20444) {G14,W4,D2,L1,V3,M1} R(20425,203);r(20425) { coll( Z, X
% 214.21/214.61 , Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := skol27
% 214.21/214.61 Z := skol27
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (40106) {G16,W6,D3,L1,V2,M1} S(20838);r(20444) { midp( skol7(
% 214.21/214.61 X, Y ), X, Y ) }.
% 214.21/214.61 parent0: (149009) {G15,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149010) {G2,W10,D2,L2,V3,M2} { cyclic( Z, Y, X, X ), ! para(
% 214.21/214.61 X, Z, X, Z ) }.
% 214.21/214.61 parent0[0]: (869) {G1,W14,D2,L3,V3,M3} R(42,39) { ! coll( X, X, Y ), cyclic
% 214.21/214.61 ( Z, Y, X, X ), ! para( X, Z, X, Z ) }.
% 214.21/214.61 parent1[0]: (20444) {G14,W4,D2,L1,V3,M1} R(20425,203);r(20425) { coll( Z, X
% 214.21/214.61 , Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (40361) {G15,W10,D2,L2,V3,M2} S(869);r(20444) { cyclic( Z, Y,
% 214.21/214.61 X, X ), ! para( X, Z, X, Z ) }.
% 214.21/214.61 parent0: (149010) {G2,W10,D2,L2,V3,M2} { cyclic( Z, Y, X, X ), ! para( X,
% 214.21/214.61 Z, X, Z ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 1 ==> 1
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149011) {G1,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), Y, X ) }.
% 214.21/214.61 parent0[0]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 214.21/214.61 }.
% 214.21/214.61 parent1[0]: (40106) {G16,W6,D3,L1,V2,M1} S(20838);r(20444) { midp( skol7( X
% 214.21/214.61 , Y ), X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 Z := skol7( X, Y )
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (46475) {G17,W6,D3,L1,V2,M1} R(40106,10) { midp( skol7( X, Y )
% 214.21/214.61 , Y, X ) }.
% 214.21/214.61 parent0: (149011) {G1,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), Y, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149012) {G3,W5,D2,L1,V2,M1} { para( Y, X, X, Y ) }.
% 214.21/214.61 parent0[0]: (2156) {G2,W9,D2,L2,V3,M2} F(2136) { ! midp( X, Y, Z ), para( Y
% 214.21/214.61 , Z, Z, Y ) }.
% 214.21/214.61 parent1[0]: (46475) {G17,W6,D3,L1,V2,M1} R(40106,10) { midp( skol7( X, Y )
% 214.21/214.61 , Y, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := skol7( X, Y )
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (127502) {G18,W5,D2,L1,V2,M1} R(2156,46475) { para( X, Y, Y, X
% 214.21/214.61 ) }.
% 214.21/214.61 parent0: (149012) {G3,W5,D2,L1,V2,M1} { para( Y, X, X, Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149013) {G2,W5,D2,L1,V2,M1} { para( Y, X, Y, X ) }.
% 214.21/214.61 parent0[0]: (232) {G1,W10,D2,L2,V4,M2} R(4,3) { ! para( X, Y, Z, T ), para
% 214.21/214.61 ( Z, T, Y, X ) }.
% 214.21/214.61 parent1[0]: (127502) {G18,W5,D2,L1,V2,M1} R(2156,46475) { para( X, Y, Y, X
% 214.21/214.61 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Y
% 214.21/214.61 T := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (127515) {G19,W5,D2,L1,V2,M1} R(127502,232) { para( X, Y, X, Y
% 214.21/214.61 ) }.
% 214.21/214.61 parent0: (149013) {G2,W5,D2,L1,V2,M1} { para( Y, X, Y, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Y
% 214.21/214.61 Y := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149014) {G16,W5,D2,L1,V3,M1} { cyclic( X, Y, Z, Z ) }.
% 214.21/214.61 parent0[1]: (40361) {G15,W10,D2,L2,V3,M2} S(869);r(20444) { cyclic( Z, Y, X
% 214.21/214.61 , X ), ! para( X, Z, X, Z ) }.
% 214.21/214.61 parent1[0]: (127515) {G19,W5,D2,L1,V2,M1} R(127502,232) { para( X, Y, X, Y
% 214.21/214.61 ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (142307) {G20,W5,D2,L1,V3,M1} S(40361);r(127515) { cyclic( Z,
% 214.21/214.61 Y, X, X ) }.
% 214.21/214.61 parent0: (149014) {G16,W5,D2,L1,V3,M1} { cyclic( X, Y, Z, Z ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149015) {G2,W5,D2,L1,V3,M1} { cyclic( Y, Z, X, Z ) }.
% 214.21/214.61 parent0[0]: (406) {G1,W10,D2,L2,V4,M2} R(15,14) { ! cyclic( X, Y, Z, T ),
% 214.21/214.61 cyclic( Y, Z, X, T ) }.
% 214.21/214.61 parent1[0]: (142307) {G20,W5,D2,L1,V3,M1} S(40361);r(127515) { cyclic( Z, Y
% 214.21/214.61 , X, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := Z
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := X
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (147716) {G21,W5,D2,L1,V3,M1} R(142307,406) { cyclic( X, Y, Z
% 214.21/214.61 , Y ) }.
% 214.21/214.61 parent0: (149015) {G2,W5,D2,L1,V3,M1} { cyclic( Y, Z, X, Z ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := Z
% 214.21/214.61 Y := X
% 214.21/214.61 Z := Y
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149016) {G2,W5,D2,L1,V3,M1} { cyclic( X, Y, Z, X ) }.
% 214.21/214.61 parent0[1]: (405) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), !
% 214.21/214.61 cyclic( Y, Z, X, T ) }.
% 214.21/214.61 parent1[0]: (142307) {G20,W5,D2,L1,V3,M1} S(40361);r(127515) { cyclic( Z, Y
% 214.21/214.61 , X, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 T := X
% 214.21/214.61 end
% 214.21/214.61 substitution1:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Z
% 214.21/214.61 Z := Y
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 subsumption: (147717) {G21,W5,D2,L1,V3,M1} R(142307,405) { cyclic( X, Y, Z
% 214.21/214.61 , X ) }.
% 214.21/214.61 parent0: (149016) {G2,W5,D2,L1,V3,M1} { cyclic( X, Y, Z, X ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.61 end
% 214.21/214.61 permutation0:
% 214.21/214.61 0 ==> 0
% 214.21/214.61 end
% 214.21/214.61
% 214.21/214.61 resolution: (149018) {G3,W10,D2,L2,V3,M2} { ! cyclic( X, Y, Z, X ), cong(
% 214.21/214.61 X, Y, X, Y ) }.
% 214.21/214.61 parent0[1]: (1030) {G2,W15,D2,L3,V3,M3} F(998) { ! cyclic( X, Y, Z, X ), !
% 214.21/214.61 cyclic( X, Y, Z, Y ), cong( X, Y, X, Y ) }.
% 214.21/214.61 parent1[0]: (147716) {G21,W5,D2,L1,V3,M1} R(142307,406) { cyclic( X, Y, Z,
% 214.21/214.61 Y ) }.
% 214.21/214.61 substitution0:
% 214.21/214.61 X := X
% 214.21/214.61 Y := Y
% 214.21/214.61 Z := Z
% 214.21/214.62 end
% 214.21/214.62 substitution1:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 Z := Z
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 resolution: (149020) {G4,W5,D2,L1,V2,M1} { cong( X, Y, X, Y ) }.
% 214.21/214.62 parent0[0]: (149018) {G3,W10,D2,L2,V3,M2} { ! cyclic( X, Y, Z, X ), cong(
% 214.21/214.62 X, Y, X, Y ) }.
% 214.21/214.62 parent1[0]: (147717) {G21,W5,D2,L1,V3,M1} R(142307,405) { cyclic( X, Y, Z,
% 214.21/214.62 X ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 Z := Z
% 214.21/214.62 end
% 214.21/214.62 substitution1:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 Z := Z
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 subsumption: (147733) {G22,W5,D2,L1,V2,M1} R(147716,1030);r(147717) { cong
% 214.21/214.62 ( X, Y, X, Y ) }.
% 214.21/214.62 parent0: (149020) {G4,W5,D2,L1,V2,M1} { cong( X, Y, X, Y ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 end
% 214.21/214.62 permutation0:
% 214.21/214.62 0 ==> 0
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 resolution: (149021) {G2,W10,D2,L2,V3,M2} { ! cong( X, Z, X, Z ), perp( Y
% 214.21/214.62 , Z, X, X ) }.
% 214.21/214.62 parent0[0]: (1847) {G1,W15,D2,L3,V4,M3} R(56,7) { ! cong( X, Y, Z, Y ), !
% 214.21/214.62 cong( X, T, Z, T ), perp( Y, T, X, Z ) }.
% 214.21/214.62 parent1[0]: (147733) {G22,W5,D2,L1,V2,M1} R(147716,1030);r(147717) { cong(
% 214.21/214.62 X, Y, X, Y ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 Z := X
% 214.21/214.62 T := Z
% 214.21/214.62 end
% 214.21/214.62 substitution1:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 resolution: (149023) {G3,W5,D2,L1,V3,M1} { perp( Z, Y, X, X ) }.
% 214.21/214.62 parent0[0]: (149021) {G2,W10,D2,L2,V3,M2} { ! cong( X, Z, X, Z ), perp( Y
% 214.21/214.62 , Z, X, X ) }.
% 214.21/214.62 parent1[0]: (147733) {G22,W5,D2,L1,V2,M1} R(147716,1030);r(147717) { cong(
% 214.21/214.62 X, Y, X, Y ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Z
% 214.21/214.62 Z := Y
% 214.21/214.62 end
% 214.21/214.62 substitution1:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 subsumption: (148244) {G23,W5,D2,L1,V3,M1} R(147733,1847);r(147733) { perp
% 214.21/214.62 ( Z, Y, X, X ) }.
% 214.21/214.62 parent0: (149023) {G3,W5,D2,L1,V3,M1} { perp( Z, Y, X, X ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 Z := Z
% 214.21/214.62 end
% 214.21/214.62 permutation0:
% 214.21/214.62 0 ==> 0
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 resolution: (149024) {G3,W10,D2,L2,V4,M2} { ! cong( X, Y, X, Y ), para( Z
% 214.21/214.62 , T, Y, Y ) }.
% 214.21/214.62 parent0[1]: (1849) {G2,W15,D2,L3,V5,M3} F(1846) { ! cong( X, Y, Z, Y ), !
% 214.21/214.62 perp( T, U, X, Z ), para( T, U, Y, Y ) }.
% 214.21/214.62 parent1[0]: (148244) {G23,W5,D2,L1,V3,M1} R(147733,1847);r(147733) { perp(
% 214.21/214.62 Z, Y, X, X ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 Z := X
% 214.21/214.62 T := Z
% 214.21/214.62 U := T
% 214.21/214.62 end
% 214.21/214.62 substitution1:
% 214.21/214.62 X := X
% 214.21/214.62 Y := T
% 214.21/214.62 Z := Z
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 resolution: (149025) {G4,W5,D2,L1,V3,M1} { para( Z, T, Y, Y ) }.
% 214.21/214.62 parent0[0]: (149024) {G3,W10,D2,L2,V4,M2} { ! cong( X, Y, X, Y ), para( Z
% 214.21/214.62 , T, Y, Y ) }.
% 214.21/214.62 parent1[0]: (147733) {G22,W5,D2,L1,V2,M1} R(147716,1030);r(147717) { cong(
% 214.21/214.62 X, Y, X, Y ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 Z := Z
% 214.21/214.62 T := T
% 214.21/214.62 end
% 214.21/214.62 substitution1:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 subsumption: (148328) {G24,W5,D2,L1,V3,M1} R(148244,1849);r(147733) { para
% 214.21/214.62 ( Z, T, Y, Y ) }.
% 214.21/214.62 parent0: (149025) {G4,W5,D2,L1,V3,M1} { para( Z, T, Y, Y ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := U
% 214.21/214.62 Y := Y
% 214.21/214.62 Z := Z
% 214.21/214.62 T := T
% 214.21/214.62 end
% 214.21/214.62 permutation0:
% 214.21/214.62 0 ==> 0
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 resolution: (149026) {G2,W10,D2,L2,V5,M2} { ! para( X, Y, Z, Z ), perp( X
% 214.21/214.62 , Y, T, U ) }.
% 214.21/214.62 parent0[2]: (314) {G1,W15,D2,L3,V6,M3} R(9,7) { ! para( X, Y, Z, T ), perp
% 214.21/214.62 ( X, Y, U, W ), ! perp( U, W, Z, T ) }.
% 214.21/214.62 parent1[0]: (148244) {G23,W5,D2,L1,V3,M1} R(147733,1847);r(147733) { perp(
% 214.21/214.62 Z, Y, X, X ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 Z := Z
% 214.21/214.62 T := Z
% 214.21/214.62 U := T
% 214.21/214.62 W := U
% 214.21/214.62 end
% 214.21/214.62 substitution1:
% 214.21/214.62 X := Z
% 214.21/214.62 Y := U
% 214.21/214.62 Z := T
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 resolution: (149027) {G3,W5,D2,L1,V4,M1} { perp( X, Y, T, U ) }.
% 214.21/214.62 parent0[0]: (149026) {G2,W10,D2,L2,V5,M2} { ! para( X, Y, Z, Z ), perp( X
% 214.21/214.62 , Y, T, U ) }.
% 214.21/214.62 parent1[0]: (148328) {G24,W5,D2,L1,V3,M1} R(148244,1849);r(147733) { para(
% 214.21/214.62 Z, T, Y, Y ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 Z := Z
% 214.21/214.62 T := T
% 214.21/214.62 U := U
% 214.21/214.62 end
% 214.21/214.62 substitution1:
% 214.21/214.62 X := W
% 214.21/214.62 Y := Z
% 214.21/214.62 Z := X
% 214.21/214.62 T := Y
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 subsumption: (148333) {G25,W5,D2,L1,V4,M1} R(148244,314);r(148328) { perp(
% 214.21/214.62 X, Y, T, U ) }.
% 214.21/214.62 parent0: (149027) {G3,W5,D2,L1,V4,M1} { perp( X, Y, T, U ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 Y := Y
% 214.21/214.62 Z := W
% 214.21/214.62 T := T
% 214.21/214.62 U := U
% 214.21/214.62 end
% 214.21/214.62 permutation0:
% 214.21/214.62 0 ==> 0
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 resolution: (149028) {G2,W5,D2,L1,V1,M1} { ! perp( X, X, skol23, skol24 )
% 214.21/214.62 }.
% 214.21/214.62 parent0[0]: (286) {G1,W10,D2,L2,V2,M2} R(8,130) { ! perp( skol20, skol22, X
% 214.21/214.62 , Y ), ! perp( X, Y, skol23, skol24 ) }.
% 214.21/214.62 parent1[0]: (148244) {G23,W5,D2,L1,V3,M1} R(147733,1847);r(147733) { perp(
% 214.21/214.62 Z, Y, X, X ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 Y := X
% 214.21/214.62 end
% 214.21/214.62 substitution1:
% 214.21/214.62 X := X
% 214.21/214.62 Y := skol22
% 214.21/214.62 Z := skol20
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 resolution: (149029) {G3,W0,D0,L0,V0,M0} { }.
% 214.21/214.62 parent0[0]: (149028) {G2,W5,D2,L1,V1,M1} { ! perp( X, X, skol23, skol24 )
% 214.21/214.62 }.
% 214.21/214.62 parent1[0]: (148333) {G25,W5,D2,L1,V4,M1} R(148244,314);r(148328) { perp( X
% 214.21/214.62 , Y, T, U ) }.
% 214.21/214.62 substitution0:
% 214.21/214.62 X := X
% 214.21/214.62 end
% 214.21/214.62 substitution1:
% 214.21/214.62 X := X
% 214.21/214.62 Y := X
% 214.21/214.62 Z := Y
% 214.21/214.62 T := skol23
% 214.21/214.62 U := skol24
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 subsumption: (148336) {G26,W0,D0,L0,V0,M0} R(148244,286);r(148333) { }.
% 214.21/214.62 parent0: (149029) {G3,W0,D0,L0,V0,M0} { }.
% 214.21/214.62 substitution0:
% 214.21/214.62 end
% 214.21/214.62 permutation0:
% 214.21/214.62 end
% 214.21/214.62
% 214.21/214.62 Proof check complete!
% 214.21/214.62
% 214.21/214.62 Memory use:
% 214.21/214.62
% 214.21/214.62 space for terms: 2086141
% 214.21/214.62 space for clauses: 6877137
% 214.21/214.62
% 214.21/214.62
% 214.21/214.62 clauses generated: 704023
% 214.21/214.62 clauses kept: 148337
% 214.21/214.62 clauses selected: 5010
% 214.21/214.62 clauses deleted: 26761
% 214.21/214.62 clauses inuse deleted: 1469
% 214.21/214.62
% 214.21/214.62 subsentry: 29130603
% 214.21/214.62 literals s-matched: 19791947
% 214.21/214.62 literals matched: 10494616
% 214.21/214.62 full subsumption: 5539788
% 214.21/214.62
% 214.21/214.62 checksum: 2130025529
% 214.21/214.62
% 214.21/214.62
% 214.21/214.62 Bliksem ended
%------------------------------------------------------------------------------