%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GEO550+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Sat Jul 16 02:54:39 EDT 2022
% Result : Theorem 15.30s 15.69s
% Output : Refutation 15.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO550+1 : TPTP v8.1.0. Released v7.5.0.
% 0.07/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n007.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Sat Jun 18 12:27:28 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.77/1.19 *** allocated 10000 integers for termspace/termends
% 0.77/1.19 *** allocated 10000 integers for clauses
% 0.77/1.19 *** allocated 10000 integers for justifications
% 0.77/1.19 Bliksem 1.12
% 0.77/1.19
% 0.77/1.19
% 0.77/1.19 Automatic Strategy Selection
% 0.77/1.19
% 0.77/1.19 *** allocated 15000 integers for termspace/termends
% 0.77/1.19
% 0.77/1.19 Clauses:
% 0.77/1.19
% 0.77/1.19 { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 0.77/1.19 { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 0.77/1.19 { ! coll( X, T, Y ), ! coll( X, T, Z ), coll( Y, Z, X ) }.
% 0.77/1.19 { ! para( X, Y, Z, T ), para( X, Y, T, Z ) }.
% 0.77/1.19 { ! para( X, Y, Z, T ), para( Z, T, X, Y ) }.
% 0.77/1.19 { ! para( X, Y, U, W ), ! para( U, W, Z, T ), para( X, Y, Z, T ) }.
% 0.77/1.19 { ! perp( X, Y, Z, T ), perp( X, Y, T, Z ) }.
% 0.77/1.19 { ! perp( X, Y, Z, T ), perp( Z, T, X, Y ) }.
% 0.77/1.19 { ! perp( X, Y, U, W ), ! perp( U, W, Z, T ), para( X, Y, Z, T ) }.
% 0.77/1.19 { ! para( X, Y, U, W ), ! perp( U, W, Z, T ), perp( X, Y, Z, T ) }.
% 0.77/1.19 { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 0.77/1.19 { ! cong( T, X, T, Y ), ! cong( T, X, T, Z ), circle( T, X, Y, Z ) }.
% 0.77/1.19 { ! cong( U, X, U, Y ), ! cong( U, X, U, Z ), ! cong( U, X, U, T ), cyclic
% 0.77/1.19 ( X, Y, Z, T ) }.
% 0.77/1.19 { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z ) }.
% 0.77/1.19 { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T ) }.
% 0.77/1.19 { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T ) }.
% 0.77/1.19 { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 0.77/1.19 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( Y, X, Z, T, U, W, V0, V1
% 0.77/1.19 ) }.
% 0.77/1.19 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( Z, T, X, Y, V0, V1, U, W
% 0.77/1.19 ) }.
% 0.77/1.19 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( U, W, V0, V1, X, Y, Z, T
% 0.77/1.19 ) }.
% 0.77/1.19 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( X, Y, U, W, Z, T, V0, V1
% 0.77/1.19 ) }.
% 0.77/1.19 { ! eqangle( X, Y, Z, T, V2, V3, V4, V5 ), ! eqangle( V2, V3, V4, V5, U, W
% 0.77/1.19 , V0, V1 ), eqangle( X, Y, Z, T, U, W, V0, V1 ) }.
% 0.77/1.19 { ! cong( X, Y, Z, T ), cong( X, Y, T, Z ) }.
% 0.77/1.19 { ! cong( X, Y, Z, T ), cong( Z, T, X, Y ) }.
% 0.77/1.19 { ! cong( X, Y, U, W ), ! cong( U, W, Z, T ), cong( X, Y, Z, T ) }.
% 0.77/1.19 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( Y, X, Z, T, U, W, V0, V1
% 0.77/1.19 ) }.
% 0.77/1.19 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( Z, T, X, Y, V0, V1, U, W
% 0.77/1.19 ) }.
% 0.77/1.19 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( U, W, V0, V1, X, Y, Z, T
% 0.77/1.19 ) }.
% 0.77/1.19 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( X, Y, U, W, Z, T, V0, V1
% 0.77/1.19 ) }.
% 0.77/1.19 { ! eqratio( X, Y, Z, T, V2, V3, V4, V5 ), ! eqratio( V2, V3, V4, V5, U, W
% 0.77/1.19 , V0, V1 ), eqratio( X, Y, Z, T, U, W, V0, V1 ) }.
% 0.77/1.19 { ! simtri( X, Z, Y, T, W, U ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.19 { ! simtri( Y, X, Z, U, T, W ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.19 { ! simtri( T, U, W, X, Y, Z ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.19 { ! simtri( X, Y, Z, V0, V1, V2 ), ! simtri( V0, V1, V2, T, U, W ), simtri
% 0.77/1.19 ( X, Y, Z, T, U, W ) }.
% 0.77/1.19 { ! contri( X, Z, Y, T, W, U ), contri( X, Y, Z, T, U, W ) }.
% 0.77/1.19 { ! contri( Y, X, Z, U, T, W ), contri( X, Y, Z, T, U, W ) }.
% 0.77/1.19 { ! contri( T, U, W, X, Y, Z ), contri( X, Y, Z, T, U, W ) }.
% 0.77/1.19 { ! contri( X, Y, Z, V0, V1, V2 ), ! contri( V0, V1, V2, T, U, W ), contri
% 0.77/1.19 ( X, Y, Z, T, U, W ) }.
% 0.77/1.19 { ! eqangle( X, Y, U, W, Z, T, U, W ), para( X, Y, Z, T ) }.
% 0.77/1.19 { ! para( X, Y, Z, T ), eqangle( X, Y, U, W, Z, T, U, W ) }.
% 0.77/1.19 { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z, Y, T, X, T, Y ) }.
% 0.77/1.19 { ! eqangle( Z, X, Z, Y, T, X, T, Y ), coll( Z, T, X ), cyclic( X, Y, Z, T
% 0.77/1.19 ) }.
% 0.77/1.19 { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll( Z, T, Y ), cyclic( X, Y, Z,
% 0.77/1.19 T ) }.
% 0.77/1.19 { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U, T ), ! cyclic( X, Y, U, W ), !
% 0.77/1.19 eqangle( U, X, U, Y, W, Z, W, T ), cong( X, Y, Z, T ) }.
% 0.77/1.19 { ! midp( Z, U, X ), ! midp( T, U, Y ), para( Z, T, X, Y ) }.
% 0.77/1.19 { ! midp( U, X, T ), ! para( U, Z, T, Y ), ! coll( Z, X, Y ), midp( Z, X, Y
% 0.77/1.19 ) }.
% 0.77/1.19 { ! cong( Z, X, Z, Y ), eqangle( Z, X, X, Y, X, Y, Z, Y ) }.
% 0.77/1.19 { ! eqangle( Z, X, X, Y, X, Y, Z, Y ), coll( Z, X, Y ), cong( Z, X, Z, Y )
% 0.77/1.19 }.
% 0.77/1.19 { ! circle( U, X, Y, Z ), ! perp( U, X, X, T ), eqangle( X, T, X, Y, Z, X,
% 0.77/1.19 Z, Y ) }.
% 0.77/1.19 { ! circle( Y, X, T, U ), ! eqangle( X, Z, X, T, U, X, U, T ), perp( Y, X,
% 0.77/1.19 X, Z ) }.
% 0.77/1.19 { ! circle( T, X, Y, Z ), ! midp( U, Y, Z ), eqangle( X, Y, X, Z, T, Y, T,
% 0.77/1.19 U ) }.
% 0.77/1.19 { ! circle( U, T, X, Y ), ! coll( Z, X, Y ), ! eqangle( T, X, T, Y, U, X, U
% 0.77/1.19 , Z ), midp( Z, X, Y ) }.
% 0.77/1.19 { ! perp( X, Y, Y, T ), ! midp( Z, X, T ), cong( X, Z, Y, Z ) }.
% 0.77/1.19 { ! circle( T, X, Y, Z ), ! coll( T, X, Z ), perp( X, Y, Y, Z ) }.
% 0.77/1.19 { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T ), eqangle( X, T, Z, T, Z, T,
% 0.77/1.19 Z, Y ) }.
% 0.77/1.19 { ! midp( T, X, Y ), ! perp( Z, T, X, Y ), cong( Z, X, Z, Y ) }.
% 0.77/1.19 { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T ), perp( X, Y, Z, T ) }.
% 0.77/1.19 { ! cong( X, Y, T, Y ), ! cong( X, Z, T, Z ), ! cyclic( X, T, Y, Z ), perp
% 0.77/1.19 ( Y, X, X, Z ) }.
% 0.77/1.19 { ! eqangle( X, Y, Y, Z, T, U, U, W ), ! eqangle( X, Z, Y, Z, T, W, U, W )
% 0.77/1.19 , coll( X, Y, Z ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.19 { ! simtri( X, Y, Z, T, U, W ), eqratio( X, Y, X, Z, T, U, T, W ) }.
% 0.77/1.19 { ! simtri( X, Y, Z, T, U, W ), eqangle( X, Y, Y, Z, T, U, U, W ) }.
% 0.77/1.19 { ! simtri( X, Y, Z, T, U, W ), ! cong( X, Y, T, U ), contri( X, Y, Z, T, U
% 0.77/1.19 , W ) }.
% 0.77/1.19 { ! contri( X, Y, U, Z, T, W ), cong( X, Y, Z, T ) }.
% 0.77/1.19 { ! midp( U, X, Y ), ! midp( U, Z, T ), para( X, Z, Y, T ) }.
% 0.77/1.19 { ! midp( Z, T, U ), ! para( T, X, U, Y ), ! para( T, Y, U, X ), midp( Z, X
% 0.77/1.19 , Y ) }.
% 0.77/1.19 { ! para( X, Y, Z, T ), ! coll( U, X, Z ), ! coll( U, Y, T ), eqratio( U, X
% 0.77/1.19 , X, Z, U, Y, Y, T ) }.
% 0.77/1.19 { ! para( X, Y, X, Z ), coll( X, Y, Z ) }.
% 0.77/1.19 { ! cong( X, Y, X, Z ), ! coll( X, Y, Z ), midp( X, Y, Z ) }.
% 0.77/1.19 { ! midp( X, Y, Z ), cong( X, Y, X, Z ) }.
% 0.77/1.19 { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 0.77/1.19 { ! midp( U, X, Y ), ! midp( W, Z, T ), eqratio( U, X, X, Y, W, Z, Z, T ) }
% 0.77/1.19 .
% 0.77/1.19 { ! eqangle( X, Y, Z, T, Z, T, X, Y ), para( X, Y, Z, T ), perp( X, Y, Z, T
% 0.77/1.19 ) }.
% 0.77/1.19 { ! eqangle( X, Y, Z, T, Z, T, X, Y ), perp( X, Y, Z, T ), para( X, Y, Z, T
% 0.77/1.19 ) }.
% 0.77/1.19 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), ! para( U, W, V0, V1 ), para( X, Y
% 0.77/1.19 , Z, T ) }.
% 0.77/1.19 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), ! perp( U, W, V0, V1 ), perp( X, Y
% 0.77/1.19 , Z, T ) }.
% 0.77/1.19 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), ! cong( U, W, V0, V1 ), cong( X, Y
% 0.77/1.19 , Z, T ) }.
% 0.77/1.19 { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z, Y, Z, X, Z ), coll( skol1( U
% 0.77/1.19 , W, Z, T ), Z, T ) }.
% 0.77/1.19 { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z, Y, Z, X, Z ), coll( skol1( X
% 0.77/1.19 , Y, Z, T ), X, Y ) }.
% 0.77/1.19 { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( skol2( U
% 0.77/1.19 , W, Z, T ), Z, T ) }.
% 0.77/1.19 { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( Y, X,
% 0.77/1.19 skol2( X, Y, Z, T ) ) }.
% 0.77/1.19 { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( skol3( U
% 0.77/1.19 , W, Z, T ), Z, T ) }.
% 0.77/1.19 { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( Y, X,
% 0.77/1.19 skol3( X, Y, Z, T ) ) }.
% 0.77/1.19 { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y ), coll( skol4( U, W, Z, T ), Z
% 0.77/1.19 , T ) }.
% 0.77/1.19 { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y ), coll( Y, X, skol4( X, Y, Z, T
% 0.77/1.19 ) ) }.
% 0.77/1.19 { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll( X, Y, Z ), cyclic( T, Y, Z,
% 0.77/1.19 skol5( W, Y, Z, T ) ) }.
% 0.77/1.19 { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll( X, Y, Z ), eqangle( X, Z, Y, Z
% 0.77/1.19 , X, skol5( X, Y, Z, T ), Y, skol5( X, Y, Z, T ) ) }.
% 0.77/1.19 { ! midp( U, X, Y ), ! midp( W, Z, T ), midp( skol6( X, V0, V1, T, V2, V3 )
% 0.77/1.19 , X, T ) }.
% 0.77/1.19 { ! midp( U, X, Y ), ! midp( W, Z, T ), para( skol6( X, V0, Z, T, V1, W ),
% 0.77/1.19 W, X, Z ) }.
% 0.77/1.19 { ! midp( U, X, Y ), ! midp( W, Z, T ), para( skol6( X, Y, Z, T, U, W ), U
% 0.77/1.19 , Y, T ) }.
% 0.77/1.19 { ! midp( Z, X, Y ), ! midp( W, T, U ), ! coll( T, X, Y ), ! coll( U, X, Y
% 0.77/1.19 ), midp( skol7( X, V0 ), X, V0 ) }.
% 0.77/1.19 { ! midp( T, X, U ), ! para( X, W, Z, T ), ! para( X, W, U, Y ), ! coll( W
% 0.77/1.19 , Y, Z ), coll( skol8( V0, V1, Z, T ), T, Z ) }.
% 0.77/1.19 { ! midp( T, X, U ), ! para( X, W, Z, T ), ! para( X, W, U, Y ), ! coll( W
% 0.77/1.19 , Y, Z ), coll( skol8( X, Y, Z, T ), X, Y ) }.
% 0.77/1.19 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), cong( T, Z, T, skol9( W, V0,
% 0.77/1.19 Z, T ) ) }.
% 0.77/1.19 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), cong( Y, Z, Y, skol9( W, Y, Z
% 0.77/1.19 , T ) ) }.
% 0.77/1.19 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), para( skol9( X, Y, Z, T ), Z
% 0.77/1.19 , X, Y ) }.
% 0.77/1.19 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), coll( skol10( U, Y, Z ), Z, Y
% 0.77/1.19 ) }.
% 0.77/1.19 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), perp( X, skol10( X, Y, Z ), Z
% 0.77/1.19 , Y ) }.
% 0.77/1.19 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), alpha1( X, Y, Z ) }.
% 0.77/1.19 { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z ), Z, X ) }.
% 0.77/1.19 { ! alpha1( X, Y, Z ), perp( Y, skol11( X, Y, Z ), Z, X ) }.
% 0.77/1.19 { ! coll( T, Z, X ), ! perp( Y, T, Z, X ), alpha1( X, Y, Z ) }.
% 0.77/1.19 { ! circle( Y, X, Z, T ), perp( skol12( X, Y ), X, X, Y ) }.
% 5.31/5.72 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 5.31/5.72 , alpha2( X, Z, U, skol13( X, V0, Z, V1, U ) ) }.
% 5.31/5.72 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 5.31/5.72 , coll( skol21( V0, Y, T, V1 ), Y, T ) }.
% 5.31/5.72 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 5.31/5.72 , cong( skol21( X, Y, T, U ), U, U, X ) }.
% 5.31/5.72 { ! alpha2( X, Y, Z, T ), coll( T, X, Y ) }.
% 5.31/5.72 { ! alpha2( X, Y, Z, T ), cong( T, Z, Z, X ) }.
% 5.31/5.72 { ! coll( T, X, Y ), ! cong( T, Z, Z, X ), alpha2( X, Y, Z, T ) }.
% 5.31/5.72 { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T ), ! midp( U, X, Y ), circle(
% 5.31/5.72 skol14( X, Y, Z ), X, Y, Z ) }.
% 5.31/5.72 { ! perp( X, Z, Z, Y ), ! cyclic( X, Y, Z, T ), circle( skol15( X, Y, Z ),
% 5.31/5.72 X, Y, Z ) }.
% 5.31/5.72 { ! perp( X, U, U, T ), ! coll( T, Y, Z ), coll( skol16( W, Y, Z ), Y, Z )
% 5.31/5.72 }.
% 5.31/5.72 { ! perp( X, U, U, T ), ! coll( T, Y, Z ), perp( skol16( X, Y, Z ), X, Y, Z
% 5.31/5.72 ) }.
% 5.31/5.72 { ! perp( X, Z, X, Y ), ! perp( Y, X, Y, T ), ! midp( U, Z, T ), midp(
% 5.31/5.72 skol17( X, Y ), X, Y ) }.
% 5.31/5.72 { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z ), coll( X, Y, skol18( X, Y ) )
% 5.31/5.72 }.
% 5.31/5.72 { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z ), cong( Y, X, Y, skol18( X, Y )
% 5.31/5.72 ) }.
% 5.31/5.72 { ! para( U, W, X, Y ), ! coll( Z, U, X ), ! coll( Z, W, Y ), ! coll( T, U
% 5.31/5.72 , W ), coll( Z, T, skol19( V0, V1, Z, T ) ) }.
% 5.31/5.72 { ! para( U, W, X, Y ), ! coll( Z, U, X ), ! coll( Z, W, Y ), ! coll( T, U
% 5.31/5.72 , W ), coll( skol19( X, Y, Z, T ), X, Y ) }.
% 5.31/5.72 { coll( skol23, skol25, skol22 ) }.
% 5.31/5.72 { coll( skol23, skol20, skol26 ) }.
% 5.31/5.72 { coll( skol27, skol26, skol25 ) }.
% 5.31/5.72 { coll( skol27, skol20, skol22 ) }.
% 5.31/5.72 { circle( skol28, skol25, skol22, skol27 ) }.
% 5.31/5.72 { circle( skol29, skol27, skol26, skol20 ) }.
% 5.31/5.72 { circle( skol28, skol25, skol24, skol30 ) }.
% 5.31/5.72 { circle( skol29, skol20, skol24, skol31 ) }.
% 5.31/5.72 { ! cyclic( skol23, skol22, skol24, skol20 ) }.
% 5.31/5.72
% 5.31/5.72 percentage equality = 0.008746, percentage horn = 0.928000
% 5.31/5.72 This is a problem with some equality
% 5.31/5.72
% 5.31/5.72
% 5.31/5.72
% 5.31/5.72 Options Used:
% 5.31/5.72
% 5.31/5.72 useres = 1
% 5.31/5.72 useparamod = 1
% 5.31/5.72 useeqrefl = 1
% 5.31/5.72 useeqfact = 1
% 5.31/5.72 usefactor = 1
% 5.31/5.72 usesimpsplitting = 0
% 5.31/5.72 usesimpdemod = 5
% 5.31/5.72 usesimpres = 3
% 5.31/5.72
% 5.31/5.72 resimpinuse = 1000
% 5.31/5.72 resimpclauses = 20000
% 5.31/5.72 substype = eqrewr
% 5.31/5.72 backwardsubs = 1
% 5.31/5.72 selectoldest = 5
% 5.31/5.72
% 5.31/5.72 litorderings [0] = split
% 5.31/5.72 litorderings [1] = extend the termordering, first sorting on arguments
% 5.31/5.72
% 5.31/5.72 termordering = kbo
% 5.31/5.72
% 5.31/5.72 litapriori = 0
% 5.31/5.72 termapriori = 1
% 5.31/5.72 litaposteriori = 0
% 5.31/5.72 termaposteriori = 0
% 5.31/5.72 demodaposteriori = 0
% 5.31/5.72 ordereqreflfact = 0
% 5.31/5.72
% 5.31/5.72 litselect = negord
% 5.31/5.72
% 5.31/5.72 maxweight = 15
% 5.31/5.72 maxdepth = 30000
% 5.31/5.72 maxlength = 115
% 5.31/5.72 maxnrvars = 195
% 5.31/5.72 excuselevel = 1
% 5.31/5.72 increasemaxweight = 1
% 5.31/5.72
% 5.31/5.72 maxselected = 10000000
% 5.31/5.72 maxnrclauses = 10000000
% 5.31/5.72
% 5.31/5.72 showgenerated = 0
% 5.31/5.72 showkept = 0
% 5.31/5.72 showselected = 0
% 5.31/5.72 showdeleted = 0
% 5.31/5.72 showresimp = 1
% 5.31/5.72 showstatus = 2000
% 5.31/5.72
% 5.31/5.72 prologoutput = 0
% 5.31/5.72 nrgoals = 5000000
% 5.31/5.72 totalproof = 1
% 5.31/5.72
% 5.31/5.72 Symbols occurring in the translation:
% 5.31/5.72
% 5.31/5.72 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 5.31/5.72 . [1, 2] (w:1, o:43, a:1, s:1, b:0),
% 5.31/5.72 ! [4, 1] (w:0, o:38, a:1, s:1, b:0),
% 5.31/5.72 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.31/5.72 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.31/5.72 coll [38, 3] (w:1, o:71, a:1, s:1, b:0),
% 5.31/5.72 para [40, 4] (w:1, o:79, a:1, s:1, b:0),
% 5.31/5.72 perp [43, 4] (w:1, o:80, a:1, s:1, b:0),
% 5.31/5.72 midp [45, 3] (w:1, o:72, a:1, s:1, b:0),
% 5.31/5.72 cong [47, 4] (w:1, o:81, a:1, s:1, b:0),
% 5.31/5.72 circle [48, 4] (w:1, o:82, a:1, s:1, b:0),
% 5.31/5.72 cyclic [49, 4] (w:1, o:83, a:1, s:1, b:0),
% 5.31/5.72 eqangle [54, 8] (w:1, o:98, a:1, s:1, b:0),
% 5.31/5.72 eqratio [57, 8] (w:1, o:99, a:1, s:1, b:0),
% 5.31/5.72 simtri [59, 6] (w:1, o:95, a:1, s:1, b:0),
% 5.31/5.72 contri [60, 6] (w:1, o:96, a:1, s:1, b:0),
% 5.31/5.72 alpha1 [67, 3] (w:1, o:73, a:1, s:1, b:1),
% 5.31/5.72 alpha2 [68, 4] (w:1, o:84, a:1, s:1, b:1),
% 5.31/5.72 skol1 [69, 4] (w:1, o:85, a:1, s:1, b:1),
% 5.31/5.72 skol2 [70, 4] (w:1, o:87, a:1, s:1, b:1),
% 5.31/5.72 skol3 [71, 4] (w:1, o:89, a:1, s:1, b:1),
% 5.31/5.72 skol4 [72, 4] (w:1, o:90, a:1, s:1, b:1),
% 5.31/5.72 skol5 [73, 4] (w:1, o:91, a:1, s:1, b:1),
% 5.31/5.72 skol6 [74, 6] (w:1, o:97, a:1, s:1, b:1),
% 5.31/5.72 skol7 [75, 2] (w:1, o:67, a:1, s:1, b:1),
% 15.30/15.69 skol8 [76, 4] (w:1, o:92, a:1, s:1, b:1),
% 15.30/15.69 skol9 [77, 4] (w:1, o:93, a:1, s:1, b:1),
% 15.30/15.69 skol10 [78, 3] (w:1, o:74, a:1, s:1, b:1),
% 15.30/15.69 skol11 [79, 3] (w:1, o:75, a:1, s:1, b:1),
% 15.30/15.69 skol12 [80, 2] (w:1, o:68, a:1, s:1, b:1),
% 15.30/15.69 skol13 [81, 5] (w:1, o:94, a:1, s:1, b:1),
% 15.30/15.69 skol14 [82, 3] (w:1, o:76, a:1, s:1, b:1),
% 15.30/15.69 skol15 [83, 3] (w:1, o:77, a:1, s:1, b:1),
% 15.30/15.69 skol16 [84, 3] (w:1, o:78, a:1, s:1, b:1),
% 15.30/15.69 skol17 [85, 2] (w:1, o:69, a:1, s:1, b:1),
% 15.30/15.69 skol18 [86, 2] (w:1, o:70, a:1, s:1, b:1),
% 15.30/15.69 skol19 [87, 4] (w:1, o:86, a:1, s:1, b:1),
% 15.30/15.69 skol20 [88, 0] (w:1, o:27, a:1, s:1, b:1),
% 15.30/15.69 skol21 [89, 4] (w:1, o:88, a:1, s:1, b:1),
% 15.30/15.69 skol22 [90, 0] (w:1, o:28, a:1, s:1, b:1),
% 15.30/15.69 skol23 [91, 0] (w:1, o:29, a:1, s:1, b:1),
% 15.30/15.69 skol24 [92, 0] (w:1, o:30, a:1, s:1, b:1),
% 15.30/15.69 skol25 [93, 0] (w:1, o:31, a:1, s:1, b:1),
% 15.30/15.69 skol26 [94, 0] (w:1, o:32, a:1, s:1, b:1),
% 15.30/15.69 skol27 [95, 0] (w:1, o:33, a:1, s:1, b:1),
% 15.30/15.69 skol28 [96, 0] (w:1, o:34, a:1, s:1, b:1),
% 15.30/15.69 skol29 [97, 0] (w:1, o:35, a:1, s:1, b:1),
% 15.30/15.69 skol30 [98, 0] (w:1, o:36, a:1, s:1, b:1),
% 15.30/15.69 skol31 [99, 0] (w:1, o:37, a:1, s:1, b:1).
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Starting Search:
% 15.30/15.69
% 15.30/15.69 *** allocated 15000 integers for clauses
% 15.30/15.69 *** allocated 22500 integers for clauses
% 15.30/15.69 *** allocated 33750 integers for clauses
% 15.30/15.69 *** allocated 50625 integers for clauses
% 15.30/15.69 *** allocated 22500 integers for termspace/termends
% 15.30/15.69 *** allocated 75937 integers for clauses
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 *** allocated 33750 integers for termspace/termends
% 15.30/15.69 *** allocated 113905 integers for clauses
% 15.30/15.69 *** allocated 50625 integers for termspace/termends
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 13028
% 15.30/15.69 Kept: 2005
% 15.30/15.69 Inuse: 330
% 15.30/15.69 Deleted: 1
% 15.30/15.69 Deletedinuse: 1
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 *** allocated 170857 integers for clauses
% 15.30/15.69 *** allocated 75937 integers for termspace/termends
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 *** allocated 256285 integers for clauses
% 15.30/15.69 *** allocated 113905 integers for termspace/termends
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 34715
% 15.30/15.69 Kept: 4009
% 15.30/15.69 Inuse: 471
% 15.30/15.69 Deleted: 1
% 15.30/15.69 Deletedinuse: 1
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 *** allocated 384427 integers for clauses
% 15.30/15.69 *** allocated 170857 integers for termspace/termends
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 47832
% 15.30/15.69 Kept: 6024
% 15.30/15.69 Inuse: 536
% 15.30/15.69 Deleted: 1
% 15.30/15.69 Deletedinuse: 1
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 *** allocated 576640 integers for clauses
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 62448
% 15.30/15.69 Kept: 8040
% 15.30/15.69 Inuse: 685
% 15.30/15.69 Deleted: 2
% 15.30/15.69 Deletedinuse: 1
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 *** allocated 256285 integers for termspace/termends
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 82607
% 15.30/15.69 Kept: 10048
% 15.30/15.69 Inuse: 788
% 15.30/15.69 Deleted: 9
% 15.30/15.69 Deletedinuse: 4
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 94517
% 15.30/15.69 Kept: 12058
% 15.30/15.69 Inuse: 855
% 15.30/15.69 Deleted: 12
% 15.30/15.69 Deletedinuse: 6
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 *** allocated 864960 integers for clauses
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 104205
% 15.30/15.69 Kept: 14072
% 15.30/15.69 Inuse: 909
% 15.30/15.69 Deleted: 14
% 15.30/15.69 Deletedinuse: 8
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 *** allocated 384427 integers for termspace/termends
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 130900
% 15.30/15.69 Kept: 16106
% 15.30/15.69 Inuse: 1040
% 15.30/15.69 Deleted: 16
% 15.30/15.69 Deletedinuse: 8
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 169663
% 15.30/15.69 Kept: 18106
% 15.30/15.69 Inuse: 1174
% 15.30/15.69 Deleted: 26
% 15.30/15.69 Deletedinuse: 8
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 *** allocated 1297440 integers for clauses
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying clauses:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 181425
% 15.30/15.69 Kept: 20134
% 15.30/15.69 Inuse: 1281
% 15.30/15.69 Deleted: 1231
% 15.30/15.69 Deletedinuse: 16
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 195086
% 15.30/15.69 Kept: 22145
% 15.30/15.69 Inuse: 1386
% 15.30/15.69 Deleted: 1257
% 15.30/15.69 Deletedinuse: 42
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 207523
% 15.30/15.69 Kept: 24155
% 15.30/15.69 Inuse: 1509
% 15.30/15.69 Deleted: 1264
% 15.30/15.69 Deletedinuse: 48
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 227833
% 15.30/15.69 Kept: 26156
% 15.30/15.69 Inuse: 1668
% 15.30/15.69 Deleted: 1284
% 15.30/15.69 Deletedinuse: 68
% 15.30/15.69
% 15.30/15.69 *** allocated 576640 integers for termspace/termends
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 248356
% 15.30/15.69 Kept: 28162
% 15.30/15.69 Inuse: 1852
% 15.30/15.69 Deleted: 1300
% 15.30/15.69 Deletedinuse: 84
% 15.30/15.69
% 15.30/15.69 *** allocated 1946160 integers for clauses
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 267266
% 15.30/15.69 Kept: 30179
% 15.30/15.69 Inuse: 2064
% 15.30/15.69 Deleted: 1308
% 15.30/15.69 Deletedinuse: 92
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 278521
% 15.30/15.69 Kept: 32714
% 15.30/15.69 Inuse: 2121
% 15.30/15.69 Deleted: 1308
% 15.30/15.69 Deletedinuse: 92
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 282790
% 15.30/15.69 Kept: 34895
% 15.30/15.69 Inuse: 2126
% 15.30/15.69 Deleted: 1308
% 15.30/15.69 Deletedinuse: 92
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 293376
% 15.30/15.69 Kept: 37674
% 15.30/15.69 Inuse: 2141
% 15.30/15.69 Deleted: 1308
% 15.30/15.69 Deletedinuse: 92
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 *** allocated 864960 integers for termspace/termends
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 319176
% 15.30/15.69 Kept: 41724
% 15.30/15.69 Inuse: 2194
% 15.30/15.69 Deleted: 1318
% 15.30/15.69 Deletedinuse: 100
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying clauses:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 330359
% 15.30/15.69 Kept: 44252
% 15.30/15.69 Inuse: 2274
% 15.30/15.69 Deleted: 5979
% 15.30/15.69 Deletedinuse: 105
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 *** allocated 2919240 integers for clauses
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 339683
% 15.30/15.69 Kept: 46254
% 15.30/15.69 Inuse: 2343
% 15.30/15.69 Deleted: 5980
% 15.30/15.69 Deletedinuse: 106
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 352392
% 15.30/15.69 Kept: 48259
% 15.30/15.69 Inuse: 2443
% 15.30/15.69 Deleted: 5989
% 15.30/15.69 Deletedinuse: 115
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Intermediate Status:
% 15.30/15.69 Generated: 378518
% 15.30/15.69 Kept: 50264
% 15.30/15.69 Inuse: 2579
% 15.30/15.69 Deleted: 6002
% 15.30/15.69 Deletedinuse: 121
% 15.30/15.69
% 15.30/15.69 Resimplifying inuse:
% 15.30/15.69 Done
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Bliksems!, er is een bewijs:
% 15.30/15.69 % SZS status Theorem
% 15.30/15.69 % SZS output start Refutation
% 15.30/15.69
% 15.30/15.69 (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 15.30/15.69 (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 15.30/15.69 (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z ), coll( Y
% 15.30/15.69 , Z, X ) }.
% 15.30/15.69 (6) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( X, Y, T, Z ) }.
% 15.30/15.69 (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T, X, Y ) }.
% 15.30/15.69 (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U, W, Z, T ),
% 15.30/15.69 para( X, Y, Z, T ) }.
% 15.30/15.69 (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z )
% 15.30/15.69 }.
% 15.30/15.69 (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T )
% 15.30/15.69 }.
% 15.30/15.69 (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T )
% 15.30/15.69 }.
% 15.30/15.69 (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y, T
% 15.30/15.69 ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 (18) {G0,W18,D2,L2,V8,M2} I { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 15.30/15.69 eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 15.30/15.69 (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X, Y, U, W, Z
% 15.30/15.69 , T, U, W ) }.
% 15.30/15.69 (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll(
% 15.30/15.69 Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 (53) {G0,W14,D2,L3,V4,M3} I { ! circle( T, X, Y, Z ), ! coll( T, X, Z ),
% 15.30/15.69 perp( X, Y, Y, Z ) }.
% 15.30/15.69 (96) {G0,W14,D2,L3,V4,M3} I { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ),
% 15.30/15.69 alpha1( X, Y, Z ) }.
% 15.30/15.69 (97) {G0,W11,D3,L2,V4,M2} I { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z )
% 15.30/15.69 , Z, X ) }.
% 15.30/15.69 (100) {G0,W12,D3,L2,V4,M2} I { ! circle( Y, X, Z, T ), perp( skol12( X, Y )
% 15.30/15.69 , X, X, Y ) }.
% 15.30/15.69 (118) {G0,W4,D2,L1,V0,M1} I { coll( skol27, skol26, skol25 ) }.
% 15.30/15.69 (119) {G0,W4,D2,L1,V0,M1} I { coll( skol27, skol20, skol22 ) }.
% 15.30/15.69 (120) {G0,W5,D2,L1,V0,M1} I { circle( skol28, skol25, skol22, skol27 ) }.
% 15.30/15.69 (124) {G0,W5,D2,L1,V0,M1} I { ! cyclic( skol23, skol22, skol24, skol20 )
% 15.30/15.69 }.
% 15.30/15.69 (164) {G1,W4,D2,L1,V0,M1} R(0,118) { coll( skol27, skol25, skol26 ) }.
% 15.30/15.69 (167) {G2,W4,D2,L1,V0,M1} R(1,164) { coll( skol25, skol27, skol26 ) }.
% 15.30/15.69 (170) {G1,W8,D2,L2,V3,M2} R(1,0) { coll( X, Y, Z ), ! coll( Y, Z, X ) }.
% 15.30/15.69 (174) {G1,W4,D2,L1,V0,M1} R(1,118) { coll( skol26, skol27, skol25 ) }.
% 15.30/15.69 (178) {G3,W4,D2,L1,V0,M1} R(167,0) { coll( skol25, skol26, skol27 ) }.
% 15.30/15.69 (201) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll( X, Y, T ),
% 15.30/15.69 coll( Z, X, T ) }.
% 15.30/15.69 (210) {G2,W8,D2,L2,V3,M2} F(201) { ! coll( X, Y, Z ), coll( Z, X, Z ) }.
% 15.30/15.69 (214) {G4,W8,D2,L2,V1,M2} R(178,2) { ! coll( skol25, skol26, X ), coll( X,
% 15.30/15.69 skol27, skol25 ) }.
% 15.30/15.69 (254) {G3,W4,D2,L1,V0,M1} R(210,174) { coll( skol25, skol26, skol25 ) }.
% 15.30/15.69 (265) {G3,W12,D2,L3,V4,M3} R(210,2) { coll( X, Y, X ), ! coll( X, Z, Y ), !
% 15.30/15.69 coll( X, Z, T ) }.
% 15.30/15.69 (281) {G3,W4,D2,L1,V0,M1} R(210,119) { coll( skol22, skol27, skol22 ) }.
% 15.30/15.69 (282) {G4,W8,D2,L2,V3,M2} F(265) { coll( X, Y, X ), ! coll( X, Z, Y ) }.
% 15.30/15.69 (295) {G4,W4,D2,L1,V0,M1} R(254,0) { coll( skol25, skol25, skol26 ) }.
% 15.30/15.69 (297) {G1,W15,D2,L3,V6,M3} R(8,7) { ! perp( X, Y, Z, T ), para( U, W, Z, T
% 15.30/15.69 ), ! perp( X, Y, U, W ) }.
% 15.30/15.69 (307) {G2,W10,D2,L2,V4,M2} F(297) { ! perp( X, Y, Z, T ), para( Z, T, Z, T
% 15.30/15.69 ) }.
% 15.30/15.69 (308) {G5,W8,D2,L2,V1,M2} R(295,2) { ! coll( skol25, skol25, X ), coll(
% 15.30/15.69 skol26, X, skol25 ) }.
% 15.30/15.69 (365) {G1,W10,D2,L2,V4,M2} R(14,13) { ! cyclic( X, Y, Z, T ), cyclic( X, Z
% 15.30/15.69 , T, Y ) }.
% 15.30/15.69 (374) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), ! cyclic( Y, Z
% 15.30/15.69 , X, T ) }.
% 15.30/15.69 (376) {G1,W10,D2,L2,V4,M2} R(15,13) { cyclic( X, Y, Z, T ), ! cyclic( Y, X
% 15.30/15.69 , T, Z ) }.
% 15.30/15.69 (378) {G1,W5,D2,L1,V0,M1} R(15,124) { ! cyclic( skol22, skol23, skol24,
% 15.30/15.69 skol20 ) }.
% 15.30/15.69 (394) {G1,W15,D2,L3,V5,M3} R(16,15) { ! cyclic( X, Y, Z, T ), ! cyclic( X,
% 15.30/15.69 Y, Z, U ), cyclic( Z, Y, T, U ) }.
% 15.30/15.69 (399) {G1,W15,D2,L3,V5,M3} R(16,13) { ! cyclic( X, Y, Z, T ), cyclic( Y, Z
% 15.30/15.69 , T, U ), ! cyclic( X, Y, U, Z ) }.
% 15.30/15.69 (404) {G2,W10,D2,L2,V4,M2} F(394) { ! cyclic( X, Y, Z, T ), cyclic( Z, Y, T
% 15.30/15.69 , T ) }.
% 15.30/15.69 (534) {G4,W4,D2,L1,V0,M1} R(281,0) { coll( skol22, skol22, skol27 ) }.
% 15.30/15.69 (539) {G2,W5,D2,L1,V0,M1} R(378,14) { ! cyclic( skol22, skol24, skol23,
% 15.30/15.69 skol20 ) }.
% 15.30/15.69 (545) {G3,W5,D2,L1,V0,M1} R(539,15) { ! cyclic( skol24, skol22, skol23,
% 15.30/15.69 skol20 ) }.
% 15.30/15.69 (548) {G4,W5,D2,L1,V0,M1} R(545,14) { ! cyclic( skol24, skol23, skol22,
% 15.30/15.69 skol20 ) }.
% 15.30/15.69 (552) {G5,W5,D2,L1,V0,M1} R(548,13) { ! cyclic( skol24, skol23, skol20,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 (553) {G6,W5,D2,L1,V0,M1} R(552,15) { ! cyclic( skol23, skol24, skol20,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 (559) {G7,W5,D2,L1,V0,M1} R(553,14) { ! cyclic( skol23, skol20, skol24,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 (561) {G8,W5,D2,L1,V0,M1} R(559,15) { ! cyclic( skol20, skol23, skol24,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 (564) {G9,W5,D2,L1,V0,M1} R(561,14) { ! cyclic( skol20, skol24, skol23,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 (568) {G10,W5,D2,L1,V0,M1} R(564,13) { ! cyclic( skol20, skol24, skol22,
% 15.30/15.69 skol23 ) }.
% 15.30/15.69 (573) {G11,W5,D2,L1,V0,M1} R(568,14) { ! cyclic( skol20, skol22, skol24,
% 15.30/15.69 skol23 ) }.
% 15.30/15.69 (576) {G12,W5,D2,L1,V0,M1} R(573,15) { ! cyclic( skol22, skol20, skol24,
% 15.30/15.69 skol23 ) }.
% 15.30/15.69 (578) {G13,W10,D2,L2,V1,M2} R(576,16) { ! cyclic( X, skol22, skol20, skol24
% 15.30/15.69 ), ! cyclic( X, skol22, skol20, skol23 ) }.
% 15.30/15.69 (600) {G5,W8,D2,L2,V3,M2} R(282,1) { ! coll( X, Y, Z ), coll( Z, X, X ) }.
% 15.30/15.69 (605) {G6,W8,D2,L2,V3,M2} R(600,1) { coll( X, Y, Y ), ! coll( Z, Y, X ) }.
% 15.30/15.69 (606) {G6,W8,D2,L2,V3,M2} R(600,0) { coll( X, Y, Y ), ! coll( Y, X, Z ) }.
% 15.30/15.69 (607) {G7,W8,D2,L2,V3,M2} R(605,600) { ! coll( X, Y, Z ), coll( Y, Z, Z )
% 15.30/15.69 }.
% 15.30/15.69 (626) {G7,W8,D2,L2,V3,M2} R(606,606) { ! coll( X, Y, Z ), coll( X, Y, Y )
% 15.30/15.69 }.
% 15.30/15.69 (629) {G8,W12,D2,L3,V4,M3} R(626,2) { ! coll( X, Y, Z ), ! coll( X, Y, T )
% 15.30/15.69 , coll( T, Y, X ) }.
% 15.30/15.69 (630) {G9,W8,D2,L2,V3,M2} F(629) { ! coll( X, Y, Z ), coll( Z, Y, X ) }.
% 15.30/15.69 (633) {G10,W8,D2,L2,V3,M2} R(630,607) { coll( X, X, Y ), ! coll( Z, Y, X )
% 15.30/15.69 }.
% 15.30/15.69 (722) {G1,W14,D2,L2,V6,M2} R(39,18) { ! para( X, Y, Z, T ), eqangle( U, W,
% 15.30/15.69 X, Y, U, W, Z, T ) }.
% 15.30/15.69 (816) {G5,W14,D2,L2,V1,M2} R(42,534) { ! eqangle( skol22, X, skol22, skol27
% 15.30/15.69 , skol22, X, skol22, skol27 ), cyclic( X, skol27, skol22, skol22 ) }.
% 15.30/15.69 (1597) {G1,W9,D2,L2,V0,M2} R(53,120) { ! coll( skol28, skol25, skol27 ),
% 15.30/15.69 perp( skol25, skol22, skol22, skol27 ) }.
% 15.30/15.69 (4262) {G11,W8,D2,L2,V3,M2} R(97,633) { ! alpha1( X, Y, Z ), coll( X, X, Z
% 15.30/15.69 ) }.
% 15.30/15.69 (4761) {G1,W7,D3,L1,V0,M1} R(100,120) { perp( skol12( skol25, skol28 ),
% 15.30/15.69 skol25, skol25, skol28 ) }.
% 15.30/15.69 (4776) {G2,W7,D3,L1,V0,M1} R(4761,7) { perp( skol25, skol28, skol12( skol25
% 15.30/15.69 , skol28 ), skol25 ) }.
% 15.30/15.69 (4787) {G3,W7,D3,L1,V0,M1} R(4776,6) { perp( skol25, skol28, skol25, skol12
% 15.30/15.69 ( skol25, skol28 ) ) }.
% 15.30/15.69 (4797) {G4,W7,D3,L1,V0,M1} R(4787,7) { perp( skol25, skol12( skol25, skol28
% 15.30/15.69 ), skol25, skol28 ) }.
% 15.30/15.69 (4959) {G5,W4,D2,L1,V0,M1} R(4797,96);r(4797) { alpha1( skol25, skol25,
% 15.30/15.69 skol28 ) }.
% 15.30/15.69 (5132) {G12,W4,D2,L1,V0,M1} R(4959,4262) { coll( skol25, skol25, skol28 )
% 15.30/15.69 }.
% 15.30/15.69 (18189) {G13,W4,D2,L1,V0,M1} R(308,5132) { coll( skol26, skol28, skol25 )
% 15.30/15.69 }.
% 15.30/15.69 (18237) {G14,W4,D2,L1,V0,M1} R(18189,170) { coll( skol25, skol26, skol28 )
% 15.30/15.69 }.
% 15.30/15.69 (18269) {G15,W4,D2,L1,V0,M1} R(18237,214) { coll( skol28, skol27, skol25 )
% 15.30/15.69 }.
% 15.30/15.69 (18321) {G16,W4,D2,L1,V0,M1} R(18269,0) { coll( skol28, skol25, skol27 )
% 15.30/15.69 }.
% 15.30/15.69 (20018) {G17,W5,D2,L1,V0,M1} S(1597);r(18321) { perp( skol25, skol22,
% 15.30/15.69 skol22, skol27 ) }.
% 15.30/15.69 (23008) {G18,W5,D2,L1,V0,M1} R(20018,307) { para( skol22, skol27, skol22,
% 15.30/15.69 skol27 ) }.
% 15.30/15.69 (46472) {G19,W9,D2,L1,V2,M1} R(722,23008) { eqangle( X, Y, skol22, skol27,
% 15.30/15.69 X, Y, skol22, skol27 ) }.
% 15.30/15.69 (51338) {G20,W5,D2,L1,V1,M1} S(816);r(46472) { cyclic( X, skol27, skol22,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 (51359) {G21,W5,D2,L1,V1,M1} R(51338,376) { cyclic( skol27, X, skol22,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 (51371) {G22,W5,D2,L1,V1,M1} R(51359,404) { cyclic( skol22, X, skol22,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 (51393) {G23,W5,D2,L1,V1,M1} R(51371,374) { cyclic( skol22, skol22, X,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 (51394) {G23,W5,D2,L1,V1,M1} R(51371,365) { cyclic( skol22, skol22, skol22
% 15.30/15.69 , X ) }.
% 15.30/15.69 (51399) {G24,W5,D2,L1,V2,M1} R(51393,399);r(51394) { cyclic( skol22, skol22
% 15.30/15.69 , X, Y ) }.
% 15.30/15.69 (51417) {G25,W0,D0,L0,V0,M0} R(51399,578);r(51399) { }.
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 % SZS output end Refutation
% 15.30/15.69 found a proof!
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Unprocessed initial clauses:
% 15.30/15.69
% 15.30/15.69 (51419) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 15.30/15.69 (51420) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 15.30/15.69 (51421) {G0,W12,D2,L3,V4,M3} { ! coll( X, T, Y ), ! coll( X, T, Z ), coll
% 15.30/15.69 ( Y, Z, X ) }.
% 15.30/15.69 (51422) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( X, Y, T, Z )
% 15.30/15.69 }.
% 15.30/15.69 (51423) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( Z, T, X, Y )
% 15.30/15.69 }.
% 15.30/15.69 (51424) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! para( U, W, Z, T )
% 15.30/15.69 , para( X, Y, Z, T ) }.
% 15.30/15.69 (51425) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( X, Y, T, Z )
% 15.30/15.69 }.
% 15.30/15.69 (51426) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( Z, T, X, Y )
% 15.30/15.69 }.
% 15.30/15.69 (51427) {G0,W15,D2,L3,V6,M3} { ! perp( X, Y, U, W ), ! perp( U, W, Z, T )
% 15.30/15.69 , para( X, Y, Z, T ) }.
% 15.30/15.69 (51428) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! perp( U, W, Z, T )
% 15.30/15.69 , perp( X, Y, Z, T ) }.
% 15.30/15.69 (51429) {G0,W8,D2,L2,V3,M2} { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 15.30/15.69 (51430) {G0,W15,D2,L3,V4,M3} { ! cong( T, X, T, Y ), ! cong( T, X, T, Z )
% 15.30/15.69 , circle( T, X, Y, Z ) }.
% 15.30/15.69 (51431) {G0,W20,D2,L4,V5,M4} { ! cong( U, X, U, Y ), ! cong( U, X, U, Z )
% 15.30/15.69 , ! cong( U, X, U, T ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 (51432) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z
% 15.30/15.69 ) }.
% 15.30/15.69 (51433) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T
% 15.30/15.69 ) }.
% 15.30/15.69 (51434) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T
% 15.30/15.69 ) }.
% 15.30/15.69 (51435) {G0,W15,D2,L3,V5,M3} { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y,
% 15.30/15.69 T ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 (51436) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 15.30/15.69 eqangle( Y, X, Z, T, U, W, V0, V1 ) }.
% 15.30/15.69 (51437) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 15.30/15.69 eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 15.30/15.69 (51438) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 15.30/15.69 eqangle( U, W, V0, V1, X, Y, Z, T ) }.
% 15.30/15.69 (51439) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 15.30/15.69 eqangle( X, Y, U, W, Z, T, V0, V1 ) }.
% 15.30/15.69 (51440) {G0,W27,D2,L3,V12,M3} { ! eqangle( X, Y, Z, T, V2, V3, V4, V5 ), !
% 15.30/15.69 eqangle( V2, V3, V4, V5, U, W, V0, V1 ), eqangle( X, Y, Z, T, U, W, V0,
% 15.30/15.69 V1 ) }.
% 15.30/15.69 (51441) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( X, Y, T, Z )
% 15.30/15.69 }.
% 15.30/15.69 (51442) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( Z, T, X, Y )
% 15.30/15.69 }.
% 15.30/15.69 (51443) {G0,W15,D2,L3,V6,M3} { ! cong( X, Y, U, W ), ! cong( U, W, Z, T )
% 15.30/15.69 , cong( X, Y, Z, T ) }.
% 15.30/15.69 (51444) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 15.30/15.69 eqratio( Y, X, Z, T, U, W, V0, V1 ) }.
% 15.30/15.69 (51445) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 15.30/15.69 eqratio( Z, T, X, Y, V0, V1, U, W ) }.
% 15.30/15.69 (51446) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 15.30/15.69 eqratio( U, W, V0, V1, X, Y, Z, T ) }.
% 15.30/15.69 (51447) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 15.30/15.69 eqratio( X, Y, U, W, Z, T, V0, V1 ) }.
% 15.30/15.69 (51448) {G0,W27,D2,L3,V12,M3} { ! eqratio( X, Y, Z, T, V2, V3, V4, V5 ), !
% 15.30/15.69 eqratio( V2, V3, V4, V5, U, W, V0, V1 ), eqratio( X, Y, Z, T, U, W, V0,
% 15.30/15.69 V1 ) }.
% 15.30/15.69 (51449) {G0,W14,D2,L2,V6,M2} { ! simtri( X, Z, Y, T, W, U ), simtri( X, Y
% 15.30/15.69 , Z, T, U, W ) }.
% 15.30/15.69 (51450) {G0,W14,D2,L2,V6,M2} { ! simtri( Y, X, Z, U, T, W ), simtri( X, Y
% 15.30/15.69 , Z, T, U, W ) }.
% 15.30/15.69 (51451) {G0,W14,D2,L2,V6,M2} { ! simtri( T, U, W, X, Y, Z ), simtri( X, Y
% 15.30/15.69 , Z, T, U, W ) }.
% 15.30/15.69 (51452) {G0,W21,D2,L3,V9,M3} { ! simtri( X, Y, Z, V0, V1, V2 ), ! simtri(
% 15.30/15.69 V0, V1, V2, T, U, W ), simtri( X, Y, Z, T, U, W ) }.
% 15.30/15.69 (51453) {G0,W14,D2,L2,V6,M2} { ! contri( X, Z, Y, T, W, U ), contri( X, Y
% 15.30/15.69 , Z, T, U, W ) }.
% 15.30/15.69 (51454) {G0,W14,D2,L2,V6,M2} { ! contri( Y, X, Z, U, T, W ), contri( X, Y
% 15.30/15.69 , Z, T, U, W ) }.
% 15.30/15.69 (51455) {G0,W14,D2,L2,V6,M2} { ! contri( T, U, W, X, Y, Z ), contri( X, Y
% 15.30/15.69 , Z, T, U, W ) }.
% 15.30/15.69 (51456) {G0,W21,D2,L3,V9,M3} { ! contri( X, Y, Z, V0, V1, V2 ), ! contri(
% 15.30/15.69 V0, V1, V2, T, U, W ), contri( X, Y, Z, T, U, W ) }.
% 15.30/15.69 (51457) {G0,W14,D2,L2,V6,M2} { ! eqangle( X, Y, U, W, Z, T, U, W ), para(
% 15.30/15.69 X, Y, Z, T ) }.
% 15.30/15.69 (51458) {G0,W14,D2,L2,V6,M2} { ! para( X, Y, Z, T ), eqangle( X, Y, U, W,
% 15.30/15.69 Z, T, U, W ) }.
% 15.30/15.69 (51459) {G0,W14,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z, Y
% 15.30/15.69 , T, X, T, Y ) }.
% 15.30/15.69 (51460) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y ), coll(
% 15.30/15.69 Z, T, X ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 (51461) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll
% 15.30/15.69 ( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 (51462) {G0,W29,D2,L5,V6,M5} { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U,
% 15.30/15.69 T ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T ), cong( X
% 15.30/15.69 , Y, Z, T ) }.
% 15.30/15.69 (51463) {G0,W13,D2,L3,V5,M3} { ! midp( Z, U, X ), ! midp( T, U, Y ), para
% 15.30/15.69 ( Z, T, X, Y ) }.
% 15.30/15.69 (51464) {G0,W17,D2,L4,V5,M4} { ! midp( U, X, T ), ! para( U, Z, T, Y ), !
% 15.30/15.69 coll( Z, X, Y ), midp( Z, X, Y ) }.
% 15.30/15.69 (51465) {G0,W14,D2,L2,V3,M2} { ! cong( Z, X, Z, Y ), eqangle( Z, X, X, Y,
% 15.30/15.69 X, Y, Z, Y ) }.
% 15.30/15.69 (51466) {G0,W18,D2,L3,V3,M3} { ! eqangle( Z, X, X, Y, X, Y, Z, Y ), coll(
% 15.30/15.69 Z, X, Y ), cong( Z, X, Z, Y ) }.
% 15.30/15.69 (51467) {G0,W19,D2,L3,V5,M3} { ! circle( U, X, Y, Z ), ! perp( U, X, X, T
% 15.30/15.69 ), eqangle( X, T, X, Y, Z, X, Z, Y ) }.
% 15.30/15.69 (51468) {G0,W19,D2,L3,V5,M3} { ! circle( Y, X, T, U ), ! eqangle( X, Z, X
% 15.30/15.69 , T, U, X, U, T ), perp( Y, X, X, Z ) }.
% 15.30/15.69 (51469) {G0,W18,D2,L3,V5,M3} { ! circle( T, X, Y, Z ), ! midp( U, Y, Z ),
% 15.30/15.69 eqangle( X, Y, X, Z, T, Y, T, U ) }.
% 15.30/15.69 (51470) {G0,W22,D2,L4,V5,M4} { ! circle( U, T, X, Y ), ! coll( Z, X, Y ),
% 15.30/15.69 ! eqangle( T, X, T, Y, U, X, U, Z ), midp( Z, X, Y ) }.
% 15.30/15.69 (51471) {G0,W14,D2,L3,V4,M3} { ! perp( X, Y, Y, T ), ! midp( Z, X, T ),
% 15.30/15.69 cong( X, Z, Y, Z ) }.
% 15.30/15.69 (51472) {G0,W14,D2,L3,V4,M3} { ! circle( T, X, Y, Z ), ! coll( T, X, Z ),
% 15.30/15.69 perp( X, Y, Y, Z ) }.
% 15.30/15.69 (51473) {G0,W19,D2,L3,V4,M3} { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T
% 15.30/15.69 ), eqangle( X, T, Z, T, Z, T, Z, Y ) }.
% 15.30/15.69 (51474) {G0,W14,D2,L3,V4,M3} { ! midp( T, X, Y ), ! perp( Z, T, X, Y ),
% 15.30/15.69 cong( Z, X, Z, Y ) }.
% 15.30/15.69 (51475) {G0,W15,D2,L3,V4,M3} { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T )
% 15.30/15.69 , perp( X, Y, Z, T ) }.
% 15.30/15.69 (51476) {G0,W20,D2,L4,V4,M4} { ! cong( X, Y, T, Y ), ! cong( X, Z, T, Z )
% 15.30/15.69 , ! cyclic( X, T, Y, Z ), perp( Y, X, X, Z ) }.
% 15.30/15.69 (51477) {G0,W29,D2,L4,V6,M4} { ! eqangle( X, Y, Y, Z, T, U, U, W ), !
% 15.30/15.69 eqangle( X, Z, Y, Z, T, W, U, W ), coll( X, Y, Z ), simtri( X, Y, Z, T, U
% 15.30/15.69 , W ) }.
% 15.30/15.69 (51478) {G0,W16,D2,L2,V6,M2} { ! simtri( X, Y, Z, T, U, W ), eqratio( X, Y
% 15.30/15.69 , X, Z, T, U, T, W ) }.
% 15.30/15.69 (51479) {G0,W16,D2,L2,V6,M2} { ! simtri( X, Y, Z, T, U, W ), eqangle( X, Y
% 15.30/15.69 , Y, Z, T, U, U, W ) }.
% 15.30/15.69 (51480) {G0,W19,D2,L3,V6,M3} { ! simtri( X, Y, Z, T, U, W ), ! cong( X, Y
% 15.30/15.69 , T, U ), contri( X, Y, Z, T, U, W ) }.
% 15.30/15.69 (51481) {G0,W12,D2,L2,V6,M2} { ! contri( X, Y, U, Z, T, W ), cong( X, Y, Z
% 15.30/15.69 , T ) }.
% 15.30/15.69 (51482) {G0,W13,D2,L3,V5,M3} { ! midp( U, X, Y ), ! midp( U, Z, T ), para
% 15.30/15.69 ( X, Z, Y, T ) }.
% 15.30/15.69 (51483) {G0,W18,D2,L4,V5,M4} { ! midp( Z, T, U ), ! para( T, X, U, Y ), !
% 15.30/15.69 para( T, Y, U, X ), midp( Z, X, Y ) }.
% 15.30/15.69 (51484) {G0,W22,D2,L4,V5,M4} { ! para( X, Y, Z, T ), ! coll( U, X, Z ), !
% 15.30/15.69 coll( U, Y, T ), eqratio( U, X, X, Z, U, Y, Y, T ) }.
% 15.30/15.69 (51485) {G0,W9,D2,L2,V3,M2} { ! para( X, Y, X, Z ), coll( X, Y, Z ) }.
% 15.30/15.69 (51486) {G0,W13,D2,L3,V3,M3} { ! cong( X, Y, X, Z ), ! coll( X, Y, Z ),
% 15.30/15.69 midp( X, Y, Z ) }.
% 15.30/15.69 (51487) {G0,W9,D2,L2,V3,M2} { ! midp( X, Y, Z ), cong( X, Y, X, Z ) }.
% 15.30/15.69 (51488) {G0,W8,D2,L2,V3,M2} { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 15.30/15.69 (51489) {G0,W17,D2,L3,V6,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ),
% 15.30/15.69 eqratio( U, X, X, Y, W, Z, Z, T ) }.
% 15.30/15.69 (51490) {G0,W19,D2,L3,V4,M3} { ! eqangle( X, Y, Z, T, Z, T, X, Y ), para(
% 15.30/15.69 X, Y, Z, T ), perp( X, Y, Z, T ) }.
% 15.30/15.69 (51491) {G0,W19,D2,L3,V4,M3} { ! eqangle( X, Y, Z, T, Z, T, X, Y ), perp(
% 15.30/15.69 X, Y, Z, T ), para( X, Y, Z, T ) }.
% 15.30/15.69 (51492) {G0,W19,D2,L3,V8,M3} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), !
% 15.30/15.69 para( U, W, V0, V1 ), para( X, Y, Z, T ) }.
% 15.30/15.69 (51493) {G0,W19,D2,L3,V8,M3} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), !
% 15.30/15.69 perp( U, W, V0, V1 ), perp( X, Y, Z, T ) }.
% 15.30/15.69 (51494) {G0,W19,D2,L3,V8,M3} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), !
% 15.30/15.69 cong( U, W, V0, V1 ), cong( X, Y, Z, T ) }.
% 15.30/15.69 (51495) {G0,W22,D3,L3,V6,M3} { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z
% 15.30/15.69 , Y, Z, X, Z ), coll( skol1( U, W, Z, T ), Z, T ) }.
% 15.30/15.69 (51496) {G0,W22,D3,L3,V4,M3} { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z
% 15.30/15.69 , Y, Z, X, Z ), coll( skol1( X, Y, Z, T ), X, Y ) }.
% 15.30/15.69 (51497) {G0,W22,D3,L3,V6,M3} { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T
% 15.30/15.69 , Z, T, Z, Y ), coll( skol2( U, W, Z, T ), Z, T ) }.
% 15.30/15.69 (51498) {G0,W22,D3,L3,V4,M3} { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T
% 15.30/15.69 , Z, T, Z, Y ), coll( Y, X, skol2( X, Y, Z, T ) ) }.
% 15.30/15.69 (51499) {G0,W22,D3,L3,V6,M3} { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T
% 15.30/15.69 , Z, T, Z, Y ), coll( skol3( U, W, Z, T ), Z, T ) }.
% 15.30/15.69 (51500) {G0,W22,D3,L3,V4,M3} { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T
% 15.30/15.69 , Z, T, Z, Y ), coll( Y, X, skol3( X, Y, Z, T ) ) }.
% 15.30/15.69 (51501) {G0,W18,D3,L3,V6,M3} { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y )
% 15.30/15.69 , coll( skol4( U, W, Z, T ), Z, T ) }.
% 15.30/15.69 (51502) {G0,W18,D3,L3,V4,M3} { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y )
% 15.30/15.69 , coll( Y, X, skol4( X, Y, Z, T ) ) }.
% 15.30/15.69 (51503) {G0,W22,D3,L3,V6,M3} { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll(
% 15.30/15.69 X, Y, Z ), cyclic( T, Y, Z, skol5( W, Y, Z, T ) ) }.
% 15.30/15.69 (51504) {G0,W30,D3,L3,V5,M3} { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll(
% 15.30/15.69 X, Y, Z ), eqangle( X, Z, Y, Z, X, skol5( X, Y, Z, T ), Y, skol5( X, Y, Z
% 15.30/15.69 , T ) ) }.
% 15.30/15.69 (51505) {G0,W18,D3,L3,V10,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), midp
% 15.30/15.69 ( skol6( X, V0, V1, T, V2, V3 ), X, T ) }.
% 15.30/15.69 (51506) {G0,W19,D3,L3,V8,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), para
% 15.30/15.69 ( skol6( X, V0, Z, T, V1, W ), W, X, Z ) }.
% 15.30/15.69 (51507) {G0,W19,D3,L3,V6,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), para
% 15.30/15.69 ( skol6( X, Y, Z, T, U, W ), U, Y, T ) }.
% 15.30/15.69 (51508) {G0,W22,D3,L5,V7,M5} { ! midp( Z, X, Y ), ! midp( W, T, U ), !
% 15.30/15.69 coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0 ) }.
% 15.30/15.69 (51509) {G0,W26,D3,L5,V8,M5} { ! midp( T, X, U ), ! para( X, W, Z, T ), !
% 15.30/15.69 para( X, W, U, Y ), ! coll( W, Y, Z ), coll( skol8( V0, V1, Z, T ), T, Z
% 15.30/15.69 ) }.
% 15.30/15.69 (51510) {G0,W26,D3,L5,V6,M5} { ! midp( T, X, U ), ! para( X, W, Z, T ), !
% 15.30/15.69 para( X, W, U, Y ), ! coll( W, Y, Z ), coll( skol8( X, Y, Z, T ), X, Y )
% 15.30/15.69 }.
% 15.30/15.69 (51511) {G0,W19,D3,L3,V7,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 15.30/15.69 , cong( T, Z, T, skol9( W, V0, Z, T ) ) }.
% 15.30/15.69 (51512) {G0,W19,D3,L3,V6,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 15.30/15.69 , cong( Y, Z, Y, skol9( W, Y, Z, T ) ) }.
% 15.30/15.69 (51513) {G0,W19,D3,L3,V5,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 15.30/15.69 , para( skol9( X, Y, Z, T ), Z, X, Y ) }.
% 15.30/15.69 (51514) {G0,W17,D3,L3,V5,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 15.30/15.69 , coll( skol10( U, Y, Z ), Z, Y ) }.
% 15.30/15.69 (51515) {G0,W18,D3,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 15.30/15.69 , perp( X, skol10( X, Y, Z ), Z, Y ) }.
% 15.30/15.69 (51516) {G0,W14,D2,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 15.30/15.69 , alpha1( X, Y, Z ) }.
% 15.30/15.69 (51517) {G0,W11,D3,L2,V4,M2} { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z
% 15.30/15.69 ), Z, X ) }.
% 15.30/15.69 (51518) {G0,W12,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), perp( Y, skol11( X, Y
% 15.30/15.69 , Z ), Z, X ) }.
% 15.30/15.69 (51519) {G0,W13,D2,L3,V4,M3} { ! coll( T, Z, X ), ! perp( Y, T, Z, X ),
% 15.30/15.69 alpha1( X, Y, Z ) }.
% 15.30/15.69 (51520) {G0,W12,D3,L2,V4,M2} { ! circle( Y, X, Z, T ), perp( skol12( X, Y
% 15.30/15.69 ), X, X, Y ) }.
% 15.30/15.69 (51521) {G0,W28,D3,L5,V8,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 15.30/15.69 ), ! cong( U, X, U, Y ), W = U, alpha2( X, Z, U, skol13( X, V0, Z, V1, U
% 15.30/15.69 ) ) }.
% 15.30/15.69 (51522) {G0,W26,D3,L5,V8,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 15.30/15.69 ), ! cong( U, X, U, Y ), W = U, coll( skol21( V0, Y, T, V1 ), Y, T ) }.
% 15.30/15.69 (51523) {G0,W27,D3,L5,V6,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 15.30/15.69 ), ! cong( U, X, U, Y ), W = U, cong( skol21( X, Y, T, U ), U, U, X )
% 15.30/15.69 }.
% 15.30/15.69 (51524) {G0,W9,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), coll( T, X, Y ) }.
% 15.30/15.69 (51525) {G0,W10,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), cong( T, Z, Z, X )
% 15.30/15.69 }.
% 15.30/15.69 (51526) {G0,W14,D2,L3,V4,M3} { ! coll( T, X, Y ), ! cong( T, Z, Z, X ),
% 15.30/15.69 alpha2( X, Y, Z, T ) }.
% 15.30/15.69 (51527) {G0,W22,D3,L4,V5,M4} { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T
% 15.30/15.69 ), ! midp( U, X, Y ), circle( skol14( X, Y, Z ), X, Y, Z ) }.
% 15.30/15.69 (51528) {G0,W18,D3,L3,V4,M3} { ! perp( X, Z, Z, Y ), ! cyclic( X, Y, Z, T
% 15.30/15.69 ), circle( skol15( X, Y, Z ), X, Y, Z ) }.
% 15.30/15.69 (51529) {G0,W16,D3,L3,V6,M3} { ! perp( X, U, U, T ), ! coll( T, Y, Z ),
% 15.30/15.69 coll( skol16( W, Y, Z ), Y, Z ) }.
% 15.30/15.69 (51530) {G0,W17,D3,L3,V5,M3} { ! perp( X, U, U, T ), ! coll( T, Y, Z ),
% 15.30/15.69 perp( skol16( X, Y, Z ), X, Y, Z ) }.
% 15.30/15.69 (51531) {G0,W20,D3,L4,V5,M4} { ! perp( X, Z, X, Y ), ! perp( Y, X, Y, T )
% 15.30/15.69 , ! midp( U, Z, T ), midp( skol17( X, Y ), X, Y ) }.
% 15.30/15.69 (51532) {G0,W16,D3,L3,V3,M3} { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z )
% 15.30/15.69 , coll( X, Y, skol18( X, Y ) ) }.
% 15.30/15.69 (51533) {G0,W17,D3,L3,V3,M3} { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z )
% 15.30/15.69 , cong( Y, X, Y, skol18( X, Y ) ) }.
% 15.30/15.69 (51534) {G0,W25,D3,L5,V8,M5} { ! para( U, W, X, Y ), ! coll( Z, U, X ), !
% 15.30/15.69 coll( Z, W, Y ), ! coll( T, U, W ), coll( Z, T, skol19( V0, V1, Z, T ) )
% 15.30/15.69 }.
% 15.30/15.69 (51535) {G0,W25,D3,L5,V6,M5} { ! para( U, W, X, Y ), ! coll( Z, U, X ), !
% 15.30/15.69 coll( Z, W, Y ), ! coll( T, U, W ), coll( skol19( X, Y, Z, T ), X, Y )
% 15.30/15.69 }.
% 15.30/15.69 (51536) {G0,W4,D2,L1,V0,M1} { coll( skol23, skol25, skol22 ) }.
% 15.30/15.69 (51537) {G0,W4,D2,L1,V0,M1} { coll( skol23, skol20, skol26 ) }.
% 15.30/15.69 (51538) {G0,W4,D2,L1,V0,M1} { coll( skol27, skol26, skol25 ) }.
% 15.30/15.69 (51539) {G0,W4,D2,L1,V0,M1} { coll( skol27, skol20, skol22 ) }.
% 15.30/15.69 (51540) {G0,W5,D2,L1,V0,M1} { circle( skol28, skol25, skol22, skol27 ) }.
% 15.30/15.69 (51541) {G0,W5,D2,L1,V0,M1} { circle( skol29, skol27, skol26, skol20 ) }.
% 15.30/15.69 (51542) {G0,W5,D2,L1,V0,M1} { circle( skol28, skol25, skol24, skol30 ) }.
% 15.30/15.69 (51543) {G0,W5,D2,L1,V0,M1} { circle( skol29, skol20, skol24, skol31 ) }.
% 15.30/15.69 (51544) {G0,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol22, skol24, skol20 )
% 15.30/15.69 }.
% 15.30/15.69
% 15.30/15.69
% 15.30/15.69 Total Proof:
% 15.30/15.69
% 15.30/15.69 subsumption: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 15.30/15.69 }.
% 15.30/15.69 parent0: (51419) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( X, Z, Y )
% 15.30/15.69 }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 15.30/15.69 }.
% 15.30/15.69 parent0: (51420) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Y, X, Z )
% 15.30/15.69 }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T,
% 15.30/15.69 Z ), coll( Y, Z, X ) }.
% 15.30/15.69 parent0: (51421) {G0,W12,D2,L3,V4,M3} { ! coll( X, T, Y ), ! coll( X, T, Z
% 15.30/15.69 ), coll( Y, Z, X ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 2 ==> 2
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (6) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( X, Y
% 15.30/15.69 , T, Z ) }.
% 15.30/15.69 parent0: (51425) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( X, Y,
% 15.30/15.69 T, Z ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T
% 15.30/15.69 , X, Y ) }.
% 15.30/15.69 parent0: (51426) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( Z, T,
% 15.30/15.69 X, Y ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U,
% 15.30/15.69 W, Z, T ), para( X, Y, Z, T ) }.
% 15.30/15.69 parent0: (51427) {G0,W15,D2,L3,V6,M3} { ! perp( X, Y, U, W ), ! perp( U, W
% 15.30/15.69 , Z, T ), para( X, Y, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 U := U
% 15.30/15.69 W := W
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 2 ==> 2
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 15.30/15.69 X, Y, T, Z ) }.
% 15.30/15.69 parent0: (51432) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Y, T, Z ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 15.30/15.69 X, Z, Y, T ) }.
% 15.30/15.69 parent0: (51433) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Z, Y, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 15.30/15.69 Y, X, Z, T ) }.
% 15.30/15.69 parent0: (51434) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Y
% 15.30/15.69 , X, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic
% 15.30/15.69 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 parent0: (51435) {G0,W15,D2,L3,V5,M3} { ! cyclic( U, X, Y, Z ), ! cyclic(
% 15.30/15.69 U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 U := U
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 2 ==> 2
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (18) {G0,W18,D2,L2,V8,M2} I { ! eqangle( X, Y, Z, T, U, W, V0
% 15.30/15.69 , V1 ), eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 15.30/15.69 parent0: (51437) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0,
% 15.30/15.69 V1 ), eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 U := U
% 15.30/15.69 W := W
% 15.30/15.69 V0 := V0
% 15.30/15.69 V1 := V1
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X
% 15.30/15.69 , Y, U, W, Z, T, U, W ) }.
% 15.30/15.69 parent0: (51458) {G0,W14,D2,L2,V6,M2} { ! para( X, Y, Z, T ), eqangle( X,
% 15.30/15.69 Y, U, W, Z, T, U, W ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 U := U
% 15.30/15.69 W := W
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T,
% 15.30/15.69 Y ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 parent0: (51461) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y
% 15.30/15.69 ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 2 ==> 2
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (53) {G0,W14,D2,L3,V4,M3} I { ! circle( T, X, Y, Z ), ! coll(
% 15.30/15.69 T, X, Z ), perp( X, Y, Y, Z ) }.
% 15.30/15.69 parent0: (51472) {G0,W14,D2,L3,V4,M3} { ! circle( T, X, Y, Z ), ! coll( T
% 15.30/15.69 , X, Z ), perp( X, Y, Y, Z ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 2 ==> 2
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (96) {G0,W14,D2,L3,V4,M3} I { ! perp( X, T, Y, Z ), ! perp( Y
% 15.30/15.69 , T, X, Z ), alpha1( X, Y, Z ) }.
% 15.30/15.69 parent0: (51516) {G0,W14,D2,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T
% 15.30/15.69 , X, Z ), alpha1( X, Y, Z ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 2 ==> 2
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (97) {G0,W11,D3,L2,V4,M2} I { ! alpha1( X, Y, Z ), coll(
% 15.30/15.69 skol11( X, T, Z ), Z, X ) }.
% 15.30/15.69 parent0: (51517) {G0,W11,D3,L2,V4,M2} { ! alpha1( X, Y, Z ), coll( skol11
% 15.30/15.69 ( X, T, Z ), Z, X ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (100) {G0,W12,D3,L2,V4,M2} I { ! circle( Y, X, Z, T ), perp(
% 15.30/15.69 skol12( X, Y ), X, X, Y ) }.
% 15.30/15.69 parent0: (51520) {G0,W12,D3,L2,V4,M2} { ! circle( Y, X, Z, T ), perp(
% 15.30/15.69 skol12( X, Y ), X, X, Y ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (118) {G0,W4,D2,L1,V0,M1} I { coll( skol27, skol26, skol25 )
% 15.30/15.69 }.
% 15.30/15.69 parent0: (51538) {G0,W4,D2,L1,V0,M1} { coll( skol27, skol26, skol25 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (119) {G0,W4,D2,L1,V0,M1} I { coll( skol27, skol20, skol22 )
% 15.30/15.69 }.
% 15.30/15.69 parent0: (51539) {G0,W4,D2,L1,V0,M1} { coll( skol27, skol20, skol22 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (120) {G0,W5,D2,L1,V0,M1} I { circle( skol28, skol25, skol22,
% 15.30/15.69 skol27 ) }.
% 15.30/15.69 parent0: (51540) {G0,W5,D2,L1,V0,M1} { circle( skol28, skol25, skol22,
% 15.30/15.69 skol27 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (124) {G0,W5,D2,L1,V0,M1} I { ! cyclic( skol23, skol22, skol24
% 15.30/15.69 , skol20 ) }.
% 15.30/15.69 parent0: (51544) {G0,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol22, skol24,
% 15.30/15.69 skol20 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51961) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol25, skol26 )
% 15.30/15.69 }.
% 15.30/15.69 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 15.30/15.69 }.
% 15.30/15.69 parent1[0]: (118) {G0,W4,D2,L1,V0,M1} I { coll( skol27, skol26, skol25 )
% 15.30/15.69 }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := skol27
% 15.30/15.69 Y := skol26
% 15.30/15.69 Z := skol25
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (164) {G1,W4,D2,L1,V0,M1} R(0,118) { coll( skol27, skol25,
% 15.30/15.69 skol26 ) }.
% 15.30/15.69 parent0: (51961) {G1,W4,D2,L1,V0,M1} { coll( skol27, skol25, skol26 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51962) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol27, skol26 )
% 15.30/15.69 }.
% 15.30/15.69 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 15.30/15.69 }.
% 15.30/15.69 parent1[0]: (164) {G1,W4,D2,L1,V0,M1} R(0,118) { coll( skol27, skol25,
% 15.30/15.69 skol26 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := skol27
% 15.30/15.69 Y := skol25
% 15.30/15.69 Z := skol26
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (167) {G2,W4,D2,L1,V0,M1} R(1,164) { coll( skol25, skol27,
% 15.30/15.69 skol26 ) }.
% 15.30/15.69 parent0: (51962) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol27, skol26 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51963) {G1,W8,D2,L2,V3,M2} { coll( Y, X, Z ), ! coll( X, Z, Y
% 15.30/15.69 ) }.
% 15.30/15.69 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 15.30/15.69 }.
% 15.30/15.69 parent1[1]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 15.30/15.69 }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Z
% 15.30/15.69 Z := Y
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (170) {G1,W8,D2,L2,V3,M2} R(1,0) { coll( X, Y, Z ), ! coll( Y
% 15.30/15.69 , Z, X ) }.
% 15.30/15.69 parent0: (51963) {G1,W8,D2,L2,V3,M2} { coll( Y, X, Z ), ! coll( X, Z, Y )
% 15.30/15.69 }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := Y
% 15.30/15.69 Y := X
% 15.30/15.69 Z := Z
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51964) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol27, skol25 )
% 15.30/15.69 }.
% 15.30/15.69 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 15.30/15.69 }.
% 15.30/15.69 parent1[0]: (118) {G0,W4,D2,L1,V0,M1} I { coll( skol27, skol26, skol25 )
% 15.30/15.69 }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := skol27
% 15.30/15.69 Y := skol26
% 15.30/15.69 Z := skol25
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (174) {G1,W4,D2,L1,V0,M1} R(1,118) { coll( skol26, skol27,
% 15.30/15.69 skol25 ) }.
% 15.30/15.69 parent0: (51964) {G1,W4,D2,L1,V0,M1} { coll( skol26, skol27, skol25 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51965) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol26, skol27 )
% 15.30/15.69 }.
% 15.30/15.69 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 15.30/15.69 }.
% 15.30/15.69 parent1[0]: (167) {G2,W4,D2,L1,V0,M1} R(1,164) { coll( skol25, skol27,
% 15.30/15.69 skol26 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := skol25
% 15.30/15.69 Y := skol27
% 15.30/15.69 Z := skol26
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (178) {G3,W4,D2,L1,V0,M1} R(167,0) { coll( skol25, skol26,
% 15.30/15.69 skol27 ) }.
% 15.30/15.69 parent0: (51965) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol26, skol27 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51969) {G1,W12,D2,L3,V4,M3} { coll( X, Z, Y ), ! coll( Z, T,
% 15.30/15.69 X ), ! coll( Z, T, Y ) }.
% 15.30/15.69 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 15.30/15.69 }.
% 15.30/15.69 parent1[2]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 15.30/15.69 ), coll( Y, Z, X ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := Z
% 15.30/15.69 Y := X
% 15.30/15.69 Z := Y
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (201) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll
% 15.30/15.69 ( X, Y, T ), coll( Z, X, T ) }.
% 15.30/15.69 parent0: (51969) {G1,W12,D2,L3,V4,M3} { coll( X, Z, Y ), ! coll( Z, T, X )
% 15.30/15.69 , ! coll( Z, T, Y ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := Z
% 15.30/15.69 Y := T
% 15.30/15.69 Z := X
% 15.30/15.69 T := Y
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 2
% 15.30/15.69 1 ==> 0
% 15.30/15.69 2 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 factor: (51971) {G1,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, X, Z )
% 15.30/15.69 }.
% 15.30/15.69 parent0[0, 1]: (201) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), !
% 15.30/15.69 coll( X, Y, T ), coll( Z, X, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := Z
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (210) {G2,W8,D2,L2,V3,M2} F(201) { ! coll( X, Y, Z ), coll( Z
% 15.30/15.69 , X, Z ) }.
% 15.30/15.69 parent0: (51971) {G1,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, X, Z )
% 15.30/15.69 }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51973) {G1,W8,D2,L2,V1,M2} { ! coll( skol25, skol26, X ),
% 15.30/15.69 coll( X, skol27, skol25 ) }.
% 15.30/15.69 parent0[1]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 15.30/15.69 ), coll( Y, Z, X ) }.
% 15.30/15.69 parent1[0]: (178) {G3,W4,D2,L1,V0,M1} R(167,0) { coll( skol25, skol26,
% 15.30/15.69 skol27 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := skol25
% 15.30/15.69 Y := X
% 15.30/15.69 Z := skol27
% 15.30/15.69 T := skol26
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (214) {G4,W8,D2,L2,V1,M2} R(178,2) { ! coll( skol25, skol26, X
% 15.30/15.69 ), coll( X, skol27, skol25 ) }.
% 15.30/15.69 parent0: (51973) {G1,W8,D2,L2,V1,M2} { ! coll( skol25, skol26, X ), coll(
% 15.30/15.69 X, skol27, skol25 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51974) {G2,W4,D2,L1,V0,M1} { coll( skol25, skol26, skol25 )
% 15.30/15.69 }.
% 15.30/15.69 parent0[0]: (210) {G2,W8,D2,L2,V3,M2} F(201) { ! coll( X, Y, Z ), coll( Z,
% 15.30/15.69 X, Z ) }.
% 15.30/15.69 parent1[0]: (174) {G1,W4,D2,L1,V0,M1} R(1,118) { coll( skol26, skol27,
% 15.30/15.69 skol25 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := skol26
% 15.30/15.69 Y := skol27
% 15.30/15.69 Z := skol25
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (254) {G3,W4,D2,L1,V0,M1} R(210,174) { coll( skol25, skol26,
% 15.30/15.69 skol25 ) }.
% 15.30/15.69 parent0: (51974) {G2,W4,D2,L1,V0,M1} { coll( skol25, skol26, skol25 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51975) {G1,W12,D2,L3,V4,M3} { coll( Z, X, Z ), ! coll( Z, T,
% 15.30/15.69 X ), ! coll( Z, T, Y ) }.
% 15.30/15.69 parent0[0]: (210) {G2,W8,D2,L2,V3,M2} F(201) { ! coll( X, Y, Z ), coll( Z,
% 15.30/15.69 X, Z ) }.
% 15.30/15.69 parent1[2]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 15.30/15.69 ), coll( Y, Z, X ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := Z
% 15.30/15.69 Y := X
% 15.30/15.69 Z := Y
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (265) {G3,W12,D2,L3,V4,M3} R(210,2) { coll( X, Y, X ), ! coll
% 15.30/15.69 ( X, Z, Y ), ! coll( X, Z, T ) }.
% 15.30/15.69 parent0: (51975) {G1,W12,D2,L3,V4,M3} { coll( Z, X, Z ), ! coll( Z, T, X )
% 15.30/15.69 , ! coll( Z, T, Y ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := Y
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := X
% 15.30/15.69 T := Z
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 2 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51977) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol27, skol22 )
% 15.30/15.69 }.
% 15.30/15.69 parent0[0]: (210) {G2,W8,D2,L2,V3,M2} F(201) { ! coll( X, Y, Z ), coll( Z,
% 15.30/15.69 X, Z ) }.
% 15.30/15.69 parent1[0]: (119) {G0,W4,D2,L1,V0,M1} I { coll( skol27, skol20, skol22 )
% 15.30/15.69 }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := skol27
% 15.30/15.69 Y := skol20
% 15.30/15.69 Z := skol22
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (281) {G3,W4,D2,L1,V0,M1} R(210,119) { coll( skol22, skol27,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 parent0: (51977) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol27, skol22 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 factor: (51978) {G3,W8,D2,L2,V3,M2} { coll( X, Y, X ), ! coll( X, Z, Y )
% 15.30/15.69 }.
% 15.30/15.69 parent0[1, 2]: (265) {G3,W12,D2,L3,V4,M3} R(210,2) { coll( X, Y, X ), !
% 15.30/15.69 coll( X, Z, Y ), ! coll( X, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := Y
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (282) {G4,W8,D2,L2,V3,M2} F(265) { coll( X, Y, X ), ! coll( X
% 15.30/15.69 , Z, Y ) }.
% 15.30/15.69 parent0: (51978) {G3,W8,D2,L2,V3,M2} { coll( X, Y, X ), ! coll( X, Z, Y )
% 15.30/15.69 }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51979) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol25, skol26 )
% 15.30/15.69 }.
% 15.30/15.69 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 15.30/15.69 }.
% 15.30/15.69 parent1[0]: (254) {G3,W4,D2,L1,V0,M1} R(210,174) { coll( skol25, skol26,
% 15.30/15.69 skol25 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := skol25
% 15.30/15.69 Y := skol26
% 15.30/15.69 Z := skol25
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (295) {G4,W4,D2,L1,V0,M1} R(254,0) { coll( skol25, skol25,
% 15.30/15.69 skol26 ) }.
% 15.30/15.69 parent0: (51979) {G1,W4,D2,L1,V0,M1} { coll( skol25, skol25, skol26 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51980) {G1,W15,D2,L3,V6,M3} { ! perp( Z, T, U, W ), para( X,
% 15.30/15.69 Y, U, W ), ! perp( Z, T, X, Y ) }.
% 15.30/15.69 parent0[0]: (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U, W
% 15.30/15.69 , Z, T ), para( X, Y, Z, T ) }.
% 15.30/15.69 parent1[1]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 15.30/15.69 X, Y ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := U
% 15.30/15.69 T := W
% 15.30/15.69 U := Z
% 15.30/15.69 W := T
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := Z
% 15.30/15.69 Y := T
% 15.30/15.69 Z := X
% 15.30/15.69 T := Y
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (297) {G1,W15,D2,L3,V6,M3} R(8,7) { ! perp( X, Y, Z, T ), para
% 15.30/15.69 ( U, W, Z, T ), ! perp( X, Y, U, W ) }.
% 15.30/15.69 parent0: (51980) {G1,W15,D2,L3,V6,M3} { ! perp( Z, T, U, W ), para( X, Y,
% 15.30/15.69 U, W ), ! perp( Z, T, X, Y ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := U
% 15.30/15.69 Y := W
% 15.30/15.69 Z := X
% 15.30/15.69 T := Y
% 15.30/15.69 U := Z
% 15.30/15.69 W := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 2 ==> 2
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 factor: (51984) {G1,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), para( Z, T, Z
% 15.30/15.69 , T ) }.
% 15.30/15.69 parent0[0, 2]: (297) {G1,W15,D2,L3,V6,M3} R(8,7) { ! perp( X, Y, Z, T ),
% 15.30/15.69 para( U, W, Z, T ), ! perp( X, Y, U, W ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 U := Z
% 15.30/15.69 W := T
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (307) {G2,W10,D2,L2,V4,M2} F(297) { ! perp( X, Y, Z, T ), para
% 15.30/15.69 ( Z, T, Z, T ) }.
% 15.30/15.69 parent0: (51984) {G1,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), para( Z, T,
% 15.30/15.69 Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51985) {G1,W8,D2,L2,V1,M2} { ! coll( skol25, skol25, X ),
% 15.30/15.69 coll( skol26, X, skol25 ) }.
% 15.30/15.69 parent0[0]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 15.30/15.69 ), coll( Y, Z, X ) }.
% 15.30/15.69 parent1[0]: (295) {G4,W4,D2,L1,V0,M1} R(254,0) { coll( skol25, skol25,
% 15.30/15.69 skol26 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := skol25
% 15.30/15.69 Y := skol26
% 15.30/15.69 Z := X
% 15.30/15.69 T := skol25
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (308) {G5,W8,D2,L2,V1,M2} R(295,2) { ! coll( skol25, skol25, X
% 15.30/15.69 ), coll( skol26, X, skol25 ) }.
% 15.30/15.69 parent0: (51985) {G1,W8,D2,L2,V1,M2} { ! coll( skol25, skol25, X ), coll(
% 15.30/15.69 skol26, X, skol25 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51988) {G1,W10,D2,L2,V4,M2} { cyclic( X, Y, T, Z ), ! cyclic
% 15.30/15.69 ( X, Z, Y, T ) }.
% 15.30/15.69 parent0[0]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Y, T, Z ) }.
% 15.30/15.69 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Z, Y, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Z
% 15.30/15.69 Z := Y
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (365) {G1,W10,D2,L2,V4,M2} R(14,13) { ! cyclic( X, Y, Z, T ),
% 15.30/15.69 cyclic( X, Z, T, Y ) }.
% 15.30/15.69 parent0: (51988) {G1,W10,D2,L2,V4,M2} { cyclic( X, Y, T, Z ), ! cyclic( X
% 15.30/15.69 , Z, Y, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Z
% 15.30/15.69 Z := Y
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 1
% 15.30/15.69 1 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51989) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic
% 15.30/15.69 ( X, Z, Y, T ) }.
% 15.30/15.69 parent0[0]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 15.30/15.69 , X, Z, T ) }.
% 15.30/15.69 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Z, Y, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Z
% 15.30/15.69 Z := Y
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (374) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), !
% 15.30/15.69 cyclic( Y, Z, X, T ) }.
% 15.30/15.69 parent0: (51989) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic( X
% 15.30/15.69 , Z, Y, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := Y
% 15.30/15.69 Y := X
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51990) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic
% 15.30/15.69 ( X, Y, T, Z ) }.
% 15.30/15.69 parent0[0]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 15.30/15.69 , X, Z, T ) }.
% 15.30/15.69 parent1[1]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Y, T, Z ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := T
% 15.30/15.69 T := Z
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (376) {G1,W10,D2,L2,V4,M2} R(15,13) { cyclic( X, Y, Z, T ), !
% 15.30/15.69 cyclic( Y, X, T, Z ) }.
% 15.30/15.69 parent0: (51990) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic( X
% 15.30/15.69 , Y, T, Z ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := Y
% 15.30/15.69 Y := X
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51991) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol23, skol24
% 15.30/15.69 , skol20 ) }.
% 15.30/15.69 parent0[0]: (124) {G0,W5,D2,L1,V0,M1} I { ! cyclic( skol23, skol22, skol24
% 15.30/15.69 , skol20 ) }.
% 15.30/15.69 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 15.30/15.69 , X, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol22
% 15.30/15.69 Y := skol23
% 15.30/15.69 Z := skol24
% 15.30/15.69 T := skol20
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (378) {G1,W5,D2,L1,V0,M1} R(15,124) { ! cyclic( skol22, skol23
% 15.30/15.69 , skol24, skol20 ) }.
% 15.30/15.69 parent0: (51991) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol23, skol24,
% 15.30/15.69 skol20 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51995) {G1,W15,D2,L3,V5,M3} { cyclic( Y, X, Z, T ), ! cyclic
% 15.30/15.69 ( U, X, Y, Z ), ! cyclic( U, X, Y, T ) }.
% 15.30/15.69 parent0[0]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 15.30/15.69 , X, Z, T ) }.
% 15.30/15.69 parent1[2]: (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic
% 15.30/15.69 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 U := U
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (394) {G1,W15,D2,L3,V5,M3} R(16,15) { ! cyclic( X, Y, Z, T ),
% 15.30/15.69 ! cyclic( X, Y, Z, U ), cyclic( Z, Y, T, U ) }.
% 15.30/15.69 parent0: (51995) {G1,W15,D2,L3,V5,M3} { cyclic( Y, X, Z, T ), ! cyclic( U
% 15.30/15.69 , X, Y, Z ), ! cyclic( U, X, Y, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := Y
% 15.30/15.69 Y := Z
% 15.30/15.69 Z := T
% 15.30/15.69 T := U
% 15.30/15.69 U := X
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 2
% 15.30/15.69 1 ==> 0
% 15.30/15.69 2 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (51998) {G1,W15,D2,L3,V5,M3} { ! cyclic( X, Y, Z, T ), cyclic
% 15.30/15.69 ( Y, Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 15.30/15.69 parent0[1]: (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic
% 15.30/15.69 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 parent1[1]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Y, T, Z ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := Y
% 15.30/15.69 Y := Z
% 15.30/15.69 Z := T
% 15.30/15.69 T := U
% 15.30/15.69 U := X
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := U
% 15.30/15.69 T := Z
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (399) {G1,W15,D2,L3,V5,M3} R(16,13) { ! cyclic( X, Y, Z, T ),
% 15.30/15.69 cyclic( Y, Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 15.30/15.69 parent0: (51998) {G1,W15,D2,L3,V5,M3} { ! cyclic( X, Y, Z, T ), cyclic( Y
% 15.30/15.69 , Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 U := U
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 2 ==> 2
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 factor: (52000) {G1,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Z,
% 15.30/15.69 Y, T, T ) }.
% 15.30/15.69 parent0[0, 1]: (394) {G1,W15,D2,L3,V5,M3} R(16,15) { ! cyclic( X, Y, Z, T )
% 15.30/15.69 , ! cyclic( X, Y, Z, U ), cyclic( Z, Y, T, U ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 U := T
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (404) {G2,W10,D2,L2,V4,M2} F(394) { ! cyclic( X, Y, Z, T ),
% 15.30/15.69 cyclic( Z, Y, T, T ) }.
% 15.30/15.69 parent0: (52000) {G1,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Z
% 15.30/15.69 , Y, T, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := X
% 15.30/15.69 Y := Y
% 15.30/15.69 Z := Z
% 15.30/15.69 T := T
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 1 ==> 1
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52001) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol22, skol27 )
% 15.30/15.69 }.
% 15.30/15.69 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 15.30/15.69 }.
% 15.30/15.69 parent1[0]: (281) {G3,W4,D2,L1,V0,M1} R(210,119) { coll( skol22, skol27,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 X := skol22
% 15.30/15.69 Y := skol27
% 15.30/15.69 Z := skol22
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (534) {G4,W4,D2,L1,V0,M1} R(281,0) { coll( skol22, skol22,
% 15.30/15.69 skol27 ) }.
% 15.30/15.69 parent0: (52001) {G1,W4,D2,L1,V0,M1} { coll( skol22, skol22, skol27 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52002) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol24, skol23
% 15.30/15.69 , skol20 ) }.
% 15.30/15.69 parent0[0]: (378) {G1,W5,D2,L1,V0,M1} R(15,124) { ! cyclic( skol22, skol23
% 15.30/15.69 , skol24, skol20 ) }.
% 15.30/15.69 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Z, Y, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol22
% 15.30/15.69 Y := skol24
% 15.30/15.69 Z := skol23
% 15.30/15.69 T := skol20
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (539) {G2,W5,D2,L1,V0,M1} R(378,14) { ! cyclic( skol22, skol24
% 15.30/15.69 , skol23, skol20 ) }.
% 15.30/15.69 parent0: (52002) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol24, skol23,
% 15.30/15.69 skol20 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52003) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol22, skol23
% 15.30/15.69 , skol20 ) }.
% 15.30/15.69 parent0[0]: (539) {G2,W5,D2,L1,V0,M1} R(378,14) { ! cyclic( skol22, skol24
% 15.30/15.69 , skol23, skol20 ) }.
% 15.30/15.69 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 15.30/15.69 , X, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol24
% 15.30/15.69 Y := skol22
% 15.30/15.69 Z := skol23
% 15.30/15.69 T := skol20
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (545) {G3,W5,D2,L1,V0,M1} R(539,15) { ! cyclic( skol24, skol22
% 15.30/15.69 , skol23, skol20 ) }.
% 15.30/15.69 parent0: (52003) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol22, skol23,
% 15.30/15.69 skol20 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52004) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol23, skol22
% 15.30/15.69 , skol20 ) }.
% 15.30/15.69 parent0[0]: (545) {G3,W5,D2,L1,V0,M1} R(539,15) { ! cyclic( skol24, skol22
% 15.30/15.69 , skol23, skol20 ) }.
% 15.30/15.69 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Z, Y, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol24
% 15.30/15.69 Y := skol23
% 15.30/15.69 Z := skol22
% 15.30/15.69 T := skol20
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (548) {G4,W5,D2,L1,V0,M1} R(545,14) { ! cyclic( skol24, skol23
% 15.30/15.69 , skol22, skol20 ) }.
% 15.30/15.69 parent0: (52004) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol23, skol22,
% 15.30/15.69 skol20 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52005) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol23, skol20
% 15.30/15.69 , skol22 ) }.
% 15.30/15.69 parent0[0]: (548) {G4,W5,D2,L1,V0,M1} R(545,14) { ! cyclic( skol24, skol23
% 15.30/15.69 , skol22, skol20 ) }.
% 15.30/15.69 parent1[1]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Y, T, Z ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol24
% 15.30/15.69 Y := skol23
% 15.30/15.69 Z := skol20
% 15.30/15.69 T := skol22
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (552) {G5,W5,D2,L1,V0,M1} R(548,13) { ! cyclic( skol24, skol23
% 15.30/15.69 , skol20, skol22 ) }.
% 15.30/15.69 parent0: (52005) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol23, skol20,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52006) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol24, skol20
% 15.30/15.69 , skol22 ) }.
% 15.30/15.69 parent0[0]: (552) {G5,W5,D2,L1,V0,M1} R(548,13) { ! cyclic( skol24, skol23
% 15.30/15.69 , skol20, skol22 ) }.
% 15.30/15.69 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 15.30/15.69 , X, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol23
% 15.30/15.69 Y := skol24
% 15.30/15.69 Z := skol20
% 15.30/15.69 T := skol22
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (553) {G6,W5,D2,L1,V0,M1} R(552,15) { ! cyclic( skol23, skol24
% 15.30/15.69 , skol20, skol22 ) }.
% 15.30/15.69 parent0: (52006) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol24, skol20,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52007) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol20, skol24
% 15.30/15.69 , skol22 ) }.
% 15.30/15.69 parent0[0]: (553) {G6,W5,D2,L1,V0,M1} R(552,15) { ! cyclic( skol23, skol24
% 15.30/15.69 , skol20, skol22 ) }.
% 15.30/15.69 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Z, Y, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol23
% 15.30/15.69 Y := skol20
% 15.30/15.69 Z := skol24
% 15.30/15.69 T := skol22
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (559) {G7,W5,D2,L1,V0,M1} R(553,14) { ! cyclic( skol23, skol20
% 15.30/15.69 , skol24, skol22 ) }.
% 15.30/15.69 parent0: (52007) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol20, skol24,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52008) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol23, skol24
% 15.30/15.69 , skol22 ) }.
% 15.30/15.69 parent0[0]: (559) {G7,W5,D2,L1,V0,M1} R(553,14) { ! cyclic( skol23, skol20
% 15.30/15.69 , skol24, skol22 ) }.
% 15.30/15.69 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 15.30/15.69 , X, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol20
% 15.30/15.69 Y := skol23
% 15.30/15.69 Z := skol24
% 15.30/15.69 T := skol22
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (561) {G8,W5,D2,L1,V0,M1} R(559,15) { ! cyclic( skol20, skol23
% 15.30/15.69 , skol24, skol22 ) }.
% 15.30/15.69 parent0: (52008) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol23, skol24,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52009) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol24, skol23
% 15.30/15.69 , skol22 ) }.
% 15.30/15.69 parent0[0]: (561) {G8,W5,D2,L1,V0,M1} R(559,15) { ! cyclic( skol20, skol23
% 15.30/15.69 , skol24, skol22 ) }.
% 15.30/15.69 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Z, Y, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol20
% 15.30/15.69 Y := skol24
% 15.30/15.69 Z := skol23
% 15.30/15.69 T := skol22
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (564) {G9,W5,D2,L1,V0,M1} R(561,14) { ! cyclic( skol20, skol24
% 15.30/15.69 , skol23, skol22 ) }.
% 15.30/15.69 parent0: (52009) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol24, skol23,
% 15.30/15.69 skol22 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52010) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol24, skol22
% 15.30/15.69 , skol23 ) }.
% 15.30/15.69 parent0[0]: (564) {G9,W5,D2,L1,V0,M1} R(561,14) { ! cyclic( skol20, skol24
% 15.30/15.69 , skol23, skol22 ) }.
% 15.30/15.69 parent1[1]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Y, T, Z ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol20
% 15.30/15.69 Y := skol24
% 15.30/15.69 Z := skol22
% 15.30/15.69 T := skol23
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (568) {G10,W5,D2,L1,V0,M1} R(564,13) { ! cyclic( skol20,
% 15.30/15.69 skol24, skol22, skol23 ) }.
% 15.30/15.69 parent0: (52010) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol24, skol22,
% 15.30/15.69 skol23 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52011) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol22, skol24
% 15.30/15.69 , skol23 ) }.
% 15.30/15.69 parent0[0]: (568) {G10,W5,D2,L1,V0,M1} R(564,13) { ! cyclic( skol20, skol24
% 15.30/15.69 , skol22, skol23 ) }.
% 15.30/15.69 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 15.30/15.69 , Z, Y, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol20
% 15.30/15.69 Y := skol22
% 15.30/15.69 Z := skol24
% 15.30/15.69 T := skol23
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (573) {G11,W5,D2,L1,V0,M1} R(568,14) { ! cyclic( skol20,
% 15.30/15.69 skol22, skol24, skol23 ) }.
% 15.30/15.69 parent0: (52011) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol22, skol24,
% 15.30/15.69 skol23 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52012) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol20, skol24
% 15.30/15.69 , skol23 ) }.
% 15.30/15.69 parent0[0]: (573) {G11,W5,D2,L1,V0,M1} R(568,14) { ! cyclic( skol20, skol22
% 15.30/15.69 , skol24, skol23 ) }.
% 15.30/15.69 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 15.30/15.69 , X, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol22
% 15.30/15.69 Y := skol20
% 15.30/15.69 Z := skol24
% 15.30/15.69 T := skol23
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 subsumption: (576) {G12,W5,D2,L1,V0,M1} R(573,15) { ! cyclic( skol22,
% 15.30/15.69 skol20, skol24, skol23 ) }.
% 15.30/15.69 parent0: (52012) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol20, skol24,
% 15.30/15.69 skol23 ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 permutation0:
% 15.30/15.69 0 ==> 0
% 15.30/15.69 end
% 15.30/15.69
% 15.30/15.69 resolution: (52013) {G1,W10,D2,L2,V1,M2} { ! cyclic( X, skol22, skol20,
% 15.30/15.69 skol24 ), ! cyclic( X, skol22, skol20, skol23 ) }.
% 15.30/15.69 parent0[0]: (576) {G12,W5,D2,L1,V0,M1} R(573,15) { ! cyclic( skol22, skol20
% 15.30/15.69 , skol24, skol23 ) }.
% 15.30/15.69 parent1[2]: (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic
% 15.30/15.69 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 15.30/15.69 substitution0:
% 15.30/15.69 end
% 15.30/15.69 substitution1:
% 15.30/15.69 X := skol22
% 15.30/15.69 Y := skol20
% 15.30/15.69 Z := skol24
% 15.30/15.69 T := skol23
% 15.30/15.70 U := X
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (578) {G13,W10,D2,L2,V1,M2} R(576,16) { ! cyclic( X, skol22,
% 15.30/15.70 skol20, skol24 ), ! cyclic( X, skol22, skol20, skol23 ) }.
% 15.30/15.70 parent0: (52013) {G1,W10,D2,L2,V1,M2} { ! cyclic( X, skol22, skol20,
% 15.30/15.70 skol24 ), ! cyclic( X, skol22, skol20, skol23 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 1 ==> 1
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52015) {G1,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( X, Z, Y
% 15.30/15.70 ) }.
% 15.30/15.70 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 15.30/15.70 }.
% 15.30/15.70 parent1[0]: (282) {G4,W8,D2,L2,V3,M2} F(265) { coll( X, Y, X ), ! coll( X,
% 15.30/15.70 Z, Y ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := X
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := Z
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (600) {G5,W8,D2,L2,V3,M2} R(282,1) { ! coll( X, Y, Z ), coll(
% 15.30/15.70 Z, X, X ) }.
% 15.30/15.70 parent0: (52015) {G1,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( X, Z, Y )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Z
% 15.30/15.70 Z := Y
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 1
% 15.30/15.70 1 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52016) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( Y, X, Z
% 15.30/15.70 ) }.
% 15.30/15.70 parent0[0]: (600) {G5,W8,D2,L2,V3,M2} R(282,1) { ! coll( X, Y, Z ), coll( Z
% 15.30/15.70 , X, X ) }.
% 15.30/15.70 parent1[1]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := Z
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := Y
% 15.30/15.70 Y := X
% 15.30/15.70 Z := Z
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (605) {G6,W8,D2,L2,V3,M2} R(600,1) { coll( X, Y, Y ), ! coll(
% 15.30/15.70 Z, Y, X ) }.
% 15.30/15.70 parent0: (52016) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( Y, X, Z )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := Y
% 15.30/15.70 Y := Z
% 15.30/15.70 Z := X
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 1 ==> 1
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52017) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( X, Z, Y
% 15.30/15.70 ) }.
% 15.30/15.70 parent0[0]: (600) {G5,W8,D2,L2,V3,M2} R(282,1) { ! coll( X, Y, Z ), coll( Z
% 15.30/15.70 , X, X ) }.
% 15.30/15.70 parent1[1]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := Z
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Z
% 15.30/15.70 Z := Y
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (606) {G6,W8,D2,L2,V3,M2} R(600,0) { coll( X, Y, Y ), ! coll(
% 15.30/15.70 Y, X, Z ) }.
% 15.30/15.70 parent0: (52017) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( X, Z, Y )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := Y
% 15.30/15.70 Y := Z
% 15.30/15.70 Z := X
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 1 ==> 1
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52019) {G6,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( Z, Y, X
% 15.30/15.70 ) }.
% 15.30/15.70 parent0[0]: (600) {G5,W8,D2,L2,V3,M2} R(282,1) { ! coll( X, Y, Z ), coll( Z
% 15.30/15.70 , X, X ) }.
% 15.30/15.70 parent1[0]: (605) {G6,W8,D2,L2,V3,M2} R(600,1) { coll( X, Y, Y ), ! coll( Z
% 15.30/15.70 , Y, X ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := Y
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := Z
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (607) {G7,W8,D2,L2,V3,M2} R(605,600) { ! coll( X, Y, Z ), coll
% 15.30/15.70 ( Y, Z, Z ) }.
% 15.30/15.70 parent0: (52019) {G6,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( Z, Y, X )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := Z
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := X
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 1
% 15.30/15.70 1 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52020) {G7,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! coll( X, Y, Z
% 15.30/15.70 ) }.
% 15.30/15.70 parent0[1]: (606) {G6,W8,D2,L2,V3,M2} R(600,0) { coll( X, Y, Y ), ! coll( Y
% 15.30/15.70 , X, Z ) }.
% 15.30/15.70 parent1[0]: (606) {G6,W8,D2,L2,V3,M2} R(600,0) { coll( X, Y, Y ), ! coll( Y
% 15.30/15.70 , X, Z ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := X
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := Y
% 15.30/15.70 Y := X
% 15.30/15.70 Z := Z
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (626) {G7,W8,D2,L2,V3,M2} R(606,606) { ! coll( X, Y, Z ), coll
% 15.30/15.70 ( X, Y, Y ) }.
% 15.30/15.70 parent0: (52020) {G7,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! coll( X, Y, Z )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := Z
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 1
% 15.30/15.70 1 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52024) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, Y,
% 15.30/15.70 X ), ! coll( X, Y, T ) }.
% 15.30/15.70 parent0[1]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 15.30/15.70 ), coll( Y, Z, X ) }.
% 15.30/15.70 parent1[1]: (626) {G7,W8,D2,L2,V3,M2} R(606,606) { ! coll( X, Y, Z ), coll
% 15.30/15.70 ( X, Y, Y ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Z
% 15.30/15.70 Z := Y
% 15.30/15.70 T := Y
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := T
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (629) {G8,W12,D2,L3,V4,M3} R(626,2) { ! coll( X, Y, Z ), !
% 15.30/15.70 coll( X, Y, T ), coll( T, Y, X ) }.
% 15.30/15.70 parent0: (52024) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 15.30/15.70 , ! coll( X, Y, T ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := T
% 15.30/15.70 T := Z
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 1
% 15.30/15.70 1 ==> 2
% 15.30/15.70 2 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 factor: (52027) {G8,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 15.30/15.70 }.
% 15.30/15.70 parent0[0, 1]: (629) {G8,W12,D2,L3,V4,M3} R(626,2) { ! coll( X, Y, Z ), !
% 15.30/15.70 coll( X, Y, T ), coll( T, Y, X ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := Z
% 15.30/15.70 T := Z
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (630) {G9,W8,D2,L2,V3,M2} F(629) { ! coll( X, Y, Z ), coll( Z
% 15.30/15.70 , Y, X ) }.
% 15.30/15.70 parent0: (52027) {G8,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := Z
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 1 ==> 1
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52028) {G8,W8,D2,L2,V3,M2} { coll( Y, Y, X ), ! coll( Z, X, Y
% 15.30/15.70 ) }.
% 15.30/15.70 parent0[0]: (630) {G9,W8,D2,L2,V3,M2} F(629) { ! coll( X, Y, Z ), coll( Z,
% 15.30/15.70 Y, X ) }.
% 15.30/15.70 parent1[1]: (607) {G7,W8,D2,L2,V3,M2} R(605,600) { ! coll( X, Y, Z ), coll
% 15.30/15.70 ( Y, Z, Z ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := Y
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := Z
% 15.30/15.70 Y := X
% 15.30/15.70 Z := Y
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (633) {G10,W8,D2,L2,V3,M2} R(630,607) { coll( X, X, Y ), !
% 15.30/15.70 coll( Z, Y, X ) }.
% 15.30/15.70 parent0: (52028) {G8,W8,D2,L2,V3,M2} { coll( Y, Y, X ), ! coll( Z, X, Y )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := Y
% 15.30/15.70 Y := X
% 15.30/15.70 Z := Z
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 1 ==> 1
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52029) {G1,W14,D2,L2,V6,M2} { eqangle( Z, T, X, Y, Z, T, U, W
% 15.30/15.70 ), ! para( X, Y, U, W ) }.
% 15.30/15.70 parent0[0]: (18) {G0,W18,D2,L2,V8,M2} I { ! eqangle( X, Y, Z, T, U, W, V0,
% 15.30/15.70 V1 ), eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 15.30/15.70 parent1[1]: (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X
% 15.30/15.70 , Y, U, W, Z, T, U, W ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := Z
% 15.30/15.70 T := T
% 15.30/15.70 U := U
% 15.30/15.70 W := W
% 15.30/15.70 V0 := Z
% 15.30/15.70 V1 := T
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := U
% 15.30/15.70 T := W
% 15.30/15.70 U := Z
% 15.30/15.70 W := T
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (722) {G1,W14,D2,L2,V6,M2} R(39,18) { ! para( X, Y, Z, T ),
% 15.30/15.70 eqangle( U, W, X, Y, U, W, Z, T ) }.
% 15.30/15.70 parent0: (52029) {G1,W14,D2,L2,V6,M2} { eqangle( Z, T, X, Y, Z, T, U, W )
% 15.30/15.70 , ! para( X, Y, U, W ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := U
% 15.30/15.70 T := W
% 15.30/15.70 U := Z
% 15.30/15.70 W := T
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 1
% 15.30/15.70 1 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52030) {G1,W14,D2,L2,V1,M2} { ! eqangle( skol22, X, skol22,
% 15.30/15.70 skol27, skol22, X, skol22, skol27 ), cyclic( X, skol27, skol22, skol22 )
% 15.30/15.70 }.
% 15.30/15.70 parent0[1]: (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T, Y
% 15.30/15.70 ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 15.30/15.70 parent1[0]: (534) {G4,W4,D2,L1,V0,M1} R(281,0) { coll( skol22, skol22,
% 15.30/15.70 skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := skol27
% 15.30/15.70 Z := skol22
% 15.30/15.70 T := skol22
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (816) {G5,W14,D2,L2,V1,M2} R(42,534) { ! eqangle( skol22, X,
% 15.30/15.70 skol22, skol27, skol22, X, skol22, skol27 ), cyclic( X, skol27, skol22,
% 15.30/15.70 skol22 ) }.
% 15.30/15.70 parent0: (52030) {G1,W14,D2,L2,V1,M2} { ! eqangle( skol22, X, skol22,
% 15.30/15.70 skol27, skol22, X, skol22, skol27 ), cyclic( X, skol27, skol22, skol22 )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 1 ==> 1
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52031) {G1,W9,D2,L2,V0,M2} { ! coll( skol28, skol25, skol27 )
% 15.30/15.70 , perp( skol25, skol22, skol22, skol27 ) }.
% 15.30/15.70 parent0[0]: (53) {G0,W14,D2,L3,V4,M3} I { ! circle( T, X, Y, Z ), ! coll( T
% 15.30/15.70 , X, Z ), perp( X, Y, Y, Z ) }.
% 15.30/15.70 parent1[0]: (120) {G0,W5,D2,L1,V0,M1} I { circle( skol28, skol25, skol22,
% 15.30/15.70 skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol25
% 15.30/15.70 Y := skol22
% 15.30/15.70 Z := skol27
% 15.30/15.70 T := skol28
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (1597) {G1,W9,D2,L2,V0,M2} R(53,120) { ! coll( skol28, skol25
% 15.30/15.70 , skol27 ), perp( skol25, skol22, skol22, skol27 ) }.
% 15.30/15.70 parent0: (52031) {G1,W9,D2,L2,V0,M2} { ! coll( skol28, skol25, skol27 ),
% 15.30/15.70 perp( skol25, skol22, skol22, skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 1 ==> 1
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52032) {G1,W8,D2,L2,V3,M2} { coll( X, X, Y ), ! alpha1( X, T
% 15.30/15.70 , Y ) }.
% 15.30/15.70 parent0[1]: (633) {G10,W8,D2,L2,V3,M2} R(630,607) { coll( X, X, Y ), ! coll
% 15.30/15.70 ( Z, Y, X ) }.
% 15.30/15.70 parent1[1]: (97) {G0,W11,D3,L2,V4,M2} I { ! alpha1( X, Y, Z ), coll( skol11
% 15.30/15.70 ( X, T, Z ), Z, X ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 Z := skol11( X, Z, Y )
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := X
% 15.30/15.70 Y := T
% 15.30/15.70 Z := Y
% 15.30/15.70 T := Z
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (4262) {G11,W8,D2,L2,V3,M2} R(97,633) { ! alpha1( X, Y, Z ),
% 15.30/15.70 coll( X, X, Z ) }.
% 15.30/15.70 parent0: (52032) {G1,W8,D2,L2,V3,M2} { coll( X, X, Y ), ! alpha1( X, T, Y
% 15.30/15.70 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Z
% 15.30/15.70 Z := T
% 15.30/15.70 T := Y
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 1
% 15.30/15.70 1 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52033) {G1,W7,D3,L1,V0,M1} { perp( skol12( skol25, skol28 ),
% 15.30/15.70 skol25, skol25, skol28 ) }.
% 15.30/15.70 parent0[0]: (100) {G0,W12,D3,L2,V4,M2} I { ! circle( Y, X, Z, T ), perp(
% 15.30/15.70 skol12( X, Y ), X, X, Y ) }.
% 15.30/15.70 parent1[0]: (120) {G0,W5,D2,L1,V0,M1} I { circle( skol28, skol25, skol22,
% 15.30/15.70 skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol25
% 15.30/15.70 Y := skol28
% 15.30/15.70 Z := skol22
% 15.30/15.70 T := skol27
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (4761) {G1,W7,D3,L1,V0,M1} R(100,120) { perp( skol12( skol25,
% 15.30/15.70 skol28 ), skol25, skol25, skol28 ) }.
% 15.30/15.70 parent0: (52033) {G1,W7,D3,L1,V0,M1} { perp( skol12( skol25, skol28 ),
% 15.30/15.70 skol25, skol25, skol28 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52034) {G1,W7,D3,L1,V0,M1} { perp( skol25, skol28, skol12(
% 15.30/15.70 skol25, skol28 ), skol25 ) }.
% 15.30/15.70 parent0[0]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 15.30/15.70 X, Y ) }.
% 15.30/15.70 parent1[0]: (4761) {G1,W7,D3,L1,V0,M1} R(100,120) { perp( skol12( skol25,
% 15.30/15.70 skol28 ), skol25, skol25, skol28 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol12( skol25, skol28 )
% 15.30/15.70 Y := skol25
% 15.30/15.70 Z := skol25
% 15.30/15.70 T := skol28
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (4776) {G2,W7,D3,L1,V0,M1} R(4761,7) { perp( skol25, skol28,
% 15.30/15.70 skol12( skol25, skol28 ), skol25 ) }.
% 15.30/15.70 parent0: (52034) {G1,W7,D3,L1,V0,M1} { perp( skol25, skol28, skol12(
% 15.30/15.70 skol25, skol28 ), skol25 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52035) {G1,W7,D3,L1,V0,M1} { perp( skol25, skol28, skol25,
% 15.30/15.70 skol12( skol25, skol28 ) ) }.
% 15.30/15.70 parent0[0]: (6) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( X, Y,
% 15.30/15.70 T, Z ) }.
% 15.30/15.70 parent1[0]: (4776) {G2,W7,D3,L1,V0,M1} R(4761,7) { perp( skol25, skol28,
% 15.30/15.70 skol12( skol25, skol28 ), skol25 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol25
% 15.30/15.70 Y := skol28
% 15.30/15.70 Z := skol12( skol25, skol28 )
% 15.30/15.70 T := skol25
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (4787) {G3,W7,D3,L1,V0,M1} R(4776,6) { perp( skol25, skol28,
% 15.30/15.70 skol25, skol12( skol25, skol28 ) ) }.
% 15.30/15.70 parent0: (52035) {G1,W7,D3,L1,V0,M1} { perp( skol25, skol28, skol25,
% 15.30/15.70 skol12( skol25, skol28 ) ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52036) {G1,W7,D3,L1,V0,M1} { perp( skol25, skol12( skol25,
% 15.30/15.70 skol28 ), skol25, skol28 ) }.
% 15.30/15.70 parent0[0]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 15.30/15.70 X, Y ) }.
% 15.30/15.70 parent1[0]: (4787) {G3,W7,D3,L1,V0,M1} R(4776,6) { perp( skol25, skol28,
% 15.30/15.70 skol25, skol12( skol25, skol28 ) ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol25
% 15.30/15.70 Y := skol28
% 15.30/15.70 Z := skol25
% 15.30/15.70 T := skol12( skol25, skol28 )
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (4797) {G4,W7,D3,L1,V0,M1} R(4787,7) { perp( skol25, skol12(
% 15.30/15.70 skol25, skol28 ), skol25, skol28 ) }.
% 15.30/15.70 parent0: (52036) {G1,W7,D3,L1,V0,M1} { perp( skol25, skol12( skol25,
% 15.30/15.70 skol28 ), skol25, skol28 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52037) {G1,W11,D3,L2,V0,M2} { ! perp( skol25, skol12( skol25
% 15.30/15.70 , skol28 ), skol25, skol28 ), alpha1( skol25, skol25, skol28 ) }.
% 15.30/15.70 parent0[0]: (96) {G0,W14,D2,L3,V4,M3} I { ! perp( X, T, Y, Z ), ! perp( Y,
% 15.30/15.70 T, X, Z ), alpha1( X, Y, Z ) }.
% 15.30/15.70 parent1[0]: (4797) {G4,W7,D3,L1,V0,M1} R(4787,7) { perp( skol25, skol12(
% 15.30/15.70 skol25, skol28 ), skol25, skol28 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol25
% 15.30/15.70 Y := skol25
% 15.30/15.70 Z := skol28
% 15.30/15.70 T := skol12( skol25, skol28 )
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52038) {G2,W4,D2,L1,V0,M1} { alpha1( skol25, skol25, skol28 )
% 15.30/15.70 }.
% 15.30/15.70 parent0[0]: (52037) {G1,W11,D3,L2,V0,M2} { ! perp( skol25, skol12( skol25
% 15.30/15.70 , skol28 ), skol25, skol28 ), alpha1( skol25, skol25, skol28 ) }.
% 15.30/15.70 parent1[0]: (4797) {G4,W7,D3,L1,V0,M1} R(4787,7) { perp( skol25, skol12(
% 15.30/15.70 skol25, skol28 ), skol25, skol28 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (4959) {G5,W4,D2,L1,V0,M1} R(4797,96);r(4797) { alpha1( skol25
% 15.30/15.70 , skol25, skol28 ) }.
% 15.30/15.70 parent0: (52038) {G2,W4,D2,L1,V0,M1} { alpha1( skol25, skol25, skol28 )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52039) {G6,W4,D2,L1,V0,M1} { coll( skol25, skol25, skol28 )
% 15.30/15.70 }.
% 15.30/15.70 parent0[0]: (4262) {G11,W8,D2,L2,V3,M2} R(97,633) { ! alpha1( X, Y, Z ),
% 15.30/15.70 coll( X, X, Z ) }.
% 15.30/15.70 parent1[0]: (4959) {G5,W4,D2,L1,V0,M1} R(4797,96);r(4797) { alpha1( skol25
% 15.30/15.70 , skol25, skol28 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol25
% 15.30/15.70 Y := skol25
% 15.30/15.70 Z := skol28
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (5132) {G12,W4,D2,L1,V0,M1} R(4959,4262) { coll( skol25,
% 15.30/15.70 skol25, skol28 ) }.
% 15.30/15.70 parent0: (52039) {G6,W4,D2,L1,V0,M1} { coll( skol25, skol25, skol28 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52040) {G6,W4,D2,L1,V0,M1} { coll( skol26, skol28, skol25 )
% 15.30/15.70 }.
% 15.30/15.70 parent0[0]: (308) {G5,W8,D2,L2,V1,M2} R(295,2) { ! coll( skol25, skol25, X
% 15.30/15.70 ), coll( skol26, X, skol25 ) }.
% 15.30/15.70 parent1[0]: (5132) {G12,W4,D2,L1,V0,M1} R(4959,4262) { coll( skol25, skol25
% 15.30/15.70 , skol28 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol28
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (18189) {G13,W4,D2,L1,V0,M1} R(308,5132) { coll( skol26,
% 15.30/15.70 skol28, skol25 ) }.
% 15.30/15.70 parent0: (52040) {G6,W4,D2,L1,V0,M1} { coll( skol26, skol28, skol25 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52041) {G2,W4,D2,L1,V0,M1} { coll( skol25, skol26, skol28 )
% 15.30/15.70 }.
% 15.30/15.70 parent0[1]: (170) {G1,W8,D2,L2,V3,M2} R(1,0) { coll( X, Y, Z ), ! coll( Y,
% 15.30/15.70 Z, X ) }.
% 15.30/15.70 parent1[0]: (18189) {G13,W4,D2,L1,V0,M1} R(308,5132) { coll( skol26, skol28
% 15.30/15.70 , skol25 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol25
% 15.30/15.70 Y := skol26
% 15.30/15.70 Z := skol28
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (18237) {G14,W4,D2,L1,V0,M1} R(18189,170) { coll( skol25,
% 15.30/15.70 skol26, skol28 ) }.
% 15.30/15.70 parent0: (52041) {G2,W4,D2,L1,V0,M1} { coll( skol25, skol26, skol28 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52042) {G5,W4,D2,L1,V0,M1} { coll( skol28, skol27, skol25 )
% 15.30/15.70 }.
% 15.30/15.70 parent0[0]: (214) {G4,W8,D2,L2,V1,M2} R(178,2) { ! coll( skol25, skol26, X
% 15.30/15.70 ), coll( X, skol27, skol25 ) }.
% 15.30/15.70 parent1[0]: (18237) {G14,W4,D2,L1,V0,M1} R(18189,170) { coll( skol25,
% 15.30/15.70 skol26, skol28 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol28
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (18269) {G15,W4,D2,L1,V0,M1} R(18237,214) { coll( skol28,
% 15.30/15.70 skol27, skol25 ) }.
% 15.30/15.70 parent0: (52042) {G5,W4,D2,L1,V0,M1} { coll( skol28, skol27, skol25 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52043) {G1,W4,D2,L1,V0,M1} { coll( skol28, skol25, skol27 )
% 15.30/15.70 }.
% 15.30/15.70 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 15.30/15.70 }.
% 15.30/15.70 parent1[0]: (18269) {G15,W4,D2,L1,V0,M1} R(18237,214) { coll( skol28,
% 15.30/15.70 skol27, skol25 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol28
% 15.30/15.70 Y := skol27
% 15.30/15.70 Z := skol25
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (18321) {G16,W4,D2,L1,V0,M1} R(18269,0) { coll( skol28, skol25
% 15.30/15.70 , skol27 ) }.
% 15.30/15.70 parent0: (52043) {G1,W4,D2,L1,V0,M1} { coll( skol28, skol25, skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52044) {G2,W5,D2,L1,V0,M1} { perp( skol25, skol22, skol22,
% 15.30/15.70 skol27 ) }.
% 15.30/15.70 parent0[0]: (1597) {G1,W9,D2,L2,V0,M2} R(53,120) { ! coll( skol28, skol25,
% 15.30/15.70 skol27 ), perp( skol25, skol22, skol22, skol27 ) }.
% 15.30/15.70 parent1[0]: (18321) {G16,W4,D2,L1,V0,M1} R(18269,0) { coll( skol28, skol25
% 15.30/15.70 , skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (20018) {G17,W5,D2,L1,V0,M1} S(1597);r(18321) { perp( skol25,
% 15.30/15.70 skol22, skol22, skol27 ) }.
% 15.30/15.70 parent0: (52044) {G2,W5,D2,L1,V0,M1} { perp( skol25, skol22, skol22,
% 15.30/15.70 skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52045) {G3,W5,D2,L1,V0,M1} { para( skol22, skol27, skol22,
% 15.30/15.70 skol27 ) }.
% 15.30/15.70 parent0[0]: (307) {G2,W10,D2,L2,V4,M2} F(297) { ! perp( X, Y, Z, T ), para
% 15.30/15.70 ( Z, T, Z, T ) }.
% 15.30/15.70 parent1[0]: (20018) {G17,W5,D2,L1,V0,M1} S(1597);r(18321) { perp( skol25,
% 15.30/15.70 skol22, skol22, skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol25
% 15.30/15.70 Y := skol22
% 15.30/15.70 Z := skol22
% 15.30/15.70 T := skol27
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (23008) {G18,W5,D2,L1,V0,M1} R(20018,307) { para( skol22,
% 15.30/15.70 skol27, skol22, skol27 ) }.
% 15.30/15.70 parent0: (52045) {G3,W5,D2,L1,V0,M1} { para( skol22, skol27, skol22,
% 15.30/15.70 skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52046) {G2,W9,D2,L1,V2,M1} { eqangle( X, Y, skol22, skol27, X
% 15.30/15.70 , Y, skol22, skol27 ) }.
% 15.30/15.70 parent0[0]: (722) {G1,W14,D2,L2,V6,M2} R(39,18) { ! para( X, Y, Z, T ),
% 15.30/15.70 eqangle( U, W, X, Y, U, W, Z, T ) }.
% 15.30/15.70 parent1[0]: (23008) {G18,W5,D2,L1,V0,M1} R(20018,307) { para( skol22,
% 15.30/15.70 skol27, skol22, skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol22
% 15.30/15.70 Y := skol27
% 15.30/15.70 Z := skol22
% 15.30/15.70 T := skol27
% 15.30/15.70 U := X
% 15.30/15.70 W := Y
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (46472) {G19,W9,D2,L1,V2,M1} R(722,23008) { eqangle( X, Y,
% 15.30/15.70 skol22, skol27, X, Y, skol22, skol27 ) }.
% 15.30/15.70 parent0: (52046) {G2,W9,D2,L1,V2,M1} { eqangle( X, Y, skol22, skol27, X, Y
% 15.30/15.70 , skol22, skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52047) {G6,W5,D2,L1,V1,M1} { cyclic( X, skol27, skol22,
% 15.30/15.70 skol22 ) }.
% 15.30/15.70 parent0[0]: (816) {G5,W14,D2,L2,V1,M2} R(42,534) { ! eqangle( skol22, X,
% 15.30/15.70 skol22, skol27, skol22, X, skol22, skol27 ), cyclic( X, skol27, skol22,
% 15.30/15.70 skol22 ) }.
% 15.30/15.70 parent1[0]: (46472) {G19,W9,D2,L1,V2,M1} R(722,23008) { eqangle( X, Y,
% 15.30/15.70 skol22, skol27, X, Y, skol22, skol27 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := skol22
% 15.30/15.70 Y := X
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (51338) {G20,W5,D2,L1,V1,M1} S(816);r(46472) { cyclic( X,
% 15.30/15.70 skol27, skol22, skol22 ) }.
% 15.30/15.70 parent0: (52047) {G6,W5,D2,L1,V1,M1} { cyclic( X, skol27, skol22, skol22 )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52048) {G2,W5,D2,L1,V1,M1} { cyclic( skol27, X, skol22,
% 15.30/15.70 skol22 ) }.
% 15.30/15.70 parent0[1]: (376) {G1,W10,D2,L2,V4,M2} R(15,13) { cyclic( X, Y, Z, T ), !
% 15.30/15.70 cyclic( Y, X, T, Z ) }.
% 15.30/15.70 parent1[0]: (51338) {G20,W5,D2,L1,V1,M1} S(816);r(46472) { cyclic( X,
% 15.30/15.70 skol27, skol22, skol22 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol27
% 15.30/15.70 Y := X
% 15.30/15.70 Z := skol22
% 15.30/15.70 T := skol22
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (51359) {G21,W5,D2,L1,V1,M1} R(51338,376) { cyclic( skol27, X
% 15.30/15.70 , skol22, skol22 ) }.
% 15.30/15.70 parent0: (52048) {G2,W5,D2,L1,V1,M1} { cyclic( skol27, X, skol22, skol22 )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52049) {G3,W5,D2,L1,V1,M1} { cyclic( skol22, X, skol22,
% 15.30/15.70 skol22 ) }.
% 15.30/15.70 parent0[0]: (404) {G2,W10,D2,L2,V4,M2} F(394) { ! cyclic( X, Y, Z, T ),
% 15.30/15.70 cyclic( Z, Y, T, T ) }.
% 15.30/15.70 parent1[0]: (51359) {G21,W5,D2,L1,V1,M1} R(51338,376) { cyclic( skol27, X,
% 15.30/15.70 skol22, skol22 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol27
% 15.30/15.70 Y := X
% 15.30/15.70 Z := skol22
% 15.30/15.70 T := skol22
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (51371) {G22,W5,D2,L1,V1,M1} R(51359,404) { cyclic( skol22, X
% 15.30/15.70 , skol22, skol22 ) }.
% 15.30/15.70 parent0: (52049) {G3,W5,D2,L1,V1,M1} { cyclic( skol22, X, skol22, skol22 )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52050) {G2,W5,D2,L1,V1,M1} { cyclic( skol22, skol22, X,
% 15.30/15.70 skol22 ) }.
% 15.30/15.70 parent0[1]: (374) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), !
% 15.30/15.70 cyclic( Y, Z, X, T ) }.
% 15.30/15.70 parent1[0]: (51371) {G22,W5,D2,L1,V1,M1} R(51359,404) { cyclic( skol22, X,
% 15.30/15.70 skol22, skol22 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol22
% 15.30/15.70 Y := skol22
% 15.30/15.70 Z := X
% 15.30/15.70 T := skol22
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (51393) {G23,W5,D2,L1,V1,M1} R(51371,374) { cyclic( skol22,
% 15.30/15.70 skol22, X, skol22 ) }.
% 15.30/15.70 parent0: (52050) {G2,W5,D2,L1,V1,M1} { cyclic( skol22, skol22, X, skol22 )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52051) {G2,W5,D2,L1,V1,M1} { cyclic( skol22, skol22, skol22,
% 15.30/15.70 X ) }.
% 15.30/15.70 parent0[0]: (365) {G1,W10,D2,L2,V4,M2} R(14,13) { ! cyclic( X, Y, Z, T ),
% 15.30/15.70 cyclic( X, Z, T, Y ) }.
% 15.30/15.70 parent1[0]: (51371) {G22,W5,D2,L1,V1,M1} R(51359,404) { cyclic( skol22, X,
% 15.30/15.70 skol22, skol22 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol22
% 15.30/15.70 Y := X
% 15.30/15.70 Z := skol22
% 15.30/15.70 T := skol22
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (51394) {G23,W5,D2,L1,V1,M1} R(51371,365) { cyclic( skol22,
% 15.30/15.70 skol22, skol22, X ) }.
% 15.30/15.70 parent0: (52051) {G2,W5,D2,L1,V1,M1} { cyclic( skol22, skol22, skol22, X )
% 15.30/15.70 }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52053) {G2,W10,D2,L2,V2,M2} { ! cyclic( skol22, skol22,
% 15.30/15.70 skol22, X ), cyclic( skol22, skol22, X, Y ) }.
% 15.30/15.70 parent0[2]: (399) {G1,W15,D2,L3,V5,M3} R(16,13) { ! cyclic( X, Y, Z, T ),
% 15.30/15.70 cyclic( Y, Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 15.30/15.70 parent1[0]: (51393) {G23,W5,D2,L1,V1,M1} R(51371,374) { cyclic( skol22,
% 15.30/15.70 skol22, X, skol22 ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol22
% 15.30/15.70 Y := skol22
% 15.30/15.70 Z := skol22
% 15.30/15.70 T := X
% 15.30/15.70 U := Y
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := Y
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52054) {G3,W5,D2,L1,V2,M1} { cyclic( skol22, skol22, X, Y )
% 15.30/15.70 }.
% 15.30/15.70 parent0[0]: (52053) {G2,W10,D2,L2,V2,M2} { ! cyclic( skol22, skol22,
% 15.30/15.70 skol22, X ), cyclic( skol22, skol22, X, Y ) }.
% 15.30/15.70 parent1[0]: (51394) {G23,W5,D2,L1,V1,M1} R(51371,365) { cyclic( skol22,
% 15.30/15.70 skol22, skol22, X ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := X
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (51399) {G24,W5,D2,L1,V2,M1} R(51393,399);r(51394) { cyclic(
% 15.30/15.70 skol22, skol22, X, Y ) }.
% 15.30/15.70 parent0: (52054) {G3,W5,D2,L1,V2,M1} { cyclic( skol22, skol22, X, Y ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := X
% 15.30/15.70 Y := Y
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 0 ==> 0
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52055) {G14,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol22,
% 15.30/15.70 skol20, skol23 ) }.
% 15.30/15.70 parent0[0]: (578) {G13,W10,D2,L2,V1,M2} R(576,16) { ! cyclic( X, skol22,
% 15.30/15.70 skol20, skol24 ), ! cyclic( X, skol22, skol20, skol23 ) }.
% 15.30/15.70 parent1[0]: (51399) {G24,W5,D2,L1,V2,M1} R(51393,399);r(51394) { cyclic(
% 15.30/15.70 skol22, skol22, X, Y ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 X := skol22
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := skol20
% 15.30/15.70 Y := skol24
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 resolution: (52057) {G15,W0,D0,L0,V0,M0} { }.
% 15.30/15.70 parent0[0]: (52055) {G14,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol22,
% 15.30/15.70 skol20, skol23 ) }.
% 15.30/15.70 parent1[0]: (51399) {G24,W5,D2,L1,V2,M1} R(51393,399);r(51394) { cyclic(
% 15.30/15.70 skol22, skol22, X, Y ) }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 substitution1:
% 15.30/15.70 X := skol20
% 15.30/15.70 Y := skol23
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 subsumption: (51417) {G25,W0,D0,L0,V0,M0} R(51399,578);r(51399) { }.
% 15.30/15.70 parent0: (52057) {G15,W0,D0,L0,V0,M0} { }.
% 15.30/15.70 substitution0:
% 15.30/15.70 end
% 15.30/15.70 permutation0:
% 15.30/15.70 end
% 15.30/15.70
% 15.30/15.70 Proof check complete!
% 15.30/15.70
% 15.30/15.70 Memory use:
% 15.30/15.70
% 15.30/15.70 space for terms: 699541
% 15.30/15.70 space for clauses: 2253703
% 15.30/15.70
% 15.30/15.70
% 15.30/15.70 clauses generated: 389917
% 15.30/15.70 clauses kept: 51418
% 15.30/15.70 clauses selected: 2677
% 15.30/15.70 clauses deleted: 6027
% 15.30/15.70 clauses inuse deleted: 125
% 15.30/15.70
% 15.30/15.70 subsentry: 19658987
% 15.30/15.70 literals s-matched: 11654084
% 15.30/15.70 literals matched: 6499235
% 15.30/15.70 full subsumption: 2452022
% 15.30/15.70
% 15.30/15.70 checksum: 2128220995
% 15.30/15.70
% 15.30/15.70
% 15.30/15.70 Bliksem ended
%------------------------------------------------------------------------------