%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GEO593+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n032.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:54:57 EDT 2022
% Result : Theorem 37.82s 38.20s
% Output : Refutation 37.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : GEO593+1 : TPTP v8.1.0. Released v7.5.0.
% 0.00/0.10 % Command : bliksem %s
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % DateTime : Fri Jun 17 21:22:46 EDT 2022
% 0.10/0.29 % CPUTime :
% 0.54/0.97 *** allocated 10000 integers for termspace/termends
% 0.54/0.97 *** allocated 10000 integers for clauses
% 0.54/0.97 *** allocated 10000 integers for justifications
% 0.54/0.97 Bliksem 1.12
% 0.54/0.97
% 0.54/0.97
% 0.54/0.97 Automatic Strategy Selection
% 0.54/0.97
% 0.54/0.97 *** allocated 15000 integers for termspace/termends
% 0.54/0.97
% 0.54/0.97 Clauses:
% 0.54/0.97
% 0.54/0.97 { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 0.54/0.97 { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 0.54/0.97 { ! coll( X, T, Y ), ! coll( X, T, Z ), coll( Y, Z, X ) }.
% 0.54/0.97 { ! para( X, Y, Z, T ), para( X, Y, T, Z ) }.
% 0.54/0.97 { ! para( X, Y, Z, T ), para( Z, T, X, Y ) }.
% 0.54/0.97 { ! para( X, Y, U, W ), ! para( U, W, Z, T ), para( X, Y, Z, T ) }.
% 0.54/0.97 { ! perp( X, Y, Z, T ), perp( X, Y, T, Z ) }.
% 0.54/0.97 { ! perp( X, Y, Z, T ), perp( Z, T, X, Y ) }.
% 0.54/0.97 { ! perp( X, Y, U, W ), ! perp( U, W, Z, T ), para( X, Y, Z, T ) }.
% 0.54/0.97 { ! para( X, Y, U, W ), ! perp( U, W, Z, T ), perp( X, Y, Z, T ) }.
% 0.54/0.97 { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 0.54/0.97 { ! cong( T, X, T, Y ), ! cong( T, X, T, Z ), circle( T, X, Y, Z ) }.
% 0.54/0.97 { ! cong( U, X, U, Y ), ! cong( U, X, U, Z ), ! cong( U, X, U, T ), cyclic
% 0.54/0.97 ( X, Y, Z, T ) }.
% 0.54/0.97 { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z ) }.
% 0.54/0.97 { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T ) }.
% 0.54/0.97 { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T ) }.
% 0.54/0.97 { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 0.54/0.97 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( Y, X, Z, T, U, W, V0, V1
% 0.54/0.97 ) }.
% 0.54/0.97 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( Z, T, X, Y, V0, V1, U, W
% 0.54/0.97 ) }.
% 0.54/0.97 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( U, W, V0, V1, X, Y, Z, T
% 0.54/0.97 ) }.
% 0.54/0.97 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( X, Y, U, W, Z, T, V0, V1
% 0.54/0.97 ) }.
% 0.54/0.97 { ! eqangle( X, Y, Z, T, V2, V3, V4, V5 ), ! eqangle( V2, V3, V4, V5, U, W
% 0.54/0.97 , V0, V1 ), eqangle( X, Y, Z, T, U, W, V0, V1 ) }.
% 0.54/0.97 { ! cong( X, Y, Z, T ), cong( X, Y, T, Z ) }.
% 0.54/0.97 { ! cong( X, Y, Z, T ), cong( Z, T, X, Y ) }.
% 0.54/0.97 { ! cong( X, Y, U, W ), ! cong( U, W, Z, T ), cong( X, Y, Z, T ) }.
% 0.54/0.97 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( Y, X, Z, T, U, W, V0, V1
% 0.54/0.97 ) }.
% 0.54/0.97 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( Z, T, X, Y, V0, V1, U, W
% 0.54/0.97 ) }.
% 0.54/0.97 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( U, W, V0, V1, X, Y, Z, T
% 0.54/0.97 ) }.
% 0.54/0.97 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( X, Y, U, W, Z, T, V0, V1
% 0.54/0.97 ) }.
% 0.54/0.97 { ! eqratio( X, Y, Z, T, V2, V3, V4, V5 ), ! eqratio( V2, V3, V4, V5, U, W
% 0.54/0.97 , V0, V1 ), eqratio( X, Y, Z, T, U, W, V0, V1 ) }.
% 0.54/0.97 { ! simtri( X, Z, Y, T, W, U ), simtri( X, Y, Z, T, U, W ) }.
% 0.54/0.97 { ! simtri( Y, X, Z, U, T, W ), simtri( X, Y, Z, T, U, W ) }.
% 0.54/0.97 { ! simtri( T, U, W, X, Y, Z ), simtri( X, Y, Z, T, U, W ) }.
% 0.54/0.97 { ! simtri( X, Y, Z, V0, V1, V2 ), ! simtri( V0, V1, V2, T, U, W ), simtri
% 0.54/0.97 ( X, Y, Z, T, U, W ) }.
% 0.54/0.97 { ! contri( X, Z, Y, T, W, U ), contri( X, Y, Z, T, U, W ) }.
% 0.54/0.97 { ! contri( Y, X, Z, U, T, W ), contri( X, Y, Z, T, U, W ) }.
% 0.54/0.97 { ! contri( T, U, W, X, Y, Z ), contri( X, Y, Z, T, U, W ) }.
% 0.54/0.97 { ! contri( X, Y, Z, V0, V1, V2 ), ! contri( V0, V1, V2, T, U, W ), contri
% 0.54/0.97 ( X, Y, Z, T, U, W ) }.
% 0.54/0.97 { ! eqangle( X, Y, U, W, Z, T, U, W ), para( X, Y, Z, T ) }.
% 0.54/0.97 { ! para( X, Y, Z, T ), eqangle( X, Y, U, W, Z, T, U, W ) }.
% 0.54/0.97 { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z, Y, T, X, T, Y ) }.
% 0.54/0.97 { ! eqangle( Z, X, Z, Y, T, X, T, Y ), coll( Z, T, X ), cyclic( X, Y, Z, T
% 0.54/0.97 ) }.
% 0.54/0.97 { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll( Z, T, Y ), cyclic( X, Y, Z,
% 0.54/0.97 T ) }.
% 0.54/0.97 { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U, T ), ! cyclic( X, Y, U, W ), !
% 0.54/0.97 eqangle( U, X, U, Y, W, Z, W, T ), cong( X, Y, Z, T ) }.
% 0.54/0.97 { ! midp( Z, U, X ), ! midp( T, U, Y ), para( Z, T, X, Y ) }.
% 0.54/0.97 { ! midp( U, X, T ), ! para( U, Z, T, Y ), ! coll( Z, X, Y ), midp( Z, X, Y
% 0.54/0.97 ) }.
% 0.54/0.97 { ! cong( Z, X, Z, Y ), eqangle( Z, X, X, Y, X, Y, Z, Y ) }.
% 0.54/0.97 { ! eqangle( Z, X, X, Y, X, Y, Z, Y ), coll( Z, X, Y ), cong( Z, X, Z, Y )
% 0.54/0.97 }.
% 0.54/0.97 { ! circle( U, X, Y, Z ), ! perp( U, X, X, T ), eqangle( X, T, X, Y, Z, X,
% 0.54/0.97 Z, Y ) }.
% 0.54/0.97 { ! circle( Y, X, T, U ), ! eqangle( X, Z, X, T, U, X, U, T ), perp( Y, X,
% 0.54/0.97 X, Z ) }.
% 0.54/0.97 { ! circle( T, X, Y, Z ), ! midp( U, Y, Z ), eqangle( X, Y, X, Z, T, Y, T,
% 0.54/0.97 U ) }.
% 0.54/0.97 { ! circle( U, T, X, Y ), ! coll( Z, X, Y ), ! eqangle( T, X, T, Y, U, X, U
% 0.54/0.97 , Z ), midp( Z, X, Y ) }.
% 0.54/0.97 { ! perp( X, Y, Y, T ), ! midp( Z, X, T ), cong( X, Z, Y, Z ) }.
% 0.54/0.97 { ! circle( T, X, Y, Z ), ! coll( T, X, Z ), perp( X, Y, Y, Z ) }.
% 0.54/0.97 { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T ), eqangle( X, T, Z, T, Z, T,
% 0.54/0.97 Z, Y ) }.
% 0.54/0.97 { ! midp( T, X, Y ), ! perp( Z, T, X, Y ), cong( Z, X, Z, Y ) }.
% 0.54/0.97 { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T ), perp( X, Y, Z, T ) }.
% 0.54/0.97 { ! cong( X, Y, T, Y ), ! cong( X, Z, T, Z ), ! cyclic( X, T, Y, Z ), perp
% 0.54/0.97 ( Y, X, X, Z ) }.
% 0.54/0.97 { ! eqangle( X, Y, Y, Z, T, U, U, W ), ! eqangle( X, Z, Y, Z, T, W, U, W )
% 0.54/0.97 , coll( X, Y, Z ), simtri( X, Y, Z, T, U, W ) }.
% 0.54/0.97 { ! simtri( X, Y, Z, T, U, W ), eqratio( X, Y, X, Z, T, U, T, W ) }.
% 0.54/0.97 { ! simtri( X, Y, Z, T, U, W ), eqangle( X, Y, Y, Z, T, U, U, W ) }.
% 0.54/0.97 { ! simtri( X, Y, Z, T, U, W ), ! cong( X, Y, T, U ), contri( X, Y, Z, T, U
% 0.54/0.97 , W ) }.
% 0.54/0.97 { ! contri( X, Y, U, Z, T, W ), cong( X, Y, Z, T ) }.
% 0.54/0.97 { ! midp( U, X, Y ), ! midp( U, Z, T ), para( X, Z, Y, T ) }.
% 0.54/0.97 { ! midp( Z, T, U ), ! para( T, X, U, Y ), ! para( T, Y, U, X ), midp( Z, X
% 0.54/0.97 , Y ) }.
% 0.54/0.97 { ! para( X, Y, Z, T ), ! coll( U, X, Z ), ! coll( U, Y, T ), eqratio( U, X
% 0.54/0.97 , X, Z, U, Y, Y, T ) }.
% 0.54/0.97 { ! para( X, Y, X, Z ), coll( X, Y, Z ) }.
% 0.54/0.97 { ! cong( X, Y, X, Z ), ! coll( X, Y, Z ), midp( X, Y, Z ) }.
% 0.54/0.97 { ! midp( X, Y, Z ), cong( X, Y, X, Z ) }.
% 0.54/0.97 { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 0.54/0.97 { ! midp( U, X, Y ), ! midp( W, Z, T ), eqratio( U, X, X, Y, W, Z, Z, T ) }
% 0.54/0.97 .
% 0.54/0.97 { ! eqangle( X, Y, Z, T, Z, T, X, Y ), para( X, Y, Z, T ), perp( X, Y, Z, T
% 0.54/0.97 ) }.
% 0.54/0.97 { ! eqangle( X, Y, Z, T, Z, T, X, Y ), perp( X, Y, Z, T ), para( X, Y, Z, T
% 0.54/0.97 ) }.
% 0.54/0.97 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), ! para( U, W, V0, V1 ), para( X, Y
% 0.54/0.97 , Z, T ) }.
% 0.54/0.97 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), ! perp( U, W, V0, V1 ), perp( X, Y
% 0.54/0.97 , Z, T ) }.
% 0.54/0.97 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), ! cong( U, W, V0, V1 ), cong( X, Y
% 0.54/0.97 , Z, T ) }.
% 0.54/0.97 { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z, Y, Z, X, Z ), coll( skol1( U
% 0.54/0.97 , W, Z, T ), Z, T ) }.
% 0.54/0.97 { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z, Y, Z, X, Z ), coll( skol1( X
% 0.54/0.97 , Y, Z, T ), X, Y ) }.
% 0.54/0.97 { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( skol2( U
% 0.54/0.97 , W, Z, T ), Z, T ) }.
% 0.54/0.97 { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( Y, X,
% 0.54/0.97 skol2( X, Y, Z, T ) ) }.
% 0.54/0.97 { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( skol3( U
% 0.54/0.97 , W, Z, T ), Z, T ) }.
% 0.54/0.97 { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( Y, X,
% 0.54/0.97 skol3( X, Y, Z, T ) ) }.
% 0.54/0.97 { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y ), coll( skol4( U, W, Z, T ), Z
% 0.54/0.97 , T ) }.
% 0.54/0.97 { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y ), coll( Y, X, skol4( X, Y, Z, T
% 0.54/0.97 ) ) }.
% 0.54/0.97 { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll( X, Y, Z ), cyclic( T, Y, Z,
% 0.54/0.97 skol5( W, Y, Z, T ) ) }.
% 0.54/0.97 { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll( X, Y, Z ), eqangle( X, Z, Y, Z
% 0.54/0.97 , X, skol5( X, Y, Z, T ), Y, skol5( X, Y, Z, T ) ) }.
% 0.54/0.97 { ! midp( U, X, Y ), ! midp( W, Z, T ), midp( skol6( X, V0, V1, T, V2, V3 )
% 0.54/0.97 , X, T ) }.
% 0.54/0.97 { ! midp( U, X, Y ), ! midp( W, Z, T ), para( skol6( X, V0, Z, T, V1, W ),
% 0.54/0.97 W, X, Z ) }.
% 0.54/0.97 { ! midp( U, X, Y ), ! midp( W, Z, T ), para( skol6( X, Y, Z, T, U, W ), U
% 0.54/0.97 , Y, T ) }.
% 0.54/0.97 { ! midp( Z, X, Y ), ! midp( W, T, U ), ! coll( T, X, Y ), ! coll( U, X, Y
% 0.54/0.97 ), midp( skol7( X, V0 ), X, V0 ) }.
% 0.54/0.97 { ! midp( T, X, U ), ! para( X, W, Z, T ), ! para( X, W, U, Y ), ! coll( W
% 0.54/0.97 , Y, Z ), coll( skol8( V0, V1, Z, T ), T, Z ) }.
% 0.54/0.97 { ! midp( T, X, U ), ! para( X, W, Z, T ), ! para( X, W, U, Y ), ! coll( W
% 0.54/0.97 , Y, Z ), coll( skol8( X, Y, Z, T ), X, Y ) }.
% 0.54/0.97 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), cong( T, Z, T, skol9( W, V0,
% 0.54/0.97 Z, T ) ) }.
% 0.54/0.97 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), cong( Y, Z, Y, skol9( W, Y, Z
% 0.54/0.97 , T ) ) }.
% 0.54/0.97 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), para( skol9( X, Y, Z, T ), Z
% 0.54/0.97 , X, Y ) }.
% 0.54/0.97 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), coll( skol10( U, Y, Z ), Z, Y
% 0.54/0.97 ) }.
% 0.54/0.97 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), perp( X, skol10( X, Y, Z ), Z
% 0.54/0.97 , Y ) }.
% 0.54/0.97 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), alpha1( X, Y, Z ) }.
% 0.54/0.97 { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z ), Z, X ) }.
% 0.54/0.97 { ! alpha1( X, Y, Z ), perp( Y, skol11( X, Y, Z ), Z, X ) }.
% 0.54/0.97 { ! coll( T, Z, X ), ! perp( Y, T, Z, X ), alpha1( X, Y, Z ) }.
% 0.54/0.97 { ! circle( Y, X, Z, T ), perp( skol12( X, Y ), X, X, Y ) }.
% 2.64/3.05 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 2.64/3.05 , alpha2( X, Z, U, skol13( X, V0, Z, V1, U ) ) }.
% 2.64/3.05 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 2.64/3.05 , coll( skol21( V0, Y, T, V1 ), Y, T ) }.
% 2.64/3.05 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 2.64/3.05 , cong( skol21( X, Y, T, U ), U, U, X ) }.
% 2.64/3.05 { ! alpha2( X, Y, Z, T ), coll( T, X, Y ) }.
% 2.64/3.05 { ! alpha2( X, Y, Z, T ), cong( T, Z, Z, X ) }.
% 2.64/3.05 { ! coll( T, X, Y ), ! cong( T, Z, Z, X ), alpha2( X, Y, Z, T ) }.
% 2.64/3.05 { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T ), ! midp( U, X, Y ), circle(
% 2.64/3.05 skol14( X, Y, Z ), X, Y, Z ) }.
% 2.64/3.05 { ! perp( X, Z, Z, Y ), ! cyclic( X, Y, Z, T ), circle( skol15( X, Y, Z ),
% 2.64/3.05 X, Y, Z ) }.
% 2.64/3.05 { ! perp( X, U, U, T ), ! coll( T, Y, Z ), coll( skol16( W, Y, Z ), Y, Z )
% 2.64/3.05 }.
% 2.64/3.05 { ! perp( X, U, U, T ), ! coll( T, Y, Z ), perp( skol16( X, Y, Z ), X, Y, Z
% 2.64/3.05 ) }.
% 2.64/3.05 { ! perp( X, Z, X, Y ), ! perp( Y, X, Y, T ), ! midp( U, Z, T ), midp(
% 2.64/3.05 skol17( X, Y ), X, Y ) }.
% 2.64/3.05 { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z ), coll( X, Y, skol18( X, Y ) )
% 2.64/3.05 }.
% 2.64/3.05 { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z ), cong( Y, X, Y, skol18( X, Y )
% 2.64/3.05 ) }.
% 2.64/3.05 { ! para( U, W, X, Y ), ! coll( Z, U, X ), ! coll( Z, W, Y ), ! coll( T, U
% 2.64/3.05 , W ), coll( Z, T, skol19( V0, V1, Z, T ) ) }.
% 2.64/3.05 { ! para( U, W, X, Y ), ! coll( Z, U, X ), ! coll( Z, W, Y ), ! coll( T, U
% 2.64/3.05 , W ), coll( skol19( X, Y, Z, T ), X, Y ) }.
% 2.64/3.05 { perp( skol20, skol24, skol20, skol25 ) }.
% 2.64/3.05 { perp( skol26, skol20, skol24, skol25 ) }.
% 2.64/3.05 { coll( skol26, skol24, skol25 ) }.
% 2.64/3.05 { midp( skol27, skol25, skol24 ) }.
% 2.64/3.05 { circle( skol27, skol20, skol28, skol29 ) }.
% 2.64/3.05 { perp( skol30, skol24, skol20, skol27 ) }.
% 2.64/3.05 { coll( skol30, skol20, skol27 ) }.
% 2.64/3.05 { coll( skol31, skol24, skol30 ) }.
% 2.64/3.05 { circle( skol27, skol20, skol31, skol32 ) }.
% 2.64/3.05 { coll( skol22, skol25, skol20 ) }.
% 2.64/3.05 { coll( skol22, skol24, skol30 ) }.
% 2.64/3.05 { coll( skol23, skol20, skol26 ) }.
% 2.64/3.05 { coll( skol23, skol24, skol30 ) }.
% 2.64/3.05 { ! cong( skol23, skol20, skol23, skol22 ) }.
% 2.64/3.05
% 2.64/3.05 percentage equality = 0.008621, percentage horn = 0.930769
% 2.64/3.05 This is a problem with some equality
% 2.64/3.05
% 2.64/3.05
% 2.64/3.05
% 2.64/3.05 Options Used:
% 2.64/3.05
% 2.64/3.05 useres = 1
% 2.64/3.05 useparamod = 1
% 2.64/3.05 useeqrefl = 1
% 2.64/3.05 useeqfact = 1
% 2.64/3.05 usefactor = 1
% 2.64/3.05 usesimpsplitting = 0
% 2.64/3.05 usesimpdemod = 5
% 2.64/3.05 usesimpres = 3
% 2.64/3.05
% 2.64/3.05 resimpinuse = 1000
% 2.64/3.05 resimpclauses = 20000
% 2.64/3.05 substype = eqrewr
% 2.64/3.05 backwardsubs = 1
% 2.64/3.05 selectoldest = 5
% 2.64/3.05
% 2.64/3.05 litorderings [0] = split
% 2.64/3.05 litorderings [1] = extend the termordering, first sorting on arguments
% 2.64/3.05
% 2.64/3.05 termordering = kbo
% 2.64/3.05
% 2.64/3.05 litapriori = 0
% 2.64/3.05 termapriori = 1
% 2.64/3.05 litaposteriori = 0
% 2.64/3.05 termaposteriori = 0
% 2.64/3.05 demodaposteriori = 0
% 2.64/3.05 ordereqreflfact = 0
% 2.64/3.05
% 2.64/3.05 litselect = negord
% 2.64/3.05
% 2.64/3.05 maxweight = 15
% 2.64/3.05 maxdepth = 30000
% 2.64/3.05 maxlength = 115
% 2.64/3.05 maxnrvars = 195
% 2.64/3.05 excuselevel = 1
% 2.64/3.05 increasemaxweight = 1
% 2.64/3.05
% 2.64/3.05 maxselected = 10000000
% 2.64/3.05 maxnrclauses = 10000000
% 2.64/3.05
% 2.64/3.05 showgenerated = 0
% 2.64/3.05 showkept = 0
% 2.64/3.05 showselected = 0
% 2.64/3.05 showdeleted = 0
% 2.64/3.05 showresimp = 1
% 2.64/3.05 showstatus = 2000
% 2.64/3.05
% 2.64/3.05 prologoutput = 0
% 2.64/3.05 nrgoals = 5000000
% 2.64/3.05 totalproof = 1
% 2.64/3.05
% 2.64/3.05 Symbols occurring in the translation:
% 2.64/3.05
% 2.64/3.05 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.64/3.05 . [1, 2] (w:1, o:44, a:1, s:1, b:0),
% 2.64/3.05 ! [4, 1] (w:0, o:39, a:1, s:1, b:0),
% 2.64/3.05 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.64/3.05 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.64/3.05 coll [38, 3] (w:1, o:72, a:1, s:1, b:0),
% 2.64/3.05 para [40, 4] (w:1, o:80, a:1, s:1, b:0),
% 2.64/3.05 perp [43, 4] (w:1, o:81, a:1, s:1, b:0),
% 2.64/3.05 midp [45, 3] (w:1, o:73, a:1, s:1, b:0),
% 2.64/3.05 cong [47, 4] (w:1, o:82, a:1, s:1, b:0),
% 2.64/3.05 circle [48, 4] (w:1, o:83, a:1, s:1, b:0),
% 2.64/3.05 cyclic [49, 4] (w:1, o:84, a:1, s:1, b:0),
% 2.64/3.05 eqangle [54, 8] (w:1, o:99, a:1, s:1, b:0),
% 2.64/3.05 eqratio [57, 8] (w:1, o:100, a:1, s:1, b:0),
% 2.64/3.05 simtri [59, 6] (w:1, o:96, a:1, s:1, b:0),
% 2.64/3.05 contri [60, 6] (w:1, o:97, a:1, s:1, b:0),
% 2.64/3.05 alpha1 [67, 3] (w:1, o:74, a:1, s:1, b:1),
% 2.64/3.05 alpha2 [68, 4] (w:1, o:85, a:1, s:1, b:1),
% 2.64/3.05 skol1 [69, 4] (w:1, o:86, a:1, s:1, b:1),
% 2.64/3.05 skol2 [70, 4] (w:1, o:88, a:1, s:1, b:1),
% 2.64/3.05 skol3 [71, 4] (w:1, o:90, a:1, s:1, b:1),
% 23.02/23.41 skol4 [72, 4] (w:1, o:91, a:1, s:1, b:1),
% 23.02/23.41 skol5 [73, 4] (w:1, o:92, a:1, s:1, b:1),
% 23.02/23.41 skol6 [74, 6] (w:1, o:98, a:1, s:1, b:1),
% 23.02/23.41 skol7 [75, 2] (w:1, o:68, a:1, s:1, b:1),
% 23.02/23.41 skol8 [76, 4] (w:1, o:93, a:1, s:1, b:1),
% 23.02/23.41 skol9 [77, 4] (w:1, o:94, a:1, s:1, b:1),
% 23.02/23.41 skol10 [78, 3] (w:1, o:75, a:1, s:1, b:1),
% 23.02/23.41 skol11 [79, 3] (w:1, o:76, a:1, s:1, b:1),
% 23.02/23.41 skol12 [80, 2] (w:1, o:69, a:1, s:1, b:1),
% 23.02/23.41 skol13 [81, 5] (w:1, o:95, a:1, s:1, b:1),
% 23.02/23.41 skol14 [82, 3] (w:1, o:77, a:1, s:1, b:1),
% 23.02/23.41 skol15 [83, 3] (w:1, o:78, a:1, s:1, b:1),
% 23.02/23.41 skol16 [84, 3] (w:1, o:79, a:1, s:1, b:1),
% 23.02/23.41 skol17 [85, 2] (w:1, o:70, a:1, s:1, b:1),
% 23.02/23.41 skol18 [86, 2] (w:1, o:71, a:1, s:1, b:1),
% 23.02/23.41 skol19 [87, 4] (w:1, o:87, a:1, s:1, b:1),
% 23.02/23.41 skol20 [88, 0] (w:1, o:27, a:1, s:1, b:1),
% 23.02/23.41 skol21 [89, 4] (w:1, o:89, a:1, s:1, b:1),
% 23.02/23.41 skol22 [90, 0] (w:1, o:28, a:1, s:1, b:1),
% 23.02/23.41 skol23 [91, 0] (w:1, o:29, a:1, s:1, b:1),
% 23.02/23.41 skol24 [92, 0] (w:1, o:30, a:1, s:1, b:1),
% 23.02/23.41 skol25 [93, 0] (w:1, o:31, a:1, s:1, b:1),
% 23.02/23.41 skol26 [94, 0] (w:1, o:32, a:1, s:1, b:1),
% 23.02/23.41 skol27 [95, 0] (w:1, o:33, a:1, s:1, b:1),
% 23.02/23.41 skol28 [96, 0] (w:1, o:34, a:1, s:1, b:1),
% 23.02/23.41 skol29 [97, 0] (w:1, o:35, a:1, s:1, b:1),
% 23.02/23.41 skol30 [98, 0] (w:1, o:36, a:1, s:1, b:1),
% 23.02/23.41 skol31 [99, 0] (w:1, o:37, a:1, s:1, b:1),
% 23.02/23.41 skol32 [100, 0] (w:1, o:38, a:1, s:1, b:1).
% 23.02/23.41
% 23.02/23.41
% 23.02/23.41 Starting Search:
% 23.02/23.41
% 23.02/23.41 *** allocated 15000 integers for clauses
% 23.02/23.41 *** allocated 22500 integers for clauses
% 23.02/23.41 *** allocated 33750 integers for clauses
% 23.02/23.41 *** allocated 50625 integers for clauses
% 23.02/23.41 *** allocated 22500 integers for termspace/termends
% 23.02/23.41 *** allocated 75937 integers for clauses
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 *** allocated 33750 integers for termspace/termends
% 23.02/23.41 *** allocated 113905 integers for clauses
% 23.02/23.41 *** allocated 50625 integers for termspace/termends
% 23.02/23.41
% 23.02/23.41 Intermediate Status:
% 23.02/23.41 Generated: 8145
% 23.02/23.41 Kept: 2000
% 23.02/23.41 Inuse: 303
% 23.02/23.41 Deleted: 0
% 23.02/23.41 Deletedinuse: 0
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 *** allocated 170857 integers for clauses
% 23.02/23.41 *** allocated 75937 integers for termspace/termends
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 *** allocated 256285 integers for clauses
% 23.02/23.41 *** allocated 113905 integers for termspace/termends
% 23.02/23.41
% 23.02/23.41 Intermediate Status:
% 23.02/23.41 Generated: 16823
% 23.02/23.41 Kept: 4040
% 23.02/23.41 Inuse: 466
% 23.02/23.41 Deleted: 0
% 23.02/23.41 Deletedinuse: 0
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 *** allocated 384427 integers for clauses
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 *** allocated 170857 integers for termspace/termends
% 23.02/23.41
% 23.02/23.41 Intermediate Status:
% 23.02/23.41 Generated: 28703
% 23.02/23.41 Kept: 6070
% 23.02/23.41 Inuse: 541
% 23.02/23.41 Deleted: 0
% 23.02/23.41 Deletedinuse: 0
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 *** allocated 576640 integers for clauses
% 23.02/23.41
% 23.02/23.41 Intermediate Status:
% 23.02/23.41 Generated: 41361
% 23.02/23.41 Kept: 8166
% 23.02/23.41 Inuse: 685
% 23.02/23.41 Deleted: 1
% 23.02/23.41 Deletedinuse: 0
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 *** allocated 256285 integers for termspace/termends
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41
% 23.02/23.41 Intermediate Status:
% 23.02/23.41 Generated: 61712
% 23.02/23.41 Kept: 10354
% 23.02/23.41 Inuse: 809
% 23.02/23.41 Deleted: 4
% 23.02/23.41 Deletedinuse: 2
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 *** allocated 864960 integers for clauses
% 23.02/23.41
% 23.02/23.41 Intermediate Status:
% 23.02/23.41 Generated: 71708
% 23.02/23.41 Kept: 12420
% 23.02/23.41 Inuse: 869
% 23.02/23.41 Deleted: 5
% 23.02/23.41 Deletedinuse: 3
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41
% 23.02/23.41 Intermediate Status:
% 23.02/23.41 Generated: 84251
% 23.02/23.41 Kept: 14427
% 23.02/23.41 Inuse: 991
% 23.02/23.41 Deleted: 7
% 23.02/23.41 Deletedinuse: 3
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 *** allocated 384427 integers for termspace/termends
% 23.02/23.41
% 23.02/23.41 Intermediate Status:
% 23.02/23.41 Generated: 98206
% 23.02/23.41 Kept: 16432
% 23.02/23.41 Inuse: 1135
% 23.02/23.41 Deleted: 7
% 23.02/23.41 Deletedinuse: 3
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 *** allocated 1297440 integers for clauses
% 23.02/23.41
% 23.02/23.41 Intermediate Status:
% 23.02/23.41 Generated: 112515
% 23.02/23.41 Kept: 18449
% 23.02/23.41 Inuse: 1263
% 23.02/23.41 Deleted: 9
% 23.02/23.41 Deletedinuse: 3
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41 Resimplifying clauses:
% 23.02/23.41 Done
% 23.02/23.41
% 23.02/23.41
% 23.02/23.41 Intermediate Status:
% 23.02/23.41 Generated: 120906
% 23.02/23.41 Kept: 20471
% 23.02/23.41 Inuse: 1335
% 23.02/23.41 Deleted: 1053
% 23.02/23.41 Deletedinuse: 3
% 23.02/23.41
% 23.02/23.41 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 130688
% 37.82/38.20 Kept: 22471
% 37.82/38.20 Inuse: 1432
% 37.82/38.20 Deleted: 1053
% 37.82/38.20 Deletedinuse: 3
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 140330
% 37.82/38.20 Kept: 24474
% 37.82/38.20 Inuse: 1531
% 37.82/38.20 Deleted: 1053
% 37.82/38.20 Deletedinuse: 3
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 *** allocated 576640 integers for termspace/termends
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 149197
% 37.82/38.20 Kept: 26476
% 37.82/38.20 Inuse: 1633
% 37.82/38.20 Deleted: 1053
% 37.82/38.20 Deletedinuse: 3
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 *** allocated 1946160 integers for clauses
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 159393
% 37.82/38.20 Kept: 28487
% 37.82/38.20 Inuse: 1740
% 37.82/38.20 Deleted: 1053
% 37.82/38.20 Deletedinuse: 3
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 172301
% 37.82/38.20 Kept: 30491
% 37.82/38.20 Inuse: 1881
% 37.82/38.20 Deleted: 1217
% 37.82/38.20 Deletedinuse: 3
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 181507
% 37.82/38.20 Kept: 32504
% 37.82/38.20 Inuse: 2006
% 37.82/38.20 Deleted: 2671
% 37.82/38.20 Deletedinuse: 1395
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 193050
% 37.82/38.20 Kept: 34524
% 37.82/38.20 Inuse: 2212
% 37.82/38.20 Deleted: 2689
% 37.82/38.20 Deletedinuse: 1395
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 203866
% 37.82/38.20 Kept: 36630
% 37.82/38.20 Inuse: 2365
% 37.82/38.20 Deleted: 2795
% 37.82/38.20 Deletedinuse: 1395
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 231592
% 37.82/38.20 Kept: 38634
% 37.82/38.20 Inuse: 2474
% 37.82/38.20 Deleted: 3979
% 37.82/38.20 Deletedinuse: 1401
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying clauses:
% 37.82/38.20 *** allocated 2919240 integers for clauses
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 238063
% 37.82/38.20 Kept: 40650
% 37.82/38.20 Inuse: 2530
% 37.82/38.20 Deleted: 24314
% 37.82/38.20 Deletedinuse: 1404
% 37.82/38.20
% 37.82/38.20 *** allocated 864960 integers for termspace/termends
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 248995
% 37.82/38.20 Kept: 42695
% 37.82/38.20 Inuse: 2622
% 37.82/38.20 Deleted: 24318
% 37.82/38.20 Deletedinuse: 1408
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 258998
% 37.82/38.20 Kept: 44746
% 37.82/38.20 Inuse: 2716
% 37.82/38.20 Deleted: 24336
% 37.82/38.20 Deletedinuse: 1425
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 267851
% 37.82/38.20 Kept: 46755
% 37.82/38.20 Inuse: 2789
% 37.82/38.20 Deleted: 24336
% 37.82/38.20 Deletedinuse: 1425
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 281867
% 37.82/38.20 Kept: 48757
% 37.82/38.20 Inuse: 2906
% 37.82/38.20 Deleted: 24336
% 37.82/38.20 Deletedinuse: 1425
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 293453
% 37.82/38.20 Kept: 50796
% 37.82/38.20 Inuse: 2986
% 37.82/38.20 Deleted: 24336
% 37.82/38.20 Deletedinuse: 1425
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 314360
% 37.82/38.20 Kept: 52797
% 37.82/38.20 Inuse: 3103
% 37.82/38.20 Deleted: 24336
% 37.82/38.20 Deletedinuse: 1425
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 324523
% 37.82/38.20 Kept: 54820
% 37.82/38.20 Inuse: 3180
% 37.82/38.20 Deleted: 24340
% 37.82/38.20 Deletedinuse: 1425
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 340530
% 37.82/38.20 Kept: 56832
% 37.82/38.20 Inuse: 3269
% 37.82/38.20 Deleted: 24343
% 37.82/38.20 Deletedinuse: 1425
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 355164
% 37.82/38.20 Kept: 58879
% 37.82/38.20 Inuse: 3339
% 37.82/38.20 Deleted: 24343
% 37.82/38.20 Deletedinuse: 1425
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 *** allocated 4378860 integers for clauses
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying clauses:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 363309
% 37.82/38.20 Kept: 60892
% 37.82/38.20 Inuse: 3381
% 37.82/38.20 Deleted: 25522
% 37.82/38.20 Deletedinuse: 1425
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 *** allocated 1297440 integers for termspace/termends
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 373536
% 37.82/38.20 Kept: 62895
% 37.82/38.20 Inuse: 3433
% 37.82/38.20 Deleted: 25522
% 37.82/38.20 Deletedinuse: 1425
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 398618
% 37.82/38.20 Kept: 64897
% 37.82/38.20 Inuse: 3539
% 37.82/38.20 Deleted: 25522
% 37.82/38.20 Deletedinuse: 1425
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 414676
% 37.82/38.20 Kept: 66929
% 37.82/38.20 Inuse: 3665
% 37.82/38.20 Deleted: 25523
% 37.82/38.20 Deletedinuse: 1426
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 431421
% 37.82/38.20 Kept: 68971
% 37.82/38.20 Inuse: 3779
% 37.82/38.20 Deleted: 25523
% 37.82/38.20 Deletedinuse: 1426
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 442948
% 37.82/38.20 Kept: 70989
% 37.82/38.20 Inuse: 3848
% 37.82/38.20 Deleted: 25523
% 37.82/38.20 Deletedinuse: 1426
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 449315
% 37.82/38.20 Kept: 73264
% 37.82/38.20 Inuse: 3879
% 37.82/38.20 Deleted: 25527
% 37.82/38.20 Deletedinuse: 1430
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 454616
% 37.82/38.20 Kept: 75305
% 37.82/38.20 Inuse: 3902
% 37.82/38.20 Deleted: 25527
% 37.82/38.20 Deletedinuse: 1430
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 461359
% 37.82/38.20 Kept: 77690
% 37.82/38.20 Inuse: 3928
% 37.82/38.20 Deleted: 25528
% 37.82/38.20 Deletedinuse: 1430
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Intermediate Status:
% 37.82/38.20 Generated: 472495
% 37.82/38.20 Kept: 79723
% 37.82/38.20 Inuse: 3980
% 37.82/38.20 Deleted: 25607
% 37.82/38.20 Deletedinuse: 1509
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying clauses:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20 Resimplifying inuse:
% 37.82/38.20 Done
% 37.82/38.20
% 37.82/38.20
% 37.82/38.20 Bliksems!, er is een bewijs:
% 37.82/38.20 % SZS status Theorem
% 37.82/38.20 % SZS output start Refutation
% 37.82/38.20
% 37.82/38.20 (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 37.82/38.20 (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 37.82/38.20 (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z ), coll( Y
% 37.82/38.20 , Z, X ) }.
% 37.82/38.20 (3) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( X, Y, T, Z ) }.
% 37.82/38.20 (4) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( Z, T, X, Y ) }.
% 37.82/38.20 (6) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( X, Y, T, Z ) }.
% 37.82/38.20 (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T, X, Y ) }.
% 37.82/38.20 (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U, W, Z, T ),
% 37.82/38.20 para( X, Y, Z, T ) }.
% 37.82/38.20 (9) {G0,W15,D2,L3,V6,M3} I { ! para( X, Y, U, W ), ! perp( U, W, Z, T ),
% 37.82/38.20 perp( X, Y, Z, T ) }.
% 37.82/38.20 (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 37.82/38.20 (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T )
% 37.82/38.20 }.
% 37.82/38.20 (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T )
% 37.82/38.20 }.
% 37.82/38.20 (23) {G0,W10,D2,L2,V4,M2} I { ! cong( X, Y, Z, T ), cong( Z, T, X, Y ) }.
% 37.82/38.20 (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X, Y, U, W, Z
% 37.82/38.20 , T, U, W ) }.
% 37.82/38.20 (40) {G0,W14,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z, Y,
% 37.82/38.20 T, X, T, Y ) }.
% 37.82/38.20 (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll(
% 37.82/38.20 Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 37.82/38.20 (43) {G0,W29,D2,L5,V6,M5} I { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U, T
% 37.82/38.20 ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T ), cong( X
% 37.82/38.20 , Y, Z, T ) }.
% 37.82/38.20 (55) {G0,W14,D2,L3,V4,M3} I { ! midp( T, X, Y ), ! perp( Z, T, X, Y ), cong
% 37.82/38.20 ( Z, X, Z, Y ) }.
% 37.82/38.20 (56) {G0,W15,D2,L3,V4,M3} I { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T ),
% 37.82/38.20 perp( X, Y, Z, T ) }.
% 37.82/38.20 (63) {G0,W13,D2,L3,V5,M3} I { ! midp( U, X, Y ), ! midp( U, Z, T ), para( X
% 37.82/38.20 , Z, Y, T ) }.
% 37.82/38.20 (69) {G0,W8,D2,L2,V3,M2} I { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 37.82/38.20 (88) {G0,W22,D3,L5,V7,M5} I { ! midp( Z, X, Y ), ! midp( W, T, U ), ! coll
% 37.82/38.20 ( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0 ) }.
% 37.82/38.20 (94) {G0,W17,D3,L3,V5,M3} I { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ),
% 37.82/38.20 coll( skol10( U, Y, Z ), Z, Y ) }.
% 37.82/38.20 (116) {G0,W5,D2,L1,V0,M1} I { perp( skol20, skol24, skol20, skol25 ) }.
% 37.82/38.20 (118) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol24, skol25 ) }.
% 37.82/38.20 (119) {G0,W4,D2,L1,V0,M1} I { midp( skol27, skol25, skol24 ) }.
% 37.82/38.20 (129) {G0,W5,D2,L1,V0,M1} I { ! cong( skol23, skol20, skol23, skol22 ) }.
% 37.82/38.20 (152) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y, Y, Z ), !
% 37.82/38.20 coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 37.82/38.20 (176) {G1,W8,D2,L2,V3,M2} R(1,0) { coll( X, Y, Z ), ! coll( Y, Z, X ) }.
% 37.82/38.20 (187) {G1,W16,D2,L4,V5,M4} R(2,2) { ! coll( X, Y, Z ), coll( Z, T, X ), !
% 37.82/38.20 coll( T, U, X ), ! coll( T, U, Y ) }.
% 37.82/38.20 (208) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll( X, Y, T ),
% 37.82/38.20 coll( Z, X, T ) }.
% 37.82/38.20 (219) {G2,W8,D2,L2,V3,M2} F(208) { ! coll( X, Y, Z ), coll( Z, X, Z ) }.
% 37.82/38.20 (244) {G1,W10,D2,L2,V4,M2} R(4,3) { ! para( X, Y, Z, T ), para( Z, T, Y, X
% 37.82/38.20 ) }.
% 37.82/38.20 (306) {G1,W4,D2,L1,V0,M1} R(118,1) { coll( skol24, skol26, skol25 ) }.
% 37.82/38.20 (310) {G2,W4,D2,L1,V0,M1} R(306,0) { coll( skol24, skol25, skol26 ) }.
% 37.82/38.20 (313) {G3,W4,D2,L1,V0,M1} R(310,1) { coll( skol25, skol24, skol26 ) }.
% 37.82/38.20 (316) {G4,W4,D2,L1,V0,M1} R(313,0) { coll( skol25, skol26, skol24 ) }.
% 37.82/38.20 (320) {G1,W15,D2,L3,V6,M3} R(9,7) { ! para( X, Y, Z, T ), perp( X, Y, U, W
% 37.82/38.20 ), ! perp( U, W, Z, T ) }.
% 37.82/38.20 (329) {G1,W4,D2,L1,V0,M1} R(10,119) { midp( skol27, skol24, skol25 ) }.
% 37.82/38.20 (397) {G1,W5,D2,L1,V0,M1} R(116,7) { perp( skol20, skol25, skol20, skol24 )
% 37.82/38.20 }.
% 37.82/38.20 (402) {G2,W5,D2,L1,V0,M1} R(397,6) { perp( skol20, skol25, skol24, skol20 )
% 37.82/38.20 }.
% 37.82/38.20 (403) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), ! cyclic( Y, Z
% 37.82/38.20 , X, T ) }.
% 37.82/38.20 (404) {G1,W10,D2,L2,V4,M2} R(15,14) { ! cyclic( X, Y, Z, T ), cyclic( Y, Z
% 37.82/38.20 , X, T ) }.
% 37.82/38.20 (414) {G3,W5,D2,L1,V0,M1} R(402,7) { perp( skol24, skol20, skol20, skol25 )
% 37.82/38.20 }.
% 37.82/38.20 (418) {G4,W5,D2,L1,V0,M1} R(414,6) { perp( skol24, skol20, skol25, skol20 )
% 37.82/38.20 }.
% 37.82/38.20 (422) {G5,W5,D2,L1,V0,M1} R(418,7) { perp( skol25, skol20, skol24, skol20 )
% 37.82/38.20 }.
% 37.82/38.20 (451) {G5,W4,D2,L1,V0,M1} R(219,316) { coll( skol24, skol25, skol24 ) }.
% 37.82/38.20 (454) {G3,W4,D2,L1,V0,M1} R(219,306) { coll( skol25, skol24, skol25 ) }.
% 37.82/38.20 (476) {G3,W12,D2,L3,V4,M3} R(219,2) { coll( X, Y, X ), ! coll( X, Z, Y ), !
% 37.82/38.20 coll( X, Z, T ) }.
% 37.82/38.20 (493) {G4,W8,D2,L2,V3,M2} F(476) { coll( X, Y, X ), ! coll( X, Z, Y ) }.
% 37.82/38.20 (503) {G6,W4,D2,L1,V0,M1} R(451,0) { coll( skol24, skol24, skol25 ) }.
% 37.82/38.20 (531) {G4,W4,D2,L1,V0,M1} R(454,0) { coll( skol25, skol25, skol24 ) }.
% 37.82/38.20 (576) {G1,W5,D2,L1,V0,M1} R(23,129) { ! cong( skol23, skol22, skol23,
% 37.82/38.20 skol20 ) }.
% 37.82/38.20 (862) {G1,W14,D2,L3,V3,M3} R(42,39) { ! coll( X, X, Y ), cyclic( Z, Y, X, X
% 37.82/38.20 ), ! para( X, Z, X, Z ) }.
% 37.82/38.20 (1026) {G1,W20,D2,L4,V4,M4} R(43,40);f { ! cyclic( X, Y, Z, X ), ! cyclic(
% 37.82/38.20 X, Y, Z, Y ), ! cyclic( X, Y, Z, T ), cong( X, Y, X, Y ) }.
% 37.82/38.20 (1059) {G2,W15,D2,L3,V3,M3} F(1026) { ! cyclic( X, Y, Z, X ), ! cyclic( X,
% 37.82/38.20 Y, Z, Y ), cong( X, Y, X, Y ) }.
% 37.82/38.20 (1418) {G5,W8,D2,L2,V3,M2} R(493,1) { ! coll( X, Y, Z ), coll( Z, X, X )
% 37.82/38.20 }.
% 37.82/38.20 (1423) {G6,W8,D2,L2,V3,M2} R(1418,1) { coll( X, Y, Y ), ! coll( Z, Y, X )
% 37.82/38.20 }.
% 37.82/38.20 (1424) {G6,W8,D2,L2,V3,M2} R(1418,0) { coll( X, Y, Y ), ! coll( Y, X, Z )
% 37.82/38.20 }.
% 37.82/38.20 (1425) {G7,W8,D2,L2,V3,M2} R(1423,1418) { ! coll( X, Y, Z ), coll( Y, Z, Z
% 37.82/38.20 ) }.
% 37.82/38.20 (1456) {G7,W8,D2,L2,V3,M2} R(1424,1424) { ! coll( X, Y, Z ), coll( X, Y, Y
% 37.82/38.20 ) }.
% 37.82/38.20 (1459) {G8,W12,D2,L3,V4,M3} R(1456,2) { ! coll( X, Y, Z ), ! coll( X, Y, T
% 37.82/38.20 ), coll( T, Y, X ) }.
% 37.82/38.20 (1460) {G9,W8,D2,L2,V3,M2} F(1459) { ! coll( X, Y, Z ), coll( Z, Y, X ) }.
% 37.82/38.20 (1463) {G10,W8,D2,L2,V3,M2} R(1460,1425) { coll( X, X, Y ), ! coll( Z, Y, X
% 37.82/38.20 ) }.
% 37.82/38.20 (1749) {G7,W8,D2,L2,V3,M2} R(69,1423) { ! midp( X, Y, Z ), coll( Z, Y, Y )
% 37.82/38.20 }.
% 37.82/38.20 (1766) {G2,W9,D2,L2,V1,M2} R(55,576) { ! midp( X, skol22, skol20 ), ! perp
% 37.82/38.20 ( skol23, X, skol22, skol20 ) }.
% 37.82/38.21 (1863) {G1,W20,D2,L4,V6,M4} R(56,8) { ! cong( X, Y, Z, Y ), ! cong( X, T, Z
% 37.82/38.21 , T ), ! perp( U, W, X, Z ), para( U, W, Y, T ) }.
% 37.82/38.21 (1864) {G1,W15,D2,L3,V4,M3} R(56,7) { ! cong( X, Y, Z, Y ), ! cong( X, T, Z
% 37.82/38.21 , T ), perp( Y, T, X, Z ) }.
% 37.82/38.21 (1866) {G2,W15,D2,L3,V5,M3} F(1863) { ! cong( X, Y, Z, Y ), ! perp( T, U, X
% 37.82/38.21 , Z ), para( T, U, Y, Y ) }.
% 37.82/38.21 (2102) {G1,W13,D2,L3,V5,M3} R(63,10) { ! midp( X, Y, Z ), para( Y, T, Z, U
% 37.82/38.21 ), ! midp( X, U, T ) }.
% 37.82/38.21 (2114) {G2,W9,D2,L2,V3,M2} F(2102) { ! midp( X, Y, Z ), para( Y, Z, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 (4092) {G6,W7,D3,L1,V1,M1} R(94,422);r(418) { coll( skol10( X, skol24,
% 37.82/38.21 skol20 ), skol20, skol24 ) }.
% 37.82/38.21 (4158) {G11,W4,D2,L1,V0,M1} R(4092,1463) { coll( skol24, skol24, skol20 )
% 37.82/38.21 }.
% 37.82/38.21 (8164) {G7,W10,D3,L2,V1,M2} R(152,329);r(503) { ! coll( skol25, skol24,
% 37.82/38.21 skol25 ), midp( skol7( skol24, X ), skol24, X ) }.
% 37.82/38.21 (8165) {G5,W10,D3,L2,V1,M2} R(152,119);r(531) { ! coll( skol24, skol25,
% 37.82/38.21 skol24 ), midp( skol7( skol25, X ), skol25, X ) }.
% 37.82/38.21 (9555) {G12,W8,D2,L2,V2,M2} R(187,4158);f { coll( skol20, X, skol24 ), !
% 37.82/38.21 coll( X, Y, skol24 ) }.
% 37.82/38.21 (20078) {G8,W6,D3,L1,V1,M1} S(8164);r(454) { midp( skol7( skol24, X ),
% 37.82/38.21 skol24, X ) }.
% 37.82/38.21 (20079) {G6,W6,D3,L1,V1,M1} S(8165);r(451) { midp( skol7( skol25, X ),
% 37.82/38.21 skol25, X ) }.
% 37.82/38.21 (29734) {G9,W4,D2,L1,V1,M1} R(20078,1749) { coll( X, skol24, skol24 ) }.
% 37.82/38.21 (29775) {G13,W4,D2,L1,V1,M1} R(29734,9555) { coll( skol20, X, skol24 ) }.
% 37.82/38.21 (29805) {G14,W4,D2,L1,V1,M1} R(29775,176) { coll( skol24, skol20, X ) }.
% 37.82/38.21 (29835) {G15,W4,D2,L1,V2,M1} R(29805,208);r(29805) { coll( Y, skol24, X )
% 37.82/38.21 }.
% 37.82/38.21 (29888) {G16,W4,D2,L1,V3,M1} R(29835,208);r(29835) { coll( Z, X, Y ) }.
% 37.82/38.21 (30287) {G7,W6,D3,L1,V1,M1} R(20079,10) { midp( skol7( skol25, X ), X,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 (30331) {G17,W10,D3,L2,V2,M2} R(30287,152);r(29888) { ! coll( skol25, X,
% 37.82/38.21 skol25 ), midp( skol7( X, Y ), X, Y ) }.
% 37.82/38.21 (37185) {G17,W10,D2,L2,V3,M2} S(862);r(29888) { cyclic( Z, Y, X, X ), !
% 37.82/38.21 para( X, Z, X, Z ) }.
% 37.82/38.21 (40165) {G18,W6,D3,L1,V2,M1} S(30331);r(29888) { midp( skol7( X, Y ), X, Y
% 37.82/38.21 ) }.
% 37.82/38.21 (43124) {G19,W6,D3,L1,V2,M1} R(40165,10) { midp( skol7( X, Y ), Y, X ) }.
% 37.82/38.21 (52359) {G19,W7,D3,L1,V0,M1} R(1766,40165) { ! perp( skol23, skol7( skol22
% 37.82/38.21 , skol20 ), skol22, skol20 ) }.
% 37.82/38.21 (52645) {G20,W7,D3,L1,V0,M1} R(52359,6) { ! perp( skol23, skol7( skol22,
% 37.82/38.21 skol20 ), skol20, skol22 ) }.
% 37.82/38.21 (77017) {G20,W5,D2,L1,V2,M1} R(2114,43124) { para( X, Y, Y, X ) }.
% 37.82/38.21 (77030) {G21,W5,D2,L1,V2,M1} R(77017,244) { para( X, Y, X, Y ) }.
% 37.82/38.21 (80676) {G22,W5,D2,L1,V3,M1} S(37185);r(77030) { cyclic( Z, Y, X, X ) }.
% 37.82/38.21 (80782) {G23,W5,D2,L1,V3,M1} R(80676,404) { cyclic( X, Y, Z, Y ) }.
% 37.82/38.21 (80783) {G23,W5,D2,L1,V3,M1} R(80676,403) { cyclic( X, Y, Z, X ) }.
% 37.82/38.21 (80798) {G24,W5,D2,L1,V2,M1} R(80782,1059);r(80783) { cong( X, Y, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 (81565) {G25,W5,D2,L1,V3,M1} R(80798,1864);r(80798) { perp( Z, Y, X, X )
% 37.82/38.21 }.
% 37.82/38.21 (81670) {G26,W5,D2,L1,V3,M1} R(81565,1866);r(80798) { para( Z, T, Y, Y )
% 37.82/38.21 }.
% 37.82/38.21 (81673) {G27,W5,D2,L1,V4,M1} R(81565,320);r(81670) { perp( X, Y, T, U ) }.
% 37.82/38.21 (81685) {G28,W0,D0,L0,V0,M0} R(81673,52645) { }.
% 37.82/38.21
% 37.82/38.21
% 37.82/38.21 % SZS output end Refutation
% 37.82/38.21 found a proof!
% 37.82/38.21
% 37.82/38.21
% 37.82/38.21 Unprocessed initial clauses:
% 37.82/38.21
% 37.82/38.21 (81687) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 37.82/38.21 (81688) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 37.82/38.21 (81689) {G0,W12,D2,L3,V4,M3} { ! coll( X, T, Y ), ! coll( X, T, Z ), coll
% 37.82/38.21 ( Y, Z, X ) }.
% 37.82/38.21 (81690) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( X, Y, T, Z )
% 37.82/38.21 }.
% 37.82/38.21 (81691) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( Z, T, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 (81692) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! para( U, W, Z, T )
% 37.82/38.21 , para( X, Y, Z, T ) }.
% 37.82/38.21 (81693) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( X, Y, T, Z )
% 37.82/38.21 }.
% 37.82/38.21 (81694) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( Z, T, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 (81695) {G0,W15,D2,L3,V6,M3} { ! perp( X, Y, U, W ), ! perp( U, W, Z, T )
% 37.82/38.21 , para( X, Y, Z, T ) }.
% 37.82/38.21 (81696) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! perp( U, W, Z, T )
% 37.82/38.21 , perp( X, Y, Z, T ) }.
% 37.82/38.21 (81697) {G0,W8,D2,L2,V3,M2} { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 37.82/38.21 (81698) {G0,W15,D2,L3,V4,M3} { ! cong( T, X, T, Y ), ! cong( T, X, T, Z )
% 37.82/38.21 , circle( T, X, Y, Z ) }.
% 37.82/38.21 (81699) {G0,W20,D2,L4,V5,M4} { ! cong( U, X, U, Y ), ! cong( U, X, U, Z )
% 37.82/38.21 , ! cong( U, X, U, T ), cyclic( X, Y, Z, T ) }.
% 37.82/38.21 (81700) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z
% 37.82/38.21 ) }.
% 37.82/38.21 (81701) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T
% 37.82/38.21 ) }.
% 37.82/38.21 (81702) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T
% 37.82/38.21 ) }.
% 37.82/38.21 (81703) {G0,W15,D2,L3,V5,M3} { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y,
% 37.82/38.21 T ), cyclic( X, Y, Z, T ) }.
% 37.82/38.21 (81704) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 37.82/38.21 eqangle( Y, X, Z, T, U, W, V0, V1 ) }.
% 37.82/38.21 (81705) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 37.82/38.21 eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 37.82/38.21 (81706) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 37.82/38.21 eqangle( U, W, V0, V1, X, Y, Z, T ) }.
% 37.82/38.21 (81707) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 37.82/38.21 eqangle( X, Y, U, W, Z, T, V0, V1 ) }.
% 37.82/38.21 (81708) {G0,W27,D2,L3,V12,M3} { ! eqangle( X, Y, Z, T, V2, V3, V4, V5 ), !
% 37.82/38.21 eqangle( V2, V3, V4, V5, U, W, V0, V1 ), eqangle( X, Y, Z, T, U, W, V0,
% 37.82/38.21 V1 ) }.
% 37.82/38.21 (81709) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( X, Y, T, Z )
% 37.82/38.21 }.
% 37.82/38.21 (81710) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( Z, T, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 (81711) {G0,W15,D2,L3,V6,M3} { ! cong( X, Y, U, W ), ! cong( U, W, Z, T )
% 37.82/38.21 , cong( X, Y, Z, T ) }.
% 37.82/38.21 (81712) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 37.82/38.21 eqratio( Y, X, Z, T, U, W, V0, V1 ) }.
% 37.82/38.21 (81713) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 37.82/38.21 eqratio( Z, T, X, Y, V0, V1, U, W ) }.
% 37.82/38.21 (81714) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 37.82/38.21 eqratio( U, W, V0, V1, X, Y, Z, T ) }.
% 37.82/38.21 (81715) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 37.82/38.21 eqratio( X, Y, U, W, Z, T, V0, V1 ) }.
% 37.82/38.21 (81716) {G0,W27,D2,L3,V12,M3} { ! eqratio( X, Y, Z, T, V2, V3, V4, V5 ), !
% 37.82/38.21 eqratio( V2, V3, V4, V5, U, W, V0, V1 ), eqratio( X, Y, Z, T, U, W, V0,
% 37.82/38.21 V1 ) }.
% 37.82/38.21 (81717) {G0,W14,D2,L2,V6,M2} { ! simtri( X, Z, Y, T, W, U ), simtri( X, Y
% 37.82/38.21 , Z, T, U, W ) }.
% 37.82/38.21 (81718) {G0,W14,D2,L2,V6,M2} { ! simtri( Y, X, Z, U, T, W ), simtri( X, Y
% 37.82/38.21 , Z, T, U, W ) }.
% 37.82/38.21 (81719) {G0,W14,D2,L2,V6,M2} { ! simtri( T, U, W, X, Y, Z ), simtri( X, Y
% 37.82/38.21 , Z, T, U, W ) }.
% 37.82/38.21 (81720) {G0,W21,D2,L3,V9,M3} { ! simtri( X, Y, Z, V0, V1, V2 ), ! simtri(
% 37.82/38.21 V0, V1, V2, T, U, W ), simtri( X, Y, Z, T, U, W ) }.
% 37.82/38.21 (81721) {G0,W14,D2,L2,V6,M2} { ! contri( X, Z, Y, T, W, U ), contri( X, Y
% 37.82/38.21 , Z, T, U, W ) }.
% 37.82/38.21 (81722) {G0,W14,D2,L2,V6,M2} { ! contri( Y, X, Z, U, T, W ), contri( X, Y
% 37.82/38.21 , Z, T, U, W ) }.
% 37.82/38.21 (81723) {G0,W14,D2,L2,V6,M2} { ! contri( T, U, W, X, Y, Z ), contri( X, Y
% 37.82/38.21 , Z, T, U, W ) }.
% 37.82/38.21 (81724) {G0,W21,D2,L3,V9,M3} { ! contri( X, Y, Z, V0, V1, V2 ), ! contri(
% 37.82/38.21 V0, V1, V2, T, U, W ), contri( X, Y, Z, T, U, W ) }.
% 37.82/38.21 (81725) {G0,W14,D2,L2,V6,M2} { ! eqangle( X, Y, U, W, Z, T, U, W ), para(
% 37.82/38.21 X, Y, Z, T ) }.
% 37.82/38.21 (81726) {G0,W14,D2,L2,V6,M2} { ! para( X, Y, Z, T ), eqangle( X, Y, U, W,
% 37.82/38.21 Z, T, U, W ) }.
% 37.82/38.21 (81727) {G0,W14,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z, Y
% 37.82/38.21 , T, X, T, Y ) }.
% 37.82/38.21 (81728) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y ), coll(
% 37.82/38.21 Z, T, X ), cyclic( X, Y, Z, T ) }.
% 37.82/38.21 (81729) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll
% 37.82/38.21 ( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 37.82/38.21 (81730) {G0,W29,D2,L5,V6,M5} { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U,
% 37.82/38.21 T ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T ), cong( X
% 37.82/38.21 , Y, Z, T ) }.
% 37.82/38.21 (81731) {G0,W13,D2,L3,V5,M3} { ! midp( Z, U, X ), ! midp( T, U, Y ), para
% 37.82/38.21 ( Z, T, X, Y ) }.
% 37.82/38.21 (81732) {G0,W17,D2,L4,V5,M4} { ! midp( U, X, T ), ! para( U, Z, T, Y ), !
% 37.82/38.21 coll( Z, X, Y ), midp( Z, X, Y ) }.
% 37.82/38.21 (81733) {G0,W14,D2,L2,V3,M2} { ! cong( Z, X, Z, Y ), eqangle( Z, X, X, Y,
% 37.82/38.21 X, Y, Z, Y ) }.
% 37.82/38.21 (81734) {G0,W18,D2,L3,V3,M3} { ! eqangle( Z, X, X, Y, X, Y, Z, Y ), coll(
% 37.82/38.21 Z, X, Y ), cong( Z, X, Z, Y ) }.
% 37.82/38.21 (81735) {G0,W19,D2,L3,V5,M3} { ! circle( U, X, Y, Z ), ! perp( U, X, X, T
% 37.82/38.21 ), eqangle( X, T, X, Y, Z, X, Z, Y ) }.
% 37.82/38.21 (81736) {G0,W19,D2,L3,V5,M3} { ! circle( Y, X, T, U ), ! eqangle( X, Z, X
% 37.82/38.21 , T, U, X, U, T ), perp( Y, X, X, Z ) }.
% 37.82/38.21 (81737) {G0,W18,D2,L3,V5,M3} { ! circle( T, X, Y, Z ), ! midp( U, Y, Z ),
% 37.82/38.21 eqangle( X, Y, X, Z, T, Y, T, U ) }.
% 37.82/38.21 (81738) {G0,W22,D2,L4,V5,M4} { ! circle( U, T, X, Y ), ! coll( Z, X, Y ),
% 37.82/38.21 ! eqangle( T, X, T, Y, U, X, U, Z ), midp( Z, X, Y ) }.
% 37.82/38.21 (81739) {G0,W14,D2,L3,V4,M3} { ! perp( X, Y, Y, T ), ! midp( Z, X, T ),
% 37.82/38.21 cong( X, Z, Y, Z ) }.
% 37.82/38.21 (81740) {G0,W14,D2,L3,V4,M3} { ! circle( T, X, Y, Z ), ! coll( T, X, Z ),
% 37.82/38.21 perp( X, Y, Y, Z ) }.
% 37.82/38.21 (81741) {G0,W19,D2,L3,V4,M3} { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T
% 37.82/38.21 ), eqangle( X, T, Z, T, Z, T, Z, Y ) }.
% 37.82/38.21 (81742) {G0,W14,D2,L3,V4,M3} { ! midp( T, X, Y ), ! perp( Z, T, X, Y ),
% 37.82/38.21 cong( Z, X, Z, Y ) }.
% 37.82/38.21 (81743) {G0,W15,D2,L3,V4,M3} { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T )
% 37.82/38.21 , perp( X, Y, Z, T ) }.
% 37.82/38.21 (81744) {G0,W20,D2,L4,V4,M4} { ! cong( X, Y, T, Y ), ! cong( X, Z, T, Z )
% 37.82/38.21 , ! cyclic( X, T, Y, Z ), perp( Y, X, X, Z ) }.
% 37.82/38.21 (81745) {G0,W29,D2,L4,V6,M4} { ! eqangle( X, Y, Y, Z, T, U, U, W ), !
% 37.82/38.21 eqangle( X, Z, Y, Z, T, W, U, W ), coll( X, Y, Z ), simtri( X, Y, Z, T, U
% 37.82/38.21 , W ) }.
% 37.82/38.21 (81746) {G0,W16,D2,L2,V6,M2} { ! simtri( X, Y, Z, T, U, W ), eqratio( X, Y
% 37.82/38.21 , X, Z, T, U, T, W ) }.
% 37.82/38.21 (81747) {G0,W16,D2,L2,V6,M2} { ! simtri( X, Y, Z, T, U, W ), eqangle( X, Y
% 37.82/38.21 , Y, Z, T, U, U, W ) }.
% 37.82/38.21 (81748) {G0,W19,D2,L3,V6,M3} { ! simtri( X, Y, Z, T, U, W ), ! cong( X, Y
% 37.82/38.21 , T, U ), contri( X, Y, Z, T, U, W ) }.
% 37.82/38.21 (81749) {G0,W12,D2,L2,V6,M2} { ! contri( X, Y, U, Z, T, W ), cong( X, Y, Z
% 37.82/38.21 , T ) }.
% 37.82/38.21 (81750) {G0,W13,D2,L3,V5,M3} { ! midp( U, X, Y ), ! midp( U, Z, T ), para
% 37.82/38.21 ( X, Z, Y, T ) }.
% 37.82/38.21 (81751) {G0,W18,D2,L4,V5,M4} { ! midp( Z, T, U ), ! para( T, X, U, Y ), !
% 37.82/38.21 para( T, Y, U, X ), midp( Z, X, Y ) }.
% 37.82/38.21 (81752) {G0,W22,D2,L4,V5,M4} { ! para( X, Y, Z, T ), ! coll( U, X, Z ), !
% 37.82/38.21 coll( U, Y, T ), eqratio( U, X, X, Z, U, Y, Y, T ) }.
% 37.82/38.21 (81753) {G0,W9,D2,L2,V3,M2} { ! para( X, Y, X, Z ), coll( X, Y, Z ) }.
% 37.82/38.21 (81754) {G0,W13,D2,L3,V3,M3} { ! cong( X, Y, X, Z ), ! coll( X, Y, Z ),
% 37.82/38.21 midp( X, Y, Z ) }.
% 37.82/38.21 (81755) {G0,W9,D2,L2,V3,M2} { ! midp( X, Y, Z ), cong( X, Y, X, Z ) }.
% 37.82/38.21 (81756) {G0,W8,D2,L2,V3,M2} { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 37.82/38.21 (81757) {G0,W17,D2,L3,V6,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ),
% 37.82/38.21 eqratio( U, X, X, Y, W, Z, Z, T ) }.
% 37.82/38.21 (81758) {G0,W19,D2,L3,V4,M3} { ! eqangle( X, Y, Z, T, Z, T, X, Y ), para(
% 37.82/38.21 X, Y, Z, T ), perp( X, Y, Z, T ) }.
% 37.82/38.21 (81759) {G0,W19,D2,L3,V4,M3} { ! eqangle( X, Y, Z, T, Z, T, X, Y ), perp(
% 37.82/38.21 X, Y, Z, T ), para( X, Y, Z, T ) }.
% 37.82/38.21 (81760) {G0,W19,D2,L3,V8,M3} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), !
% 37.82/38.21 para( U, W, V0, V1 ), para( X, Y, Z, T ) }.
% 37.82/38.21 (81761) {G0,W19,D2,L3,V8,M3} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), !
% 37.82/38.21 perp( U, W, V0, V1 ), perp( X, Y, Z, T ) }.
% 37.82/38.21 (81762) {G0,W19,D2,L3,V8,M3} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), !
% 37.82/38.21 cong( U, W, V0, V1 ), cong( X, Y, Z, T ) }.
% 37.82/38.21 (81763) {G0,W22,D3,L3,V6,M3} { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z
% 37.82/38.21 , Y, Z, X, Z ), coll( skol1( U, W, Z, T ), Z, T ) }.
% 37.82/38.21 (81764) {G0,W22,D3,L3,V4,M3} { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z
% 37.82/38.21 , Y, Z, X, Z ), coll( skol1( X, Y, Z, T ), X, Y ) }.
% 37.82/38.21 (81765) {G0,W22,D3,L3,V6,M3} { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T
% 37.82/38.21 , Z, T, Z, Y ), coll( skol2( U, W, Z, T ), Z, T ) }.
% 37.82/38.21 (81766) {G0,W22,D3,L3,V4,M3} { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T
% 37.82/38.21 , Z, T, Z, Y ), coll( Y, X, skol2( X, Y, Z, T ) ) }.
% 37.82/38.21 (81767) {G0,W22,D3,L3,V6,M3} { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T
% 37.82/38.21 , Z, T, Z, Y ), coll( skol3( U, W, Z, T ), Z, T ) }.
% 37.82/38.21 (81768) {G0,W22,D3,L3,V4,M3} { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T
% 37.82/38.21 , Z, T, Z, Y ), coll( Y, X, skol3( X, Y, Z, T ) ) }.
% 37.82/38.21 (81769) {G0,W18,D3,L3,V6,M3} { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y )
% 37.82/38.21 , coll( skol4( U, W, Z, T ), Z, T ) }.
% 37.82/38.21 (81770) {G0,W18,D3,L3,V4,M3} { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y )
% 37.82/38.21 , coll( Y, X, skol4( X, Y, Z, T ) ) }.
% 37.82/38.21 (81771) {G0,W22,D3,L3,V6,M3} { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll(
% 37.82/38.21 X, Y, Z ), cyclic( T, Y, Z, skol5( W, Y, Z, T ) ) }.
% 37.82/38.21 (81772) {G0,W30,D3,L3,V5,M3} { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll(
% 37.82/38.21 X, Y, Z ), eqangle( X, Z, Y, Z, X, skol5( X, Y, Z, T ), Y, skol5( X, Y, Z
% 37.82/38.21 , T ) ) }.
% 37.82/38.21 (81773) {G0,W18,D3,L3,V10,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), midp
% 37.82/38.21 ( skol6( X, V0, V1, T, V2, V3 ), X, T ) }.
% 37.82/38.21 (81774) {G0,W19,D3,L3,V8,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), para
% 37.82/38.21 ( skol6( X, V0, Z, T, V1, W ), W, X, Z ) }.
% 37.82/38.21 (81775) {G0,W19,D3,L3,V6,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), para
% 37.82/38.21 ( skol6( X, Y, Z, T, U, W ), U, Y, T ) }.
% 37.82/38.21 (81776) {G0,W22,D3,L5,V7,M5} { ! midp( Z, X, Y ), ! midp( W, T, U ), !
% 37.82/38.21 coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0 ) }.
% 37.82/38.21 (81777) {G0,W26,D3,L5,V8,M5} { ! midp( T, X, U ), ! para( X, W, Z, T ), !
% 37.82/38.21 para( X, W, U, Y ), ! coll( W, Y, Z ), coll( skol8( V0, V1, Z, T ), T, Z
% 37.82/38.21 ) }.
% 37.82/38.21 (81778) {G0,W26,D3,L5,V6,M5} { ! midp( T, X, U ), ! para( X, W, Z, T ), !
% 37.82/38.21 para( X, W, U, Y ), ! coll( W, Y, Z ), coll( skol8( X, Y, Z, T ), X, Y )
% 37.82/38.21 }.
% 37.82/38.21 (81779) {G0,W19,D3,L3,V7,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 37.82/38.21 , cong( T, Z, T, skol9( W, V0, Z, T ) ) }.
% 37.82/38.21 (81780) {G0,W19,D3,L3,V6,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 37.82/38.21 , cong( Y, Z, Y, skol9( W, Y, Z, T ) ) }.
% 37.82/38.21 (81781) {G0,W19,D3,L3,V5,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 37.82/38.21 , para( skol9( X, Y, Z, T ), Z, X, Y ) }.
% 37.82/38.21 (81782) {G0,W17,D3,L3,V5,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 37.82/38.21 , coll( skol10( U, Y, Z ), Z, Y ) }.
% 37.82/38.21 (81783) {G0,W18,D3,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 37.82/38.21 , perp( X, skol10( X, Y, Z ), Z, Y ) }.
% 37.82/38.21 (81784) {G0,W14,D2,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 37.82/38.21 , alpha1( X, Y, Z ) }.
% 37.82/38.21 (81785) {G0,W11,D3,L2,V4,M2} { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z
% 37.82/38.21 ), Z, X ) }.
% 37.82/38.21 (81786) {G0,W12,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), perp( Y, skol11( X, Y
% 37.82/38.21 , Z ), Z, X ) }.
% 37.82/38.21 (81787) {G0,W13,D2,L3,V4,M3} { ! coll( T, Z, X ), ! perp( Y, T, Z, X ),
% 37.82/38.21 alpha1( X, Y, Z ) }.
% 37.82/38.21 (81788) {G0,W12,D3,L2,V4,M2} { ! circle( Y, X, Z, T ), perp( skol12( X, Y
% 37.82/38.21 ), X, X, Y ) }.
% 37.82/38.21 (81789) {G0,W28,D3,L5,V8,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 37.82/38.21 ), ! cong( U, X, U, Y ), W = U, alpha2( X, Z, U, skol13( X, V0, Z, V1, U
% 37.82/38.21 ) ) }.
% 37.82/38.21 (81790) {G0,W26,D3,L5,V8,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 37.82/38.21 ), ! cong( U, X, U, Y ), W = U, coll( skol21( V0, Y, T, V1 ), Y, T ) }.
% 37.82/38.21 (81791) {G0,W27,D3,L5,V6,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 37.82/38.21 ), ! cong( U, X, U, Y ), W = U, cong( skol21( X, Y, T, U ), U, U, X )
% 37.82/38.21 }.
% 37.82/38.21 (81792) {G0,W9,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), coll( T, X, Y ) }.
% 37.82/38.21 (81793) {G0,W10,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), cong( T, Z, Z, X )
% 37.82/38.21 }.
% 37.82/38.21 (81794) {G0,W14,D2,L3,V4,M3} { ! coll( T, X, Y ), ! cong( T, Z, Z, X ),
% 37.82/38.21 alpha2( X, Y, Z, T ) }.
% 37.82/38.21 (81795) {G0,W22,D3,L4,V5,M4} { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T
% 37.82/38.21 ), ! midp( U, X, Y ), circle( skol14( X, Y, Z ), X, Y, Z ) }.
% 37.82/38.21 (81796) {G0,W18,D3,L3,V4,M3} { ! perp( X, Z, Z, Y ), ! cyclic( X, Y, Z, T
% 37.82/38.21 ), circle( skol15( X, Y, Z ), X, Y, Z ) }.
% 37.82/38.21 (81797) {G0,W16,D3,L3,V6,M3} { ! perp( X, U, U, T ), ! coll( T, Y, Z ),
% 37.82/38.21 coll( skol16( W, Y, Z ), Y, Z ) }.
% 37.82/38.21 (81798) {G0,W17,D3,L3,V5,M3} { ! perp( X, U, U, T ), ! coll( T, Y, Z ),
% 37.82/38.21 perp( skol16( X, Y, Z ), X, Y, Z ) }.
% 37.82/38.21 (81799) {G0,W20,D3,L4,V5,M4} { ! perp( X, Z, X, Y ), ! perp( Y, X, Y, T )
% 37.82/38.21 , ! midp( U, Z, T ), midp( skol17( X, Y ), X, Y ) }.
% 37.82/38.21 (81800) {G0,W16,D3,L3,V3,M3} { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z )
% 37.82/38.21 , coll( X, Y, skol18( X, Y ) ) }.
% 37.82/38.21 (81801) {G0,W17,D3,L3,V3,M3} { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z )
% 37.82/38.21 , cong( Y, X, Y, skol18( X, Y ) ) }.
% 37.82/38.21 (81802) {G0,W25,D3,L5,V8,M5} { ! para( U, W, X, Y ), ! coll( Z, U, X ), !
% 37.82/38.21 coll( Z, W, Y ), ! coll( T, U, W ), coll( Z, T, skol19( V0, V1, Z, T ) )
% 37.82/38.21 }.
% 37.82/38.21 (81803) {G0,W25,D3,L5,V6,M5} { ! para( U, W, X, Y ), ! coll( Z, U, X ), !
% 37.82/38.21 coll( Z, W, Y ), ! coll( T, U, W ), coll( skol19( X, Y, Z, T ), X, Y )
% 37.82/38.21 }.
% 37.82/38.21 (81804) {G0,W5,D2,L1,V0,M1} { perp( skol20, skol24, skol20, skol25 ) }.
% 37.82/38.21 (81805) {G0,W5,D2,L1,V0,M1} { perp( skol26, skol20, skol24, skol25 ) }.
% 37.82/38.21 (81806) {G0,W4,D2,L1,V0,M1} { coll( skol26, skol24, skol25 ) }.
% 37.82/38.21 (81807) {G0,W4,D2,L1,V0,M1} { midp( skol27, skol25, skol24 ) }.
% 37.82/38.21 (81808) {G0,W5,D2,L1,V0,M1} { circle( skol27, skol20, skol28, skol29 ) }.
% 37.82/38.21 (81809) {G0,W5,D2,L1,V0,M1} { perp( skol30, skol24, skol20, skol27 ) }.
% 37.82/38.21 (81810) {G0,W4,D2,L1,V0,M1} { coll( skol30, skol20, skol27 ) }.
% 37.82/38.21 (81811) {G0,W4,D2,L1,V0,M1} { coll( skol31, skol24, skol30 ) }.
% 37.82/38.21 (81812) {G0,W5,D2,L1,V0,M1} { circle( skol27, skol20, skol31, skol32 ) }.
% 37.82/38.21 (81813) {G0,W4,D2,L1,V0,M1} { coll( skol22, skol25, skol20 ) }.
% 37.82/38.21 (81814) {G0,W4,D2,L1,V0,M1} { coll( skol22, skol24, skol30 ) }.
% 37.82/38.21 (81815) {G0,W4,D2,L1,V0,M1} { coll( skol23, skol20, skol26 ) }.
% 37.82/38.21 (81816) {G0,W4,D2,L1,V0,M1} { coll( skol23, skol24, skol30 ) }.
% 37.82/38.21 (81817) {G0,W5,D2,L1,V0,M1} { ! cong( skol23, skol20, skol23, skol22 ) }.
% 37.82/38.21
% 37.82/38.21
% 37.82/38.21 Total Proof:
% 37.82/38.21
% 37.82/38.21 subsumption: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent0: (81687) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 37.82/38.21 }.
% 37.82/38.21 parent0: (81688) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Y, X, Z )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T,
% 37.82/38.21 Z ), coll( Y, Z, X ) }.
% 37.82/38.21 parent0: (81689) {G0,W12,D2,L3,V4,M3} { ! coll( X, T, Y ), ! coll( X, T, Z
% 37.82/38.21 ), coll( Y, Z, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (3) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( X, Y
% 37.82/38.21 , T, Z ) }.
% 37.82/38.21 parent0: (81690) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( X, Y,
% 37.82/38.21 T, Z ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (4) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( Z, T
% 37.82/38.21 , X, Y ) }.
% 37.82/38.21 parent0: (81691) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( Z, T,
% 37.82/38.21 X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (6) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( X, Y
% 37.82/38.21 , T, Z ) }.
% 37.82/38.21 parent0: (81693) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( X, Y,
% 37.82/38.21 T, Z ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T
% 37.82/38.21 , X, Y ) }.
% 37.82/38.21 parent0: (81694) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( Z, T,
% 37.82/38.21 X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U,
% 37.82/38.21 W, Z, T ), para( X, Y, Z, T ) }.
% 37.82/38.21 parent0: (81695) {G0,W15,D2,L3,V6,M3} { ! perp( X, Y, U, W ), ! perp( U, W
% 37.82/38.21 , Z, T ), para( X, Y, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 W := W
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (9) {G0,W15,D2,L3,V6,M3} I { ! para( X, Y, U, W ), ! perp( U,
% 37.82/38.21 W, Z, T ), perp( X, Y, Z, T ) }.
% 37.82/38.21 parent0: (81696) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! perp( U, W
% 37.82/38.21 , Z, T ), perp( X, Y, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 W := W
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y
% 37.82/38.21 ) }.
% 37.82/38.21 parent0: (81697) {G0,W8,D2,L2,V3,M2} { ! midp( Z, Y, X ), midp( Z, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 37.82/38.21 X, Z, Y, T ) }.
% 37.82/38.21 parent0: (81701) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X
% 37.82/38.21 , Z, Y, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 37.82/38.21 Y, X, Z, T ) }.
% 37.82/38.21 parent0: (81702) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Y
% 37.82/38.21 , X, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (23) {G0,W10,D2,L2,V4,M2} I { ! cong( X, Y, Z, T ), cong( Z, T
% 37.82/38.21 , X, Y ) }.
% 37.82/38.21 parent0: (81710) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( Z, T,
% 37.82/38.21 X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X
% 37.82/38.21 , Y, U, W, Z, T, U, W ) }.
% 37.82/38.21 parent0: (81726) {G0,W14,D2,L2,V6,M2} { ! para( X, Y, Z, T ), eqangle( X,
% 37.82/38.21 Y, U, W, Z, T, U, W ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 W := W
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (40) {G0,W14,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), eqangle
% 37.82/38.21 ( Z, X, Z, Y, T, X, T, Y ) }.
% 37.82/38.21 parent0: (81727) {G0,W14,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), eqangle( Z
% 37.82/38.21 , X, Z, Y, T, X, T, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T,
% 37.82/38.21 Y ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 37.82/38.21 parent0: (81729) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y
% 37.82/38.21 ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (43) {G0,W29,D2,L5,V6,M5} I { ! cyclic( X, Y, U, Z ), ! cyclic
% 37.82/38.21 ( X, Y, U, T ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T
% 37.82/38.21 ), cong( X, Y, Z, T ) }.
% 37.82/38.21 parent0: (81730) {G0,W29,D2,L5,V6,M5} { ! cyclic( X, Y, U, Z ), ! cyclic(
% 37.82/38.21 X, Y, U, T ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T )
% 37.82/38.21 , cong( X, Y, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 W := W
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 3 ==> 3
% 37.82/38.21 4 ==> 4
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (55) {G0,W14,D2,L3,V4,M3} I { ! midp( T, X, Y ), ! perp( Z, T
% 37.82/38.21 , X, Y ), cong( Z, X, Z, Y ) }.
% 37.82/38.21 parent0: (81742) {G0,W14,D2,L3,V4,M3} { ! midp( T, X, Y ), ! perp( Z, T, X
% 37.82/38.21 , Y ), cong( Z, X, Z, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (56) {G0,W15,D2,L3,V4,M3} I { ! cong( X, Z, Y, Z ), ! cong( X
% 37.82/38.21 , T, Y, T ), perp( X, Y, Z, T ) }.
% 37.82/38.21 parent0: (81743) {G0,W15,D2,L3,V4,M3} { ! cong( X, Z, Y, Z ), ! cong( X, T
% 37.82/38.21 , Y, T ), perp( X, Y, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (63) {G0,W13,D2,L3,V5,M3} I { ! midp( U, X, Y ), ! midp( U, Z
% 37.82/38.21 , T ), para( X, Z, Y, T ) }.
% 37.82/38.21 parent0: (81750) {G0,W13,D2,L3,V5,M3} { ! midp( U, X, Y ), ! midp( U, Z, T
% 37.82/38.21 ), para( X, Z, Y, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (69) {G0,W8,D2,L2,V3,M2} I { ! midp( X, Y, Z ), coll( X, Y, Z
% 37.82/38.21 ) }.
% 37.82/38.21 parent0: (81756) {G0,W8,D2,L2,V3,M2} { ! midp( X, Y, Z ), coll( X, Y, Z )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (88) {G0,W22,D3,L5,V7,M5} I { ! midp( Z, X, Y ), ! midp( W, T
% 37.82/38.21 , U ), ! coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0
% 37.82/38.21 ) }.
% 37.82/38.21 parent0: (81776) {G0,W22,D3,L5,V7,M5} { ! midp( Z, X, Y ), ! midp( W, T, U
% 37.82/38.21 ), ! coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0 )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 W := W
% 37.82/38.21 V0 := V0
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 3 ==> 3
% 37.82/38.21 4 ==> 4
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (94) {G0,W17,D3,L3,V5,M3} I { ! perp( X, T, Y, Z ), ! perp( Y
% 37.82/38.21 , T, X, Z ), coll( skol10( U, Y, Z ), Z, Y ) }.
% 37.82/38.21 parent0: (81782) {G0,W17,D3,L3,V5,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T
% 37.82/38.21 , X, Z ), coll( skol10( U, Y, Z ), Z, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (116) {G0,W5,D2,L1,V0,M1} I { perp( skol20, skol24, skol20,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 parent0: (81804) {G0,W5,D2,L1,V0,M1} { perp( skol20, skol24, skol20,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (118) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol24, skol25 )
% 37.82/38.21 }.
% 37.82/38.21 parent0: (81806) {G0,W4,D2,L1,V0,M1} { coll( skol26, skol24, skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (119) {G0,W4,D2,L1,V0,M1} I { midp( skol27, skol25, skol24 )
% 37.82/38.21 }.
% 37.82/38.21 parent0: (81807) {G0,W4,D2,L1,V0,M1} { midp( skol27, skol25, skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (129) {G0,W5,D2,L1,V0,M1} I { ! cong( skol23, skol20, skol23,
% 37.82/38.21 skol22 ) }.
% 37.82/38.21 parent0: (81817) {G0,W5,D2,L1,V0,M1} { ! cong( skol23, skol20, skol23,
% 37.82/38.21 skol22 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 factor: (82282) {G0,W18,D3,L4,V4,M4} { ! midp( X, Y, Z ), ! coll( Y, Y, Z
% 37.82/38.21 ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 37.82/38.21 parent0[0, 1]: (88) {G0,W22,D3,L5,V7,M5} I { ! midp( Z, X, Y ), ! midp( W,
% 37.82/38.21 T, U ), ! coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0
% 37.82/38.21 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := X
% 37.82/38.21 T := Y
% 37.82/38.21 U := Z
% 37.82/38.21 W := X
% 37.82/38.21 V0 := T
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (152) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll(
% 37.82/38.21 Y, Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 37.82/38.21 parent0: (82282) {G0,W18,D3,L4,V4,M4} { ! midp( X, Y, Z ), ! coll( Y, Y, Z
% 37.82/38.21 ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 3 ==> 3
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82285) {G1,W8,D2,L2,V3,M2} { coll( Y, X, Z ), ! coll( X, Z, Y
% 37.82/38.21 ) }.
% 37.82/38.21 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 37.82/38.21 }.
% 37.82/38.21 parent1[1]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (176) {G1,W8,D2,L2,V3,M2} R(1,0) { coll( X, Y, Z ), ! coll( Y
% 37.82/38.21 , Z, X ) }.
% 37.82/38.21 parent0: (82285) {G1,W8,D2,L2,V3,M2} { coll( Y, X, Z ), ! coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82287) {G1,W16,D2,L4,V5,M4} { ! coll( X, Y, Z ), coll( Z, T,
% 37.82/38.21 X ), ! coll( T, U, X ), ! coll( T, U, Y ) }.
% 37.82/38.21 parent0[1]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 37.82/38.21 ), coll( Y, Z, X ) }.
% 37.82/38.21 parent1[2]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 37.82/38.21 ), coll( Y, Z, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := T
% 37.82/38.21 T := Y
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := T
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Y
% 37.82/38.21 T := U
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (187) {G1,W16,D2,L4,V5,M4} R(2,2) { ! coll( X, Y, Z ), coll( Z
% 37.82/38.21 , T, X ), ! coll( T, U, X ), ! coll( T, U, Y ) }.
% 37.82/38.21 parent0: (82287) {G1,W16,D2,L4,V5,M4} { ! coll( X, Y, Z ), coll( Z, T, X )
% 37.82/38.21 , ! coll( T, U, X ), ! coll( T, U, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 3 ==> 3
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82297) {G1,W12,D2,L3,V4,M3} { coll( X, Z, Y ), ! coll( Z, T,
% 37.82/38.21 X ), ! coll( Z, T, Y ) }.
% 37.82/38.21 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent1[2]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 37.82/38.21 ), coll( Y, Z, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Y
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (208) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll
% 37.82/38.21 ( X, Y, T ), coll( Z, X, T ) }.
% 37.82/38.21 parent0: (82297) {G1,W12,D2,L3,V4,M3} { coll( X, Z, Y ), ! coll( Z, T, X )
% 37.82/38.21 , ! coll( Z, T, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := T
% 37.82/38.21 Z := X
% 37.82/38.21 T := Y
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 2
% 37.82/38.21 1 ==> 0
% 37.82/38.21 2 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 factor: (82299) {G1,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, X, Z )
% 37.82/38.21 }.
% 37.82/38.21 parent0[0, 1]: (208) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), !
% 37.82/38.21 coll( X, Y, T ), coll( Z, X, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := Z
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (219) {G2,W8,D2,L2,V3,M2} F(208) { ! coll( X, Y, Z ), coll( Z
% 37.82/38.21 , X, Z ) }.
% 37.82/38.21 parent0: (82299) {G1,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, X, Z )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82301) {G1,W10,D2,L2,V4,M2} { para( X, Y, T, Z ), ! para( Z,
% 37.82/38.21 T, X, Y ) }.
% 37.82/38.21 parent0[0]: (3) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( X, Y,
% 37.82/38.21 T, Z ) }.
% 37.82/38.21 parent1[1]: (4) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( Z, T,
% 37.82/38.21 X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := T
% 37.82/38.21 Z := X
% 37.82/38.21 T := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (244) {G1,W10,D2,L2,V4,M2} R(4,3) { ! para( X, Y, Z, T ), para
% 37.82/38.21 ( Z, T, Y, X ) }.
% 37.82/38.21 parent0: (82301) {G1,W10,D2,L2,V4,M2} { para( X, Y, T, Z ), ! para( Z, T,
% 37.82/38.21 X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := T
% 37.82/38.21 Z := X
% 37.82/38.21 T := Y
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 1
% 37.82/38.21 1 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82302) {G1,W4,D2,L1,V0,M1} { coll( skol24, skol26, skol25 )
% 37.82/38.21 }.
% 37.82/38.21 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 37.82/38.21 }.
% 37.82/38.21 parent1[0]: (118) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol24, skol25 )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol26
% 37.82/38.21 Y := skol24
% 37.82/38.21 Z := skol25
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (306) {G1,W4,D2,L1,V0,M1} R(118,1) { coll( skol24, skol26,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 parent0: (82302) {G1,W4,D2,L1,V0,M1} { coll( skol24, skol26, skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82303) {G1,W4,D2,L1,V0,M1} { coll( skol24, skol25, skol26 )
% 37.82/38.21 }.
% 37.82/38.21 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent1[0]: (306) {G1,W4,D2,L1,V0,M1} R(118,1) { coll( skol24, skol26,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol24
% 37.82/38.21 Y := skol26
% 37.82/38.21 Z := skol25
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (310) {G2,W4,D2,L1,V0,M1} R(306,0) { coll( skol24, skol25,
% 37.82/38.21 skol26 ) }.
% 37.82/38.21 parent0: (82303) {G1,W4,D2,L1,V0,M1} { coll( skol24, skol25, skol26 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82304) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol24, skol26 )
% 37.82/38.21 }.
% 37.82/38.21 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 37.82/38.21 }.
% 37.82/38.21 parent1[0]: (310) {G2,W4,D2,L1,V0,M1} R(306,0) { coll( skol24, skol25,
% 37.82/38.21 skol26 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol24
% 37.82/38.21 Y := skol25
% 37.82/38.21 Z := skol26
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (313) {G3,W4,D2,L1,V0,M1} R(310,1) { coll( skol25, skol24,
% 37.82/38.21 skol26 ) }.
% 37.82/38.21 parent0: (82304) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol24, skol26 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82305) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol26, skol24 )
% 37.82/38.21 }.
% 37.82/38.21 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent1[0]: (313) {G3,W4,D2,L1,V0,M1} R(310,1) { coll( skol25, skol24,
% 37.82/38.21 skol26 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol25
% 37.82/38.21 Y := skol24
% 37.82/38.21 Z := skol26
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (316) {G4,W4,D2,L1,V0,M1} R(313,0) { coll( skol25, skol26,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 parent0: (82305) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol26, skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82306) {G1,W15,D2,L3,V6,M3} { ! para( X, Y, Z, T ), perp( X,
% 37.82/38.21 Y, U, W ), ! perp( U, W, Z, T ) }.
% 37.82/38.21 parent0[1]: (9) {G0,W15,D2,L3,V6,M3} I { ! para( X, Y, U, W ), ! perp( U, W
% 37.82/38.21 , Z, T ), perp( X, Y, Z, T ) }.
% 37.82/38.21 parent1[1]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 37.82/38.21 X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := U
% 37.82/38.21 T := W
% 37.82/38.21 U := Z
% 37.82/38.21 W := T
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := U
% 37.82/38.21 Y := W
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (320) {G1,W15,D2,L3,V6,M3} R(9,7) { ! para( X, Y, Z, T ), perp
% 37.82/38.21 ( X, Y, U, W ), ! perp( U, W, Z, T ) }.
% 37.82/38.21 parent0: (82306) {G1,W15,D2,L3,V6,M3} { ! para( X, Y, Z, T ), perp( X, Y,
% 37.82/38.21 U, W ), ! perp( U, W, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 W := W
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82307) {G1,W4,D2,L1,V0,M1} { midp( skol27, skol24, skol25 )
% 37.82/38.21 }.
% 37.82/38.21 parent0[0]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent1[0]: (119) {G0,W4,D2,L1,V0,M1} I { midp( skol27, skol25, skol24 )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol24
% 37.82/38.21 Y := skol25
% 37.82/38.21 Z := skol27
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (329) {G1,W4,D2,L1,V0,M1} R(10,119) { midp( skol27, skol24,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 parent0: (82307) {G1,W4,D2,L1,V0,M1} { midp( skol27, skol24, skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82308) {G1,W5,D2,L1,V0,M1} { perp( skol20, skol25, skol20,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 parent0[0]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 37.82/38.21 X, Y ) }.
% 37.82/38.21 parent1[0]: (116) {G0,W5,D2,L1,V0,M1} I { perp( skol20, skol24, skol20,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol20
% 37.82/38.21 Y := skol24
% 37.82/38.21 Z := skol20
% 37.82/38.21 T := skol25
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (397) {G1,W5,D2,L1,V0,M1} R(116,7) { perp( skol20, skol25,
% 37.82/38.21 skol20, skol24 ) }.
% 37.82/38.21 parent0: (82308) {G1,W5,D2,L1,V0,M1} { perp( skol20, skol25, skol20,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82309) {G1,W5,D2,L1,V0,M1} { perp( skol20, skol25, skol24,
% 37.82/38.21 skol20 ) }.
% 37.82/38.21 parent0[0]: (6) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( X, Y,
% 37.82/38.21 T, Z ) }.
% 37.82/38.21 parent1[0]: (397) {G1,W5,D2,L1,V0,M1} R(116,7) { perp( skol20, skol25,
% 37.82/38.21 skol20, skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol20
% 37.82/38.21 Y := skol25
% 37.82/38.21 Z := skol20
% 37.82/38.21 T := skol24
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (402) {G2,W5,D2,L1,V0,M1} R(397,6) { perp( skol20, skol25,
% 37.82/38.21 skol24, skol20 ) }.
% 37.82/38.21 parent0: (82309) {G1,W5,D2,L1,V0,M1} { perp( skol20, skol25, skol24,
% 37.82/38.21 skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82310) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic
% 37.82/38.21 ( X, Z, Y, T ) }.
% 37.82/38.21 parent0[0]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 37.82/38.21 , X, Z, T ) }.
% 37.82/38.21 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 37.82/38.21 , Z, Y, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := Y
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (403) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), !
% 37.82/38.21 cyclic( Y, Z, X, T ) }.
% 37.82/38.21 parent0: (82310) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic( X
% 37.82/38.21 , Z, Y, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82312) {G1,W10,D2,L2,V4,M2} { cyclic( X, Z, Y, T ), ! cyclic
% 37.82/38.21 ( Y, X, Z, T ) }.
% 37.82/38.21 parent0[0]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 37.82/38.21 , Z, Y, T ) }.
% 37.82/38.21 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 37.82/38.21 , X, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (404) {G1,W10,D2,L2,V4,M2} R(15,14) { ! cyclic( X, Y, Z, T ),
% 37.82/38.21 cyclic( Y, Z, X, T ) }.
% 37.82/38.21 parent0: (82312) {G1,W10,D2,L2,V4,M2} { cyclic( X, Z, Y, T ), ! cyclic( Y
% 37.82/38.21 , X, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 1
% 37.82/38.21 1 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82313) {G1,W5,D2,L1,V0,M1} { perp( skol24, skol20, skol20,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 parent0[0]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 37.82/38.21 X, Y ) }.
% 37.82/38.21 parent1[0]: (402) {G2,W5,D2,L1,V0,M1} R(397,6) { perp( skol20, skol25,
% 37.82/38.21 skol24, skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol20
% 37.82/38.21 Y := skol25
% 37.82/38.21 Z := skol24
% 37.82/38.21 T := skol20
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (414) {G3,W5,D2,L1,V0,M1} R(402,7) { perp( skol24, skol20,
% 37.82/38.21 skol20, skol25 ) }.
% 37.82/38.21 parent0: (82313) {G1,W5,D2,L1,V0,M1} { perp( skol24, skol20, skol20,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82314) {G1,W5,D2,L1,V0,M1} { perp( skol24, skol20, skol25,
% 37.82/38.21 skol20 ) }.
% 37.82/38.21 parent0[0]: (6) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( X, Y,
% 37.82/38.21 T, Z ) }.
% 37.82/38.21 parent1[0]: (414) {G3,W5,D2,L1,V0,M1} R(402,7) { perp( skol24, skol20,
% 37.82/38.21 skol20, skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol24
% 37.82/38.21 Y := skol20
% 37.82/38.21 Z := skol20
% 37.82/38.21 T := skol25
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (418) {G4,W5,D2,L1,V0,M1} R(414,6) { perp( skol24, skol20,
% 37.82/38.21 skol25, skol20 ) }.
% 37.82/38.21 parent0: (82314) {G1,W5,D2,L1,V0,M1} { perp( skol24, skol20, skol25,
% 37.82/38.21 skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82315) {G1,W5,D2,L1,V0,M1} { perp( skol25, skol20, skol24,
% 37.82/38.21 skol20 ) }.
% 37.82/38.21 parent0[0]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 37.82/38.21 X, Y ) }.
% 37.82/38.21 parent1[0]: (418) {G4,W5,D2,L1,V0,M1} R(414,6) { perp( skol24, skol20,
% 37.82/38.21 skol25, skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol24
% 37.82/38.21 Y := skol20
% 37.82/38.21 Z := skol25
% 37.82/38.21 T := skol20
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (422) {G5,W5,D2,L1,V0,M1} R(418,7) { perp( skol25, skol20,
% 37.82/38.21 skol24, skol20 ) }.
% 37.82/38.21 parent0: (82315) {G1,W5,D2,L1,V0,M1} { perp( skol25, skol20, skol24,
% 37.82/38.21 skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82316) {G3,W4,D2,L1,V0,M1} { coll( skol24, skol25, skol24 )
% 37.82/38.21 }.
% 37.82/38.21 parent0[0]: (219) {G2,W8,D2,L2,V3,M2} F(208) { ! coll( X, Y, Z ), coll( Z,
% 37.82/38.21 X, Z ) }.
% 37.82/38.21 parent1[0]: (316) {G4,W4,D2,L1,V0,M1} R(313,0) { coll( skol25, skol26,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol25
% 37.82/38.21 Y := skol26
% 37.82/38.21 Z := skol24
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (451) {G5,W4,D2,L1,V0,M1} R(219,316) { coll( skol24, skol25,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 parent0: (82316) {G3,W4,D2,L1,V0,M1} { coll( skol24, skol25, skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82317) {G2,W4,D2,L1,V0,M1} { coll( skol25, skol24, skol25 )
% 37.82/38.21 }.
% 37.82/38.21 parent0[0]: (219) {G2,W8,D2,L2,V3,M2} F(208) { ! coll( X, Y, Z ), coll( Z,
% 37.82/38.21 X, Z ) }.
% 37.82/38.21 parent1[0]: (306) {G1,W4,D2,L1,V0,M1} R(118,1) { coll( skol24, skol26,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol24
% 37.82/38.21 Y := skol26
% 37.82/38.21 Z := skol25
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (454) {G3,W4,D2,L1,V0,M1} R(219,306) { coll( skol25, skol24,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 parent0: (82317) {G2,W4,D2,L1,V0,M1} { coll( skol25, skol24, skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82318) {G1,W12,D2,L3,V4,M3} { coll( Z, X, Z ), ! coll( Z, T,
% 37.82/38.21 X ), ! coll( Z, T, Y ) }.
% 37.82/38.21 parent0[0]: (219) {G2,W8,D2,L2,V3,M2} F(208) { ! coll( X, Y, Z ), coll( Z,
% 37.82/38.21 X, Z ) }.
% 37.82/38.21 parent1[2]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 37.82/38.21 ), coll( Y, Z, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Y
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (476) {G3,W12,D2,L3,V4,M3} R(219,2) { coll( X, Y, X ), ! coll
% 37.82/38.21 ( X, Z, Y ), ! coll( X, Z, T ) }.
% 37.82/38.21 parent0: (82318) {G1,W12,D2,L3,V4,M3} { coll( Z, X, Z ), ! coll( Z, T, X )
% 37.82/38.21 , ! coll( Z, T, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 T := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 factor: (82320) {G3,W8,D2,L2,V3,M2} { coll( X, Y, X ), ! coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent0[1, 2]: (476) {G3,W12,D2,L3,V4,M3} R(219,2) { coll( X, Y, X ), !
% 37.82/38.21 coll( X, Z, Y ), ! coll( X, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (493) {G4,W8,D2,L2,V3,M2} F(476) { coll( X, Y, X ), ! coll( X
% 37.82/38.21 , Z, Y ) }.
% 37.82/38.21 parent0: (82320) {G3,W8,D2,L2,V3,M2} { coll( X, Y, X ), ! coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82321) {G1,W4,D2,L1,V0,M1} { coll( skol24, skol24, skol25 )
% 37.82/38.21 }.
% 37.82/38.21 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent1[0]: (451) {G5,W4,D2,L1,V0,M1} R(219,316) { coll( skol24, skol25,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol24
% 37.82/38.21 Y := skol25
% 37.82/38.21 Z := skol24
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (503) {G6,W4,D2,L1,V0,M1} R(451,0) { coll( skol24, skol24,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 parent0: (82321) {G1,W4,D2,L1,V0,M1} { coll( skol24, skol24, skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82322) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol25, skol24 )
% 37.82/38.21 }.
% 37.82/38.21 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent1[0]: (454) {G3,W4,D2,L1,V0,M1} R(219,306) { coll( skol25, skol24,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol25
% 37.82/38.21 Y := skol24
% 37.82/38.21 Z := skol25
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (531) {G4,W4,D2,L1,V0,M1} R(454,0) { coll( skol25, skol25,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 parent0: (82322) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol25, skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82323) {G1,W5,D2,L1,V0,M1} { ! cong( skol23, skol22, skol23,
% 37.82/38.21 skol20 ) }.
% 37.82/38.21 parent0[0]: (129) {G0,W5,D2,L1,V0,M1} I { ! cong( skol23, skol20, skol23,
% 37.82/38.21 skol22 ) }.
% 37.82/38.21 parent1[1]: (23) {G0,W10,D2,L2,V4,M2} I { ! cong( X, Y, Z, T ), cong( Z, T
% 37.82/38.21 , X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := skol23
% 37.82/38.21 Y := skol22
% 37.82/38.21 Z := skol23
% 37.82/38.21 T := skol20
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (576) {G1,W5,D2,L1,V0,M1} R(23,129) { ! cong( skol23, skol22,
% 37.82/38.21 skol23, skol20 ) }.
% 37.82/38.21 parent0: (82323) {G1,W5,D2,L1,V0,M1} { ! cong( skol23, skol22, skol23,
% 37.82/38.21 skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82324) {G1,W14,D2,L3,V3,M3} { ! coll( X, X, Z ), cyclic( Y, Z
% 37.82/38.21 , X, X ), ! para( X, Y, X, Y ) }.
% 37.82/38.21 parent0[0]: (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T, Y
% 37.82/38.21 ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 37.82/38.21 parent1[1]: (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X
% 37.82/38.21 , Y, U, W, Z, T, U, W ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := X
% 37.82/38.21 T := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 T := Y
% 37.82/38.21 U := X
% 37.82/38.21 W := Z
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (862) {G1,W14,D2,L3,V3,M3} R(42,39) { ! coll( X, X, Y ),
% 37.82/38.21 cyclic( Z, Y, X, X ), ! para( X, Z, X, Z ) }.
% 37.82/38.21 parent0: (82324) {G1,W14,D2,L3,V3,M3} { ! coll( X, X, Z ), cyclic( Y, Z, X
% 37.82/38.21 , X ), ! para( X, Y, X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := Y
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82325) {G1,W25,D2,L5,V4,M5} { ! cyclic( X, Y, Z, X ), !
% 37.82/38.21 cyclic( X, Y, Z, Y ), ! cyclic( X, Y, Z, T ), cong( X, Y, X, Y ), !
% 37.82/38.21 cyclic( X, Y, Z, T ) }.
% 37.82/38.21 parent0[3]: (43) {G0,W29,D2,L5,V6,M5} I { ! cyclic( X, Y, U, Z ), ! cyclic
% 37.82/38.21 ( X, Y, U, T ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T
% 37.82/38.21 ), cong( X, Y, Z, T ) }.
% 37.82/38.21 parent1[1]: (40) {G0,W14,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), eqangle(
% 37.82/38.21 Z, X, Z, Y, T, X, T, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 T := Y
% 37.82/38.21 U := Z
% 37.82/38.21 W := T
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 factor: (82327) {G1,W20,D2,L4,V3,M4} { ! cyclic( X, Y, Z, X ), ! cyclic( X
% 37.82/38.21 , Y, Z, Y ), cong( X, Y, X, Y ), ! cyclic( X, Y, Z, X ) }.
% 37.82/38.21 parent0[0, 2]: (82325) {G1,W25,D2,L5,V4,M5} { ! cyclic( X, Y, Z, X ), !
% 37.82/38.21 cyclic( X, Y, Z, Y ), ! cyclic( X, Y, Z, T ), cong( X, Y, X, Y ), !
% 37.82/38.21 cyclic( X, Y, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1026) {G1,W20,D2,L4,V4,M4} R(43,40);f { ! cyclic( X, Y, Z, X
% 37.82/38.21 ), ! cyclic( X, Y, Z, Y ), ! cyclic( X, Y, Z, T ), cong( X, Y, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent0: (82327) {G1,W20,D2,L4,V3,M4} { ! cyclic( X, Y, Z, X ), ! cyclic(
% 37.82/38.21 X, Y, Z, Y ), cong( X, Y, X, Y ), ! cyclic( X, Y, Z, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 3
% 37.82/38.21 3 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 factor: (82332) {G1,W15,D2,L3,V3,M3} { ! cyclic( X, Y, Z, X ), ! cyclic( X
% 37.82/38.21 , Y, Z, Y ), cong( X, Y, X, Y ) }.
% 37.82/38.21 parent0[0, 2]: (1026) {G1,W20,D2,L4,V4,M4} R(43,40);f { ! cyclic( X, Y, Z,
% 37.82/38.21 X ), ! cyclic( X, Y, Z, Y ), ! cyclic( X, Y, Z, T ), cong( X, Y, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1059) {G2,W15,D2,L3,V3,M3} F(1026) { ! cyclic( X, Y, Z, X ),
% 37.82/38.21 ! cyclic( X, Y, Z, Y ), cong( X, Y, X, Y ) }.
% 37.82/38.21 parent0: (82332) {G1,W15,D2,L3,V3,M3} { ! cyclic( X, Y, Z, X ), ! cyclic(
% 37.82/38.21 X, Y, Z, Y ), cong( X, Y, X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82335) {G1,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( X, Z, Y
% 37.82/38.21 ) }.
% 37.82/38.21 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 37.82/38.21 }.
% 37.82/38.21 parent1[0]: (493) {G4,W8,D2,L2,V3,M2} F(476) { coll( X, Y, X ), ! coll( X,
% 37.82/38.21 Z, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1418) {G5,W8,D2,L2,V3,M2} R(493,1) { ! coll( X, Y, Z ), coll
% 37.82/38.21 ( Z, X, X ) }.
% 37.82/38.21 parent0: (82335) {G1,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := Y
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 1
% 37.82/38.21 1 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82336) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( Y, X, Z
% 37.82/38.21 ) }.
% 37.82/38.21 parent0[0]: (1418) {G5,W8,D2,L2,V3,M2} R(493,1) { ! coll( X, Y, Z ), coll(
% 37.82/38.21 Z, X, X ) }.
% 37.82/38.21 parent1[1]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1423) {G6,W8,D2,L2,V3,M2} R(1418,1) { coll( X, Y, Y ), ! coll
% 37.82/38.21 ( Z, Y, X ) }.
% 37.82/38.21 parent0: (82336) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( Y, X, Z )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82337) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( X, Z, Y
% 37.82/38.21 ) }.
% 37.82/38.21 parent0[0]: (1418) {G5,W8,D2,L2,V3,M2} R(493,1) { ! coll( X, Y, Z ), coll(
% 37.82/38.21 Z, X, X ) }.
% 37.82/38.21 parent1[1]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1424) {G6,W8,D2,L2,V3,M2} R(1418,0) { coll( X, Y, Y ), ! coll
% 37.82/38.21 ( Y, X, Z ) }.
% 37.82/38.21 parent0: (82337) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( X, Z, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82339) {G6,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( Z, Y, X
% 37.82/38.21 ) }.
% 37.82/38.21 parent0[0]: (1418) {G5,W8,D2,L2,V3,M2} R(493,1) { ! coll( X, Y, Z ), coll(
% 37.82/38.21 Z, X, X ) }.
% 37.82/38.21 parent1[0]: (1423) {G6,W8,D2,L2,V3,M2} R(1418,1) { coll( X, Y, Y ), ! coll
% 37.82/38.21 ( Z, Y, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Y
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1425) {G7,W8,D2,L2,V3,M2} R(1423,1418) { ! coll( X, Y, Z ),
% 37.82/38.21 coll( Y, Z, Z ) }.
% 37.82/38.21 parent0: (82339) {G6,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( Z, Y, X )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 1
% 37.82/38.21 1 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82340) {G7,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! coll( X, Y, Z
% 37.82/38.21 ) }.
% 37.82/38.21 parent0[1]: (1424) {G6,W8,D2,L2,V3,M2} R(1418,0) { coll( X, Y, Y ), ! coll
% 37.82/38.21 ( Y, X, Z ) }.
% 37.82/38.21 parent1[0]: (1424) {G6,W8,D2,L2,V3,M2} R(1418,0) { coll( X, Y, Y ), ! coll
% 37.82/38.21 ( Y, X, Z ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1456) {G7,W8,D2,L2,V3,M2} R(1424,1424) { ! coll( X, Y, Z ),
% 37.82/38.21 coll( X, Y, Y ) }.
% 37.82/38.21 parent0: (82340) {G7,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! coll( X, Y, Z )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 1
% 37.82/38.21 1 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82344) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, Y,
% 37.82/38.21 X ), ! coll( X, Y, T ) }.
% 37.82/38.21 parent0[1]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 37.82/38.21 ), coll( Y, Z, X ) }.
% 37.82/38.21 parent1[1]: (1456) {G7,W8,D2,L2,V3,M2} R(1424,1424) { ! coll( X, Y, Z ),
% 37.82/38.21 coll( X, Y, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := Y
% 37.82/38.21 T := Y
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := T
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1459) {G8,W12,D2,L3,V4,M3} R(1456,2) { ! coll( X, Y, Z ), !
% 37.82/38.21 coll( X, Y, T ), coll( T, Y, X ) }.
% 37.82/38.21 parent0: (82344) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 37.82/38.21 , ! coll( X, Y, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := T
% 37.82/38.21 T := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 1
% 37.82/38.21 1 ==> 2
% 37.82/38.21 2 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 factor: (82347) {G8,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 37.82/38.21 }.
% 37.82/38.21 parent0[0, 1]: (1459) {G8,W12,D2,L3,V4,M3} R(1456,2) { ! coll( X, Y, Z ), !
% 37.82/38.21 coll( X, Y, T ), coll( T, Y, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := Z
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1460) {G9,W8,D2,L2,V3,M2} F(1459) { ! coll( X, Y, Z ), coll(
% 37.82/38.21 Z, Y, X ) }.
% 37.82/38.21 parent0: (82347) {G8,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82348) {G8,W8,D2,L2,V3,M2} { coll( Y, Y, X ), ! coll( Z, X, Y
% 37.82/38.21 ) }.
% 37.82/38.21 parent0[0]: (1460) {G9,W8,D2,L2,V3,M2} F(1459) { ! coll( X, Y, Z ), coll( Z
% 37.82/38.21 , Y, X ) }.
% 37.82/38.21 parent1[1]: (1425) {G7,W8,D2,L2,V3,M2} R(1423,1418) { ! coll( X, Y, Z ),
% 37.82/38.21 coll( Y, Z, Z ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Y
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1463) {G10,W8,D2,L2,V3,M2} R(1460,1425) { coll( X, X, Y ), !
% 37.82/38.21 coll( Z, Y, X ) }.
% 37.82/38.21 parent0: (82348) {G8,W8,D2,L2,V3,M2} { coll( Y, Y, X ), ! coll( Z, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82349) {G1,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! midp( Z, Y, X
% 37.82/38.21 ) }.
% 37.82/38.21 parent0[1]: (1423) {G6,W8,D2,L2,V3,M2} R(1418,1) { coll( X, Y, Y ), ! coll
% 37.82/38.21 ( Z, Y, X ) }.
% 37.82/38.21 parent1[1]: (69) {G0,W8,D2,L2,V3,M2} I { ! midp( X, Y, Z ), coll( X, Y, Z )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1749) {G7,W8,D2,L2,V3,M2} R(69,1423) { ! midp( X, Y, Z ),
% 37.82/38.21 coll( Z, Y, Y ) }.
% 37.82/38.21 parent0: (82349) {G1,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! midp( Z, Y, X )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 1
% 37.82/38.21 1 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82350) {G1,W9,D2,L2,V1,M2} { ! midp( X, skol22, skol20 ), !
% 37.82/38.21 perp( skol23, X, skol22, skol20 ) }.
% 37.82/38.21 parent0[0]: (576) {G1,W5,D2,L1,V0,M1} R(23,129) { ! cong( skol23, skol22,
% 37.82/38.21 skol23, skol20 ) }.
% 37.82/38.21 parent1[2]: (55) {G0,W14,D2,L3,V4,M3} I { ! midp( T, X, Y ), ! perp( Z, T,
% 37.82/38.21 X, Y ), cong( Z, X, Z, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := skol22
% 37.82/38.21 Y := skol20
% 37.82/38.21 Z := skol23
% 37.82/38.21 T := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1766) {G2,W9,D2,L2,V1,M2} R(55,576) { ! midp( X, skol22,
% 37.82/38.21 skol20 ), ! perp( skol23, X, skol22, skol20 ) }.
% 37.82/38.21 parent0: (82350) {G1,W9,D2,L2,V1,M2} { ! midp( X, skol22, skol20 ), ! perp
% 37.82/38.21 ( skol23, X, skol22, skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82352) {G1,W20,D2,L4,V6,M4} { ! perp( X, Y, Z, T ), para( X,
% 37.82/38.21 Y, U, W ), ! cong( Z, U, T, U ), ! cong( Z, W, T, W ) }.
% 37.82/38.21 parent0[1]: (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U, W
% 37.82/38.21 , Z, T ), para( X, Y, Z, T ) }.
% 37.82/38.21 parent1[2]: (56) {G0,W15,D2,L3,V4,M3} I { ! cong( X, Z, Y, Z ), ! cong( X,
% 37.82/38.21 T, Y, T ), perp( X, Y, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := U
% 37.82/38.21 T := W
% 37.82/38.21 U := Z
% 37.82/38.21 W := T
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := T
% 37.82/38.21 Z := U
% 37.82/38.21 T := W
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1863) {G1,W20,D2,L4,V6,M4} R(56,8) { ! cong( X, Y, Z, Y ), !
% 37.82/38.21 cong( X, T, Z, T ), ! perp( U, W, X, Z ), para( U, W, Y, T ) }.
% 37.82/38.21 parent0: (82352) {G1,W20,D2,L4,V6,M4} { ! perp( X, Y, Z, T ), para( X, Y,
% 37.82/38.21 U, W ), ! cong( Z, U, T, U ), ! cong( Z, W, T, W ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := U
% 37.82/38.21 Y := W
% 37.82/38.21 Z := X
% 37.82/38.21 T := Z
% 37.82/38.21 U := Y
% 37.82/38.21 W := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 2
% 37.82/38.21 1 ==> 3
% 37.82/38.21 2 ==> 0
% 37.82/38.21 3 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82355) {G1,W15,D2,L3,V4,M3} { perp( Z, T, X, Y ), ! cong( X,
% 37.82/38.21 Z, Y, Z ), ! cong( X, T, Y, T ) }.
% 37.82/38.21 parent0[0]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 37.82/38.21 X, Y ) }.
% 37.82/38.21 parent1[2]: (56) {G0,W15,D2,L3,V4,M3} I { ! cong( X, Z, Y, Z ), ! cong( X,
% 37.82/38.21 T, Y, T ), perp( X, Y, Z, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1864) {G1,W15,D2,L3,V4,M3} R(56,7) { ! cong( X, Y, Z, Y ), !
% 37.82/38.21 cong( X, T, Z, T ), perp( Y, T, X, Z ) }.
% 37.82/38.21 parent0: (82355) {G1,W15,D2,L3,V4,M3} { perp( Z, T, X, Y ), ! cong( X, Z,
% 37.82/38.21 Y, Z ), ! cong( X, T, Y, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := Y
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 2
% 37.82/38.21 1 ==> 0
% 37.82/38.21 2 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 factor: (82357) {G1,W15,D2,L3,V5,M3} { ! cong( X, Y, Z, Y ), ! perp( T, U
% 37.82/38.21 , X, Z ), para( T, U, Y, Y ) }.
% 37.82/38.21 parent0[0, 1]: (1863) {G1,W20,D2,L4,V6,M4} R(56,8) { ! cong( X, Y, Z, Y ),
% 37.82/38.21 ! cong( X, T, Z, T ), ! perp( U, W, X, Z ), para( U, W, Y, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := Y
% 37.82/38.21 U := T
% 37.82/38.21 W := U
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (1866) {G2,W15,D2,L3,V5,M3} F(1863) { ! cong( X, Y, Z, Y ), !
% 37.82/38.21 perp( T, U, X, Z ), para( T, U, Y, Y ) }.
% 37.82/38.21 parent0: (82357) {G1,W15,D2,L3,V5,M3} { ! cong( X, Y, Z, Y ), ! perp( T, U
% 37.82/38.21 , X, Z ), para( T, U, Y, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82359) {G1,W13,D2,L3,V5,M3} { ! midp( X, Y, Z ), para( Y, T,
% 37.82/38.21 Z, U ), ! midp( X, U, T ) }.
% 37.82/38.21 parent0[1]: (63) {G0,W13,D2,L3,V5,M3} I { ! midp( U, X, Y ), ! midp( U, Z,
% 37.82/38.21 T ), para( X, Z, Y, T ) }.
% 37.82/38.21 parent1[1]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := T
% 37.82/38.21 T := U
% 37.82/38.21 U := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := T
% 37.82/38.21 Y := U
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (2102) {G1,W13,D2,L3,V5,M3} R(63,10) { ! midp( X, Y, Z ), para
% 37.82/38.21 ( Y, T, Z, U ), ! midp( X, U, T ) }.
% 37.82/38.21 parent0: (82359) {G1,W13,D2,L3,V5,M3} { ! midp( X, Y, Z ), para( Y, T, Z,
% 37.82/38.21 U ), ! midp( X, U, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 2 ==> 2
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 factor: (82362) {G1,W9,D2,L2,V3,M2} { ! midp( X, Y, Z ), para( Y, Z, Z, Y
% 37.82/38.21 ) }.
% 37.82/38.21 parent0[0, 2]: (2102) {G1,W13,D2,L3,V5,M3} R(63,10) { ! midp( X, Y, Z ),
% 37.82/38.21 para( Y, T, Z, U ), ! midp( X, U, T ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := Z
% 37.82/38.21 U := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (2114) {G2,W9,D2,L2,V3,M2} F(2102) { ! midp( X, Y, Z ), para(
% 37.82/38.21 Y, Z, Z, Y ) }.
% 37.82/38.21 parent0: (82362) {G1,W9,D2,L2,V3,M2} { ! midp( X, Y, Z ), para( Y, Z, Z, Y
% 37.82/38.21 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82363) {G1,W12,D3,L2,V1,M2} { ! perp( skol24, skol20, skol25
% 37.82/38.21 , skol20 ), coll( skol10( X, skol24, skol20 ), skol20, skol24 ) }.
% 37.82/38.21 parent0[0]: (94) {G0,W17,D3,L3,V5,M3} I { ! perp( X, T, Y, Z ), ! perp( Y,
% 37.82/38.21 T, X, Z ), coll( skol10( U, Y, Z ), Z, Y ) }.
% 37.82/38.21 parent1[0]: (422) {G5,W5,D2,L1,V0,M1} R(418,7) { perp( skol25, skol20,
% 37.82/38.21 skol24, skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol25
% 37.82/38.21 Y := skol24
% 37.82/38.21 Z := skol20
% 37.82/38.21 T := skol20
% 37.82/38.21 U := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82365) {G2,W7,D3,L1,V1,M1} { coll( skol10( X, skol24, skol20
% 37.82/38.21 ), skol20, skol24 ) }.
% 37.82/38.21 parent0[0]: (82363) {G1,W12,D3,L2,V1,M2} { ! perp( skol24, skol20, skol25
% 37.82/38.21 , skol20 ), coll( skol10( X, skol24, skol20 ), skol20, skol24 ) }.
% 37.82/38.21 parent1[0]: (418) {G4,W5,D2,L1,V0,M1} R(414,6) { perp( skol24, skol20,
% 37.82/38.21 skol25, skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (4092) {G6,W7,D3,L1,V1,M1} R(94,422);r(418) { coll( skol10( X
% 37.82/38.21 , skol24, skol20 ), skol20, skol24 ) }.
% 37.82/38.21 parent0: (82365) {G2,W7,D3,L1,V1,M1} { coll( skol10( X, skol24, skol20 ),
% 37.82/38.21 skol20, skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82366) {G7,W4,D2,L1,V0,M1} { coll( skol24, skol24, skol20 )
% 37.82/38.21 }.
% 37.82/38.21 parent0[1]: (1463) {G10,W8,D2,L2,V3,M2} R(1460,1425) { coll( X, X, Y ), !
% 37.82/38.21 coll( Z, Y, X ) }.
% 37.82/38.21 parent1[0]: (4092) {G6,W7,D3,L1,V1,M1} R(94,422);r(418) { coll( skol10( X,
% 37.82/38.21 skol24, skol20 ), skol20, skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol24
% 37.82/38.21 Y := skol20
% 37.82/38.21 Z := skol10( X, skol24, skol20 )
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (4158) {G11,W4,D2,L1,V0,M1} R(4092,1463) { coll( skol24,
% 37.82/38.21 skol24, skol20 ) }.
% 37.82/38.21 parent0: (82366) {G7,W4,D2,L1,V0,M1} { coll( skol24, skol24, skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82367) {G2,W14,D3,L3,V1,M3} { ! coll( skol24, skol24, skol25
% 37.82/38.21 ), ! coll( skol25, skol24, skol25 ), midp( skol7( skol24, X ), skol24, X
% 37.82/38.21 ) }.
% 37.82/38.21 parent0[0]: (152) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y
% 37.82/38.21 , Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 37.82/38.21 parent1[0]: (329) {G1,W4,D2,L1,V0,M1} R(10,119) { midp( skol27, skol24,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol27
% 37.82/38.21 Y := skol24
% 37.82/38.21 Z := skol25
% 37.82/38.21 T := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82368) {G3,W10,D3,L2,V1,M2} { ! coll( skol25, skol24, skol25
% 37.82/38.21 ), midp( skol7( skol24, X ), skol24, X ) }.
% 37.82/38.21 parent0[0]: (82367) {G2,W14,D3,L3,V1,M3} { ! coll( skol24, skol24, skol25
% 37.82/38.21 ), ! coll( skol25, skol24, skol25 ), midp( skol7( skol24, X ), skol24, X
% 37.82/38.21 ) }.
% 37.82/38.21 parent1[0]: (503) {G6,W4,D2,L1,V0,M1} R(451,0) { coll( skol24, skol24,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (8164) {G7,W10,D3,L2,V1,M2} R(152,329);r(503) { ! coll( skol25
% 37.82/38.21 , skol24, skol25 ), midp( skol7( skol24, X ), skol24, X ) }.
% 37.82/38.21 parent0: (82368) {G3,W10,D3,L2,V1,M2} { ! coll( skol25, skol24, skol25 ),
% 37.82/38.21 midp( skol7( skol24, X ), skol24, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82369) {G1,W14,D3,L3,V1,M3} { ! coll( skol25, skol25, skol24
% 37.82/38.21 ), ! coll( skol24, skol25, skol24 ), midp( skol7( skol25, X ), skol25, X
% 37.82/38.21 ) }.
% 37.82/38.21 parent0[0]: (152) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y
% 37.82/38.21 , Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 37.82/38.21 parent1[0]: (119) {G0,W4,D2,L1,V0,M1} I { midp( skol27, skol25, skol24 )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol27
% 37.82/38.21 Y := skol25
% 37.82/38.21 Z := skol24
% 37.82/38.21 T := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82370) {G2,W10,D3,L2,V1,M2} { ! coll( skol24, skol25, skol24
% 37.82/38.21 ), midp( skol7( skol25, X ), skol25, X ) }.
% 37.82/38.21 parent0[0]: (82369) {G1,W14,D3,L3,V1,M3} { ! coll( skol25, skol25, skol24
% 37.82/38.21 ), ! coll( skol24, skol25, skol24 ), midp( skol7( skol25, X ), skol25, X
% 37.82/38.21 ) }.
% 37.82/38.21 parent1[0]: (531) {G4,W4,D2,L1,V0,M1} R(454,0) { coll( skol25, skol25,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (8165) {G5,W10,D3,L2,V1,M2} R(152,119);r(531) { ! coll( skol24
% 37.82/38.21 , skol25, skol24 ), midp( skol7( skol25, X ), skol25, X ) }.
% 37.82/38.21 parent0: (82370) {G2,W10,D3,L2,V1,M2} { ! coll( skol24, skol25, skol24 ),
% 37.82/38.21 midp( skol7( skol25, X ), skol25, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82371) {G2,W12,D2,L3,V2,M3} { coll( skol20, X, skol24 ), !
% 37.82/38.21 coll( X, Y, skol24 ), ! coll( X, Y, skol24 ) }.
% 37.82/38.21 parent0[0]: (187) {G1,W16,D2,L4,V5,M4} R(2,2) { ! coll( X, Y, Z ), coll( Z
% 37.82/38.21 , T, X ), ! coll( T, U, X ), ! coll( T, U, Y ) }.
% 37.82/38.21 parent1[0]: (4158) {G11,W4,D2,L1,V0,M1} R(4092,1463) { coll( skol24, skol24
% 37.82/38.21 , skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol24
% 37.82/38.21 Y := skol24
% 37.82/38.21 Z := skol20
% 37.82/38.21 T := X
% 37.82/38.21 U := Y
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 factor: (82374) {G2,W8,D2,L2,V2,M2} { coll( skol20, X, skol24 ), ! coll( X
% 37.82/38.21 , Y, skol24 ) }.
% 37.82/38.21 parent0[1, 2]: (82371) {G2,W12,D2,L3,V2,M3} { coll( skol20, X, skol24 ), !
% 37.82/38.21 coll( X, Y, skol24 ), ! coll( X, Y, skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (9555) {G12,W8,D2,L2,V2,M2} R(187,4158);f { coll( skol20, X,
% 37.82/38.21 skol24 ), ! coll( X, Y, skol24 ) }.
% 37.82/38.21 parent0: (82374) {G2,W8,D2,L2,V2,M2} { coll( skol20, X, skol24 ), ! coll(
% 37.82/38.21 X, Y, skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82375) {G4,W6,D3,L1,V1,M1} { midp( skol7( skol24, X ), skol24
% 37.82/38.21 , X ) }.
% 37.82/38.21 parent0[0]: (8164) {G7,W10,D3,L2,V1,M2} R(152,329);r(503) { ! coll( skol25
% 37.82/38.21 , skol24, skol25 ), midp( skol7( skol24, X ), skol24, X ) }.
% 37.82/38.21 parent1[0]: (454) {G3,W4,D2,L1,V0,M1} R(219,306) { coll( skol25, skol24,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (20078) {G8,W6,D3,L1,V1,M1} S(8164);r(454) { midp( skol7(
% 37.82/38.21 skol24, X ), skol24, X ) }.
% 37.82/38.21 parent0: (82375) {G4,W6,D3,L1,V1,M1} { midp( skol7( skol24, X ), skol24, X
% 37.82/38.21 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82376) {G6,W6,D3,L1,V1,M1} { midp( skol7( skol25, X ), skol25
% 37.82/38.21 , X ) }.
% 37.82/38.21 parent0[0]: (8165) {G5,W10,D3,L2,V1,M2} R(152,119);r(531) { ! coll( skol24
% 37.82/38.21 , skol25, skol24 ), midp( skol7( skol25, X ), skol25, X ) }.
% 37.82/38.21 parent1[0]: (451) {G5,W4,D2,L1,V0,M1} R(219,316) { coll( skol24, skol25,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (20079) {G6,W6,D3,L1,V1,M1} S(8165);r(451) { midp( skol7(
% 37.82/38.21 skol25, X ), skol25, X ) }.
% 37.82/38.21 parent0: (82376) {G6,W6,D3,L1,V1,M1} { midp( skol7( skol25, X ), skol25, X
% 37.82/38.21 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82377) {G8,W4,D2,L1,V1,M1} { coll( X, skol24, skol24 ) }.
% 37.82/38.21 parent0[0]: (1749) {G7,W8,D2,L2,V3,M2} R(69,1423) { ! midp( X, Y, Z ), coll
% 37.82/38.21 ( Z, Y, Y ) }.
% 37.82/38.21 parent1[0]: (20078) {G8,W6,D3,L1,V1,M1} S(8164);r(454) { midp( skol7(
% 37.82/38.21 skol24, X ), skol24, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol7( skol24, X )
% 37.82/38.21 Y := skol24
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (29734) {G9,W4,D2,L1,V1,M1} R(20078,1749) { coll( X, skol24,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 parent0: (82377) {G8,W4,D2,L1,V1,M1} { coll( X, skol24, skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82378) {G10,W4,D2,L1,V1,M1} { coll( skol20, X, skol24 ) }.
% 37.82/38.21 parent0[1]: (9555) {G12,W8,D2,L2,V2,M2} R(187,4158);f { coll( skol20, X,
% 37.82/38.21 skol24 ), ! coll( X, Y, skol24 ) }.
% 37.82/38.21 parent1[0]: (29734) {G9,W4,D2,L1,V1,M1} R(20078,1749) { coll( X, skol24,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := skol24
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (29775) {G13,W4,D2,L1,V1,M1} R(29734,9555) { coll( skol20, X,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 parent0: (82378) {G10,W4,D2,L1,V1,M1} { coll( skol20, X, skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82379) {G2,W4,D2,L1,V1,M1} { coll( skol24, skol20, X ) }.
% 37.82/38.21 parent0[1]: (176) {G1,W8,D2,L2,V3,M2} R(1,0) { coll( X, Y, Z ), ! coll( Y,
% 37.82/38.21 Z, X ) }.
% 37.82/38.21 parent1[0]: (29775) {G13,W4,D2,L1,V1,M1} R(29734,9555) { coll( skol20, X,
% 37.82/38.21 skol24 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol24
% 37.82/38.21 Y := skol20
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (29805) {G14,W4,D2,L1,V1,M1} R(29775,176) { coll( skol24,
% 37.82/38.21 skol20, X ) }.
% 37.82/38.21 parent0: (82379) {G2,W4,D2,L1,V1,M1} { coll( skol24, skol20, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82380) {G2,W8,D2,L2,V2,M2} { ! coll( skol24, skol20, Y ),
% 37.82/38.21 coll( X, skol24, Y ) }.
% 37.82/38.21 parent0[0]: (208) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll(
% 37.82/38.21 X, Y, T ), coll( Z, X, T ) }.
% 37.82/38.21 parent1[0]: (29805) {G14,W4,D2,L1,V1,M1} R(29775,176) { coll( skol24,
% 37.82/38.21 skol20, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol24
% 37.82/38.21 Y := skol20
% 37.82/38.21 Z := X
% 37.82/38.21 T := Y
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82382) {G3,W4,D2,L1,V2,M1} { coll( Y, skol24, X ) }.
% 37.82/38.21 parent0[0]: (82380) {G2,W8,D2,L2,V2,M2} { ! coll( skol24, skol20, Y ),
% 37.82/38.21 coll( X, skol24, Y ) }.
% 37.82/38.21 parent1[0]: (29805) {G14,W4,D2,L1,V1,M1} R(29775,176) { coll( skol24,
% 37.82/38.21 skol20, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (29835) {G15,W4,D2,L1,V2,M1} R(29805,208);r(29805) { coll( Y,
% 37.82/38.21 skol24, X ) }.
% 37.82/38.21 parent0: (82382) {G3,W4,D2,L1,V2,M1} { coll( Y, skol24, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82383) {G2,W8,D2,L2,V3,M2} { ! coll( X, skol24, Z ), coll( Y
% 37.82/38.21 , X, Z ) }.
% 37.82/38.21 parent0[0]: (208) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll(
% 37.82/38.21 X, Y, T ), coll( Z, X, T ) }.
% 37.82/38.21 parent1[0]: (29835) {G15,W4,D2,L1,V2,M1} R(29805,208);r(29805) { coll( Y,
% 37.82/38.21 skol24, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := skol24
% 37.82/38.21 Z := Y
% 37.82/38.21 T := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82385) {G3,W4,D2,L1,V3,M1} { coll( Z, X, Y ) }.
% 37.82/38.21 parent0[0]: (82383) {G2,W8,D2,L2,V3,M2} { ! coll( X, skol24, Z ), coll( Y
% 37.82/38.21 , X, Z ) }.
% 37.82/38.21 parent1[0]: (29835) {G15,W4,D2,L1,V2,M1} R(29805,208);r(29805) { coll( Y,
% 37.82/38.21 skol24, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := Y
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (29888) {G16,W4,D2,L1,V3,M1} R(29835,208);r(29835) { coll( Z,
% 37.82/38.21 X, Y ) }.
% 37.82/38.21 parent0: (82385) {G3,W4,D2,L1,V3,M1} { coll( Z, X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82386) {G1,W6,D3,L1,V1,M1} { midp( skol7( skol25, X ), X,
% 37.82/38.21 skol25 ) }.
% 37.82/38.21 parent0[0]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent1[0]: (20079) {G6,W6,D3,L1,V1,M1} S(8165);r(451) { midp( skol7(
% 37.82/38.21 skol25, X ), skol25, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := skol25
% 37.82/38.21 Z := skol7( skol25, X )
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (30287) {G7,W6,D3,L1,V1,M1} R(20079,10) { midp( skol7( skol25
% 37.82/38.21 , X ), X, skol25 ) }.
% 37.82/38.21 parent0: (82386) {G1,W6,D3,L1,V1,M1} { midp( skol7( skol25, X ), X, skol25
% 37.82/38.21 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82387) {G2,W14,D3,L3,V2,M3} { ! coll( X, X, skol25 ), ! coll
% 37.82/38.21 ( skol25, X, skol25 ), midp( skol7( X, Y ), X, Y ) }.
% 37.82/38.21 parent0[0]: (152) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y
% 37.82/38.21 , Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 37.82/38.21 parent1[0]: (30287) {G7,W6,D3,L1,V1,M1} R(20079,10) { midp( skol7( skol25,
% 37.82/38.21 X ), X, skol25 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol7( skol25, X )
% 37.82/38.21 Y := X
% 37.82/38.21 Z := skol25
% 37.82/38.21 T := Y
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82390) {G3,W10,D3,L2,V2,M2} { ! coll( skol25, X, skol25 ),
% 37.82/38.21 midp( skol7( X, Y ), X, Y ) }.
% 37.82/38.21 parent0[0]: (82387) {G2,W14,D3,L3,V2,M3} { ! coll( X, X, skol25 ), ! coll
% 37.82/38.21 ( skol25, X, skol25 ), midp( skol7( X, Y ), X, Y ) }.
% 37.82/38.21 parent1[0]: (29888) {G16,W4,D2,L1,V3,M1} R(29835,208);r(29835) { coll( Z, X
% 37.82/38.21 , Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := skol25
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (30331) {G17,W10,D3,L2,V2,M2} R(30287,152);r(29888) { ! coll(
% 37.82/38.21 skol25, X, skol25 ), midp( skol7( X, Y ), X, Y ) }.
% 37.82/38.21 parent0: (82390) {G3,W10,D3,L2,V2,M2} { ! coll( skol25, X, skol25 ), midp
% 37.82/38.21 ( skol7( X, Y ), X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82392) {G2,W10,D2,L2,V3,M2} { cyclic( Z, Y, X, X ), ! para( X
% 37.82/38.21 , Z, X, Z ) }.
% 37.82/38.21 parent0[0]: (862) {G1,W14,D2,L3,V3,M3} R(42,39) { ! coll( X, X, Y ), cyclic
% 37.82/38.21 ( Z, Y, X, X ), ! para( X, Z, X, Z ) }.
% 37.82/38.21 parent1[0]: (29888) {G16,W4,D2,L1,V3,M1} R(29835,208);r(29835) { coll( Z, X
% 37.82/38.21 , Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (37185) {G17,W10,D2,L2,V3,M2} S(862);r(29888) { cyclic( Z, Y,
% 37.82/38.21 X, X ), ! para( X, Z, X, Z ) }.
% 37.82/38.21 parent0: (82392) {G2,W10,D2,L2,V3,M2} { cyclic( Z, Y, X, X ), ! para( X, Z
% 37.82/38.21 , X, Z ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 1 ==> 1
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82393) {G17,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), X, Y ) }.
% 37.82/38.21 parent0[0]: (30331) {G17,W10,D3,L2,V2,M2} R(30287,152);r(29888) { ! coll(
% 37.82/38.21 skol25, X, skol25 ), midp( skol7( X, Y ), X, Y ) }.
% 37.82/38.21 parent1[0]: (29888) {G16,W4,D2,L1,V3,M1} R(29835,208);r(29835) { coll( Z, X
% 37.82/38.21 , Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := skol25
% 37.82/38.21 Z := skol25
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (40165) {G18,W6,D3,L1,V2,M1} S(30331);r(29888) { midp( skol7(
% 37.82/38.21 X, Y ), X, Y ) }.
% 37.82/38.21 parent0: (82393) {G17,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82394) {G1,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), Y, X ) }.
% 37.82/38.21 parent0[0]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent1[0]: (40165) {G18,W6,D3,L1,V2,M1} S(30331);r(29888) { midp( skol7( X
% 37.82/38.21 , Y ), X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 Z := skol7( X, Y )
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (43124) {G19,W6,D3,L1,V2,M1} R(40165,10) { midp( skol7( X, Y )
% 37.82/38.21 , Y, X ) }.
% 37.82/38.21 parent0: (82394) {G1,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), Y, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82395) {G3,W7,D3,L1,V0,M1} { ! perp( skol23, skol7( skol22,
% 37.82/38.21 skol20 ), skol22, skol20 ) }.
% 37.82/38.21 parent0[0]: (1766) {G2,W9,D2,L2,V1,M2} R(55,576) { ! midp( X, skol22,
% 37.82/38.21 skol20 ), ! perp( skol23, X, skol22, skol20 ) }.
% 37.82/38.21 parent1[0]: (40165) {G18,W6,D3,L1,V2,M1} S(30331);r(29888) { midp( skol7( X
% 37.82/38.21 , Y ), X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol7( skol22, skol20 )
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := skol22
% 37.82/38.21 Y := skol20
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (52359) {G19,W7,D3,L1,V0,M1} R(1766,40165) { ! perp( skol23,
% 37.82/38.21 skol7( skol22, skol20 ), skol22, skol20 ) }.
% 37.82/38.21 parent0: (82395) {G3,W7,D3,L1,V0,M1} { ! perp( skol23, skol7( skol22,
% 37.82/38.21 skol20 ), skol22, skol20 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82396) {G1,W7,D3,L1,V0,M1} { ! perp( skol23, skol7( skol22,
% 37.82/38.21 skol20 ), skol20, skol22 ) }.
% 37.82/38.21 parent0[0]: (52359) {G19,W7,D3,L1,V0,M1} R(1766,40165) { ! perp( skol23,
% 37.82/38.21 skol7( skol22, skol20 ), skol22, skol20 ) }.
% 37.82/38.21 parent1[1]: (6) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( X, Y,
% 37.82/38.21 T, Z ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := skol23
% 37.82/38.21 Y := skol7( skol22, skol20 )
% 37.82/38.21 Z := skol20
% 37.82/38.21 T := skol22
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (52645) {G20,W7,D3,L1,V0,M1} R(52359,6) { ! perp( skol23,
% 37.82/38.21 skol7( skol22, skol20 ), skol20, skol22 ) }.
% 37.82/38.21 parent0: (82396) {G1,W7,D3,L1,V0,M1} { ! perp( skol23, skol7( skol22,
% 37.82/38.21 skol20 ), skol20, skol22 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82397) {G3,W5,D2,L1,V2,M1} { para( Y, X, X, Y ) }.
% 37.82/38.21 parent0[0]: (2114) {G2,W9,D2,L2,V3,M2} F(2102) { ! midp( X, Y, Z ), para( Y
% 37.82/38.21 , Z, Z, Y ) }.
% 37.82/38.21 parent1[0]: (43124) {G19,W6,D3,L1,V2,M1} R(40165,10) { midp( skol7( X, Y )
% 37.82/38.21 , Y, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := skol7( X, Y )
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (77017) {G20,W5,D2,L1,V2,M1} R(2114,43124) { para( X, Y, Y, X
% 37.82/38.21 ) }.
% 37.82/38.21 parent0: (82397) {G3,W5,D2,L1,V2,M1} { para( Y, X, X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82398) {G2,W5,D2,L1,V2,M1} { para( Y, X, Y, X ) }.
% 37.82/38.21 parent0[0]: (244) {G1,W10,D2,L2,V4,M2} R(4,3) { ! para( X, Y, Z, T ), para
% 37.82/38.21 ( Z, T, Y, X ) }.
% 37.82/38.21 parent1[0]: (77017) {G20,W5,D2,L1,V2,M1} R(2114,43124) { para( X, Y, Y, X )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Y
% 37.82/38.21 T := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (77030) {G21,W5,D2,L1,V2,M1} R(77017,244) { para( X, Y, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 parent0: (82398) {G2,W5,D2,L1,V2,M1} { para( Y, X, Y, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Y
% 37.82/38.21 Y := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82399) {G18,W5,D2,L1,V3,M1} { cyclic( X, Y, Z, Z ) }.
% 37.82/38.21 parent0[1]: (37185) {G17,W10,D2,L2,V3,M2} S(862);r(29888) { cyclic( Z, Y, X
% 37.82/38.21 , X ), ! para( X, Z, X, Z ) }.
% 37.82/38.21 parent1[0]: (77030) {G21,W5,D2,L1,V2,M1} R(77017,244) { para( X, Y, X, Y )
% 37.82/38.21 }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (80676) {G22,W5,D2,L1,V3,M1} S(37185);r(77030) { cyclic( Z, Y
% 37.82/38.21 , X, X ) }.
% 37.82/38.21 parent0: (82399) {G18,W5,D2,L1,V3,M1} { cyclic( X, Y, Z, Z ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82400) {G2,W5,D2,L1,V3,M1} { cyclic( Y, Z, X, Z ) }.
% 37.82/38.21 parent0[0]: (404) {G1,W10,D2,L2,V4,M2} R(15,14) { ! cyclic( X, Y, Z, T ),
% 37.82/38.21 cyclic( Y, Z, X, T ) }.
% 37.82/38.21 parent1[0]: (80676) {G22,W5,D2,L1,V3,M1} S(37185);r(77030) { cyclic( Z, Y,
% 37.82/38.21 X, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (80782) {G23,W5,D2,L1,V3,M1} R(80676,404) { cyclic( X, Y, Z, Y
% 37.82/38.21 ) }.
% 37.82/38.21 parent0: (82400) {G2,W5,D2,L1,V3,M1} { cyclic( Y, Z, X, Z ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := X
% 37.82/38.21 Z := Y
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82401) {G2,W5,D2,L1,V3,M1} { cyclic( X, Y, Z, X ) }.
% 37.82/38.21 parent0[1]: (403) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), !
% 37.82/38.21 cyclic( Y, Z, X, T ) }.
% 37.82/38.21 parent1[0]: (80676) {G22,W5,D2,L1,V3,M1} S(37185);r(77030) { cyclic( Z, Y,
% 37.82/38.21 X, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := X
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (80783) {G23,W5,D2,L1,V3,M1} R(80676,403) { cyclic( X, Y, Z, X
% 37.82/38.21 ) }.
% 37.82/38.21 parent0: (82401) {G2,W5,D2,L1,V3,M1} { cyclic( X, Y, Z, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82403) {G3,W10,D2,L2,V3,M2} { ! cyclic( X, Y, Z, X ), cong( X
% 37.82/38.21 , Y, X, Y ) }.
% 37.82/38.21 parent0[1]: (1059) {G2,W15,D2,L3,V3,M3} F(1026) { ! cyclic( X, Y, Z, X ), !
% 37.82/38.21 cyclic( X, Y, Z, Y ), cong( X, Y, X, Y ) }.
% 37.82/38.21 parent1[0]: (80782) {G23,W5,D2,L1,V3,M1} R(80676,404) { cyclic( X, Y, Z, Y
% 37.82/38.21 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82405) {G4,W5,D2,L1,V2,M1} { cong( X, Y, X, Y ) }.
% 37.82/38.21 parent0[0]: (82403) {G3,W10,D2,L2,V3,M2} { ! cyclic( X, Y, Z, X ), cong( X
% 37.82/38.21 , Y, X, Y ) }.
% 37.82/38.21 parent1[0]: (80783) {G23,W5,D2,L1,V3,M1} R(80676,403) { cyclic( X, Y, Z, X
% 37.82/38.21 ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (80798) {G24,W5,D2,L1,V2,M1} R(80782,1059);r(80783) { cong( X
% 37.82/38.21 , Y, X, Y ) }.
% 37.82/38.21 parent0: (82405) {G4,W5,D2,L1,V2,M1} { cong( X, Y, X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82406) {G2,W10,D2,L2,V3,M2} { ! cong( X, Z, X, Z ), perp( Y,
% 37.82/38.21 Z, X, X ) }.
% 37.82/38.21 parent0[0]: (1864) {G1,W15,D2,L3,V4,M3} R(56,7) { ! cong( X, Y, Z, Y ), !
% 37.82/38.21 cong( X, T, Z, T ), perp( Y, T, X, Z ) }.
% 37.82/38.21 parent1[0]: (80798) {G24,W5,D2,L1,V2,M1} R(80782,1059);r(80783) { cong( X,
% 37.82/38.21 Y, X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 T := Z
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82408) {G3,W5,D2,L1,V3,M1} { perp( Z, Y, X, X ) }.
% 37.82/38.21 parent0[0]: (82406) {G2,W10,D2,L2,V3,M2} { ! cong( X, Z, X, Z ), perp( Y,
% 37.82/38.21 Z, X, X ) }.
% 37.82/38.21 parent1[0]: (80798) {G24,W5,D2,L1,V2,M1} R(80782,1059);r(80783) { cong( X,
% 37.82/38.21 Y, X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := Y
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (81565) {G25,W5,D2,L1,V3,M1} R(80798,1864);r(80798) { perp( Z
% 37.82/38.21 , Y, X, X ) }.
% 37.82/38.21 parent0: (82408) {G3,W5,D2,L1,V3,M1} { perp( Z, Y, X, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82409) {G3,W10,D2,L2,V4,M2} { ! cong( X, Y, X, Y ), para( Z,
% 37.82/38.21 T, Y, Y ) }.
% 37.82/38.21 parent0[1]: (1866) {G2,W15,D2,L3,V5,M3} F(1863) { ! cong( X, Y, Z, Y ), !
% 37.82/38.21 perp( T, U, X, Z ), para( T, U, Y, Y ) }.
% 37.82/38.21 parent1[0]: (81565) {G25,W5,D2,L1,V3,M1} R(80798,1864);r(80798) { perp( Z,
% 37.82/38.21 Y, X, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := X
% 37.82/38.21 T := Z
% 37.82/38.21 U := T
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := T
% 37.82/38.21 Z := Z
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82410) {G4,W5,D2,L1,V3,M1} { para( Z, T, Y, Y ) }.
% 37.82/38.21 parent0[0]: (82409) {G3,W10,D2,L2,V4,M2} { ! cong( X, Y, X, Y ), para( Z,
% 37.82/38.21 T, Y, Y ) }.
% 37.82/38.21 parent1[0]: (80798) {G24,W5,D2,L1,V2,M1} R(80782,1059);r(80783) { cong( X,
% 37.82/38.21 Y, X, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (81670) {G26,W5,D2,L1,V3,M1} R(81565,1866);r(80798) { para( Z
% 37.82/38.21 , T, Y, Y ) }.
% 37.82/38.21 parent0: (82410) {G4,W5,D2,L1,V3,M1} { para( Z, T, Y, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := U
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82411) {G2,W10,D2,L2,V5,M2} { ! para( X, Y, Z, Z ), perp( X,
% 37.82/38.21 Y, T, U ) }.
% 37.82/38.21 parent0[2]: (320) {G1,W15,D2,L3,V6,M3} R(9,7) { ! para( X, Y, Z, T ), perp
% 37.82/38.21 ( X, Y, U, W ), ! perp( U, W, Z, T ) }.
% 37.82/38.21 parent1[0]: (81565) {G25,W5,D2,L1,V3,M1} R(80798,1864);r(80798) { perp( Z,
% 37.82/38.21 Y, X, X ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := Z
% 37.82/38.21 U := T
% 37.82/38.21 W := U
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := Z
% 37.82/38.21 Y := U
% 37.82/38.21 Z := T
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82412) {G3,W5,D2,L1,V4,M1} { perp( X, Y, T, U ) }.
% 37.82/38.21 parent0[0]: (82411) {G2,W10,D2,L2,V5,M2} { ! para( X, Y, Z, Z ), perp( X,
% 37.82/38.21 Y, T, U ) }.
% 37.82/38.21 parent1[0]: (81670) {G26,W5,D2,L1,V3,M1} R(81565,1866);r(80798) { para( Z,
% 37.82/38.21 T, Y, Y ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := Z
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := W
% 37.82/38.21 Y := Z
% 37.82/38.21 Z := X
% 37.82/38.21 T := Y
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (81673) {G27,W5,D2,L1,V4,M1} R(81565,320);r(81670) { perp( X,
% 37.82/38.21 Y, T, U ) }.
% 37.82/38.21 parent0: (82412) {G3,W5,D2,L1,V4,M1} { perp( X, Y, T, U ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 X := X
% 37.82/38.21 Y := Y
% 37.82/38.21 Z := W
% 37.82/38.21 T := T
% 37.82/38.21 U := U
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 0 ==> 0
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 resolution: (82413) {G21,W0,D0,L0,V0,M0} { }.
% 37.82/38.21 parent0[0]: (52645) {G20,W7,D3,L1,V0,M1} R(52359,6) { ! perp( skol23, skol7
% 37.82/38.21 ( skol22, skol20 ), skol20, skol22 ) }.
% 37.82/38.21 parent1[0]: (81673) {G27,W5,D2,L1,V4,M1} R(81565,320);r(81670) { perp( X, Y
% 37.82/38.21 , T, U ) }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 substitution1:
% 37.82/38.21 X := skol23
% 37.82/38.21 Y := skol7( skol22, skol20 )
% 37.82/38.21 Z := X
% 37.82/38.21 T := skol20
% 37.82/38.21 U := skol22
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 subsumption: (81685) {G28,W0,D0,L0,V0,M0} R(81673,52645) { }.
% 37.82/38.21 parent0: (82413) {G21,W0,D0,L0,V0,M0} { }.
% 37.82/38.21 substitution0:
% 37.82/38.21 end
% 37.82/38.21 permutation0:
% 37.82/38.21 end
% 37.82/38.21
% 37.82/38.21 Proof check complete!
% 37.82/38.21
% 37.82/38.21 Memory use:
% 37.82/38.21
% 37.82/38.21 space for terms: 1142163
% 37.82/38.21 space for clauses: 3886586
% 37.82/38.21
% 37.82/38.21
% 37.82/38.21 clauses generated: 493143
% 37.82/38.21 clauses kept: 81686
% 37.82/38.21 clauses selected: 4032
% 37.82/38.21 clauses deleted: 28456
% 37.82/38.21 clauses inuse deleted: 2288
% 37.82/38.21
% 37.82/38.21 subsentry: 13136562
% 37.82/38.21 literals s-matched: 7849565
% 37.82/38.21 literals matched: 4118991
% 37.82/38.21 full subsumption: 2202473
% 37.82/38.21
% 37.82/38.21 checksum: -305575917
% 37.82/38.21
% 37.82/38.21
% 37.82/38.21 Bliksem ended
%------------------------------------------------------------------------------