%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GEO643+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:55:18 EDT 2022
% Result : Theorem 10.69s 11.12s
% Output : Refutation 10.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO643+1 : TPTP v8.1.0. Released v7.5.0.
% 0.03/0.14 % Command : bliksem %s
% 0.14/0.35 % Computer : n007.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % DateTime : Sat Jun 18 13:37:43 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.77/1.17 *** allocated 10000 integers for termspace/termends
% 0.77/1.17 *** allocated 10000 integers for clauses
% 0.77/1.17 *** allocated 10000 integers for justifications
% 0.77/1.17 Bliksem 1.12
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Automatic Strategy Selection
% 0.77/1.17
% 0.77/1.17 *** allocated 15000 integers for termspace/termends
% 0.77/1.17
% 0.77/1.17 Clauses:
% 0.77/1.17
% 0.77/1.17 { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 0.77/1.17 { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 0.77/1.17 { ! coll( X, T, Y ), ! coll( X, T, Z ), coll( Y, Z, X ) }.
% 0.77/1.17 { ! para( X, Y, Z, T ), para( X, Y, T, Z ) }.
% 0.77/1.17 { ! para( X, Y, Z, T ), para( Z, T, X, Y ) }.
% 0.77/1.17 { ! para( X, Y, U, W ), ! para( U, W, Z, T ), para( X, Y, Z, T ) }.
% 0.77/1.17 { ! perp( X, Y, Z, T ), perp( X, Y, T, Z ) }.
% 0.77/1.17 { ! perp( X, Y, Z, T ), perp( Z, T, X, Y ) }.
% 0.77/1.17 { ! perp( X, Y, U, W ), ! perp( U, W, Z, T ), para( X, Y, Z, T ) }.
% 0.77/1.17 { ! para( X, Y, U, W ), ! perp( U, W, Z, T ), perp( X, Y, Z, T ) }.
% 0.77/1.17 { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 0.77/1.17 { ! cong( T, X, T, Y ), ! cong( T, X, T, Z ), circle( T, X, Y, Z ) }.
% 0.77/1.17 { ! cong( U, X, U, Y ), ! cong( U, X, U, Z ), ! cong( U, X, U, T ), cyclic
% 0.77/1.17 ( X, Y, Z, T ) }.
% 0.77/1.17 { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z ) }.
% 0.77/1.17 { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T ) }.
% 0.77/1.17 { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T ) }.
% 0.77/1.17 { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 0.77/1.17 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( Y, X, Z, T, U, W, V0, V1
% 0.77/1.17 ) }.
% 0.77/1.17 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( Z, T, X, Y, V0, V1, U, W
% 0.77/1.17 ) }.
% 0.77/1.17 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( U, W, V0, V1, X, Y, Z, T
% 0.77/1.17 ) }.
% 0.77/1.17 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), eqangle( X, Y, U, W, Z, T, V0, V1
% 0.77/1.17 ) }.
% 0.77/1.17 { ! eqangle( X, Y, Z, T, V2, V3, V4, V5 ), ! eqangle( V2, V3, V4, V5, U, W
% 0.77/1.17 , V0, V1 ), eqangle( X, Y, Z, T, U, W, V0, V1 ) }.
% 0.77/1.17 { ! cong( X, Y, Z, T ), cong( X, Y, T, Z ) }.
% 0.77/1.17 { ! cong( X, Y, Z, T ), cong( Z, T, X, Y ) }.
% 0.77/1.17 { ! cong( X, Y, U, W ), ! cong( U, W, Z, T ), cong( X, Y, Z, T ) }.
% 0.77/1.17 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( Y, X, Z, T, U, W, V0, V1
% 0.77/1.17 ) }.
% 0.77/1.17 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( Z, T, X, Y, V0, V1, U, W
% 0.77/1.17 ) }.
% 0.77/1.17 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( U, W, V0, V1, X, Y, Z, T
% 0.77/1.17 ) }.
% 0.77/1.17 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), eqratio( X, Y, U, W, Z, T, V0, V1
% 0.77/1.17 ) }.
% 0.77/1.17 { ! eqratio( X, Y, Z, T, V2, V3, V4, V5 ), ! eqratio( V2, V3, V4, V5, U, W
% 0.77/1.17 , V0, V1 ), eqratio( X, Y, Z, T, U, W, V0, V1 ) }.
% 0.77/1.17 { ! simtri( X, Z, Y, T, W, U ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.17 { ! simtri( Y, X, Z, U, T, W ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.17 { ! simtri( T, U, W, X, Y, Z ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.17 { ! simtri( X, Y, Z, V0, V1, V2 ), ! simtri( V0, V1, V2, T, U, W ), simtri
% 0.77/1.17 ( X, Y, Z, T, U, W ) }.
% 0.77/1.17 { ! contri( X, Z, Y, T, W, U ), contri( X, Y, Z, T, U, W ) }.
% 0.77/1.17 { ! contri( Y, X, Z, U, T, W ), contri( X, Y, Z, T, U, W ) }.
% 0.77/1.17 { ! contri( T, U, W, X, Y, Z ), contri( X, Y, Z, T, U, W ) }.
% 0.77/1.17 { ! contri( X, Y, Z, V0, V1, V2 ), ! contri( V0, V1, V2, T, U, W ), contri
% 0.77/1.17 ( X, Y, Z, T, U, W ) }.
% 0.77/1.17 { ! eqangle( X, Y, U, W, Z, T, U, W ), para( X, Y, Z, T ) }.
% 0.77/1.17 { ! para( X, Y, Z, T ), eqangle( X, Y, U, W, Z, T, U, W ) }.
% 0.77/1.17 { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z, Y, T, X, T, Y ) }.
% 0.77/1.17 { ! eqangle( Z, X, Z, Y, T, X, T, Y ), coll( Z, T, X ), cyclic( X, Y, Z, T
% 0.77/1.17 ) }.
% 0.77/1.17 { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll( Z, T, Y ), cyclic( X, Y, Z,
% 0.77/1.17 T ) }.
% 0.77/1.17 { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U, T ), ! cyclic( X, Y, U, W ), !
% 0.77/1.17 eqangle( U, X, U, Y, W, Z, W, T ), cong( X, Y, Z, T ) }.
% 0.77/1.17 { ! midp( Z, U, X ), ! midp( T, U, Y ), para( Z, T, X, Y ) }.
% 0.77/1.17 { ! midp( U, X, T ), ! para( U, Z, T, Y ), ! coll( Z, X, Y ), midp( Z, X, Y
% 0.77/1.17 ) }.
% 0.77/1.17 { ! cong( Z, X, Z, Y ), eqangle( Z, X, X, Y, X, Y, Z, Y ) }.
% 0.77/1.17 { ! eqangle( Z, X, X, Y, X, Y, Z, Y ), coll( Z, X, Y ), cong( Z, X, Z, Y )
% 0.77/1.17 }.
% 0.77/1.17 { ! circle( U, X, Y, Z ), ! perp( U, X, X, T ), eqangle( X, T, X, Y, Z, X,
% 0.77/1.17 Z, Y ) }.
% 0.77/1.17 { ! circle( Y, X, T, U ), ! eqangle( X, Z, X, T, U, X, U, T ), perp( Y, X,
% 0.77/1.17 X, Z ) }.
% 0.77/1.17 { ! circle( T, X, Y, Z ), ! midp( U, Y, Z ), eqangle( X, Y, X, Z, T, Y, T,
% 0.77/1.17 U ) }.
% 0.77/1.17 { ! circle( U, T, X, Y ), ! coll( Z, X, Y ), ! eqangle( T, X, T, Y, U, X, U
% 0.77/1.17 , Z ), midp( Z, X, Y ) }.
% 0.77/1.17 { ! perp( X, Y, Y, T ), ! midp( Z, X, T ), cong( X, Z, Y, Z ) }.
% 0.77/1.17 { ! circle( T, X, Y, Z ), ! coll( T, X, Z ), perp( X, Y, Y, Z ) }.
% 0.77/1.17 { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T ), eqangle( X, T, Z, T, Z, T,
% 0.77/1.17 Z, Y ) }.
% 0.77/1.17 { ! midp( T, X, Y ), ! perp( Z, T, X, Y ), cong( Z, X, Z, Y ) }.
% 0.77/1.17 { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T ), perp( X, Y, Z, T ) }.
% 0.77/1.17 { ! cong( X, Y, T, Y ), ! cong( X, Z, T, Z ), ! cyclic( X, T, Y, Z ), perp
% 0.77/1.17 ( Y, X, X, Z ) }.
% 0.77/1.17 { ! eqangle( X, Y, Y, Z, T, U, U, W ), ! eqangle( X, Z, Y, Z, T, W, U, W )
% 0.77/1.17 , coll( X, Y, Z ), simtri( X, Y, Z, T, U, W ) }.
% 0.77/1.17 { ! simtri( X, Y, Z, T, U, W ), eqratio( X, Y, X, Z, T, U, T, W ) }.
% 0.77/1.17 { ! simtri( X, Y, Z, T, U, W ), eqangle( X, Y, Y, Z, T, U, U, W ) }.
% 0.77/1.17 { ! simtri( X, Y, Z, T, U, W ), ! cong( X, Y, T, U ), contri( X, Y, Z, T, U
% 0.77/1.17 , W ) }.
% 0.77/1.17 { ! contri( X, Y, U, Z, T, W ), cong( X, Y, Z, T ) }.
% 0.77/1.17 { ! midp( U, X, Y ), ! midp( U, Z, T ), para( X, Z, Y, T ) }.
% 0.77/1.17 { ! midp( Z, T, U ), ! para( T, X, U, Y ), ! para( T, Y, U, X ), midp( Z, X
% 0.77/1.17 , Y ) }.
% 0.77/1.17 { ! para( X, Y, Z, T ), ! coll( U, X, Z ), ! coll( U, Y, T ), eqratio( U, X
% 0.77/1.17 , X, Z, U, Y, Y, T ) }.
% 0.77/1.17 { ! para( X, Y, X, Z ), coll( X, Y, Z ) }.
% 0.77/1.17 { ! cong( X, Y, X, Z ), ! coll( X, Y, Z ), midp( X, Y, Z ) }.
% 0.77/1.17 { ! midp( X, Y, Z ), cong( X, Y, X, Z ) }.
% 0.77/1.17 { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 0.77/1.17 { ! midp( U, X, Y ), ! midp( W, Z, T ), eqratio( U, X, X, Y, W, Z, Z, T ) }
% 0.77/1.17 .
% 0.77/1.17 { ! eqangle( X, Y, Z, T, Z, T, X, Y ), para( X, Y, Z, T ), perp( X, Y, Z, T
% 0.77/1.17 ) }.
% 0.77/1.17 { ! eqangle( X, Y, Z, T, Z, T, X, Y ), perp( X, Y, Z, T ), para( X, Y, Z, T
% 0.77/1.17 ) }.
% 0.77/1.17 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), ! para( U, W, V0, V1 ), para( X, Y
% 0.77/1.17 , Z, T ) }.
% 0.77/1.17 { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), ! perp( U, W, V0, V1 ), perp( X, Y
% 0.77/1.17 , Z, T ) }.
% 0.77/1.17 { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), ! cong( U, W, V0, V1 ), cong( X, Y
% 0.77/1.17 , Z, T ) }.
% 0.77/1.17 { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z, Y, Z, X, Z ), coll( skol1( U
% 0.77/1.17 , W, Z, T ), Z, T ) }.
% 0.77/1.17 { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z, Y, Z, X, Z ), coll( skol1( X
% 0.77/1.17 , Y, Z, T ), X, Y ) }.
% 0.77/1.17 { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( skol2( U
% 0.77/1.17 , W, Z, T ), Z, T ) }.
% 0.77/1.17 { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( Y, X,
% 0.77/1.17 skol2( X, Y, Z, T ) ) }.
% 0.77/1.17 { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( skol3( U
% 0.77/1.17 , W, Z, T ), Z, T ) }.
% 0.77/1.17 { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T, Z, T, Z, Y ), coll( Y, X,
% 0.77/1.17 skol3( X, Y, Z, T ) ) }.
% 0.77/1.17 { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y ), coll( skol4( U, W, Z, T ), Z
% 0.77/1.17 , T ) }.
% 0.77/1.17 { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y ), coll( Y, X, skol4( X, Y, Z, T
% 0.77/1.17 ) ) }.
% 0.77/1.17 { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll( X, Y, Z ), cyclic( T, Y, Z,
% 0.77/1.17 skol5( W, Y, Z, T ) ) }.
% 0.77/1.17 { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll( X, Y, Z ), eqangle( X, Z, Y, Z
% 0.77/1.17 , X, skol5( X, Y, Z, T ), Y, skol5( X, Y, Z, T ) ) }.
% 0.77/1.17 { ! midp( U, X, Y ), ! midp( W, Z, T ), midp( skol6( X, V0, V1, T, V2, V3 )
% 0.77/1.17 , X, T ) }.
% 0.77/1.17 { ! midp( U, X, Y ), ! midp( W, Z, T ), para( skol6( X, V0, Z, T, V1, W ),
% 0.77/1.17 W, X, Z ) }.
% 0.77/1.17 { ! midp( U, X, Y ), ! midp( W, Z, T ), para( skol6( X, Y, Z, T, U, W ), U
% 0.77/1.17 , Y, T ) }.
% 0.77/1.17 { ! midp( Z, X, Y ), ! midp( W, T, U ), ! coll( T, X, Y ), ! coll( U, X, Y
% 0.77/1.17 ), midp( skol7( X, V0 ), X, V0 ) }.
% 0.77/1.17 { ! midp( T, X, U ), ! para( X, W, Z, T ), ! para( X, W, U, Y ), ! coll( W
% 0.77/1.17 , Y, Z ), coll( skol8( V0, V1, Z, T ), T, Z ) }.
% 0.77/1.17 { ! midp( T, X, U ), ! para( X, W, Z, T ), ! para( X, W, U, Y ), ! coll( W
% 0.77/1.17 , Y, Z ), coll( skol8( X, Y, Z, T ), X, Y ) }.
% 0.77/1.17 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), cong( T, Z, T, skol9( W, V0,
% 0.77/1.17 Z, T ) ) }.
% 0.77/1.17 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), cong( Y, Z, Y, skol9( W, Y, Z
% 0.77/1.17 , T ) ) }.
% 0.77/1.17 { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T ), para( skol9( X, Y, Z, T ), Z
% 0.77/1.17 , X, Y ) }.
% 0.77/1.17 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), coll( skol10( U, Y, Z ), Z, Y
% 0.77/1.17 ) }.
% 0.77/1.17 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), perp( X, skol10( X, Y, Z ), Z
% 0.77/1.17 , Y ) }.
% 0.77/1.17 { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ), alpha1( X, Y, Z ) }.
% 0.77/1.17 { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z ), Z, X ) }.
% 0.77/1.17 { ! alpha1( X, Y, Z ), perp( Y, skol11( X, Y, Z ), Z, X ) }.
% 0.77/1.17 { ! coll( T, Z, X ), ! perp( Y, T, Z, X ), alpha1( X, Y, Z ) }.
% 0.77/1.17 { ! circle( Y, X, Z, T ), perp( skol12( X, Y ), X, X, Y ) }.
% 3.92/4.33 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 3.92/4.33 , alpha2( X, Z, U, skol13( X, V0, Z, V1, U ) ) }.
% 3.92/4.33 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 3.92/4.33 , coll( skol21( V0, Y, T, V1 ), Y, T ) }.
% 3.92/4.33 { ! circle( W, X, Y, Z ), ! cong( W, X, W, T ), ! cong( U, X, U, Y ), W = U
% 3.92/4.33 , cong( skol21( X, Y, T, U ), U, U, X ) }.
% 3.92/4.33 { ! alpha2( X, Y, Z, T ), coll( T, X, Y ) }.
% 3.92/4.33 { ! alpha2( X, Y, Z, T ), cong( T, Z, Z, X ) }.
% 3.92/4.33 { ! coll( T, X, Y ), ! cong( T, Z, Z, X ), alpha2( X, Y, Z, T ) }.
% 3.92/4.33 { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T ), ! midp( U, X, Y ), circle(
% 3.92/4.33 skol14( X, Y, Z ), X, Y, Z ) }.
% 3.92/4.33 { ! perp( X, Z, Z, Y ), ! cyclic( X, Y, Z, T ), circle( skol15( X, Y, Z ),
% 3.92/4.33 X, Y, Z ) }.
% 3.92/4.33 { ! perp( X, U, U, T ), ! coll( T, Y, Z ), coll( skol16( W, Y, Z ), Y, Z )
% 3.92/4.33 }.
% 3.92/4.33 { ! perp( X, U, U, T ), ! coll( T, Y, Z ), perp( skol16( X, Y, Z ), X, Y, Z
% 3.92/4.33 ) }.
% 3.92/4.33 { ! perp( X, Z, X, Y ), ! perp( Y, X, Y, T ), ! midp( U, Z, T ), midp(
% 3.92/4.33 skol17( X, Y ), X, Y ) }.
% 3.92/4.33 { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z ), coll( X, Y, skol18( X, Y ) )
% 3.92/4.33 }.
% 3.92/4.33 { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z ), cong( Y, X, Y, skol18( X, Y )
% 3.92/4.33 ) }.
% 3.92/4.33 { ! para( U, W, X, Y ), ! coll( Z, U, X ), ! coll( Z, W, Y ), ! coll( T, U
% 3.92/4.33 , W ), coll( Z, T, skol19( V0, V1, Z, T ) ) }.
% 3.92/4.33 { ! para( U, W, X, Y ), ! coll( Z, U, X ), ! coll( Z, W, Y ), ! coll( T, U
% 3.92/4.33 , W ), coll( skol19( X, Y, Z, T ), X, Y ) }.
% 3.92/4.33 { coll( skol27, skol25, skol26 ) }.
% 3.92/4.33 { coll( skol29, skol25, skol28 ) }.
% 3.92/4.33 { coll( skol30, skol26, skol29 ) }.
% 3.92/4.33 { coll( skol30, skol27, skol28 ) }.
% 3.92/4.33 { circle( skol20, skol28, skol29, skol30 ) }.
% 3.92/4.33 { circle( skol22, skol25, skol27, skol28 ) }.
% 3.92/4.33 { circle( skol23, skol26, skol27, skol30 ) }.
% 3.92/4.33 { circle( skol24, skol26, skol25, skol29 ) }.
% 3.92/4.33 { ! cyclic( skol23, skol24, skol22, skol20 ) }.
% 3.92/4.33
% 3.92/4.33 percentage equality = 0.008746, percentage horn = 0.928000
% 3.92/4.33 This is a problem with some equality
% 3.92/4.33
% 3.92/4.33
% 3.92/4.33
% 3.92/4.33 Options Used:
% 3.92/4.33
% 3.92/4.33 useres = 1
% 3.92/4.33 useparamod = 1
% 3.92/4.33 useeqrefl = 1
% 3.92/4.33 useeqfact = 1
% 3.92/4.33 usefactor = 1
% 3.92/4.33 usesimpsplitting = 0
% 3.92/4.33 usesimpdemod = 5
% 3.92/4.33 usesimpres = 3
% 3.92/4.33
% 3.92/4.33 resimpinuse = 1000
% 3.92/4.33 resimpclauses = 20000
% 3.92/4.33 substype = eqrewr
% 3.92/4.33 backwardsubs = 1
% 3.92/4.33 selectoldest = 5
% 3.92/4.33
% 3.92/4.33 litorderings [0] = split
% 3.92/4.33 litorderings [1] = extend the termordering, first sorting on arguments
% 3.92/4.33
% 3.92/4.33 termordering = kbo
% 3.92/4.33
% 3.92/4.33 litapriori = 0
% 3.92/4.33 termapriori = 1
% 3.92/4.33 litaposteriori = 0
% 3.92/4.33 termaposteriori = 0
% 3.92/4.33 demodaposteriori = 0
% 3.92/4.33 ordereqreflfact = 0
% 3.92/4.33
% 3.92/4.33 litselect = negord
% 3.92/4.33
% 3.92/4.33 maxweight = 15
% 3.92/4.33 maxdepth = 30000
% 3.92/4.33 maxlength = 115
% 3.92/4.33 maxnrvars = 195
% 3.92/4.33 excuselevel = 1
% 3.92/4.33 increasemaxweight = 1
% 3.92/4.33
% 3.92/4.33 maxselected = 10000000
% 3.92/4.33 maxnrclauses = 10000000
% 3.92/4.33
% 3.92/4.33 showgenerated = 0
% 3.92/4.33 showkept = 0
% 3.92/4.33 showselected = 0
% 3.92/4.33 showdeleted = 0
% 3.92/4.33 showresimp = 1
% 3.92/4.33 showstatus = 2000
% 3.92/4.33
% 3.92/4.33 prologoutput = 0
% 3.92/4.33 nrgoals = 5000000
% 3.92/4.33 totalproof = 1
% 3.92/4.33
% 3.92/4.33 Symbols occurring in the translation:
% 3.92/4.33
% 3.92/4.33 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 3.92/4.33 . [1, 2] (w:1, o:41, a:1, s:1, b:0),
% 3.92/4.33 ! [4, 1] (w:0, o:36, a:1, s:1, b:0),
% 3.92/4.33 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.92/4.33 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.92/4.33 coll [38, 3] (w:1, o:69, a:1, s:1, b:0),
% 3.92/4.33 para [40, 4] (w:1, o:77, a:1, s:1, b:0),
% 3.92/4.33 perp [43, 4] (w:1, o:78, a:1, s:1, b:0),
% 3.92/4.33 midp [45, 3] (w:1, o:70, a:1, s:1, b:0),
% 3.92/4.33 cong [47, 4] (w:1, o:79, a:1, s:1, b:0),
% 3.92/4.33 circle [48, 4] (w:1, o:80, a:1, s:1, b:0),
% 3.92/4.33 cyclic [49, 4] (w:1, o:81, a:1, s:1, b:0),
% 3.92/4.33 eqangle [54, 8] (w:1, o:96, a:1, s:1, b:0),
% 3.92/4.33 eqratio [57, 8] (w:1, o:97, a:1, s:1, b:0),
% 3.92/4.33 simtri [59, 6] (w:1, o:93, a:1, s:1, b:0),
% 3.92/4.33 contri [60, 6] (w:1, o:94, a:1, s:1, b:0),
% 3.92/4.33 alpha1 [66, 3] (w:1, o:71, a:1, s:1, b:1),
% 3.92/4.33 alpha2 [67, 4] (w:1, o:82, a:1, s:1, b:1),
% 3.92/4.33 skol1 [68, 4] (w:1, o:83, a:1, s:1, b:1),
% 3.92/4.33 skol2 [69, 4] (w:1, o:85, a:1, s:1, b:1),
% 3.92/4.33 skol3 [70, 4] (w:1, o:87, a:1, s:1, b:1),
% 3.92/4.33 skol4 [71, 4] (w:1, o:88, a:1, s:1, b:1),
% 3.92/4.33 skol5 [72, 4] (w:1, o:89, a:1, s:1, b:1),
% 3.92/4.33 skol6 [73, 6] (w:1, o:95, a:1, s:1, b:1),
% 3.92/4.33 skol7 [74, 2] (w:1, o:65, a:1, s:1, b:1),
% 10.69/11.12 skol8 [75, 4] (w:1, o:90, a:1, s:1, b:1),
% 10.69/11.12 skol9 [76, 4] (w:1, o:91, a:1, s:1, b:1),
% 10.69/11.12 skol10 [77, 3] (w:1, o:72, a:1, s:1, b:1),
% 10.69/11.12 skol11 [78, 3] (w:1, o:73, a:1, s:1, b:1),
% 10.69/11.12 skol12 [79, 2] (w:1, o:66, a:1, s:1, b:1),
% 10.69/11.12 skol13 [80, 5] (w:1, o:92, a:1, s:1, b:1),
% 10.69/11.12 skol14 [81, 3] (w:1, o:74, a:1, s:1, b:1),
% 10.69/11.12 skol15 [82, 3] (w:1, o:75, a:1, s:1, b:1),
% 10.69/11.12 skol16 [83, 3] (w:1, o:76, a:1, s:1, b:1),
% 10.69/11.12 skol17 [84, 2] (w:1, o:67, a:1, s:1, b:1),
% 10.69/11.12 skol18 [85, 2] (w:1, o:68, a:1, s:1, b:1),
% 10.69/11.12 skol19 [86, 4] (w:1, o:84, a:1, s:1, b:1),
% 10.69/11.12 skol20 [87, 0] (w:1, o:26, a:1, s:1, b:1),
% 10.69/11.12 skol21 [88, 4] (w:1, o:86, a:1, s:1, b:1),
% 10.69/11.12 skol22 [89, 0] (w:1, o:27, a:1, s:1, b:1),
% 10.69/11.12 skol23 [90, 0] (w:1, o:28, a:1, s:1, b:1),
% 10.69/11.12 skol24 [91, 0] (w:1, o:29, a:1, s:1, b:1),
% 10.69/11.12 skol25 [92, 0] (w:1, o:30, a:1, s:1, b:1),
% 10.69/11.12 skol26 [93, 0] (w:1, o:31, a:1, s:1, b:1),
% 10.69/11.12 skol27 [94, 0] (w:1, o:32, a:1, s:1, b:1),
% 10.69/11.12 skol28 [95, 0] (w:1, o:33, a:1, s:1, b:1),
% 10.69/11.12 skol29 [96, 0] (w:1, o:34, a:1, s:1, b:1),
% 10.69/11.12 skol30 [97, 0] (w:1, o:35, a:1, s:1, b:1).
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Starting Search:
% 10.69/11.12
% 10.69/11.12 *** allocated 15000 integers for clauses
% 10.69/11.12 *** allocated 22500 integers for clauses
% 10.69/11.12 *** allocated 33750 integers for clauses
% 10.69/11.12 *** allocated 50625 integers for clauses
% 10.69/11.12 *** allocated 22500 integers for termspace/termends
% 10.69/11.12 *** allocated 75937 integers for clauses
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 *** allocated 33750 integers for termspace/termends
% 10.69/11.12 *** allocated 113905 integers for clauses
% 10.69/11.12 *** allocated 50625 integers for termspace/termends
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 13028
% 10.69/11.12 Kept: 2005
% 10.69/11.12 Inuse: 330
% 10.69/11.12 Deleted: 1
% 10.69/11.12 Deletedinuse: 1
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 *** allocated 170857 integers for clauses
% 10.69/11.12 *** allocated 75937 integers for termspace/termends
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 *** allocated 256285 integers for clauses
% 10.69/11.12 *** allocated 113905 integers for termspace/termends
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 34715
% 10.69/11.12 Kept: 4009
% 10.69/11.12 Inuse: 471
% 10.69/11.12 Deleted: 1
% 10.69/11.12 Deletedinuse: 1
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 *** allocated 170857 integers for termspace/termends
% 10.69/11.12 *** allocated 384427 integers for clauses
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 48628
% 10.69/11.12 Kept: 6009
% 10.69/11.12 Inuse: 533
% 10.69/11.12 Deleted: 1
% 10.69/11.12 Deletedinuse: 1
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 66577
% 10.69/11.12 Kept: 8037
% 10.69/11.12 Inuse: 685
% 10.69/11.12 Deleted: 2
% 10.69/11.12 Deletedinuse: 1
% 10.69/11.12
% 10.69/11.12 *** allocated 576640 integers for clauses
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 *** allocated 256285 integers for termspace/termends
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 87082
% 10.69/11.12 Kept: 10048
% 10.69/11.12 Inuse: 791
% 10.69/11.12 Deleted: 9
% 10.69/11.12 Deletedinuse: 3
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 98655
% 10.69/11.12 Kept: 12156
% 10.69/11.12 Inuse: 855
% 10.69/11.12 Deleted: 15
% 10.69/11.12 Deletedinuse: 9
% 10.69/11.12
% 10.69/11.12 *** allocated 864960 integers for clauses
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 107714
% 10.69/11.12 Kept: 14157
% 10.69/11.12 Inuse: 904
% 10.69/11.12 Deleted: 15
% 10.69/11.12 Deletedinuse: 9
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 *** allocated 384427 integers for termspace/termends
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 125532
% 10.69/11.12 Kept: 16163
% 10.69/11.12 Inuse: 1057
% 10.69/11.12 Deleted: 17
% 10.69/11.12 Deletedinuse: 9
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 140914
% 10.69/11.12 Kept: 18167
% 10.69/11.12 Inuse: 1218
% 10.69/11.12 Deleted: 35
% 10.69/11.12 Deletedinuse: 15
% 10.69/11.12
% 10.69/11.12 *** allocated 1297440 integers for clauses
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying clauses:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 151957
% 10.69/11.12 Kept: 20178
% 10.69/11.12 Inuse: 1318
% 10.69/11.12 Deleted: 1228
% 10.69/11.12 Deletedinuse: 29
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 163564
% 10.69/11.12 Kept: 22185
% 10.69/11.12 Inuse: 1421
% 10.69/11.12 Deleted: 1246
% 10.69/11.12 Deletedinuse: 47
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 175888
% 10.69/11.12 Kept: 24195
% 10.69/11.12 Inuse: 1531
% 10.69/11.12 Deleted: 1254
% 10.69/11.12 Deletedinuse: 54
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 191042
% 10.69/11.12 Kept: 26195
% 10.69/11.12 Inuse: 1661
% 10.69/11.12 Deleted: 1270
% 10.69/11.12 Deletedinuse: 70
% 10.69/11.12
% 10.69/11.12 *** allocated 576640 integers for termspace/termends
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 *** allocated 1946160 integers for clauses
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 205372
% 10.69/11.12 Kept: 28200
% 10.69/11.12 Inuse: 1808
% 10.69/11.12 Deleted: 1282
% 10.69/11.12 Deletedinuse: 82
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 221934
% 10.69/11.12 Kept: 30211
% 10.69/11.12 Inuse: 1967
% 10.69/11.12 Deleted: 1294
% 10.69/11.12 Deletedinuse: 94
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 240553
% 10.69/11.12 Kept: 33856
% 10.69/11.12 Inuse: 2133
% 10.69/11.12 Deleted: 1294
% 10.69/11.12 Deletedinuse: 94
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 244564
% 10.69/11.12 Kept: 36129
% 10.69/11.12 Inuse: 2138
% 10.69/11.12 Deleted: 1294
% 10.69/11.12 Deletedinuse: 94
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 254000
% 10.69/11.12 Kept: 38967
% 10.69/11.12 Inuse: 2153
% 10.69/11.12 Deleted: 1294
% 10.69/11.12 Deletedinuse: 94
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying clauses:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 *** allocated 2919240 integers for clauses
% 10.69/11.12 *** allocated 864960 integers for termspace/termends
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 274982
% 10.69/11.12 Kept: 42990
% 10.69/11.12 Inuse: 2206
% 10.69/11.12 Deleted: 4602
% 10.69/11.12 Deletedinuse: 102
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 283877
% 10.69/11.12 Kept: 45669
% 10.69/11.12 Inuse: 2290
% 10.69/11.12 Deleted: 4608
% 10.69/11.12 Deletedinuse: 107
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 293480
% 10.69/11.12 Kept: 47682
% 10.69/11.12 Inuse: 2366
% 10.69/11.12 Deleted: 4612
% 10.69/11.12 Deletedinuse: 108
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 305856
% 10.69/11.12 Kept: 49693
% 10.69/11.12 Inuse: 2470
% 10.69/11.12 Deleted: 4622
% 10.69/11.12 Deletedinuse: 115
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 318650
% 10.69/11.12 Kept: 51699
% 10.69/11.12 Inuse: 2589
% 10.69/11.12 Deleted: 4640
% 10.69/11.12 Deletedinuse: 121
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Intermediate Status:
% 10.69/11.12 Generated: 345350
% 10.69/11.12 Kept: 53706
% 10.69/11.12 Inuse: 2774
% 10.69/11.12 Deleted: 4674
% 10.69/11.12 Deletedinuse: 133
% 10.69/11.12
% 10.69/11.12 Resimplifying inuse:
% 10.69/11.12 Done
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Bliksems!, er is een bewijs:
% 10.69/11.12 % SZS status Theorem
% 10.69/11.12 % SZS output start Refutation
% 10.69/11.12
% 10.69/11.12 (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 10.69/11.12 (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 10.69/11.12 (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z ), coll( Y
% 10.69/11.12 , Z, X ) }.
% 10.69/11.12 (6) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( X, Y, T, Z ) }.
% 10.69/11.12 (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T, X, Y ) }.
% 10.69/11.12 (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U, W, Z, T ),
% 10.69/11.12 para( X, Y, Z, T ) }.
% 10.69/11.12 (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z )
% 10.69/11.12 }.
% 10.69/11.12 (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T )
% 10.69/11.12 }.
% 10.69/11.12 (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T )
% 10.69/11.12 }.
% 10.69/11.12 (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y, T
% 10.69/11.12 ), cyclic( X, Y, Z, T ) }.
% 10.69/11.12 (18) {G0,W18,D2,L2,V8,M2} I { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 10.69/11.12 eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 10.69/11.12 (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X, Y, U, W, Z
% 10.69/11.12 , T, U, W ) }.
% 10.69/11.12 (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll(
% 10.69/11.12 Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 10.69/11.12 (53) {G0,W14,D2,L3,V4,M3} I { ! circle( T, X, Y, Z ), ! coll( T, X, Z ),
% 10.69/11.12 perp( X, Y, Y, Z ) }.
% 10.69/11.12 (96) {G0,W14,D2,L3,V4,M3} I { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z ),
% 10.69/11.12 alpha1( X, Y, Z ) }.
% 10.69/11.12 (97) {G0,W11,D3,L2,V4,M2} I { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z )
% 10.69/11.12 , Z, X ) }.
% 10.69/11.12 (100) {G0,W12,D3,L2,V4,M2} I { ! circle( Y, X, Z, T ), perp( skol12( X, Y )
% 10.69/11.12 , X, X, Y ) }.
% 10.69/11.12 (118) {G0,W4,D2,L1,V0,M1} I { coll( skol30, skol26, skol29 ) }.
% 10.69/11.12 (119) {G0,W4,D2,L1,V0,M1} I { coll( skol30, skol27, skol28 ) }.
% 10.69/11.12 (120) {G0,W5,D2,L1,V0,M1} I { circle( skol20, skol28, skol29, skol30 ) }.
% 10.69/11.12 (124) {G0,W5,D2,L1,V0,M1} I { ! cyclic( skol23, skol24, skol22, skol20 )
% 10.69/11.12 }.
% 10.69/11.12 (125) {G1,W8,D2,L2,V3,M2} F(2) { ! coll( X, Y, Z ), coll( Z, Z, X ) }.
% 10.69/11.12 (171) {G1,W8,D2,L2,V3,M2} R(1,0) { ! coll( X, Y, Z ), coll( Y, Z, X ) }.
% 10.69/11.12 (201) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll( X, Y, T ),
% 10.69/11.12 coll( Z, X, T ) }.
% 10.69/11.12 (210) {G2,W8,D2,L2,V3,M2} F(201) { ! coll( X, Y, Z ), coll( Z, X, Z ) }.
% 10.69/11.12 (265) {G3,W12,D2,L3,V4,M3} R(210,2) { coll( X, Y, X ), ! coll( X, Z, Y ), !
% 10.69/11.12 coll( X, Z, T ) }.
% 10.69/11.12 (280) {G3,W4,D2,L1,V0,M1} R(210,118) { coll( skol29, skol30, skol29 ) }.
% 10.69/11.12 (281) {G3,W4,D2,L1,V0,M1} R(210,119) { coll( skol28, skol30, skol28 ) }.
% 10.69/11.12 (282) {G4,W8,D2,L2,V3,M2} F(265) { coll( X, Y, X ), ! coll( X, Z, Y ) }.
% 10.69/11.12 (297) {G1,W15,D2,L3,V6,M3} R(8,7) { ! perp( X, Y, Z, T ), para( U, W, Z, T
% 10.69/11.12 ), ! perp( X, Y, U, W ) }.
% 10.69/11.12 (307) {G2,W10,D2,L2,V4,M2} F(297) { ! perp( X, Y, Z, T ), para( Z, T, Z, T
% 10.69/11.12 ) }.
% 10.69/11.12 (364) {G1,W10,D2,L2,V4,M2} R(14,13) { ! cyclic( X, Y, Z, T ), cyclic( X, Z
% 10.69/11.12 , T, Y ) }.
% 10.69/11.12 (374) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), ! cyclic( Y, Z
% 10.69/11.12 , X, T ) }.
% 10.69/11.12 (376) {G1,W10,D2,L2,V4,M2} R(15,13) { cyclic( X, Y, Z, T ), ! cyclic( Y, X
% 10.69/11.12 , T, Z ) }.
% 10.69/11.12 (378) {G1,W5,D2,L1,V0,M1} R(15,124) { ! cyclic( skol24, skol23, skol22,
% 10.69/11.12 skol20 ) }.
% 10.69/11.12 (394) {G1,W15,D2,L3,V5,M3} R(16,15) { ! cyclic( X, Y, Z, T ), ! cyclic( X,
% 10.69/11.12 Y, Z, U ), cyclic( Z, Y, T, U ) }.
% 10.69/11.12 (399) {G1,W15,D2,L3,V5,M3} R(16,13) { ! cyclic( X, Y, Z, T ), cyclic( Y, Z
% 10.69/11.12 , T, U ), ! cyclic( X, Y, U, Z ) }.
% 10.69/11.12 (404) {G2,W10,D2,L2,V4,M2} F(394) { ! cyclic( X, Y, Z, T ), cyclic( Z, Y, T
% 10.69/11.12 , T ) }.
% 10.69/11.12 (528) {G4,W4,D2,L1,V0,M1} R(280,0) { coll( skol29, skol29, skol30 ) }.
% 10.69/11.12 (534) {G4,W4,D2,L1,V0,M1} R(281,0) { coll( skol28, skol28, skol30 ) }.
% 10.69/11.12 (536) {G5,W8,D2,L2,V1,M2} R(534,2) { ! coll( skol28, skol28, X ), coll(
% 10.69/11.12 skol30, X, skol28 ) }.
% 10.69/11.12 (539) {G2,W5,D2,L1,V0,M1} R(378,14) { ! cyclic( skol24, skol22, skol23,
% 10.69/11.12 skol20 ) }.
% 10.69/11.12 (545) {G3,W5,D2,L1,V0,M1} R(539,15) { ! cyclic( skol22, skol24, skol23,
% 10.69/11.12 skol20 ) }.
% 10.69/11.12 (548) {G4,W5,D2,L1,V0,M1} R(545,14) { ! cyclic( skol22, skol23, skol24,
% 10.69/11.12 skol20 ) }.
% 10.69/11.12 (552) {G5,W5,D2,L1,V0,M1} R(548,13) { ! cyclic( skol22, skol23, skol20,
% 10.69/11.12 skol24 ) }.
% 10.69/11.12 (553) {G6,W5,D2,L1,V0,M1} R(552,15) { ! cyclic( skol23, skol22, skol20,
% 10.69/11.12 skol24 ) }.
% 10.69/11.12 (559) {G7,W5,D2,L1,V0,M1} R(553,14) { ! cyclic( skol23, skol20, skol22,
% 10.69/11.12 skol24 ) }.
% 10.69/11.12 (561) {G8,W5,D2,L1,V0,M1} R(559,15) { ! cyclic( skol20, skol23, skol22,
% 10.69/11.12 skol24 ) }.
% 10.69/11.12 (564) {G9,W5,D2,L1,V0,M1} R(561,14) { ! cyclic( skol20, skol22, skol23,
% 10.69/11.12 skol24 ) }.
% 10.69/11.12 (568) {G10,W5,D2,L1,V0,M1} R(564,13) { ! cyclic( skol20, skol22, skol24,
% 10.69/11.12 skol23 ) }.
% 10.69/11.12 (573) {G11,W5,D2,L1,V0,M1} R(568,14) { ! cyclic( skol20, skol24, skol22,
% 10.69/11.12 skol23 ) }.
% 10.69/11.12 (576) {G12,W5,D2,L1,V0,M1} R(573,15) { ! cyclic( skol24, skol20, skol22,
% 10.69/11.12 skol23 ) }.
% 10.69/11.12 (578) {G13,W10,D2,L2,V1,M2} R(576,16) { ! cyclic( X, skol24, skol20, skol22
% 10.69/11.12 ), ! cyclic( X, skol24, skol20, skol23 ) }.
% 10.69/11.12 (600) {G5,W8,D2,L2,V3,M2} R(282,1) { ! coll( X, Y, Z ), coll( Z, X, X ) }.
% 10.69/11.12 (605) {G6,W8,D2,L2,V3,M2} R(600,1) { coll( X, Y, Y ), ! coll( Z, Y, X ) }.
% 10.69/11.12 (606) {G6,W8,D2,L2,V3,M2} R(600,0) { coll( X, Y, Y ), ! coll( Y, X, Z ) }.
% 10.69/11.12 (626) {G7,W8,D2,L2,V3,M2} R(606,606) { ! coll( X, Y, Z ), coll( X, Y, Y )
% 10.69/11.12 }.
% 10.69/11.12 (629) {G8,W12,D2,L3,V4,M3} R(626,2) { ! coll( X, Y, Z ), ! coll( X, Y, T )
% 10.69/11.12 , coll( T, Y, X ) }.
% 10.69/11.12 (630) {G9,W8,D2,L2,V3,M2} F(629) { ! coll( X, Y, Z ), coll( Z, Y, X ) }.
% 10.69/11.12 (634) {G10,W8,D2,L2,V3,M2} R(630,605) { coll( X, X, Y ), ! coll( Z, X, Y )
% 10.69/11.12 }.
% 10.69/11.12 (722) {G1,W14,D2,L2,V6,M2} R(39,18) { ! para( X, Y, Z, T ), eqangle( U, W,
% 10.69/11.12 X, Y, U, W, Z, T ) }.
% 10.69/11.12 (819) {G5,W14,D2,L2,V1,M2} R(42,528) { ! eqangle( skol29, X, skol29, skol30
% 10.69/11.12 , skol29, X, skol29, skol30 ), cyclic( X, skol30, skol29, skol29 ) }.
% 10.69/11.12 (990) {G6,W8,D2,L2,V2,M2} R(536,125) { coll( skol30, X, skol28 ), ! coll( X
% 10.69/11.12 , Y, skol28 ) }.
% 10.69/11.12 (1264) {G7,W8,D2,L2,V2,M2} R(990,171) { ! coll( X, Y, skol28 ), coll( X,
% 10.69/11.12 skol28, skol30 ) }.
% 10.69/11.12 (1306) {G11,W8,D2,L2,V2,M2} R(1264,634) { coll( X, skol28, skol30 ), ! coll
% 10.69/11.12 ( Y, X, skol28 ) }.
% 10.69/11.12 (1597) {G1,W9,D2,L2,V0,M2} R(53,120) { ! coll( skol20, skol28, skol30 ),
% 10.69/11.12 perp( skol28, skol29, skol29, skol30 ) }.
% 10.69/11.12 (4229) {G12,W8,D2,L2,V2,M2} R(97,1306) { ! alpha1( skol28, X, Y ), coll( Y
% 10.69/11.12 , skol28, skol30 ) }.
% 10.69/11.12 (4767) {G1,W7,D3,L1,V0,M1} R(100,120) { perp( skol12( skol28, skol20 ),
% 10.69/11.12 skol28, skol28, skol20 ) }.
% 10.69/11.12 (4783) {G2,W7,D3,L1,V0,M1} R(4767,7) { perp( skol28, skol20, skol12( skol28
% 10.69/11.12 , skol20 ), skol28 ) }.
% 10.69/11.12 (4794) {G3,W7,D3,L1,V0,M1} R(4783,6) { perp( skol28, skol20, skol28, skol12
% 10.69/11.12 ( skol28, skol20 ) ) }.
% 10.69/11.12 (4804) {G4,W7,D3,L1,V0,M1} R(4794,7) { perp( skol28, skol12( skol28, skol20
% 10.69/11.12 ), skol28, skol20 ) }.
% 10.69/11.12 (5469) {G5,W4,D2,L1,V0,M1} R(4804,96);r(4804) { alpha1( skol28, skol28,
% 10.69/11.12 skol20 ) }.
% 10.69/11.12 (5478) {G13,W4,D2,L1,V0,M1} R(5469,4229) { coll( skol20, skol28, skol30 )
% 10.69/11.12 }.
% 10.69/11.12 (20004) {G14,W5,D2,L1,V0,M1} S(1597);r(5478) { perp( skol28, skol29, skol29
% 10.69/11.12 , skol30 ) }.
% 10.69/11.12 (26759) {G15,W5,D2,L1,V0,M1} R(20004,307) { para( skol29, skol30, skol29,
% 10.69/11.12 skol30 ) }.
% 10.69/11.12 (47969) {G16,W9,D2,L1,V2,M1} R(722,26759) { eqangle( X, Y, skol29, skol30,
% 10.69/11.12 X, Y, skol29, skol30 ) }.
% 10.69/11.12 (54239) {G17,W5,D2,L1,V1,M1} S(819);r(47969) { cyclic( X, skol30, skol29,
% 10.69/11.12 skol29 ) }.
% 10.69/11.12 (54260) {G18,W5,D2,L1,V1,M1} R(54239,376) { cyclic( skol30, X, skol29,
% 10.69/11.12 skol29 ) }.
% 10.69/11.12 (54272) {G19,W5,D2,L1,V1,M1} R(54260,404) { cyclic( skol29, X, skol29,
% 10.69/11.12 skol29 ) }.
% 10.69/11.12 (54294) {G20,W5,D2,L1,V1,M1} R(54272,374) { cyclic( skol29, skol29, X,
% 10.69/11.12 skol29 ) }.
% 10.69/11.12 (54295) {G20,W5,D2,L1,V1,M1} R(54272,364) { cyclic( skol29, skol29, skol29
% 10.69/11.12 , X ) }.
% 10.69/11.12 (54300) {G21,W5,D2,L1,V2,M1} R(54294,399);r(54295) { cyclic( skol29, skol29
% 10.69/11.12 , X, Y ) }.
% 10.69/11.12 (54322) {G22,W5,D2,L1,V3,M1} R(54300,399);r(54300) { cyclic( skol29, X, Y,
% 10.69/11.12 Z ) }.
% 10.69/11.12 (54338) {G23,W0,D0,L0,V0,M0} R(54322,578);r(54322) { }.
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 % SZS output end Refutation
% 10.69/11.12 found a proof!
% 10.69/11.12
% 10.69/11.12
% 10.69/11.12 Unprocessed initial clauses:
% 10.69/11.12
% 10.69/11.12 (54340) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( X, Z, Y ) }.
% 10.69/11.12 (54341) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Y, X, Z ) }.
% 10.69/11.12 (54342) {G0,W12,D2,L3,V4,M3} { ! coll( X, T, Y ), ! coll( X, T, Z ), coll
% 10.69/11.12 ( Y, Z, X ) }.
% 10.69/11.12 (54343) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( X, Y, T, Z )
% 10.69/11.12 }.
% 10.69/11.12 (54344) {G0,W10,D2,L2,V4,M2} { ! para( X, Y, Z, T ), para( Z, T, X, Y )
% 10.69/11.12 }.
% 10.69/11.12 (54345) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! para( U, W, Z, T )
% 10.69/11.12 , para( X, Y, Z, T ) }.
% 10.69/11.12 (54346) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( X, Y, T, Z )
% 10.69/11.12 }.
% 10.69/11.12 (54347) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( Z, T, X, Y )
% 10.69/11.12 }.
% 10.69/11.12 (54348) {G0,W15,D2,L3,V6,M3} { ! perp( X, Y, U, W ), ! perp( U, W, Z, T )
% 10.69/11.12 , para( X, Y, Z, T ) }.
% 10.69/11.12 (54349) {G0,W15,D2,L3,V6,M3} { ! para( X, Y, U, W ), ! perp( U, W, Z, T )
% 10.69/11.12 , perp( X, Y, Z, T ) }.
% 10.69/11.12 (54350) {G0,W8,D2,L2,V3,M2} { ! midp( Z, Y, X ), midp( Z, X, Y ) }.
% 10.69/11.12 (54351) {G0,W15,D2,L3,V4,M3} { ! cong( T, X, T, Y ), ! cong( T, X, T, Z )
% 10.69/11.12 , circle( T, X, Y, Z ) }.
% 10.69/11.12 (54352) {G0,W20,D2,L4,V5,M4} { ! cong( U, X, U, Y ), ! cong( U, X, U, Z )
% 10.69/11.12 , ! cong( U, X, U, T ), cyclic( X, Y, Z, T ) }.
% 10.69/11.12 (54353) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X, Y, T, Z
% 10.69/11.12 ) }.
% 10.69/11.12 (54354) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X, Z, Y, T
% 10.69/11.12 ) }.
% 10.69/11.12 (54355) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Y, X, Z, T
% 10.69/11.12 ) }.
% 10.69/11.12 (54356) {G0,W15,D2,L3,V5,M3} { ! cyclic( U, X, Y, Z ), ! cyclic( U, X, Y,
% 10.69/11.12 T ), cyclic( X, Y, Z, T ) }.
% 10.69/11.12 (54357) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 10.69/11.12 eqangle( Y, X, Z, T, U, W, V0, V1 ) }.
% 10.69/11.12 (54358) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 10.69/11.12 eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 10.69/11.12 (54359) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 10.69/11.12 eqangle( U, W, V0, V1, X, Y, Z, T ) }.
% 10.69/11.12 (54360) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ),
% 10.69/11.12 eqangle( X, Y, U, W, Z, T, V0, V1 ) }.
% 10.69/11.12 (54361) {G0,W27,D2,L3,V12,M3} { ! eqangle( X, Y, Z, T, V2, V3, V4, V5 ), !
% 10.69/11.12 eqangle( V2, V3, V4, V5, U, W, V0, V1 ), eqangle( X, Y, Z, T, U, W, V0,
% 10.69/11.12 V1 ) }.
% 10.69/11.12 (54362) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( X, Y, T, Z )
% 10.69/11.12 }.
% 10.69/11.12 (54363) {G0,W10,D2,L2,V4,M2} { ! cong( X, Y, Z, T ), cong( Z, T, X, Y )
% 10.69/11.12 }.
% 10.69/11.12 (54364) {G0,W15,D2,L3,V6,M3} { ! cong( X, Y, U, W ), ! cong( U, W, Z, T )
% 10.69/11.12 , cong( X, Y, Z, T ) }.
% 10.69/11.12 (54365) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 10.69/11.12 eqratio( Y, X, Z, T, U, W, V0, V1 ) }.
% 10.69/11.12 (54366) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 10.69/11.12 eqratio( Z, T, X, Y, V0, V1, U, W ) }.
% 10.69/11.12 (54367) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 10.69/11.12 eqratio( U, W, V0, V1, X, Y, Z, T ) }.
% 10.69/11.12 (54368) {G0,W18,D2,L2,V8,M2} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ),
% 10.69/11.12 eqratio( X, Y, U, W, Z, T, V0, V1 ) }.
% 10.69/11.12 (54369) {G0,W27,D2,L3,V12,M3} { ! eqratio( X, Y, Z, T, V2, V3, V4, V5 ), !
% 10.69/11.12 eqratio( V2, V3, V4, V5, U, W, V0, V1 ), eqratio( X, Y, Z, T, U, W, V0,
% 10.69/11.12 V1 ) }.
% 10.69/11.12 (54370) {G0,W14,D2,L2,V6,M2} { ! simtri( X, Z, Y, T, W, U ), simtri( X, Y
% 10.69/11.12 , Z, T, U, W ) }.
% 10.69/11.12 (54371) {G0,W14,D2,L2,V6,M2} { ! simtri( Y, X, Z, U, T, W ), simtri( X, Y
% 10.69/11.12 , Z, T, U, W ) }.
% 10.69/11.12 (54372) {G0,W14,D2,L2,V6,M2} { ! simtri( T, U, W, X, Y, Z ), simtri( X, Y
% 10.69/11.12 , Z, T, U, W ) }.
% 10.69/11.12 (54373) {G0,W21,D2,L3,V9,M3} { ! simtri( X, Y, Z, V0, V1, V2 ), ! simtri(
% 10.69/11.12 V0, V1, V2, T, U, W ), simtri( X, Y, Z, T, U, W ) }.
% 10.69/11.12 (54374) {G0,W14,D2,L2,V6,M2} { ! contri( X, Z, Y, T, W, U ), contri( X, Y
% 10.69/11.12 , Z, T, U, W ) }.
% 10.69/11.12 (54375) {G0,W14,D2,L2,V6,M2} { ! contri( Y, X, Z, U, T, W ), contri( X, Y
% 10.69/11.12 , Z, T, U, W ) }.
% 10.69/11.12 (54376) {G0,W14,D2,L2,V6,M2} { ! contri( T, U, W, X, Y, Z ), contri( X, Y
% 10.69/11.12 , Z, T, U, W ) }.
% 10.69/11.12 (54377) {G0,W21,D2,L3,V9,M3} { ! contri( X, Y, Z, V0, V1, V2 ), ! contri(
% 10.69/11.12 V0, V1, V2, T, U, W ), contri( X, Y, Z, T, U, W ) }.
% 10.69/11.12 (54378) {G0,W14,D2,L2,V6,M2} { ! eqangle( X, Y, U, W, Z, T, U, W ), para(
% 10.69/11.12 X, Y, Z, T ) }.
% 10.69/11.12 (54379) {G0,W14,D2,L2,V6,M2} { ! para( X, Y, Z, T ), eqangle( X, Y, U, W,
% 10.69/11.12 Z, T, U, W ) }.
% 10.69/11.12 (54380) {G0,W14,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), eqangle( Z, X, Z, Y
% 10.69/11.12 , T, X, T, Y ) }.
% 10.69/11.12 (54381) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y ), coll(
% 10.69/11.12 Z, T, X ), cyclic( X, Y, Z, T ) }.
% 10.69/11.12 (54382) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y ), ! coll
% 10.69/11.12 ( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 10.69/11.12 (54383) {G0,W29,D2,L5,V6,M5} { ! cyclic( X, Y, U, Z ), ! cyclic( X, Y, U,
% 10.69/11.12 T ), ! cyclic( X, Y, U, W ), ! eqangle( U, X, U, Y, W, Z, W, T ), cong( X
% 10.69/11.12 , Y, Z, T ) }.
% 10.69/11.12 (54384) {G0,W13,D2,L3,V5,M3} { ! midp( Z, U, X ), ! midp( T, U, Y ), para
% 10.69/11.12 ( Z, T, X, Y ) }.
% 10.69/11.12 (54385) {G0,W17,D2,L4,V5,M4} { ! midp( U, X, T ), ! para( U, Z, T, Y ), !
% 10.69/11.12 coll( Z, X, Y ), midp( Z, X, Y ) }.
% 10.69/11.12 (54386) {G0,W14,D2,L2,V3,M2} { ! cong( Z, X, Z, Y ), eqangle( Z, X, X, Y,
% 10.69/11.12 X, Y, Z, Y ) }.
% 10.69/11.12 (54387) {G0,W18,D2,L3,V3,M3} { ! eqangle( Z, X, X, Y, X, Y, Z, Y ), coll(
% 10.69/11.12 Z, X, Y ), cong( Z, X, Z, Y ) }.
% 10.69/11.12 (54388) {G0,W19,D2,L3,V5,M3} { ! circle( U, X, Y, Z ), ! perp( U, X, X, T
% 10.69/11.12 ), eqangle( X, T, X, Y, Z, X, Z, Y ) }.
% 10.69/11.12 (54389) {G0,W19,D2,L3,V5,M3} { ! circle( Y, X, T, U ), ! eqangle( X, Z, X
% 10.69/11.12 , T, U, X, U, T ), perp( Y, X, X, Z ) }.
% 10.69/11.12 (54390) {G0,W18,D2,L3,V5,M3} { ! circle( T, X, Y, Z ), ! midp( U, Y, Z ),
% 10.69/11.12 eqangle( X, Y, X, Z, T, Y, T, U ) }.
% 10.69/11.12 (54391) {G0,W22,D2,L4,V5,M4} { ! circle( U, T, X, Y ), ! coll( Z, X, Y ),
% 10.69/11.12 ! eqangle( T, X, T, Y, U, X, U, Z ), midp( Z, X, Y ) }.
% 10.69/11.12 (54392) {G0,W14,D2,L3,V4,M3} { ! perp( X, Y, Y, T ), ! midp( Z, X, T ),
% 10.69/11.12 cong( X, Z, Y, Z ) }.
% 10.69/11.12 (54393) {G0,W14,D2,L3,V4,M3} { ! circle( T, X, Y, Z ), ! coll( T, X, Z ),
% 10.69/11.12 perp( X, Y, Y, Z ) }.
% 10.69/11.12 (54394) {G0,W19,D2,L3,V4,M3} { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T
% 10.69/11.12 ), eqangle( X, T, Z, T, Z, T, Z, Y ) }.
% 10.69/11.12 (54395) {G0,W14,D2,L3,V4,M3} { ! midp( T, X, Y ), ! perp( Z, T, X, Y ),
% 10.69/11.12 cong( Z, X, Z, Y ) }.
% 10.69/11.12 (54396) {G0,W15,D2,L3,V4,M3} { ! cong( X, Z, Y, Z ), ! cong( X, T, Y, T )
% 10.69/11.12 , perp( X, Y, Z, T ) }.
% 10.69/11.12 (54397) {G0,W20,D2,L4,V4,M4} { ! cong( X, Y, T, Y ), ! cong( X, Z, T, Z )
% 10.69/11.12 , ! cyclic( X, T, Y, Z ), perp( Y, X, X, Z ) }.
% 10.69/11.12 (54398) {G0,W29,D2,L4,V6,M4} { ! eqangle( X, Y, Y, Z, T, U, U, W ), !
% 10.69/11.12 eqangle( X, Z, Y, Z, T, W, U, W ), coll( X, Y, Z ), simtri( X, Y, Z, T, U
% 10.69/11.12 , W ) }.
% 10.69/11.12 (54399) {G0,W16,D2,L2,V6,M2} { ! simtri( X, Y, Z, T, U, W ), eqratio( X, Y
% 10.69/11.12 , X, Z, T, U, T, W ) }.
% 10.69/11.12 (54400) {G0,W16,D2,L2,V6,M2} { ! simtri( X, Y, Z, T, U, W ), eqangle( X, Y
% 10.69/11.12 , Y, Z, T, U, U, W ) }.
% 10.69/11.12 (54401) {G0,W19,D2,L3,V6,M3} { ! simtri( X, Y, Z, T, U, W ), ! cong( X, Y
% 10.69/11.12 , T, U ), contri( X, Y, Z, T, U, W ) }.
% 10.69/11.12 (54402) {G0,W12,D2,L2,V6,M2} { ! contri( X, Y, U, Z, T, W ), cong( X, Y, Z
% 10.69/11.12 , T ) }.
% 10.69/11.12 (54403) {G0,W13,D2,L3,V5,M3} { ! midp( U, X, Y ), ! midp( U, Z, T ), para
% 10.69/11.12 ( X, Z, Y, T ) }.
% 10.69/11.12 (54404) {G0,W18,D2,L4,V5,M4} { ! midp( Z, T, U ), ! para( T, X, U, Y ), !
% 10.69/11.12 para( T, Y, U, X ), midp( Z, X, Y ) }.
% 10.69/11.12 (54405) {G0,W22,D2,L4,V5,M4} { ! para( X, Y, Z, T ), ! coll( U, X, Z ), !
% 10.69/11.12 coll( U, Y, T ), eqratio( U, X, X, Z, U, Y, Y, T ) }.
% 10.69/11.12 (54406) {G0,W9,D2,L2,V3,M2} { ! para( X, Y, X, Z ), coll( X, Y, Z ) }.
% 10.69/11.12 (54407) {G0,W13,D2,L3,V3,M3} { ! cong( X, Y, X, Z ), ! coll( X, Y, Z ),
% 10.69/11.12 midp( X, Y, Z ) }.
% 10.69/11.12 (54408) {G0,W9,D2,L2,V3,M2} { ! midp( X, Y, Z ), cong( X, Y, X, Z ) }.
% 10.69/11.12 (54409) {G0,W8,D2,L2,V3,M2} { ! midp( X, Y, Z ), coll( X, Y, Z ) }.
% 10.69/11.12 (54410) {G0,W17,D2,L3,V6,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ),
% 10.69/11.12 eqratio( U, X, X, Y, W, Z, Z, T ) }.
% 10.69/11.12 (54411) {G0,W19,D2,L3,V4,M3} { ! eqangle( X, Y, Z, T, Z, T, X, Y ), para(
% 10.69/11.12 X, Y, Z, T ), perp( X, Y, Z, T ) }.
% 10.69/11.12 (54412) {G0,W19,D2,L3,V4,M3} { ! eqangle( X, Y, Z, T, Z, T, X, Y ), perp(
% 10.69/11.13 X, Y, Z, T ), para( X, Y, Z, T ) }.
% 10.69/11.13 (54413) {G0,W19,D2,L3,V8,M3} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), !
% 10.69/11.13 para( U, W, V0, V1 ), para( X, Y, Z, T ) }.
% 10.69/11.13 (54414) {G0,W19,D2,L3,V8,M3} { ! eqangle( X, Y, Z, T, U, W, V0, V1 ), !
% 10.69/11.13 perp( U, W, V0, V1 ), perp( X, Y, Z, T ) }.
% 10.69/11.13 (54415) {G0,W19,D2,L3,V8,M3} { ! eqratio( X, Y, Z, T, U, W, V0, V1 ), !
% 10.69/11.13 cong( U, W, V0, V1 ), cong( X, Y, Z, T ) }.
% 10.69/11.13 (54416) {G0,W22,D3,L3,V6,M3} { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z
% 10.69/11.13 , Y, Z, X, Z ), coll( skol1( U, W, Z, T ), Z, T ) }.
% 10.69/11.13 (54417) {G0,W22,D3,L3,V4,M3} { ! perp( Z, Y, Y, X ), ! eqangle( T, Z, Y, Z
% 10.69/11.13 , Y, Z, X, Z ), coll( skol1( X, Y, Z, T ), X, Y ) }.
% 10.69/11.13 (54418) {G0,W22,D3,L3,V6,M3} { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T
% 10.69/11.13 , Z, T, Z, Y ), coll( skol2( U, W, Z, T ), Z, T ) }.
% 10.69/11.13 (54419) {G0,W22,D3,L3,V4,M3} { ! cong( Z, X, Z, Y ), ! eqangle( X, Z, Z, T
% 10.69/11.13 , Z, T, Z, Y ), coll( Y, X, skol2( X, Y, Z, T ) ) }.
% 10.69/11.13 (54420) {G0,W22,D3,L3,V6,M3} { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T
% 10.69/11.13 , Z, T, Z, Y ), coll( skol3( U, W, Z, T ), Z, T ) }.
% 10.69/11.13 (54421) {G0,W22,D3,L3,V4,M3} { ! perp( Z, T, X, Y ), ! eqangle( X, Z, Z, T
% 10.69/11.13 , Z, T, Z, Y ), coll( Y, X, skol3( X, Y, Z, T ) ) }.
% 10.69/11.13 (54422) {G0,W18,D3,L3,V6,M3} { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y )
% 10.69/11.13 , coll( skol4( U, W, Z, T ), Z, T ) }.
% 10.69/11.13 (54423) {G0,W18,D3,L3,V4,M3} { ! perp( Z, T, X, Y ), ! cong( Z, X, Z, Y )
% 10.69/11.13 , coll( Y, X, skol4( X, Y, Z, T ) ) }.
% 10.69/11.13 (54424) {G0,W22,D3,L3,V6,M3} { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll(
% 10.69/11.13 X, Y, Z ), cyclic( T, Y, Z, skol5( W, Y, Z, T ) ) }.
% 10.69/11.13 (54425) {G0,W30,D3,L3,V5,M3} { ! eqangle( X, Z, Y, Z, X, T, Y, U ), coll(
% 10.69/11.13 X, Y, Z ), eqangle( X, Z, Y, Z, X, skol5( X, Y, Z, T ), Y, skol5( X, Y, Z
% 10.69/11.13 , T ) ) }.
% 10.69/11.13 (54426) {G0,W18,D3,L3,V10,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), midp
% 10.69/11.13 ( skol6( X, V0, V1, T, V2, V3 ), X, T ) }.
% 10.69/11.13 (54427) {G0,W19,D3,L3,V8,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), para
% 10.69/11.13 ( skol6( X, V0, Z, T, V1, W ), W, X, Z ) }.
% 10.69/11.13 (54428) {G0,W19,D3,L3,V6,M3} { ! midp( U, X, Y ), ! midp( W, Z, T ), para
% 10.69/11.13 ( skol6( X, Y, Z, T, U, W ), U, Y, T ) }.
% 10.69/11.13 (54429) {G0,W22,D3,L5,V7,M5} { ! midp( Z, X, Y ), ! midp( W, T, U ), !
% 10.69/11.13 coll( T, X, Y ), ! coll( U, X, Y ), midp( skol7( X, V0 ), X, V0 ) }.
% 10.69/11.13 (54430) {G0,W26,D3,L5,V8,M5} { ! midp( T, X, U ), ! para( X, W, Z, T ), !
% 10.69/11.13 para( X, W, U, Y ), ! coll( W, Y, Z ), coll( skol8( V0, V1, Z, T ), T, Z
% 10.69/11.13 ) }.
% 10.69/11.13 (54431) {G0,W26,D3,L5,V6,M5} { ! midp( T, X, U ), ! para( X, W, Z, T ), !
% 10.69/11.13 para( X, W, U, Y ), ! coll( W, Y, Z ), coll( skol8( X, Y, Z, T ), X, Y )
% 10.69/11.13 }.
% 10.69/11.13 (54432) {G0,W19,D3,L3,V7,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 10.69/11.13 , cong( T, Z, T, skol9( W, V0, Z, T ) ) }.
% 10.69/11.13 (54433) {G0,W19,D3,L3,V6,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 10.69/11.13 , cong( Y, Z, Y, skol9( W, Y, Z, T ) ) }.
% 10.69/11.13 (54434) {G0,W19,D3,L3,V5,M3} { ! cong( T, Z, T, U ), ! perp( X, Y, Y, T )
% 10.69/11.13 , para( skol9( X, Y, Z, T ), Z, X, Y ) }.
% 10.69/11.13 (54435) {G0,W17,D3,L3,V5,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 10.69/11.13 , coll( skol10( U, Y, Z ), Z, Y ) }.
% 10.69/11.13 (54436) {G0,W18,D3,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 10.69/11.13 , perp( X, skol10( X, Y, Z ), Z, Y ) }.
% 10.69/11.13 (54437) {G0,W14,D2,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T, X, Z )
% 10.69/11.13 , alpha1( X, Y, Z ) }.
% 10.69/11.13 (54438) {G0,W11,D3,L2,V4,M2} { ! alpha1( X, Y, Z ), coll( skol11( X, T, Z
% 10.69/11.13 ), Z, X ) }.
% 10.69/11.13 (54439) {G0,W12,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), perp( Y, skol11( X, Y
% 10.69/11.13 , Z ), Z, X ) }.
% 10.69/11.13 (54440) {G0,W13,D2,L3,V4,M3} { ! coll( T, Z, X ), ! perp( Y, T, Z, X ),
% 10.69/11.13 alpha1( X, Y, Z ) }.
% 10.69/11.13 (54441) {G0,W12,D3,L2,V4,M2} { ! circle( Y, X, Z, T ), perp( skol12( X, Y
% 10.69/11.13 ), X, X, Y ) }.
% 10.69/11.13 (54442) {G0,W28,D3,L5,V8,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 10.69/11.13 ), ! cong( U, X, U, Y ), W = U, alpha2( X, Z, U, skol13( X, V0, Z, V1, U
% 10.69/11.13 ) ) }.
% 10.69/11.13 (54443) {G0,W26,D3,L5,V8,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 10.69/11.13 ), ! cong( U, X, U, Y ), W = U, coll( skol21( V0, Y, T, V1 ), Y, T ) }.
% 10.69/11.13 (54444) {G0,W27,D3,L5,V6,M5} { ! circle( W, X, Y, Z ), ! cong( W, X, W, T
% 10.69/11.13 ), ! cong( U, X, U, Y ), W = U, cong( skol21( X, Y, T, U ), U, U, X )
% 10.69/11.13 }.
% 10.69/11.13 (54445) {G0,W9,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), coll( T, X, Y ) }.
% 10.69/11.13 (54446) {G0,W10,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), cong( T, Z, Z, X )
% 10.69/11.13 }.
% 10.69/11.13 (54447) {G0,W14,D2,L3,V4,M3} { ! coll( T, X, Y ), ! cong( T, Z, Z, X ),
% 10.69/11.13 alpha2( X, Y, Z, T ) }.
% 10.69/11.13 (54448) {G0,W22,D3,L4,V5,M4} { ! cyclic( X, Y, Z, T ), ! para( X, Y, Z, T
% 10.69/11.13 ), ! midp( U, X, Y ), circle( skol14( X, Y, Z ), X, Y, Z ) }.
% 10.69/11.13 (54449) {G0,W18,D3,L3,V4,M3} { ! perp( X, Z, Z, Y ), ! cyclic( X, Y, Z, T
% 10.69/11.13 ), circle( skol15( X, Y, Z ), X, Y, Z ) }.
% 10.69/11.13 (54450) {G0,W16,D3,L3,V6,M3} { ! perp( X, U, U, T ), ! coll( T, Y, Z ),
% 10.69/11.13 coll( skol16( W, Y, Z ), Y, Z ) }.
% 10.69/11.13 (54451) {G0,W17,D3,L3,V5,M3} { ! perp( X, U, U, T ), ! coll( T, Y, Z ),
% 10.69/11.13 perp( skol16( X, Y, Z ), X, Y, Z ) }.
% 10.69/11.13 (54452) {G0,W20,D3,L4,V5,M4} { ! perp( X, Z, X, Y ), ! perp( Y, X, Y, T )
% 10.69/11.13 , ! midp( U, Z, T ), midp( skol17( X, Y ), X, Y ) }.
% 10.69/11.13 (54453) {G0,W16,D3,L3,V3,M3} { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z )
% 10.69/11.13 , coll( X, Y, skol18( X, Y ) ) }.
% 10.69/11.13 (54454) {G0,W17,D3,L3,V3,M3} { ! cong( Y, X, Y, Z ), ! perp( X, Y, Y, Z )
% 10.69/11.13 , cong( Y, X, Y, skol18( X, Y ) ) }.
% 10.69/11.13 (54455) {G0,W25,D3,L5,V8,M5} { ! para( U, W, X, Y ), ! coll( Z, U, X ), !
% 10.69/11.13 coll( Z, W, Y ), ! coll( T, U, W ), coll( Z, T, skol19( V0, V1, Z, T ) )
% 10.69/11.13 }.
% 10.69/11.13 (54456) {G0,W25,D3,L5,V6,M5} { ! para( U, W, X, Y ), ! coll( Z, U, X ), !
% 10.69/11.13 coll( Z, W, Y ), ! coll( T, U, W ), coll( skol19( X, Y, Z, T ), X, Y )
% 10.69/11.13 }.
% 10.69/11.13 (54457) {G0,W4,D2,L1,V0,M1} { coll( skol27, skol25, skol26 ) }.
% 10.69/11.13 (54458) {G0,W4,D2,L1,V0,M1} { coll( skol29, skol25, skol28 ) }.
% 10.69/11.13 (54459) {G0,W4,D2,L1,V0,M1} { coll( skol30, skol26, skol29 ) }.
% 10.69/11.13 (54460) {G0,W4,D2,L1,V0,M1} { coll( skol30, skol27, skol28 ) }.
% 10.69/11.13 (54461) {G0,W5,D2,L1,V0,M1} { circle( skol20, skol28, skol29, skol30 ) }.
% 10.69/11.13 (54462) {G0,W5,D2,L1,V0,M1} { circle( skol22, skol25, skol27, skol28 ) }.
% 10.69/11.13 (54463) {G0,W5,D2,L1,V0,M1} { circle( skol23, skol26, skol27, skol30 ) }.
% 10.69/11.13 (54464) {G0,W5,D2,L1,V0,M1} { circle( skol24, skol26, skol25, skol29 ) }.
% 10.69/11.13 (54465) {G0,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol24, skol22, skol20 )
% 10.69/11.13 }.
% 10.69/11.13
% 10.69/11.13
% 10.69/11.13 Total Proof:
% 10.69/11.13
% 10.69/11.13 subsumption: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 10.69/11.13 }.
% 10.69/11.13 parent0: (54340) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( X, Z, Y )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 10.69/11.13 }.
% 10.69/11.13 parent0: (54341) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Y, X, Z )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T,
% 10.69/11.13 Z ), coll( Y, Z, X ) }.
% 10.69/11.13 parent0: (54342) {G0,W12,D2,L3,V4,M3} { ! coll( X, T, Y ), ! coll( X, T, Z
% 10.69/11.13 ), coll( Y, Z, X ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 2 ==> 2
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (6) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( X, Y
% 10.69/11.13 , T, Z ) }.
% 10.69/11.13 parent0: (54346) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( X, Y,
% 10.69/11.13 T, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T
% 10.69/11.13 , X, Y ) }.
% 10.69/11.13 parent0: (54347) {G0,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), perp( Z, T,
% 10.69/11.13 X, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U,
% 10.69/11.13 W, Z, T ), para( X, Y, Z, T ) }.
% 10.69/11.13 parent0: (54348) {G0,W15,D2,L3,V6,M3} { ! perp( X, Y, U, W ), ! perp( U, W
% 10.69/11.13 , Z, T ), para( X, Y, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 U := U
% 10.69/11.13 W := W
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 2 ==> 2
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 10.69/11.13 X, Y, T, Z ) }.
% 10.69/11.13 parent0: (54353) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Y, T, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 10.69/11.13 X, Z, Y, T ) }.
% 10.69/11.13 parent0: (54354) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Z, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic(
% 10.69/11.13 Y, X, Z, T ) }.
% 10.69/11.13 parent0: (54355) {G0,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Y
% 10.69/11.13 , X, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic
% 10.69/11.13 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 10.69/11.13 parent0: (54356) {G0,W15,D2,L3,V5,M3} { ! cyclic( U, X, Y, Z ), ! cyclic(
% 10.69/11.13 U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 U := U
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 2 ==> 2
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (18) {G0,W18,D2,L2,V8,M2} I { ! eqangle( X, Y, Z, T, U, W, V0
% 10.69/11.13 , V1 ), eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 10.69/11.13 parent0: (54358) {G0,W18,D2,L2,V8,M2} { ! eqangle( X, Y, Z, T, U, W, V0,
% 10.69/11.13 V1 ), eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 U := U
% 10.69/11.13 W := W
% 10.69/11.13 V0 := V0
% 10.69/11.13 V1 := V1
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X
% 10.69/11.13 , Y, U, W, Z, T, U, W ) }.
% 10.69/11.13 parent0: (54379) {G0,W14,D2,L2,V6,M2} { ! para( X, Y, Z, T ), eqangle( X,
% 10.69/11.13 Y, U, W, Z, T, U, W ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 U := U
% 10.69/11.13 W := W
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T,
% 10.69/11.13 Y ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 10.69/11.13 parent0: (54382) {G0,W18,D2,L3,V4,M3} { ! eqangle( Z, X, Z, Y, T, X, T, Y
% 10.69/11.13 ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 2 ==> 2
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (53) {G0,W14,D2,L3,V4,M3} I { ! circle( T, X, Y, Z ), ! coll(
% 10.69/11.13 T, X, Z ), perp( X, Y, Y, Z ) }.
% 10.69/11.13 parent0: (54393) {G0,W14,D2,L3,V4,M3} { ! circle( T, X, Y, Z ), ! coll( T
% 10.69/11.13 , X, Z ), perp( X, Y, Y, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 2 ==> 2
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (96) {G0,W14,D2,L3,V4,M3} I { ! perp( X, T, Y, Z ), ! perp( Y
% 10.69/11.13 , T, X, Z ), alpha1( X, Y, Z ) }.
% 10.69/11.13 parent0: (54437) {G0,W14,D2,L3,V4,M3} { ! perp( X, T, Y, Z ), ! perp( Y, T
% 10.69/11.13 , X, Z ), alpha1( X, Y, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 2 ==> 2
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (97) {G0,W11,D3,L2,V4,M2} I { ! alpha1( X, Y, Z ), coll(
% 10.69/11.13 skol11( X, T, Z ), Z, X ) }.
% 10.69/11.13 parent0: (54438) {G0,W11,D3,L2,V4,M2} { ! alpha1( X, Y, Z ), coll( skol11
% 10.69/11.13 ( X, T, Z ), Z, X ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (100) {G0,W12,D3,L2,V4,M2} I { ! circle( Y, X, Z, T ), perp(
% 10.69/11.13 skol12( X, Y ), X, X, Y ) }.
% 10.69/11.13 parent0: (54441) {G0,W12,D3,L2,V4,M2} { ! circle( Y, X, Z, T ), perp(
% 10.69/11.13 skol12( X, Y ), X, X, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (118) {G0,W4,D2,L1,V0,M1} I { coll( skol30, skol26, skol29 )
% 10.69/11.13 }.
% 10.69/11.13 parent0: (54459) {G0,W4,D2,L1,V0,M1} { coll( skol30, skol26, skol29 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (119) {G0,W4,D2,L1,V0,M1} I { coll( skol30, skol27, skol28 )
% 10.69/11.13 }.
% 10.69/11.13 parent0: (54460) {G0,W4,D2,L1,V0,M1} { coll( skol30, skol27, skol28 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (120) {G0,W5,D2,L1,V0,M1} I { circle( skol20, skol28, skol29,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 parent0: (54461) {G0,W5,D2,L1,V0,M1} { circle( skol20, skol28, skol29,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (124) {G0,W5,D2,L1,V0,M1} I { ! cyclic( skol23, skol24, skol22
% 10.69/11.13 , skol20 ) }.
% 10.69/11.13 parent0: (54465) {G0,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol24, skol22,
% 10.69/11.13 skol20 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 factor: (54882) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Z, X )
% 10.69/11.13 }.
% 10.69/11.13 parent0[0, 1]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T
% 10.69/11.13 , Z ), coll( Y, Z, X ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := Z
% 10.69/11.13 T := Y
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (125) {G1,W8,D2,L2,V3,M2} F(2) { ! coll( X, Y, Z ), coll( Z, Z
% 10.69/11.13 , X ) }.
% 10.69/11.13 parent0: (54882) {G0,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Z, X )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54884) {G1,W8,D2,L2,V3,M2} { coll( X, Z, Y ), ! coll( Y, X, Z
% 10.69/11.13 ) }.
% 10.69/11.13 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 10.69/11.13 }.
% 10.69/11.13 parent1[1]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := X
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (171) {G1,W8,D2,L2,V3,M2} R(1,0) { ! coll( X, Y, Z ), coll( Y
% 10.69/11.13 , Z, X ) }.
% 10.69/11.13 parent0: (54884) {G1,W8,D2,L2,V3,M2} { coll( X, Z, Y ), ! coll( Y, X, Z )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := X
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 1
% 10.69/11.13 1 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54888) {G1,W12,D2,L3,V4,M3} { coll( X, Z, Y ), ! coll( Z, T,
% 10.69/11.13 X ), ! coll( Z, T, Y ) }.
% 10.69/11.13 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 10.69/11.13 }.
% 10.69/11.13 parent1[2]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 10.69/11.13 ), coll( Y, Z, X ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := Z
% 10.69/11.13 Y := X
% 10.69/11.13 Z := Y
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (201) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), ! coll
% 10.69/11.13 ( X, Y, T ), coll( Z, X, T ) }.
% 10.69/11.13 parent0: (54888) {G1,W12,D2,L3,V4,M3} { coll( X, Z, Y ), ! coll( Z, T, X )
% 10.69/11.13 , ! coll( Z, T, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := Z
% 10.69/11.13 Y := T
% 10.69/11.13 Z := X
% 10.69/11.13 T := Y
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 2
% 10.69/11.13 1 ==> 0
% 10.69/11.13 2 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 factor: (54890) {G1,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, X, Z )
% 10.69/11.13 }.
% 10.69/11.13 parent0[0, 1]: (201) {G1,W12,D2,L3,V4,M3} R(2,0) { ! coll( X, Y, Z ), !
% 10.69/11.13 coll( X, Y, T ), coll( Z, X, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := Z
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (210) {G2,W8,D2,L2,V3,M2} F(201) { ! coll( X, Y, Z ), coll( Z
% 10.69/11.13 , X, Z ) }.
% 10.69/11.13 parent0: (54890) {G1,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, X, Z )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54891) {G1,W12,D2,L3,V4,M3} { coll( Z, X, Z ), ! coll( Z, T,
% 10.69/11.13 X ), ! coll( Z, T, Y ) }.
% 10.69/11.13 parent0[0]: (210) {G2,W8,D2,L2,V3,M2} F(201) { ! coll( X, Y, Z ), coll( Z,
% 10.69/11.13 X, Z ) }.
% 10.69/11.13 parent1[2]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 10.69/11.13 ), coll( Y, Z, X ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := Z
% 10.69/11.13 Y := X
% 10.69/11.13 Z := Y
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (265) {G3,W12,D2,L3,V4,M3} R(210,2) { coll( X, Y, X ), ! coll
% 10.69/11.13 ( X, Z, Y ), ! coll( X, Z, T ) }.
% 10.69/11.13 parent0: (54891) {G1,W12,D2,L3,V4,M3} { coll( Z, X, Z ), ! coll( Z, T, X )
% 10.69/11.13 , ! coll( Z, T, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := X
% 10.69/11.13 T := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 2 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54893) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol30, skol29 )
% 10.69/11.13 }.
% 10.69/11.13 parent0[0]: (210) {G2,W8,D2,L2,V3,M2} F(201) { ! coll( X, Y, Z ), coll( Z,
% 10.69/11.13 X, Z ) }.
% 10.69/11.13 parent1[0]: (118) {G0,W4,D2,L1,V0,M1} I { coll( skol30, skol26, skol29 )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol30
% 10.69/11.13 Y := skol26
% 10.69/11.13 Z := skol29
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (280) {G3,W4,D2,L1,V0,M1} R(210,118) { coll( skol29, skol30,
% 10.69/11.13 skol29 ) }.
% 10.69/11.13 parent0: (54893) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol30, skol29 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54894) {G1,W4,D2,L1,V0,M1} { coll( skol28, skol30, skol28 )
% 10.69/11.13 }.
% 10.69/11.13 parent0[0]: (210) {G2,W8,D2,L2,V3,M2} F(201) { ! coll( X, Y, Z ), coll( Z,
% 10.69/11.13 X, Z ) }.
% 10.69/11.13 parent1[0]: (119) {G0,W4,D2,L1,V0,M1} I { coll( skol30, skol27, skol28 )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol30
% 10.69/11.13 Y := skol27
% 10.69/11.13 Z := skol28
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (281) {G3,W4,D2,L1,V0,M1} R(210,119) { coll( skol28, skol30,
% 10.69/11.13 skol28 ) }.
% 10.69/11.13 parent0: (54894) {G1,W4,D2,L1,V0,M1} { coll( skol28, skol30, skol28 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 factor: (54895) {G3,W8,D2,L2,V3,M2} { coll( X, Y, X ), ! coll( X, Z, Y )
% 10.69/11.13 }.
% 10.69/11.13 parent0[1, 2]: (265) {G3,W12,D2,L3,V4,M3} R(210,2) { coll( X, Y, X ), !
% 10.69/11.13 coll( X, Z, Y ), ! coll( X, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := Y
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (282) {G4,W8,D2,L2,V3,M2} F(265) { coll( X, Y, X ), ! coll( X
% 10.69/11.13 , Z, Y ) }.
% 10.69/11.13 parent0: (54895) {G3,W8,D2,L2,V3,M2} { coll( X, Y, X ), ! coll( X, Z, Y )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54896) {G1,W15,D2,L3,V6,M3} { ! perp( Z, T, U, W ), para( X,
% 10.69/11.13 Y, U, W ), ! perp( Z, T, X, Y ) }.
% 10.69/11.13 parent0[0]: (8) {G0,W15,D2,L3,V6,M3} I { ! perp( X, Y, U, W ), ! perp( U, W
% 10.69/11.13 , Z, T ), para( X, Y, Z, T ) }.
% 10.69/11.13 parent1[1]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 10.69/11.13 X, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := U
% 10.69/11.13 T := W
% 10.69/11.13 U := Z
% 10.69/11.13 W := T
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := Z
% 10.69/11.13 Y := T
% 10.69/11.13 Z := X
% 10.69/11.13 T := Y
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (297) {G1,W15,D2,L3,V6,M3} R(8,7) { ! perp( X, Y, Z, T ), para
% 10.69/11.13 ( U, W, Z, T ), ! perp( X, Y, U, W ) }.
% 10.69/11.13 parent0: (54896) {G1,W15,D2,L3,V6,M3} { ! perp( Z, T, U, W ), para( X, Y,
% 10.69/11.13 U, W ), ! perp( Z, T, X, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := U
% 10.69/11.13 Y := W
% 10.69/11.13 Z := X
% 10.69/11.13 T := Y
% 10.69/11.13 U := Z
% 10.69/11.13 W := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 2 ==> 2
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 factor: (54900) {G1,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), para( Z, T, Z
% 10.69/11.13 , T ) }.
% 10.69/11.13 parent0[0, 2]: (297) {G1,W15,D2,L3,V6,M3} R(8,7) { ! perp( X, Y, Z, T ),
% 10.69/11.13 para( U, W, Z, T ), ! perp( X, Y, U, W ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 U := Z
% 10.69/11.13 W := T
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (307) {G2,W10,D2,L2,V4,M2} F(297) { ! perp( X, Y, Z, T ), para
% 10.69/11.13 ( Z, T, Z, T ) }.
% 10.69/11.13 parent0: (54900) {G1,W10,D2,L2,V4,M2} { ! perp( X, Y, Z, T ), para( Z, T,
% 10.69/11.13 Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54902) {G1,W10,D2,L2,V4,M2} { cyclic( X, Y, T, Z ), ! cyclic
% 10.69/11.13 ( X, Z, Y, T ) }.
% 10.69/11.13 parent0[0]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Y, T, Z ) }.
% 10.69/11.13 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Z, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := Y
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (364) {G1,W10,D2,L2,V4,M2} R(14,13) { ! cyclic( X, Y, Z, T ),
% 10.69/11.13 cyclic( X, Z, T, Y ) }.
% 10.69/11.13 parent0: (54902) {G1,W10,D2,L2,V4,M2} { cyclic( X, Y, T, Z ), ! cyclic( X
% 10.69/11.13 , Z, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := Y
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 1
% 10.69/11.13 1 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54903) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic
% 10.69/11.13 ( X, Z, Y, T ) }.
% 10.69/11.13 parent0[0]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 10.69/11.13 , X, Z, T ) }.
% 10.69/11.13 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Z, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := Y
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (374) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), !
% 10.69/11.13 cyclic( Y, Z, X, T ) }.
% 10.69/11.13 parent0: (54903) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic( X
% 10.69/11.13 , Z, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := X
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54904) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic
% 10.69/11.13 ( X, Y, T, Z ) }.
% 10.69/11.13 parent0[0]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 10.69/11.13 , X, Z, T ) }.
% 10.69/11.13 parent1[1]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Y, T, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := T
% 10.69/11.13 T := Z
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (376) {G1,W10,D2,L2,V4,M2} R(15,13) { cyclic( X, Y, Z, T ), !
% 10.69/11.13 cyclic( Y, X, T, Z ) }.
% 10.69/11.13 parent0: (54904) {G1,W10,D2,L2,V4,M2} { cyclic( Y, X, Z, T ), ! cyclic( X
% 10.69/11.13 , Y, T, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := X
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54905) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol23, skol22
% 10.69/11.13 , skol20 ) }.
% 10.69/11.13 parent0[0]: (124) {G0,W5,D2,L1,V0,M1} I { ! cyclic( skol23, skol24, skol22
% 10.69/11.13 , skol20 ) }.
% 10.69/11.13 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 10.69/11.13 , X, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol24
% 10.69/11.13 Y := skol23
% 10.69/11.13 Z := skol22
% 10.69/11.13 T := skol20
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (378) {G1,W5,D2,L1,V0,M1} R(15,124) { ! cyclic( skol24, skol23
% 10.69/11.13 , skol22, skol20 ) }.
% 10.69/11.13 parent0: (54905) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol23, skol22,
% 10.69/11.13 skol20 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54909) {G1,W15,D2,L3,V5,M3} { cyclic( Y, X, Z, T ), ! cyclic
% 10.69/11.13 ( U, X, Y, Z ), ! cyclic( U, X, Y, T ) }.
% 10.69/11.13 parent0[0]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 10.69/11.13 , X, Z, T ) }.
% 10.69/11.13 parent1[2]: (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic
% 10.69/11.13 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 U := U
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (394) {G1,W15,D2,L3,V5,M3} R(16,15) { ! cyclic( X, Y, Z, T ),
% 10.69/11.13 ! cyclic( X, Y, Z, U ), cyclic( Z, Y, T, U ) }.
% 10.69/11.13 parent0: (54909) {G1,W15,D2,L3,V5,M3} { cyclic( Y, X, Z, T ), ! cyclic( U
% 10.69/11.13 , X, Y, Z ), ! cyclic( U, X, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := T
% 10.69/11.13 T := U
% 10.69/11.13 U := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 2
% 10.69/11.13 1 ==> 0
% 10.69/11.13 2 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54912) {G1,W15,D2,L3,V5,M3} { ! cyclic( X, Y, Z, T ), cyclic
% 10.69/11.13 ( Y, Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 10.69/11.13 parent0[1]: (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic
% 10.69/11.13 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 10.69/11.13 parent1[1]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Y, T, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := T
% 10.69/11.13 T := U
% 10.69/11.13 U := X
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := U
% 10.69/11.13 T := Z
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (399) {G1,W15,D2,L3,V5,M3} R(16,13) { ! cyclic( X, Y, Z, T ),
% 10.69/11.13 cyclic( Y, Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 10.69/11.13 parent0: (54912) {G1,W15,D2,L3,V5,M3} { ! cyclic( X, Y, Z, T ), cyclic( Y
% 10.69/11.13 , Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 U := U
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 2 ==> 2
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 factor: (54914) {G1,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Z,
% 10.69/11.13 Y, T, T ) }.
% 10.69/11.13 parent0[0, 1]: (394) {G1,W15,D2,L3,V5,M3} R(16,15) { ! cyclic( X, Y, Z, T )
% 10.69/11.13 , ! cyclic( X, Y, Z, U ), cyclic( Z, Y, T, U ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 U := T
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (404) {G2,W10,D2,L2,V4,M2} F(394) { ! cyclic( X, Y, Z, T ),
% 10.69/11.13 cyclic( Z, Y, T, T ) }.
% 10.69/11.13 parent0: (54914) {G1,W10,D2,L2,V4,M2} { ! cyclic( X, Y, Z, T ), cyclic( Z
% 10.69/11.13 , Y, T, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54915) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol29, skol30 )
% 10.69/11.13 }.
% 10.69/11.13 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 10.69/11.13 }.
% 10.69/11.13 parent1[0]: (280) {G3,W4,D2,L1,V0,M1} R(210,118) { coll( skol29, skol30,
% 10.69/11.13 skol29 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol29
% 10.69/11.13 Y := skol30
% 10.69/11.13 Z := skol29
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (528) {G4,W4,D2,L1,V0,M1} R(280,0) { coll( skol29, skol29,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 parent0: (54915) {G1,W4,D2,L1,V0,M1} { coll( skol29, skol29, skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54916) {G1,W4,D2,L1,V0,M1} { coll( skol28, skol28, skol30 )
% 10.69/11.13 }.
% 10.69/11.13 parent0[0]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 10.69/11.13 }.
% 10.69/11.13 parent1[0]: (281) {G3,W4,D2,L1,V0,M1} R(210,119) { coll( skol28, skol30,
% 10.69/11.13 skol28 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol28
% 10.69/11.13 Y := skol30
% 10.69/11.13 Z := skol28
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (534) {G4,W4,D2,L1,V0,M1} R(281,0) { coll( skol28, skol28,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 parent0: (54916) {G1,W4,D2,L1,V0,M1} { coll( skol28, skol28, skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54917) {G1,W8,D2,L2,V1,M2} { ! coll( skol28, skol28, X ),
% 10.69/11.13 coll( skol30, X, skol28 ) }.
% 10.69/11.13 parent0[0]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 10.69/11.13 ), coll( Y, Z, X ) }.
% 10.69/11.13 parent1[0]: (534) {G4,W4,D2,L1,V0,M1} R(281,0) { coll( skol28, skol28,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol28
% 10.69/11.13 Y := skol30
% 10.69/11.13 Z := X
% 10.69/11.13 T := skol28
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (536) {G5,W8,D2,L2,V1,M2} R(534,2) { ! coll( skol28, skol28, X
% 10.69/11.13 ), coll( skol30, X, skol28 ) }.
% 10.69/11.13 parent0: (54917) {G1,W8,D2,L2,V1,M2} { ! coll( skol28, skol28, X ), coll(
% 10.69/11.13 skol30, X, skol28 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54919) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol22, skol23
% 10.69/11.13 , skol20 ) }.
% 10.69/11.13 parent0[0]: (378) {G1,W5,D2,L1,V0,M1} R(15,124) { ! cyclic( skol24, skol23
% 10.69/11.13 , skol22, skol20 ) }.
% 10.69/11.13 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Z, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol24
% 10.69/11.13 Y := skol22
% 10.69/11.13 Z := skol23
% 10.69/11.13 T := skol20
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (539) {G2,W5,D2,L1,V0,M1} R(378,14) { ! cyclic( skol24, skol22
% 10.69/11.13 , skol23, skol20 ) }.
% 10.69/11.13 parent0: (54919) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol22, skol23,
% 10.69/11.13 skol20 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54920) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol24, skol23
% 10.69/11.13 , skol20 ) }.
% 10.69/11.13 parent0[0]: (539) {G2,W5,D2,L1,V0,M1} R(378,14) { ! cyclic( skol24, skol22
% 10.69/11.13 , skol23, skol20 ) }.
% 10.69/11.13 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 10.69/11.13 , X, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol22
% 10.69/11.13 Y := skol24
% 10.69/11.13 Z := skol23
% 10.69/11.13 T := skol20
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (545) {G3,W5,D2,L1,V0,M1} R(539,15) { ! cyclic( skol22, skol24
% 10.69/11.13 , skol23, skol20 ) }.
% 10.69/11.13 parent0: (54920) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol24, skol23,
% 10.69/11.13 skol20 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54921) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol23, skol24
% 10.69/11.13 , skol20 ) }.
% 10.69/11.13 parent0[0]: (545) {G3,W5,D2,L1,V0,M1} R(539,15) { ! cyclic( skol22, skol24
% 10.69/11.13 , skol23, skol20 ) }.
% 10.69/11.13 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Z, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol22
% 10.69/11.13 Y := skol23
% 10.69/11.13 Z := skol24
% 10.69/11.13 T := skol20
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (548) {G4,W5,D2,L1,V0,M1} R(545,14) { ! cyclic( skol22, skol23
% 10.69/11.13 , skol24, skol20 ) }.
% 10.69/11.13 parent0: (54921) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol23, skol24,
% 10.69/11.13 skol20 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54922) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol23, skol20
% 10.69/11.13 , skol24 ) }.
% 10.69/11.13 parent0[0]: (548) {G4,W5,D2,L1,V0,M1} R(545,14) { ! cyclic( skol22, skol23
% 10.69/11.13 , skol24, skol20 ) }.
% 10.69/11.13 parent1[1]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Y, T, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol22
% 10.69/11.13 Y := skol23
% 10.69/11.13 Z := skol20
% 10.69/11.13 T := skol24
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (552) {G5,W5,D2,L1,V0,M1} R(548,13) { ! cyclic( skol22, skol23
% 10.69/11.13 , skol20, skol24 ) }.
% 10.69/11.13 parent0: (54922) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol22, skol23, skol20,
% 10.69/11.13 skol24 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54923) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol22, skol20
% 10.69/11.13 , skol24 ) }.
% 10.69/11.13 parent0[0]: (552) {G5,W5,D2,L1,V0,M1} R(548,13) { ! cyclic( skol22, skol23
% 10.69/11.13 , skol20, skol24 ) }.
% 10.69/11.13 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 10.69/11.13 , X, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol23
% 10.69/11.13 Y := skol22
% 10.69/11.13 Z := skol20
% 10.69/11.13 T := skol24
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (553) {G6,W5,D2,L1,V0,M1} R(552,15) { ! cyclic( skol23, skol22
% 10.69/11.13 , skol20, skol24 ) }.
% 10.69/11.13 parent0: (54923) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol22, skol20,
% 10.69/11.13 skol24 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54924) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol20, skol22
% 10.69/11.13 , skol24 ) }.
% 10.69/11.13 parent0[0]: (553) {G6,W5,D2,L1,V0,M1} R(552,15) { ! cyclic( skol23, skol22
% 10.69/11.13 , skol20, skol24 ) }.
% 10.69/11.13 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Z, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol23
% 10.69/11.13 Y := skol20
% 10.69/11.13 Z := skol22
% 10.69/11.13 T := skol24
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (559) {G7,W5,D2,L1,V0,M1} R(553,14) { ! cyclic( skol23, skol20
% 10.69/11.13 , skol22, skol24 ) }.
% 10.69/11.13 parent0: (54924) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol23, skol20, skol22,
% 10.69/11.13 skol24 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54925) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol23, skol22
% 10.69/11.13 , skol24 ) }.
% 10.69/11.13 parent0[0]: (559) {G7,W5,D2,L1,V0,M1} R(553,14) { ! cyclic( skol23, skol20
% 10.69/11.13 , skol22, skol24 ) }.
% 10.69/11.13 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 10.69/11.13 , X, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol20
% 10.69/11.13 Y := skol23
% 10.69/11.13 Z := skol22
% 10.69/11.13 T := skol24
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (561) {G8,W5,D2,L1,V0,M1} R(559,15) { ! cyclic( skol20, skol23
% 10.69/11.13 , skol22, skol24 ) }.
% 10.69/11.13 parent0: (54925) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol23, skol22,
% 10.69/11.13 skol24 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54926) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol22, skol23
% 10.69/11.13 , skol24 ) }.
% 10.69/11.13 parent0[0]: (561) {G8,W5,D2,L1,V0,M1} R(559,15) { ! cyclic( skol20, skol23
% 10.69/11.13 , skol22, skol24 ) }.
% 10.69/11.13 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Z, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol20
% 10.69/11.13 Y := skol22
% 10.69/11.13 Z := skol23
% 10.69/11.13 T := skol24
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (564) {G9,W5,D2,L1,V0,M1} R(561,14) { ! cyclic( skol20, skol22
% 10.69/11.13 , skol23, skol24 ) }.
% 10.69/11.13 parent0: (54926) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol22, skol23,
% 10.69/11.13 skol24 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54927) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol22, skol24
% 10.69/11.13 , skol23 ) }.
% 10.69/11.13 parent0[0]: (564) {G9,W5,D2,L1,V0,M1} R(561,14) { ! cyclic( skol20, skol22
% 10.69/11.13 , skol23, skol24 ) }.
% 10.69/11.13 parent1[1]: (13) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Y, T, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol20
% 10.69/11.13 Y := skol22
% 10.69/11.13 Z := skol24
% 10.69/11.13 T := skol23
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (568) {G10,W5,D2,L1,V0,M1} R(564,13) { ! cyclic( skol20,
% 10.69/11.13 skol22, skol24, skol23 ) }.
% 10.69/11.13 parent0: (54927) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol22, skol24,
% 10.69/11.13 skol23 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54928) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol24, skol22
% 10.69/11.13 , skol23 ) }.
% 10.69/11.13 parent0[0]: (568) {G10,W5,D2,L1,V0,M1} R(564,13) { ! cyclic( skol20, skol22
% 10.69/11.13 , skol24, skol23 ) }.
% 10.69/11.13 parent1[1]: (14) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( X
% 10.69/11.13 , Z, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol20
% 10.69/11.13 Y := skol24
% 10.69/11.13 Z := skol22
% 10.69/11.13 T := skol23
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (573) {G11,W5,D2,L1,V0,M1} R(568,14) { ! cyclic( skol20,
% 10.69/11.13 skol24, skol22, skol23 ) }.
% 10.69/11.13 parent0: (54928) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol20, skol24, skol22,
% 10.69/11.13 skol23 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54929) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol20, skol22
% 10.69/11.13 , skol23 ) }.
% 10.69/11.13 parent0[0]: (573) {G11,W5,D2,L1,V0,M1} R(568,14) { ! cyclic( skol20, skol24
% 10.69/11.13 , skol22, skol23 ) }.
% 10.69/11.13 parent1[1]: (15) {G0,W10,D2,L2,V4,M2} I { ! cyclic( X, Y, Z, T ), cyclic( Y
% 10.69/11.13 , X, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol24
% 10.69/11.13 Y := skol20
% 10.69/11.13 Z := skol22
% 10.69/11.13 T := skol23
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (576) {G12,W5,D2,L1,V0,M1} R(573,15) { ! cyclic( skol24,
% 10.69/11.13 skol20, skol22, skol23 ) }.
% 10.69/11.13 parent0: (54929) {G1,W5,D2,L1,V0,M1} { ! cyclic( skol24, skol20, skol22,
% 10.69/11.13 skol23 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54930) {G1,W10,D2,L2,V1,M2} { ! cyclic( X, skol24, skol20,
% 10.69/11.13 skol22 ), ! cyclic( X, skol24, skol20, skol23 ) }.
% 10.69/11.13 parent0[0]: (576) {G12,W5,D2,L1,V0,M1} R(573,15) { ! cyclic( skol24, skol20
% 10.69/11.13 , skol22, skol23 ) }.
% 10.69/11.13 parent1[2]: (16) {G0,W15,D2,L3,V5,M3} I { ! cyclic( U, X, Y, Z ), ! cyclic
% 10.69/11.13 ( U, X, Y, T ), cyclic( X, Y, Z, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol24
% 10.69/11.13 Y := skol20
% 10.69/11.13 Z := skol22
% 10.69/11.13 T := skol23
% 10.69/11.13 U := X
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (578) {G13,W10,D2,L2,V1,M2} R(576,16) { ! cyclic( X, skol24,
% 10.69/11.13 skol20, skol22 ), ! cyclic( X, skol24, skol20, skol23 ) }.
% 10.69/11.13 parent0: (54930) {G1,W10,D2,L2,V1,M2} { ! cyclic( X, skol24, skol20,
% 10.69/11.13 skol22 ), ! cyclic( X, skol24, skol20, skol23 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54932) {G1,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( X, Z, Y
% 10.69/11.13 ) }.
% 10.69/11.13 parent0[0]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 10.69/11.13 }.
% 10.69/11.13 parent1[0]: (282) {G4,W8,D2,L2,V3,M2} F(265) { coll( X, Y, X ), ! coll( X,
% 10.69/11.13 Z, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := X
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (600) {G5,W8,D2,L2,V3,M2} R(282,1) { ! coll( X, Y, Z ), coll(
% 10.69/11.13 Z, X, X ) }.
% 10.69/11.13 parent0: (54932) {G1,W8,D2,L2,V3,M2} { coll( Y, X, X ), ! coll( X, Z, Y )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := Y
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 1
% 10.69/11.13 1 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54933) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( Y, X, Z
% 10.69/11.13 ) }.
% 10.69/11.13 parent0[0]: (600) {G5,W8,D2,L2,V3,M2} R(282,1) { ! coll( X, Y, Z ), coll( Z
% 10.69/11.13 , X, X ) }.
% 10.69/11.13 parent1[1]: (1) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( Y, X, Z )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := X
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (605) {G6,W8,D2,L2,V3,M2} R(600,1) { coll( X, Y, Y ), ! coll(
% 10.69/11.13 Z, Y, X ) }.
% 10.69/11.13 parent0: (54933) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( Y, X, Z )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54934) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( X, Z, Y
% 10.69/11.13 ) }.
% 10.69/11.13 parent0[0]: (600) {G5,W8,D2,L2,V3,M2} R(282,1) { ! coll( X, Y, Z ), coll( Z
% 10.69/11.13 , X, X ) }.
% 10.69/11.13 parent1[1]: (0) {G0,W8,D2,L2,V3,M2} I { ! coll( X, Y, Z ), coll( X, Z, Y )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := Y
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (606) {G6,W8,D2,L2,V3,M2} R(600,0) { coll( X, Y, Y ), ! coll(
% 10.69/11.13 Y, X, Z ) }.
% 10.69/11.13 parent0: (54934) {G1,W8,D2,L2,V3,M2} { coll( Z, X, X ), ! coll( X, Z, Y )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54935) {G7,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! coll( X, Y, Z
% 10.69/11.13 ) }.
% 10.69/11.13 parent0[1]: (606) {G6,W8,D2,L2,V3,M2} R(600,0) { coll( X, Y, Y ), ! coll( Y
% 10.69/11.13 , X, Z ) }.
% 10.69/11.13 parent1[0]: (606) {G6,W8,D2,L2,V3,M2} R(600,0) { coll( X, Y, Y ), ! coll( Y
% 10.69/11.13 , X, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := X
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := X
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (626) {G7,W8,D2,L2,V3,M2} R(606,606) { ! coll( X, Y, Z ), coll
% 10.69/11.13 ( X, Y, Y ) }.
% 10.69/11.13 parent0: (54935) {G7,W8,D2,L2,V3,M2} { coll( X, Y, Y ), ! coll( X, Y, Z )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 1
% 10.69/11.13 1 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54939) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, Y,
% 10.69/11.13 X ), ! coll( X, Y, T ) }.
% 10.69/11.13 parent0[1]: (2) {G0,W12,D2,L3,V4,M3} I { ! coll( X, T, Y ), ! coll( X, T, Z
% 10.69/11.13 ), coll( Y, Z, X ) }.
% 10.69/11.13 parent1[1]: (626) {G7,W8,D2,L2,V3,M2} R(606,606) { ! coll( X, Y, Z ), coll
% 10.69/11.13 ( X, Y, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := Y
% 10.69/11.13 T := Y
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := T
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (629) {G8,W12,D2,L3,V4,M3} R(626,2) { ! coll( X, Y, Z ), !
% 10.69/11.13 coll( X, Y, T ), coll( T, Y, X ) }.
% 10.69/11.13 parent0: (54939) {G1,W12,D2,L3,V4,M3} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 10.69/11.13 , ! coll( X, Y, T ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := T
% 10.69/11.13 T := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 1
% 10.69/11.13 1 ==> 2
% 10.69/11.13 2 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 factor: (54942) {G8,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 10.69/11.13 }.
% 10.69/11.13 parent0[0, 1]: (629) {G8,W12,D2,L3,V4,M3} R(626,2) { ! coll( X, Y, Z ), !
% 10.69/11.13 coll( X, Y, T ), coll( T, Y, X ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := Z
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (630) {G9,W8,D2,L2,V3,M2} F(629) { ! coll( X, Y, Z ), coll( Z
% 10.69/11.13 , Y, X ) }.
% 10.69/11.13 parent0: (54942) {G8,W8,D2,L2,V3,M2} { ! coll( X, Y, Z ), coll( Z, Y, X )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54943) {G7,W8,D2,L2,V3,M2} { coll( Y, Y, X ), ! coll( Z, Y, X
% 10.69/11.13 ) }.
% 10.69/11.13 parent0[0]: (630) {G9,W8,D2,L2,V3,M2} F(629) { ! coll( X, Y, Z ), coll( Z,
% 10.69/11.13 Y, X ) }.
% 10.69/11.13 parent1[0]: (605) {G6,W8,D2,L2,V3,M2} R(600,1) { coll( X, Y, Y ), ! coll( Z
% 10.69/11.13 , Y, X ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Y
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (634) {G10,W8,D2,L2,V3,M2} R(630,605) { coll( X, X, Y ), !
% 10.69/11.13 coll( Z, X, Y ) }.
% 10.69/11.13 parent0: (54943) {G7,W8,D2,L2,V3,M2} { coll( Y, Y, X ), ! coll( Z, Y, X )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := X
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54944) {G1,W14,D2,L2,V6,M2} { eqangle( Z, T, X, Y, Z, T, U, W
% 10.69/11.13 ), ! para( X, Y, U, W ) }.
% 10.69/11.13 parent0[0]: (18) {G0,W18,D2,L2,V8,M2} I { ! eqangle( X, Y, Z, T, U, W, V0,
% 10.69/11.13 V1 ), eqangle( Z, T, X, Y, V0, V1, U, W ) }.
% 10.69/11.13 parent1[1]: (39) {G0,W14,D2,L2,V6,M2} I { ! para( X, Y, Z, T ), eqangle( X
% 10.69/11.13 , Y, U, W, Z, T, U, W ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 T := T
% 10.69/11.13 U := U
% 10.69/11.13 W := W
% 10.69/11.13 V0 := Z
% 10.69/11.13 V1 := T
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := U
% 10.69/11.13 T := W
% 10.69/11.13 U := Z
% 10.69/11.13 W := T
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (722) {G1,W14,D2,L2,V6,M2} R(39,18) { ! para( X, Y, Z, T ),
% 10.69/11.13 eqangle( U, W, X, Y, U, W, Z, T ) }.
% 10.69/11.13 parent0: (54944) {G1,W14,D2,L2,V6,M2} { eqangle( Z, T, X, Y, Z, T, U, W )
% 10.69/11.13 , ! para( X, Y, U, W ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := U
% 10.69/11.13 T := W
% 10.69/11.13 U := Z
% 10.69/11.13 W := T
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 1
% 10.69/11.13 1 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54945) {G1,W14,D2,L2,V1,M2} { ! eqangle( skol29, X, skol29,
% 10.69/11.13 skol30, skol29, X, skol29, skol30 ), cyclic( X, skol30, skol29, skol29 )
% 10.69/11.13 }.
% 10.69/11.13 parent0[1]: (42) {G0,W18,D2,L3,V4,M3} I { ! eqangle( Z, X, Z, Y, T, X, T, Y
% 10.69/11.13 ), ! coll( Z, T, Y ), cyclic( X, Y, Z, T ) }.
% 10.69/11.13 parent1[0]: (528) {G4,W4,D2,L1,V0,M1} R(280,0) { coll( skol29, skol29,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := skol30
% 10.69/11.13 Z := skol29
% 10.69/11.13 T := skol29
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (819) {G5,W14,D2,L2,V1,M2} R(42,528) { ! eqangle( skol29, X,
% 10.69/11.13 skol29, skol30, skol29, X, skol29, skol30 ), cyclic( X, skol30, skol29,
% 10.69/11.13 skol29 ) }.
% 10.69/11.13 parent0: (54945) {G1,W14,D2,L2,V1,M2} { ! eqangle( skol29, X, skol29,
% 10.69/11.13 skol30, skol29, X, skol29, skol30 ), cyclic( X, skol30, skol29, skol29 )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54946) {G2,W8,D2,L2,V2,M2} { coll( skol30, X, skol28 ), !
% 10.69/11.13 coll( X, Y, skol28 ) }.
% 10.69/11.13 parent0[0]: (536) {G5,W8,D2,L2,V1,M2} R(534,2) { ! coll( skol28, skol28, X
% 10.69/11.13 ), coll( skol30, X, skol28 ) }.
% 10.69/11.13 parent1[1]: (125) {G1,W8,D2,L2,V3,M2} F(2) { ! coll( X, Y, Z ), coll( Z, Z
% 10.69/11.13 , X ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := skol28
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (990) {G6,W8,D2,L2,V2,M2} R(536,125) { coll( skol30, X, skol28
% 10.69/11.13 ), ! coll( X, Y, skol28 ) }.
% 10.69/11.13 parent0: (54946) {G2,W8,D2,L2,V2,M2} { coll( skol30, X, skol28 ), ! coll(
% 10.69/11.13 X, Y, skol28 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54948) {G2,W8,D2,L2,V2,M2} { coll( X, skol28, skol30 ), !
% 10.69/11.13 coll( X, Y, skol28 ) }.
% 10.69/11.13 parent0[0]: (171) {G1,W8,D2,L2,V3,M2} R(1,0) { ! coll( X, Y, Z ), coll( Y,
% 10.69/11.13 Z, X ) }.
% 10.69/11.13 parent1[0]: (990) {G6,W8,D2,L2,V2,M2} R(536,125) { coll( skol30, X, skol28
% 10.69/11.13 ), ! coll( X, Y, skol28 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol30
% 10.69/11.13 Y := X
% 10.69/11.13 Z := skol28
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (1264) {G7,W8,D2,L2,V2,M2} R(990,171) { ! coll( X, Y, skol28 )
% 10.69/11.13 , coll( X, skol28, skol30 ) }.
% 10.69/11.13 parent0: (54948) {G2,W8,D2,L2,V2,M2} { coll( X, skol28, skol30 ), ! coll(
% 10.69/11.13 X, Y, skol28 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 1
% 10.69/11.13 1 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54949) {G8,W8,D2,L2,V2,M2} { coll( X, skol28, skol30 ), !
% 10.69/11.13 coll( Y, X, skol28 ) }.
% 10.69/11.13 parent0[0]: (1264) {G7,W8,D2,L2,V2,M2} R(990,171) { ! coll( X, Y, skol28 )
% 10.69/11.13 , coll( X, skol28, skol30 ) }.
% 10.69/11.13 parent1[0]: (634) {G10,W8,D2,L2,V3,M2} R(630,605) { coll( X, X, Y ), ! coll
% 10.69/11.13 ( Z, X, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := X
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := skol28
% 10.69/11.13 Z := Y
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (1306) {G11,W8,D2,L2,V2,M2} R(1264,634) { coll( X, skol28,
% 10.69/11.13 skol30 ), ! coll( Y, X, skol28 ) }.
% 10.69/11.13 parent0: (54949) {G8,W8,D2,L2,V2,M2} { coll( X, skol28, skol30 ), ! coll(
% 10.69/11.13 Y, X, skol28 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54950) {G1,W9,D2,L2,V0,M2} { ! coll( skol20, skol28, skol30 )
% 10.69/11.13 , perp( skol28, skol29, skol29, skol30 ) }.
% 10.69/11.13 parent0[0]: (53) {G0,W14,D2,L3,V4,M3} I { ! circle( T, X, Y, Z ), ! coll( T
% 10.69/11.13 , X, Z ), perp( X, Y, Y, Z ) }.
% 10.69/11.13 parent1[0]: (120) {G0,W5,D2,L1,V0,M1} I { circle( skol20, skol28, skol29,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol28
% 10.69/11.13 Y := skol29
% 10.69/11.13 Z := skol30
% 10.69/11.13 T := skol20
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (1597) {G1,W9,D2,L2,V0,M2} R(53,120) { ! coll( skol20, skol28
% 10.69/11.13 , skol30 ), perp( skol28, skol29, skol29, skol30 ) }.
% 10.69/11.13 parent0: (54950) {G1,W9,D2,L2,V0,M2} { ! coll( skol20, skol28, skol30 ),
% 10.69/11.13 perp( skol28, skol29, skol29, skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 1 ==> 1
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54951) {G1,W8,D2,L2,V2,M2} { coll( X, skol28, skol30 ), !
% 10.69/11.13 alpha1( skol28, Z, X ) }.
% 10.69/11.13 parent0[1]: (1306) {G11,W8,D2,L2,V2,M2} R(1264,634) { coll( X, skol28,
% 10.69/11.13 skol30 ), ! coll( Y, X, skol28 ) }.
% 10.69/11.13 parent1[1]: (97) {G0,W11,D3,L2,V4,M2} I { ! alpha1( X, Y, Z ), coll( skol11
% 10.69/11.13 ( X, T, Z ), Z, X ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := skol11( skol28, Y, X )
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol28
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := X
% 10.69/11.13 T := Y
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (4229) {G12,W8,D2,L2,V2,M2} R(97,1306) { ! alpha1( skol28, X,
% 10.69/11.13 Y ), coll( Y, skol28, skol30 ) }.
% 10.69/11.13 parent0: (54951) {G1,W8,D2,L2,V2,M2} { coll( X, skol28, skol30 ), ! alpha1
% 10.69/11.13 ( skol28, Z, X ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := Y
% 10.69/11.13 Y := Z
% 10.69/11.13 Z := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 1
% 10.69/11.13 1 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54952) {G1,W7,D3,L1,V0,M1} { perp( skol12( skol28, skol20 ),
% 10.69/11.13 skol28, skol28, skol20 ) }.
% 10.69/11.13 parent0[0]: (100) {G0,W12,D3,L2,V4,M2} I { ! circle( Y, X, Z, T ), perp(
% 10.69/11.13 skol12( X, Y ), X, X, Y ) }.
% 10.69/11.13 parent1[0]: (120) {G0,W5,D2,L1,V0,M1} I { circle( skol20, skol28, skol29,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol28
% 10.69/11.13 Y := skol20
% 10.69/11.13 Z := skol29
% 10.69/11.13 T := skol30
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (4767) {G1,W7,D3,L1,V0,M1} R(100,120) { perp( skol12( skol28,
% 10.69/11.13 skol20 ), skol28, skol28, skol20 ) }.
% 10.69/11.13 parent0: (54952) {G1,W7,D3,L1,V0,M1} { perp( skol12( skol28, skol20 ),
% 10.69/11.13 skol28, skol28, skol20 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54953) {G1,W7,D3,L1,V0,M1} { perp( skol28, skol20, skol12(
% 10.69/11.13 skol28, skol20 ), skol28 ) }.
% 10.69/11.13 parent0[0]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 10.69/11.13 X, Y ) }.
% 10.69/11.13 parent1[0]: (4767) {G1,W7,D3,L1,V0,M1} R(100,120) { perp( skol12( skol28,
% 10.69/11.13 skol20 ), skol28, skol28, skol20 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol12( skol28, skol20 )
% 10.69/11.13 Y := skol28
% 10.69/11.13 Z := skol28
% 10.69/11.13 T := skol20
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (4783) {G2,W7,D3,L1,V0,M1} R(4767,7) { perp( skol28, skol20,
% 10.69/11.13 skol12( skol28, skol20 ), skol28 ) }.
% 10.69/11.13 parent0: (54953) {G1,W7,D3,L1,V0,M1} { perp( skol28, skol20, skol12(
% 10.69/11.13 skol28, skol20 ), skol28 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54954) {G1,W7,D3,L1,V0,M1} { perp( skol28, skol20, skol28,
% 10.69/11.13 skol12( skol28, skol20 ) ) }.
% 10.69/11.13 parent0[0]: (6) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( X, Y,
% 10.69/11.13 T, Z ) }.
% 10.69/11.13 parent1[0]: (4783) {G2,W7,D3,L1,V0,M1} R(4767,7) { perp( skol28, skol20,
% 10.69/11.13 skol12( skol28, skol20 ), skol28 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol28
% 10.69/11.13 Y := skol20
% 10.69/11.13 Z := skol12( skol28, skol20 )
% 10.69/11.13 T := skol28
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (4794) {G3,W7,D3,L1,V0,M1} R(4783,6) { perp( skol28, skol20,
% 10.69/11.13 skol28, skol12( skol28, skol20 ) ) }.
% 10.69/11.13 parent0: (54954) {G1,W7,D3,L1,V0,M1} { perp( skol28, skol20, skol28,
% 10.69/11.13 skol12( skol28, skol20 ) ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54955) {G1,W7,D3,L1,V0,M1} { perp( skol28, skol12( skol28,
% 10.69/11.13 skol20 ), skol28, skol20 ) }.
% 10.69/11.13 parent0[0]: (7) {G0,W10,D2,L2,V4,M2} I { ! perp( X, Y, Z, T ), perp( Z, T,
% 10.69/11.13 X, Y ) }.
% 10.69/11.13 parent1[0]: (4794) {G3,W7,D3,L1,V0,M1} R(4783,6) { perp( skol28, skol20,
% 10.69/11.13 skol28, skol12( skol28, skol20 ) ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol28
% 10.69/11.13 Y := skol20
% 10.69/11.13 Z := skol28
% 10.69/11.13 T := skol12( skol28, skol20 )
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (4804) {G4,W7,D3,L1,V0,M1} R(4794,7) { perp( skol28, skol12(
% 10.69/11.13 skol28, skol20 ), skol28, skol20 ) }.
% 10.69/11.13 parent0: (54955) {G1,W7,D3,L1,V0,M1} { perp( skol28, skol12( skol28,
% 10.69/11.13 skol20 ), skol28, skol20 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54956) {G1,W11,D3,L2,V0,M2} { ! perp( skol28, skol12( skol28
% 10.69/11.13 , skol20 ), skol28, skol20 ), alpha1( skol28, skol28, skol20 ) }.
% 10.69/11.13 parent0[0]: (96) {G0,W14,D2,L3,V4,M3} I { ! perp( X, T, Y, Z ), ! perp( Y,
% 10.69/11.13 T, X, Z ), alpha1( X, Y, Z ) }.
% 10.69/11.13 parent1[0]: (4804) {G4,W7,D3,L1,V0,M1} R(4794,7) { perp( skol28, skol12(
% 10.69/11.13 skol28, skol20 ), skol28, skol20 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol28
% 10.69/11.13 Y := skol28
% 10.69/11.13 Z := skol20
% 10.69/11.13 T := skol12( skol28, skol20 )
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54957) {G2,W4,D2,L1,V0,M1} { alpha1( skol28, skol28, skol20 )
% 10.69/11.13 }.
% 10.69/11.13 parent0[0]: (54956) {G1,W11,D3,L2,V0,M2} { ! perp( skol28, skol12( skol28
% 10.69/11.13 , skol20 ), skol28, skol20 ), alpha1( skol28, skol28, skol20 ) }.
% 10.69/11.13 parent1[0]: (4804) {G4,W7,D3,L1,V0,M1} R(4794,7) { perp( skol28, skol12(
% 10.69/11.13 skol28, skol20 ), skol28, skol20 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (5469) {G5,W4,D2,L1,V0,M1} R(4804,96);r(4804) { alpha1( skol28
% 10.69/11.13 , skol28, skol20 ) }.
% 10.69/11.13 parent0: (54957) {G2,W4,D2,L1,V0,M1} { alpha1( skol28, skol28, skol20 )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54958) {G6,W4,D2,L1,V0,M1} { coll( skol20, skol28, skol30 )
% 10.69/11.13 }.
% 10.69/11.13 parent0[0]: (4229) {G12,W8,D2,L2,V2,M2} R(97,1306) { ! alpha1( skol28, X, Y
% 10.69/11.13 ), coll( Y, skol28, skol30 ) }.
% 10.69/11.13 parent1[0]: (5469) {G5,W4,D2,L1,V0,M1} R(4804,96);r(4804) { alpha1( skol28
% 10.69/11.13 , skol28, skol20 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol28
% 10.69/11.13 Y := skol20
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (5478) {G13,W4,D2,L1,V0,M1} R(5469,4229) { coll( skol20,
% 10.69/11.13 skol28, skol30 ) }.
% 10.69/11.13 parent0: (54958) {G6,W4,D2,L1,V0,M1} { coll( skol20, skol28, skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54959) {G2,W5,D2,L1,V0,M1} { perp( skol28, skol29, skol29,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 parent0[0]: (1597) {G1,W9,D2,L2,V0,M2} R(53,120) { ! coll( skol20, skol28,
% 10.69/11.13 skol30 ), perp( skol28, skol29, skol29, skol30 ) }.
% 10.69/11.13 parent1[0]: (5478) {G13,W4,D2,L1,V0,M1} R(5469,4229) { coll( skol20, skol28
% 10.69/11.13 , skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (20004) {G14,W5,D2,L1,V0,M1} S(1597);r(5478) { perp( skol28,
% 10.69/11.13 skol29, skol29, skol30 ) }.
% 10.69/11.13 parent0: (54959) {G2,W5,D2,L1,V0,M1} { perp( skol28, skol29, skol29,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54960) {G3,W5,D2,L1,V0,M1} { para( skol29, skol30, skol29,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 parent0[0]: (307) {G2,W10,D2,L2,V4,M2} F(297) { ! perp( X, Y, Z, T ), para
% 10.69/11.13 ( Z, T, Z, T ) }.
% 10.69/11.13 parent1[0]: (20004) {G14,W5,D2,L1,V0,M1} S(1597);r(5478) { perp( skol28,
% 10.69/11.13 skol29, skol29, skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol28
% 10.69/11.13 Y := skol29
% 10.69/11.13 Z := skol29
% 10.69/11.13 T := skol30
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (26759) {G15,W5,D2,L1,V0,M1} R(20004,307) { para( skol29,
% 10.69/11.13 skol30, skol29, skol30 ) }.
% 10.69/11.13 parent0: (54960) {G3,W5,D2,L1,V0,M1} { para( skol29, skol30, skol29,
% 10.69/11.13 skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54961) {G2,W9,D2,L1,V2,M1} { eqangle( X, Y, skol29, skol30, X
% 10.69/11.13 , Y, skol29, skol30 ) }.
% 10.69/11.13 parent0[0]: (722) {G1,W14,D2,L2,V6,M2} R(39,18) { ! para( X, Y, Z, T ),
% 10.69/11.13 eqangle( U, W, X, Y, U, W, Z, T ) }.
% 10.69/11.13 parent1[0]: (26759) {G15,W5,D2,L1,V0,M1} R(20004,307) { para( skol29,
% 10.69/11.13 skol30, skol29, skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol29
% 10.69/11.13 Y := skol30
% 10.69/11.13 Z := skol29
% 10.69/11.13 T := skol30
% 10.69/11.13 U := X
% 10.69/11.13 W := Y
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (47969) {G16,W9,D2,L1,V2,M1} R(722,26759) { eqangle( X, Y,
% 10.69/11.13 skol29, skol30, X, Y, skol29, skol30 ) }.
% 10.69/11.13 parent0: (54961) {G2,W9,D2,L1,V2,M1} { eqangle( X, Y, skol29, skol30, X, Y
% 10.69/11.13 , skol29, skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54962) {G6,W5,D2,L1,V1,M1} { cyclic( X, skol30, skol29,
% 10.69/11.13 skol29 ) }.
% 10.69/11.13 parent0[0]: (819) {G5,W14,D2,L2,V1,M2} R(42,528) { ! eqangle( skol29, X,
% 10.69/11.13 skol29, skol30, skol29, X, skol29, skol30 ), cyclic( X, skol30, skol29,
% 10.69/11.13 skol29 ) }.
% 10.69/11.13 parent1[0]: (47969) {G16,W9,D2,L1,V2,M1} R(722,26759) { eqangle( X, Y,
% 10.69/11.13 skol29, skol30, X, Y, skol29, skol30 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol29
% 10.69/11.13 Y := X
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (54239) {G17,W5,D2,L1,V1,M1} S(819);r(47969) { cyclic( X,
% 10.69/11.13 skol30, skol29, skol29 ) }.
% 10.69/11.13 parent0: (54962) {G6,W5,D2,L1,V1,M1} { cyclic( X, skol30, skol29, skol29 )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54963) {G2,W5,D2,L1,V1,M1} { cyclic( skol30, X, skol29,
% 10.69/11.13 skol29 ) }.
% 10.69/11.13 parent0[1]: (376) {G1,W10,D2,L2,V4,M2} R(15,13) { cyclic( X, Y, Z, T ), !
% 10.69/11.13 cyclic( Y, X, T, Z ) }.
% 10.69/11.13 parent1[0]: (54239) {G17,W5,D2,L1,V1,M1} S(819);r(47969) { cyclic( X,
% 10.69/11.13 skol30, skol29, skol29 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol30
% 10.69/11.13 Y := X
% 10.69/11.13 Z := skol29
% 10.69/11.13 T := skol29
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (54260) {G18,W5,D2,L1,V1,M1} R(54239,376) { cyclic( skol30, X
% 10.69/11.13 , skol29, skol29 ) }.
% 10.69/11.13 parent0: (54963) {G2,W5,D2,L1,V1,M1} { cyclic( skol30, X, skol29, skol29 )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54964) {G3,W5,D2,L1,V1,M1} { cyclic( skol29, X, skol29,
% 10.69/11.13 skol29 ) }.
% 10.69/11.13 parent0[0]: (404) {G2,W10,D2,L2,V4,M2} F(394) { ! cyclic( X, Y, Z, T ),
% 10.69/11.13 cyclic( Z, Y, T, T ) }.
% 10.69/11.13 parent1[0]: (54260) {G18,W5,D2,L1,V1,M1} R(54239,376) { cyclic( skol30, X,
% 10.69/11.13 skol29, skol29 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol30
% 10.69/11.13 Y := X
% 10.69/11.13 Z := skol29
% 10.69/11.13 T := skol29
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (54272) {G19,W5,D2,L1,V1,M1} R(54260,404) { cyclic( skol29, X
% 10.69/11.13 , skol29, skol29 ) }.
% 10.69/11.13 parent0: (54964) {G3,W5,D2,L1,V1,M1} { cyclic( skol29, X, skol29, skol29 )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54965) {G2,W5,D2,L1,V1,M1} { cyclic( skol29, skol29, X,
% 10.69/11.13 skol29 ) }.
% 10.69/11.13 parent0[1]: (374) {G1,W10,D2,L2,V4,M2} R(15,14) { cyclic( X, Y, Z, T ), !
% 10.69/11.13 cyclic( Y, Z, X, T ) }.
% 10.69/11.13 parent1[0]: (54272) {G19,W5,D2,L1,V1,M1} R(54260,404) { cyclic( skol29, X,
% 10.69/11.13 skol29, skol29 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol29
% 10.69/11.13 Y := skol29
% 10.69/11.13 Z := X
% 10.69/11.13 T := skol29
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (54294) {G20,W5,D2,L1,V1,M1} R(54272,374) { cyclic( skol29,
% 10.69/11.13 skol29, X, skol29 ) }.
% 10.69/11.13 parent0: (54965) {G2,W5,D2,L1,V1,M1} { cyclic( skol29, skol29, X, skol29 )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54966) {G2,W5,D2,L1,V1,M1} { cyclic( skol29, skol29, skol29,
% 10.69/11.13 X ) }.
% 10.69/11.13 parent0[0]: (364) {G1,W10,D2,L2,V4,M2} R(14,13) { ! cyclic( X, Y, Z, T ),
% 10.69/11.13 cyclic( X, Z, T, Y ) }.
% 10.69/11.13 parent1[0]: (54272) {G19,W5,D2,L1,V1,M1} R(54260,404) { cyclic( skol29, X,
% 10.69/11.13 skol29, skol29 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol29
% 10.69/11.13 Y := X
% 10.69/11.13 Z := skol29
% 10.69/11.13 T := skol29
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (54295) {G20,W5,D2,L1,V1,M1} R(54272,364) { cyclic( skol29,
% 10.69/11.13 skol29, skol29, X ) }.
% 10.69/11.13 parent0: (54966) {G2,W5,D2,L1,V1,M1} { cyclic( skol29, skol29, skol29, X )
% 10.69/11.13 }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54968) {G2,W10,D2,L2,V2,M2} { ! cyclic( skol29, skol29,
% 10.69/11.13 skol29, X ), cyclic( skol29, skol29, X, Y ) }.
% 10.69/11.13 parent0[2]: (399) {G1,W15,D2,L3,V5,M3} R(16,13) { ! cyclic( X, Y, Z, T ),
% 10.69/11.13 cyclic( Y, Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 10.69/11.13 parent1[0]: (54294) {G20,W5,D2,L1,V1,M1} R(54272,374) { cyclic( skol29,
% 10.69/11.13 skol29, X, skol29 ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol29
% 10.69/11.13 Y := skol29
% 10.69/11.13 Z := skol29
% 10.69/11.13 T := X
% 10.69/11.13 U := Y
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := Y
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54969) {G3,W5,D2,L1,V2,M1} { cyclic( skol29, skol29, X, Y )
% 10.69/11.13 }.
% 10.69/11.13 parent0[0]: (54968) {G2,W10,D2,L2,V2,M2} { ! cyclic( skol29, skol29,
% 10.69/11.13 skol29, X ), cyclic( skol29, skol29, X, Y ) }.
% 10.69/11.13 parent1[0]: (54295) {G20,W5,D2,L1,V1,M1} R(54272,364) { cyclic( skol29,
% 10.69/11.13 skol29, skol29, X ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (54300) {G21,W5,D2,L1,V2,M1} R(54294,399);r(54295) { cyclic(
% 10.69/11.13 skol29, skol29, X, Y ) }.
% 10.69/11.13 parent0: (54969) {G3,W5,D2,L1,V2,M1} { cyclic( skol29, skol29, X, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54970) {G2,W10,D2,L2,V3,M2} { cyclic( skol29, X, Y, Z ), !
% 10.69/11.13 cyclic( skol29, skol29, Z, X ) }.
% 10.69/11.13 parent0[0]: (399) {G1,W15,D2,L3,V5,M3} R(16,13) { ! cyclic( X, Y, Z, T ),
% 10.69/11.13 cyclic( Y, Z, T, U ), ! cyclic( X, Y, U, Z ) }.
% 10.69/11.13 parent1[0]: (54300) {G21,W5,D2,L1,V2,M1} R(54294,399);r(54295) { cyclic(
% 10.69/11.13 skol29, skol29, X, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol29
% 10.69/11.13 Y := skol29
% 10.69/11.13 Z := X
% 10.69/11.13 T := Y
% 10.69/11.13 U := Z
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54972) {G3,W5,D2,L1,V3,M1} { cyclic( skol29, X, Y, Z ) }.
% 10.69/11.13 parent0[1]: (54970) {G2,W10,D2,L2,V3,M2} { cyclic( skol29, X, Y, Z ), !
% 10.69/11.13 cyclic( skol29, skol29, Z, X ) }.
% 10.69/11.13 parent1[0]: (54300) {G21,W5,D2,L1,V2,M1} R(54294,399);r(54295) { cyclic(
% 10.69/11.13 skol29, skol29, X, Y ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := Z
% 10.69/11.13 Y := X
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (54322) {G22,W5,D2,L1,V3,M1} R(54300,399);r(54300) { cyclic(
% 10.69/11.13 skol29, X, Y, Z ) }.
% 10.69/11.13 parent0: (54972) {G3,W5,D2,L1,V3,M1} { cyclic( skol29, X, Y, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := X
% 10.69/11.13 Y := Y
% 10.69/11.13 Z := Z
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 0 ==> 0
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54973) {G14,W5,D2,L1,V0,M1} { ! cyclic( skol29, skol24,
% 10.69/11.13 skol20, skol23 ) }.
% 10.69/11.13 parent0[0]: (578) {G13,W10,D2,L2,V1,M2} R(576,16) { ! cyclic( X, skol24,
% 10.69/11.13 skol20, skol22 ), ! cyclic( X, skol24, skol20, skol23 ) }.
% 10.69/11.13 parent1[0]: (54322) {G22,W5,D2,L1,V3,M1} R(54300,399);r(54300) { cyclic(
% 10.69/11.13 skol29, X, Y, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 X := skol29
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol24
% 10.69/11.13 Y := skol20
% 10.69/11.13 Z := skol22
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 resolution: (54975) {G15,W0,D0,L0,V0,M0} { }.
% 10.69/11.13 parent0[0]: (54973) {G14,W5,D2,L1,V0,M1} { ! cyclic( skol29, skol24,
% 10.69/11.13 skol20, skol23 ) }.
% 10.69/11.13 parent1[0]: (54322) {G22,W5,D2,L1,V3,M1} R(54300,399);r(54300) { cyclic(
% 10.69/11.13 skol29, X, Y, Z ) }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 substitution1:
% 10.69/11.13 X := skol24
% 10.69/11.13 Y := skol20
% 10.69/11.13 Z := skol23
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 subsumption: (54338) {G23,W0,D0,L0,V0,M0} R(54322,578);r(54322) { }.
% 10.69/11.13 parent0: (54975) {G15,W0,D0,L0,V0,M0} { }.
% 10.69/11.13 substitution0:
% 10.69/11.13 end
% 10.69/11.13 permutation0:
% 10.69/11.13 end
% 10.69/11.13
% 10.69/11.13 Proof check complete!
% 10.69/11.13
% 10.69/11.13 Memory use:
% 10.69/11.13
% 10.69/11.13 space for terms: 717868
% 10.69/11.13 space for clauses: 2467341
% 10.69/11.13
% 10.69/11.13
% 10.69/11.13 clauses generated: 349842
% 10.69/11.13 clauses kept: 54339
% 10.69/11.13 clauses selected: 2823
% 10.69/11.13 clauses deleted: 4684
% 10.69/11.13 clauses inuse deleted: 134
% 10.69/11.13
% 10.69/11.13 subsentry: 15023852
% 10.69/11.13 literals s-matched: 8074579
% 10.69/11.13 literals matched: 4295093
% 10.69/11.13 full subsumption: 1758226
% 10.69/11.13
% 10.69/11.13 checksum: 1818959130
% 10.69/11.13
% 10.69/11.13
% 10.69/11.13 Bliksem ended
%------------------------------------------------------------------------------