%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : PRO011+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n011.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:56 EDT 2022
% Result : Theorem 0.69s 1.17s
% Output : Refutation 0.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : PRO011+2 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n011.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 02:03:33 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.69/1.09 *** allocated 10000 integers for termspace/termends
% 0.69/1.09 *** allocated 10000 integers for clauses
% 0.69/1.09 *** allocated 10000 integers for justifications
% 0.69/1.09 Bliksem 1.12
% 0.69/1.09
% 0.69/1.09
% 0.69/1.09 Automatic Strategy Selection
% 0.69/1.09
% 0.69/1.09
% 0.69/1.09 Clauses:
% 0.69/1.09
% 0.69/1.09 { ! min_precedes( X, T, Z ), ! min_precedes( T, Y, Z ), min_precedes( X, Y
% 0.69/1.09 , Z ) }.
% 0.69/1.09 { ! earlier( X, Z ), ! earlier( Z, Y ), earlier( X, Y ) }.
% 0.69/1.09 { ! occurrence_of( Z, T ), ! root_occ( X, Z ), ! root_occ( Y, Z ), X = Y }
% 0.69/1.09 .
% 0.69/1.09 { ! occurrence_of( Z, T ), atomic( T ), ! leaf_occ( X, Z ), ! leaf_occ( Y,
% 0.69/1.09 Z ), X = Y }.
% 0.69/1.09 { ! next_subocc( X, Y, Z ), min_precedes( X, Y, Z ) }.
% 0.69/1.09 { ! next_subocc( X, Y, Z ), alpha1( X, Y, Z ) }.
% 0.69/1.09 { ! min_precedes( X, Y, Z ), ! alpha1( X, Y, Z ), next_subocc( X, Y, Z ) }
% 0.69/1.09 .
% 0.69/1.09 { ! alpha1( X, Y, Z ), ! min_precedes( X, T, Z ), ! min_precedes( T, Y, Z )
% 0.69/1.09 }.
% 0.69/1.09 { min_precedes( skol1( T, Y, Z ), Y, Z ), alpha1( X, Y, Z ) }.
% 0.69/1.09 { min_precedes( X, skol1( X, Y, Z ), Z ), alpha1( X, Y, Z ) }.
% 0.69/1.09 { ! next_subocc( X, Y, Z ), arboreal( X ) }.
% 0.69/1.09 { ! next_subocc( X, Y, Z ), arboreal( Y ) }.
% 0.69/1.09 { ! min_precedes( X, Y, Z ), precedes( X, Y ) }.
% 0.69/1.09 { ! min_precedes( Z, X, Y ), ! root( X, Y ) }.
% 0.69/1.09 { ! precedes( X, Y ), earlier( X, Y ) }.
% 0.69/1.09 { ! precedes( X, Y ), legal( Y ) }.
% 0.69/1.09 { ! earlier( X, Y ), ! legal( Y ), precedes( X, Y ) }.
% 0.69/1.09 { ! earlier( X, Y ), ! earlier( Y, X ) }.
% 0.69/1.09 { ! root_occ( X, Y ), occurrence_of( Y, skol2( Z, Y ) ) }.
% 0.69/1.09 { ! root_occ( X, Y ), alpha2( X, Y, skol2( X, Y ) ) }.
% 0.69/1.09 { ! occurrence_of( Y, Z ), ! alpha2( X, Y, Z ), root_occ( X, Y ) }.
% 0.69/1.09 { ! alpha2( X, Y, Z ), subactivity_occurrence( X, Y ) }.
% 0.69/1.09 { ! alpha2( X, Y, Z ), root( X, Z ) }.
% 0.69/1.09 { ! subactivity_occurrence( X, Y ), ! root( X, Z ), alpha2( X, Y, Z ) }.
% 0.69/1.09 { ! leaf_occ( X, Y ), occurrence_of( Y, skol3( Z, Y ) ) }.
% 0.69/1.09 { ! leaf_occ( X, Y ), alpha3( X, Y, skol3( X, Y ) ) }.
% 0.69/1.09 { ! occurrence_of( Y, Z ), ! alpha3( X, Y, Z ), leaf_occ( X, Y ) }.
% 0.69/1.09 { ! alpha3( X, Y, Z ), subactivity_occurrence( X, Y ) }.
% 0.69/1.09 { ! alpha3( X, Y, Z ), leaf( X, Z ) }.
% 0.69/1.09 { ! subactivity_occurrence( X, Y ), ! leaf( X, Z ), alpha3( X, Y, Z ) }.
% 0.69/1.09 { ! root( X, Y ), legal( X ) }.
% 0.69/1.09 { ! occurrence_of( X, Y ), ! arboreal( X ), atomic( Y ) }.
% 0.69/1.09 { ! occurrence_of( X, Y ), ! atomic( Y ), arboreal( X ) }.
% 0.69/1.09 { ! leaf( X, Y ), alpha4( X, Y ) }.
% 0.69/1.09 { ! leaf( X, Y ), ! min_precedes( X, Z, Y ) }.
% 0.69/1.09 { ! alpha4( X, Y ), min_precedes( X, skol4( X, Y ), Y ), leaf( X, Y ) }.
% 0.69/1.09 { ! alpha4( X, Y ), root( X, Y ), min_precedes( skol5( X, Y ), X, Y ) }.
% 0.69/1.09 { ! root( X, Y ), alpha4( X, Y ) }.
% 0.69/1.09 { ! min_precedes( Z, X, Y ), alpha4( X, Y ) }.
% 0.69/1.09 { ! atocc( X, Y ), subactivity( Y, skol6( Z, Y ) ) }.
% 0.69/1.09 { ! atocc( X, Y ), alpha5( X, skol6( X, Y ) ) }.
% 0.69/1.09 { ! subactivity( Y, Z ), ! alpha5( X, Z ), atocc( X, Y ) }.
% 0.69/1.09 { ! alpha5( X, Y ), atomic( Y ) }.
% 0.69/1.09 { ! alpha5( X, Y ), occurrence_of( X, Y ) }.
% 0.69/1.09 { ! atomic( Y ), ! occurrence_of( X, Y ), alpha5( X, Y ) }.
% 0.69/1.09 { ! atocc( X, Y ), ! legal( X ), root( X, Y ) }.
% 0.69/1.09 { ! legal( X ), arboreal( X ) }.
% 0.69/1.09 { ! activity_occurrence( X ), activity( skol7( Y ) ) }.
% 0.69/1.09 { ! activity_occurrence( X ), occurrence_of( X, skol7( X ) ) }.
% 0.69/1.09 { ! subactivity_occurrence( X, Y ), activity_occurrence( X ) }.
% 0.69/1.09 { ! subactivity_occurrence( X, Y ), activity_occurrence( Y ) }.
% 0.69/1.09 { ! occurrence_of( Z, Y ), ! root_occ( X, Z ), ! min_precedes( T, X, Y ) }
% 0.69/1.09 .
% 0.69/1.09 { ! occurrence_of( Z, Y ), ! leaf_occ( X, Z ), ! min_precedes( X, T, Y ) }
% 0.69/1.09 .
% 0.69/1.09 { ! occurrence_of( Z, X ), ! occurrence_of( Z, Y ), X = Y }.
% 0.69/1.09 { ! leaf( X, Y ), atomic( Y ), occurrence_of( skol8( Z, Y ), Y ) }.
% 0.69/1.09 { ! leaf( X, Y ), atomic( Y ), leaf_occ( X, skol8( X, Y ) ) }.
% 0.69/1.09 { ! min_precedes( Y, Z, X ), subactivity_occurrence( Z, skol9( T, U, Z ) )
% 0.69/1.09 }.
% 0.69/1.09 { ! min_precedes( Y, Z, X ), subactivity_occurrence( Y, skol9( T, Y, Z ) )
% 0.69/1.09 }.
% 0.69/1.09 { ! min_precedes( Y, Z, X ), occurrence_of( skol9( X, Y, Z ), X ) }.
% 0.69/1.09 { ! leaf( X, Y ), atomic( Y ), occurrence_of( skol10( Z, Y ), Y ) }.
% 0.69/1.09 { ! leaf( X, Y ), atomic( Y ), leaf_occ( X, skol10( X, Y ) ) }.
% 0.69/1.09 { ! min_precedes( Y, Z, X ), subactivity( skol11( X, T, U ), X ) }.
% 0.69/1.09 { ! min_precedes( Y, Z, X ), alpha6( X, Y, Z, skol11( X, Y, Z ) ) }.
% 0.69/1.09 { ! alpha6( X, Y, Z, T ), atocc( Z, skol12( U, W, Z, V0 ) ) }.
% 0.69/1.09 { ! alpha6( X, Y, Z, T ), subactivity( skol12( X, U, Z, W ), X ) }.
% 0.69/1.09 { ! alpha6( X, Y, Z, T ), atocc( Y, T ) }.
% 0.69/1.09 { ! subactivity( U, X ), ! atocc( Y, T ), ! atocc( Z, U ), alpha6( X, Y, Z
% 0.69/1.17 , T ) }.
% 0.69/1.17 { ! root( Y, X ), atocc( Y, skol13( Z, Y ) ) }.
% 0.69/1.17 { ! root( Y, X ), subactivity( skol13( X, Y ), X ) }.
% 0.69/1.17 { ! occurrence_of( T, X ), ! arboreal( Y ), ! arboreal( Z ), !
% 0.69/1.17 subactivity_occurrence( Y, T ), ! subactivity_occurrence( Z, T ),
% 0.69/1.17 min_precedes( Y, Z, X ), min_precedes( Z, Y, X ), Y = Z }.
% 0.69/1.17 { ! occurrence_of( Y, X ), activity( X ) }.
% 0.69/1.17 { ! occurrence_of( Y, X ), activity_occurrence( Y ) }.
% 0.69/1.17 { ! occurrence_of( Y, X ), atomic( X ), subactivity_occurrence( skol14( Z,
% 0.69/1.17 Y ), Y ) }.
% 0.69/1.17 { ! occurrence_of( Y, X ), atomic( X ), root( skol14( X, Y ), X ) }.
% 0.69/1.17 { ! activity( X ), subactivity( X, X ) }.
% 0.69/1.17 { ! occurrence_of( X, tptp0 ), alpha7( X, skol15( X ) ) }.
% 0.69/1.17 { ! occurrence_of( X, tptp0 ), alpha9( skol15( X ), skol20( X ) ) }.
% 0.69/1.17 { ! occurrence_of( X, tptp0 ), alpha11( X, skol20( X ) ) }.
% 0.69/1.17 { ! alpha11( X, Y ), alpha13( skol16( Z, T ) ) }.
% 0.69/1.17 { ! alpha11( X, Y ), next_subocc( Y, skol16( Z, Y ), tptp0 ) }.
% 0.69/1.17 { ! alpha11( X, Y ), leaf_occ( skol16( X, Y ), X ) }.
% 0.69/1.17 { ! alpha13( Z ), ! next_subocc( Y, Z, tptp0 ), ! leaf_occ( Z, X ), alpha11
% 0.69/1.17 ( X, Y ) }.
% 0.69/1.17 { ! alpha13( X ), occurrence_of( X, tptp1 ), occurrence_of( X, tptp2 ) }.
% 0.69/1.17 { ! occurrence_of( X, tptp1 ), alpha13( X ) }.
% 0.69/1.17 { ! occurrence_of( X, tptp2 ), alpha13( X ) }.
% 0.69/1.17 { ! alpha9( X, Y ), occurrence_of( Y, tptp4 ) }.
% 0.69/1.17 { ! alpha9( X, Y ), next_subocc( X, Y, tptp0 ) }.
% 0.69/1.17 { ! occurrence_of( Y, tptp4 ), ! next_subocc( X, Y, tptp0 ), alpha9( X, Y )
% 0.69/1.17 }.
% 0.69/1.17 { ! alpha7( X, Y ), occurrence_of( Y, tptp3 ) }.
% 0.69/1.17 { ! alpha7( X, Y ), root_occ( Y, X ) }.
% 0.69/1.17 { ! occurrence_of( Y, tptp3 ), ! root_occ( Y, X ), alpha7( X, Y ) }.
% 0.69/1.17 { activity( tptp0 ) }.
% 0.69/1.17 { ! atomic( tptp0 ) }.
% 0.69/1.17 { atomic( tptp4 ) }.
% 0.69/1.17 { atomic( tptp1 ) }.
% 0.69/1.17 { atomic( tptp2 ) }.
% 0.69/1.17 { atomic( tptp3 ) }.
% 0.69/1.17 { ! tptp4 = tptp3 }.
% 0.69/1.17 { ! tptp4 = tptp1 }.
% 0.69/1.17 { ! tptp4 = tptp2 }.
% 0.69/1.17 { ! tptp3 = tptp1 }.
% 0.69/1.17 { ! tptp3 = tptp2 }.
% 0.69/1.17 { ! tptp1 = tptp2 }.
% 0.69/1.17 { occurrence_of( skol17, tptp0 ) }.
% 0.69/1.17 { ! leaf_occ( X, skol17 ), alpha12( skol17, X, Y ), occurrence_of( X, tptp2
% 0.69/1.17 ) }.
% 0.69/1.17 { ! leaf_occ( X, skol17 ), alpha12( skol17, X, Y ), alpha10( skol17, Y ) }
% 0.69/1.17 .
% 0.69/1.17 { ! alpha12( X, Y, Z ), occurrence_of( Y, tptp1 ) }.
% 0.69/1.17 { ! alpha12( X, Y, Z ), alpha8( X, Z ) }.
% 0.69/1.17 { ! occurrence_of( Y, tptp1 ), ! alpha8( X, Z ), alpha12( X, Y, Z ) }.
% 0.69/1.17 { ! alpha10( X, Y ), occurrence_of( skol18( Z, T ), tptp1 ) }.
% 0.69/1.17 { ! alpha10( X, Y ), min_precedes( Y, skol18( Z, Y ), tptp0 ) }.
% 0.69/1.17 { ! alpha10( X, Y ), subactivity_occurrence( skol18( X, Y ), X ) }.
% 0.69/1.17 { ! occurrence_of( Z, tptp1 ), ! subactivity_occurrence( Z, X ), !
% 0.69/1.17 min_precedes( Y, Z, tptp0 ), alpha10( X, Y ) }.
% 0.69/1.17 { ! alpha8( X, Y ), occurrence_of( skol19( Z, T ), tptp2 ) }.
% 0.69/1.17 { ! alpha8( X, Y ), min_precedes( Y, skol19( Z, Y ), tptp0 ) }.
% 0.69/1.17 { ! alpha8( X, Y ), subactivity_occurrence( skol19( X, Y ), X ) }.
% 0.69/1.17 { ! occurrence_of( Z, tptp2 ), ! subactivity_occurrence( Z, X ), !
% 0.69/1.17 min_precedes( Y, Z, tptp0 ), alpha8( X, Y ) }.
% 0.69/1.17
% 0.69/1.17 percentage equality = 0.036900, percentage horn = 0.871795
% 0.69/1.17 This is a problem with some equality
% 0.69/1.17
% 0.69/1.17
% 0.69/1.17
% 0.69/1.17 Options Used:
% 0.69/1.17
% 0.69/1.17 useres = 1
% 0.69/1.17 useparamod = 1
% 0.69/1.17 useeqrefl = 1
% 0.69/1.17 useeqfact = 1
% 0.69/1.17 usefactor = 1
% 0.69/1.17 usesimpsplitting = 0
% 0.69/1.17 usesimpdemod = 5
% 0.69/1.17 usesimpres = 3
% 0.69/1.17
% 0.69/1.17 resimpinuse = 1000
% 0.69/1.17 resimpclauses = 20000
% 0.69/1.17 substype = eqrewr
% 0.69/1.17 backwardsubs = 1
% 0.69/1.17 selectoldest = 5
% 0.69/1.17
% 0.69/1.17 litorderings [0] = split
% 0.69/1.17 litorderings [1] = extend the termordering, first sorting on arguments
% 0.69/1.17
% 0.69/1.17 termordering = kbo
% 0.69/1.17
% 0.69/1.17 litapriori = 0
% 0.69/1.17 termapriori = 1
% 0.69/1.17 litaposteriori = 0
% 0.69/1.17 termaposteriori = 0
% 0.69/1.17 demodaposteriori = 0
% 0.69/1.17 ordereqreflfact = 0
% 0.69/1.17
% 0.69/1.17 litselect = negord
% 0.69/1.17
% 0.69/1.17 maxweight = 15
% 0.69/1.17 maxdepth = 30000
% 0.69/1.17 maxlength = 115
% 0.69/1.17 maxnrvars = 195
% 0.69/1.17 excuselevel = 1
% 0.69/1.17 increasemaxweight = 1
% 0.69/1.17
% 0.69/1.17 maxselected = 10000000
% 0.69/1.17 maxnrclauses = 10000000
% 0.69/1.17
% 0.69/1.17 showgenerated = 0
% 0.69/1.17 showkept = 0
% 0.69/1.17 showselected = 0
% 0.69/1.17 showdeleted = 0
% 0.69/1.17 showresimp = 1
% 0.69/1.17 showstatus = 2000
% 0.69/1.17
% 0.69/1.17 prologoutput = 0
% 0.69/1.17 nrgoals = 5000000
% 0.69/1.17 totalproof = 1
% 0.69/1.17
% 0.69/1.17 Symbols occurring in the translation:
% 0.69/1.17
% 0.69/1.17 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.69/1.17 . [1, 2] (w:1, o:130, a:1, s:1, b:0),
% 0.69/1.17 ! [4, 1] (w:0, o:116, a:1, s:1, b:0),
% 0.69/1.17 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.69/1.17 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.69/1.17 min_precedes [39, 3] (w:1, o:183, a:1, s:1, b:0),
% 0.69/1.17 earlier [43, 2] (w:1, o:154, a:1, s:1, b:0),
% 0.69/1.17 occurrence_of [48, 2] (w:1, o:155, a:1, s:1, b:0),
% 0.69/1.17 root_occ [49, 2] (w:1, o:156, a:1, s:1, b:0),
% 0.69/1.17 atomic [54, 1] (w:1, o:121, a:1, s:1, b:0),
% 0.69/1.17 leaf_occ [55, 2] (w:1, o:157, a:1, s:1, b:0),
% 0.69/1.17 next_subocc [59, 3] (w:1, o:184, a:1, s:1, b:0),
% 0.69/1.17 arboreal [64, 1] (w:1, o:122, a:1, s:1, b:0),
% 0.69/1.17 precedes [68, 2] (w:1, o:158, a:1, s:1, b:0),
% 0.69/1.17 root [72, 2] (w:1, o:159, a:1, s:1, b:0),
% 0.69/1.17 legal [75, 1] (w:1, o:123, a:1, s:1, b:0),
% 0.69/1.17 subactivity_occurrence [81, 2] (w:1, o:160, a:1, s:1, b:0),
% 0.69/1.17 leaf [85, 2] (w:1, o:161, a:1, s:1, b:0),
% 0.69/1.17 atocc [96, 2] (w:1, o:162, a:1, s:1, b:0),
% 0.69/1.17 subactivity [98, 2] (w:1, o:163, a:1, s:1, b:0),
% 0.69/1.17 activity_occurrence [103, 1] (w:1, o:124, a:1, s:1, b:0),
% 0.69/1.17 activity [105, 1] (w:1, o:125, a:1, s:1, b:0),
% 0.69/1.17 tptp0 [148, 0] (w:1, o:107, a:1, s:1, b:0),
% 0.69/1.17 tptp3 [152, 0] (w:1, o:112, a:1, s:1, b:0),
% 0.69/1.17 tptp4 [153, 0] (w:1, o:113, a:1, s:1, b:0),
% 0.69/1.17 tptp1 [154, 0] (w:1, o:114, a:1, s:1, b:0),
% 0.69/1.17 tptp2 [155, 0] (w:1, o:111, a:1, s:1, b:0),
% 0.69/1.17 alpha1 [161, 3] (w:1, o:185, a:1, s:1, b:1),
% 0.69/1.17 alpha2 [162, 3] (w:1, o:187, a:1, s:1, b:1),
% 0.69/1.17 alpha3 [163, 3] (w:1, o:188, a:1, s:1, b:1),
% 0.69/1.17 alpha4 [164, 2] (w:1, o:164, a:1, s:1, b:1),
% 0.69/1.17 alpha5 [165, 2] (w:1, o:165, a:1, s:1, b:1),
% 0.69/1.17 alpha6 [166, 4] (w:1, o:192, a:1, s:1, b:1),
% 0.69/1.17 alpha7 [167, 2] (w:1, o:166, a:1, s:1, b:1),
% 0.69/1.17 alpha8 [168, 2] (w:1, o:167, a:1, s:1, b:1),
% 0.69/1.17 alpha9 [169, 2] (w:1, o:168, a:1, s:1, b:1),
% 0.69/1.17 alpha10 [170, 2] (w:1, o:169, a:1, s:1, b:1),
% 0.69/1.17 alpha11 [171, 2] (w:1, o:170, a:1, s:1, b:1),
% 0.69/1.17 alpha12 [172, 3] (w:1, o:186, a:1, s:1, b:1),
% 0.69/1.17 alpha13 [173, 1] (w:1, o:126, a:1, s:1, b:1),
% 0.69/1.17 skol1 [174, 3] (w:1, o:189, a:1, s:1, b:1),
% 0.69/1.17 skol2 [175, 2] (w:1, o:177, a:1, s:1, b:1),
% 0.69/1.17 skol3 [176, 2] (w:1, o:178, a:1, s:1, b:1),
% 0.69/1.17 skol4 [177, 2] (w:1, o:179, a:1, s:1, b:1),
% 0.69/1.17 skol5 [178, 2] (w:1, o:180, a:1, s:1, b:1),
% 0.69/1.17 skol6 [179, 2] (w:1, o:181, a:1, s:1, b:1),
% 0.69/1.17 skol7 [180, 1] (w:1, o:127, a:1, s:1, b:1),
% 0.69/1.17 skol8 [181, 2] (w:1, o:182, a:1, s:1, b:1),
% 0.69/1.17 skol9 [182, 3] (w:1, o:190, a:1, s:1, b:1),
% 0.69/1.17 skol10 [183, 2] (w:1, o:171, a:1, s:1, b:1),
% 0.69/1.17 skol11 [184, 3] (w:1, o:191, a:1, s:1, b:1),
% 0.69/1.17 skol12 [185, 4] (w:1, o:193, a:1, s:1, b:1),
% 0.69/1.17 skol13 [186, 2] (w:1, o:172, a:1, s:1, b:1),
% 0.69/1.17 skol14 [187, 2] (w:1, o:173, a:1, s:1, b:1),
% 0.69/1.17 skol15 [188, 1] (w:1, o:128, a:1, s:1, b:1),
% 0.69/1.17 skol16 [189, 2] (w:1, o:174, a:1, s:1, b:1),
% 0.69/1.17 skol17 [190, 0] (w:1, o:106, a:1, s:1, b:1),
% 0.69/1.17 skol18 [191, 2] (w:1, o:175, a:1, s:1, b:1),
% 0.69/1.17 skol19 [192, 2] (w:1, o:176, a:1, s:1, b:1),
% 0.69/1.17 skol20 [193, 1] (w:1, o:129, a:1, s:1, b:1).
% 0.69/1.17
% 0.69/1.17
% 0.69/1.17 Starting Search:
% 0.69/1.17
% 0.69/1.17 *** allocated 15000 integers for clauses
% 0.69/1.17 *** allocated 22500 integers for clauses
% 0.69/1.17 *** allocated 33750 integers for clauses
% 0.69/1.17 *** allocated 15000 integers for termspace/termends
% 0.69/1.17 *** allocated 50625 integers for clauses
% 0.69/1.17 Resimplifying inuse:
% 0.69/1.17 Done
% 0.69/1.17
% 0.69/1.17 *** allocated 22500 integers for termspace/termends
% 0.69/1.17 *** allocated 75937 integers for clauses
% 0.69/1.17 *** allocated 33750 integers for termspace/termends
% 0.69/1.17 *** allocated 113905 integers for clauses
% 0.69/1.17
% 0.69/1.17 Intermediate Status:
% 0.69/1.17 Generated: 5361
% 0.69/1.17 Kept: 2002
% 0.69/1.17 Inuse: 364
% 0.69/1.17 Deleted: 14
% 0.69/1.17 Deletedinuse: 7
% 0.69/1.17
% 0.69/1.17 Resimplifying inuse:
% 0.69/1.17 Done
% 0.69/1.17
% 0.69/1.17
% 0.69/1.17 Bliksems!, er is een bewijs:
% 0.69/1.17 % SZS status Theorem
% 0.69/1.17 % SZS output start Refutation
% 0.69/1.17
% 0.69/1.17 (31) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), ! arboreal( X ),
% 0.69/1.17 atomic( Y ) }.
% 0.69/1.17 (32) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), ! atomic( Y ),
% 0.69/1.17 arboreal( X ) }.
% 0.69/1.17 (40) {G0,W8,D3,L2,V2,M2} I { ! atocc( X, Y ), alpha5( X, skol6( X, Y ) )
% 0.69/1.17 }.
% 0.69/1.17 (42) {G0,W5,D2,L2,V2,M2} I { ! alpha5( X, Y ), atomic( Y ) }.
% 0.69/1.17 (43) {G0,W6,D2,L2,V2,M2} I { ! alpha5( X, Y ), occurrence_of( X, Y ) }.
% 0.69/1.17 (62) {G0,W12,D3,L2,V3,M2} I { ! min_precedes( Y, Z, X ), alpha6( X, Y, Z,
% 0.69/1.17 skol11( X, Y, Z ) ) }.
% 0.69/1.17 (65) {G0,W8,D2,L2,V4,M2} I { ! alpha6( X, Y, Z, T ), atocc( Y, T ) }.
% 0.69/1.17 (77) {G0,W7,D3,L2,V1,M2} I { ! occurrence_of( X, tptp0 ), alpha11( X,
% 0.69/1.17 skol20( X ) ) }.
% 0.69/1.17 (80) {G0,W8,D3,L2,V2,M2} I { ! alpha11( X, Y ), leaf_occ( skol16( X, Y ), X
% 0.69/1.17 ) }.
% 0.69/1.17 (92) {G0,W2,D2,L1,V0,M1} I { ! atomic( tptp0 ) }.
% 0.69/1.17 (103) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol17, tptp0 ) }.
% 0.69/1.17 (105) {G0,W10,D2,L3,V2,M3} I { ! leaf_occ( X, skol17 ), alpha12( skol17, X
% 0.69/1.17 , Y ), alpha10( skol17, Y ) }.
% 0.69/1.17 (107) {G0,W7,D2,L2,V3,M2} I { ! alpha12( X, Y, Z ), alpha8( X, Z ) }.
% 0.69/1.17 (110) {G0,W9,D3,L2,V3,M2} I { ! alpha10( X, Y ), min_precedes( Y, skol18( Z
% 0.69/1.17 , Y ), tptp0 ) }.
% 0.69/1.17 (114) {G0,W9,D3,L2,V3,M2} I { ! alpha8( X, Y ), min_precedes( Y, skol19( Z
% 0.69/1.17 , Y ), tptp0 ) }.
% 0.69/1.17 (463) {G1,W2,D2,L1,V0,M1} R(31,103);r(92) { ! arboreal( skol17 ) }.
% 0.69/1.17 (479) {G2,W5,D2,L2,V1,M2} R(32,463) { ! occurrence_of( skol17, X ), !
% 0.69/1.17 atomic( X ) }.
% 0.69/1.17 (567) {G1,W7,D3,L2,V2,M2} R(40,42) { ! atocc( X, Y ), atomic( skol6( X, Y )
% 0.69/1.17 ) }.
% 0.69/1.17 (587) {G3,W5,D2,L2,V1,M2} R(479,43) { ! atomic( X ), ! alpha5( skol17, X )
% 0.69/1.17 }.
% 0.69/1.17 (647) {G4,W3,D2,L1,V1,M1} R(587,40);r(567) { ! atocc( skol17, X ) }.
% 0.69/1.17 (1103) {G5,W5,D2,L1,V3,M1} R(65,647) { ! alpha6( X, skol17, Y, Z ) }.
% 0.69/1.17 (1108) {G6,W4,D2,L1,V2,M1} R(1103,62) { ! min_precedes( skol17, X, Y ) }.
% 0.69/1.17 (1553) {G1,W4,D3,L1,V0,M1} R(77,103) { alpha11( skol17, skol20( skol17 ) )
% 0.69/1.17 }.
% 0.69/1.17 (1913) {G7,W3,D2,L1,V1,M1} R(110,1108) { ! alpha10( X, skol17 ) }.
% 0.69/1.17 (2041) {G7,W3,D2,L1,V1,M1} R(114,1108) { ! alpha8( X, skol17 ) }.
% 0.69/1.17 (2072) {G8,W4,D2,L1,V2,M1} R(2041,107) { ! alpha12( X, Y, skol17 ) }.
% 0.69/1.17 (2073) {G9,W3,D2,L1,V1,M1} R(2072,105);r(1913) { ! leaf_occ( X, skol17 )
% 0.69/1.17 }.
% 0.69/1.17 (2074) {G10,W3,D2,L1,V1,M1} R(2073,80) { ! alpha11( skol17, X ) }.
% 0.69/1.17 (2078) {G11,W0,D0,L0,V0,M0} R(2074,1553) { }.
% 0.69/1.17
% 0.69/1.17
% 0.69/1.17 % SZS output end Refutation
% 0.69/1.17 found a proof!
% 0.69/1.17
% 0.69/1.17
% 0.69/1.17 Unprocessed initial clauses:
% 0.69/1.17
% 0.69/1.17 (2080) {G0,W12,D2,L3,V4,M3} { ! min_precedes( X, T, Z ), ! min_precedes( T
% 0.69/1.17 , Y, Z ), min_precedes( X, Y, Z ) }.
% 0.69/1.17 (2081) {G0,W9,D2,L3,V3,M3} { ! earlier( X, Z ), ! earlier( Z, Y ), earlier
% 0.69/1.17 ( X, Y ) }.
% 0.69/1.17 (2082) {G0,W12,D2,L4,V4,M4} { ! occurrence_of( Z, T ), ! root_occ( X, Z )
% 0.69/1.17 , ! root_occ( Y, Z ), X = Y }.
% 0.69/1.17 (2083) {G0,W14,D2,L5,V4,M5} { ! occurrence_of( Z, T ), atomic( T ), !
% 0.69/1.17 leaf_occ( X, Z ), ! leaf_occ( Y, Z ), X = Y }.
% 0.69/1.17 (2084) {G0,W8,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), min_precedes( X, Y
% 0.69/1.17 , Z ) }.
% 0.69/1.17 (2085) {G0,W8,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), alpha1( X, Y, Z )
% 0.69/1.17 }.
% 0.69/1.17 (2086) {G0,W12,D2,L3,V3,M3} { ! min_precedes( X, Y, Z ), ! alpha1( X, Y, Z
% 0.69/1.17 ), next_subocc( X, Y, Z ) }.
% 0.69/1.17 (2087) {G0,W12,D2,L3,V4,M3} { ! alpha1( X, Y, Z ), ! min_precedes( X, T, Z
% 0.69/1.17 ), ! min_precedes( T, Y, Z ) }.
% 0.69/1.17 (2088) {G0,W11,D3,L2,V4,M2} { min_precedes( skol1( T, Y, Z ), Y, Z ),
% 0.69/1.17 alpha1( X, Y, Z ) }.
% 0.69/1.17 (2089) {G0,W11,D3,L2,V3,M2} { min_precedes( X, skol1( X, Y, Z ), Z ),
% 0.69/1.17 alpha1( X, Y, Z ) }.
% 0.69/1.17 (2090) {G0,W6,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), arboreal( X ) }.
% 0.69/1.17 (2091) {G0,W6,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), arboreal( Y ) }.
% 0.69/1.17 (2092) {G0,W7,D2,L2,V3,M2} { ! min_precedes( X, Y, Z ), precedes( X, Y )
% 0.69/1.17 }.
% 0.69/1.17 (2093) {G0,W7,D2,L2,V3,M2} { ! min_precedes( Z, X, Y ), ! root( X, Y ) }.
% 0.69/1.17 (2094) {G0,W6,D2,L2,V2,M2} { ! precedes( X, Y ), earlier( X, Y ) }.
% 0.69/1.17 (2095) {G0,W5,D2,L2,V2,M2} { ! precedes( X, Y ), legal( Y ) }.
% 0.69/1.17 (2096) {G0,W8,D2,L3,V2,M3} { ! earlier( X, Y ), ! legal( Y ), precedes( X
% 0.69/1.17 , Y ) }.
% 0.69/1.17 (2097) {G0,W6,D2,L2,V2,M2} { ! earlier( X, Y ), ! earlier( Y, X ) }.
% 0.69/1.17 (2098) {G0,W8,D3,L2,V3,M2} { ! root_occ( X, Y ), occurrence_of( Y, skol2(
% 0.69/1.17 Z, Y ) ) }.
% 0.69/1.17 (2099) {G0,W9,D3,L2,V2,M2} { ! root_occ( X, Y ), alpha2( X, Y, skol2( X, Y
% 0.69/1.17 ) ) }.
% 0.69/1.17 (2100) {G0,W10,D2,L3,V3,M3} { ! occurrence_of( Y, Z ), ! alpha2( X, Y, Z )
% 0.69/1.17 , root_occ( X, Y ) }.
% 0.69/1.17 (2101) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), subactivity_occurrence(
% 0.69/1.17 X, Y ) }.
% 0.69/1.17 (2102) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), root( X, Z ) }.
% 0.69/1.17 (2103) {G0,W10,D2,L3,V3,M3} { ! subactivity_occurrence( X, Y ), ! root( X
% 0.69/1.17 , Z ), alpha2( X, Y, Z ) }.
% 0.69/1.17 (2104) {G0,W8,D3,L2,V3,M2} { ! leaf_occ( X, Y ), occurrence_of( Y, skol3(
% 0.69/1.17 Z, Y ) ) }.
% 0.69/1.17 (2105) {G0,W9,D3,L2,V2,M2} { ! leaf_occ( X, Y ), alpha3( X, Y, skol3( X, Y
% 0.69/1.17 ) ) }.
% 0.69/1.17 (2106) {G0,W10,D2,L3,V3,M3} { ! occurrence_of( Y, Z ), ! alpha3( X, Y, Z )
% 0.69/1.17 , leaf_occ( X, Y ) }.
% 0.69/1.17 (2107) {G0,W7,D2,L2,V3,M2} { ! alpha3( X, Y, Z ), subactivity_occurrence(
% 0.69/1.17 X, Y ) }.
% 0.69/1.17 (2108) {G0,W7,D2,L2,V3,M2} { ! alpha3( X, Y, Z ), leaf( X, Z ) }.
% 0.69/1.17 (2109) {G0,W10,D2,L3,V3,M3} { ! subactivity_occurrence( X, Y ), ! leaf( X
% 0.69/1.17 , Z ), alpha3( X, Y, Z ) }.
% 0.69/1.17 (2110) {G0,W5,D2,L2,V2,M2} { ! root( X, Y ), legal( X ) }.
% 0.69/1.17 (2111) {G0,W7,D2,L3,V2,M3} { ! occurrence_of( X, Y ), ! arboreal( X ),
% 0.69/1.17 atomic( Y ) }.
% 0.69/1.17 (2112) {G0,W7,D2,L3,V2,M3} { ! occurrence_of( X, Y ), ! atomic( Y ),
% 0.69/1.17 arboreal( X ) }.
% 0.69/1.17 (2113) {G0,W6,D2,L2,V2,M2} { ! leaf( X, Y ), alpha4( X, Y ) }.
% 0.69/1.17 (2114) {G0,W7,D2,L2,V3,M2} { ! leaf( X, Y ), ! min_precedes( X, Z, Y ) }.
% 0.69/1.17 (2115) {G0,W12,D3,L3,V2,M3} { ! alpha4( X, Y ), min_precedes( X, skol4( X
% 0.69/1.17 , Y ), Y ), leaf( X, Y ) }.
% 0.69/1.17 (2116) {G0,W12,D3,L3,V2,M3} { ! alpha4( X, Y ), root( X, Y ), min_precedes
% 0.69/1.17 ( skol5( X, Y ), X, Y ) }.
% 0.69/1.17 (2117) {G0,W6,D2,L2,V2,M2} { ! root( X, Y ), alpha4( X, Y ) }.
% 0.69/1.17 (2118) {G0,W7,D2,L2,V3,M2} { ! min_precedes( Z, X, Y ), alpha4( X, Y ) }.
% 0.69/1.17 (2119) {G0,W8,D3,L2,V3,M2} { ! atocc( X, Y ), subactivity( Y, skol6( Z, Y
% 0.69/1.17 ) ) }.
% 0.69/1.17 (2120) {G0,W8,D3,L2,V2,M2} { ! atocc( X, Y ), alpha5( X, skol6( X, Y ) )
% 0.69/1.17 }.
% 0.69/1.17 (2121) {G0,W9,D2,L3,V3,M3} { ! subactivity( Y, Z ), ! alpha5( X, Z ),
% 0.69/1.17 atocc( X, Y ) }.
% 0.69/1.17 (2122) {G0,W5,D2,L2,V2,M2} { ! alpha5( X, Y ), atomic( Y ) }.
% 0.69/1.17 (2123) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), occurrence_of( X, Y ) }.
% 0.69/1.17 (2124) {G0,W8,D2,L3,V2,M3} { ! atomic( Y ), ! occurrence_of( X, Y ),
% 0.69/1.17 alpha5( X, Y ) }.
% 0.69/1.17 (2125) {G0,W8,D2,L3,V2,M3} { ! atocc( X, Y ), ! legal( X ), root( X, Y )
% 0.69/1.17 }.
% 0.69/1.17 (2126) {G0,W4,D2,L2,V1,M2} { ! legal( X ), arboreal( X ) }.
% 0.69/1.17 (2127) {G0,W5,D3,L2,V2,M2} { ! activity_occurrence( X ), activity( skol7(
% 0.69/1.17 Y ) ) }.
% 0.69/1.17 (2128) {G0,W6,D3,L2,V1,M2} { ! activity_occurrence( X ), occurrence_of( X
% 0.69/1.17 , skol7( X ) ) }.
% 0.69/1.17 (2129) {G0,W5,D2,L2,V2,M2} { ! subactivity_occurrence( X, Y ),
% 0.69/1.17 activity_occurrence( X ) }.
% 0.69/1.17 (2130) {G0,W5,D2,L2,V2,M2} { ! subactivity_occurrence( X, Y ),
% 0.69/1.17 activity_occurrence( Y ) }.
% 0.69/1.17 (2131) {G0,W10,D2,L3,V4,M3} { ! occurrence_of( Z, Y ), ! root_occ( X, Z )
% 0.69/1.17 , ! min_precedes( T, X, Y ) }.
% 0.69/1.17 (2132) {G0,W10,D2,L3,V4,M3} { ! occurrence_of( Z, Y ), ! leaf_occ( X, Z )
% 0.69/1.17 , ! min_precedes( X, T, Y ) }.
% 0.69/1.17 (2133) {G0,W9,D2,L3,V3,M3} { ! occurrence_of( Z, X ), ! occurrence_of( Z,
% 0.69/1.17 Y ), X = Y }.
% 0.69/1.17 (2134) {G0,W10,D3,L3,V3,M3} { ! leaf( X, Y ), atomic( Y ), occurrence_of(
% 0.69/1.17 skol8( Z, Y ), Y ) }.
% 0.69/1.17 (2135) {G0,W10,D3,L3,V2,M3} { ! leaf( X, Y ), atomic( Y ), leaf_occ( X,
% 0.69/1.17 skol8( X, Y ) ) }.
% 0.69/1.17 (2136) {G0,W10,D3,L2,V5,M2} { ! min_precedes( Y, Z, X ),
% 0.69/1.17 subactivity_occurrence( Z, skol9( T, U, Z ) ) }.
% 0.69/1.17 (2137) {G0,W10,D3,L2,V4,M2} { ! min_precedes( Y, Z, X ),
% 0.69/1.17 subactivity_occurrence( Y, skol9( T, Y, Z ) ) }.
% 0.69/1.17 (2138) {G0,W10,D3,L2,V3,M2} { ! min_precedes( Y, Z, X ), occurrence_of(
% 0.69/1.17 skol9( X, Y, Z ), X ) }.
% 0.69/1.17 (2139) {G0,W10,D3,L3,V3,M3} { ! leaf( X, Y ), atomic( Y ), occurrence_of(
% 0.69/1.17 skol10( Z, Y ), Y ) }.
% 0.69/1.17 (2140) {G0,W10,D3,L3,V2,M3} { ! leaf( X, Y ), atomic( Y ), leaf_occ( X,
% 0.69/1.17 skol10( X, Y ) ) }.
% 0.69/1.17 (2141) {G0,W10,D3,L2,V5,M2} { ! min_precedes( Y, Z, X ), subactivity(
% 0.69/1.17 skol11( X, T, U ), X ) }.
% 0.69/1.17 (2142) {G0,W12,D3,L2,V3,M2} { ! min_precedes( Y, Z, X ), alpha6( X, Y, Z,
% 0.69/1.17 skol11( X, Y, Z ) ) }.
% 0.69/1.17 (2143) {G0,W12,D3,L2,V7,M2} { ! alpha6( X, Y, Z, T ), atocc( Z, skol12( U
% 0.69/1.17 , W, Z, V0 ) ) }.
% 0.69/1.17 (2144) {G0,W12,D3,L2,V6,M2} { ! alpha6( X, Y, Z, T ), subactivity( skol12
% 0.69/1.17 ( X, U, Z, W ), X ) }.
% 0.69/1.17 (2145) {G0,W8,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), atocc( Y, T ) }.
% 0.69/1.17 (2146) {G0,W14,D2,L4,V5,M4} { ! subactivity( U, X ), ! atocc( Y, T ), !
% 0.69/1.17 atocc( Z, U ), alpha6( X, Y, Z, T ) }.
% 0.69/1.17 (2147) {G0,W8,D3,L2,V3,M2} { ! root( Y, X ), atocc( Y, skol13( Z, Y ) )
% 0.69/1.17 }.
% 0.69/1.17 (2148) {G0,W8,D3,L2,V2,M2} { ! root( Y, X ), subactivity( skol13( X, Y ),
% 0.69/1.17 X ) }.
% 0.69/1.17 (2149) {G0,W24,D2,L8,V4,M8} { ! occurrence_of( T, X ), ! arboreal( Y ), !
% 0.69/1.17 arboreal( Z ), ! subactivity_occurrence( Y, T ), ! subactivity_occurrence
% 0.69/1.17 ( Z, T ), min_precedes( Y, Z, X ), min_precedes( Z, Y, X ), Y = Z }.
% 0.69/1.17 (2150) {G0,W5,D2,L2,V2,M2} { ! occurrence_of( Y, X ), activity( X ) }.
% 0.69/1.17 (2151) {G0,W5,D2,L2,V2,M2} { ! occurrence_of( Y, X ), activity_occurrence
% 0.69/1.17 ( Y ) }.
% 0.69/1.17 (2152) {G0,W10,D3,L3,V3,M3} { ! occurrence_of( Y, X ), atomic( X ),
% 0.69/1.17 subactivity_occurrence( skol14( Z, Y ), Y ) }.
% 0.69/1.17 (2153) {G0,W10,D3,L3,V2,M3} { ! occurrence_of( Y, X ), atomic( X ), root(
% 0.69/1.17 skol14( X, Y ), X ) }.
% 0.69/1.17 (2154) {G0,W5,D2,L2,V1,M2} { ! activity( X ), subactivity( X, X ) }.
% 0.69/1.17 (2155) {G0,W7,D3,L2,V1,M2} { ! occurrence_of( X, tptp0 ), alpha7( X,
% 0.69/1.17 skol15( X ) ) }.
% 0.69/1.17 (2156) {G0,W8,D3,L2,V1,M2} { ! occurrence_of( X, tptp0 ), alpha9( skol15(
% 0.69/1.17 X ), skol20( X ) ) }.
% 0.69/1.17 (2157) {G0,W7,D3,L2,V1,M2} { ! occurrence_of( X, tptp0 ), alpha11( X,
% 0.69/1.17 skol20( X ) ) }.
% 0.69/1.17 (2158) {G0,W7,D3,L2,V4,M2} { ! alpha11( X, Y ), alpha13( skol16( Z, T ) )
% 0.69/1.17 }.
% 0.69/1.17 (2159) {G0,W9,D3,L2,V3,M2} { ! alpha11( X, Y ), next_subocc( Y, skol16( Z
% 0.69/1.17 , Y ), tptp0 ) }.
% 0.69/1.17 (2160) {G0,W8,D3,L2,V2,M2} { ! alpha11( X, Y ), leaf_occ( skol16( X, Y ),
% 0.69/1.17 X ) }.
% 0.69/1.17 (2161) {G0,W12,D2,L4,V3,M4} { ! alpha13( Z ), ! next_subocc( Y, Z, tptp0 )
% 0.69/1.17 , ! leaf_occ( Z, X ), alpha11( X, Y ) }.
% 0.69/1.17 (2162) {G0,W8,D2,L3,V1,M3} { ! alpha13( X ), occurrence_of( X, tptp1 ),
% 0.69/1.17 occurrence_of( X, tptp2 ) }.
% 0.69/1.17 (2163) {G0,W5,D2,L2,V1,M2} { ! occurrence_of( X, tptp1 ), alpha13( X ) }.
% 0.69/1.17 (2164) {G0,W5,D2,L2,V1,M2} { ! occurrence_of( X, tptp2 ), alpha13( X ) }.
% 0.69/1.17 (2165) {G0,W6,D2,L2,V2,M2} { ! alpha9( X, Y ), occurrence_of( Y, tptp4 )
% 0.69/1.17 }.
% 0.69/1.17 (2166) {G0,W7,D2,L2,V2,M2} { ! alpha9( X, Y ), next_subocc( X, Y, tptp0 )
% 0.69/1.17 }.
% 0.69/1.17 (2167) {G0,W10,D2,L3,V2,M3} { ! occurrence_of( Y, tptp4 ), ! next_subocc(
% 0.69/1.17 X, Y, tptp0 ), alpha9( X, Y ) }.
% 0.69/1.17 (2168) {G0,W6,D2,L2,V2,M2} { ! alpha7( X, Y ), occurrence_of( Y, tptp3 )
% 0.69/1.17 }.
% 0.69/1.17 (2169) {G0,W6,D2,L2,V2,M2} { ! alpha7( X, Y ), root_occ( Y, X ) }.
% 0.69/1.17 (2170) {G0,W9,D2,L3,V2,M3} { ! occurrence_of( Y, tptp3 ), ! root_occ( Y, X
% 0.69/1.17 ), alpha7( X, Y ) }.
% 0.69/1.17 (2171) {G0,W2,D2,L1,V0,M1} { activity( tptp0 ) }.
% 0.69/1.17 (2172) {G0,W2,D2,L1,V0,M1} { ! atomic( tptp0 ) }.
% 0.69/1.17 (2173) {G0,W2,D2,L1,V0,M1} { atomic( tptp4 ) }.
% 0.69/1.17 (2174) {G0,W2,D2,L1,V0,M1} { atomic( tptp1 ) }.
% 0.69/1.17 (2175) {G0,W2,D2,L1,V0,M1} { atomic( tptp2 ) }.
% 0.69/1.17 (2176) {G0,W2,D2,L1,V0,M1} { atomic( tptp3 ) }.
% 0.69/1.17 (2177) {G0,W3,D2,L1,V0,M1} { ! tptp4 = tptp3 }.
% 0.69/1.17 (2178) {G0,W3,D2,L1,V0,M1} { ! tptp4 = tptp1 }.
% 0.69/1.17 (2179) {G0,W3,D2,L1,V0,M1} { ! tptp4 = tptp2 }.
% 0.69/1.17 (2180) {G0,W3,D2,L1,V0,M1} { ! tptp3 = tptp1 }.
% 0.69/1.17 (2181) {G0,W3,D2,L1,V0,M1} { ! tptp3 = tptp2 }.
% 0.69/1.17 (2182) {G0,W3,D2,L1,V0,M1} { ! tptp1 = tptp2 }.
% 0.69/1.17 (2183) {G0,W3,D2,L1,V0,M1} { occurrence_of( skol17, tptp0 ) }.
% 0.69/1.17 (2184) {G0,W10,D2,L3,V2,M3} { ! leaf_occ( X, skol17 ), alpha12( skol17, X
% 0.69/1.17 , Y ), occurrence_of( X, tptp2 ) }.
% 0.69/1.17 (2185) {G0,W10,D2,L3,V2,M3} { ! leaf_occ( X, skol17 ), alpha12( skol17, X
% 0.69/1.17 , Y ), alpha10( skol17, Y ) }.
% 0.69/1.17 (2186) {G0,W7,D2,L2,V3,M2} { ! alpha12( X, Y, Z ), occurrence_of( Y, tptp1
% 0.69/1.17 ) }.
% 0.69/1.17 (2187) {G0,W7,D2,L2,V3,M2} { ! alpha12( X, Y, Z ), alpha8( X, Z ) }.
% 0.69/1.17 (2188) {G0,W10,D2,L3,V3,M3} { ! occurrence_of( Y, tptp1 ), ! alpha8( X, Z
% 0.69/1.17 ), alpha12( X, Y, Z ) }.
% 0.69/1.17 (2189) {G0,W8,D3,L2,V4,M2} { ! alpha10( X, Y ), occurrence_of( skol18( Z,
% 0.69/1.17 T ), tptp1 ) }.
% 0.69/1.17 (2190) {G0,W9,D3,L2,V3,M2} { ! alpha10( X, Y ), min_precedes( Y, skol18( Z
% 0.69/1.17 , Y ), tptp0 ) }.
% 0.69/1.17 (2191) {G0,W8,D3,L2,V2,M2} { ! alpha10( X, Y ), subactivity_occurrence(
% 0.69/1.17 skol18( X, Y ), X ) }.
% 0.69/1.17 (2192) {G0,W13,D2,L4,V3,M4} { ! occurrence_of( Z, tptp1 ), !
% 0.69/1.17 subactivity_occurrence( Z, X ), ! min_precedes( Y, Z, tptp0 ), alpha10( X
% 0.69/1.17 , Y ) }.
% 0.69/1.17 (2193) {G0,W8,D3,L2,V4,M2} { ! alpha8( X, Y ), occurrence_of( skol19( Z, T
% 0.69/1.17 ), tptp2 ) }.
% 0.69/1.17 (2194) {G0,W9,D3,L2,V3,M2} { ! alpha8( X, Y ), min_precedes( Y, skol19( Z
% 0.69/1.17 , Y ), tptp0 ) }.
% 0.69/1.17 (2195) {G0,W8,D3,L2,V2,M2} { ! alpha8( X, Y ), subactivity_occurrence(
% 0.69/1.17 skol19( X, Y ), X ) }.
% 0.69/1.17 (2196) {G0,W13,D2,L4,V3,M4} { ! occurrence_of( Z, tptp2 ), !
% 0.69/1.17 subactivity_occurrence( Z, X ), ! min_precedes( Y, Z, tptp0 ), alpha8( X
% 0.69/1.17 , Y ) }.
% 0.69/1.17
% 0.69/1.17
% 0.69/1.17 Total Proof:
% 0.69/1.17
% 0.69/1.17 subsumption: (31) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), !
% 0.69/1.17 arboreal( X ), atomic( Y ) }.
% 0.69/1.17 parent0: (2111) {G0,W7,D2,L3,V2,M3} { ! occurrence_of( X, Y ), ! arboreal
% 0.69/1.17 ( X ), atomic( Y ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 2 ==> 2
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (32) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), ! atomic
% 0.69/1.17 ( Y ), arboreal( X ) }.
% 0.69/1.17 parent0: (2112) {G0,W7,D2,L3,V2,M3} { ! occurrence_of( X, Y ), ! atomic( Y
% 0.69/1.17 ), arboreal( X ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 2 ==> 2
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (40) {G0,W8,D3,L2,V2,M2} I { ! atocc( X, Y ), alpha5( X, skol6
% 0.69/1.17 ( X, Y ) ) }.
% 0.69/1.17 parent0: (2120) {G0,W8,D3,L2,V2,M2} { ! atocc( X, Y ), alpha5( X, skol6( X
% 0.69/1.17 , Y ) ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (42) {G0,W5,D2,L2,V2,M2} I { ! alpha5( X, Y ), atomic( Y ) }.
% 0.69/1.17 parent0: (2122) {G0,W5,D2,L2,V2,M2} { ! alpha5( X, Y ), atomic( Y ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (43) {G0,W6,D2,L2,V2,M2} I { ! alpha5( X, Y ), occurrence_of(
% 0.69/1.17 X, Y ) }.
% 0.69/1.17 parent0: (2123) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), occurrence_of( X,
% 0.69/1.17 Y ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (62) {G0,W12,D3,L2,V3,M2} I { ! min_precedes( Y, Z, X ),
% 0.69/1.17 alpha6( X, Y, Z, skol11( X, Y, Z ) ) }.
% 0.69/1.17 parent0: (2142) {G0,W12,D3,L2,V3,M2} { ! min_precedes( Y, Z, X ), alpha6(
% 0.69/1.17 X, Y, Z, skol11( X, Y, Z ) ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 Z := Z
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (65) {G0,W8,D2,L2,V4,M2} I { ! alpha6( X, Y, Z, T ), atocc( Y
% 0.69/1.17 , T ) }.
% 0.69/1.17 parent0: (2145) {G0,W8,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), atocc( Y, T
% 0.69/1.17 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 Z := Z
% 0.69/1.17 T := T
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (77) {G0,W7,D3,L2,V1,M2} I { ! occurrence_of( X, tptp0 ),
% 0.69/1.17 alpha11( X, skol20( X ) ) }.
% 0.69/1.17 parent0: (2157) {G0,W7,D3,L2,V1,M2} { ! occurrence_of( X, tptp0 ), alpha11
% 0.69/1.17 ( X, skol20( X ) ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (80) {G0,W8,D3,L2,V2,M2} I { ! alpha11( X, Y ), leaf_occ(
% 0.69/1.17 skol16( X, Y ), X ) }.
% 0.69/1.17 parent0: (2160) {G0,W8,D3,L2,V2,M2} { ! alpha11( X, Y ), leaf_occ( skol16
% 0.69/1.17 ( X, Y ), X ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (92) {G0,W2,D2,L1,V0,M1} I { ! atomic( tptp0 ) }.
% 0.69/1.17 parent0: (2172) {G0,W2,D2,L1,V0,M1} { ! atomic( tptp0 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (103) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol17, tptp0 )
% 0.69/1.17 }.
% 0.69/1.17 parent0: (2183) {G0,W3,D2,L1,V0,M1} { occurrence_of( skol17, tptp0 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (105) {G0,W10,D2,L3,V2,M3} I { ! leaf_occ( X, skol17 ),
% 0.69/1.17 alpha12( skol17, X, Y ), alpha10( skol17, Y ) }.
% 0.69/1.17 parent0: (2185) {G0,W10,D2,L3,V2,M3} { ! leaf_occ( X, skol17 ), alpha12(
% 0.69/1.17 skol17, X, Y ), alpha10( skol17, Y ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 2 ==> 2
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (107) {G0,W7,D2,L2,V3,M2} I { ! alpha12( X, Y, Z ), alpha8( X
% 0.69/1.17 , Z ) }.
% 0.69/1.17 parent0: (2187) {G0,W7,D2,L2,V3,M2} { ! alpha12( X, Y, Z ), alpha8( X, Z )
% 0.69/1.17 }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 Z := Z
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (110) {G0,W9,D3,L2,V3,M2} I { ! alpha10( X, Y ), min_precedes
% 0.69/1.17 ( Y, skol18( Z, Y ), tptp0 ) }.
% 0.69/1.17 parent0: (2190) {G0,W9,D3,L2,V3,M2} { ! alpha10( X, Y ), min_precedes( Y,
% 0.69/1.17 skol18( Z, Y ), tptp0 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 Z := Z
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (114) {G0,W9,D3,L2,V3,M2} I { ! alpha8( X, Y ), min_precedes(
% 0.69/1.17 Y, skol19( Z, Y ), tptp0 ) }.
% 0.69/1.17 parent0: (2194) {G0,W9,D3,L2,V3,M2} { ! alpha8( X, Y ), min_precedes( Y,
% 0.69/1.17 skol19( Z, Y ), tptp0 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 Z := Z
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2383) {G1,W4,D2,L2,V0,M2} { ! arboreal( skol17 ), atomic(
% 0.69/1.17 tptp0 ) }.
% 0.69/1.17 parent0[0]: (31) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), !
% 0.69/1.17 arboreal( X ), atomic( Y ) }.
% 0.69/1.17 parent1[0]: (103) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol17, tptp0 )
% 0.69/1.17 }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := skol17
% 0.69/1.17 Y := tptp0
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2384) {G1,W2,D2,L1,V0,M1} { ! arboreal( skol17 ) }.
% 0.69/1.17 parent0[0]: (92) {G0,W2,D2,L1,V0,M1} I { ! atomic( tptp0 ) }.
% 0.69/1.17 parent1[1]: (2383) {G1,W4,D2,L2,V0,M2} { ! arboreal( skol17 ), atomic(
% 0.69/1.17 tptp0 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (463) {G1,W2,D2,L1,V0,M1} R(31,103);r(92) { ! arboreal( skol17
% 0.69/1.17 ) }.
% 0.69/1.17 parent0: (2384) {G1,W2,D2,L1,V0,M1} { ! arboreal( skol17 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2385) {G1,W5,D2,L2,V1,M2} { ! occurrence_of( skol17, X ), !
% 0.69/1.17 atomic( X ) }.
% 0.69/1.17 parent0[0]: (463) {G1,W2,D2,L1,V0,M1} R(31,103);r(92) { ! arboreal( skol17
% 0.69/1.17 ) }.
% 0.69/1.17 parent1[2]: (32) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), ! atomic
% 0.69/1.17 ( Y ), arboreal( X ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := skol17
% 0.69/1.17 Y := X
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (479) {G2,W5,D2,L2,V1,M2} R(32,463) { ! occurrence_of( skol17
% 0.69/1.17 , X ), ! atomic( X ) }.
% 0.69/1.17 parent0: (2385) {G1,W5,D2,L2,V1,M2} { ! occurrence_of( skol17, X ), !
% 0.69/1.17 atomic( X ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2386) {G1,W7,D3,L2,V2,M2} { atomic( skol6( X, Y ) ), ! atocc
% 0.69/1.17 ( X, Y ) }.
% 0.69/1.17 parent0[0]: (42) {G0,W5,D2,L2,V2,M2} I { ! alpha5( X, Y ), atomic( Y ) }.
% 0.69/1.17 parent1[1]: (40) {G0,W8,D3,L2,V2,M2} I { ! atocc( X, Y ), alpha5( X, skol6
% 0.69/1.17 ( X, Y ) ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := skol6( X, Y )
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (567) {G1,W7,D3,L2,V2,M2} R(40,42) { ! atocc( X, Y ), atomic(
% 0.69/1.17 skol6( X, Y ) ) }.
% 0.69/1.17 parent0: (2386) {G1,W7,D3,L2,V2,M2} { atomic( skol6( X, Y ) ), ! atocc( X
% 0.69/1.17 , Y ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 1
% 0.69/1.17 1 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2387) {G1,W5,D2,L2,V1,M2} { ! atomic( X ), ! alpha5( skol17,
% 0.69/1.17 X ) }.
% 0.69/1.17 parent0[0]: (479) {G2,W5,D2,L2,V1,M2} R(32,463) { ! occurrence_of( skol17,
% 0.69/1.17 X ), ! atomic( X ) }.
% 0.69/1.17 parent1[1]: (43) {G0,W6,D2,L2,V2,M2} I { ! alpha5( X, Y ), occurrence_of( X
% 0.69/1.17 , Y ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := skol17
% 0.69/1.17 Y := X
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (587) {G3,W5,D2,L2,V1,M2} R(479,43) { ! atomic( X ), ! alpha5
% 0.69/1.17 ( skol17, X ) }.
% 0.69/1.17 parent0: (2387) {G1,W5,D2,L2,V1,M2} { ! atomic( X ), ! alpha5( skol17, X )
% 0.69/1.17 }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 1 ==> 1
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2388) {G1,W7,D3,L2,V1,M2} { ! atomic( skol6( skol17, X ) ), !
% 0.69/1.17 atocc( skol17, X ) }.
% 0.69/1.17 parent0[1]: (587) {G3,W5,D2,L2,V1,M2} R(479,43) { ! atomic( X ), ! alpha5(
% 0.69/1.17 skol17, X ) }.
% 0.69/1.17 parent1[1]: (40) {G0,W8,D3,L2,V2,M2} I { ! atocc( X, Y ), alpha5( X, skol6
% 0.69/1.17 ( X, Y ) ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := skol6( skol17, X )
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := skol17
% 0.69/1.17 Y := X
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2389) {G2,W6,D2,L2,V1,M2} { ! atocc( skol17, X ), ! atocc(
% 0.69/1.17 skol17, X ) }.
% 0.69/1.17 parent0[0]: (2388) {G1,W7,D3,L2,V1,M2} { ! atomic( skol6( skol17, X ) ), !
% 0.69/1.17 atocc( skol17, X ) }.
% 0.69/1.17 parent1[1]: (567) {G1,W7,D3,L2,V2,M2} R(40,42) { ! atocc( X, Y ), atomic(
% 0.69/1.17 skol6( X, Y ) ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := skol17
% 0.69/1.17 Y := X
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 factor: (2390) {G2,W3,D2,L1,V1,M1} { ! atocc( skol17, X ) }.
% 0.69/1.17 parent0[0, 1]: (2389) {G2,W6,D2,L2,V1,M2} { ! atocc( skol17, X ), ! atocc
% 0.69/1.17 ( skol17, X ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (647) {G4,W3,D2,L1,V1,M1} R(587,40);r(567) { ! atocc( skol17,
% 0.69/1.17 X ) }.
% 0.69/1.17 parent0: (2390) {G2,W3,D2,L1,V1,M1} { ! atocc( skol17, X ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2391) {G1,W5,D2,L1,V3,M1} { ! alpha6( Y, skol17, Z, X ) }.
% 0.69/1.17 parent0[0]: (647) {G4,W3,D2,L1,V1,M1} R(587,40);r(567) { ! atocc( skol17, X
% 0.69/1.17 ) }.
% 0.69/1.17 parent1[1]: (65) {G0,W8,D2,L2,V4,M2} I { ! alpha6( X, Y, Z, T ), atocc( Y,
% 0.69/1.17 T ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := Y
% 0.69/1.17 Y := skol17
% 0.69/1.17 Z := Z
% 0.69/1.17 T := X
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (1103) {G5,W5,D2,L1,V3,M1} R(65,647) { ! alpha6( X, skol17, Y
% 0.69/1.17 , Z ) }.
% 0.69/1.17 parent0: (2391) {G1,W5,D2,L1,V3,M1} { ! alpha6( Y, skol17, Z, X ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := Z
% 0.69/1.17 Y := X
% 0.69/1.17 Z := Y
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2392) {G1,W4,D2,L1,V2,M1} { ! min_precedes( skol17, Y, X )
% 0.69/1.17 }.
% 0.69/1.17 parent0[0]: (1103) {G5,W5,D2,L1,V3,M1} R(65,647) { ! alpha6( X, skol17, Y,
% 0.69/1.17 Z ) }.
% 0.69/1.17 parent1[1]: (62) {G0,W12,D3,L2,V3,M2} I { ! min_precedes( Y, Z, X ), alpha6
% 0.69/1.17 ( X, Y, Z, skol11( X, Y, Z ) ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 Z := skol11( X, skol17, Y )
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := X
% 0.69/1.17 Y := skol17
% 0.69/1.17 Z := Y
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (1108) {G6,W4,D2,L1,V2,M1} R(1103,62) { ! min_precedes( skol17
% 0.69/1.17 , X, Y ) }.
% 0.69/1.17 parent0: (2392) {G1,W4,D2,L1,V2,M1} { ! min_precedes( skol17, Y, X ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := Y
% 0.69/1.17 Y := X
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2393) {G1,W4,D3,L1,V0,M1} { alpha11( skol17, skol20( skol17 )
% 0.69/1.17 ) }.
% 0.69/1.17 parent0[0]: (77) {G0,W7,D3,L2,V1,M2} I { ! occurrence_of( X, tptp0 ),
% 0.69/1.17 alpha11( X, skol20( X ) ) }.
% 0.69/1.17 parent1[0]: (103) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol17, tptp0 )
% 0.69/1.17 }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := skol17
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (1553) {G1,W4,D3,L1,V0,M1} R(77,103) { alpha11( skol17, skol20
% 0.69/1.17 ( skol17 ) ) }.
% 0.69/1.17 parent0: (2393) {G1,W4,D3,L1,V0,M1} { alpha11( skol17, skol20( skol17 ) )
% 0.69/1.17 }.
% 0.69/1.17 substitution0:
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2394) {G1,W3,D2,L1,V1,M1} { ! alpha10( Y, skol17 ) }.
% 0.69/1.17 parent0[0]: (1108) {G6,W4,D2,L1,V2,M1} R(1103,62) { ! min_precedes( skol17
% 0.69/1.17 , X, Y ) }.
% 0.69/1.17 parent1[1]: (110) {G0,W9,D3,L2,V3,M2} I { ! alpha10( X, Y ), min_precedes(
% 0.69/1.17 Y, skol18( Z, Y ), tptp0 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := skol18( X, skol17 )
% 0.69/1.17 Y := tptp0
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := Y
% 0.69/1.17 Y := skol17
% 0.69/1.17 Z := X
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (1913) {G7,W3,D2,L1,V1,M1} R(110,1108) { ! alpha10( X, skol17
% 0.69/1.17 ) }.
% 0.69/1.17 parent0: (2394) {G1,W3,D2,L1,V1,M1} { ! alpha10( Y, skol17 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := Y
% 0.69/1.17 Y := X
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2395) {G1,W3,D2,L1,V1,M1} { ! alpha8( Y, skol17 ) }.
% 0.69/1.17 parent0[0]: (1108) {G6,W4,D2,L1,V2,M1} R(1103,62) { ! min_precedes( skol17
% 0.69/1.17 , X, Y ) }.
% 0.69/1.17 parent1[1]: (114) {G0,W9,D3,L2,V3,M2} I { ! alpha8( X, Y ), min_precedes( Y
% 0.69/1.17 , skol19( Z, Y ), tptp0 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := skol19( X, skol17 )
% 0.69/1.17 Y := tptp0
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := Y
% 0.69/1.17 Y := skol17
% 0.69/1.17 Z := X
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (2041) {G7,W3,D2,L1,V1,M1} R(114,1108) { ! alpha8( X, skol17 )
% 0.69/1.17 }.
% 0.69/1.17 parent0: (2395) {G1,W3,D2,L1,V1,M1} { ! alpha8( Y, skol17 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := Y
% 0.69/1.17 Y := X
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2396) {G1,W4,D2,L1,V2,M1} { ! alpha12( X, Y, skol17 ) }.
% 0.69/1.17 parent0[0]: (2041) {G7,W3,D2,L1,V1,M1} R(114,1108) { ! alpha8( X, skol17 )
% 0.69/1.17 }.
% 0.69/1.17 parent1[1]: (107) {G0,W7,D2,L2,V3,M2} I { ! alpha12( X, Y, Z ), alpha8( X,
% 0.69/1.17 Z ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 Z := skol17
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (2072) {G8,W4,D2,L1,V2,M1} R(2041,107) { ! alpha12( X, Y,
% 0.69/1.17 skol17 ) }.
% 0.69/1.17 parent0: (2396) {G1,W4,D2,L1,V2,M1} { ! alpha12( X, Y, skol17 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 Y := Y
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2397) {G1,W6,D2,L2,V1,M2} { ! leaf_occ( X, skol17 ), alpha10
% 0.69/1.17 ( skol17, skol17 ) }.
% 0.69/1.17 parent0[0]: (2072) {G8,W4,D2,L1,V2,M1} R(2041,107) { ! alpha12( X, Y,
% 0.69/1.17 skol17 ) }.
% 0.69/1.17 parent1[1]: (105) {G0,W10,D2,L3,V2,M3} I { ! leaf_occ( X, skol17 ), alpha12
% 0.69/1.17 ( skol17, X, Y ), alpha10( skol17, Y ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := skol17
% 0.69/1.17 Y := X
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := X
% 0.69/1.17 Y := skol17
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2398) {G2,W3,D2,L1,V1,M1} { ! leaf_occ( X, skol17 ) }.
% 0.69/1.17 parent0[0]: (1913) {G7,W3,D2,L1,V1,M1} R(110,1108) { ! alpha10( X, skol17 )
% 0.69/1.17 }.
% 0.69/1.17 parent1[1]: (2397) {G1,W6,D2,L2,V1,M2} { ! leaf_occ( X, skol17 ), alpha10
% 0.69/1.17 ( skol17, skol17 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := skol17
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (2073) {G9,W3,D2,L1,V1,M1} R(2072,105);r(1913) { ! leaf_occ( X
% 0.69/1.17 , skol17 ) }.
% 0.69/1.17 parent0: (2398) {G2,W3,D2,L1,V1,M1} { ! leaf_occ( X, skol17 ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2399) {G1,W3,D2,L1,V1,M1} { ! alpha11( skol17, X ) }.
% 0.69/1.17 parent0[0]: (2073) {G9,W3,D2,L1,V1,M1} R(2072,105);r(1913) { ! leaf_occ( X
% 0.69/1.17 , skol17 ) }.
% 0.69/1.17 parent1[1]: (80) {G0,W8,D3,L2,V2,M2} I { ! alpha11( X, Y ), leaf_occ(
% 0.69/1.17 skol16( X, Y ), X ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := skol16( skol17, X )
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 X := skol17
% 0.69/1.17 Y := X
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (2074) {G10,W3,D2,L1,V1,M1} R(2073,80) { ! alpha11( skol17, X
% 0.69/1.17 ) }.
% 0.69/1.17 parent0: (2399) {G1,W3,D2,L1,V1,M1} { ! alpha11( skol17, X ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := X
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 0 ==> 0
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 resolution: (2400) {G2,W0,D0,L0,V0,M0} { }.
% 0.69/1.17 parent0[0]: (2074) {G10,W3,D2,L1,V1,M1} R(2073,80) { ! alpha11( skol17, X )
% 0.69/1.17 }.
% 0.69/1.17 parent1[0]: (1553) {G1,W4,D3,L1,V0,M1} R(77,103) { alpha11( skol17, skol20
% 0.69/1.17 ( skol17 ) ) }.
% 0.69/1.17 substitution0:
% 0.69/1.17 X := skol20( skol17 )
% 0.69/1.17 end
% 0.69/1.17 substitution1:
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 subsumption: (2078) {G11,W0,D0,L0,V0,M0} R(2074,1553) { }.
% 0.69/1.17 parent0: (2400) {G2,W0,D0,L0,V0,M0} { }.
% 0.69/1.17 substitution0:
% 0.69/1.17 end
% 0.69/1.17 permutation0:
% 0.69/1.17 end
% 0.69/1.17
% 0.69/1.17 Proof check complete!
% 0.69/1.17
% 0.69/1.17 Memory use:
% 0.69/1.17
% 0.69/1.17 space for terms: 29572
% 0.69/1.17 space for clauses: 94035
% 0.69/1.17
% 0.69/1.17
% 0.69/1.17 clauses generated: 5571
% 0.69/1.17 clauses kept: 2079
% 0.69/1.17 clauses selected: 378
% 0.69/1.17 clauses deleted: 29
% 0.69/1.17 clauses inuse deleted: 22
% 0.69/1.17
% 0.69/1.17 subsentry: 8129
% 0.69/1.17 literals s-matched: 5611
% 0.69/1.17 literals matched: 5540
% 0.69/1.17 full subsumption: 1583
% 0.69/1.17
% 0.69/1.17 checksum: 2130146158
% 0.69/1.17
% 0.69/1.17
% 0.69/1.17 Bliksem ended
%------------------------------------------------------------------------------