%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GEO624+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Sat Jul 16 02:55:11 EDT 2022
% Result : Theorem 55.54s 55.94s
% Output : Refutation 55.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : GEO624+1 : TPTP v8.1.0. Released v7.5.0.
% 0.12/0.14 % Command : bliksem %s
% 0.14/0.35 % Computer : n020.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % DateTime : Fri Jun 17 22:46:34 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.78/1.18 *** allocated 10000 integers for termspace/termends
% 0.78/1.18 *** allocated 10000 integers for clauses
% 0.78/1.18 *** allocated 10000 integers for justifications
% 0.78/1.18 Bliksem 1.12
% 0.78/1.18
% 0.78/1.18
% 0.78/1.18 Automatic Strategy Selection
% 0.78/1.18
% 0.78/1.18 *** allocated 15000 integers for termspace/termends
% 0.78/1.18
% 0.78/1.18 Clauses:
% 0.78/1.18
% 0.78/1.18 { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 0.78/1.18 { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 0.78/1.18 { ! coll( X, T, Y ), ! coll( X, T, Z ), coll( Y, Z, X ) }.
% 0.78/1.18 { ! para( X, Y, Z, T ), para( X, Y, T, Z ) }.
% 0.78/1.18 { ! para( X, Y, Z, T ), para( Z, T, X, Y ) }.
% 0.78/1.18 { ! para( X, Y, U, W ), ! para( U, W, Z, T ), para( X, Y, Z, T ) }.
% 0.78/1.18 { ! perp( X, Y, Z, T ), perp( X, Y, T, Z ) }.
% 0.78/1.18 { ! perp( X, Y, Z, T ), perp( Z, T, X, Y ) }.
% 0.78/1.18 { ! perp( X, Y, U, W ), ! perp( U, W, Z, T ), para( X, Y, Z, T ) }.
% 0.78/1.18 { ! para( X, Y, U, W ), ! perp( U, W, Z, T ), perp( X, Y, Z, T ) }.
% 0.78/1.18 { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 0.78/1.18 { ! cong( T, X, T, Y ), ! cong( T, X, T, Z ), circle( T, X, Y, Z ) }.
% 0.78/1.18 { ! cong( U, X, U, Y ), ! cong( U, X, U, Z ), ! cong( U, X, U, T ), cyclic
% 0.78/1.18 ( X, Y, Z, T ) }.
% 0.78/1.18 { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z ) }.
% 0.78/1.18 { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T ) }.
% 0.78/1.18 { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T ) }.
% 0.78/1.18 { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 0.78/1.18 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( Y, X, Z, T, U, W, V0, V1
% 0.78/1.18 ) }.
% 0.78/1.18 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( Z, T, X, Y, V0, V1, U, W
% 0.78/1.18 ) }.
% 0.78/1.18 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( U, W, V0, V1, X, Y, Z, T
% 0.78/1.18 ) }.
% 0.78/1.18 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( X, Y, U, W, Z, T, V0, V1
% 0.78/1.18 ) }.
% 0.78/1.18 { ! eqangle( X, Y, Z, T, V2, V3, V4, V5 ), ! eqangle( V2, V3, V4, V5, U, W
% 0.78/1.18 , V0, V1 ), eqangle( X, Y, Z, T, U, W, V0, V1 ) }.
% 0.78/1.18 { ! cong( X, Y, Z, T ), cong( X, Y, T, Z ) }.
% 0.78/1.18 { ! cong( X, Y, Z, T ), cong( Z, T, X, Y ) }.
% 0.78/1.18 { ! cong( X, Y, U, W ), ! cong( U, W, Z, T ), cong( X, Y, Z, T ) }.
% 0.78/1.18 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( Y, X, Z, T, U, W, V0, V1
% 0.78/1.18 ) }.
% 0.78/1.18 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( Z, T, X, Y, V0, V1, U, W
% 0.78/1.18 ) }.
% 0.78/1.18 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( U, W, V0, V1, X, Y, Z, T
% 0.78/1.18 ) }.
% 0.78/1.18 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( X, Y, U, W, Z, T, V0, V1
% 0.78/1.18 ) }.
% 0.78/1.18 { ! eqratio( X, Y, Z, T, V2, V3, V4, V5 ), ! eqratio( V2, V3, V4, V5, U, W
% 0.78/1.18 , V0, V1 ), eqratio( X, Y, Z, T, U, W, V0, V1 ) }.
% 0.78/1.18 { ! simtri( X, Z, Y, T, W, U ), simtri( X, Y, Z, T, U, W ) }.
% 0.78/1.18 { ! simtri( Y, X, Z, U, T, W ), simtri( X, Y, Z, T, U, W ) }.
% 0.78/1.18 { ! simtri( T, U, W, X, Y, Z ), simtri( X, Y, Z, T, U, W ) }.
% 0.78/1.18 { ! simtri( X, Y, Z, V0, V1, V2 ), ! simtri( V0, V1, V2, T, U, W ), simtri
% 0.78/1.18 ( X, Y, Z, T, U, W ) }.
% 0.78/1.18 { ! contri( X, Z, Y, T, W, U ), contri( X, Y, Z, T, U, W ) }.
% 0.78/1.18 { ! contri( Y, X, Z, U, T, W ), contri( X, Y, Z, T, U, W ) }.
% 0.78/1.18 { ! contri( T, U, W, X, Y, Z ), contri( X, Y, Z, T, U, W ) }.
% 0.78/1.18 { ! contri( X, Y, Z, V0, V1, V2 ), ! contri( V0, V1, V2, T, U, W ), contri
% 0.78/1.18 ( X, Y, Z, T, U, W ) }.
% 0.78/1.18 { ! eqangle( X, Y, U, W, Z, T, U, W ), para( X, Y, Z, T ) }.
% 0.78/1.18 { ! para( X, Y, Z, T ), eqangle( X, Y, U, W, Z, T, U, W ) }.
% 0.78/1.18 { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z, Y, T, X, T, Y ) }.
% 0.78/1.18 { ! eqangle( Z, X, Z, Y, T, X, T, Y ), coll( Z, T, X ), cyclic( X, Y, Z, T
% 0.78/1.19 ) }.
% 0.78/1.19 { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll( Z, T, Y ), cyclic( X, Y, Z,
% 0.78/1.19 T ) }.
% 0.78/1.19 { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U, T ), ! cyclic( X, Y, U, W ), !
% 0.78/1.19 eqangle( U, X, U, Y, W, Z, W, T ), cong( X, Y, Z, T ) }.
% 0.78/1.19 { ! midp( Z, U, X ), ! midp( T, U, Y ), para( Z, T, X, Y ) }.
% 0.78/1.19 { ! midp( U, X, T ), ! para( U, Z, T, Y ), ! coll( Z, X, Y ), midp( Z, X, Y
% 0.78/1.19 ) }.
% 0.78/1.19 { ! cong( Z, X, Z, Y ), eqangle( Z, X, X, Y, X, Y, Z, Y ) }.
% 0.78/1.19 { ! eqangle( Z, X, X, Y, X, Y, Z, Y ), coll( Z, X, Y ), cong( Z, X, Z, Y )
% 0.78/1.19 }.
% 0.78/1.19 { ! circle( U, X, Y, Z ), ! perp( U, X, X, T ), eqangle( X, T, X, Y, Z, X,
% 0.78/1.19 Z, Y ) }.
% 0.78/1.19 { ! circle( Y, X, T, U ), ! eqangle( X, Z, X, T, U, X, U, T ), perp( Y, X,
% 0.78/1.19 X, Z ) }.
% 0.78/1.19 { ! circle( T, X, Y, Z ), ! midp( U, Y, Z ), eqangle( X, Y, X, Z, T, Y, T,
% 0.78/1.19 U ) }.
% 0.78/1.19 { ! circle( U, T, X, Y ), ! coll( Z, X, Y ), ! eqangle( T, X, T, Y, U, X, U
% 0.78/1.19 , Z ), midp( Z, X, Y ) }.
% 0.78/1.19 { ! perp( X, Y, Y, T ), ! midp( Z, X, T ), cong( X, Z, Y, Z ) }.
% 0.78/1.19 { ! circle( T, X, Y, Z ), ! coll( T, X, Z ), perp( X, Y, Y, Z ) }.
% 0.78/1.19 { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T ), eqangle( X, T, Z, T, Z, T,
% 0.78/1.19 Z, Y ) }.
% 0.78/1.19 { ! midp( T, X, Y ), ! perp( Z, T, X, Y ), cong( Z, X, Z, Y ) }.
% 0.78/1.19 { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T ), perp( X, Y, Z, T ) }.
% 0.78/1.19 { ! cong( X, Y, T, Y ), ! cong( X, Z, T, Z ), ! cyclic( X, T, Y, Z ), perp
% 0.78/1.19 ( Y, X, X, Z ) }.
% 0.78/1.19 { ! eqangle( X, Y, Y, Z, T, U, U, W ), ! eqangle( X, Z, Y, Z, T, W, U, W )
% 0.78/1.19 , coll( X, Y, Z ), simtri( X, Y, Z, T, U, W ) }.
% 0.78/1.19 { ! simtri( X, Y, Z, T, U, W ), eqratio( X, Y, X, Z, T, U, T, W ) }.
% 0.78/1.19 { ! simtri( X, Y, Z, T, U, W ), eqangle( X, Y, Y, Z, T, U, U, W ) }.
% 0.78/1.19 { ! simtri( X, Y, Z, T, U, W ), ! cong( X, Y, T, U ), contri( X, Y, Z, T, U
% 0.78/1.19 , W ) }.
% 0.78/1.19 { ! contri( X, Y, U, Z, T, W ), cong( X, Y, Z, T ) }.
% 0.78/1.19 { ! midp( U, X, Y ), ! midp( U, Z, T ), para( X, Z, Y, T ) }.
% 0.78/1.19 { ! midp( Z, T, U ), ! para( T, X, U, Y ), ! para( T, Y, U, X ), midp( Z, X
% 0.78/1.19 , Y ) }.
% 0.78/1.19 { ! para( X, Y, Z, T ), ! coll( U, X, Z ), ! coll( U, Y, T ), eqratio( U, X
% 0.78/1.19 , X, Z, U, Y, Y, T ) }.
% 0.78/1.19 { ! para( X, Y, X, Z ), coll( X, Y, Z ) }.
% 0.78/1.19 { ! cong( X, Y, X, Z ), ! coll( X, Y, Z ), midp( X, Y, Z ) }.
% 0.78/1.19 { ! midp( X, Y, Z ), cong( X, Y, X, Z ) }.
% 0.78/1.19 { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 0.78/1.19 { ! midp( U, X, Y ), ! midp( W, Z, T ), eqratio( U, X, X, Y, W, Z, Z, T ) }
% 0.78/1.19 .
% 0.78/1.19 { ! eqangle( X, Y, Z, T, Z, T, X, Y ), para( X, Y, Z, T ), perp( X, Y, Z, T
% 0.78/1.19 ) }.
% 0.78/1.19 { ! eqangle( X, Y, Z, T, Z, T, X, Y ), perp( X, Y, Z, T ), para( X, Y, Z, T
% 0.78/1.19 ) }.
% 0.78/1.19 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), ! para( U, W, V0, V1 ), para( X, Y
% 0.78/1.19 , Z, T ) }.
% 0.78/1.19 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), ! perp( U, W, V0, V1 ), perp( X, Y
% 0.78/1.19 , Z, T ) }.
% 0.78/1.19 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), ! cong( U, W, V0, V1 ), cong( X, Y
% 0.78/1.19 , Z, T ) }.
% 0.78/1.19 { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z, Y, Z, X, Z ), coll( skol1( U
% 0.78/1.19 , W, Z, T ), Z, T ) }.
% 0.78/1.19 { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z, Y, Z, X, Z ), coll( skol1( X
% 0.78/1.19 , Y, Z, T ), X, Y ) }.
% 0.78/1.19 { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( skol2( U
% 0.78/1.19 , W, Z, T ), Z, T ) }.
% 0.78/1.19 { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( Y, X,
% 0.78/1.19 skol2( X, Y, Z, T ) ) }.
% 0.78/1.19 { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( skol3( U
% 0.78/1.19 , W, Z, T ), Z, T ) }.
% 0.78/1.19 { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( Y, X,
% 0.78/1.19 skol3( X, Y, Z, T ) ) }.
% 0.78/1.19 { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y ), coll( skol4( U, W, Z, T ), Z
% 0.78/1.19 , T ) }.
% 0.78/1.19 { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y ), coll( Y, X, skol4( X, Y, Z, T
% 0.78/1.19 ) ) }.
% 0.78/1.19 { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll( X, Y, Z ), cyclic( T, Y, Z,
% 0.78/1.19 skol5( W, Y, Z, T ) ) }.
% 0.78/1.19 { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll( X, Y, Z ), eqangle( X, Z, Y, Z
% 0.78/1.19 , X, skol5( X, Y, Z, T ), Y, skol5( X, Y, Z, T ) ) }.
% 0.78/1.19 { ! midp( U, X, Y ), ! midp( W, Z, T ), midp( skol6( X, V0, V1, T, V2, V3 )
% 0.78/1.19 , X, T ) }.
% 0.78/1.19 { ! midp( U, X, Y ), ! midp( W, Z, T ), para( skol6( X, V0, Z, T, V1, W ),
% 0.78/1.19 W, X, Z ) }.
% 0.78/1.19 { ! midp( U, X, Y ), ! midp( W, Z, T ), para( skol6( X, Y, Z, T, U, W ), U
% 0.78/1.19 , Y, T ) }.
% 0.78/1.19 { ! midp( Z, X, Y ), ! midp( W, T, U ), ! coll( T, X, Y ), ! coll( U, X, Y
% 0.78/1.19 ), midp( skol7( X, V0 ), X, V0 ) }.
% 0.78/1.19 { ! midp( T, X, U ), ! para( X, W, Z, T ), ! para( X, W, U, Y ), ! coll( W
% 0.78/1.19 , Y, Z ), coll( skol8( V0, V1, Z, T ), T, Z ) }.
% 0.78/1.19 { ! midp( T, X, U ), ! para( X, W, Z, T ), ! para( X, W, U, Y ), ! coll( W
% 0.78/1.19 , Y, Z ), coll( skol8( X, Y, Z, T ), X, Y ) }.
% 0.78/1.19 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), cong( T, Z, T, skol9( W, V0,
% 0.78/1.19 Z, T ) ) }.
% 0.78/1.19 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), cong( Y, Z, Y, skol9( W, Y, Z
% 0.78/1.19 , T ) ) }.
% 0.78/1.19 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), para( skol9( X, Y, Z, T ), Z
% 0.78/1.19 , X, Y ) }.
% 0.78/1.19 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), coll( skol10( U, Y, Z ), Z, Y
% 0.78/1.19 ) }.
% 0.78/1.19 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), perp( X, skol10( X, Y, Z ), Z
% 0.78/1.19 , Y ) }.
% 0.78/1.19 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), alpha1( X, Y, Z ) }.
% 0.78/1.19 { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z ), Z, X ) }.
% 0.78/1.19 { ! alpha1( X, Y, Z ), perp( Y, skol11( X, Y, Z ), Z, X ) }.
% 0.78/1.19 { ! coll( T, Z, X ), ! perp( Y, T, Z, X ), alpha1( X, Y, Z ) }.
% 0.78/1.19 { ! circle( Y, X, Z, T ), perp( skol12( X, Y ), X, X, Y ) }.
% 3.32/3.68 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 3.32/3.68 , alpha2( X, Z, U, skol13( X, V0, Z, V1, U ) ) }.
% 3.32/3.68 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 3.32/3.68 , coll( skol21( V0, Y, T, V1 ), Y, T ) }.
% 3.32/3.68 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 3.32/3.68 , cong( skol21( X, Y, T, U ), U, U, X ) }.
% 3.32/3.68 { ! alpha2( X, Y, Z, T ), coll( T, X, Y ) }.
% 3.32/3.68 { ! alpha2( X, Y, Z, T ), cong( T, Z, Z, X ) }.
% 3.32/3.68 { ! coll( T, X, Y ), ! cong( T, Z, Z, X ), alpha2( X, Y, Z, T ) }.
% 3.32/3.68 { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T ), ! midp( U, X, Y ), circle(
% 3.32/3.68 skol14( X, Y, Z ), X, Y, Z ) }.
% 3.32/3.68 { ! perp( X, Z, Z, Y ), ! cyclic( X, Y, Z, T ), circle( skol15( X, Y, Z ),
% 3.32/3.68 X, Y, Z ) }.
% 3.32/3.68 { ! perp( X, U, U, T ), ! coll( T, Y, Z ), coll( skol16( W, Y, Z ), Y, Z )
% 3.32/3.68 }.
% 3.32/3.68 { ! perp( X, U, U, T ), ! coll( T, Y, Z ), perp( skol16( X, Y, Z ), X, Y, Z
% 3.32/3.68 ) }.
% 3.32/3.68 { ! perp( X, Z, X, Y ), ! perp( Y, X, Y, T ), ! midp( U, Z, T ), midp(
% 3.32/3.68 skol17( X, Y ), X, Y ) }.
% 3.32/3.68 { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z ), coll( X, Y, skol18( X, Y ) )
% 3.32/3.68 }.
% 3.32/3.68 { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z ), cong( Y, X, Y, skol18( X, Y )
% 3.32/3.68 ) }.
% 3.32/3.68 { ! para( U, W, X, Y ), ! coll( Z, U, X ), ! coll( Z, W, Y ), ! coll( T, U
% 3.32/3.68 , W ), coll( Z, T, skol19( V0, V1, Z, T ) ) }.
% 3.32/3.68 { ! para( U, W, X, Y ), ! coll( Z, U, X ), ! coll( Z, W, Y ), ! coll( T, U
% 3.32/3.68 , W ), coll( skol19( X, Y, Z, T ), X, Y ) }.
% 3.32/3.68 { perp( skol27, skol26, skol20, skol25 ) }.
% 3.32/3.68 { coll( skol27, skol20, skol25 ) }.
% 3.32/3.68 { perp( skol29, skol26, skol20, skol28 ) }.
% 3.32/3.68 { coll( skol29, skol20, skol28 ) }.
% 3.32/3.68 { coll( skol26, skol27, skol22 ) }.
% 3.32/3.68 { cong( skol26, skol27, skol26, skol22 ) }.
% 3.32/3.68 { coll( skol26, skol29, skol23 ) }.
% 3.32/3.68 { cong( skol26, skol29, skol26, skol23 ) }.
% 3.32/3.68 { coll( skol30, skol26, skol27 ) }.
% 3.32/3.68 { coll( skol30, skol20, skol28 ) }.
% 3.32/3.68 { coll( skol24, skol20, skol25 ) }.
% 3.32/3.68 { coll( skol24, skol26, skol29 ) }.
% 3.32/3.68 { ! cyclic( skol20, skol22, skol23, skol24 ) }.
% 3.32/3.68
% 3.32/3.68 percentage equality = 0.008646, percentage horn = 0.930233
% 3.32/3.68 This is a problem with some equality
% 3.32/3.68
% 3.32/3.68
% 3.32/3.68
% 3.32/3.68 Options Used:
% 3.32/3.68
% 3.32/3.68 useres = 1
% 3.32/3.68 useparamod = 1
% 3.32/3.68 useeqrefl = 1
% 3.32/3.68 useeqfact = 1
% 3.32/3.68 usefactor = 1
% 3.32/3.68 usesimpsplitting = 0
% 3.32/3.68 usesimpdemod = 5
% 3.32/3.68 usesimpres = 3
% 3.32/3.68
% 3.32/3.68 resimpinuse = 1000
% 3.32/3.68 resimpclauses = 20000
% 3.32/3.68 substype = eqrewr
% 3.32/3.68 backwardsubs = 1
% 3.32/3.68 selectoldest = 5
% 3.32/3.68
% 3.32/3.68 litorderings [0] = split
% 3.32/3.68 litorderings [1] = extend the termordering, first sorting on arguments
% 3.32/3.68
% 3.32/3.68 termordering = kbo
% 3.32/3.68
% 3.32/3.68 litapriori = 0
% 3.32/3.68 termapriori = 1
% 3.32/3.68 litaposteriori = 0
% 3.32/3.68 termaposteriori = 0
% 3.32/3.68 demodaposteriori = 0
% 3.32/3.68 ordereqreflfact = 0
% 3.32/3.68
% 3.32/3.68 litselect = negord
% 3.32/3.68
% 3.32/3.68 maxweight = 15
% 3.32/3.68 maxdepth = 30000
% 3.32/3.68 maxlength = 115
% 3.32/3.68 maxnrvars = 195
% 3.32/3.68 excuselevel = 1
% 3.32/3.68 increasemaxweight = 1
% 3.32/3.68
% 3.32/3.68 maxselected = 10000000
% 3.32/3.68 maxnrclauses = 10000000
% 3.32/3.68
% 3.32/3.68 showgenerated = 0
% 3.32/3.68 showkept = 0
% 3.32/3.68 showselected = 0
% 3.32/3.68 showdeleted = 0
% 3.32/3.68 showresimp = 1
% 3.32/3.68 showstatus = 2000
% 3.32/3.68
% 3.32/3.68 prologoutput = 0
% 3.32/3.68 nrgoals = 5000000
% 3.32/3.68 totalproof = 1
% 3.32/3.68
% 3.32/3.68 Symbols occurring in the translation:
% 3.32/3.68
% 3.32/3.68 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 3.32/3.68 . [1, 2] (w:1, o:42, a:1, s:1, b:0),
% 3.32/3.68 ! [4, 1] (w:0, o:37, a:1, s:1, b:0),
% 3.32/3.68 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.32/3.68 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.32/3.68 coll [38, 3] (w:1, o:70, a:1, s:1, b:0),
% 3.32/3.68 para [40, 4] (w:1, o:78, a:1, s:1, b:0),
% 3.32/3.68 perp [43, 4] (w:1, o:79, a:1, s:1, b:0),
% 3.32/3.68 midp [45, 3] (w:1, o:71, a:1, s:1, b:0),
% 3.32/3.68 cong [47, 4] (w:1, o:80, a:1, s:1, b:0),
% 3.32/3.68 circle [48, 4] (w:1, o:81, a:1, s:1, b:0),
% 3.32/3.68 cyclic [49, 4] (w:1, o:82, a:1, s:1, b:0),
% 3.32/3.68 eqangle [54, 8] (w:1, o:97, a:1, s:1, b:0),
% 3.32/3.68 eqratio [57, 8] (w:1, o:98, a:1, s:1, b:0),
% 3.32/3.68 simtri [59, 6] (w:1, o:94, a:1, s:1, b:0),
% 3.32/3.68 contri [60, 6] (w:1, o:95, a:1, s:1, b:0),
% 3.32/3.68 alpha1 [67, 3] (w:1, o:72, a:1, s:1, b:1),
% 3.32/3.68 alpha2 [68, 4] (w:1, o:83, a:1, s:1, b:1),
% 3.32/3.68 skol1 [69, 4] (w:1, o:84, a:1, s:1, b:1),
% 3.32/3.68 skol2 [70, 4] (w:1, o:86, a:1, s:1, b:1),
% 3.32/3.68 skol3 [71, 4] (w:1, o:88, a:1, s:1, b:1),
% 3.32/3.68 skol4 [72, 4] (w:1, o:89, a:1, s:1, b:1),
% 21.96/22.33 skol5 [73, 4] (w:1, o:90, a:1, s:1, b:1),
% 21.96/22.33 skol6 [74, 6] (w:1, o:96, a:1, s:1, b:1),
% 21.96/22.33 skol7 [75, 2] (w:1, o:66, a:1, s:1, b:1),
% 21.96/22.33 skol8 [76, 4] (w:1, o:91, a:1, s:1, b:1),
% 21.96/22.33 skol9 [77, 4] (w:1, o:92, a:1, s:1, b:1),
% 21.96/22.33 skol10 [78, 3] (w:1, o:73, a:1, s:1, b:1),
% 21.96/22.33 skol11 [79, 3] (w:1, o:74, a:1, s:1, b:1),
% 21.96/22.33 skol12 [80, 2] (w:1, o:67, a:1, s:1, b:1),
% 21.96/22.33 skol13 [81, 5] (w:1, o:93, a:1, s:1, b:1),
% 21.96/22.33 skol14 [82, 3] (w:1, o:75, a:1, s:1, b:1),
% 21.96/22.33 skol15 [83, 3] (w:1, o:76, a:1, s:1, b:1),
% 21.96/22.33 skol16 [84, 3] (w:1, o:77, a:1, s:1, b:1),
% 21.96/22.33 skol17 [85, 2] (w:1, o:68, a:1, s:1, b:1),
% 21.96/22.33 skol18 [86, 2] (w:1, o:69, a:1, s:1, b:1),
% 21.96/22.33 skol19 [87, 4] (w:1, o:85, a:1, s:1, b:1),
% 21.96/22.33 skol20 [88, 0] (w:1, o:27, a:1, s:1, b:1),
% 21.96/22.33 skol21 [89, 4] (w:1, o:87, a:1, s:1, b:1),
% 21.96/22.33 skol22 [90, 0] (w:1, o:28, a:1, s:1, b:1),
% 21.96/22.33 skol23 [91, 0] (w:1, o:29, a:1, s:1, b:1),
% 21.96/22.33 skol24 [92, 0] (w:1, o:30, a:1, s:1, b:1),
% 21.96/22.33 skol25 [93, 0] (w:1, o:31, a:1, s:1, b:1),
% 21.96/22.33 skol26 [94, 0] (w:1, o:32, a:1, s:1, b:1),
% 21.96/22.33 skol27 [95, 0] (w:1, o:33, a:1, s:1, b:1),
% 21.96/22.33 skol28 [96, 0] (w:1, o:34, a:1, s:1, b:1),
% 21.96/22.33 skol29 [97, 0] (w:1, o:35, a:1, s:1, b:1),
% 21.96/22.33 skol30 [98, 0] (w:1, o:36, a:1, s:1, b:1).
% 21.96/22.33
% 21.96/22.33
% 21.96/22.33 Starting Search:
% 21.96/22.33
% 21.96/22.33 *** allocated 15000 integers for clauses
% 21.96/22.33 *** allocated 22500 integers for clauses
% 21.96/22.33 *** allocated 33750 integers for clauses
% 21.96/22.33 *** allocated 50625 integers for clauses
% 21.96/22.33 *** allocated 22500 integers for termspace/termends
% 21.96/22.33 *** allocated 75937 integers for clauses
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 *** allocated 33750 integers for termspace/termends
% 21.96/22.33 *** allocated 113905 integers for clauses
% 21.96/22.33 *** allocated 50625 integers for termspace/termends
% 21.96/22.33
% 21.96/22.33 Intermediate Status:
% 21.96/22.33 Generated: 4530
% 21.96/22.33 Kept: 2005
% 21.96/22.33 Inuse: 301
% 21.96/22.33 Deleted: 0
% 21.96/22.33 Deletedinuse: 0
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 *** allocated 170857 integers for clauses
% 21.96/22.33 *** allocated 75937 integers for termspace/termends
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 *** allocated 256285 integers for clauses
% 21.96/22.33 *** allocated 113905 integers for termspace/termends
% 21.96/22.33
% 21.96/22.33 Intermediate Status:
% 21.96/22.33 Generated: 17222
% 21.96/22.33 Kept: 4005
% 21.96/22.33 Inuse: 452
% 21.96/22.33 Deleted: 1
% 21.96/22.33 Deletedinuse: 1
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 *** allocated 384427 integers for clauses
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 *** allocated 170857 integers for termspace/termends
% 21.96/22.33
% 21.96/22.33 Intermediate Status:
% 21.96/22.33 Generated: 32268
% 21.96/22.33 Kept: 6156
% 21.96/22.33 Inuse: 531
% 21.96/22.33 Deleted: 1
% 21.96/22.33 Deletedinuse: 1
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 *** allocated 576640 integers for clauses
% 21.96/22.33
% 21.96/22.33 Intermediate Status:
% 21.96/22.33 Generated: 43766
% 21.96/22.33 Kept: 8275
% 21.96/22.33 Inuse: 660
% 21.96/22.33 Deleted: 2
% 21.96/22.33 Deletedinuse: 1
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 *** allocated 256285 integers for termspace/termends
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33
% 21.96/22.33 Intermediate Status:
% 21.96/22.33 Generated: 61577
% 21.96/22.33 Kept: 10302
% 21.96/22.33 Inuse: 779
% 21.96/22.33 Deleted: 4
% 21.96/22.33 Deletedinuse: 2
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 *** allocated 864960 integers for clauses
% 21.96/22.33
% 21.96/22.33 Intermediate Status:
% 21.96/22.33 Generated: 76356
% 21.96/22.33 Kept: 12876
% 21.96/22.33 Inuse: 869
% 21.96/22.33 Deleted: 6
% 21.96/22.33 Deletedinuse: 4
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33
% 21.96/22.33 Intermediate Status:
% 21.96/22.33 Generated: 88819
% 21.96/22.33 Kept: 14877
% 21.96/22.33 Inuse: 979
% 21.96/22.33 Deleted: 8
% 21.96/22.33 Deletedinuse: 4
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 *** allocated 384427 integers for termspace/termends
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33
% 21.96/22.33 Intermediate Status:
% 21.96/22.33 Generated: 104619
% 21.96/22.33 Kept: 16882
% 21.96/22.33 Inuse: 1129
% 21.96/22.33 Deleted: 10
% 21.96/22.33 Deletedinuse: 4
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 *** allocated 1297440 integers for clauses
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33
% 21.96/22.33 Intermediate Status:
% 21.96/22.33 Generated: 114062
% 21.96/22.33 Kept: 18898
% 21.96/22.33 Inuse: 1212
% 21.96/22.33 Deleted: 14
% 21.96/22.33 Deletedinuse: 8
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 Resimplifying clauses:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33
% 21.96/22.33 Intermediate Status:
% 21.96/22.33 Generated: 124135
% 21.96/22.33 Kept: 20902
% 21.96/22.33 Inuse: 1304
% 21.96/22.33 Deleted: 949
% 21.96/22.33 Deletedinuse: 8
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33 Resimplifying inuse:
% 21.96/22.33 Done
% 21.96/22.33
% 21.96/22.33
% 21.96/22.33 Intermediate Status:
% 21.96/22.33 Generated: 135084
% 21.96/22.33 Kept: 22947
% 21.96/22.33 Inuse: 1399
% 21.96/22.33 Deleted: 949
% 55.54/55.94 Deletedinuse: 8
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 145197
% 55.54/55.94 Kept: 24966
% 55.54/55.94 Inuse: 1503
% 55.54/55.94 Deleted: 949
% 55.54/55.94 Deletedinuse: 8
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 *** allocated 1946160 integers for clauses
% 55.54/55.94 *** allocated 576640 integers for termspace/termends
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 155348
% 55.54/55.94 Kept: 26978
% 55.54/55.94 Inuse: 1610
% 55.54/55.94 Deleted: 949
% 55.54/55.94 Deletedinuse: 8
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 166629
% 55.54/55.94 Kept: 28981
% 55.54/55.94 Inuse: 1727
% 55.54/55.94 Deleted: 949
% 55.54/55.94 Deletedinuse: 8
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 178595
% 55.54/55.94 Kept: 30994
% 55.54/55.94 Inuse: 1841
% 55.54/55.94 Deleted: 987
% 55.54/55.94 Deletedinuse: 8
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 190184
% 55.54/55.94 Kept: 33024
% 55.54/55.94 Inuse: 1985
% 55.54/55.94 Deleted: 2614
% 55.54/55.94 Deletedinuse: 1444
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 199401
% 55.54/55.94 Kept: 35028
% 55.54/55.94 Inuse: 2148
% 55.54/55.94 Deleted: 2683
% 55.54/55.94 Deletedinuse: 1444
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 207260
% 55.54/55.94 Kept: 37041
% 55.54/55.94 Inuse: 2290
% 55.54/55.94 Deleted: 2696
% 55.54/55.94 Deletedinuse: 1444
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 218882
% 55.54/55.94 Kept: 39052
% 55.54/55.94 Inuse: 2458
% 55.54/55.94 Deleted: 2702
% 55.54/55.94 Deletedinuse: 1444
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 *** allocated 2919240 integers for clauses
% 55.54/55.94 Resimplifying clauses:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 234685
% 55.54/55.94 Kept: 41052
% 55.54/55.94 Inuse: 2590
% 55.54/55.94 Deleted: 26289
% 55.54/55.94 Deletedinuse: 1455
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 *** allocated 864960 integers for termspace/termends
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 262025
% 55.54/55.94 Kept: 43251
% 55.54/55.94 Inuse: 2727
% 55.54/55.94 Deleted: 26304
% 55.54/55.94 Deletedinuse: 1470
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 273866
% 55.54/55.94 Kept: 45254
% 55.54/55.94 Inuse: 2830
% 55.54/55.94 Deleted: 26310
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 284898
% 55.54/55.94 Kept: 47292
% 55.54/55.94 Inuse: 2913
% 55.54/55.94 Deleted: 26311
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 297269
% 55.54/55.94 Kept: 49306
% 55.54/55.94 Inuse: 2997
% 55.54/55.94 Deleted: 26311
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 310847
% 55.54/55.94 Kept: 51515
% 55.54/55.94 Inuse: 3081
% 55.54/55.94 Deleted: 26311
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 325816
% 55.54/55.94 Kept: 53525
% 55.54/55.94 Inuse: 3151
% 55.54/55.94 Deleted: 26311
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 347025
% 55.54/55.94 Kept: 55536
% 55.54/55.94 Inuse: 3282
% 55.54/55.94 Deleted: 26311
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 356797
% 55.54/55.94 Kept: 57559
% 55.54/55.94 Inuse: 3326
% 55.54/55.94 Deleted: 26311
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 370053
% 55.54/55.94 Kept: 59590
% 55.54/55.94 Inuse: 3404
% 55.54/55.94 Deleted: 26318
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 *** allocated 4378860 integers for clauses
% 55.54/55.94 Resimplifying clauses:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 *** allocated 1297440 integers for termspace/termends
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 382071
% 55.54/55.94 Kept: 61619
% 55.54/55.94 Inuse: 3456
% 55.54/55.94 Deleted: 27304
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 393469
% 55.54/55.94 Kept: 63646
% 55.54/55.94 Inuse: 3534
% 55.54/55.94 Deleted: 27304
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 411102
% 55.54/55.94 Kept: 65657
% 55.54/55.94 Inuse: 3605
% 55.54/55.94 Deleted: 27304
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 420443
% 55.54/55.94 Kept: 67800
% 55.54/55.94 Inuse: 3646
% 55.54/55.94 Deleted: 27304
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 429898
% 55.54/55.94 Kept: 69804
% 55.54/55.94 Inuse: 3700
% 55.54/55.94 Deleted: 27304
% 55.54/55.94 Deletedinuse: 1471
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 446738
% 55.54/55.94 Kept: 71804
% 55.54/55.94 Inuse: 3790
% 55.54/55.94 Deleted: 27305
% 55.54/55.94 Deletedinuse: 1472
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 477380
% 55.54/55.94 Kept: 73833
% 55.54/55.94 Inuse: 3911
% 55.54/55.94 Deleted: 27306
% 55.54/55.94 Deletedinuse: 1473
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 494321
% 55.54/55.94 Kept: 75848
% 55.54/55.94 Inuse: 4067
% 55.54/55.94 Deleted: 27306
% 55.54/55.94 Deletedinuse: 1473
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 518783
% 55.54/55.94 Kept: 77878
% 55.54/55.94 Inuse: 4226
% 55.54/55.94 Deleted: 27306
% 55.54/55.94 Deletedinuse: 1473
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 534381
% 55.54/55.94 Kept: 80302
% 55.54/55.94 Inuse: 4291
% 55.54/55.94 Deleted: 27306
% 55.54/55.94 Deletedinuse: 1473
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying clauses:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 544212
% 55.54/55.94 Kept: 82585
% 55.54/55.94 Inuse: 4316
% 55.54/55.94 Deleted: 27761
% 55.54/55.94 Deletedinuse: 1473
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 586145
% 55.54/55.94 Kept: 84625
% 55.54/55.94 Inuse: 4396
% 55.54/55.94 Deleted: 28172
% 55.54/55.94 Deletedinuse: 1879
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 615076
% 55.54/55.94 Kept: 86626
% 55.54/55.94 Inuse: 4465
% 55.54/55.94 Deleted: 28175
% 55.54/55.94 Deletedinuse: 1879
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 623940
% 55.54/55.94 Kept: 88634
% 55.54/55.94 Inuse: 4521
% 55.54/55.94 Deleted: 28176
% 55.54/55.94 Deletedinuse: 1879
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 634897
% 55.54/55.94 Kept: 90646
% 55.54/55.94 Inuse: 4595
% 55.54/55.94 Deleted: 28178
% 55.54/55.94 Deletedinuse: 1879
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 *** allocated 6568290 integers for clauses
% 55.54/55.94 *** allocated 1946160 integers for termspace/termends
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 647274
% 55.54/55.94 Kept: 92706
% 55.54/55.94 Inuse: 4654
% 55.54/55.94 Deleted: 28179
% 55.54/55.94 Deletedinuse: 1879
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 654110
% 55.54/55.94 Kept: 94729
% 55.54/55.94 Inuse: 4676
% 55.54/55.94 Deleted: 28179
% 55.54/55.94 Deletedinuse: 1879
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 664213
% 55.54/55.94 Kept: 96738
% 55.54/55.94 Inuse: 4705
% 55.54/55.94 Deleted: 28179
% 55.54/55.94 Deletedinuse: 1879
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 670581
% 55.54/55.94 Kept: 98777
% 55.54/55.94 Inuse: 4725
% 55.54/55.94 Deleted: 28179
% 55.54/55.94 Deletedinuse: 1879
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Intermediate Status:
% 55.54/55.94 Generated: 675542
% 55.54/55.94 Kept: 100842
% 55.54/55.94 Inuse: 4744
% 55.54/55.94 Deleted: 28179
% 55.54/55.94 Deletedinuse: 1879
% 55.54/55.94
% 55.54/55.94 Resimplifying inuse:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94 Resimplifying clauses:
% 55.54/55.94 Done
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Bliksems!, er is een bewijs:
% 55.54/55.94 % SZS status Theorem
% 55.54/55.94 % SZS output start Refutation
% 55.54/55.94
% 55.54/55.94 (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 55.54/55.94 (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 55.54/55.94 (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z ), coll( Y
% 55.54/55.94 , Z, X ) }.
% 55.54/55.94 (3) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( X, Y, T, Z ) }.
% 55.54/55.94 (4) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( Z, T, X, Y ) }.
% 55.54/55.94 (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 55.54/55.94 (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z )
% 55.54/55.94 }.
% 55.54/55.94 (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T )
% 55.54/55.94 }.
% 55.54/55.94 (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T )
% 55.54/55.94 }.
% 55.54/55.94 (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y, T
% 55.54/55.94 ), cyclic( X, Y, Z, T ) }.
% 55.54/55.94 (23) {G0,W10,D2,L2,V4,M2} I { ! cong( X, Y, Z, T ), cong( Z, T, X, Y ) }.
% 55.54/55.94 (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X, Y, U, W, Z
% 55.54/55.94 , T, U, W ) }.
% 55.54/55.94 (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll(
% 55.54/55.94 Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 55.54/55.94 (63) {G0,W13,D2,L3,V5,M3} I { ! midp( U, X, Y ), ! midp( U, Z, T ), para( X
% 55.54/55.94 , Z, Y, T ) }.
% 55.54/55.94 (67) {G0,W13,D2,L3,V3,M3} I { ! cong( X, Y, X, Z ), ! coll( X, Y, Z ), midp
% 55.54/55.94 ( X, Y, Z ) }.
% 55.54/55.94 (69) {G0,W8,D2,L2,V3,M2} I { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 55.54/55.94 (88) {G0,W22,D3,L5,V7,M5} I { ! midp( Z, X, Y ), ! midp( W, T, U ), ! coll
% 55.54/55.94 ( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0 ) }.
% 55.54/55.94 (120) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol27, skol22 ) }.
% 55.54/55.94 (121) {G0,W5,D2,L1,V0,M1} I { cong( skol26, skol27, skol26, skol22 ) }.
% 55.54/55.94 (122) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol29, skol23 ) }.
% 55.54/55.94 (123) {G0,W5,D2,L1,V0,M1} I { cong( skol26, skol29, skol26, skol23 ) }.
% 55.54/55.94 (127) {G0,W4,D2,L1,V0,M1} I { coll( skol24, skol26, skol29 ) }.
% 55.54/55.94 (128) {G0,W5,D2,L1,V0,M1} I { ! cyclic( skol20, skol22, skol23, skol24 )
% 55.54/55.94 }.
% 55.54/55.94 (129) {G1,W8,D2,L2,V3,M2} F(2) { ! coll( X, Y, Z ), coll( Z, Z, X ) }.
% 55.54/55.94 (151) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y, Y, Z ), !
% 55.54/55.94 coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 55.54/55.94 (166) {G1,W4,D2,L1,V0,M1} R(0,122) { coll( skol26, skol23, skol29 ) }.
% 55.54/55.94 (174) {G2,W4,D2,L1,V0,M1} R(1,166) { coll( skol23, skol26, skol29 ) }.
% 55.54/55.94 (176) {G1,W8,D2,L2,V3,M2} R(1,0) { ! coll( X, Y, Z ), coll( Y, Z, X ) }.
% 55.54/55.94 (177) {G1,W4,D2,L1,V0,M1} R(1,122) { coll( skol29, skol26, skol23 ) }.
% 55.54/55.94 (206) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), coll( Z, T, X ), !
% 55.54/55.94 coll( X, T, Y ) }.
% 55.54/55.94 (207) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll( X, Y, T ),
% 55.54/55.94 coll( Z, X, T ) }.
% 55.54/55.94 (218) {G2,W8,D2,L2,V3,M2} F(207) { ! coll( X, Y, Z ), coll( Z, X, Z ) }.
% 55.54/55.94 (243) {G1,W10,D2,L2,V4,M2} R(4,3) { ! para( X, Y, Z, T ), para( Z, T, Y, X
% 55.54/55.94 ) }.
% 55.54/55.94 (275) {G1,W4,D2,L1,V0,M1} R(120,1) { coll( skol27, skol26, skol22 ) }.
% 55.54/55.94 (276) {G1,W4,D2,L1,V0,M1} R(120,0) { coll( skol26, skol22, skol27 ) }.
% 55.54/55.94 (279) {G2,W4,D2,L1,V0,M1} R(275,0) { coll( skol27, skol22, skol26 ) }.
% 55.54/55.94 (282) {G3,W4,D2,L1,V0,M1} R(279,1) { coll( skol22, skol27, skol26 ) }.
% 55.54/55.94 (287) {G4,W4,D2,L1,V0,M1} R(282,0) { coll( skol22, skol26, skol27 ) }.
% 55.54/55.94 (387) {G1,W5,D2,L1,V0,M1} R(13,128) { ! cyclic( skol20, skol22, skol24,
% 55.54/55.94 skol23 ) }.
% 55.54/55.94 (401) {G1,W10,D2,L2,V4,M2} R(14,13) { ! cyclic( X, Y, Z, T ), cyclic( X, Z
% 55.54/55.94 , T, Y ) }.
% 55.54/55.94 (410) {G1,W10,D2,L2,V4,M2} R(15,14) { ! cyclic( X, Y, Z, T ), cyclic( Y, Z
% 55.54/55.94 , X, T ) }.
% 55.54/55.94 (411) {G2,W5,D2,L1,V0,M1} R(15,387) { ! cyclic( skol22, skol20, skol24,
% 55.54/55.94 skol23 ) }.
% 55.54/55.94 (441) {G1,W15,D2,L3,V5,M3} R(16,13) { ! cyclic( X, Y, Z, T ), cyclic( Y, Z
% 55.54/55.94 , T, U ), ! cyclic( X, Y, U, Z ) }.
% 55.54/55.94 (466) {G3,W10,D2,L2,V1,M2} R(411,16) { ! cyclic( X, skol22, skol20, skol24
% 55.54/55.94 ), ! cyclic( X, skol22, skol20, skol23 ) }.
% 55.54/55.94 (522) {G5,W4,D2,L1,V0,M1} R(218,287) { coll( skol27, skol22, skol27 ) }.
% 55.54/55.94 (525) {G3,W4,D2,L1,V0,M1} R(218,275) { coll( skol22, skol27, skol22 ) }.
% 55.54/55.94 (532) {G3,W4,D2,L1,V0,M1} R(218,177) { coll( skol23, skol29, skol23 ) }.
% 55.54/55.94 (534) {G3,W4,D2,L1,V0,M1} R(218,174) { coll( skol29, skol23, skol29 ) }.
% 55.54/55.94 (539) {G3,W12,D2,L3,V4,M3} R(218,2) { coll( X, Y, X ), ! coll( X, Z, Y ), !
% 55.54/55.94 coll( X, Z, T ) }.
% 55.54/55.94 (553) {G3,W4,D2,L1,V0,M1} R(218,127) { coll( skol29, skol24, skol29 ) }.
% 55.54/55.94 (554) {G4,W8,D2,L2,V3,M2} F(539) { coll( X, Y, X ), ! coll( X, Z, Y ) }.
% 55.54/55.94 (581) {G1,W5,D2,L1,V0,M1} R(23,121) { cong( skol26, skol22, skol26, skol27
% 55.54/55.94 ) }.
% 55.54/55.94 (743) {G4,W4,D2,L1,V0,M1} R(525,0) { coll( skol22, skol22, skol27 ) }.
% 55.54/55.94 (895) {G1,W14,D2,L3,V3,M3} R(42,39) { ! coll( X, X, Y ), cyclic( Z, Y, X, X
% 55.54/55.94 ), ! para( X, Z, X, Z ) }.
% 55.54/55.94 (1060) {G4,W4,D2,L1,V0,M1} R(534,0) { coll( skol29, skol29, skol23 ) }.
% 55.54/55.94 (1746) {G4,W4,D2,L1,V0,M1} R(553,0) { coll( skol29, skol29, skol24 ) }.
% 55.54/55.94 (1754) {G5,W8,D2,L2,V1,M2} R(1746,2) { ! coll( skol29, skol29, X ), coll(
% 55.54/55.94 skol24, X, skol29 ) }.
% 55.54/55.94 (1985) {G5,W8,D2,L2,V3,M2} R(554,1) { ! coll( X, Y, Z ), coll( Z, X, X )
% 55.54/55.94 }.
% 55.54/55.94 (1992) {G6,W8,D2,L2,V3,M2} R(1985,0) { coll( X, Y, Y ), ! coll( Y, X, Z )
% 55.54/55.94 }.
% 55.54/55.94 (2007) {G7,W8,D2,L2,V3,M2} R(1992,1992) { ! coll( X, Y, Z ), coll( X, Y, Y
% 55.54/55.94 ) }.
% 55.54/55.94 (2012) {G8,W12,D2,L3,V4,M3} R(2007,2) { ! coll( X, Y, Z ), ! coll( X, Y, T
% 55.54/55.94 ), coll( T, Y, X ) }.
% 55.54/55.94 (2013) {G9,W8,D2,L2,V3,M2} F(2012) { ! coll( X, Y, Z ), coll( Z, Y, X ) }.
% 55.54/55.94 (2125) {G1,W13,D2,L3,V5,M3} R(63,10) { ! midp( X, Y, Z ), para( Y, T, Z, U
% 55.54/55.94 ), ! midp( X, U, T ) }.
% 55.54/55.94 (2135) {G2,W9,D2,L2,V3,M2} F(2125) { ! midp( X, Y, Z ), para( Y, Z, Z, Y )
% 55.54/55.94 }.
% 55.54/55.94 (2166) {G1,W8,D2,L2,V3,M2} R(69,1) { ! midp( X, Y, Z ), coll( Y, X, Z ) }.
% 55.54/55.94 (2373) {G2,W4,D2,L1,V0,M1} R(67,581);r(276) { midp( skol26, skol22, skol27
% 55.54/55.94 ) }.
% 55.54/55.94 (2517) {G1,W4,D2,L1,V0,M1} R(67,123);r(122) { midp( skol26, skol29, skol23
% 55.54/55.94 ) }.
% 55.54/55.94 (2739) {G6,W8,D2,L2,V2,M2} R(1754,129) { coll( skol24, X, skol29 ), ! coll
% 55.54/55.94 ( X, Y, skol29 ) }.
% 55.54/55.94 (3216) {G7,W8,D2,L2,V2,M2} R(2739,176) { ! coll( X, Y, skol29 ), coll( X,
% 55.54/55.94 skol29, skol24 ) }.
% 55.54/55.94 (3264) {G8,W8,D2,L2,V2,M2} R(3216,129) { coll( X, skol29, skol24 ), ! coll
% 55.54/55.94 ( skol29, Y, X ) }.
% 55.54/55.94 (3283) {G9,W8,D2,L2,V2,M2} R(3264,176) { ! coll( skol29, X, Y ), coll(
% 55.54/55.94 skol29, skol24, Y ) }.
% 55.54/55.94 (4424) {G10,W8,D2,L2,V2,M2} R(3283,2166) { coll( skol29, skol24, X ), !
% 55.54/55.94 midp( Y, skol29, X ) }.
% 55.54/55.94 (4497) {G11,W8,D2,L2,V2,M2} R(4424,2013) { ! midp( X, skol29, Y ), coll( Y
% 55.54/55.94 , skol24, skol29 ) }.
% 55.54/55.94 (8457) {G5,W10,D3,L2,V1,M2} R(151,2517);r(1060) { ! coll( skol23, skol29,
% 55.54/55.94 skol23 ), midp( skol7( skol29, X ), skol29, X ) }.
% 55.54/55.94 (8459) {G5,W10,D3,L2,V1,M2} R(151,2373);r(743) { ! coll( skol27, skol22,
% 55.54/55.94 skol27 ), midp( skol7( skol22, X ), skol22, X ) }.
% 55.54/55.94 (20056) {G6,W6,D3,L1,V1,M1} S(8457);r(532) { midp( skol7( skol29, X ),
% 55.54/55.94 skol29, X ) }.
% 55.54/55.94 (20058) {G6,W6,D3,L1,V1,M1} S(8459);r(522) { midp( skol7( skol22, X ),
% 55.54/55.94 skol22, X ) }.
% 55.54/55.94 (30423) {G12,W4,D2,L1,V1,M1} R(20056,4497) { coll( X, skol24, skol29 ) }.
% 55.54/55.94 (30493) {G13,W4,D2,L1,V1,M1} R(30423,2739) { coll( skol24, X, skol29 ) }.
% 55.54/55.94 (30495) {G13,W4,D2,L1,V1,M1} R(30423,176) { coll( skol24, skol29, X ) }.
% 55.54/55.94 (30515) {G14,W4,D2,L1,V2,M1} R(30493,206);r(30495) { coll( X, Y, skol24 )
% 55.54/55.94 }.
% 55.54/55.94 (30579) {G15,W4,D2,L1,V2,M1} R(30515,176) { coll( X, skol24, Y ) }.
% 55.54/55.94 (30591) {G16,W4,D2,L1,V3,M1} R(30579,207);r(30579) { coll( Z, X, Y ) }.
% 55.54/55.94 (31010) {G7,W6,D3,L1,V1,M1} R(20058,10) { midp( skol7( skol22, X ), X,
% 55.54/55.94 skol22 ) }.
% 55.54/55.94 (31054) {G17,W10,D3,L2,V2,M2} R(31010,151);r(30591) { ! coll( skol22, X,
% 55.54/55.94 skol22 ), midp( skol7( X, Y ), X, Y ) }.
% 55.54/55.94 (40120) {G18,W6,D3,L1,V2,M1} S(31054);r(30591) { midp( skol7( X, Y ), X, Y
% 55.54/55.94 ) }.
% 55.54/55.94 (40280) {G17,W10,D2,L2,V3,M2} S(895);r(30591) { cyclic( Z, Y, X, X ), !
% 55.54/55.94 para( X, Z, X, Z ) }.
% 55.54/55.94 (41382) {G19,W6,D3,L1,V2,M1} R(40120,10) { midp( skol7( X, Y ), Y, X ) }.
% 55.54/55.94 (82798) {G20,W5,D2,L1,V2,M1} R(2135,41382) { para( X, Y, Y, X ) }.
% 55.54/55.94 (82811) {G21,W5,D2,L1,V2,M1} R(82798,243) { para( X, Y, X, Y ) }.
% 55.54/55.94 (100879) {G22,W5,D2,L1,V3,M1} S(40280);r(82811) { cyclic( Z, Y, X, X ) }.
% 55.54/55.94 (100948) {G23,W5,D2,L1,V3,M1} R(100879,410) { cyclic( X, Y, Z, Y ) }.
% 55.54/55.94 (100950) {G23,W5,D2,L1,V3,M1} R(100879,401) { cyclic( X, Y, Y, Z ) }.
% 55.54/55.94 (100980) {G24,W5,D2,L1,V3,M1} R(100948,441);r(100950) { cyclic( Y, Y, Z, T
% 55.54/55.94 ) }.
% 55.54/55.94 (101026) {G25,W0,D0,L0,V0,M0} R(100980,466);r(100980) { }.
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 % SZS output end Refutation
% 55.54/55.94 found a proof!
% 55.54/55.94
% 55.54/55.94
% 55.54/55.94 Unprocessed initial clauses:
% 55.54/55.94
% 55.54/55.94 (101028) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 55.54/55.94 (101029) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 55.54/55.94 (101030) {G0,W12,D2,L3,V4,M3} { ! coll( X, T, Y ), ! coll( X, T, Z ), coll
% 55.54/55.94 ( Y, Z, X ) }.
% 55.54/55.94 (101031) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( X, Y, T, Z )
% 55.54/55.94 }.
% 55.54/55.94 (101032) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( Z, T, X, Y )
% 55.54/55.94 }.
% 55.54/55.94 (101033) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! para( U, W, Z, T )
% 55.54/55.94 , para( X, Y, Z, T ) }.
% 55.54/55.94 (101034) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( X, Y, T, Z )
% 55.54/55.94 }.
% 55.54/55.94 (101035) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( Z, T, X, Y )
% 55.54/55.94 }.
% 55.54/55.94 (101036) {G0,W15,D2,L3,V6,M3} { ! perp( X, Y, U, W ), ! perp( U, W, Z, T )
% 55.54/55.94 , para( X, Y, Z, T ) }.
% 55.54/55.94 (101037) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! perp( U, W, Z, T )
% 55.54/55.94 , perp( X, Y, Z, T ) }.
% 55.54/55.94 (101038) {G0,W8,D2,L2,V3,M2} { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 55.54/55.94 (101039) {G0,W15,D2,L3,V4,M3} { ! cong( T, X, T, Y ), ! cong( T, X, T, Z )
% 55.54/55.94 , circle( T, X, Y, Z ) }.
% 55.54/55.94 (101040) {G0,W20,D2,L4,V5,M4} { ! cong( U, X, U, Y ), ! cong( U, X, U, Z )
% 55.54/55.94 , ! cong( U, X, U, T ), cyclic( X, Y, Z, T ) }.
% 55.54/55.94 (101041) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z
% 55.54/55.94 ) }.
% 55.54/55.94 (101042) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T
% 55.54/55.94 ) }.
% 55.54/55.94 (101043) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T
% 55.54/55.94 ) }.
% 55.54/55.94 (101044) {G0,W15,D2,L3,V5,M3} { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y
% 55.54/55.94 , T ), cyclic( X, Y, Z, T ) }.
% 55.54/55.94 (101045) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 55.54/55.94 eqangle( Y, X, Z, T, U, W, V0, V1 ) }.
% 55.54/55.94 (101046) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 55.54/55.94 eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 55.54/55.94 (101047) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 55.54/55.94 eqangle( U, W, V0, V1, X, Y, Z, T ) }.
% 55.54/55.94 (101048) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 55.54/55.94 eqangle( X, Y, U, W, Z, T, V0, V1 ) }.
% 55.54/55.94 (101049) {G0,W27,D2,L3,V12,M3} { ! eqangle( X, Y, Z, T, V2, V3, V4, V5 ),
% 55.54/55.94 ! eqangle( V2, V3, V4, V5, U, W, V0, V1 ), eqangle( X, Y, Z, T, U, W, V0
% 55.54/55.94 , V1 ) }.
% 55.54/55.94 (101050) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( X, Y, T, Z )
% 55.54/55.94 }.
% 55.54/55.94 (101051) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( Z, T, X, Y )
% 55.54/55.94 }.
% 55.54/55.94 (101052) {G0,W15,D2,L3,V6,M3} { ! cong( X, Y, U, W ), ! cong( U, W, Z, T )
% 55.54/55.94 , cong( X, Y, Z, T ) }.
% 55.54/55.94 (101053) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 55.54/55.94 eqratio( Y, X, Z, T, U, W, V0, V1 ) }.
% 55.54/55.94 (101054) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 55.54/55.94 eqratio( Z, T, X, Y, V0, V1, U, W ) }.
% 55.54/55.94 (101055) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 55.54/55.94 eqratio( U, W, V0, V1, X, Y, Z, T ) }.
% 55.54/55.94 (101056) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 55.54/55.94 eqratio( X, Y, U, W, Z, T, V0, V1 ) }.
% 55.54/55.94 (101057) {G0,W27,D2,L3,V12,M3} { ! eqratio( X, Y, Z, T, V2, V3, V4, V5 ),
% 55.54/55.94 ! eqratio( V2, V3, V4, V5, U, W, V0, V1 ), eqratio( X, Y, Z, T, U, W, V0
% 55.54/55.94 , V1 ) }.
% 55.54/55.94 (101058) {G0,W14,D2,L2,V6,M2} { ! simtri( X, Z, Y, T, W, U ), simtri( X, Y
% 55.54/55.94 , Z, T, U, W ) }.
% 55.54/55.94 (101059) {G0,W14,D2,L2,V6,M2} { ! simtri( Y, X, Z, U, T, W ), simtri( X, Y
% 55.54/55.94 , Z, T, U, W ) }.
% 55.54/55.94 (101060) {G0,W14,D2,L2,V6,M2} { ! simtri( T, U, W, X, Y, Z ), simtri( X, Y
% 55.54/55.94 , Z, T, U, W ) }.
% 55.54/55.94 (101061) {G0,W21,D2,L3,V9,M3} { ! simtri( X, Y, Z, V0, V1, V2 ), ! simtri
% 55.54/55.94 ( V0, V1, V2, T, U, W ), simtri( X, Y, Z, T, U, W ) }.
% 55.54/55.94 (101062) {G0,W14,D2,L2,V6,M2} { ! contri( X, Z, Y, T, W, U ), contri( X, Y
% 55.54/55.94 , Z, T, U, W ) }.
% 55.54/55.94 (101063) {G0,W14,D2,L2,V6,M2} { ! contri( Y, X, Z, U, T, W ), contri( X, Y
% 55.54/55.94 , Z, T, U, W ) }.
% 55.54/55.94 (101064) {G0,W14,D2,L2,V6,M2} { ! contri( T, U, W, X, Y, Z ), contri( X, Y
% 55.54/55.94 , Z, T, U, W ) }.
% 55.54/55.94 (101065) {G0,W21,D2,L3,V9,M3} { ! contri( X, Y, Z, V0, V1, V2 ), ! contri
% 55.54/55.94 ( V0, V1, V2, T, U, W ), contri( X, Y, Z, T, U, W ) }.
% 55.54/55.94 (101066) {G0,W14,D2,L2,V6,M2} { ! eqangle( X, Y, U, W, Z, T, U, W ), para
% 55.54/55.94 ( X, Y, Z, T ) }.
% 55.54/55.94 (101067) {G0,W14,D2,L2,V6,M2} { ! para( X, Y, Z, T ), eqangle( X, Y, U, W
% 55.54/55.94 , Z, T, U, W ) }.
% 55.54/55.94 (101068) {G0,W14,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z,
% 55.54/55.94 Y, T, X, T, Y ) }.
% 55.54/55.94 (101069) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y ), coll
% 55.54/55.94 ( Z, T, X ), cyclic( X, Y, Z, T ) }.
% 55.54/55.94 (101070) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y ), !
% 55.54/55.94 coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 55.54/55.94 (101071) {G0,W29,D2,L5,V6,M5} { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U
% 55.54/55.94 , T ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T ), cong
% 55.54/55.94 ( X, Y, Z, T ) }.
% 55.54/55.94 (101072) {G0,W13,D2,L3,V5,M3} { ! midp( Z, U, X ), ! midp( T, U, Y ), para
% 55.54/55.94 ( Z, T, X, Y ) }.
% 55.54/55.94 (101073) {G0,W17,D2,L4,V5,M4} { ! midp( U, X, T ), ! para( U, Z, T, Y ), !
% 55.54/55.94 coll( Z, X, Y ), midp( Z, X, Y ) }.
% 55.54/55.94 (101074) {G0,W14,D2,L2,V3,M2} { ! cong( Z, X, Z, Y ), eqangle( Z, X, X, Y
% 55.54/55.94 , X, Y, Z, Y ) }.
% 55.54/55.94 (101075) {G0,W18,D2,L3,V3,M3} { ! eqangle( Z, X, X, Y, X, Y, Z, Y ), coll
% 55.54/55.94 ( Z, X, Y ), cong( Z, X, Z, Y ) }.
% 55.54/55.94 (101076) {G0,W19,D2,L3,V5,M3} { ! circle( U, X, Y, Z ), ! perp( U, X, X, T
% 55.54/55.94 ), eqangle( X, T, X, Y, Z, X, Z, Y ) }.
% 55.54/55.94 (101077) {G0,W19,D2,L3,V5,M3} { ! circle( Y, X, T, U ), ! eqangle( X, Z, X
% 55.54/55.94 , T, U, X, U, T ), perp( Y, X, X, Z ) }.
% 55.54/55.94 (101078) {G0,W18,D2,L3,V5,M3} { ! circle( T, X, Y, Z ), ! midp( U, Y, Z )
% 55.54/55.94 , eqangle( X, Y, X, Z, T, Y, T, U ) }.
% 55.54/55.94 (101079) {G0,W22,D2,L4,V5,M4} { ! circle( U, T, X, Y ), ! coll( Z, X, Y )
% 55.54/55.94 , ! eqangle( T, X, T, Y, U, X, U, Z ), midp( Z, X, Y ) }.
% 55.54/55.94 (101080) {G0,W14,D2,L3,V4,M3} { ! perp( X, Y, Y, T ), ! midp( Z, X, T ),
% 55.54/55.94 cong( X, Z, Y, Z ) }.
% 55.54/55.94 (101081) {G0,W14,D2,L3,V4,M3} { ! circle( T, X, Y, Z ), ! coll( T, X, Z )
% 55.54/55.94 , perp( X, Y, Y, Z ) }.
% 55.54/55.94 (101082) {G0,W19,D2,L3,V4,M3} { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T
% 55.54/55.94 ), eqangle( X, T, Z, T, Z, T, Z, Y ) }.
% 55.54/55.94 (101083) {G0,W14,D2,L3,V4,M3} { ! midp( T, X, Y ), ! perp( Z, T, X, Y ),
% 55.54/55.94 cong( Z, X, Z, Y ) }.
% 55.54/55.94 (101084) {G0,W15,D2,L3,V4,M3} { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T )
% 55.54/55.94 , perp( X, Y, Z, T ) }.
% 55.54/55.94 (101085) {G0,W20,D2,L4,V4,M4} { ! cong( X, Y, T, Y ), ! cong( X, Z, T, Z )
% 55.54/55.94 , ! cyclic( X, T, Y, Z ), perp( Y, X, X, Z ) }.
% 55.54/55.94 (101086) {G0,W29,D2,L4,V6,M4} { ! eqangle( X, Y, Y, Z, T, U, U, W ), !
% 55.54/55.94 eqangle( X, Z, Y, Z, T, W, U, W ), coll( X, Y, Z ), simtri( X, Y, Z, T, U
% 55.54/55.94 , W ) }.
% 55.54/55.95 (101087) {G0,W16,D2,L2,V6,M2} { ! simtri( X, Y, Z, T, U, W ), eqratio( X,
% 55.54/55.95 Y, X, Z, T, U, T, W ) }.
% 55.54/55.95 (101088) {G0,W16,D2,L2,V6,M2} { ! simtri( X, Y, Z, T, U, W ), eqangle( X,
% 55.54/55.95 Y, Y, Z, T, U, U, W ) }.
% 55.54/55.95 (101089) {G0,W19,D2,L3,V6,M3} { ! simtri( X, Y, Z, T, U, W ), ! cong( X, Y
% 55.54/55.95 , T, U ), contri( X, Y, Z, T, U, W ) }.
% 55.54/55.95 (101090) {G0,W12,D2,L2,V6,M2} { ! contri( X, Y, U, Z, T, W ), cong( X, Y,
% 55.54/55.95 Z, T ) }.
% 55.54/55.95 (101091) {G0,W13,D2,L3,V5,M3} { ! midp( U, X, Y ), ! midp( U, Z, T ), para
% 55.54/55.95 ( X, Z, Y, T ) }.
% 55.54/55.95 (101092) {G0,W18,D2,L4,V5,M4} { ! midp( Z, T, U ), ! para( T, X, U, Y ), !
% 55.54/55.95 para( T, Y, U, X ), midp( Z, X, Y ) }.
% 55.54/55.95 (101093) {G0,W22,D2,L4,V5,M4} { ! para( X, Y, Z, T ), ! coll( U, X, Z ), !
% 55.54/55.95 coll( U, Y, T ), eqratio( U, X, X, Z, U, Y, Y, T ) }.
% 55.54/55.95 (101094) {G0,W9,D2,L2,V3,M2} { ! para( X, Y, X, Z ), coll( X, Y, Z ) }.
% 55.54/55.95 (101095) {G0,W13,D2,L3,V3,M3} { ! cong( X, Y, X, Z ), ! coll( X, Y, Z ),
% 55.54/55.95 midp( X, Y, Z ) }.
% 55.54/55.95 (101096) {G0,W9,D2,L2,V3,M2} { ! midp( X, Y, Z ), cong( X, Y, X, Z ) }.
% 55.54/55.95 (101097) {G0,W8,D2,L2,V3,M2} { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 55.54/55.95 (101098) {G0,W17,D2,L3,V6,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ),
% 55.54/55.95 eqratio( U, X, X, Y, W, Z, Z, T ) }.
% 55.54/55.95 (101099) {G0,W19,D2,L3,V4,M3} { ! eqangle( X, Y, Z, T, Z, T, X, Y ), para
% 55.54/55.95 ( X, Y, Z, T ), perp( X, Y, Z, T ) }.
% 55.54/55.95 (101100) {G0,W19,D2,L3,V4,M3} { ! eqangle( X, Y, Z, T, Z, T, X, Y ), perp
% 55.54/55.95 ( X, Y, Z, T ), para( X, Y, Z, T ) }.
% 55.54/55.95 (101101) {G0,W19,D2,L3,V8,M3} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), !
% 55.54/55.95 para( U, W, V0, V1 ), para( X, Y, Z, T ) }.
% 55.54/55.95 (101102) {G0,W19,D2,L3,V8,M3} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), !
% 55.54/55.95 perp( U, W, V0, V1 ), perp( X, Y, Z, T ) }.
% 55.54/55.95 (101103) {G0,W19,D2,L3,V8,M3} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), !
% 55.54/55.95 cong( U, W, V0, V1 ), cong( X, Y, Z, T ) }.
% 55.54/55.95 (101104) {G0,W22,D3,L3,V6,M3} { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y,
% 55.54/55.95 Z, Y, Z, X, Z ), coll( skol1( U, W, Z, T ), Z, T ) }.
% 55.54/55.95 (101105) {G0,W22,D3,L3,V4,M3} { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y,
% 55.54/55.95 Z, Y, Z, X, Z ), coll( skol1( X, Y, Z, T ), X, Y ) }.
% 55.54/55.95 (101106) {G0,W22,D3,L3,V6,M3} { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z,
% 55.54/55.95 T, Z, T, Z, Y ), coll( skol2( U, W, Z, T ), Z, T ) }.
% 55.54/55.95 (101107) {G0,W22,D3,L3,V4,M3} { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z,
% 55.54/55.95 T, Z, T, Z, Y ), coll( Y, X, skol2( X, Y, Z, T ) ) }.
% 55.54/55.95 (101108) {G0,W22,D3,L3,V6,M3} { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z,
% 55.54/55.95 T, Z, T, Z, Y ), coll( skol3( U, W, Z, T ), Z, T ) }.
% 55.54/55.95 (101109) {G0,W22,D3,L3,V4,M3} { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z,
% 55.54/55.95 T, Z, T, Z, Y ), coll( Y, X, skol3( X, Y, Z, T ) ) }.
% 55.54/55.95 (101110) {G0,W18,D3,L3,V6,M3} { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y )
% 55.54/55.95 , coll( skol4( U, W, Z, T ), Z, T ) }.
% 55.54/55.95 (101111) {G0,W18,D3,L3,V4,M3} { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y )
% 55.54/55.95 , coll( Y, X, skol4( X, Y, Z, T ) ) }.
% 55.54/55.95 (101112) {G0,W22,D3,L3,V6,M3} { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll
% 55.54/55.95 ( X, Y, Z ), cyclic( T, Y, Z, skol5( W, Y, Z, T ) ) }.
% 55.54/55.95 (101113) {G0,W30,D3,L3,V5,M3} { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll
% 55.54/55.95 ( X, Y, Z ), eqangle( X, Z, Y, Z, X, skol5( X, Y, Z, T ), Y, skol5( X, Y
% 55.54/55.95 , Z, T ) ) }.
% 55.54/55.95 (101114) {G0,W18,D3,L3,V10,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ),
% 55.54/55.95 midp( skol6( X, V0, V1, T, V2, V3 ), X, T ) }.
% 55.54/55.95 (101115) {G0,W19,D3,L3,V8,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), para
% 55.54/55.95 ( skol6( X, V0, Z, T, V1, W ), W, X, Z ) }.
% 55.54/55.95 (101116) {G0,W19,D3,L3,V6,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), para
% 55.54/55.95 ( skol6( X, Y, Z, T, U, W ), U, Y, T ) }.
% 55.54/55.95 (101117) {G0,W22,D3,L5,V7,M5} { ! midp( Z, X, Y ), ! midp( W, T, U ), !
% 55.54/55.95 coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0 ) }.
% 55.54/55.95 (101118) {G0,W26,D3,L5,V8,M5} { ! midp( T, X, U ), ! para( X, W, Z, T ), !
% 55.54/55.95 para( X, W, U, Y ), ! coll( W, Y, Z ), coll( skol8( V0, V1, Z, T ), T, Z
% 55.54/55.95 ) }.
% 55.54/55.95 (101119) {G0,W26,D3,L5,V6,M5} { ! midp( T, X, U ), ! para( X, W, Z, T ), !
% 55.54/55.95 para( X, W, U, Y ), ! coll( W, Y, Z ), coll( skol8( X, Y, Z, T ), X, Y )
% 55.54/55.95 }.
% 55.54/55.95 (101120) {G0,W19,D3,L3,V7,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 55.54/55.95 , cong( T, Z, T, skol9( W, V0, Z, T ) ) }.
% 55.54/55.95 (101121) {G0,W19,D3,L3,V6,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 55.54/55.95 , cong( Y, Z, Y, skol9( W, Y, Z, T ) ) }.
% 55.54/55.95 (101122) {G0,W19,D3,L3,V5,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 55.54/55.95 , para( skol9( X, Y, Z, T ), Z, X, Y ) }.
% 55.54/55.95 (101123) {G0,W17,D3,L3,V5,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 55.54/55.95 , coll( skol10( U, Y, Z ), Z, Y ) }.
% 55.54/55.95 (101124) {G0,W18,D3,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 55.54/55.95 , perp( X, skol10( X, Y, Z ), Z, Y ) }.
% 55.54/55.95 (101125) {G0,W14,D2,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 55.54/55.95 , alpha1( X, Y, Z ) }.
% 55.54/55.95 (101126) {G0,W11,D3,L2,V4,M2} { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z
% 55.54/55.95 ), Z, X ) }.
% 55.54/55.95 (101127) {G0,W12,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), perp( Y, skol11( X, Y
% 55.54/55.95 , Z ), Z, X ) }.
% 55.54/55.95 (101128) {G0,W13,D2,L3,V4,M3} { ! coll( T, Z, X ), ! perp( Y, T, Z, X ),
% 55.54/55.95 alpha1( X, Y, Z ) }.
% 55.54/55.95 (101129) {G0,W12,D3,L2,V4,M2} { ! circle( Y, X, Z, T ), perp( skol12( X, Y
% 55.54/55.95 ), X, X, Y ) }.
% 55.54/55.95 (101130) {G0,W28,D3,L5,V8,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 55.54/55.95 ), ! cong( U, X, U, Y ), W = U, alpha2( X, Z, U, skol13( X, V0, Z, V1, U
% 55.54/55.95 ) ) }.
% 55.54/55.95 (101131) {G0,W26,D3,L5,V8,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 55.54/55.95 ), ! cong( U, X, U, Y ), W = U, coll( skol21( V0, Y, T, V1 ), Y, T ) }.
% 55.54/55.95 (101132) {G0,W27,D3,L5,V6,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 55.54/55.95 ), ! cong( U, X, U, Y ), W = U, cong( skol21( X, Y, T, U ), U, U, X )
% 55.54/55.95 }.
% 55.54/55.95 (101133) {G0,W9,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), coll( T, X, Y ) }.
% 55.54/55.95 (101134) {G0,W10,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), cong( T, Z, Z, X )
% 55.54/55.95 }.
% 55.54/55.95 (101135) {G0,W14,D2,L3,V4,M3} { ! coll( T, X, Y ), ! cong( T, Z, Z, X ),
% 55.54/55.95 alpha2( X, Y, Z, T ) }.
% 55.54/55.95 (101136) {G0,W22,D3,L4,V5,M4} { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T
% 55.54/55.95 ), ! midp( U, X, Y ), circle( skol14( X, Y, Z ), X, Y, Z ) }.
% 55.54/55.95 (101137) {G0,W18,D3,L3,V4,M3} { ! perp( X, Z, Z, Y ), ! cyclic( X, Y, Z, T
% 55.54/55.95 ), circle( skol15( X, Y, Z ), X, Y, Z ) }.
% 55.54/55.95 (101138) {G0,W16,D3,L3,V6,M3} { ! perp( X, U, U, T ), ! coll( T, Y, Z ),
% 55.54/55.95 coll( skol16( W, Y, Z ), Y, Z ) }.
% 55.54/55.95 (101139) {G0,W17,D3,L3,V5,M3} { ! perp( X, U, U, T ), ! coll( T, Y, Z ),
% 55.54/55.95 perp( skol16( X, Y, Z ), X, Y, Z ) }.
% 55.54/55.95 (101140) {G0,W20,D3,L4,V5,M4} { ! perp( X, Z, X, Y ), ! perp( Y, X, Y, T )
% 55.54/55.95 , ! midp( U, Z, T ), midp( skol17( X, Y ), X, Y ) }.
% 55.54/55.95 (101141) {G0,W16,D3,L3,V3,M3} { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z )
% 55.54/55.95 , coll( X, Y, skol18( X, Y ) ) }.
% 55.54/55.95 (101142) {G0,W17,D3,L3,V3,M3} { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z )
% 55.54/55.95 , cong( Y, X, Y, skol18( X, Y ) ) }.
% 55.54/55.95 (101143) {G0,W25,D3,L5,V8,M5} { ! para( U, W, X, Y ), ! coll( Z, U, X ), !
% 55.54/55.95 coll( Z, W, Y ), ! coll( T, U, W ), coll( Z, T, skol19( V0, V1, Z, T ) )
% 55.54/55.95 }.
% 55.54/55.95 (101144) {G0,W25,D3,L5,V6,M5} { ! para( U, W, X, Y ), ! coll( Z, U, X ), !
% 55.54/55.95 coll( Z, W, Y ), ! coll( T, U, W ), coll( skol19( X, Y, Z, T ), X, Y )
% 55.54/55.95 }.
% 55.54/55.95 (101145) {G0,W5,D2,L1,V0,M1} { perp( skol27, skol26, skol20, skol25 ) }.
% 55.54/55.95 (101146) {G0,W4,D2,L1,V0,M1} { coll( skol27, skol20, skol25 ) }.
% 55.54/55.95 (101147) {G0,W5,D2,L1,V0,M1} { perp( skol29, skol26, skol20, skol28 ) }.
% 55.54/55.95 (101148) {G0,W4,D2,L1,V0,M1} { coll( skol29, skol20, skol28 ) }.
% 55.54/55.95 (101149) {G0,W4,D2,L1,V0,M1} { coll( skol26, skol27, skol22 ) }.
% 55.54/55.95 (101150) {G0,W5,D2,L1,V0,M1} { cong( skol26, skol27, skol26, skol22 ) }.
% 55.54/55.95 (101151) {G0,W4,D2,L1,V0,M1} { coll( skol26, skol29, skol23 ) }.
% 55.54/55.95 (101152) {G0,W5,D2,L1,V0,M1} { cong( skol26, skol29, skol26, skol23 ) }.
% 55.54/55.95 (101153) {G0,W4,D2,L1,V0,M1} { coll( skol30, skol26, skol27 ) }.
% 55.54/55.95 (101154) {G0,W4,D2,L1,V0,M1} { coll( skol30, skol20, skol28 ) }.
% 55.54/55.95 (101155) {G0,W4,D2,L1,V0,M1} { coll( skol24, skol20, skol25 ) }.
% 55.54/55.95 (101156) {G0,W4,D2,L1,V0,M1} { coll( skol24, skol26, skol29 ) }.
% 55.54/55.95 (101157) {G0,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol22, skol23, skol24 )
% 55.54/55.95 }.
% 55.54/55.95
% 55.54/55.95
% 55.54/55.95 Total Proof:
% 55.54/55.95
% 55.54/55.95 subsumption: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent0: (101028) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 parent0: (101029) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Y, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T,
% 55.54/55.95 Z ), coll( Y, Z, X ) }.
% 55.54/55.95 parent0: (101030) {G0,W12,D2,L3,V4,M3} { ! coll( X, T, Y ), ! coll( X, T,
% 55.54/55.95 Z ), coll( Y, Z, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 2
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (3) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( X, Y
% 55.54/55.95 , T, Z ) }.
% 55.54/55.95 parent0: (101031) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( X, Y
% 55.54/55.95 , T, Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (4) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( Z, T
% 55.54/55.95 , X, Y ) }.
% 55.54/55.95 parent0: (101032) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( Z, T
% 55.54/55.95 , X, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y
% 55.54/55.95 ) }.
% 55.54/55.95 parent0: (101038) {G0,W8,D2,L2,V3,M2} { ! midp( Z, Y, X ), midp( Z, X, Y )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 55.54/55.95 X, Y, T, Z ) }.
% 55.54/55.95 parent0: (101041) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X
% 55.54/55.95 , Y, T, Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 55.54/55.95 X, Z, Y, T ) }.
% 55.54/55.95 parent0: (101042) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X
% 55.54/55.95 , Z, Y, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 55.54/55.95 Y, X, Z, T ) }.
% 55.54/55.95 parent0: (101043) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Y
% 55.54/55.95 , X, Z, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic
% 55.54/55.95 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 55.54/55.95 parent0: (101044) {G0,W15,D2,L3,V5,M3} { ! cyclic( U, X, Y, Z ), ! cyclic
% 55.54/55.95 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 U := U
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 2
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (23) {G0,W10,D2,L2,V4,M2} I { ! cong( X, Y, Z, T ), cong( Z, T
% 55.54/55.95 , X, Y ) }.
% 55.54/55.95 parent0: (101051) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( Z, T
% 55.54/55.95 , X, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X
% 55.54/55.95 , Y, U, W, Z, T, U, W ) }.
% 55.54/55.95 parent0: (101067) {G0,W14,D2,L2,V6,M2} { ! para( X, Y, Z, T ), eqangle( X
% 55.54/55.95 , Y, U, W, Z, T, U, W ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 U := U
% 55.54/55.95 W := W
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T,
% 55.54/55.95 Y ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 55.54/55.95 parent0: (101070) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y
% 55.54/55.95 ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 2
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (63) {G0,W13,D2,L3,V5,M3} I { ! midp( U, X, Y ), ! midp( U, Z
% 55.54/55.95 , T ), para( X, Z, Y, T ) }.
% 55.54/55.95 parent0: (101091) {G0,W13,D2,L3,V5,M3} { ! midp( U, X, Y ), ! midp( U, Z,
% 55.54/55.95 T ), para( X, Z, Y, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 U := U
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 2
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (67) {G0,W13,D2,L3,V3,M3} I { ! cong( X, Y, X, Z ), ! coll( X
% 55.54/55.95 , Y, Z ), midp( X, Y, Z ) }.
% 55.54/55.95 parent0: (101095) {G0,W13,D2,L3,V3,M3} { ! cong( X, Y, X, Z ), ! coll( X,
% 55.54/55.95 Y, Z ), midp( X, Y, Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 2
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (69) {G0,W8,D2,L2,V3,M2} I { ! midp( X, Y, Z ), coll( X, Y, Z
% 55.54/55.95 ) }.
% 55.54/55.95 parent0: (101097) {G0,W8,D2,L2,V3,M2} { ! midp( X, Y, Z ), coll( X, Y, Z )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (88) {G0,W22,D3,L5,V7,M5} I { ! midp( Z, X, Y ), ! midp( W, T
% 55.54/55.95 , U ), ! coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0
% 55.54/55.95 ) }.
% 55.54/55.95 parent0: (101117) {G0,W22,D3,L5,V7,M5} { ! midp( Z, X, Y ), ! midp( W, T,
% 55.54/55.95 U ), ! coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0 )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 U := U
% 55.54/55.95 W := W
% 55.54/55.95 V0 := V0
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 2
% 55.54/55.95 3 ==> 3
% 55.54/55.95 4 ==> 4
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (120) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol27, skol22 )
% 55.54/55.95 }.
% 55.54/55.95 parent0: (101149) {G0,W4,D2,L1,V0,M1} { coll( skol26, skol27, skol22 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (121) {G0,W5,D2,L1,V0,M1} I { cong( skol26, skol27, skol26,
% 55.54/55.95 skol22 ) }.
% 55.54/55.95 parent0: (101150) {G0,W5,D2,L1,V0,M1} { cong( skol26, skol27, skol26,
% 55.54/55.95 skol22 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (122) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol29, skol23 )
% 55.54/55.95 }.
% 55.54/55.95 parent0: (101151) {G0,W4,D2,L1,V0,M1} { coll( skol26, skol29, skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (123) {G0,W5,D2,L1,V0,M1} I { cong( skol26, skol29, skol26,
% 55.54/55.95 skol23 ) }.
% 55.54/55.95 parent0: (101152) {G0,W5,D2,L1,V0,M1} { cong( skol26, skol29, skol26,
% 55.54/55.95 skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (127) {G0,W4,D2,L1,V0,M1} I { coll( skol24, skol26, skol29 )
% 55.54/55.95 }.
% 55.54/55.95 parent0: (101156) {G0,W4,D2,L1,V0,M1} { coll( skol24, skol26, skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (128) {G0,W5,D2,L1,V0,M1} I { ! cyclic( skol20, skol22, skol23
% 55.54/55.95 , skol24 ) }.
% 55.54/55.95 parent0: (101157) {G0,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol22, skol23,
% 55.54/55.95 skol24 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 factor: (101652) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Z, X )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0, 1]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T
% 55.54/55.95 , Z ), coll( Y, Z, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := Z
% 55.54/55.95 T := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (129) {G1,W8,D2,L2,V3,M2} F(2) { ! coll( X, Y, Z ), coll( Z, Z
% 55.54/55.95 , X ) }.
% 55.54/55.95 parent0: (101652) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Z, X )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 factor: (101653) {G0,W18,D3,L4,V4,M4} { ! midp( X, Y, Z ), ! coll( Y, Y, Z
% 55.54/55.95 ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 55.54/55.95 parent0[0, 1]: (88) {G0,W22,D3,L5,V7,M5} I { ! midp( Z, X, Y ), ! midp( W,
% 55.54/55.95 T, U ), ! coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0
% 55.54/55.95 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := X
% 55.54/55.95 T := Y
% 55.54/55.95 U := Z
% 55.54/55.95 W := X
% 55.54/55.95 V0 := T
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (151) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll(
% 55.54/55.95 Y, Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 55.54/55.95 parent0: (101653) {G0,W18,D3,L4,V4,M4} { ! midp( X, Y, Z ), ! coll( Y, Y,
% 55.54/55.95 Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 2
% 55.54/55.95 3 ==> 3
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101656) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol23, skol29 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (122) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol29, skol23 )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol26
% 55.54/55.95 Y := skol29
% 55.54/55.95 Z := skol23
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (166) {G1,W4,D2,L1,V0,M1} R(0,122) { coll( skol26, skol23,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 parent0: (101656) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol23, skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101657) {G1,W4,D2,L1,V0,M1} { coll( skol23, skol26, skol29 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (166) {G1,W4,D2,L1,V0,M1} R(0,122) { coll( skol26, skol23,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol26
% 55.54/55.95 Y := skol23
% 55.54/55.95 Z := skol29
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (174) {G2,W4,D2,L1,V0,M1} R(1,166) { coll( skol23, skol26,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 parent0: (101657) {G1,W4,D2,L1,V0,M1} { coll( skol23, skol26, skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101659) {G1,W8,D2,L2,V3,M2} { coll( X, Z, Y ), ! coll( Y, X,
% 55.54/55.95 Z ) }.
% 55.54/55.95 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent1[1]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (176) {G1,W8,D2,L2,V3,M2} R(1,0) { ! coll( X, Y, Z ), coll( Y
% 55.54/55.95 , Z, X ) }.
% 55.54/55.95 parent0: (101659) {G1,W8,D2,L2,V3,M2} { coll( X, Z, Y ), ! coll( Y, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 1
% 55.54/55.95 1 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101660) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol26, skol23 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (122) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol29, skol23 )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol26
% 55.54/55.95 Y := skol29
% 55.54/55.95 Z := skol23
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (177) {G1,W4,D2,L1,V0,M1} R(1,122) { coll( skol29, skol26,
% 55.54/55.95 skol23 ) }.
% 55.54/55.95 parent0: (101660) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol26, skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101662) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, T
% 55.54/55.95 , X ), ! coll( X, T, Y ) }.
% 55.54/55.95 parent0[1]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 55.54/55.95 ), coll( Y, Z, X ) }.
% 55.54/55.95 parent1[1]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := T
% 55.54/55.95 T := Y
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := T
% 55.54/55.95 Z := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (206) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), coll( Z
% 55.54/55.95 , T, X ), ! coll( X, T, Y ) }.
% 55.54/55.95 parent0: (101662) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, T, X
% 55.54/55.95 ), ! coll( X, T, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 2
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101667) {G1,W12,D2,L3,V4,M3} { coll( X, Z, Y ), ! coll( Z, T
% 55.54/55.95 , X ), ! coll( Z, T, Y ) }.
% 55.54/55.95 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent1[2]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 55.54/55.95 ), coll( Y, Z, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := Z
% 55.54/55.95 Y := X
% 55.54/55.95 Z := Y
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (207) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll
% 55.54/55.95 ( X, Y, T ), coll( Z, X, T ) }.
% 55.54/55.95 parent0: (101667) {G1,W12,D2,L3,V4,M3} { coll( X, Z, Y ), ! coll( Z, T, X
% 55.54/55.95 ), ! coll( Z, T, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Z
% 55.54/55.95 Y := T
% 55.54/55.95 Z := X
% 55.54/55.95 T := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 2
% 55.54/55.95 1 ==> 0
% 55.54/55.95 2 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 factor: (101669) {G1,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0, 1]: (207) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), !
% 55.54/55.95 coll( X, Y, T ), coll( Z, X, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := Z
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (218) {G2,W8,D2,L2,V3,M2} F(207) { ! coll( X, Y, Z ), coll( Z
% 55.54/55.95 , X, Z ) }.
% 55.54/55.95 parent0: (101669) {G1,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101671) {G1,W10,D2,L2,V4,M2} { para( X, Y, T, Z ), ! para( Z
% 55.54/55.95 , T, X, Y ) }.
% 55.54/55.95 parent0[0]: (3) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( X, Y,
% 55.54/55.95 T, Z ) }.
% 55.54/55.95 parent1[1]: (4) {G0,W10,D2,L2,V4,M2} I { ! para( X, Y, Z, T ), para( Z, T,
% 55.54/55.95 X, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := Z
% 55.54/55.95 Y := T
% 55.54/55.95 Z := X
% 55.54/55.95 T := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (243) {G1,W10,D2,L2,V4,M2} R(4,3) { ! para( X, Y, Z, T ), para
% 55.54/55.95 ( Z, T, Y, X ) }.
% 55.54/55.95 parent0: (101671) {G1,W10,D2,L2,V4,M2} { para( X, Y, T, Z ), ! para( Z, T
% 55.54/55.95 , X, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Z
% 55.54/55.95 Y := T
% 55.54/55.95 Z := X
% 55.54/55.95 T := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 1
% 55.54/55.95 1 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101672) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol26, skol22 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (120) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol27, skol22 )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol26
% 55.54/55.95 Y := skol27
% 55.54/55.95 Z := skol22
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (275) {G1,W4,D2,L1,V0,M1} R(120,1) { coll( skol27, skol26,
% 55.54/55.95 skol22 ) }.
% 55.54/55.95 parent0: (101672) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol26, skol22 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101673) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol22, skol27 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (120) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol27, skol22 )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol26
% 55.54/55.95 Y := skol27
% 55.54/55.95 Z := skol22
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (276) {G1,W4,D2,L1,V0,M1} R(120,0) { coll( skol26, skol22,
% 55.54/55.95 skol27 ) }.
% 55.54/55.95 parent0: (101673) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol22, skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101674) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol22, skol26 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (275) {G1,W4,D2,L1,V0,M1} R(120,1) { coll( skol27, skol26,
% 55.54/55.95 skol22 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol27
% 55.54/55.95 Y := skol26
% 55.54/55.95 Z := skol22
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (279) {G2,W4,D2,L1,V0,M1} R(275,0) { coll( skol27, skol22,
% 55.54/55.95 skol26 ) }.
% 55.54/55.95 parent0: (101674) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol22, skol26 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101675) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol27, skol26 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (279) {G2,W4,D2,L1,V0,M1} R(275,0) { coll( skol27, skol22,
% 55.54/55.95 skol26 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol27
% 55.54/55.95 Y := skol22
% 55.54/55.95 Z := skol26
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (282) {G3,W4,D2,L1,V0,M1} R(279,1) { coll( skol22, skol27,
% 55.54/55.95 skol26 ) }.
% 55.54/55.95 parent0: (101675) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol27, skol26 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101676) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol26, skol27 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (282) {G3,W4,D2,L1,V0,M1} R(279,1) { coll( skol22, skol27,
% 55.54/55.95 skol26 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol22
% 55.54/55.95 Y := skol27
% 55.54/55.95 Z := skol26
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (287) {G4,W4,D2,L1,V0,M1} R(282,0) { coll( skol22, skol26,
% 55.54/55.95 skol27 ) }.
% 55.54/55.95 parent0: (101676) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol26, skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101677) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol22,
% 55.54/55.95 skol24, skol23 ) }.
% 55.54/55.95 parent0[0]: (128) {G0,W5,D2,L1,V0,M1} I { ! cyclic( skol20, skol22, skol23
% 55.54/55.95 , skol24 ) }.
% 55.54/55.95 parent1[1]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 55.54/55.95 , Y, T, Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := skol20
% 55.54/55.95 Y := skol22
% 55.54/55.95 Z := skol24
% 55.54/55.95 T := skol23
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (387) {G1,W5,D2,L1,V0,M1} R(13,128) { ! cyclic( skol20, skol22
% 55.54/55.95 , skol24, skol23 ) }.
% 55.54/55.95 parent0: (101677) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol22, skol24,
% 55.54/55.95 skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101679) {G1,W10,D2,L2,V4,M2} { cyclic( X, Y, T, Z ), ! cyclic
% 55.54/55.95 ( X, Z, Y, T ) }.
% 55.54/55.95 parent0[0]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 55.54/55.95 , Y, T, Z ) }.
% 55.54/55.95 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 55.54/55.95 , Z, Y, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := Y
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (401) {G1,W10,D2,L2,V4,M2} R(14,13) { ! cyclic( X, Y, Z, T ),
% 55.54/55.95 cyclic( X, Z, T, Y ) }.
% 55.54/55.95 parent0: (101679) {G1,W10,D2,L2,V4,M2} { cyclic( X, Y, T, Z ), ! cyclic( X
% 55.54/55.95 , Z, Y, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := Y
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 1
% 55.54/55.95 1 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101681) {G1,W10,D2,L2,V4,M2} { cyclic( X, Z, Y, T ), ! cyclic
% 55.54/55.95 ( Y, X, Z, T ) }.
% 55.54/55.95 parent0[0]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 55.54/55.95 , Z, Y, T ) }.
% 55.54/55.95 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 55.54/55.95 , X, Z, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (410) {G1,W10,D2,L2,V4,M2} R(15,14) { ! cyclic( X, Y, Z, T ),
% 55.54/55.95 cyclic( Y, Z, X, T ) }.
% 55.54/55.95 parent0: (101681) {G1,W10,D2,L2,V4,M2} { cyclic( X, Z, Y, T ), ! cyclic( Y
% 55.54/55.95 , X, Z, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 1
% 55.54/55.95 1 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101682) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol20,
% 55.54/55.95 skol24, skol23 ) }.
% 55.54/55.95 parent0[0]: (387) {G1,W5,D2,L1,V0,M1} R(13,128) { ! cyclic( skol20, skol22
% 55.54/55.95 , skol24, skol23 ) }.
% 55.54/55.95 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 55.54/55.95 , X, Z, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := skol22
% 55.54/55.95 Y := skol20
% 55.54/55.95 Z := skol24
% 55.54/55.95 T := skol23
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (411) {G2,W5,D2,L1,V0,M1} R(15,387) { ! cyclic( skol22, skol20
% 55.54/55.95 , skol24, skol23 ) }.
% 55.54/55.95 parent0: (101682) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol20, skol24,
% 55.54/55.95 skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101684) {G1,W15,D2,L3,V5,M3} { ! cyclic( X, Y, Z, T ), cyclic
% 55.54/55.95 ( Y, Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 55.54/55.95 parent0[1]: (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic
% 55.54/55.95 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 55.54/55.95 parent1[1]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 55.54/55.95 , Y, T, Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := T
% 55.54/55.95 T := U
% 55.54/55.95 U := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := U
% 55.54/55.95 T := Z
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (441) {G1,W15,D2,L3,V5,M3} R(16,13) { ! cyclic( X, Y, Z, T ),
% 55.54/55.95 cyclic( Y, Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 55.54/55.95 parent0: (101684) {G1,W15,D2,L3,V5,M3} { ! cyclic( X, Y, Z, T ), cyclic( Y
% 55.54/55.95 , Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 U := U
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 2
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101686) {G1,W10,D2,L2,V1,M2} { ! cyclic( X, skol22, skol20,
% 55.54/55.95 skol24 ), ! cyclic( X, skol22, skol20, skol23 ) }.
% 55.54/55.95 parent0[0]: (411) {G2,W5,D2,L1,V0,M1} R(15,387) { ! cyclic( skol22, skol20
% 55.54/55.95 , skol24, skol23 ) }.
% 55.54/55.95 parent1[2]: (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic
% 55.54/55.95 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := skol22
% 55.54/55.95 Y := skol20
% 55.54/55.95 Z := skol24
% 55.54/55.95 T := skol23
% 55.54/55.95 U := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (466) {G3,W10,D2,L2,V1,M2} R(411,16) { ! cyclic( X, skol22,
% 55.54/55.95 skol20, skol24 ), ! cyclic( X, skol22, skol20, skol23 ) }.
% 55.54/55.95 parent0: (101686) {G1,W10,D2,L2,V1,M2} { ! cyclic( X, skol22, skol20,
% 55.54/55.95 skol24 ), ! cyclic( X, skol22, skol20, skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101687) {G3,W4,D2,L1,V0,M1} { coll( skol27, skol22, skol27 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (218) {G2,W8,D2,L2,V3,M2} F(207) { ! coll( X, Y, Z ), coll( Z,
% 55.54/55.95 X, Z ) }.
% 55.54/55.95 parent1[0]: (287) {G4,W4,D2,L1,V0,M1} R(282,0) { coll( skol22, skol26,
% 55.54/55.95 skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol22
% 55.54/55.95 Y := skol26
% 55.54/55.95 Z := skol27
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (522) {G5,W4,D2,L1,V0,M1} R(218,287) { coll( skol27, skol22,
% 55.54/55.95 skol27 ) }.
% 55.54/55.95 parent0: (101687) {G3,W4,D2,L1,V0,M1} { coll( skol27, skol22, skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101688) {G2,W4,D2,L1,V0,M1} { coll( skol22, skol27, skol22 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (218) {G2,W8,D2,L2,V3,M2} F(207) { ! coll( X, Y, Z ), coll( Z,
% 55.54/55.95 X, Z ) }.
% 55.54/55.95 parent1[0]: (275) {G1,W4,D2,L1,V0,M1} R(120,1) { coll( skol27, skol26,
% 55.54/55.95 skol22 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol27
% 55.54/55.95 Y := skol26
% 55.54/55.95 Z := skol22
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (525) {G3,W4,D2,L1,V0,M1} R(218,275) { coll( skol22, skol27,
% 55.54/55.95 skol22 ) }.
% 55.54/55.95 parent0: (101688) {G2,W4,D2,L1,V0,M1} { coll( skol22, skol27, skol22 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101689) {G2,W4,D2,L1,V0,M1} { coll( skol23, skol29, skol23 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (218) {G2,W8,D2,L2,V3,M2} F(207) { ! coll( X, Y, Z ), coll( Z,
% 55.54/55.95 X, Z ) }.
% 55.54/55.95 parent1[0]: (177) {G1,W4,D2,L1,V0,M1} R(1,122) { coll( skol29, skol26,
% 55.54/55.95 skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol29
% 55.54/55.95 Y := skol26
% 55.54/55.95 Z := skol23
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (532) {G3,W4,D2,L1,V0,M1} R(218,177) { coll( skol23, skol29,
% 55.54/55.95 skol23 ) }.
% 55.54/55.95 parent0: (101689) {G2,W4,D2,L1,V0,M1} { coll( skol23, skol29, skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101690) {G3,W4,D2,L1,V0,M1} { coll( skol29, skol23, skol29 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (218) {G2,W8,D2,L2,V3,M2} F(207) { ! coll( X, Y, Z ), coll( Z,
% 55.54/55.95 X, Z ) }.
% 55.54/55.95 parent1[0]: (174) {G2,W4,D2,L1,V0,M1} R(1,166) { coll( skol23, skol26,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol23
% 55.54/55.95 Y := skol26
% 55.54/55.95 Z := skol29
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (534) {G3,W4,D2,L1,V0,M1} R(218,174) { coll( skol29, skol23,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 parent0: (101690) {G3,W4,D2,L1,V0,M1} { coll( skol29, skol23, skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101691) {G1,W12,D2,L3,V4,M3} { coll( Z, X, Z ), ! coll( Z, T
% 55.54/55.95 , X ), ! coll( Z, T, Y ) }.
% 55.54/55.95 parent0[0]: (218) {G2,W8,D2,L2,V3,M2} F(207) { ! coll( X, Y, Z ), coll( Z,
% 55.54/55.95 X, Z ) }.
% 55.54/55.95 parent1[2]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 55.54/55.95 ), coll( Y, Z, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := Z
% 55.54/55.95 Y := X
% 55.54/55.95 Z := Y
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (539) {G3,W12,D2,L3,V4,M3} R(218,2) { coll( X, Y, X ), ! coll
% 55.54/55.95 ( X, Z, Y ), ! coll( X, Z, T ) }.
% 55.54/55.95 parent0: (101691) {G1,W12,D2,L3,V4,M3} { coll( Z, X, Z ), ! coll( Z, T, X
% 55.54/55.95 ), ! coll( Z, T, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := X
% 55.54/55.95 T := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101693) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol24, skol29 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (218) {G2,W8,D2,L2,V3,M2} F(207) { ! coll( X, Y, Z ), coll( Z,
% 55.54/55.95 X, Z ) }.
% 55.54/55.95 parent1[0]: (127) {G0,W4,D2,L1,V0,M1} I { coll( skol24, skol26, skol29 )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol24
% 55.54/55.95 Y := skol26
% 55.54/55.95 Z := skol29
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (553) {G3,W4,D2,L1,V0,M1} R(218,127) { coll( skol29, skol24,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 parent0: (101693) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol24, skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 factor: (101694) {G3,W8,D2,L2,V3,M2} { coll( X, Y, X ), ! coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent0[1, 2]: (539) {G3,W12,D2,L3,V4,M3} R(218,2) { coll( X, Y, X ), !
% 55.54/55.95 coll( X, Z, Y ), ! coll( X, Z, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (554) {G4,W8,D2,L2,V3,M2} F(539) { coll( X, Y, X ), ! coll( X
% 55.54/55.95 , Z, Y ) }.
% 55.54/55.95 parent0: (101694) {G3,W8,D2,L2,V3,M2} { coll( X, Y, X ), ! coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101695) {G1,W5,D2,L1,V0,M1} { cong( skol26, skol22, skol26,
% 55.54/55.95 skol27 ) }.
% 55.54/55.95 parent0[0]: (23) {G0,W10,D2,L2,V4,M2} I { ! cong( X, Y, Z, T ), cong( Z, T
% 55.54/55.95 , X, Y ) }.
% 55.54/55.95 parent1[0]: (121) {G0,W5,D2,L1,V0,M1} I { cong( skol26, skol27, skol26,
% 55.54/55.95 skol22 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol26
% 55.54/55.95 Y := skol27
% 55.54/55.95 Z := skol26
% 55.54/55.95 T := skol22
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (581) {G1,W5,D2,L1,V0,M1} R(23,121) { cong( skol26, skol22,
% 55.54/55.95 skol26, skol27 ) }.
% 55.54/55.95 parent0: (101695) {G1,W5,D2,L1,V0,M1} { cong( skol26, skol22, skol26,
% 55.54/55.95 skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101696) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol22, skol27 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (525) {G3,W4,D2,L1,V0,M1} R(218,275) { coll( skol22, skol27,
% 55.54/55.95 skol22 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol22
% 55.54/55.95 Y := skol27
% 55.54/55.95 Z := skol22
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (743) {G4,W4,D2,L1,V0,M1} R(525,0) { coll( skol22, skol22,
% 55.54/55.95 skol27 ) }.
% 55.54/55.95 parent0: (101696) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol22, skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101697) {G1,W14,D2,L3,V3,M3} { ! coll( X, X, Z ), cyclic( Y,
% 55.54/55.95 Z, X, X ), ! para( X, Y, X, Y ) }.
% 55.54/55.95 parent0[0]: (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T, Y
% 55.54/55.95 ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 55.54/55.95 parent1[1]: (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X
% 55.54/55.95 , Y, U, W, Z, T, U, W ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := X
% 55.54/55.95 T := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := X
% 55.54/55.95 T := Y
% 55.54/55.95 U := X
% 55.54/55.95 W := Z
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (895) {G1,W14,D2,L3,V3,M3} R(42,39) { ! coll( X, X, Y ),
% 55.54/55.95 cyclic( Z, Y, X, X ), ! para( X, Z, X, Z ) }.
% 55.54/55.95 parent0: (101697) {G1,W14,D2,L3,V3,M3} { ! coll( X, X, Z ), cyclic( Y, Z,
% 55.54/55.95 X, X ), ! para( X, Y, X, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 2
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101698) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol29, skol23 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (534) {G3,W4,D2,L1,V0,M1} R(218,174) { coll( skol29, skol23,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol29
% 55.54/55.95 Y := skol23
% 55.54/55.95 Z := skol29
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (1060) {G4,W4,D2,L1,V0,M1} R(534,0) { coll( skol29, skol29,
% 55.54/55.95 skol23 ) }.
% 55.54/55.95 parent0: (101698) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol29, skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101699) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol29, skol24 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (553) {G3,W4,D2,L1,V0,M1} R(218,127) { coll( skol29, skol24,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol29
% 55.54/55.95 Y := skol24
% 55.54/55.95 Z := skol29
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (1746) {G4,W4,D2,L1,V0,M1} R(553,0) { coll( skol29, skol29,
% 55.54/55.95 skol24 ) }.
% 55.54/55.95 parent0: (101699) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol29, skol24 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101700) {G1,W8,D2,L2,V1,M2} { ! coll( skol29, skol29, X ),
% 55.54/55.95 coll( skol24, X, skol29 ) }.
% 55.54/55.95 parent0[0]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 55.54/55.95 ), coll( Y, Z, X ) }.
% 55.54/55.95 parent1[0]: (1746) {G4,W4,D2,L1,V0,M1} R(553,0) { coll( skol29, skol29,
% 55.54/55.95 skol24 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol29
% 55.54/55.95 Y := skol24
% 55.54/55.95 Z := X
% 55.54/55.95 T := skol29
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (1754) {G5,W8,D2,L2,V1,M2} R(1746,2) { ! coll( skol29, skol29
% 55.54/55.95 , X ), coll( skol24, X, skol29 ) }.
% 55.54/55.95 parent0: (101700) {G1,W8,D2,L2,V1,M2} { ! coll( skol29, skol29, X ), coll
% 55.54/55.95 ( skol24, X, skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101703) {G1,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( X, Z,
% 55.54/55.95 Y ) }.
% 55.54/55.95 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (554) {G4,W8,D2,L2,V3,M2} F(539) { coll( X, Y, X ), ! coll( X,
% 55.54/55.95 Z, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (1985) {G5,W8,D2,L2,V3,M2} R(554,1) { ! coll( X, Y, Z ), coll
% 55.54/55.95 ( Z, X, X ) }.
% 55.54/55.95 parent0: (101703) {G1,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 1
% 55.54/55.95 1 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101704) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( X, Z,
% 55.54/55.95 Y ) }.
% 55.54/55.95 parent0[0]: (1985) {G5,W8,D2,L2,V3,M2} R(554,1) { ! coll( X, Y, Z ), coll(
% 55.54/55.95 Z, X, X ) }.
% 55.54/55.95 parent1[1]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (1992) {G6,W8,D2,L2,V3,M2} R(1985,0) { coll( X, Y, Y ), ! coll
% 55.54/55.95 ( Y, X, Z ) }.
% 55.54/55.95 parent0: (101704) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( X, Z, Y )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101705) {G7,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! coll( X, Y,
% 55.54/55.95 Z ) }.
% 55.54/55.95 parent0[1]: (1992) {G6,W8,D2,L2,V3,M2} R(1985,0) { coll( X, Y, Y ), ! coll
% 55.54/55.95 ( Y, X, Z ) }.
% 55.54/55.95 parent1[0]: (1992) {G6,W8,D2,L2,V3,M2} R(1985,0) { coll( X, Y, Y ), ! coll
% 55.54/55.95 ( Y, X, Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (2007) {G7,W8,D2,L2,V3,M2} R(1992,1992) { ! coll( X, Y, Z ),
% 55.54/55.95 coll( X, Y, Y ) }.
% 55.54/55.95 parent0: (101705) {G7,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! coll( X, Y, Z )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 1
% 55.54/55.95 1 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101709) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, Y
% 55.54/55.95 , X ), ! coll( X, Y, T ) }.
% 55.54/55.95 parent0[1]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 55.54/55.95 ), coll( Y, Z, X ) }.
% 55.54/55.95 parent1[1]: (2007) {G7,W8,D2,L2,V3,M2} R(1992,1992) { ! coll( X, Y, Z ),
% 55.54/55.95 coll( X, Y, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := Y
% 55.54/55.95 T := Y
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := T
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (2012) {G8,W12,D2,L3,V4,M3} R(2007,2) { ! coll( X, Y, Z ), !
% 55.54/55.95 coll( X, Y, T ), coll( T, Y, X ) }.
% 55.54/55.95 parent0: (101709) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, Y, X
% 55.54/55.95 ), ! coll( X, Y, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := T
% 55.54/55.95 T := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 1
% 55.54/55.95 1 ==> 2
% 55.54/55.95 2 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 factor: (101712) {G8,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0, 1]: (2012) {G8,W12,D2,L3,V4,M3} R(2007,2) { ! coll( X, Y, Z ), !
% 55.54/55.95 coll( X, Y, T ), coll( T, Y, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := Z
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (2013) {G9,W8,D2,L2,V3,M2} F(2012) { ! coll( X, Y, Z ), coll(
% 55.54/55.95 Z, Y, X ) }.
% 55.54/55.95 parent0: (101712) {G8,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101714) {G1,W13,D2,L3,V5,M3} { ! midp( X, Y, Z ), para( Y, T
% 55.54/55.95 , Z, U ), ! midp( X, U, T ) }.
% 55.54/55.95 parent0[1]: (63) {G0,W13,D2,L3,V5,M3} I { ! midp( U, X, Y ), ! midp( U, Z,
% 55.54/55.95 T ), para( X, Z, Y, T ) }.
% 55.54/55.95 parent1[1]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := T
% 55.54/55.95 T := U
% 55.54/55.95 U := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := T
% 55.54/55.95 Y := U
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (2125) {G1,W13,D2,L3,V5,M3} R(63,10) { ! midp( X, Y, Z ), para
% 55.54/55.95 ( Y, T, Z, U ), ! midp( X, U, T ) }.
% 55.54/55.95 parent0: (101714) {G1,W13,D2,L3,V5,M3} { ! midp( X, Y, Z ), para( Y, T, Z
% 55.54/55.95 , U ), ! midp( X, U, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 U := U
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 2 ==> 2
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 factor: (101717) {G1,W9,D2,L2,V3,M2} { ! midp( X, Y, Z ), para( Y, Z, Z, Y
% 55.54/55.95 ) }.
% 55.54/55.95 parent0[0, 2]: (2125) {G1,W13,D2,L3,V5,M3} R(63,10) { ! midp( X, Y, Z ),
% 55.54/55.95 para( Y, T, Z, U ), ! midp( X, U, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := Z
% 55.54/55.95 U := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (2135) {G2,W9,D2,L2,V3,M2} F(2125) { ! midp( X, Y, Z ), para(
% 55.54/55.95 Y, Z, Z, Y ) }.
% 55.54/55.95 parent0: (101717) {G1,W9,D2,L2,V3,M2} { ! midp( X, Y, Z ), para( Y, Z, Z,
% 55.54/55.95 Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101718) {G1,W8,D2,L2,V3,M2} { coll( Y, X, Z ), ! midp( X, Y,
% 55.54/55.95 Z ) }.
% 55.54/55.95 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 55.54/55.95 }.
% 55.54/55.95 parent1[1]: (69) {G0,W8,D2,L2,V3,M2} I { ! midp( X, Y, Z ), coll( X, Y, Z )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (2166) {G1,W8,D2,L2,V3,M2} R(69,1) { ! midp( X, Y, Z ), coll(
% 55.54/55.95 Y, X, Z ) }.
% 55.54/55.95 parent0: (101718) {G1,W8,D2,L2,V3,M2} { coll( Y, X, Z ), ! midp( X, Y, Z )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 1
% 55.54/55.95 1 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101719) {G1,W8,D2,L2,V0,M2} { ! coll( skol26, skol22, skol27
% 55.54/55.95 ), midp( skol26, skol22, skol27 ) }.
% 55.54/55.95 parent0[0]: (67) {G0,W13,D2,L3,V3,M3} I { ! cong( X, Y, X, Z ), ! coll( X,
% 55.54/55.95 Y, Z ), midp( X, Y, Z ) }.
% 55.54/55.95 parent1[0]: (581) {G1,W5,D2,L1,V0,M1} R(23,121) { cong( skol26, skol22,
% 55.54/55.95 skol26, skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol26
% 55.54/55.95 Y := skol22
% 55.54/55.95 Z := skol27
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101720) {G2,W4,D2,L1,V0,M1} { midp( skol26, skol22, skol27 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (101719) {G1,W8,D2,L2,V0,M2} { ! coll( skol26, skol22, skol27
% 55.54/55.95 ), midp( skol26, skol22, skol27 ) }.
% 55.54/55.95 parent1[0]: (276) {G1,W4,D2,L1,V0,M1} R(120,0) { coll( skol26, skol22,
% 55.54/55.95 skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (2373) {G2,W4,D2,L1,V0,M1} R(67,581);r(276) { midp( skol26,
% 55.54/55.95 skol22, skol27 ) }.
% 55.54/55.95 parent0: (101720) {G2,W4,D2,L1,V0,M1} { midp( skol26, skol22, skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101721) {G1,W8,D2,L2,V0,M2} { ! coll( skol26, skol29, skol23
% 55.54/55.95 ), midp( skol26, skol29, skol23 ) }.
% 55.54/55.95 parent0[0]: (67) {G0,W13,D2,L3,V3,M3} I { ! cong( X, Y, X, Z ), ! coll( X,
% 55.54/55.95 Y, Z ), midp( X, Y, Z ) }.
% 55.54/55.95 parent1[0]: (123) {G0,W5,D2,L1,V0,M1} I { cong( skol26, skol29, skol26,
% 55.54/55.95 skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol26
% 55.54/55.95 Y := skol29
% 55.54/55.95 Z := skol23
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101722) {G1,W4,D2,L1,V0,M1} { midp( skol26, skol29, skol23 )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (101721) {G1,W8,D2,L2,V0,M2} { ! coll( skol26, skol29, skol23
% 55.54/55.95 ), midp( skol26, skol29, skol23 ) }.
% 55.54/55.95 parent1[0]: (122) {G0,W4,D2,L1,V0,M1} I { coll( skol26, skol29, skol23 )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (2517) {G1,W4,D2,L1,V0,M1} R(67,123);r(122) { midp( skol26,
% 55.54/55.95 skol29, skol23 ) }.
% 55.54/55.95 parent0: (101722) {G1,W4,D2,L1,V0,M1} { midp( skol26, skol29, skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101723) {G2,W8,D2,L2,V2,M2} { coll( skol24, X, skol29 ), !
% 55.54/55.95 coll( X, Y, skol29 ) }.
% 55.54/55.95 parent0[0]: (1754) {G5,W8,D2,L2,V1,M2} R(1746,2) { ! coll( skol29, skol29,
% 55.54/55.95 X ), coll( skol24, X, skol29 ) }.
% 55.54/55.95 parent1[1]: (129) {G1,W8,D2,L2,V3,M2} F(2) { ! coll( X, Y, Z ), coll( Z, Z
% 55.54/55.95 , X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := skol29
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (2739) {G6,W8,D2,L2,V2,M2} R(1754,129) { coll( skol24, X,
% 55.54/55.95 skol29 ), ! coll( X, Y, skol29 ) }.
% 55.54/55.95 parent0: (101723) {G2,W8,D2,L2,V2,M2} { coll( skol24, X, skol29 ), ! coll
% 55.54/55.95 ( X, Y, skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101725) {G2,W8,D2,L2,V2,M2} { coll( X, skol29, skol24 ), !
% 55.54/55.95 coll( X, Y, skol29 ) }.
% 55.54/55.95 parent0[0]: (176) {G1,W8,D2,L2,V3,M2} R(1,0) { ! coll( X, Y, Z ), coll( Y,
% 55.54/55.95 Z, X ) }.
% 55.54/55.95 parent1[0]: (2739) {G6,W8,D2,L2,V2,M2} R(1754,129) { coll( skol24, X,
% 55.54/55.95 skol29 ), ! coll( X, Y, skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol24
% 55.54/55.95 Y := X
% 55.54/55.95 Z := skol29
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (3216) {G7,W8,D2,L2,V2,M2} R(2739,176) { ! coll( X, Y, skol29
% 55.54/55.95 ), coll( X, skol29, skol24 ) }.
% 55.54/55.95 parent0: (101725) {G2,W8,D2,L2,V2,M2} { coll( X, skol29, skol24 ), ! coll
% 55.54/55.95 ( X, Y, skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 1
% 55.54/55.95 1 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101726) {G2,W8,D2,L2,V2,M2} { coll( X, skol29, skol24 ), !
% 55.54/55.95 coll( skol29, Y, X ) }.
% 55.54/55.95 parent0[0]: (3216) {G7,W8,D2,L2,V2,M2} R(2739,176) { ! coll( X, Y, skol29 )
% 55.54/55.95 , coll( X, skol29, skol24 ) }.
% 55.54/55.95 parent1[1]: (129) {G1,W8,D2,L2,V3,M2} F(2) { ! coll( X, Y, Z ), coll( Z, Z
% 55.54/55.95 , X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := skol29
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (3264) {G8,W8,D2,L2,V2,M2} R(3216,129) { coll( X, skol29,
% 55.54/55.95 skol24 ), ! coll( skol29, Y, X ) }.
% 55.54/55.95 parent0: (101726) {G2,W8,D2,L2,V2,M2} { coll( X, skol29, skol24 ), ! coll
% 55.54/55.95 ( skol29, Y, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101728) {G2,W8,D2,L2,V2,M2} { coll( skol29, skol24, X ), !
% 55.54/55.95 coll( skol29, Y, X ) }.
% 55.54/55.95 parent0[0]: (176) {G1,W8,D2,L2,V3,M2} R(1,0) { ! coll( X, Y, Z ), coll( Y,
% 55.54/55.95 Z, X ) }.
% 55.54/55.95 parent1[0]: (3264) {G8,W8,D2,L2,V2,M2} R(3216,129) { coll( X, skol29,
% 55.54/55.95 skol24 ), ! coll( skol29, Y, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := skol29
% 55.54/55.95 Z := skol24
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (3283) {G9,W8,D2,L2,V2,M2} R(3264,176) { ! coll( skol29, X, Y
% 55.54/55.95 ), coll( skol29, skol24, Y ) }.
% 55.54/55.95 parent0: (101728) {G2,W8,D2,L2,V2,M2} { coll( skol29, skol24, X ), ! coll
% 55.54/55.95 ( skol29, Y, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 1
% 55.54/55.95 1 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101729) {G2,W8,D2,L2,V2,M2} { coll( skol29, skol24, Y ), !
% 55.54/55.95 midp( X, skol29, Y ) }.
% 55.54/55.95 parent0[0]: (3283) {G9,W8,D2,L2,V2,M2} R(3264,176) { ! coll( skol29, X, Y )
% 55.54/55.95 , coll( skol29, skol24, Y ) }.
% 55.54/55.95 parent1[1]: (2166) {G1,W8,D2,L2,V3,M2} R(69,1) { ! midp( X, Y, Z ), coll( Y
% 55.54/55.95 , X, Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := skol29
% 55.54/55.95 Z := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (4424) {G10,W8,D2,L2,V2,M2} R(3283,2166) { coll( skol29,
% 55.54/55.95 skol24, X ), ! midp( Y, skol29, X ) }.
% 55.54/55.95 parent0: (101729) {G2,W8,D2,L2,V2,M2} { coll( skol29, skol24, Y ), ! midp
% 55.54/55.95 ( X, skol29, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101730) {G10,W8,D2,L2,V2,M2} { coll( X, skol24, skol29 ), !
% 55.54/55.95 midp( Y, skol29, X ) }.
% 55.54/55.95 parent0[0]: (2013) {G9,W8,D2,L2,V3,M2} F(2012) { ! coll( X, Y, Z ), coll( Z
% 55.54/55.95 , Y, X ) }.
% 55.54/55.95 parent1[0]: (4424) {G10,W8,D2,L2,V2,M2} R(3283,2166) { coll( skol29, skol24
% 55.54/55.95 , X ), ! midp( Y, skol29, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol29
% 55.54/55.95 Y := skol24
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (4497) {G11,W8,D2,L2,V2,M2} R(4424,2013) { ! midp( X, skol29,
% 55.54/55.95 Y ), coll( Y, skol24, skol29 ) }.
% 55.54/55.95 parent0: (101730) {G10,W8,D2,L2,V2,M2} { coll( X, skol24, skol29 ), ! midp
% 55.54/55.95 ( Y, skol29, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 1
% 55.54/55.95 1 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101731) {G2,W14,D3,L3,V1,M3} { ! coll( skol29, skol29, skol23
% 55.54/55.95 ), ! coll( skol23, skol29, skol23 ), midp( skol7( skol29, X ), skol29, X
% 55.54/55.95 ) }.
% 55.54/55.95 parent0[0]: (151) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y
% 55.54/55.95 , Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 55.54/55.95 parent1[0]: (2517) {G1,W4,D2,L1,V0,M1} R(67,123);r(122) { midp( skol26,
% 55.54/55.95 skol29, skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol26
% 55.54/55.95 Y := skol29
% 55.54/55.95 Z := skol23
% 55.54/55.95 T := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101732) {G3,W10,D3,L2,V1,M2} { ! coll( skol23, skol29, skol23
% 55.54/55.95 ), midp( skol7( skol29, X ), skol29, X ) }.
% 55.54/55.95 parent0[0]: (101731) {G2,W14,D3,L3,V1,M3} { ! coll( skol29, skol29, skol23
% 55.54/55.95 ), ! coll( skol23, skol29, skol23 ), midp( skol7( skol29, X ), skol29, X
% 55.54/55.95 ) }.
% 55.54/55.95 parent1[0]: (1060) {G4,W4,D2,L1,V0,M1} R(534,0) { coll( skol29, skol29,
% 55.54/55.95 skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (8457) {G5,W10,D3,L2,V1,M2} R(151,2517);r(1060) { ! coll(
% 55.54/55.95 skol23, skol29, skol23 ), midp( skol7( skol29, X ), skol29, X ) }.
% 55.54/55.95 parent0: (101732) {G3,W10,D3,L2,V1,M2} { ! coll( skol23, skol29, skol23 )
% 55.54/55.95 , midp( skol7( skol29, X ), skol29, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101733) {G2,W14,D3,L3,V1,M3} { ! coll( skol22, skol22, skol27
% 55.54/55.95 ), ! coll( skol27, skol22, skol27 ), midp( skol7( skol22, X ), skol22, X
% 55.54/55.95 ) }.
% 55.54/55.95 parent0[0]: (151) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y
% 55.54/55.95 , Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 55.54/55.95 parent1[0]: (2373) {G2,W4,D2,L1,V0,M1} R(67,581);r(276) { midp( skol26,
% 55.54/55.95 skol22, skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol26
% 55.54/55.95 Y := skol22
% 55.54/55.95 Z := skol27
% 55.54/55.95 T := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101734) {G3,W10,D3,L2,V1,M2} { ! coll( skol27, skol22, skol27
% 55.54/55.95 ), midp( skol7( skol22, X ), skol22, X ) }.
% 55.54/55.95 parent0[0]: (101733) {G2,W14,D3,L3,V1,M3} { ! coll( skol22, skol22, skol27
% 55.54/55.95 ), ! coll( skol27, skol22, skol27 ), midp( skol7( skol22, X ), skol22, X
% 55.54/55.95 ) }.
% 55.54/55.95 parent1[0]: (743) {G4,W4,D2,L1,V0,M1} R(525,0) { coll( skol22, skol22,
% 55.54/55.95 skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (8459) {G5,W10,D3,L2,V1,M2} R(151,2373);r(743) { ! coll(
% 55.54/55.95 skol27, skol22, skol27 ), midp( skol7( skol22, X ), skol22, X ) }.
% 55.54/55.95 parent0: (101734) {G3,W10,D3,L2,V1,M2} { ! coll( skol27, skol22, skol27 )
% 55.54/55.95 , midp( skol7( skol22, X ), skol22, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101735) {G4,W6,D3,L1,V1,M1} { midp( skol7( skol29, X ),
% 55.54/55.95 skol29, X ) }.
% 55.54/55.95 parent0[0]: (8457) {G5,W10,D3,L2,V1,M2} R(151,2517);r(1060) { ! coll(
% 55.54/55.95 skol23, skol29, skol23 ), midp( skol7( skol29, X ), skol29, X ) }.
% 55.54/55.95 parent1[0]: (532) {G3,W4,D2,L1,V0,M1} R(218,177) { coll( skol23, skol29,
% 55.54/55.95 skol23 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (20056) {G6,W6,D3,L1,V1,M1} S(8457);r(532) { midp( skol7(
% 55.54/55.95 skol29, X ), skol29, X ) }.
% 55.54/55.95 parent0: (101735) {G4,W6,D3,L1,V1,M1} { midp( skol7( skol29, X ), skol29,
% 55.54/55.95 X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101736) {G6,W6,D3,L1,V1,M1} { midp( skol7( skol22, X ),
% 55.54/55.95 skol22, X ) }.
% 55.54/55.95 parent0[0]: (8459) {G5,W10,D3,L2,V1,M2} R(151,2373);r(743) { ! coll( skol27
% 55.54/55.95 , skol22, skol27 ), midp( skol7( skol22, X ), skol22, X ) }.
% 55.54/55.95 parent1[0]: (522) {G5,W4,D2,L1,V0,M1} R(218,287) { coll( skol27, skol22,
% 55.54/55.95 skol27 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (20058) {G6,W6,D3,L1,V1,M1} S(8459);r(522) { midp( skol7(
% 55.54/55.95 skol22, X ), skol22, X ) }.
% 55.54/55.95 parent0: (101736) {G6,W6,D3,L1,V1,M1} { midp( skol7( skol22, X ), skol22,
% 55.54/55.95 X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101737) {G7,W4,D2,L1,V1,M1} { coll( X, skol24, skol29 ) }.
% 55.54/55.95 parent0[0]: (4497) {G11,W8,D2,L2,V2,M2} R(4424,2013) { ! midp( X, skol29, Y
% 55.54/55.95 ), coll( Y, skol24, skol29 ) }.
% 55.54/55.95 parent1[0]: (20056) {G6,W6,D3,L1,V1,M1} S(8457);r(532) { midp( skol7(
% 55.54/55.95 skol29, X ), skol29, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol7( skol29, X )
% 55.54/55.95 Y := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (30423) {G12,W4,D2,L1,V1,M1} R(20056,4497) { coll( X, skol24,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 parent0: (101737) {G7,W4,D2,L1,V1,M1} { coll( X, skol24, skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101738) {G7,W4,D2,L1,V1,M1} { coll( skol24, X, skol29 ) }.
% 55.54/55.95 parent0[1]: (2739) {G6,W8,D2,L2,V2,M2} R(1754,129) { coll( skol24, X,
% 55.54/55.95 skol29 ), ! coll( X, Y, skol29 ) }.
% 55.54/55.95 parent1[0]: (30423) {G12,W4,D2,L1,V1,M1} R(20056,4497) { coll( X, skol24,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := skol24
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (30493) {G13,W4,D2,L1,V1,M1} R(30423,2739) { coll( skol24, X,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 parent0: (101738) {G7,W4,D2,L1,V1,M1} { coll( skol24, X, skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101739) {G2,W4,D2,L1,V1,M1} { coll( skol24, skol29, X ) }.
% 55.54/55.95 parent0[0]: (176) {G1,W8,D2,L2,V3,M2} R(1,0) { ! coll( X, Y, Z ), coll( Y,
% 55.54/55.95 Z, X ) }.
% 55.54/55.95 parent1[0]: (30423) {G12,W4,D2,L1,V1,M1} R(20056,4497) { coll( X, skol24,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := skol24
% 55.54/55.95 Z := skol29
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (30495) {G13,W4,D2,L1,V1,M1} R(30423,176) { coll( skol24,
% 55.54/55.95 skol29, X ) }.
% 55.54/55.95 parent0: (101739) {G2,W4,D2,L1,V1,M1} { coll( skol24, skol29, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101741) {G2,W8,D2,L2,V2,M2} { ! coll( skol24, skol29, X ),
% 55.54/55.95 coll( X, Y, skol24 ) }.
% 55.54/55.95 parent0[2]: (206) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), coll( Z
% 55.54/55.95 , T, X ), ! coll( X, T, Y ) }.
% 55.54/55.95 parent1[0]: (30493) {G13,W4,D2,L1,V1,M1} R(30423,2739) { coll( skol24, X,
% 55.54/55.95 skol29 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol24
% 55.54/55.95 Y := skol29
% 55.54/55.95 Z := X
% 55.54/55.95 T := Y
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101742) {G3,W4,D2,L1,V2,M1} { coll( X, Y, skol24 ) }.
% 55.54/55.95 parent0[0]: (101741) {G2,W8,D2,L2,V2,M2} { ! coll( skol24, skol29, X ),
% 55.54/55.95 coll( X, Y, skol24 ) }.
% 55.54/55.95 parent1[0]: (30495) {G13,W4,D2,L1,V1,M1} R(30423,176) { coll( skol24,
% 55.54/55.95 skol29, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (30515) {G14,W4,D2,L1,V2,M1} R(30493,206);r(30495) { coll( X,
% 55.54/55.95 Y, skol24 ) }.
% 55.54/55.95 parent0: (101742) {G3,W4,D2,L1,V2,M1} { coll( X, Y, skol24 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101743) {G2,W4,D2,L1,V2,M1} { coll( Y, skol24, X ) }.
% 55.54/55.95 parent0[0]: (176) {G1,W8,D2,L2,V3,M2} R(1,0) { ! coll( X, Y, Z ), coll( Y,
% 55.54/55.95 Z, X ) }.
% 55.54/55.95 parent1[0]: (30515) {G14,W4,D2,L1,V2,M1} R(30493,206);r(30495) { coll( X, Y
% 55.54/55.95 , skol24 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := skol24
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (30579) {G15,W4,D2,L1,V2,M1} R(30515,176) { coll( X, skol24, Y
% 55.54/55.95 ) }.
% 55.54/55.95 parent0: (101743) {G2,W4,D2,L1,V2,M1} { coll( Y, skol24, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101744) {G2,W8,D2,L2,V3,M2} { ! coll( X, skol24, Z ), coll( Y
% 55.54/55.95 , X, Z ) }.
% 55.54/55.95 parent0[0]: (207) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll(
% 55.54/55.95 X, Y, T ), coll( Z, X, T ) }.
% 55.54/55.95 parent1[0]: (30579) {G15,W4,D2,L1,V2,M1} R(30515,176) { coll( X, skol24, Y
% 55.54/55.95 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := skol24
% 55.54/55.95 Z := Y
% 55.54/55.95 T := Z
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101746) {G3,W4,D2,L1,V3,M1} { coll( Z, X, Y ) }.
% 55.54/55.95 parent0[0]: (101744) {G2,W8,D2,L2,V3,M2} { ! coll( X, skol24, Z ), coll( Y
% 55.54/55.95 , X, Z ) }.
% 55.54/55.95 parent1[0]: (30579) {G15,W4,D2,L1,V2,M1} R(30515,176) { coll( X, skol24, Y
% 55.54/55.95 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := Y
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (30591) {G16,W4,D2,L1,V3,M1} R(30579,207);r(30579) { coll( Z,
% 55.54/55.95 X, Y ) }.
% 55.54/55.95 parent0: (101746) {G3,W4,D2,L1,V3,M1} { coll( Z, X, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101747) {G1,W6,D3,L1,V1,M1} { midp( skol7( skol22, X ), X,
% 55.54/55.95 skol22 ) }.
% 55.54/55.95 parent0[0]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (20058) {G6,W6,D3,L1,V1,M1} S(8459);r(522) { midp( skol7(
% 55.54/55.95 skol22, X ), skol22, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := skol22
% 55.54/55.95 Z := skol7( skol22, X )
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (31010) {G7,W6,D3,L1,V1,M1} R(20058,10) { midp( skol7( skol22
% 55.54/55.95 , X ), X, skol22 ) }.
% 55.54/55.95 parent0: (101747) {G1,W6,D3,L1,V1,M1} { midp( skol7( skol22, X ), X,
% 55.54/55.95 skol22 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101748) {G2,W14,D3,L3,V2,M3} { ! coll( X, X, skol22 ), ! coll
% 55.54/55.95 ( skol22, X, skol22 ), midp( skol7( X, Y ), X, Y ) }.
% 55.54/55.95 parent0[0]: (151) {G1,W18,D3,L4,V4,M4} F(88) { ! midp( X, Y, Z ), ! coll( Y
% 55.54/55.95 , Y, Z ), ! coll( Z, Y, Z ), midp( skol7( Y, T ), Y, T ) }.
% 55.54/55.95 parent1[0]: (31010) {G7,W6,D3,L1,V1,M1} R(20058,10) { midp( skol7( skol22,
% 55.54/55.95 X ), X, skol22 ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol7( skol22, X )
% 55.54/55.95 Y := X
% 55.54/55.95 Z := skol22
% 55.54/55.95 T := Y
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101751) {G3,W10,D3,L2,V2,M2} { ! coll( skol22, X, skol22 ),
% 55.54/55.95 midp( skol7( X, Y ), X, Y ) }.
% 55.54/55.95 parent0[0]: (101748) {G2,W14,D3,L3,V2,M3} { ! coll( X, X, skol22 ), ! coll
% 55.54/55.95 ( skol22, X, skol22 ), midp( skol7( X, Y ), X, Y ) }.
% 55.54/55.95 parent1[0]: (30591) {G16,W4,D2,L1,V3,M1} R(30579,207);r(30579) { coll( Z, X
% 55.54/55.95 , Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := skol22
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (31054) {G17,W10,D3,L2,V2,M2} R(31010,151);r(30591) { ! coll(
% 55.54/55.95 skol22, X, skol22 ), midp( skol7( X, Y ), X, Y ) }.
% 55.54/55.95 parent0: (101751) {G3,W10,D3,L2,V2,M2} { ! coll( skol22, X, skol22 ), midp
% 55.54/55.95 ( skol7( X, Y ), X, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101753) {G17,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), X, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent0[0]: (31054) {G17,W10,D3,L2,V2,M2} R(31010,151);r(30591) { ! coll(
% 55.54/55.95 skol22, X, skol22 ), midp( skol7( X, Y ), X, Y ) }.
% 55.54/55.95 parent1[0]: (30591) {G16,W4,D2,L1,V3,M1} R(30579,207);r(30579) { coll( Z, X
% 55.54/55.95 , Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := skol22
% 55.54/55.95 Z := skol22
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (40120) {G18,W6,D3,L1,V2,M1} S(31054);r(30591) { midp( skol7(
% 55.54/55.95 X, Y ), X, Y ) }.
% 55.54/55.95 parent0: (101753) {G17,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), X, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101754) {G2,W10,D2,L2,V3,M2} { cyclic( Z, Y, X, X ), ! para(
% 55.54/55.95 X, Z, X, Z ) }.
% 55.54/55.95 parent0[0]: (895) {G1,W14,D2,L3,V3,M3} R(42,39) { ! coll( X, X, Y ), cyclic
% 55.54/55.95 ( Z, Y, X, X ), ! para( X, Z, X, Z ) }.
% 55.54/55.95 parent1[0]: (30591) {G16,W4,D2,L1,V3,M1} R(30579,207);r(30579) { coll( Z, X
% 55.54/55.95 , Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (40280) {G17,W10,D2,L2,V3,M2} S(895);r(30591) { cyclic( Z, Y,
% 55.54/55.95 X, X ), ! para( X, Z, X, Z ) }.
% 55.54/55.95 parent0: (101754) {G2,W10,D2,L2,V3,M2} { cyclic( Z, Y, X, X ), ! para( X,
% 55.54/55.95 Z, X, Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 1 ==> 1
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101755) {G1,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), Y, X ) }.
% 55.54/55.95 parent0[0]: (10) {G0,W8,D2,L2,V3,M2} I { ! midp( Z, Y, X ), midp( Z, X, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent1[0]: (40120) {G18,W6,D3,L1,V2,M1} S(31054);r(30591) { midp( skol7( X
% 55.54/55.95 , Y ), X, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 Z := skol7( X, Y )
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (41382) {G19,W6,D3,L1,V2,M1} R(40120,10) { midp( skol7( X, Y )
% 55.54/55.95 , Y, X ) }.
% 55.54/55.95 parent0: (101755) {G1,W6,D3,L1,V2,M1} { midp( skol7( X, Y ), Y, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101756) {G3,W5,D2,L1,V2,M1} { para( Y, X, X, Y ) }.
% 55.54/55.95 parent0[0]: (2135) {G2,W9,D2,L2,V3,M2} F(2125) { ! midp( X, Y, Z ), para( Y
% 55.54/55.95 , Z, Z, Y ) }.
% 55.54/55.95 parent1[0]: (41382) {G19,W6,D3,L1,V2,M1} R(40120,10) { midp( skol7( X, Y )
% 55.54/55.95 , Y, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol7( X, Y )
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (82798) {G20,W5,D2,L1,V2,M1} R(2135,41382) { para( X, Y, Y, X
% 55.54/55.95 ) }.
% 55.54/55.95 parent0: (101756) {G3,W5,D2,L1,V2,M1} { para( Y, X, X, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101757) {G2,W5,D2,L1,V2,M1} { para( Y, X, Y, X ) }.
% 55.54/55.95 parent0[0]: (243) {G1,W10,D2,L2,V4,M2} R(4,3) { ! para( X, Y, Z, T ), para
% 55.54/55.95 ( Z, T, Y, X ) }.
% 55.54/55.95 parent1[0]: (82798) {G20,W5,D2,L1,V2,M1} R(2135,41382) { para( X, Y, Y, X )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Y
% 55.54/55.95 T := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (82811) {G21,W5,D2,L1,V2,M1} R(82798,243) { para( X, Y, X, Y )
% 55.54/55.95 }.
% 55.54/55.95 parent0: (101757) {G2,W5,D2,L1,V2,M1} { para( Y, X, Y, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Y
% 55.54/55.95 Y := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101758) {G18,W5,D2,L1,V3,M1} { cyclic( X, Y, Z, Z ) }.
% 55.54/55.95 parent0[1]: (40280) {G17,W10,D2,L2,V3,M2} S(895);r(30591) { cyclic( Z, Y, X
% 55.54/55.95 , X ), ! para( X, Z, X, Z ) }.
% 55.54/55.95 parent1[0]: (82811) {G21,W5,D2,L1,V2,M1} R(82798,243) { para( X, Y, X, Y )
% 55.54/55.95 }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Z
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := Z
% 55.54/55.95 Y := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (100879) {G22,W5,D2,L1,V3,M1} S(40280);r(82811) { cyclic( Z, Y
% 55.54/55.95 , X, X ) }.
% 55.54/55.95 parent0: (101758) {G18,W5,D2,L1,V3,M1} { cyclic( X, Y, Z, Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Z
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101759) {G2,W5,D2,L1,V3,M1} { cyclic( Y, Z, X, Z ) }.
% 55.54/55.95 parent0[0]: (410) {G1,W10,D2,L2,V4,M2} R(15,14) { ! cyclic( X, Y, Z, T ),
% 55.54/55.95 cyclic( Y, Z, X, T ) }.
% 55.54/55.95 parent1[0]: (100879) {G22,W5,D2,L1,V3,M1} S(40280);r(82811) { cyclic( Z, Y
% 55.54/55.95 , X, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := Z
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := Z
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (100948) {G23,W5,D2,L1,V3,M1} R(100879,410) { cyclic( X, Y, Z
% 55.54/55.95 , Y ) }.
% 55.54/55.95 parent0: (101759) {G2,W5,D2,L1,V3,M1} { cyclic( Y, Z, X, Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := Z
% 55.54/55.95 Y := X
% 55.54/55.95 Z := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101760) {G2,W5,D2,L1,V3,M1} { cyclic( X, Z, Z, Y ) }.
% 55.54/55.95 parent0[0]: (401) {G1,W10,D2,L2,V4,M2} R(14,13) { ! cyclic( X, Y, Z, T ),
% 55.54/55.95 cyclic( X, Z, T, Y ) }.
% 55.54/55.95 parent1[0]: (100879) {G22,W5,D2,L1,V3,M1} S(40280);r(82811) { cyclic( Z, Y
% 55.54/55.95 , X, X ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := Z
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := Z
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := X
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (100950) {G23,W5,D2,L1,V3,M1} R(100879,401) { cyclic( X, Y, Y
% 55.54/55.95 , Z ) }.
% 55.54/55.95 parent0: (101760) {G2,W5,D2,L1,V3,M1} { cyclic( X, Z, Z, Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Z
% 55.54/55.95 Z := Y
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101762) {G2,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Y, Z ), cyclic
% 55.54/55.95 ( Y, Y, Z, T ) }.
% 55.54/55.95 parent0[2]: (441) {G1,W15,D2,L3,V5,M3} R(16,13) { ! cyclic( X, Y, Z, T ),
% 55.54/55.95 cyclic( Y, Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 55.54/55.95 parent1[0]: (100948) {G23,W5,D2,L1,V3,M1} R(100879,410) { cyclic( X, Y, Z,
% 55.54/55.95 Y ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Y
% 55.54/55.95 T := Z
% 55.54/55.95 U := T
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := T
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101763) {G3,W5,D2,L1,V3,M1} { cyclic( Y, Y, Z, T ) }.
% 55.54/55.95 parent0[0]: (101762) {G2,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Y, Z ), cyclic
% 55.54/55.95 ( Y, Y, Z, T ) }.
% 55.54/55.95 parent1[0]: (100950) {G23,W5,D2,L1,V3,M1} R(100879,401) { cyclic( X, Y, Y,
% 55.54/55.95 Z ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (100980) {G24,W5,D2,L1,V3,M1} R(100948,441);r(100950) { cyclic
% 55.54/55.95 ( Y, Y, Z, T ) }.
% 55.54/55.95 parent0: (101763) {G3,W5,D2,L1,V3,M1} { cyclic( Y, Y, Z, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := U
% 55.54/55.95 Y := Y
% 55.54/55.95 Z := Z
% 55.54/55.95 T := T
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 0 ==> 0
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101764) {G4,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol22,
% 55.54/55.95 skol20, skol23 ) }.
% 55.54/55.95 parent0[0]: (466) {G3,W10,D2,L2,V1,M2} R(411,16) { ! cyclic( X, skol22,
% 55.54/55.95 skol20, skol24 ), ! cyclic( X, skol22, skol20, skol23 ) }.
% 55.54/55.95 parent1[0]: (100980) {G24,W5,D2,L1,V3,M1} R(100948,441);r(100950) { cyclic
% 55.54/55.95 ( Y, Y, Z, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 X := skol22
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := skol22
% 55.54/55.95 Z := skol20
% 55.54/55.95 T := skol24
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 resolution: (101766) {G5,W0,D0,L0,V0,M0} { }.
% 55.54/55.95 parent0[0]: (101764) {G4,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol22,
% 55.54/55.95 skol20, skol23 ) }.
% 55.54/55.95 parent1[0]: (100980) {G24,W5,D2,L1,V3,M1} R(100948,441);r(100950) { cyclic
% 55.54/55.95 ( Y, Y, Z, T ) }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 substitution1:
% 55.54/55.95 X := X
% 55.54/55.95 Y := skol22
% 55.54/55.95 Z := skol20
% 55.54/55.95 T := skol23
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 subsumption: (101026) {G25,W0,D0,L0,V0,M0} R(100980,466);r(100980) { }.
% 55.54/55.95 parent0: (101766) {G5,W0,D0,L0,V0,M0} { }.
% 55.54/55.95 substitution0:
% 55.54/55.95 end
% 55.54/55.95 permutation0:
% 55.54/55.95 end
% 55.54/55.95
% 55.54/55.95 Proof check complete!
% 55.54/55.95
% 55.54/55.95 Memory use:
% 55.54/55.95
% 55.54/55.95 space for terms: 1431105
% 55.54/55.95 space for clauses: 4814571
% 55.54/55.95
% 55.54/55.95
% 55.54/55.95 clauses generated: 676485
% 55.54/55.95 clauses kept: 101027
% 55.54/55.95 clauses selected: 4748
% 55.54/55.95 clauses deleted: 39475
% 55.54/55.95 clauses inuse deleted: 1879
% 55.54/55.95
% 55.54/55.95 subsentry: 19189864
% 55.54/55.95 literals s-matched: 12451794
% 55.54/55.95 literals matched: 6273207
% 55.54/55.95 full subsumption: 3540841
% 55.54/55.95
% 55.54/55.95 checksum: 673508653
% 55.54/55.95
% 55.54/55.95
% 55.54/55.95 Bliksem ended
%------------------------------------------------------------------------------