%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : PRO012+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n008.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 : Mon Jul 18 17:39:58 EDT 2022
% Result : Theorem 124.45s 124.84s
% Output : Refutation 124.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : PRO012+2 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n008.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Mon Jun 13 03:21:52 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.67/1.07 *** allocated 10000 integers for termspace/termends
% 0.67/1.07 *** allocated 10000 integers for clauses
% 0.67/1.07 *** allocated 10000 integers for justifications
% 0.67/1.07 Bliksem 1.12
% 0.67/1.07
% 0.67/1.07
% 0.67/1.07 Automatic Strategy Selection
% 0.67/1.07
% 0.67/1.07
% 0.67/1.07 Clauses:
% 0.67/1.07
% 0.67/1.07 { ! min_precedes( X, T, Z ), ! min_precedes( T, Y, Z ), min_precedes( X, Y
% 0.67/1.07 , Z ) }.
% 0.67/1.07 { ! earlier( X, Z ), ! earlier( Z, Y ), earlier( X, Y ) }.
% 0.67/1.07 { ! occurrence_of( Z, T ), ! root_occ( X, Z ), ! root_occ( Y, Z ), X = Y }
% 0.67/1.07 .
% 0.67/1.07 { ! occurrence_of( Z, T ), atomic( T ), ! leaf_occ( X, Z ), ! leaf_occ( Y,
% 0.67/1.07 Z ), X = Y }.
% 0.67/1.07 { ! next_subocc( X, Y, Z ), min_precedes( X, Y, Z ) }.
% 0.67/1.07 { ! next_subocc( X, Y, Z ), alpha1( X, Y, Z ) }.
% 0.67/1.07 { ! min_precedes( X, Y, Z ), ! alpha1( X, Y, Z ), next_subocc( X, Y, Z ) }
% 0.67/1.07 .
% 0.67/1.07 { ! alpha1( X, Y, Z ), ! min_precedes( X, T, Z ), ! min_precedes( T, Y, Z )
% 0.67/1.07 }.
% 0.67/1.07 { min_precedes( skol1( T, Y, Z ), Y, Z ), alpha1( X, Y, Z ) }.
% 0.67/1.07 { min_precedes( X, skol1( X, Y, Z ), Z ), alpha1( X, Y, Z ) }.
% 0.67/1.07 { ! next_subocc( X, Y, Z ), arboreal( X ) }.
% 0.67/1.07 { ! next_subocc( X, Y, Z ), arboreal( Y ) }.
% 0.67/1.07 { ! min_precedes( X, Y, Z ), precedes( X, Y ) }.
% 0.67/1.07 { ! min_precedes( Z, X, Y ), ! root( X, Y ) }.
% 0.67/1.07 { ! precedes( X, Y ), earlier( X, Y ) }.
% 0.67/1.07 { ! precedes( X, Y ), legal( Y ) }.
% 0.67/1.07 { ! earlier( X, Y ), ! legal( Y ), precedes( X, Y ) }.
% 0.67/1.07 { ! earlier( X, Y ), ! earlier( Y, X ) }.
% 0.67/1.07 { ! root_occ( X, Y ), occurrence_of( Y, skol2( Z, Y ) ) }.
% 0.67/1.07 { ! root_occ( X, Y ), alpha2( X, Y, skol2( X, Y ) ) }.
% 0.67/1.07 { ! occurrence_of( Y, Z ), ! alpha2( X, Y, Z ), root_occ( X, Y ) }.
% 0.67/1.07 { ! alpha2( X, Y, Z ), subactivity_occurrence( X, Y ) }.
% 0.67/1.07 { ! alpha2( X, Y, Z ), root( X, Z ) }.
% 0.67/1.07 { ! subactivity_occurrence( X, Y ), ! root( X, Z ), alpha2( X, Y, Z ) }.
% 0.67/1.07 { ! leaf_occ( X, Y ), occurrence_of( Y, skol3( Z, Y ) ) }.
% 0.67/1.07 { ! leaf_occ( X, Y ), alpha3( X, Y, skol3( X, Y ) ) }.
% 0.67/1.07 { ! occurrence_of( Y, Z ), ! alpha3( X, Y, Z ), leaf_occ( X, Y ) }.
% 0.67/1.07 { ! alpha3( X, Y, Z ), subactivity_occurrence( X, Y ) }.
% 0.67/1.07 { ! alpha3( X, Y, Z ), leaf( X, Z ) }.
% 0.67/1.07 { ! subactivity_occurrence( X, Y ), ! leaf( X, Z ), alpha3( X, Y, Z ) }.
% 0.67/1.07 { ! root( X, Y ), legal( X ) }.
% 0.67/1.07 { ! occurrence_of( X, Y ), ! arboreal( X ), atomic( Y ) }.
% 0.67/1.07 { ! occurrence_of( X, Y ), ! atomic( Y ), arboreal( X ) }.
% 0.67/1.07 { ! leaf( X, Y ), alpha4( X, Y ) }.
% 0.67/1.07 { ! leaf( X, Y ), ! min_precedes( X, Z, Y ) }.
% 0.67/1.07 { ! alpha4( X, Y ), min_precedes( X, skol4( X, Y ), Y ), leaf( X, Y ) }.
% 0.67/1.07 { ! alpha4( X, Y ), root( X, Y ), min_precedes( skol5( X, Y ), X, Y ) }.
% 0.67/1.07 { ! root( X, Y ), alpha4( X, Y ) }.
% 0.67/1.07 { ! min_precedes( Z, X, Y ), alpha4( X, Y ) }.
% 0.67/1.07 { ! atocc( X, Y ), subactivity( Y, skol6( Z, Y ) ) }.
% 0.67/1.07 { ! atocc( X, Y ), alpha5( X, skol6( X, Y ) ) }.
% 0.67/1.07 { ! subactivity( Y, Z ), ! alpha5( X, Z ), atocc( X, Y ) }.
% 0.67/1.07 { ! alpha5( X, Y ), atomic( Y ) }.
% 0.67/1.07 { ! alpha5( X, Y ), occurrence_of( X, Y ) }.
% 0.67/1.07 { ! atomic( Y ), ! occurrence_of( X, Y ), alpha5( X, Y ) }.
% 0.67/1.07 { ! atocc( X, Y ), ! legal( X ), root( X, Y ) }.
% 0.67/1.07 { ! legal( X ), arboreal( X ) }.
% 0.67/1.07 { ! activity_occurrence( X ), activity( skol7( Y ) ) }.
% 0.67/1.07 { ! activity_occurrence( X ), occurrence_of( X, skol7( X ) ) }.
% 0.67/1.07 { ! subactivity_occurrence( X, Y ), activity_occurrence( X ) }.
% 0.67/1.07 { ! subactivity_occurrence( X, Y ), activity_occurrence( Y ) }.
% 0.67/1.07 { ! occurrence_of( Z, Y ), ! root_occ( X, Z ), ! min_precedes( T, X, Y ) }
% 0.67/1.07 .
% 0.67/1.07 { ! occurrence_of( Z, Y ), ! leaf_occ( X, Z ), ! min_precedes( X, T, Y ) }
% 0.67/1.07 .
% 0.67/1.07 { ! occurrence_of( Z, X ), ! occurrence_of( Z, Y ), X = Y }.
% 0.67/1.07 { ! leaf( X, Y ), atomic( Y ), occurrence_of( skol8( Z, Y ), Y ) }.
% 0.67/1.07 { ! leaf( X, Y ), atomic( Y ), leaf_occ( X, skol8( X, Y ) ) }.
% 0.67/1.07 { ! min_precedes( Y, Z, X ), subactivity_occurrence( Z, skol9( T, U, Z ) )
% 0.67/1.07 }.
% 0.67/1.07 { ! min_precedes( Y, Z, X ), subactivity_occurrence( Y, skol9( T, Y, Z ) )
% 0.67/1.07 }.
% 0.67/1.07 { ! min_precedes( Y, Z, X ), occurrence_of( skol9( X, Y, Z ), X ) }.
% 0.67/1.07 { ! leaf( X, Y ), atomic( Y ), occurrence_of( skol10( Z, Y ), Y ) }.
% 0.67/1.07 { ! leaf( X, Y ), atomic( Y ), leaf_occ( X, skol10( X, Y ) ) }.
% 0.67/1.07 { ! min_precedes( Y, Z, X ), subactivity( skol11( X, T, U ), X ) }.
% 0.67/1.07 { ! min_precedes( Y, Z, X ), alpha6( X, Y, Z, skol11( X, Y, Z ) ) }.
% 0.67/1.07 { ! alpha6( X, Y, Z, T ), atocc( Z, skol12( U, W, Z, V0 ) ) }.
% 0.67/1.07 { ! alpha6( X, Y, Z, T ), subactivity( skol12( X, U, Z, W ), X ) }.
% 0.67/1.07 { ! alpha6( X, Y, Z, T ), atocc( Y, T ) }.
% 0.67/1.07 { ! subactivity( U, X ), ! atocc( Y, T ), ! atocc( Z, U ), alpha6( X, Y, Z
% 1.49/1.86 , T ) }.
% 1.49/1.86 { ! root( Y, X ), atocc( Y, skol13( Z, Y ) ) }.
% 1.49/1.86 { ! root( Y, X ), subactivity( skol13( X, Y ), X ) }.
% 1.49/1.86 { ! occurrence_of( T, X ), ! arboreal( Y ), ! arboreal( Z ), !
% 1.49/1.86 subactivity_occurrence( Y, T ), ! subactivity_occurrence( Z, T ),
% 1.49/1.86 min_precedes( Y, Z, X ), min_precedes( Z, Y, X ), Y = Z }.
% 1.49/1.86 { ! occurrence_of( Y, X ), activity( X ) }.
% 1.49/1.86 { ! occurrence_of( Y, X ), activity_occurrence( Y ) }.
% 1.49/1.86 { ! occurrence_of( Y, X ), atomic( X ), subactivity_occurrence( skol14( Z,
% 1.49/1.86 Y ), Y ) }.
% 1.49/1.86 { ! occurrence_of( Y, X ), atomic( X ), root( skol14( X, Y ), X ) }.
% 1.49/1.86 { ! activity( X ), subactivity( X, X ) }.
% 1.49/1.86 { ! occurrence_of( X, tptp0 ), alpha8( skol15( Y ), skol17( Y ) ) }.
% 1.49/1.86 { ! occurrence_of( X, tptp0 ), alpha9( skol17( Y ), skol18( Y ) ) }.
% 1.49/1.86 { ! occurrence_of( X, tptp0 ), ! min_precedes( skol15( Y ), Z, tptp0 ), Z =
% 1.49/1.86 skol17( Y ), Z = skol18( Y ) }.
% 1.49/1.86 { ! occurrence_of( X, tptp0 ), alpha7( X, skol15( X ) ) }.
% 1.49/1.86 { ! alpha9( X, Y ), occurrence_of( Y, tptp2 ), occurrence_of( Y, tptp1 ) }
% 1.49/1.86 .
% 1.49/1.86 { ! alpha9( X, Y ), min_precedes( X, Y, tptp0 ) }.
% 1.49/1.86 { ! occurrence_of( Y, tptp2 ), ! min_precedes( X, Y, tptp0 ), alpha9( X, Y
% 1.49/1.86 ) }.
% 1.49/1.86 { ! occurrence_of( Y, tptp1 ), ! min_precedes( X, Y, tptp0 ), alpha9( X, Y
% 1.49/1.86 ) }.
% 1.49/1.86 { ! alpha8( X, Y ), occurrence_of( Y, tptp4 ) }.
% 1.49/1.86 { ! alpha8( X, Y ), min_precedes( X, Y, tptp0 ) }.
% 1.49/1.86 { ! occurrence_of( Y, tptp4 ), ! min_precedes( X, Y, tptp0 ), alpha8( X, Y
% 1.49/1.86 ) }.
% 1.49/1.86 { ! alpha7( X, Y ), occurrence_of( Y, tptp3 ) }.
% 1.49/1.86 { ! alpha7( X, Y ), root_occ( Y, X ) }.
% 1.49/1.86 { ! occurrence_of( Y, tptp3 ), ! root_occ( Y, X ), alpha7( X, Y ) }.
% 1.49/1.86 { activity( tptp0 ) }.
% 1.49/1.86 { ! atomic( tptp0 ) }.
% 1.49/1.86 { atomic( tptp4 ) }.
% 1.49/1.86 { atomic( tptp2 ) }.
% 1.49/1.86 { atomic( tptp1 ) }.
% 1.49/1.86 { atomic( tptp3 ) }.
% 1.49/1.86 { ! tptp4 = tptp3 }.
% 1.49/1.86 { ! tptp4 = tptp2 }.
% 1.49/1.86 { ! tptp4 = tptp1 }.
% 1.49/1.86 { ! tptp3 = tptp2 }.
% 1.49/1.86 { ! tptp3 = tptp1 }.
% 1.49/1.86 { ! tptp2 = tptp1 }.
% 1.49/1.86 { occurrence_of( skol16, tptp0 ) }.
% 1.49/1.86 { ! occurrence_of( X, tptp3 ), ! root_occ( X, skol16 ), ! occurrence_of( Y
% 1.49/1.86 , tptp2 ), ! min_precedes( X, Y, tptp0 ) }.
% 1.49/1.86 { ! occurrence_of( X, tptp3 ), ! root_occ( X, skol16 ), ! occurrence_of( Y
% 1.49/1.86 , tptp1 ), ! min_precedes( X, Y, tptp0 ) }.
% 1.49/1.86
% 1.49/1.86 percentage equality = 0.049180, percentage horn = 0.865385
% 1.49/1.86 This is a problem with some equality
% 1.49/1.86
% 1.49/1.86
% 1.49/1.86
% 1.49/1.86 Options Used:
% 1.49/1.86
% 1.49/1.86 useres = 1
% 1.49/1.86 useparamod = 1
% 1.49/1.86 useeqrefl = 1
% 1.49/1.86 useeqfact = 1
% 1.49/1.86 usefactor = 1
% 1.49/1.86 usesimpsplitting = 0
% 1.49/1.86 usesimpdemod = 5
% 1.49/1.86 usesimpres = 3
% 1.49/1.86
% 1.49/1.86 resimpinuse = 1000
% 1.49/1.86 resimpclauses = 20000
% 1.49/1.86 substype = eqrewr
% 1.49/1.86 backwardsubs = 1
% 1.49/1.86 selectoldest = 5
% 1.49/1.86
% 1.49/1.86 litorderings [0] = split
% 1.49/1.86 litorderings [1] = extend the termordering, first sorting on arguments
% 1.49/1.86
% 1.49/1.86 termordering = kbo
% 1.49/1.86
% 1.49/1.86 litapriori = 0
% 1.49/1.86 termapriori = 1
% 1.49/1.86 litaposteriori = 0
% 1.49/1.86 termaposteriori = 0
% 1.49/1.86 demodaposteriori = 0
% 1.49/1.86 ordereqreflfact = 0
% 1.49/1.86
% 1.49/1.86 litselect = negord
% 1.49/1.86
% 1.49/1.86 maxweight = 15
% 1.49/1.86 maxdepth = 30000
% 1.49/1.86 maxlength = 115
% 1.49/1.86 maxnrvars = 195
% 1.49/1.86 excuselevel = 1
% 1.49/1.86 increasemaxweight = 1
% 1.49/1.86
% 1.49/1.86 maxselected = 10000000
% 1.49/1.86 maxnrclauses = 10000000
% 1.49/1.86
% 1.49/1.86 showgenerated = 0
% 1.49/1.86 showkept = 0
% 1.49/1.86 showselected = 0
% 1.49/1.86 showdeleted = 0
% 1.49/1.86 showresimp = 1
% 1.49/1.86 showstatus = 2000
% 1.49/1.86
% 1.49/1.86 prologoutput = 0
% 1.49/1.86 nrgoals = 5000000
% 1.49/1.86 totalproof = 1
% 1.49/1.86
% 1.49/1.86 Symbols occurring in the translation:
% 1.49/1.86
% 1.49/1.86 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.49/1.86 . [1, 2] (w:1, o:129, a:1, s:1, b:0),
% 1.49/1.86 ! [4, 1] (w:0, o:115, a:1, s:1, b:0),
% 1.49/1.86 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.49/1.86 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.49/1.86 min_precedes [39, 3] (w:1, o:177, a:1, s:1, b:0),
% 1.49/1.86 earlier [43, 2] (w:1, o:153, a:1, s:1, b:0),
% 1.49/1.86 occurrence_of [48, 2] (w:1, o:154, a:1, s:1, b:0),
% 1.49/1.86 root_occ [49, 2] (w:1, o:155, a:1, s:1, b:0),
% 1.49/1.86 atomic [54, 1] (w:1, o:120, a:1, s:1, b:0),
% 1.49/1.86 leaf_occ [55, 2] (w:1, o:156, a:1, s:1, b:0),
% 1.49/1.86 next_subocc [59, 3] (w:1, o:178, a:1, s:1, b:0),
% 1.49/1.86 arboreal [64, 1] (w:1, o:121, a:1, s:1, b:0),
% 1.49/1.86 precedes [68, 2] (w:1, o:157, a:1, s:1, b:0),
% 1.49/1.86 root [72, 2] (w:1, o:158, a:1, s:1, b:0),
% 1.49/1.86 legal [75, 1] (w:1, o:122, a:1, s:1, b:0),
% 10.80/11.21 subactivity_occurrence [81, 2] (w:1, o:159, a:1, s:1, b:0),
% 10.80/11.21 leaf [85, 2] (w:1, o:160, a:1, s:1, b:0),
% 10.80/11.21 atocc [96, 2] (w:1, o:161, a:1, s:1, b:0),
% 10.80/11.21 subactivity [98, 2] (w:1, o:162, a:1, s:1, b:0),
% 10.80/11.21 activity_occurrence [103, 1] (w:1, o:123, a:1, s:1, b:0),
% 10.80/11.21 activity [105, 1] (w:1, o:124, a:1, s:1, b:0),
% 10.80/11.21 tptp0 [148, 0] (w:1, o:106, a:1, s:1, b:0),
% 10.80/11.21 tptp3 [152, 0] (w:1, o:112, a:1, s:1, b:0),
% 10.80/11.21 tptp4 [153, 0] (w:1, o:113, a:1, s:1, b:0),
% 10.80/11.21 tptp2 [154, 0] (w:1, o:111, a:1, s:1, b:0),
% 10.80/11.21 tptp1 [155, 0] (w:1, o:110, a:1, s:1, b:0),
% 10.80/11.21 alpha1 [160, 3] (w:1, o:179, a:1, s:1, b:1),
% 10.80/11.21 alpha2 [161, 3] (w:1, o:180, a:1, s:1, b:1),
% 10.80/11.21 alpha3 [162, 3] (w:1, o:181, a:1, s:1, b:1),
% 10.80/11.21 alpha4 [163, 2] (w:1, o:163, a:1, s:1, b:1),
% 10.80/11.21 alpha5 [164, 2] (w:1, o:164, a:1, s:1, b:1),
% 10.80/11.21 alpha6 [165, 4] (w:1, o:185, a:1, s:1, b:1),
% 10.80/11.21 alpha7 [166, 2] (w:1, o:165, a:1, s:1, b:1),
% 10.80/11.21 alpha8 [167, 2] (w:1, o:166, a:1, s:1, b:1),
% 10.80/11.21 alpha9 [168, 2] (w:1, o:167, a:1, s:1, b:1),
% 10.80/11.21 skol1 [169, 3] (w:1, o:182, a:1, s:1, b:1),
% 10.80/11.21 skol2 [170, 2] (w:1, o:171, a:1, s:1, b:1),
% 10.80/11.21 skol3 [171, 2] (w:1, o:172, a:1, s:1, b:1),
% 10.80/11.21 skol4 [172, 2] (w:1, o:173, a:1, s:1, b:1),
% 10.80/11.21 skol5 [173, 2] (w:1, o:174, a:1, s:1, b:1),
% 10.80/11.21 skol6 [174, 2] (w:1, o:175, a:1, s:1, b:1),
% 10.80/11.21 skol7 [175, 1] (w:1, o:125, a:1, s:1, b:1),
% 10.80/11.21 skol8 [176, 2] (w:1, o:176, a:1, s:1, b:1),
% 10.80/11.21 skol9 [177, 3] (w:1, o:183, a:1, s:1, b:1),
% 10.80/11.21 skol10 [178, 2] (w:1, o:168, a:1, s:1, b:1),
% 10.80/11.21 skol11 [179, 3] (w:1, o:184, a:1, s:1, b:1),
% 10.80/11.21 skol12 [180, 4] (w:1, o:186, a:1, s:1, b:1),
% 10.80/11.21 skol13 [181, 2] (w:1, o:169, a:1, s:1, b:1),
% 10.80/11.21 skol14 [182, 2] (w:1, o:170, a:1, s:1, b:1),
% 10.80/11.21 skol15 [183, 1] (w:1, o:126, a:1, s:1, b:1),
% 10.80/11.21 skol16 [184, 0] (w:1, o:105, a:1, s:1, b:1),
% 10.80/11.21 skol17 [185, 1] (w:1, o:127, a:1, s:1, b:1),
% 10.80/11.21 skol18 [186, 1] (w:1, o:128, a:1, s:1, b:1).
% 10.80/11.21
% 10.80/11.21
% 10.80/11.21 Starting Search:
% 10.80/11.21
% 10.80/11.21 *** allocated 15000 integers for clauses
% 10.80/11.21 *** allocated 22500 integers for clauses
% 10.80/11.21 *** allocated 33750 integers for clauses
% 10.80/11.21 *** allocated 15000 integers for termspace/termends
% 10.80/11.21 *** allocated 50625 integers for clauses
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21 *** allocated 22500 integers for termspace/termends
% 10.80/11.21 *** allocated 75937 integers for clauses
% 10.80/11.21 *** allocated 33750 integers for termspace/termends
% 10.80/11.21 *** allocated 113905 integers for clauses
% 10.80/11.21
% 10.80/11.21 Intermediate Status:
% 10.80/11.21 Generated: 5884
% 10.80/11.21 Kept: 2003
% 10.80/11.21 Inuse: 333
% 10.80/11.21 Deleted: 13
% 10.80/11.21 Deletedinuse: 7
% 10.80/11.21
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21 *** allocated 50625 integers for termspace/termends
% 10.80/11.21 *** allocated 170857 integers for clauses
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21 *** allocated 75937 integers for termspace/termends
% 10.80/11.21
% 10.80/11.21 Intermediate Status:
% 10.80/11.21 Generated: 16040
% 10.80/11.21 Kept: 4035
% 10.80/11.21 Inuse: 604
% 10.80/11.21 Deleted: 77
% 10.80/11.21 Deletedinuse: 33
% 10.80/11.21
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21 *** allocated 256285 integers for clauses
% 10.80/11.21 *** allocated 113905 integers for termspace/termends
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21
% 10.80/11.21 Intermediate Status:
% 10.80/11.21 Generated: 25610
% 10.80/11.21 Kept: 6271
% 10.80/11.21 Inuse: 773
% 10.80/11.21 Deleted: 89
% 10.80/11.21 Deletedinuse: 37
% 10.80/11.21
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21 *** allocated 384427 integers for clauses
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21 *** allocated 170857 integers for termspace/termends
% 10.80/11.21
% 10.80/11.21 Intermediate Status:
% 10.80/11.21 Generated: 36423
% 10.80/11.21 Kept: 8688
% 10.80/11.21 Inuse: 904
% 10.80/11.21 Deleted: 133
% 10.80/11.21 Deletedinuse: 68
% 10.80/11.21
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21 *** allocated 576640 integers for clauses
% 10.80/11.21
% 10.80/11.21 Intermediate Status:
% 10.80/11.21 Generated: 44089
% 10.80/11.21 Kept: 10701
% 10.80/11.21 Inuse: 985
% 10.80/11.21 Deleted: 142
% 10.80/11.21 Deletedinuse: 70
% 10.80/11.21
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21 *** allocated 256285 integers for termspace/termends
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21
% 10.80/11.21 Intermediate Status:
% 10.80/11.21 Generated: 52980
% 10.80/11.21 Kept: 12711
% 10.80/11.21 Inuse: 1085
% 10.80/11.21 Deleted: 154
% 10.80/11.21 Deletedinuse: 78
% 10.80/11.21
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21
% 10.80/11.21 Intermediate Status:
% 10.80/11.21 Generated: 63579
% 10.80/11.21 Kept: 14747
% 10.80/11.21 Inuse: 1189
% 10.80/11.21 Deleted: 162
% 10.80/11.21 Deletedinuse: 80
% 10.80/11.21
% 10.80/11.21 *** allocated 864960 integers for clauses
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 10.80/11.21
% 10.80/11.21 Resimplifying inuse:
% 10.80/11.21 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 77089
% 65.07/65.49 Kept: 16774
% 65.07/65.49 Inuse: 1296
% 65.07/65.49 Deleted: 168
% 65.07/65.49 Deletedinuse: 83
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 *** allocated 384427 integers for termspace/termends
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 87741
% 65.07/65.49 Kept: 18777
% 65.07/65.49 Inuse: 1404
% 65.07/65.49 Deleted: 189
% 65.07/65.49 Deletedinuse: 99
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying clauses:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 102333
% 65.07/65.49 Kept: 20793
% 65.07/65.49 Inuse: 1490
% 65.07/65.49 Deleted: 2635
% 65.07/65.49 Deletedinuse: 101
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 *** allocated 1297440 integers for clauses
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 112273
% 65.07/65.49 Kept: 22793
% 65.07/65.49 Inuse: 1574
% 65.07/65.49 Deleted: 2635
% 65.07/65.49 Deletedinuse: 101
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 127345
% 65.07/65.49 Kept: 24796
% 65.07/65.49 Inuse: 1693
% 65.07/65.49 Deleted: 2652
% 65.07/65.49 Deletedinuse: 112
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 142711
% 65.07/65.49 Kept: 26805
% 65.07/65.49 Inuse: 1796
% 65.07/65.49 Deleted: 2654
% 65.07/65.49 Deletedinuse: 114
% 65.07/65.49
% 65.07/65.49 *** allocated 576640 integers for termspace/termends
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 162058
% 65.07/65.49 Kept: 28808
% 65.07/65.49 Inuse: 1907
% 65.07/65.49 Deleted: 2677
% 65.07/65.49 Deletedinuse: 132
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 170489
% 65.07/65.49 Kept: 30837
% 65.07/65.49 Inuse: 2002
% 65.07/65.49 Deleted: 2677
% 65.07/65.49 Deletedinuse: 132
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 *** allocated 1946160 integers for clauses
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 180284
% 65.07/65.49 Kept: 34266
% 65.07/65.49 Inuse: 2066
% 65.07/65.49 Deleted: 2690
% 65.07/65.49 Deletedinuse: 144
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 190537
% 65.07/65.49 Kept: 38801
% 65.07/65.49 Inuse: 2075
% 65.07/65.49 Deleted: 2695
% 65.07/65.49 Deletedinuse: 148
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 *** allocated 864960 integers for termspace/termends
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying clauses:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 198320
% 65.07/65.49 Kept: 40815
% 65.07/65.49 Inuse: 2085
% 65.07/65.49 Deleted: 4865
% 65.07/65.49 Deletedinuse: 148
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 211707
% 65.07/65.49 Kept: 42950
% 65.07/65.49 Inuse: 2148
% 65.07/65.49 Deleted: 4867
% 65.07/65.49 Deletedinuse: 149
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 223992
% 65.07/65.49 Kept: 45227
% 65.07/65.49 Inuse: 2213
% 65.07/65.49 Deleted: 4868
% 65.07/65.49 Deletedinuse: 150
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 236506
% 65.07/65.49 Kept: 47259
% 65.07/65.49 Inuse: 2268
% 65.07/65.49 Deleted: 4868
% 65.07/65.49 Deletedinuse: 150
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 253416
% 65.07/65.49 Kept: 49270
% 65.07/65.49 Inuse: 2334
% 65.07/65.49 Deleted: 4868
% 65.07/65.49 Deletedinuse: 150
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 273794
% 65.07/65.49 Kept: 51294
% 65.07/65.49 Inuse: 2411
% 65.07/65.49 Deleted: 4868
% 65.07/65.49 Deletedinuse: 150
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 *** allocated 2919240 integers for clauses
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 296033
% 65.07/65.49 Kept: 53300
% 65.07/65.49 Inuse: 2511
% 65.07/65.49 Deleted: 4877
% 65.07/65.49 Deletedinuse: 154
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 309742
% 65.07/65.49 Kept: 55305
% 65.07/65.49 Inuse: 2606
% 65.07/65.49 Deleted: 4878
% 65.07/65.49 Deletedinuse: 154
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 325142
% 65.07/65.49 Kept: 57328
% 65.07/65.49 Inuse: 2683
% 65.07/65.49 Deleted: 4884
% 65.07/65.49 Deletedinuse: 160
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 *** allocated 1297440 integers for termspace/termends
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 337242
% 65.07/65.49 Kept: 59386
% 65.07/65.49 Inuse: 2742
% 65.07/65.49 Deleted: 4884
% 65.07/65.49 Deletedinuse: 160
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying clauses:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 364669
% 65.07/65.49 Kept: 61869
% 65.07/65.49 Inuse: 2787
% 65.07/65.49 Deleted: 6221
% 65.07/65.49 Deletedinuse: 162
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49 Resimplifying inuse:
% 65.07/65.49 Done
% 65.07/65.49
% 65.07/65.49
% 65.07/65.49 Intermediate Status:
% 65.07/65.49 Generated: 377631
% 124.45/124.84 Kept: 63871
% 124.45/124.84 Inuse: 2831
% 124.45/124.84 Deleted: 6222
% 124.45/124.84 Deletedinuse: 163
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 397035
% 124.45/124.84 Kept: 65883
% 124.45/124.84 Inuse: 2906
% 124.45/124.84 Deleted: 6222
% 124.45/124.84 Deletedinuse: 163
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 418207
% 124.45/124.84 Kept: 67911
% 124.45/124.84 Inuse: 2982
% 124.45/124.84 Deleted: 6224
% 124.45/124.84 Deletedinuse: 165
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 436385
% 124.45/124.84 Kept: 69919
% 124.45/124.84 Inuse: 3055
% 124.45/124.84 Deleted: 6224
% 124.45/124.84 Deletedinuse: 165
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 449859
% 124.45/124.84 Kept: 71933
% 124.45/124.84 Inuse: 3141
% 124.45/124.84 Deleted: 6305
% 124.45/124.84 Deletedinuse: 236
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 463094
% 124.45/124.84 Kept: 73991
% 124.45/124.84 Inuse: 3199
% 124.45/124.84 Deleted: 6306
% 124.45/124.84 Deletedinuse: 236
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 474779
% 124.45/124.84 Kept: 76016
% 124.45/124.84 Inuse: 3265
% 124.45/124.84 Deleted: 6307
% 124.45/124.84 Deletedinuse: 236
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 *** allocated 4378860 integers for clauses
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 486101
% 124.45/124.84 Kept: 78126
% 124.45/124.84 Inuse: 3325
% 124.45/124.84 Deleted: 6315
% 124.45/124.84 Deletedinuse: 244
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 496250
% 124.45/124.84 Kept: 80146
% 124.45/124.84 Inuse: 3373
% 124.45/124.84 Deleted: 6323
% 124.45/124.84 Deletedinuse: 248
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying clauses:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 512999
% 124.45/124.84 Kept: 82148
% 124.45/124.84 Inuse: 3462
% 124.45/124.84 Deleted: 9203
% 124.45/124.84 Deletedinuse: 248
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 531277
% 124.45/124.84 Kept: 84165
% 124.45/124.84 Inuse: 3527
% 124.45/124.84 Deleted: 9203
% 124.45/124.84 Deletedinuse: 248
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 *** allocated 1946160 integers for termspace/termends
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 545753
% 124.45/124.84 Kept: 86178
% 124.45/124.84 Inuse: 3590
% 124.45/124.84 Deleted: 9204
% 124.45/124.84 Deletedinuse: 249
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 573127
% 124.45/124.84 Kept: 88352
% 124.45/124.84 Inuse: 3634
% 124.45/124.84 Deleted: 9204
% 124.45/124.84 Deletedinuse: 249
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 589404
% 124.45/124.84 Kept: 90368
% 124.45/124.84 Inuse: 3686
% 124.45/124.84 Deleted: 9204
% 124.45/124.84 Deletedinuse: 249
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 764929
% 124.45/124.84 Kept: 92420
% 124.45/124.84 Inuse: 3780
% 124.45/124.84 Deleted: 9204
% 124.45/124.84 Deletedinuse: 249
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 831813
% 124.45/124.84 Kept: 94429
% 124.45/124.84 Inuse: 3805
% 124.45/124.84 Deleted: 9204
% 124.45/124.84 Deletedinuse: 249
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1039608
% 124.45/124.84 Kept: 96458
% 124.45/124.84 Inuse: 3920
% 124.45/124.84 Deleted: 9204
% 124.45/124.84 Deletedinuse: 249
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1090008
% 124.45/124.84 Kept: 98462
% 124.45/124.84 Inuse: 3986
% 124.45/124.84 Deleted: 9206
% 124.45/124.84 Deletedinuse: 251
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1142243
% 124.45/124.84 Kept: 100471
% 124.45/124.84 Inuse: 4066
% 124.45/124.84 Deleted: 9222
% 124.45/124.84 Deletedinuse: 267
% 124.45/124.84
% 124.45/124.84 Resimplifying clauses:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1182756
% 124.45/124.84 Kept: 102524
% 124.45/124.84 Inuse: 4143
% 124.45/124.84 Deleted: 10392
% 124.45/124.84 Deletedinuse: 279
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1206271
% 124.45/124.84 Kept: 104526
% 124.45/124.84 Inuse: 4187
% 124.45/124.84 Deleted: 10438
% 124.45/124.84 Deletedinuse: 324
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1229169
% 124.45/124.84 Kept: 106542
% 124.45/124.84 Inuse: 4227
% 124.45/124.84 Deleted: 10438
% 124.45/124.84 Deletedinuse: 324
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1261758
% 124.45/124.84 Kept: 108551
% 124.45/124.84 Inuse: 4306
% 124.45/124.84 Deleted: 10441
% 124.45/124.84 Deletedinuse: 324
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1288918
% 124.45/124.84 Kept: 110559
% 124.45/124.84 Inuse: 4391
% 124.45/124.84 Deleted: 10451
% 124.45/124.84 Deletedinuse: 325
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1475220
% 124.45/124.84 Kept: 112571
% 124.45/124.84 Inuse: 4475
% 124.45/124.84 Deleted: 10453
% 124.45/124.84 Deletedinuse: 326
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1594632
% 124.45/124.84 Kept: 114576
% 124.45/124.84 Inuse: 4567
% 124.45/124.84 Deleted: 10461
% 124.45/124.84 Deletedinuse: 327
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1737734
% 124.45/124.84 Kept: 116632
% 124.45/124.84 Inuse: 4653
% 124.45/124.84 Deleted: 10473
% 124.45/124.84 Deletedinuse: 329
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 *** allocated 6568290 integers for clauses
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1885472
% 124.45/124.84 Kept: 118637
% 124.45/124.84 Inuse: 4758
% 124.45/124.84 Deleted: 10475
% 124.45/124.84 Deletedinuse: 329
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1907994
% 124.45/124.84 Kept: 120691
% 124.45/124.84 Inuse: 4823
% 124.45/124.84 Deleted: 10493
% 124.45/124.84 Deletedinuse: 330
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying clauses:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1940955
% 124.45/124.84 Kept: 122717
% 124.45/124.84 Inuse: 4887
% 124.45/124.84 Deleted: 12721
% 124.45/124.84 Deletedinuse: 330
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 1976925
% 124.45/124.84 Kept: 124724
% 124.45/124.84 Inuse: 4954
% 124.45/124.84 Deleted: 12721
% 124.45/124.84 Deletedinuse: 330
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 2041132
% 124.45/124.84 Kept: 126728
% 124.45/124.84 Inuse: 5005
% 124.45/124.84 Deleted: 12724
% 124.45/124.84 Deletedinuse: 331
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 *** allocated 2919240 integers for termspace/termends
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 2078751
% 124.45/124.84 Kept: 128772
% 124.45/124.84 Inuse: 5038
% 124.45/124.84 Deleted: 12724
% 124.45/124.84 Deletedinuse: 331
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 2116213
% 124.45/124.84 Kept: 130797
% 124.45/124.84 Inuse: 5084
% 124.45/124.84 Deleted: 12724
% 124.45/124.84 Deletedinuse: 331
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Intermediate Status:
% 124.45/124.84 Generated: 2176511
% 124.45/124.84 Kept: 132798
% 124.45/124.84 Inuse: 5164
% 124.45/124.84 Deleted: 12724
% 124.45/124.84 Deletedinuse: 331
% 124.45/124.84
% 124.45/124.84 Resimplifying inuse:
% 124.45/124.84 Done
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Bliksems!, er is een bewijs:
% 124.45/124.84 % SZS status Theorem
% 124.45/124.84 % SZS output start Refutation
% 124.45/124.84
% 124.45/124.84 (0) {G0,W12,D2,L3,V4,M3} I { ! min_precedes( X, T, Z ), ! min_precedes( T,
% 124.45/124.84 Y, Z ), min_precedes( X, Y, Z ) }.
% 124.45/124.84 (2) {G0,W12,D2,L4,V4,M4} I { ! occurrence_of( Z, T ), ! root_occ( X, Z ), !
% 124.45/124.84 root_occ( Y, Z ), X = Y }.
% 124.45/124.84 (7) {G0,W12,D2,L3,V4,M3} I { ! alpha1( X, Y, Z ), ! min_precedes( X, T, Z )
% 124.45/124.84 , ! min_precedes( T, Y, Z ) }.
% 124.45/124.84 (8) {G0,W11,D3,L2,V4,M2} I { min_precedes( skol1( T, Y, Z ), Y, Z ), alpha1
% 124.45/124.84 ( X, Y, Z ) }.
% 124.45/124.84 (9) {G0,W11,D3,L2,V3,M2} I { min_precedes( X, skol1( X, Y, Z ), Z ), alpha1
% 124.45/124.84 ( X, Y, Z ) }.
% 124.45/124.84 (18) {G0,W8,D3,L2,V3,M2} I { ! root_occ( X, Y ), occurrence_of( Y, skol2( Z
% 124.45/124.84 , Y ) ) }.
% 124.45/124.84 (75) {G0,W8,D3,L2,V2,M2} I { ! occurrence_of( X, tptp0 ), alpha8( skol15( Y
% 124.45/124.84 ), skol17( Y ) ) }.
% 124.45/124.84 (76) {G0,W8,D3,L2,V2,M2} I { ! occurrence_of( X, tptp0 ), alpha9( skol17( Y
% 124.45/124.84 ), skol18( Y ) ) }.
% 124.45/124.84 (78) {G0,W7,D3,L2,V1,M2} I { ! occurrence_of( X, tptp0 ), alpha7( X, skol15
% 124.45/124.84 ( X ) ) }.
% 124.45/124.84 (79) {G0,W9,D2,L3,V2,M3} I { ! alpha9( X, Y ), occurrence_of( Y, tptp2 ),
% 124.45/124.84 occurrence_of( Y, tptp1 ) }.
% 124.45/124.84 (80) {G0,W7,D2,L2,V2,M2} I { ! alpha9( X, Y ), min_precedes( X, Y, tptp0 )
% 124.45/124.84 }.
% 124.45/124.84 (84) {G0,W7,D2,L2,V2,M2} I { ! alpha8( X, Y ), min_precedes( X, Y, tptp0 )
% 124.45/124.84 }.
% 124.45/124.84 (86) {G0,W6,D2,L2,V2,M2} I { ! alpha7( X, Y ), occurrence_of( Y, tptp3 )
% 124.45/124.84 }.
% 124.45/124.84 (87) {G0,W6,D2,L2,V2,M2} I { ! alpha7( X, Y ), root_occ( Y, X ) }.
% 124.45/124.84 (101) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol16, tptp0 ) }.
% 124.45/124.84 (102) {G0,W13,D2,L4,V2,M4} I { ! occurrence_of( X, tptp3 ), ! root_occ( X,
% 124.45/124.84 skol16 ), ! occurrence_of( Y, tptp2 ), ! min_precedes( X, Y, tptp0 ) }.
% 124.45/124.84 (103) {G0,W13,D2,L4,V2,M4} I { ! occurrence_of( X, tptp3 ), ! root_occ( X,
% 124.45/124.84 skol16 ), ! occurrence_of( Y, tptp1 ), ! min_precedes( X, Y, tptp0 ) }.
% 124.45/124.84 (201) {G1,W15,D3,L3,V5,M3} R(8,0) { alpha1( X, Y, Z ), ! min_precedes( T,
% 124.45/124.84 skol1( U, Y, Z ), Z ), min_precedes( T, Y, Z ) }.
% 124.45/124.84 (266) {G1,W12,D2,L4,V4,M4} R(18,2) { ! root_occ( X, Y ), ! root_occ( Z, Y )
% 124.45/124.84 , ! root_occ( T, Y ), Z = T }.
% 124.45/124.84 (270) {G2,W9,D2,L3,V3,M3} F(266) { ! root_occ( X, Y ), ! root_occ( Z, Y ),
% 124.45/124.84 X = Z }.
% 124.45/124.84 (1435) {G1,W5,D3,L1,V1,M1} R(75,101) { alpha8( skol15( X ), skol17( X ) )
% 124.45/124.84 }.
% 124.45/124.84 (1454) {G1,W5,D3,L1,V1,M1} R(76,101) { alpha9( skol17( X ), skol18( X ) )
% 124.45/124.84 }.
% 124.45/124.84 (1468) {G2,W6,D3,L1,V1,M1} R(1435,84) { min_precedes( skol15( X ), skol17(
% 124.45/124.84 X ), tptp0 ) }.
% 124.45/124.84 (1615) {G1,W4,D3,L1,V0,M1} R(78,101) { alpha7( skol16, skol15( skol16 ) )
% 124.45/124.84 }.
% 124.45/124.84 (1725) {G1,W11,D2,L3,V3,M3} R(80,7) { ! alpha9( X, Y ), ! alpha1( Z, Y,
% 124.45/124.84 tptp0 ), ! min_precedes( Z, X, tptp0 ) }.
% 124.45/124.84 (1754) {G2,W4,D3,L1,V0,M1} R(1615,86) { occurrence_of( skol15( skol16 ),
% 124.45/124.84 tptp3 ) }.
% 124.45/124.84 (1755) {G2,W4,D3,L1,V0,M1} R(1615,87) { root_occ( skol15( skol16 ), skol16
% 124.45/124.84 ) }.
% 124.45/124.84 (1915) {G3,W8,D3,L2,V1,M2} R(102,1755);r(1754) { ! occurrence_of( X, tptp2
% 124.45/124.84 ), ! min_precedes( skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.84 (1960) {G3,W8,D3,L2,V1,M2} R(103,1755);r(1754) { ! occurrence_of( X, tptp1
% 124.45/124.84 ), ! min_precedes( skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.84 (5410) {G2,W12,D2,L3,V4,M3} R(201,9) { alpha1( X, Y, Z ), min_precedes( T,
% 124.45/124.84 Y, Z ), alpha1( T, Y, Z ) }.
% 124.45/124.84 (5411) {G3,W8,D2,L2,V3,M2} F(5410) { alpha1( X, Y, Z ), min_precedes( X, Y
% 124.45/124.84 , Z ) }.
% 124.45/124.84 (9012) {G3,W7,D3,L2,V1,M2} R(270,1755) { ! root_occ( X, skol16 ), skol15(
% 124.45/124.84 skol16 ) = X }.
% 124.45/124.84 (13816) {G4,W8,D3,L2,V1,M2} P(9012,1468) { min_precedes( X, skol17( skol16
% 124.45/124.84 ), tptp0 ), ! root_occ( X, skol16 ) }.
% 124.45/124.84 (100949) {G4,W8,D3,L2,V2,M2} R(1960,79);r(1915) { ! min_precedes( skol15(
% 124.45/124.84 skol16 ), X, tptp0 ), ! alpha9( Y, X ) }.
% 124.45/124.84 (101335) {G5,W8,D3,L2,V2,M2} R(100949,5411) { ! alpha9( X, Y ), alpha1(
% 124.45/124.84 skol15( skol16 ), Y, tptp0 ) }.
% 124.45/124.84 (133671) {G6,W11,D3,L3,V3,M3} R(1725,101335) { ! alpha9( X, Y ), !
% 124.45/124.84 min_precedes( skol15( skol16 ), X, tptp0 ), ! alpha9( Z, Y ) }.
% 124.45/124.84 (133704) {G7,W8,D3,L2,V2,M2} F(133671) { ! alpha9( X, Y ), ! min_precedes(
% 124.45/124.84 skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.84 (133708) {G8,W4,D3,L1,V1,M1} R(133704,13816);r(1755) { ! alpha9( skol17(
% 124.45/124.84 skol16 ), X ) }.
% 124.45/124.84 (133755) {G9,W0,D0,L0,V0,M0} R(133708,1454) { }.
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 % SZS output end Refutation
% 124.45/124.84 found a proof!
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Unprocessed initial clauses:
% 124.45/124.84
% 124.45/124.84 (133757) {G0,W12,D2,L3,V4,M3} { ! min_precedes( X, T, Z ), ! min_precedes
% 124.45/124.84 ( T, Y, Z ), min_precedes( X, Y, Z ) }.
% 124.45/124.84 (133758) {G0,W9,D2,L3,V3,M3} { ! earlier( X, Z ), ! earlier( Z, Y ),
% 124.45/124.84 earlier( X, Y ) }.
% 124.45/124.84 (133759) {G0,W12,D2,L4,V4,M4} { ! occurrence_of( Z, T ), ! root_occ( X, Z
% 124.45/124.84 ), ! root_occ( Y, Z ), X = Y }.
% 124.45/124.84 (133760) {G0,W14,D2,L5,V4,M5} { ! occurrence_of( Z, T ), atomic( T ), !
% 124.45/124.84 leaf_occ( X, Z ), ! leaf_occ( Y, Z ), X = Y }.
% 124.45/124.84 (133761) {G0,W8,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), min_precedes( X,
% 124.45/124.84 Y, Z ) }.
% 124.45/124.84 (133762) {G0,W8,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), alpha1( X, Y, Z )
% 124.45/124.84 }.
% 124.45/124.84 (133763) {G0,W12,D2,L3,V3,M3} { ! min_precedes( X, Y, Z ), ! alpha1( X, Y
% 124.45/124.84 , Z ), next_subocc( X, Y, Z ) }.
% 124.45/124.84 (133764) {G0,W12,D2,L3,V4,M3} { ! alpha1( X, Y, Z ), ! min_precedes( X, T
% 124.45/124.84 , Z ), ! min_precedes( T, Y, Z ) }.
% 124.45/124.84 (133765) {G0,W11,D3,L2,V4,M2} { min_precedes( skol1( T, Y, Z ), Y, Z ),
% 124.45/124.84 alpha1( X, Y, Z ) }.
% 124.45/124.84 (133766) {G0,W11,D3,L2,V3,M2} { min_precedes( X, skol1( X, Y, Z ), Z ),
% 124.45/124.84 alpha1( X, Y, Z ) }.
% 124.45/124.84 (133767) {G0,W6,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), arboreal( X ) }.
% 124.45/124.84 (133768) {G0,W6,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), arboreal( Y ) }.
% 124.45/124.84 (133769) {G0,W7,D2,L2,V3,M2} { ! min_precedes( X, Y, Z ), precedes( X, Y )
% 124.45/124.84 }.
% 124.45/124.84 (133770) {G0,W7,D2,L2,V3,M2} { ! min_precedes( Z, X, Y ), ! root( X, Y )
% 124.45/124.84 }.
% 124.45/124.84 (133771) {G0,W6,D2,L2,V2,M2} { ! precedes( X, Y ), earlier( X, Y ) }.
% 124.45/124.84 (133772) {G0,W5,D2,L2,V2,M2} { ! precedes( X, Y ), legal( Y ) }.
% 124.45/124.84 (133773) {G0,W8,D2,L3,V2,M3} { ! earlier( X, Y ), ! legal( Y ), precedes(
% 124.45/124.84 X, Y ) }.
% 124.45/124.84 (133774) {G0,W6,D2,L2,V2,M2} { ! earlier( X, Y ), ! earlier( Y, X ) }.
% 124.45/124.84 (133775) {G0,W8,D3,L2,V3,M2} { ! root_occ( X, Y ), occurrence_of( Y, skol2
% 124.45/124.84 ( Z, Y ) ) }.
% 124.45/124.84 (133776) {G0,W9,D3,L2,V2,M2} { ! root_occ( X, Y ), alpha2( X, Y, skol2( X
% 124.45/124.84 , Y ) ) }.
% 124.45/124.84 (133777) {G0,W10,D2,L3,V3,M3} { ! occurrence_of( Y, Z ), ! alpha2( X, Y, Z
% 124.45/124.84 ), root_occ( X, Y ) }.
% 124.45/124.84 (133778) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), subactivity_occurrence
% 124.45/124.84 ( X, Y ) }.
% 124.45/124.84 (133779) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), root( X, Z ) }.
% 124.45/124.84 (133780) {G0,W10,D2,L3,V3,M3} { ! subactivity_occurrence( X, Y ), ! root(
% 124.45/124.84 X, Z ), alpha2( X, Y, Z ) }.
% 124.45/124.84 (133781) {G0,W8,D3,L2,V3,M2} { ! leaf_occ( X, Y ), occurrence_of( Y, skol3
% 124.45/124.84 ( Z, Y ) ) }.
% 124.45/124.84 (133782) {G0,W9,D3,L2,V2,M2} { ! leaf_occ( X, Y ), alpha3( X, Y, skol3( X
% 124.45/124.84 , Y ) ) }.
% 124.45/124.84 (133783) {G0,W10,D2,L3,V3,M3} { ! occurrence_of( Y, Z ), ! alpha3( X, Y, Z
% 124.45/124.84 ), leaf_occ( X, Y ) }.
% 124.45/124.84 (133784) {G0,W7,D2,L2,V3,M2} { ! alpha3( X, Y, Z ), subactivity_occurrence
% 124.45/124.84 ( X, Y ) }.
% 124.45/124.84 (133785) {G0,W7,D2,L2,V3,M2} { ! alpha3( X, Y, Z ), leaf( X, Z ) }.
% 124.45/124.84 (133786) {G0,W10,D2,L3,V3,M3} { ! subactivity_occurrence( X, Y ), ! leaf(
% 124.45/124.84 X, Z ), alpha3( X, Y, Z ) }.
% 124.45/124.84 (133787) {G0,W5,D2,L2,V2,M2} { ! root( X, Y ), legal( X ) }.
% 124.45/124.84 (133788) {G0,W7,D2,L3,V2,M3} { ! occurrence_of( X, Y ), ! arboreal( X ),
% 124.45/124.84 atomic( Y ) }.
% 124.45/124.84 (133789) {G0,W7,D2,L3,V2,M3} { ! occurrence_of( X, Y ), ! atomic( Y ),
% 124.45/124.84 arboreal( X ) }.
% 124.45/124.84 (133790) {G0,W6,D2,L2,V2,M2} { ! leaf( X, Y ), alpha4( X, Y ) }.
% 124.45/124.84 (133791) {G0,W7,D2,L2,V3,M2} { ! leaf( X, Y ), ! min_precedes( X, Z, Y )
% 124.45/124.84 }.
% 124.45/124.84 (133792) {G0,W12,D3,L3,V2,M3} { ! alpha4( X, Y ), min_precedes( X, skol4(
% 124.45/124.84 X, Y ), Y ), leaf( X, Y ) }.
% 124.45/124.84 (133793) {G0,W12,D3,L3,V2,M3} { ! alpha4( X, Y ), root( X, Y ),
% 124.45/124.84 min_precedes( skol5( X, Y ), X, Y ) }.
% 124.45/124.84 (133794) {G0,W6,D2,L2,V2,M2} { ! root( X, Y ), alpha4( X, Y ) }.
% 124.45/124.84 (133795) {G0,W7,D2,L2,V3,M2} { ! min_precedes( Z, X, Y ), alpha4( X, Y )
% 124.45/124.84 }.
% 124.45/124.84 (133796) {G0,W8,D3,L2,V3,M2} { ! atocc( X, Y ), subactivity( Y, skol6( Z,
% 124.45/124.84 Y ) ) }.
% 124.45/124.84 (133797) {G0,W8,D3,L2,V2,M2} { ! atocc( X, Y ), alpha5( X, skol6( X, Y ) )
% 124.45/124.84 }.
% 124.45/124.84 (133798) {G0,W9,D2,L3,V3,M3} { ! subactivity( Y, Z ), ! alpha5( X, Z ),
% 124.45/124.84 atocc( X, Y ) }.
% 124.45/124.84 (133799) {G0,W5,D2,L2,V2,M2} { ! alpha5( X, Y ), atomic( Y ) }.
% 124.45/124.84 (133800) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), occurrence_of( X, Y ) }.
% 124.45/124.84 (133801) {G0,W8,D2,L3,V2,M3} { ! atomic( Y ), ! occurrence_of( X, Y ),
% 124.45/124.84 alpha5( X, Y ) }.
% 124.45/124.84 (133802) {G0,W8,D2,L3,V2,M3} { ! atocc( X, Y ), ! legal( X ), root( X, Y )
% 124.45/124.84 }.
% 124.45/124.84 (133803) {G0,W4,D2,L2,V1,M2} { ! legal( X ), arboreal( X ) }.
% 124.45/124.84 (133804) {G0,W5,D3,L2,V2,M2} { ! activity_occurrence( X ), activity( skol7
% 124.45/124.84 ( Y ) ) }.
% 124.45/124.84 (133805) {G0,W6,D3,L2,V1,M2} { ! activity_occurrence( X ), occurrence_of(
% 124.45/124.84 X, skol7( X ) ) }.
% 124.45/124.84 (133806) {G0,W5,D2,L2,V2,M2} { ! subactivity_occurrence( X, Y ),
% 124.45/124.84 activity_occurrence( X ) }.
% 124.45/124.84 (133807) {G0,W5,D2,L2,V2,M2} { ! subactivity_occurrence( X, Y ),
% 124.45/124.84 activity_occurrence( Y ) }.
% 124.45/124.84 (133808) {G0,W10,D2,L3,V4,M3} { ! occurrence_of( Z, Y ), ! root_occ( X, Z
% 124.45/124.84 ), ! min_precedes( T, X, Y ) }.
% 124.45/124.84 (133809) {G0,W10,D2,L3,V4,M3} { ! occurrence_of( Z, Y ), ! leaf_occ( X, Z
% 124.45/124.84 ), ! min_precedes( X, T, Y ) }.
% 124.45/124.84 (133810) {G0,W9,D2,L3,V3,M3} { ! occurrence_of( Z, X ), ! occurrence_of( Z
% 124.45/124.84 , Y ), X = Y }.
% 124.45/124.84 (133811) {G0,W10,D3,L3,V3,M3} { ! leaf( X, Y ), atomic( Y ), occurrence_of
% 124.45/124.84 ( skol8( Z, Y ), Y ) }.
% 124.45/124.84 (133812) {G0,W10,D3,L3,V2,M3} { ! leaf( X, Y ), atomic( Y ), leaf_occ( X,
% 124.45/124.84 skol8( X, Y ) ) }.
% 124.45/124.84 (133813) {G0,W10,D3,L2,V5,M2} { ! min_precedes( Y, Z, X ),
% 124.45/124.84 subactivity_occurrence( Z, skol9( T, U, Z ) ) }.
% 124.45/124.84 (133814) {G0,W10,D3,L2,V4,M2} { ! min_precedes( Y, Z, X ),
% 124.45/124.84 subactivity_occurrence( Y, skol9( T, Y, Z ) ) }.
% 124.45/124.84 (133815) {G0,W10,D3,L2,V3,M2} { ! min_precedes( Y, Z, X ), occurrence_of(
% 124.45/124.84 skol9( X, Y, Z ), X ) }.
% 124.45/124.84 (133816) {G0,W10,D3,L3,V3,M3} { ! leaf( X, Y ), atomic( Y ), occurrence_of
% 124.45/124.84 ( skol10( Z, Y ), Y ) }.
% 124.45/124.84 (133817) {G0,W10,D3,L3,V2,M3} { ! leaf( X, Y ), atomic( Y ), leaf_occ( X,
% 124.45/124.84 skol10( X, Y ) ) }.
% 124.45/124.84 (133818) {G0,W10,D3,L2,V5,M2} { ! min_precedes( Y, Z, X ), subactivity(
% 124.45/124.84 skol11( X, T, U ), X ) }.
% 124.45/124.84 (133819) {G0,W12,D3,L2,V3,M2} { ! min_precedes( Y, Z, X ), alpha6( X, Y, Z
% 124.45/124.84 , skol11( X, Y, Z ) ) }.
% 124.45/124.84 (133820) {G0,W12,D3,L2,V7,M2} { ! alpha6( X, Y, Z, T ), atocc( Z, skol12(
% 124.45/124.84 U, W, Z, V0 ) ) }.
% 124.45/124.84 (133821) {G0,W12,D3,L2,V6,M2} { ! alpha6( X, Y, Z, T ), subactivity(
% 124.45/124.84 skol12( X, U, Z, W ), X ) }.
% 124.45/124.84 (133822) {G0,W8,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), atocc( Y, T ) }.
% 124.45/124.84 (133823) {G0,W14,D2,L4,V5,M4} { ! subactivity( U, X ), ! atocc( Y, T ), !
% 124.45/124.84 atocc( Z, U ), alpha6( X, Y, Z, T ) }.
% 124.45/124.84 (133824) {G0,W8,D3,L2,V3,M2} { ! root( Y, X ), atocc( Y, skol13( Z, Y ) )
% 124.45/124.84 }.
% 124.45/124.84 (133825) {G0,W8,D3,L2,V2,M2} { ! root( Y, X ), subactivity( skol13( X, Y )
% 124.45/124.84 , X ) }.
% 124.45/124.84 (133826) {G0,W24,D2,L8,V4,M8} { ! occurrence_of( T, X ), ! arboreal( Y ),
% 124.45/124.84 ! arboreal( Z ), ! subactivity_occurrence( Y, T ), !
% 124.45/124.84 subactivity_occurrence( Z, T ), min_precedes( Y, Z, X ), min_precedes( Z
% 124.45/124.84 , Y, X ), Y = Z }.
% 124.45/124.84 (133827) {G0,W5,D2,L2,V2,M2} { ! occurrence_of( Y, X ), activity( X ) }.
% 124.45/124.84 (133828) {G0,W5,D2,L2,V2,M2} { ! occurrence_of( Y, X ),
% 124.45/124.84 activity_occurrence( Y ) }.
% 124.45/124.84 (133829) {G0,W10,D3,L3,V3,M3} { ! occurrence_of( Y, X ), atomic( X ),
% 124.45/124.84 subactivity_occurrence( skol14( Z, Y ), Y ) }.
% 124.45/124.84 (133830) {G0,W10,D3,L3,V2,M3} { ! occurrence_of( Y, X ), atomic( X ), root
% 124.45/124.84 ( skol14( X, Y ), X ) }.
% 124.45/124.84 (133831) {G0,W5,D2,L2,V1,M2} { ! activity( X ), subactivity( X, X ) }.
% 124.45/124.84 (133832) {G0,W8,D3,L2,V2,M2} { ! occurrence_of( X, tptp0 ), alpha8( skol15
% 124.45/124.84 ( Y ), skol17( Y ) ) }.
% 124.45/124.84 (133833) {G0,W8,D3,L2,V2,M2} { ! occurrence_of( X, tptp0 ), alpha9( skol17
% 124.45/124.84 ( Y ), skol18( Y ) ) }.
% 124.45/124.84 (133834) {G0,W16,D3,L4,V3,M4} { ! occurrence_of( X, tptp0 ), !
% 124.45/124.84 min_precedes( skol15( Y ), Z, tptp0 ), Z = skol17( Y ), Z = skol18( Y )
% 124.45/124.84 }.
% 124.45/124.84 (133835) {G0,W7,D3,L2,V1,M2} { ! occurrence_of( X, tptp0 ), alpha7( X,
% 124.45/124.84 skol15( X ) ) }.
% 124.45/124.84 (133836) {G0,W9,D2,L3,V2,M3} { ! alpha9( X, Y ), occurrence_of( Y, tptp2 )
% 124.45/124.84 , occurrence_of( Y, tptp1 ) }.
% 124.45/124.84 (133837) {G0,W7,D2,L2,V2,M2} { ! alpha9( X, Y ), min_precedes( X, Y, tptp0
% 124.45/124.84 ) }.
% 124.45/124.84 (133838) {G0,W10,D2,L3,V2,M3} { ! occurrence_of( Y, tptp2 ), !
% 124.45/124.84 min_precedes( X, Y, tptp0 ), alpha9( X, Y ) }.
% 124.45/124.84 (133839) {G0,W10,D2,L3,V2,M3} { ! occurrence_of( Y, tptp1 ), !
% 124.45/124.84 min_precedes( X, Y, tptp0 ), alpha9( X, Y ) }.
% 124.45/124.84 (133840) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), occurrence_of( Y, tptp4 )
% 124.45/124.84 }.
% 124.45/124.84 (133841) {G0,W7,D2,L2,V2,M2} { ! alpha8( X, Y ), min_precedes( X, Y, tptp0
% 124.45/124.84 ) }.
% 124.45/124.84 (133842) {G0,W10,D2,L3,V2,M3} { ! occurrence_of( Y, tptp4 ), !
% 124.45/124.84 min_precedes( X, Y, tptp0 ), alpha8( X, Y ) }.
% 124.45/124.84 (133843) {G0,W6,D2,L2,V2,M2} { ! alpha7( X, Y ), occurrence_of( Y, tptp3 )
% 124.45/124.84 }.
% 124.45/124.84 (133844) {G0,W6,D2,L2,V2,M2} { ! alpha7( X, Y ), root_occ( Y, X ) }.
% 124.45/124.84 (133845) {G0,W9,D2,L3,V2,M3} { ! occurrence_of( Y, tptp3 ), ! root_occ( Y
% 124.45/124.84 , X ), alpha7( X, Y ) }.
% 124.45/124.84 (133846) {G0,W2,D2,L1,V0,M1} { activity( tptp0 ) }.
% 124.45/124.84 (133847) {G0,W2,D2,L1,V0,M1} { ! atomic( tptp0 ) }.
% 124.45/124.84 (133848) {G0,W2,D2,L1,V0,M1} { atomic( tptp4 ) }.
% 124.45/124.84 (133849) {G0,W2,D2,L1,V0,M1} { atomic( tptp2 ) }.
% 124.45/124.84 (133850) {G0,W2,D2,L1,V0,M1} { atomic( tptp1 ) }.
% 124.45/124.84 (133851) {G0,W2,D2,L1,V0,M1} { atomic( tptp3 ) }.
% 124.45/124.84 (133852) {G0,W3,D2,L1,V0,M1} { ! tptp4 = tptp3 }.
% 124.45/124.84 (133853) {G0,W3,D2,L1,V0,M1} { ! tptp4 = tptp2 }.
% 124.45/124.84 (133854) {G0,W3,D2,L1,V0,M1} { ! tptp4 = tptp1 }.
% 124.45/124.84 (133855) {G0,W3,D2,L1,V0,M1} { ! tptp3 = tptp2 }.
% 124.45/124.84 (133856) {G0,W3,D2,L1,V0,M1} { ! tptp3 = tptp1 }.
% 124.45/124.84 (133857) {G0,W3,D2,L1,V0,M1} { ! tptp2 = tptp1 }.
% 124.45/124.84 (133858) {G0,W3,D2,L1,V0,M1} { occurrence_of( skol16, tptp0 ) }.
% 124.45/124.84 (133859) {G0,W13,D2,L4,V2,M4} { ! occurrence_of( X, tptp3 ), ! root_occ( X
% 124.45/124.84 , skol16 ), ! occurrence_of( Y, tptp2 ), ! min_precedes( X, Y, tptp0 )
% 124.45/124.84 }.
% 124.45/124.84 (133860) {G0,W13,D2,L4,V2,M4} { ! occurrence_of( X, tptp3 ), ! root_occ( X
% 124.45/124.84 , skol16 ), ! occurrence_of( Y, tptp1 ), ! min_precedes( X, Y, tptp0 )
% 124.45/124.84 }.
% 124.45/124.84
% 124.45/124.84
% 124.45/124.84 Total Proof:
% 124.45/124.84
% 124.45/124.84 subsumption: (0) {G0,W12,D2,L3,V4,M3} I { ! min_precedes( X, T, Z ), !
% 124.45/124.84 min_precedes( T, Y, Z ), min_precedes( X, Y, Z ) }.
% 124.45/124.84 parent0: (133757) {G0,W12,D2,L3,V4,M3} { ! min_precedes( X, T, Z ), !
% 124.45/124.84 min_precedes( T, Y, Z ), min_precedes( X, Y, Z ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 Z := Z
% 124.45/124.84 T := T
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 2 ==> 2
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (2) {G0,W12,D2,L4,V4,M4} I { ! occurrence_of( Z, T ), !
% 124.45/124.84 root_occ( X, Z ), ! root_occ( Y, Z ), X = Y }.
% 124.45/124.84 parent0: (133759) {G0,W12,D2,L4,V4,M4} { ! occurrence_of( Z, T ), !
% 124.45/124.84 root_occ( X, Z ), ! root_occ( Y, Z ), X = Y }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 Z := Z
% 124.45/124.84 T := T
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 2 ==> 2
% 124.45/124.84 3 ==> 3
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (7) {G0,W12,D2,L3,V4,M3} I { ! alpha1( X, Y, Z ), !
% 124.45/124.84 min_precedes( X, T, Z ), ! min_precedes( T, Y, Z ) }.
% 124.45/124.84 parent0: (133764) {G0,W12,D2,L3,V4,M3} { ! alpha1( X, Y, Z ), !
% 124.45/124.84 min_precedes( X, T, Z ), ! min_precedes( T, Y, Z ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 Z := Z
% 124.45/124.84 T := T
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 2 ==> 2
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (8) {G0,W11,D3,L2,V4,M2} I { min_precedes( skol1( T, Y, Z ), Y
% 124.45/124.84 , Z ), alpha1( X, Y, Z ) }.
% 124.45/124.84 parent0: (133765) {G0,W11,D3,L2,V4,M2} { min_precedes( skol1( T, Y, Z ), Y
% 124.45/124.84 , Z ), alpha1( X, Y, Z ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 Z := Z
% 124.45/124.84 T := T
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (9) {G0,W11,D3,L2,V3,M2} I { min_precedes( X, skol1( X, Y, Z )
% 124.45/124.84 , Z ), alpha1( X, Y, Z ) }.
% 124.45/124.84 parent0: (133766) {G0,W11,D3,L2,V3,M2} { min_precedes( X, skol1( X, Y, Z )
% 124.45/124.84 , Z ), alpha1( X, Y, Z ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 Z := Z
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (18) {G0,W8,D3,L2,V3,M2} I { ! root_occ( X, Y ), occurrence_of
% 124.45/124.84 ( Y, skol2( Z, Y ) ) }.
% 124.45/124.84 parent0: (133775) {G0,W8,D3,L2,V3,M2} { ! root_occ( X, Y ), occurrence_of
% 124.45/124.84 ( Y, skol2( Z, Y ) ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 Z := Z
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (75) {G0,W8,D3,L2,V2,M2} I { ! occurrence_of( X, tptp0 ),
% 124.45/124.84 alpha8( skol15( Y ), skol17( Y ) ) }.
% 124.45/124.84 parent0: (133832) {G0,W8,D3,L2,V2,M2} { ! occurrence_of( X, tptp0 ),
% 124.45/124.84 alpha8( skol15( Y ), skol17( Y ) ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (76) {G0,W8,D3,L2,V2,M2} I { ! occurrence_of( X, tptp0 ),
% 124.45/124.84 alpha9( skol17( Y ), skol18( Y ) ) }.
% 124.45/124.84 parent0: (133833) {G0,W8,D3,L2,V2,M2} { ! occurrence_of( X, tptp0 ),
% 124.45/124.84 alpha9( skol17( Y ), skol18( Y ) ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (78) {G0,W7,D3,L2,V1,M2} I { ! occurrence_of( X, tptp0 ),
% 124.45/124.84 alpha7( X, skol15( X ) ) }.
% 124.45/124.84 parent0: (133835) {G0,W7,D3,L2,V1,M2} { ! occurrence_of( X, tptp0 ),
% 124.45/124.84 alpha7( X, skol15( X ) ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (79) {G0,W9,D2,L3,V2,M3} I { ! alpha9( X, Y ), occurrence_of(
% 124.45/124.84 Y, tptp2 ), occurrence_of( Y, tptp1 ) }.
% 124.45/124.84 parent0: (133836) {G0,W9,D2,L3,V2,M3} { ! alpha9( X, Y ), occurrence_of( Y
% 124.45/124.84 , tptp2 ), occurrence_of( Y, tptp1 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 2 ==> 2
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (80) {G0,W7,D2,L2,V2,M2} I { ! alpha9( X, Y ), min_precedes( X
% 124.45/124.84 , Y, tptp0 ) }.
% 124.45/124.84 parent0: (133837) {G0,W7,D2,L2,V2,M2} { ! alpha9( X, Y ), min_precedes( X
% 124.45/124.84 , Y, tptp0 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (84) {G0,W7,D2,L2,V2,M2} I { ! alpha8( X, Y ), min_precedes( X
% 124.45/124.84 , Y, tptp0 ) }.
% 124.45/124.84 parent0: (133841) {G0,W7,D2,L2,V2,M2} { ! alpha8( X, Y ), min_precedes( X
% 124.45/124.84 , Y, tptp0 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (86) {G0,W6,D2,L2,V2,M2} I { ! alpha7( X, Y ), occurrence_of(
% 124.45/124.84 Y, tptp3 ) }.
% 124.45/124.84 parent0: (133843) {G0,W6,D2,L2,V2,M2} { ! alpha7( X, Y ), occurrence_of( Y
% 124.45/124.84 , tptp3 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (87) {G0,W6,D2,L2,V2,M2} I { ! alpha7( X, Y ), root_occ( Y, X
% 124.45/124.84 ) }.
% 124.45/124.84 parent0: (133844) {G0,W6,D2,L2,V2,M2} { ! alpha7( X, Y ), root_occ( Y, X )
% 124.45/124.84 }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (101) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol16, tptp0 )
% 124.45/124.84 }.
% 124.45/124.84 parent0: (133858) {G0,W3,D2,L1,V0,M1} { occurrence_of( skol16, tptp0 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (102) {G0,W13,D2,L4,V2,M4} I { ! occurrence_of( X, tptp3 ), !
% 124.45/124.84 root_occ( X, skol16 ), ! occurrence_of( Y, tptp2 ), ! min_precedes( X, Y
% 124.45/124.84 , tptp0 ) }.
% 124.45/124.84 parent0: (133859) {G0,W13,D2,L4,V2,M4} { ! occurrence_of( X, tptp3 ), !
% 124.45/124.84 root_occ( X, skol16 ), ! occurrence_of( Y, tptp2 ), ! min_precedes( X, Y
% 124.45/124.84 , tptp0 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 2 ==> 2
% 124.45/124.84 3 ==> 3
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (103) {G0,W13,D2,L4,V2,M4} I { ! occurrence_of( X, tptp3 ), !
% 124.45/124.84 root_occ( X, skol16 ), ! occurrence_of( Y, tptp1 ), ! min_precedes( X, Y
% 124.45/124.84 , tptp0 ) }.
% 124.45/124.84 parent0: (133860) {G0,W13,D2,L4,V2,M4} { ! occurrence_of( X, tptp3 ), !
% 124.45/124.84 root_occ( X, skol16 ), ! occurrence_of( Y, tptp1 ), ! min_precedes( X, Y
% 124.45/124.84 , tptp0 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 2 ==> 2
% 124.45/124.84 3 ==> 3
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 resolution: (134086) {G1,W15,D3,L3,V5,M3} { ! min_precedes( X, skol1( Y, Z
% 124.45/124.84 , T ), T ), min_precedes( X, Z, T ), alpha1( U, Z, T ) }.
% 124.45/124.84 parent0[1]: (0) {G0,W12,D2,L3,V4,M3} I { ! min_precedes( X, T, Z ), !
% 124.45/124.84 min_precedes( T, Y, Z ), min_precedes( X, Y, Z ) }.
% 124.45/124.84 parent1[0]: (8) {G0,W11,D3,L2,V4,M2} I { min_precedes( skol1( T, Y, Z ), Y
% 124.45/124.84 , Z ), alpha1( X, Y, Z ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Z
% 124.45/124.84 Z := T
% 124.45/124.84 T := skol1( Y, Z, T )
% 124.45/124.84 end
% 124.45/124.84 substitution1:
% 124.45/124.84 X := U
% 124.45/124.84 Y := Z
% 124.45/124.84 Z := T
% 124.45/124.84 T := Y
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (201) {G1,W15,D3,L3,V5,M3} R(8,0) { alpha1( X, Y, Z ), !
% 124.45/124.84 min_precedes( T, skol1( U, Y, Z ), Z ), min_precedes( T, Y, Z ) }.
% 124.45/124.84 parent0: (134086) {G1,W15,D3,L3,V5,M3} { ! min_precedes( X, skol1( Y, Z, T
% 124.45/124.84 ), T ), min_precedes( X, Z, T ), alpha1( U, Z, T ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := T
% 124.45/124.84 Y := U
% 124.45/124.84 Z := Y
% 124.45/124.84 T := Z
% 124.45/124.84 U := X
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 1
% 124.45/124.84 1 ==> 2
% 124.45/124.84 2 ==> 0
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 resolution: (134087) {G1,W12,D2,L4,V4,M4} { ! root_occ( Z, X ), ! root_occ
% 124.45/124.84 ( T, X ), Z = T, ! root_occ( U, X ) }.
% 124.45/124.84 parent0[0]: (2) {G0,W12,D2,L4,V4,M4} I { ! occurrence_of( Z, T ), !
% 124.45/124.84 root_occ( X, Z ), ! root_occ( Y, Z ), X = Y }.
% 124.45/124.84 parent1[1]: (18) {G0,W8,D3,L2,V3,M2} I { ! root_occ( X, Y ), occurrence_of
% 124.45/124.84 ( Y, skol2( Z, Y ) ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := Z
% 124.45/124.84 Y := T
% 124.45/124.84 Z := X
% 124.45/124.84 T := skol2( Y, X )
% 124.45/124.84 end
% 124.45/124.84 substitution1:
% 124.45/124.84 X := U
% 124.45/124.84 Y := X
% 124.45/124.84 Z := Y
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (266) {G1,W12,D2,L4,V4,M4} R(18,2) { ! root_occ( X, Y ), !
% 124.45/124.84 root_occ( Z, Y ), ! root_occ( T, Y ), Z = T }.
% 124.45/124.84 parent0: (134087) {G1,W12,D2,L4,V4,M4} { ! root_occ( Z, X ), ! root_occ( T
% 124.45/124.84 , X ), Z = T, ! root_occ( U, X ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := Y
% 124.45/124.84 Y := U
% 124.45/124.84 Z := Z
% 124.45/124.84 T := T
% 124.45/124.84 U := X
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 1
% 124.45/124.84 1 ==> 2
% 124.45/124.84 2 ==> 3
% 124.45/124.84 3 ==> 0
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 factor: (134091) {G1,W9,D2,L3,V3,M3} { ! root_occ( X, Y ), ! root_occ( Z,
% 124.45/124.84 Y ), X = Z }.
% 124.45/124.84 parent0[0, 1]: (266) {G1,W12,D2,L4,V4,M4} R(18,2) { ! root_occ( X, Y ), !
% 124.45/124.84 root_occ( Z, Y ), ! root_occ( T, Y ), Z = T }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 Z := X
% 124.45/124.84 T := Z
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (270) {G2,W9,D2,L3,V3,M3} F(266) { ! root_occ( X, Y ), !
% 124.45/124.84 root_occ( Z, Y ), X = Z }.
% 124.45/124.84 parent0: (134091) {G1,W9,D2,L3,V3,M3} { ! root_occ( X, Y ), ! root_occ( Z
% 124.45/124.84 , Y ), X = Z }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 Z := Z
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 1 ==> 1
% 124.45/124.84 2 ==> 2
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 resolution: (134093) {G1,W5,D3,L1,V1,M1} { alpha8( skol15( X ), skol17( X
% 124.45/124.84 ) ) }.
% 124.45/124.84 parent0[0]: (75) {G0,W8,D3,L2,V2,M2} I { ! occurrence_of( X, tptp0 ),
% 124.45/124.84 alpha8( skol15( Y ), skol17( Y ) ) }.
% 124.45/124.84 parent1[0]: (101) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol16, tptp0 )
% 124.45/124.84 }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := skol16
% 124.45/124.84 Y := X
% 124.45/124.84 end
% 124.45/124.84 substitution1:
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (1435) {G1,W5,D3,L1,V1,M1} R(75,101) { alpha8( skol15( X ),
% 124.45/124.84 skol17( X ) ) }.
% 124.45/124.84 parent0: (134093) {G1,W5,D3,L1,V1,M1} { alpha8( skol15( X ), skol17( X ) )
% 124.45/124.84 }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 resolution: (134094) {G1,W5,D3,L1,V1,M1} { alpha9( skol17( X ), skol18( X
% 124.45/124.84 ) ) }.
% 124.45/124.84 parent0[0]: (76) {G0,W8,D3,L2,V2,M2} I { ! occurrence_of( X, tptp0 ),
% 124.45/124.84 alpha9( skol17( Y ), skol18( Y ) ) }.
% 124.45/124.84 parent1[0]: (101) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol16, tptp0 )
% 124.45/124.84 }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := skol16
% 124.45/124.84 Y := X
% 124.45/124.84 end
% 124.45/124.84 substitution1:
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (1454) {G1,W5,D3,L1,V1,M1} R(76,101) { alpha9( skol17( X ),
% 124.45/124.84 skol18( X ) ) }.
% 124.45/124.84 parent0: (134094) {G1,W5,D3,L1,V1,M1} { alpha9( skol17( X ), skol18( X ) )
% 124.45/124.84 }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 resolution: (134095) {G1,W6,D3,L1,V1,M1} { min_precedes( skol15( X ),
% 124.45/124.84 skol17( X ), tptp0 ) }.
% 124.45/124.84 parent0[0]: (84) {G0,W7,D2,L2,V2,M2} I { ! alpha8( X, Y ), min_precedes( X
% 124.45/124.84 , Y, tptp0 ) }.
% 124.45/124.84 parent1[0]: (1435) {G1,W5,D3,L1,V1,M1} R(75,101) { alpha8( skol15( X ),
% 124.45/124.84 skol17( X ) ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := skol15( X )
% 124.45/124.84 Y := skol17( X )
% 124.45/124.84 end
% 124.45/124.84 substitution1:
% 124.45/124.84 X := X
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (1468) {G2,W6,D3,L1,V1,M1} R(1435,84) { min_precedes( skol15(
% 124.45/124.84 X ), skol17( X ), tptp0 ) }.
% 124.45/124.84 parent0: (134095) {G1,W6,D3,L1,V1,M1} { min_precedes( skol15( X ), skol17
% 124.45/124.84 ( X ), tptp0 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 resolution: (134096) {G1,W4,D3,L1,V0,M1} { alpha7( skol16, skol15( skol16
% 124.45/124.84 ) ) }.
% 124.45/124.84 parent0[0]: (78) {G0,W7,D3,L2,V1,M2} I { ! occurrence_of( X, tptp0 ),
% 124.45/124.84 alpha7( X, skol15( X ) ) }.
% 124.45/124.84 parent1[0]: (101) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol16, tptp0 )
% 124.45/124.84 }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := skol16
% 124.45/124.84 end
% 124.45/124.84 substitution1:
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (1615) {G1,W4,D3,L1,V0,M1} R(78,101) { alpha7( skol16, skol15
% 124.45/124.84 ( skol16 ) ) }.
% 124.45/124.84 parent0: (134096) {G1,W4,D3,L1,V0,M1} { alpha7( skol16, skol15( skol16 ) )
% 124.45/124.84 }.
% 124.45/124.84 substitution0:
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 resolution: (134098) {G1,W11,D2,L3,V3,M3} { ! alpha1( X, Y, tptp0 ), !
% 124.45/124.84 min_precedes( X, Z, tptp0 ), ! alpha9( Z, Y ) }.
% 124.45/124.84 parent0[2]: (7) {G0,W12,D2,L3,V4,M3} I { ! alpha1( X, Y, Z ), !
% 124.45/124.84 min_precedes( X, T, Z ), ! min_precedes( T, Y, Z ) }.
% 124.45/124.84 parent1[1]: (80) {G0,W7,D2,L2,V2,M2} I { ! alpha9( X, Y ), min_precedes( X
% 124.45/124.84 , Y, tptp0 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 Y := Y
% 124.45/124.84 Z := tptp0
% 124.45/124.84 T := Z
% 124.45/124.84 end
% 124.45/124.84 substitution1:
% 124.45/124.84 X := Z
% 124.45/124.84 Y := Y
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (1725) {G1,W11,D2,L3,V3,M3} R(80,7) { ! alpha9( X, Y ), !
% 124.45/124.84 alpha1( Z, Y, tptp0 ), ! min_precedes( Z, X, tptp0 ) }.
% 124.45/124.84 parent0: (134098) {G1,W11,D2,L3,V3,M3} { ! alpha1( X, Y, tptp0 ), !
% 124.45/124.84 min_precedes( X, Z, tptp0 ), ! alpha9( Z, Y ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := Z
% 124.45/124.84 Y := Y
% 124.45/124.84 Z := X
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 1
% 124.45/124.84 1 ==> 2
% 124.45/124.84 2 ==> 0
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 resolution: (134099) {G1,W4,D3,L1,V0,M1} { occurrence_of( skol15( skol16 )
% 124.45/124.84 , tptp3 ) }.
% 124.45/124.84 parent0[0]: (86) {G0,W6,D2,L2,V2,M2} I { ! alpha7( X, Y ), occurrence_of( Y
% 124.45/124.84 , tptp3 ) }.
% 124.45/124.84 parent1[0]: (1615) {G1,W4,D3,L1,V0,M1} R(78,101) { alpha7( skol16, skol15(
% 124.45/124.84 skol16 ) ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := skol16
% 124.45/124.84 Y := skol15( skol16 )
% 124.45/124.84 end
% 124.45/124.84 substitution1:
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (1754) {G2,W4,D3,L1,V0,M1} R(1615,86) { occurrence_of( skol15
% 124.45/124.84 ( skol16 ), tptp3 ) }.
% 124.45/124.84 parent0: (134099) {G1,W4,D3,L1,V0,M1} { occurrence_of( skol15( skol16 ),
% 124.45/124.84 tptp3 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 resolution: (134100) {G1,W4,D3,L1,V0,M1} { root_occ( skol15( skol16 ),
% 124.45/124.84 skol16 ) }.
% 124.45/124.84 parent0[0]: (87) {G0,W6,D2,L2,V2,M2} I { ! alpha7( X, Y ), root_occ( Y, X )
% 124.45/124.84 }.
% 124.45/124.84 parent1[0]: (1615) {G1,W4,D3,L1,V0,M1} R(78,101) { alpha7( skol16, skol15(
% 124.45/124.84 skol16 ) ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := skol16
% 124.45/124.84 Y := skol15( skol16 )
% 124.45/124.84 end
% 124.45/124.84 substitution1:
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (1755) {G2,W4,D3,L1,V0,M1} R(1615,87) { root_occ( skol15(
% 124.45/124.84 skol16 ), skol16 ) }.
% 124.45/124.84 parent0: (134100) {G1,W4,D3,L1,V0,M1} { root_occ( skol15( skol16 ), skol16
% 124.45/124.84 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 end
% 124.45/124.84 permutation0:
% 124.45/124.84 0 ==> 0
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 resolution: (134101) {G1,W12,D3,L3,V1,M3} { ! occurrence_of( skol15(
% 124.45/124.84 skol16 ), tptp3 ), ! occurrence_of( X, tptp2 ), ! min_precedes( skol15(
% 124.45/124.84 skol16 ), X, tptp0 ) }.
% 124.45/124.84 parent0[1]: (102) {G0,W13,D2,L4,V2,M4} I { ! occurrence_of( X, tptp3 ), !
% 124.45/124.84 root_occ( X, skol16 ), ! occurrence_of( Y, tptp2 ), ! min_precedes( X, Y
% 124.45/124.84 , tptp0 ) }.
% 124.45/124.84 parent1[0]: (1755) {G2,W4,D3,L1,V0,M1} R(1615,87) { root_occ( skol15(
% 124.45/124.84 skol16 ), skol16 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := skol15( skol16 )
% 124.45/124.84 Y := X
% 124.45/124.84 end
% 124.45/124.84 substitution1:
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 resolution: (134102) {G2,W8,D3,L2,V1,M2} { ! occurrence_of( X, tptp2 ), !
% 124.45/124.84 min_precedes( skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.84 parent0[0]: (134101) {G1,W12,D3,L3,V1,M3} { ! occurrence_of( skol15(
% 124.45/124.84 skol16 ), tptp3 ), ! occurrence_of( X, tptp2 ), ! min_precedes( skol15(
% 124.45/124.84 skol16 ), X, tptp0 ) }.
% 124.45/124.84 parent1[0]: (1754) {G2,W4,D3,L1,V0,M1} R(1615,86) { occurrence_of( skol15(
% 124.45/124.84 skol16 ), tptp3 ) }.
% 124.45/124.84 substitution0:
% 124.45/124.84 X := X
% 124.45/124.84 end
% 124.45/124.84 substitution1:
% 124.45/124.84 end
% 124.45/124.84
% 124.45/124.84 subsumption: (1915) {G3,W8,D3,L2,V1,M2} R(102,1755);r(1754) { !
% 124.45/124.84 occurrence_of( X, tptp2 ), ! min_precedes( skol15( skol16 ), X, tptp0 )
% 124.45/124.84 }.
% 124.45/124.84 parent0: (134102) {G2,W8,D3,L2,V1,M2} { ! occurrence_of( X, tptp2 ), !
% 124.45/124.85 min_precedes( skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 0 ==> 0
% 124.45/124.85 1 ==> 1
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 resolution: (134103) {G1,W12,D3,L3,V1,M3} { ! occurrence_of( skol15(
% 124.45/124.85 skol16 ), tptp3 ), ! occurrence_of( X, tptp1 ), ! min_precedes( skol15(
% 124.45/124.85 skol16 ), X, tptp0 ) }.
% 124.45/124.85 parent0[1]: (103) {G0,W13,D2,L4,V2,M4} I { ! occurrence_of( X, tptp3 ), !
% 124.45/124.85 root_occ( X, skol16 ), ! occurrence_of( Y, tptp1 ), ! min_precedes( X, Y
% 124.45/124.85 , tptp0 ) }.
% 124.45/124.85 parent1[0]: (1755) {G2,W4,D3,L1,V0,M1} R(1615,87) { root_occ( skol15(
% 124.45/124.85 skol16 ), skol16 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := skol15( skol16 )
% 124.45/124.85 Y := X
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 resolution: (134104) {G2,W8,D3,L2,V1,M2} { ! occurrence_of( X, tptp1 ), !
% 124.45/124.85 min_precedes( skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.85 parent0[0]: (134103) {G1,W12,D3,L3,V1,M3} { ! occurrence_of( skol15(
% 124.45/124.85 skol16 ), tptp3 ), ! occurrence_of( X, tptp1 ), ! min_precedes( skol15(
% 124.45/124.85 skol16 ), X, tptp0 ) }.
% 124.45/124.85 parent1[0]: (1754) {G2,W4,D3,L1,V0,M1} R(1615,86) { occurrence_of( skol15(
% 124.45/124.85 skol16 ), tptp3 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 subsumption: (1960) {G3,W8,D3,L2,V1,M2} R(103,1755);r(1754) { !
% 124.45/124.85 occurrence_of( X, tptp1 ), ! min_precedes( skol15( skol16 ), X, tptp0 )
% 124.45/124.85 }.
% 124.45/124.85 parent0: (134104) {G2,W8,D3,L2,V1,M2} { ! occurrence_of( X, tptp1 ), !
% 124.45/124.85 min_precedes( skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 0 ==> 0
% 124.45/124.85 1 ==> 1
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 resolution: (134105) {G1,W12,D2,L3,V4,M3} { alpha1( X, Y, Z ),
% 124.45/124.85 min_precedes( T, Y, Z ), alpha1( T, Y, Z ) }.
% 124.45/124.85 parent0[1]: (201) {G1,W15,D3,L3,V5,M3} R(8,0) { alpha1( X, Y, Z ), !
% 124.45/124.85 min_precedes( T, skol1( U, Y, Z ), Z ), min_precedes( T, Y, Z ) }.
% 124.45/124.85 parent1[0]: (9) {G0,W11,D3,L2,V3,M2} I { min_precedes( X, skol1( X, Y, Z )
% 124.45/124.85 , Z ), alpha1( X, Y, Z ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 Z := Z
% 124.45/124.85 T := T
% 124.45/124.85 U := T
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 X := T
% 124.45/124.85 Y := Y
% 124.45/124.85 Z := Z
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 subsumption: (5410) {G2,W12,D2,L3,V4,M3} R(201,9) { alpha1( X, Y, Z ),
% 124.45/124.85 min_precedes( T, Y, Z ), alpha1( T, Y, Z ) }.
% 124.45/124.85 parent0: (134105) {G1,W12,D2,L3,V4,M3} { alpha1( X, Y, Z ), min_precedes(
% 124.45/124.85 T, Y, Z ), alpha1( T, Y, Z ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 Z := Z
% 124.45/124.85 T := T
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 0 ==> 0
% 124.45/124.85 1 ==> 1
% 124.45/124.85 2 ==> 2
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 factor: (134107) {G2,W8,D2,L2,V3,M2} { alpha1( X, Y, Z ), min_precedes( X
% 124.45/124.85 , Y, Z ) }.
% 124.45/124.85 parent0[0, 2]: (5410) {G2,W12,D2,L3,V4,M3} R(201,9) { alpha1( X, Y, Z ),
% 124.45/124.85 min_precedes( T, Y, Z ), alpha1( T, Y, Z ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 Z := Z
% 124.45/124.85 T := X
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 subsumption: (5411) {G3,W8,D2,L2,V3,M2} F(5410) { alpha1( X, Y, Z ),
% 124.45/124.85 min_precedes( X, Y, Z ) }.
% 124.45/124.85 parent0: (134107) {G2,W8,D2,L2,V3,M2} { alpha1( X, Y, Z ), min_precedes( X
% 124.45/124.85 , Y, Z ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 Z := Z
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 0 ==> 0
% 124.45/124.85 1 ==> 1
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 resolution: (134108) {G3,W7,D3,L2,V1,M2} { ! root_occ( X, skol16 ), skol15
% 124.45/124.85 ( skol16 ) = X }.
% 124.45/124.85 parent0[0]: (270) {G2,W9,D2,L3,V3,M3} F(266) { ! root_occ( X, Y ), !
% 124.45/124.85 root_occ( Z, Y ), X = Z }.
% 124.45/124.85 parent1[0]: (1755) {G2,W4,D3,L1,V0,M1} R(1615,87) { root_occ( skol15(
% 124.45/124.85 skol16 ), skol16 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := skol15( skol16 )
% 124.45/124.85 Y := skol16
% 124.45/124.85 Z := X
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 subsumption: (9012) {G3,W7,D3,L2,V1,M2} R(270,1755) { ! root_occ( X, skol16
% 124.45/124.85 ), skol15( skol16 ) = X }.
% 124.45/124.85 parent0: (134108) {G3,W7,D3,L2,V1,M2} { ! root_occ( X, skol16 ), skol15(
% 124.45/124.85 skol16 ) = X }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 0 ==> 0
% 124.45/124.85 1 ==> 1
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 paramod: (134543) {G3,W8,D3,L2,V1,M2} { min_precedes( X, skol17( skol16 )
% 124.45/124.85 , tptp0 ), ! root_occ( X, skol16 ) }.
% 124.45/124.85 parent0[1]: (9012) {G3,W7,D3,L2,V1,M2} R(270,1755) { ! root_occ( X, skol16
% 124.45/124.85 ), skol15( skol16 ) = X }.
% 124.45/124.85 parent1[0; 1]: (1468) {G2,W6,D3,L1,V1,M1} R(1435,84) { min_precedes( skol15
% 124.45/124.85 ( X ), skol17( X ), tptp0 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 X := skol16
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 subsumption: (13816) {G4,W8,D3,L2,V1,M2} P(9012,1468) { min_precedes( X,
% 124.45/124.85 skol17( skol16 ), tptp0 ), ! root_occ( X, skol16 ) }.
% 124.45/124.85 parent0: (134543) {G3,W8,D3,L2,V1,M2} { min_precedes( X, skol17( skol16 )
% 124.45/124.85 , tptp0 ), ! root_occ( X, skol16 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 0 ==> 0
% 124.45/124.85 1 ==> 1
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 resolution: (134544) {G1,W11,D3,L3,V2,M3} { ! min_precedes( skol15( skol16
% 124.45/124.85 ), X, tptp0 ), ! alpha9( Y, X ), occurrence_of( X, tptp2 ) }.
% 124.45/124.85 parent0[0]: (1960) {G3,W8,D3,L2,V1,M2} R(103,1755);r(1754) { !
% 124.45/124.85 occurrence_of( X, tptp1 ), ! min_precedes( skol15( skol16 ), X, tptp0 )
% 124.45/124.85 }.
% 124.45/124.85 parent1[2]: (79) {G0,W9,D2,L3,V2,M3} I { ! alpha9( X, Y ), occurrence_of( Y
% 124.45/124.85 , tptp2 ), occurrence_of( Y, tptp1 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 X := Y
% 124.45/124.85 Y := X
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 resolution: (134545) {G2,W13,D3,L3,V2,M3} { ! min_precedes( skol15( skol16
% 124.45/124.85 ), X, tptp0 ), ! min_precedes( skol15( skol16 ), X, tptp0 ), ! alpha9( Y
% 124.45/124.85 , X ) }.
% 124.45/124.85 parent0[0]: (1915) {G3,W8,D3,L2,V1,M2} R(102,1755);r(1754) { !
% 124.45/124.85 occurrence_of( X, tptp2 ), ! min_precedes( skol15( skol16 ), X, tptp0 )
% 124.45/124.85 }.
% 124.45/124.85 parent1[2]: (134544) {G1,W11,D3,L3,V2,M3} { ! min_precedes( skol15( skol16
% 124.45/124.85 ), X, tptp0 ), ! alpha9( Y, X ), occurrence_of( X, tptp2 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 factor: (134546) {G2,W8,D3,L2,V2,M2} { ! min_precedes( skol15( skol16 ), X
% 124.45/124.85 , tptp0 ), ! alpha9( Y, X ) }.
% 124.45/124.85 parent0[0, 1]: (134545) {G2,W13,D3,L3,V2,M3} { ! min_precedes( skol15(
% 124.45/124.85 skol16 ), X, tptp0 ), ! min_precedes( skol15( skol16 ), X, tptp0 ), !
% 124.45/124.85 alpha9( Y, X ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 subsumption: (100949) {G4,W8,D3,L2,V2,M2} R(1960,79);r(1915) { !
% 124.45/124.85 min_precedes( skol15( skol16 ), X, tptp0 ), ! alpha9( Y, X ) }.
% 124.45/124.85 parent0: (134546) {G2,W8,D3,L2,V2,M2} { ! min_precedes( skol15( skol16 ),
% 124.45/124.85 X, tptp0 ), ! alpha9( Y, X ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 0 ==> 0
% 124.45/124.85 1 ==> 1
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 resolution: (134547) {G4,W8,D3,L2,V2,M2} { ! alpha9( Y, X ), alpha1(
% 124.45/124.85 skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.85 parent0[0]: (100949) {G4,W8,D3,L2,V2,M2} R(1960,79);r(1915) { !
% 124.45/124.85 min_precedes( skol15( skol16 ), X, tptp0 ), ! alpha9( Y, X ) }.
% 124.45/124.85 parent1[1]: (5411) {G3,W8,D2,L2,V3,M2} F(5410) { alpha1( X, Y, Z ),
% 124.45/124.85 min_precedes( X, Y, Z ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 X := skol15( skol16 )
% 124.45/124.85 Y := X
% 124.45/124.85 Z := tptp0
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 subsumption: (101335) {G5,W8,D3,L2,V2,M2} R(100949,5411) { ! alpha9( X, Y )
% 124.45/124.85 , alpha1( skol15( skol16 ), Y, tptp0 ) }.
% 124.45/124.85 parent0: (134547) {G4,W8,D3,L2,V2,M2} { ! alpha9( Y, X ), alpha1( skol15(
% 124.45/124.85 skol16 ), X, tptp0 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := Y
% 124.45/124.85 Y := X
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 0 ==> 0
% 124.45/124.85 1 ==> 1
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 resolution: (134548) {G2,W11,D3,L3,V3,M3} { ! alpha9( X, Y ), !
% 124.45/124.85 min_precedes( skol15( skol16 ), X, tptp0 ), ! alpha9( Z, Y ) }.
% 124.45/124.85 parent0[1]: (1725) {G1,W11,D2,L3,V3,M3} R(80,7) { ! alpha9( X, Y ), !
% 124.45/124.85 alpha1( Z, Y, tptp0 ), ! min_precedes( Z, X, tptp0 ) }.
% 124.45/124.85 parent1[1]: (101335) {G5,W8,D3,L2,V2,M2} R(100949,5411) { ! alpha9( X, Y )
% 124.45/124.85 , alpha1( skol15( skol16 ), Y, tptp0 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 Z := skol15( skol16 )
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 X := Z
% 124.45/124.85 Y := Y
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 subsumption: (133671) {G6,W11,D3,L3,V3,M3} R(1725,101335) { ! alpha9( X, Y
% 124.45/124.85 ), ! min_precedes( skol15( skol16 ), X, tptp0 ), ! alpha9( Z, Y ) }.
% 124.45/124.85 parent0: (134548) {G2,W11,D3,L3,V3,M3} { ! alpha9( X, Y ), ! min_precedes
% 124.45/124.85 ( skol15( skol16 ), X, tptp0 ), ! alpha9( Z, Y ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 Z := X
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 0 ==> 0
% 124.45/124.85 1 ==> 1
% 124.45/124.85 2 ==> 0
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 factor: (134550) {G6,W8,D3,L2,V2,M2} { ! alpha9( X, Y ), ! min_precedes(
% 124.45/124.85 skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.85 parent0[0, 2]: (133671) {G6,W11,D3,L3,V3,M3} R(1725,101335) { ! alpha9( X,
% 124.45/124.85 Y ), ! min_precedes( skol15( skol16 ), X, tptp0 ), ! alpha9( Z, Y ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 Z := X
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 subsumption: (133704) {G7,W8,D3,L2,V2,M2} F(133671) { ! alpha9( X, Y ), !
% 124.45/124.85 min_precedes( skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.85 parent0: (134550) {G6,W8,D3,L2,V2,M2} { ! alpha9( X, Y ), ! min_precedes(
% 124.45/124.85 skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 Y := Y
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 0 ==> 0
% 124.45/124.85 1 ==> 1
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 resolution: (134551) {G5,W8,D3,L2,V1,M2} { ! alpha9( skol17( skol16 ), X )
% 124.45/124.85 , ! root_occ( skol15( skol16 ), skol16 ) }.
% 124.45/124.85 parent0[1]: (133704) {G7,W8,D3,L2,V2,M2} F(133671) { ! alpha9( X, Y ), !
% 124.45/124.85 min_precedes( skol15( skol16 ), X, tptp0 ) }.
% 124.45/124.85 parent1[0]: (13816) {G4,W8,D3,L2,V1,M2} P(9012,1468) { min_precedes( X,
% 124.45/124.85 skol17( skol16 ), tptp0 ), ! root_occ( X, skol16 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := skol17( skol16 )
% 124.45/124.85 Y := X
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 X := skol15( skol16 )
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 resolution: (134552) {G3,W4,D3,L1,V1,M1} { ! alpha9( skol17( skol16 ), X )
% 124.45/124.85 }.
% 124.45/124.85 parent0[1]: (134551) {G5,W8,D3,L2,V1,M2} { ! alpha9( skol17( skol16 ), X )
% 124.45/124.85 , ! root_occ( skol15( skol16 ), skol16 ) }.
% 124.45/124.85 parent1[0]: (1755) {G2,W4,D3,L1,V0,M1} R(1615,87) { root_occ( skol15(
% 124.45/124.85 skol16 ), skol16 ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 subsumption: (133708) {G8,W4,D3,L1,V1,M1} R(133704,13816);r(1755) { !
% 124.45/124.85 alpha9( skol17( skol16 ), X ) }.
% 124.45/124.85 parent0: (134552) {G3,W4,D3,L1,V1,M1} { ! alpha9( skol17( skol16 ), X )
% 124.45/124.85 }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := X
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 0 ==> 0
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 resolution: (134553) {G2,W0,D0,L0,V0,M0} { }.
% 124.45/124.85 parent0[0]: (133708) {G8,W4,D3,L1,V1,M1} R(133704,13816);r(1755) { ! alpha9
% 124.45/124.85 ( skol17( skol16 ), X ) }.
% 124.45/124.85 parent1[0]: (1454) {G1,W5,D3,L1,V1,M1} R(76,101) { alpha9( skol17( X ),
% 124.45/124.85 skol18( X ) ) }.
% 124.45/124.85 substitution0:
% 124.45/124.85 X := skol18( skol16 )
% 124.45/124.85 end
% 124.45/124.85 substitution1:
% 124.45/124.85 X := skol16
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 subsumption: (133755) {G9,W0,D0,L0,V0,M0} R(133708,1454) { }.
% 124.45/124.85 parent0: (134553) {G2,W0,D0,L0,V0,M0} { }.
% 124.45/124.85 substitution0:
% 124.45/124.85 end
% 124.45/124.85 permutation0:
% 124.45/124.85 end
% 124.45/124.85
% 124.45/124.85 Proof check complete!
% 124.45/124.85
% 124.45/124.85 Memory use:
% 124.45/124.85
% 124.45/124.85 space for terms: 2027432
% 124.45/124.85 space for clauses: 5030992
% 124.45/124.85
% 124.45/124.85
% 124.45/124.85 clauses generated: 2186948
% 124.45/124.85 clauses kept: 133756
% 124.45/124.85 clauses selected: 5193
% 124.45/124.85 clauses deleted: 12724
% 124.45/124.85 clauses inuse deleted: 331
% 124.45/124.85
% 124.45/124.85 subsentry: 10423573
% 124.45/124.85 literals s-matched: 4131525
% 124.45/124.85 literals matched: 3519503
% 124.45/124.85 full subsumption: 1180962
% 124.45/124.85
% 124.45/124.85 checksum: -1505101610
% 124.45/124.85
% 124.45/124.85
% 124.45/124.85 Bliksem ended
%------------------------------------------------------------------------------