%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : PRO010+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n025.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:55 EDT 2022
% Result : Theorem 0.82s 1.21s
% Output : Refutation 0.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : PRO010+2 : TPTP v8.1.0. Released v4.0.0.
% 0.08/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n025.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % DateTime : Mon Jun 13 02:35:38 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.45/1.12 *** allocated 10000 integers for termspace/termends
% 0.45/1.12 *** allocated 10000 integers for clauses
% 0.45/1.12 *** allocated 10000 integers for justifications
% 0.45/1.12 Bliksem 1.12
% 0.45/1.12
% 0.45/1.12
% 0.45/1.12 Automatic Strategy Selection
% 0.45/1.12
% 0.45/1.12
% 0.45/1.12 Clauses:
% 0.45/1.12
% 0.45/1.12 { ! min_precedes( X, T, Z ), ! min_precedes( T, Y, Z ), min_precedes( X, Y
% 0.45/1.12 , Z ) }.
% 0.45/1.12 { ! earlier( X, Z ), ! earlier( Z, Y ), earlier( X, Y ) }.
% 0.45/1.12 { ! occurrence_of( Z, T ), ! root_occ( X, Z ), ! root_occ( Y, Z ), X = Y }
% 0.45/1.12 .
% 0.45/1.12 { ! occurrence_of( Z, T ), atomic( T ), ! leaf_occ( X, Z ), ! leaf_occ( Y,
% 0.45/1.12 Z ), X = Y }.
% 0.45/1.12 { ! next_subocc( X, Y, Z ), min_precedes( X, Y, Z ) }.
% 0.45/1.12 { ! next_subocc( X, Y, Z ), alpha1( X, Y, Z ) }.
% 0.45/1.12 { ! min_precedes( X, Y, Z ), ! alpha1( X, Y, Z ), next_subocc( X, Y, Z ) }
% 0.45/1.12 .
% 0.45/1.12 { ! alpha1( X, Y, Z ), ! min_precedes( X, T, Z ), ! min_precedes( T, Y, Z )
% 0.45/1.12 }.
% 0.45/1.12 { min_precedes( skol1( T, Y, Z ), Y, Z ), alpha1( X, Y, Z ) }.
% 0.45/1.12 { min_precedes( X, skol1( X, Y, Z ), Z ), alpha1( X, Y, Z ) }.
% 0.45/1.12 { ! next_subocc( X, Y, Z ), arboreal( X ) }.
% 0.45/1.12 { ! next_subocc( X, Y, Z ), arboreal( Y ) }.
% 0.45/1.12 { ! min_precedes( X, Y, Z ), precedes( X, Y ) }.
% 0.45/1.12 { ! min_precedes( Z, X, Y ), ! root( X, Y ) }.
% 0.45/1.12 { ! precedes( X, Y ), earlier( X, Y ) }.
% 0.45/1.12 { ! precedes( X, Y ), legal( Y ) }.
% 0.45/1.12 { ! earlier( X, Y ), ! legal( Y ), precedes( X, Y ) }.
% 0.45/1.12 { ! earlier( X, Y ), ! earlier( Y, X ) }.
% 0.45/1.12 { ! root_occ( X, Y ), occurrence_of( Y, skol2( Z, Y ) ) }.
% 0.45/1.12 { ! root_occ( X, Y ), alpha2( X, Y, skol2( X, Y ) ) }.
% 0.45/1.12 { ! occurrence_of( Y, Z ), ! alpha2( X, Y, Z ), root_occ( X, Y ) }.
% 0.45/1.12 { ! alpha2( X, Y, Z ), subactivity_occurrence( X, Y ) }.
% 0.45/1.12 { ! alpha2( X, Y, Z ), root( X, Z ) }.
% 0.45/1.12 { ! subactivity_occurrence( X, Y ), ! root( X, Z ), alpha2( X, Y, Z ) }.
% 0.45/1.12 { ! leaf_occ( X, Y ), occurrence_of( Y, skol3( Z, Y ) ) }.
% 0.45/1.12 { ! leaf_occ( X, Y ), alpha3( X, Y, skol3( X, Y ) ) }.
% 0.45/1.12 { ! occurrence_of( Y, Z ), ! alpha3( X, Y, Z ), leaf_occ( X, Y ) }.
% 0.45/1.12 { ! alpha3( X, Y, Z ), subactivity_occurrence( X, Y ) }.
% 0.45/1.12 { ! alpha3( X, Y, Z ), leaf( X, Z ) }.
% 0.45/1.12 { ! subactivity_occurrence( X, Y ), ! leaf( X, Z ), alpha3( X, Y, Z ) }.
% 0.45/1.12 { ! root( X, Y ), legal( X ) }.
% 0.45/1.12 { ! occurrence_of( X, Y ), ! arboreal( X ), atomic( Y ) }.
% 0.45/1.12 { ! occurrence_of( X, Y ), ! atomic( Y ), arboreal( X ) }.
% 0.45/1.12 { ! leaf( X, Y ), alpha4( X, Y ) }.
% 0.45/1.12 { ! leaf( X, Y ), ! min_precedes( X, Z, Y ) }.
% 0.45/1.12 { ! alpha4( X, Y ), min_precedes( X, skol4( X, Y ), Y ), leaf( X, Y ) }.
% 0.45/1.12 { ! alpha4( X, Y ), root( X, Y ), min_precedes( skol5( X, Y ), X, Y ) }.
% 0.45/1.12 { ! root( X, Y ), alpha4( X, Y ) }.
% 0.45/1.12 { ! min_precedes( Z, X, Y ), alpha4( X, Y ) }.
% 0.45/1.12 { ! atocc( X, Y ), subactivity( Y, skol6( Z, Y ) ) }.
% 0.45/1.12 { ! atocc( X, Y ), alpha5( X, skol6( X, Y ) ) }.
% 0.45/1.12 { ! subactivity( Y, Z ), ! alpha5( X, Z ), atocc( X, Y ) }.
% 0.45/1.12 { ! alpha5( X, Y ), atomic( Y ) }.
% 0.45/1.12 { ! alpha5( X, Y ), occurrence_of( X, Y ) }.
% 0.45/1.12 { ! atomic( Y ), ! occurrence_of( X, Y ), alpha5( X, Y ) }.
% 0.45/1.12 { ! atocc( X, Y ), ! legal( X ), root( X, Y ) }.
% 0.45/1.12 { ! legal( X ), arboreal( X ) }.
% 0.45/1.12 { ! activity_occurrence( X ), activity( skol7( Y ) ) }.
% 0.45/1.12 { ! activity_occurrence( X ), occurrence_of( X, skol7( X ) ) }.
% 0.45/1.12 { ! subactivity_occurrence( X, Y ), activity_occurrence( X ) }.
% 0.45/1.12 { ! subactivity_occurrence( X, Y ), activity_occurrence( Y ) }.
% 0.45/1.12 { ! occurrence_of( Z, Y ), ! root_occ( X, Z ), ! min_precedes( T, X, Y ) }
% 0.45/1.12 .
% 0.45/1.12 { ! occurrence_of( Z, Y ), ! leaf_occ( X, Z ), ! min_precedes( X, T, Y ) }
% 0.45/1.12 .
% 0.45/1.12 { ! occurrence_of( Z, X ), ! occurrence_of( Z, Y ), X = Y }.
% 0.45/1.12 { ! leaf( X, Y ), atomic( Y ), occurrence_of( skol8( Z, Y ), Y ) }.
% 0.45/1.12 { ! leaf( X, Y ), atomic( Y ), leaf_occ( X, skol8( X, Y ) ) }.
% 0.45/1.12 { ! min_precedes( Y, Z, X ), subactivity_occurrence( Z, skol9( T, U, Z ) )
% 0.45/1.12 }.
% 0.45/1.12 { ! min_precedes( Y, Z, X ), subactivity_occurrence( Y, skol9( T, Y, Z ) )
% 0.45/1.12 }.
% 0.45/1.12 { ! min_precedes( Y, Z, X ), occurrence_of( skol9( X, Y, Z ), X ) }.
% 0.45/1.12 { ! leaf( X, Y ), atomic( Y ), occurrence_of( skol10( Z, Y ), Y ) }.
% 0.45/1.12 { ! leaf( X, Y ), atomic( Y ), leaf_occ( X, skol10( X, Y ) ) }.
% 0.45/1.12 { ! min_precedes( Y, Z, X ), subactivity( skol11( X, T, U ), X ) }.
% 0.45/1.12 { ! min_precedes( Y, Z, X ), alpha6( X, Y, Z, skol11( X, Y, Z ) ) }.
% 0.45/1.12 { ! alpha6( X, Y, Z, T ), atocc( Z, skol12( U, W, Z, V0 ) ) }.
% 0.45/1.12 { ! alpha6( X, Y, Z, T ), subactivity( skol12( X, U, Z, W ), X ) }.
% 0.45/1.12 { ! alpha6( X, Y, Z, T ), atocc( Y, T ) }.
% 0.45/1.12 { ! subactivity( U, X ), ! atocc( Y, T ), ! atocc( Z, U ), alpha6( X, Y, Z
% 0.82/1.20 , T ) }.
% 0.82/1.20 { ! root( Y, X ), atocc( Y, skol13( Z, Y ) ) }.
% 0.82/1.20 { ! root( Y, X ), subactivity( skol13( X, Y ), X ) }.
% 0.82/1.20 { ! occurrence_of( T, X ), ! arboreal( Y ), ! arboreal( Z ), !
% 0.82/1.20 subactivity_occurrence( Y, T ), ! subactivity_occurrence( Z, T ),
% 0.82/1.20 min_precedes( Y, Z, X ), min_precedes( Z, Y, X ), Y = Z }.
% 0.82/1.20 { ! occurrence_of( Y, X ), activity( X ) }.
% 0.82/1.20 { ! occurrence_of( Y, X ), activity_occurrence( Y ) }.
% 0.82/1.20 { ! occurrence_of( Y, X ), atomic( X ), subactivity_occurrence( skol14( Z,
% 0.82/1.20 Y ), Y ) }.
% 0.82/1.20 { ! occurrence_of( Y, X ), atomic( X ), root( skol14( X, Y ), X ) }.
% 0.82/1.20 { ! activity( X ), subactivity( X, X ) }.
% 0.82/1.20 { ! occurrence_of( X, tptp0 ), alpha7( X, skol15( X ) ) }.
% 0.82/1.20 { ! occurrence_of( X, tptp0 ), alpha9( skol15( X ), skol20( X ) ) }.
% 0.82/1.20 { ! occurrence_of( X, tptp0 ), alpha11( X, skol20( X ) ) }.
% 0.82/1.20 { ! alpha11( X, Y ), alpha13( skol16( Z, T ) ) }.
% 0.82/1.20 { ! alpha11( X, Y ), next_subocc( Y, skol16( Z, Y ), tptp0 ) }.
% 0.82/1.20 { ! alpha11( X, Y ), leaf_occ( skol16( X, Y ), X ) }.
% 0.82/1.20 { ! alpha13( Z ), ! next_subocc( Y, Z, tptp0 ), ! leaf_occ( Z, X ), alpha11
% 0.82/1.20 ( X, Y ) }.
% 0.82/1.20 { ! alpha13( X ), occurrence_of( X, tptp1 ), occurrence_of( X, tptp2 ) }.
% 0.82/1.20 { ! occurrence_of( X, tptp1 ), alpha13( X ) }.
% 0.82/1.20 { ! occurrence_of( X, tptp2 ), alpha13( X ) }.
% 0.82/1.20 { ! alpha9( X, Y ), occurrence_of( Y, tptp4 ) }.
% 0.82/1.20 { ! alpha9( X, Y ), next_subocc( X, Y, tptp0 ) }.
% 0.82/1.20 { ! occurrence_of( Y, tptp4 ), ! next_subocc( X, Y, tptp0 ), alpha9( X, Y )
% 0.82/1.20 }.
% 0.82/1.20 { ! alpha7( X, Y ), occurrence_of( Y, tptp3 ) }.
% 0.82/1.20 { ! alpha7( X, Y ), root_occ( Y, X ) }.
% 0.82/1.20 { ! occurrence_of( Y, tptp3 ), ! root_occ( Y, X ), alpha7( X, Y ) }.
% 0.82/1.20 { activity( tptp0 ) }.
% 0.82/1.20 { ! atomic( tptp0 ) }.
% 0.82/1.20 { atomic( tptp4 ) }.
% 0.82/1.20 { atomic( tptp1 ) }.
% 0.82/1.20 { atomic( tptp2 ) }.
% 0.82/1.20 { atomic( tptp3 ) }.
% 0.82/1.20 { ! tptp4 = tptp3 }.
% 0.82/1.20 { ! tptp4 = tptp1 }.
% 0.82/1.20 { ! tptp4 = tptp2 }.
% 0.82/1.20 { ! tptp3 = tptp1 }.
% 0.82/1.20 { ! tptp3 = tptp2 }.
% 0.82/1.20 { ! tptp1 = tptp2 }.
% 0.82/1.20 { occurrence_of( skol17, tptp0 ) }.
% 0.82/1.20 { ! leaf_occ( X, skol17 ), alpha12( X, Y ), occurrence_of( X, tptp2 ) }.
% 0.82/1.20 { ! leaf_occ( X, skol17 ), alpha12( X, Y ), alpha10( Y ) }.
% 0.82/1.20 { ! alpha12( X, Y ), occurrence_of( X, tptp1 ) }.
% 0.82/1.20 { ! alpha12( X, Y ), alpha8( Y ) }.
% 0.82/1.20 { ! occurrence_of( X, tptp1 ), ! alpha8( Y ), alpha12( X, Y ) }.
% 0.82/1.20 { ! alpha10( X ), occurrence_of( skol18( Y ), tptp1 ) }.
% 0.82/1.20 { ! alpha10( X ), min_precedes( X, skol18( X ), tptp0 ) }.
% 0.82/1.20 { ! occurrence_of( Y, tptp1 ), ! min_precedes( X, Y, tptp0 ), alpha10( X )
% 0.82/1.20 }.
% 0.82/1.20 { ! alpha8( X ), occurrence_of( skol19( Y ), tptp2 ) }.
% 0.82/1.20 { ! alpha8( X ), min_precedes( X, skol19( X ), tptp0 ) }.
% 0.82/1.20 { ! occurrence_of( Y, tptp2 ), ! min_precedes( X, Y, tptp0 ), alpha8( X ) }
% 0.82/1.20 .
% 0.82/1.20
% 0.82/1.20 percentage equality = 0.037736, percentage horn = 0.869565
% 0.82/1.20 This is a problem with some equality
% 0.82/1.20
% 0.82/1.20
% 0.82/1.20
% 0.82/1.20 Options Used:
% 0.82/1.20
% 0.82/1.20 useres = 1
% 0.82/1.20 useparamod = 1
% 0.82/1.20 useeqrefl = 1
% 0.82/1.20 useeqfact = 1
% 0.82/1.20 usefactor = 1
% 0.82/1.20 usesimpsplitting = 0
% 0.82/1.20 usesimpdemod = 5
% 0.82/1.20 usesimpres = 3
% 0.82/1.20
% 0.82/1.20 resimpinuse = 1000
% 0.82/1.20 resimpclauses = 20000
% 0.82/1.20 substype = eqrewr
% 0.82/1.20 backwardsubs = 1
% 0.82/1.20 selectoldest = 5
% 0.82/1.20
% 0.82/1.20 litorderings [0] = split
% 0.82/1.20 litorderings [1] = extend the termordering, first sorting on arguments
% 0.82/1.20
% 0.82/1.20 termordering = kbo
% 0.82/1.20
% 0.82/1.20 litapriori = 0
% 0.82/1.20 termapriori = 1
% 0.82/1.20 litaposteriori = 0
% 0.82/1.20 termaposteriori = 0
% 0.82/1.20 demodaposteriori = 0
% 0.82/1.20 ordereqreflfact = 0
% 0.82/1.20
% 0.82/1.20 litselect = negord
% 0.82/1.20
% 0.82/1.20 maxweight = 15
% 0.82/1.20 maxdepth = 30000
% 0.82/1.20 maxlength = 115
% 0.82/1.20 maxnrvars = 195
% 0.82/1.20 excuselevel = 1
% 0.82/1.20 increasemaxweight = 1
% 0.82/1.20
% 0.82/1.20 maxselected = 10000000
% 0.82/1.20 maxnrclauses = 10000000
% 0.82/1.20
% 0.82/1.20 showgenerated = 0
% 0.82/1.20 showkept = 0
% 0.82/1.20 showselected = 0
% 0.82/1.20 showdeleted = 0
% 0.82/1.20 showresimp = 1
% 0.82/1.20 showstatus = 2000
% 0.82/1.20
% 0.82/1.20 prologoutput = 0
% 0.82/1.20 nrgoals = 5000000
% 0.82/1.20 totalproof = 1
% 0.82/1.20
% 0.82/1.20 Symbols occurring in the translation:
% 0.82/1.20
% 0.82/1.20 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.82/1.20 . [1, 2] (w:1, o:134, a:1, s:1, b:0),
% 0.82/1.20 ! [4, 1] (w:0, o:116, a:1, s:1, b:0),
% 0.82/1.20 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.82/1.20 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.82/1.20 min_precedes [39, 3] (w:1, o:184, a:1, s:1, b:0),
% 0.82/1.20 earlier [43, 2] (w:1, o:158, a:1, s:1, b:0),
% 0.82/1.20 occurrence_of [48, 2] (w:1, o:159, a:1, s:1, b:0),
% 0.82/1.21 root_occ [49, 2] (w:1, o:160, a:1, s:1, b:0),
% 0.82/1.21 atomic [54, 1] (w:1, o:121, a:1, s:1, b:0),
% 0.82/1.21 leaf_occ [55, 2] (w:1, o:161, a:1, s:1, b:0),
% 0.82/1.21 next_subocc [59, 3] (w:1, o:185, a:1, s:1, b:0),
% 0.82/1.21 arboreal [64, 1] (w:1, o:122, a:1, s:1, b:0),
% 0.82/1.21 precedes [68, 2] (w:1, o:162, a:1, s:1, b:0),
% 0.82/1.21 root [72, 2] (w:1, o:163, a:1, s:1, b:0),
% 0.82/1.21 legal [75, 1] (w:1, o:123, a:1, s:1, b:0),
% 0.82/1.21 subactivity_occurrence [81, 2] (w:1, o:164, a:1, s:1, b:0),
% 0.82/1.21 leaf [85, 2] (w:1, o:165, a:1, s:1, b:0),
% 0.82/1.21 atocc [96, 2] (w:1, o:166, a:1, s:1, b:0),
% 0.82/1.21 subactivity [98, 2] (w:1, o:167, a:1, s:1, b:0),
% 0.82/1.21 activity_occurrence [103, 1] (w:1, o:124, a:1, s:1, b:0),
% 0.82/1.21 activity [105, 1] (w:1, o:125, a:1, s:1, b:0),
% 0.82/1.21 tptp0 [148, 0] (w:1, o:107, a:1, s:1, b:0),
% 0.82/1.21 tptp3 [152, 0] (w:1, o:112, a:1, s:1, b:0),
% 0.82/1.21 tptp4 [153, 0] (w:1, o:113, a:1, s:1, b:0),
% 0.82/1.21 tptp1 [154, 0] (w:1, o:114, a:1, s:1, b:0),
% 0.82/1.21 tptp2 [155, 0] (w:1, o:111, a:1, s:1, b:0),
% 0.82/1.21 alpha1 [161, 3] (w:1, o:186, a:1, s:1, b:1),
% 0.82/1.21 alpha2 [162, 3] (w:1, o:187, a:1, s:1, b:1),
% 0.82/1.21 alpha3 [163, 3] (w:1, o:188, a:1, s:1, b:1),
% 0.82/1.21 alpha4 [164, 2] (w:1, o:168, a:1, s:1, b:1),
% 0.82/1.21 alpha5 [165, 2] (w:1, o:169, a:1, s:1, b:1),
% 0.82/1.21 alpha6 [166, 4] (w:1, o:192, a:1, s:1, b:1),
% 0.82/1.21 alpha7 [167, 2] (w:1, o:170, a:1, s:1, b:1),
% 0.82/1.21 alpha8 [168, 1] (w:1, o:126, a:1, s:1, b:1),
% 0.82/1.21 alpha9 [169, 2] (w:1, o:171, a:1, s:1, b:1),
% 0.82/1.21 alpha10 [170, 1] (w:1, o:127, a:1, s:1, b:1),
% 0.82/1.21 alpha11 [171, 2] (w:1, o:172, a:1, s:1, b:1),
% 0.82/1.21 alpha12 [172, 2] (w:1, o:173, a:1, s:1, b:1),
% 0.82/1.21 alpha13 [173, 1] (w:1, o:128, a:1, s:1, b:1),
% 0.82/1.21 skol1 [174, 3] (w:1, o:189, a:1, s:1, b:1),
% 0.82/1.21 skol2 [175, 2] (w:1, o:178, a:1, s:1, b:1),
% 0.82/1.21 skol3 [176, 2] (w:1, o:179, a:1, s:1, b:1),
% 0.82/1.21 skol4 [177, 2] (w:1, o:180, a:1, s:1, b:1),
% 0.82/1.21 skol5 [178, 2] (w:1, o:181, a:1, s:1, b:1),
% 0.82/1.21 skol6 [179, 2] (w:1, o:182, a:1, s:1, b:1),
% 0.82/1.21 skol7 [180, 1] (w:1, o:129, a:1, s:1, b:1),
% 0.82/1.21 skol8 [181, 2] (w:1, o:183, a:1, s:1, b:1),
% 0.82/1.21 skol9 [182, 3] (w:1, o:190, a:1, s:1, b:1),
% 0.82/1.21 skol10 [183, 2] (w:1, o:174, a:1, s:1, b:1),
% 0.82/1.21 skol11 [184, 3] (w:1, o:191, a:1, s:1, b:1),
% 0.82/1.21 skol12 [185, 4] (w:1, o:193, a:1, s:1, b:1),
% 0.82/1.21 skol13 [186, 2] (w:1, o:175, a:1, s:1, b:1),
% 0.82/1.21 skol14 [187, 2] (w:1, o:176, a:1, s:1, b:1),
% 0.82/1.21 skol15 [188, 1] (w:1, o:130, a:1, s:1, b:1),
% 0.82/1.21 skol16 [189, 2] (w:1, o:177, a:1, s:1, b:1),
% 0.82/1.21 skol17 [190, 0] (w:1, o:106, a:1, s:1, b:1),
% 0.82/1.21 skol18 [191, 1] (w:1, o:131, a:1, s:1, b:1),
% 0.82/1.21 skol19 [192, 1] (w:1, o:132, a:1, s:1, b:1),
% 0.82/1.21 skol20 [193, 1] (w:1, o:133, a:1, s:1, b:1).
% 0.82/1.21
% 0.82/1.21
% 0.82/1.21 Starting Search:
% 0.82/1.21
% 0.82/1.21 *** allocated 15000 integers for clauses
% 0.82/1.21 *** allocated 22500 integers for clauses
% 0.82/1.21 *** allocated 33750 integers for clauses
% 0.82/1.21 *** allocated 15000 integers for termspace/termends
% 0.82/1.21 *** allocated 50625 integers for clauses
% 0.82/1.21 Resimplifying inuse:
% 0.82/1.21 Done
% 0.82/1.21
% 0.82/1.21 *** allocated 22500 integers for termspace/termends
% 0.82/1.21 *** allocated 75937 integers for clauses
% 0.82/1.21 *** allocated 33750 integers for termspace/termends
% 0.82/1.21 *** allocated 113905 integers for clauses
% 0.82/1.21
% 0.82/1.21 Intermediate Status:
% 0.82/1.21 Generated: 5488
% 0.82/1.21 Kept: 2004
% 0.82/1.21 Inuse: 370
% 0.82/1.21 Deleted: 13
% 0.82/1.21 Deletedinuse: 7
% 0.82/1.21
% 0.82/1.21 Resimplifying inuse:
% 0.82/1.21 Done
% 0.82/1.21
% 0.82/1.21
% 0.82/1.21 Bliksems!, er is een bewijs:
% 0.82/1.21 % SZS status Theorem
% 0.82/1.21 % SZS output start Refutation
% 0.82/1.21
% 0.82/1.21 (31) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), ! arboreal( X ),
% 0.82/1.21 atomic( Y ) }.
% 0.82/1.21 (32) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), ! atomic( Y ),
% 0.82/1.21 arboreal( X ) }.
% 0.82/1.21 (40) {G0,W8,D3,L2,V2,M2} I { ! atocc( X, Y ), alpha5( X, skol6( X, Y ) )
% 0.82/1.21 }.
% 0.82/1.21 (42) {G0,W5,D2,L2,V2,M2} I { ! alpha5( X, Y ), atomic( Y ) }.
% 0.82/1.21 (43) {G0,W6,D2,L2,V2,M2} I { ! alpha5( X, Y ), occurrence_of( X, Y ) }.
% 0.82/1.21 (62) {G0,W12,D3,L2,V3,M2} I { ! min_precedes( Y, Z, X ), alpha6( X, Y, Z,
% 0.82/1.21 skol11( X, Y, Z ) ) }.
% 0.82/1.21 (65) {G0,W8,D2,L2,V4,M2} I { ! alpha6( X, Y, Z, T ), atocc( Y, T ) }.
% 0.82/1.21 (77) {G0,W7,D3,L2,V1,M2} I { ! occurrence_of( X, tptp0 ), alpha11( X,
% 0.82/1.21 skol20( X ) ) }.
% 0.82/1.21 (80) {G0,W8,D3,L2,V2,M2} I { ! alpha11( X, Y ), leaf_occ( skol16( X, Y ), X
% 0.82/1.21 ) }.
% 0.82/1.21 (92) {G0,W2,D2,L1,V0,M1} I { ! atomic( tptp0 ) }.
% 0.82/1.21 (103) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol17, tptp0 ) }.
% 0.82/1.21 (105) {G0,W8,D2,L3,V2,M3} I { ! leaf_occ( X, skol17 ), alpha12( X, Y ),
% 0.82/1.21 alpha10( Y ) }.
% 0.82/1.21 (107) {G0,W5,D2,L2,V2,M2} I { ! alpha12( X, Y ), alpha8( Y ) }.
% 0.82/1.21 (110) {G0,W7,D3,L2,V1,M2} I { ! alpha10( X ), min_precedes( X, skol18( X )
% 0.82/1.21 , tptp0 ) }.
% 0.82/1.21 (113) {G0,W7,D3,L2,V1,M2} I { ! alpha8( X ), min_precedes( X, skol19( X ),
% 0.82/1.21 tptp0 ) }.
% 0.82/1.21 (468) {G1,W2,D2,L1,V0,M1} R(31,103);r(92) { ! arboreal( skol17 ) }.
% 0.82/1.21 (483) {G2,W5,D2,L2,V1,M2} R(32,468) { ! occurrence_of( skol17, X ), !
% 0.82/1.21 atomic( X ) }.
% 0.82/1.21 (582) {G3,W5,D2,L2,V1,M2} R(483,43) { ! atomic( X ), ! alpha5( skol17, X )
% 0.82/1.21 }.
% 0.82/1.21 (598) {G1,W7,D3,L2,V2,M2} R(40,42) { ! atocc( X, Y ), atomic( skol6( X, Y )
% 0.82/1.21 ) }.
% 0.82/1.21 (626) {G4,W3,D2,L1,V1,M1} R(582,40);r(598) { ! atocc( skol17, X ) }.
% 0.82/1.21 (1233) {G5,W5,D2,L1,V3,M1} R(65,626) { ! alpha6( X, skol17, Y, Z ) }.
% 0.82/1.21 (1237) {G6,W4,D2,L1,V2,M1} R(1233,62) { ! min_precedes( skol17, X, Y ) }.
% 0.82/1.21 (1588) {G1,W4,D3,L1,V0,M1} R(77,103) { alpha11( skol17, skol20( skol17 ) )
% 0.82/1.21 }.
% 0.82/1.21 (1943) {G7,W2,D2,L1,V0,M1} R(110,1237) { ! alpha10( skol17 ) }.
% 0.82/1.21 (2018) {G7,W2,D2,L1,V0,M1} R(113,1237) { ! alpha8( skol17 ) }.
% 0.82/1.21 (2049) {G8,W3,D2,L1,V1,M1} R(2018,107) { ! alpha12( X, skol17 ) }.
% 0.82/1.21 (2050) {G9,W3,D2,L1,V1,M1} R(2049,105);r(1943) { ! leaf_occ( X, skol17 )
% 0.82/1.21 }.
% 0.82/1.21 (2051) {G10,W3,D2,L1,V1,M1} R(2050,80) { ! alpha11( skol17, X ) }.
% 0.82/1.21 (2055) {G11,W0,D0,L0,V0,M0} R(2051,1588) { }.
% 0.82/1.21
% 0.82/1.21
% 0.82/1.21 % SZS output end Refutation
% 0.82/1.21 found a proof!
% 0.82/1.21
% 0.82/1.21
% 0.82/1.21 Unprocessed initial clauses:
% 0.82/1.21
% 0.82/1.21 (2057) {G0,W12,D2,L3,V4,M3} { ! min_precedes( X, T, Z ), ! min_precedes( T
% 0.82/1.21 , Y, Z ), min_precedes( X, Y, Z ) }.
% 0.82/1.21 (2058) {G0,W9,D2,L3,V3,M3} { ! earlier( X, Z ), ! earlier( Z, Y ), earlier
% 0.82/1.21 ( X, Y ) }.
% 0.82/1.21 (2059) {G0,W12,D2,L4,V4,M4} { ! occurrence_of( Z, T ), ! root_occ( X, Z )
% 0.82/1.21 , ! root_occ( Y, Z ), X = Y }.
% 0.82/1.21 (2060) {G0,W14,D2,L5,V4,M5} { ! occurrence_of( Z, T ), atomic( T ), !
% 0.82/1.21 leaf_occ( X, Z ), ! leaf_occ( Y, Z ), X = Y }.
% 0.82/1.21 (2061) {G0,W8,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), min_precedes( X, Y
% 0.82/1.21 , Z ) }.
% 0.82/1.21 (2062) {G0,W8,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), alpha1( X, Y, Z )
% 0.82/1.21 }.
% 0.82/1.21 (2063) {G0,W12,D2,L3,V3,M3} { ! min_precedes( X, Y, Z ), ! alpha1( X, Y, Z
% 0.82/1.21 ), next_subocc( X, Y, Z ) }.
% 0.82/1.21 (2064) {G0,W12,D2,L3,V4,M3} { ! alpha1( X, Y, Z ), ! min_precedes( X, T, Z
% 0.82/1.21 ), ! min_precedes( T, Y, Z ) }.
% 0.82/1.21 (2065) {G0,W11,D3,L2,V4,M2} { min_precedes( skol1( T, Y, Z ), Y, Z ),
% 0.82/1.21 alpha1( X, Y, Z ) }.
% 0.82/1.21 (2066) {G0,W11,D3,L2,V3,M2} { min_precedes( X, skol1( X, Y, Z ), Z ),
% 0.82/1.21 alpha1( X, Y, Z ) }.
% 0.82/1.21 (2067) {G0,W6,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), arboreal( X ) }.
% 0.82/1.21 (2068) {G0,W6,D2,L2,V3,M2} { ! next_subocc( X, Y, Z ), arboreal( Y ) }.
% 0.82/1.21 (2069) {G0,W7,D2,L2,V3,M2} { ! min_precedes( X, Y, Z ), precedes( X, Y )
% 0.82/1.21 }.
% 0.82/1.21 (2070) {G0,W7,D2,L2,V3,M2} { ! min_precedes( Z, X, Y ), ! root( X, Y ) }.
% 0.82/1.21 (2071) {G0,W6,D2,L2,V2,M2} { ! precedes( X, Y ), earlier( X, Y ) }.
% 0.82/1.21 (2072) {G0,W5,D2,L2,V2,M2} { ! precedes( X, Y ), legal( Y ) }.
% 0.82/1.21 (2073) {G0,W8,D2,L3,V2,M3} { ! earlier( X, Y ), ! legal( Y ), precedes( X
% 0.82/1.21 , Y ) }.
% 0.82/1.21 (2074) {G0,W6,D2,L2,V2,M2} { ! earlier( X, Y ), ! earlier( Y, X ) }.
% 0.82/1.21 (2075) {G0,W8,D3,L2,V3,M2} { ! root_occ( X, Y ), occurrence_of( Y, skol2(
% 0.82/1.21 Z, Y ) ) }.
% 0.82/1.21 (2076) {G0,W9,D3,L2,V2,M2} { ! root_occ( X, Y ), alpha2( X, Y, skol2( X, Y
% 0.82/1.21 ) ) }.
% 0.82/1.21 (2077) {G0,W10,D2,L3,V3,M3} { ! occurrence_of( Y, Z ), ! alpha2( X, Y, Z )
% 0.82/1.21 , root_occ( X, Y ) }.
% 0.82/1.21 (2078) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), subactivity_occurrence(
% 0.82/1.21 X, Y ) }.
% 0.82/1.21 (2079) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), root( X, Z ) }.
% 0.82/1.21 (2080) {G0,W10,D2,L3,V3,M3} { ! subactivity_occurrence( X, Y ), ! root( X
% 0.82/1.21 , Z ), alpha2( X, Y, Z ) }.
% 0.82/1.21 (2081) {G0,W8,D3,L2,V3,M2} { ! leaf_occ( X, Y ), occurrence_of( Y, skol3(
% 0.82/1.21 Z, Y ) ) }.
% 0.82/1.21 (2082) {G0,W9,D3,L2,V2,M2} { ! leaf_occ( X, Y ), alpha3( X, Y, skol3( X, Y
% 0.82/1.21 ) ) }.
% 0.82/1.21 (2083) {G0,W10,D2,L3,V3,M3} { ! occurrence_of( Y, Z ), ! alpha3( X, Y, Z )
% 0.82/1.21 , leaf_occ( X, Y ) }.
% 0.82/1.21 (2084) {G0,W7,D2,L2,V3,M2} { ! alpha3( X, Y, Z ), subactivity_occurrence(
% 0.82/1.21 X, Y ) }.
% 0.82/1.21 (2085) {G0,W7,D2,L2,V3,M2} { ! alpha3( X, Y, Z ), leaf( X, Z ) }.
% 0.82/1.21 (2086) {G0,W10,D2,L3,V3,M3} { ! subactivity_occurrence( X, Y ), ! leaf( X
% 0.82/1.21 , Z ), alpha3( X, Y, Z ) }.
% 0.82/1.21 (2087) {G0,W5,D2,L2,V2,M2} { ! root( X, Y ), legal( X ) }.
% 0.82/1.21 (2088) {G0,W7,D2,L3,V2,M3} { ! occurrence_of( X, Y ), ! arboreal( X ),
% 0.82/1.21 atomic( Y ) }.
% 0.82/1.21 (2089) {G0,W7,D2,L3,V2,M3} { ! occurrence_of( X, Y ), ! atomic( Y ),
% 0.82/1.21 arboreal( X ) }.
% 0.82/1.21 (2090) {G0,W6,D2,L2,V2,M2} { ! leaf( X, Y ), alpha4( X, Y ) }.
% 0.82/1.21 (2091) {G0,W7,D2,L2,V3,M2} { ! leaf( X, Y ), ! min_precedes( X, Z, Y ) }.
% 0.82/1.21 (2092) {G0,W12,D3,L3,V2,M3} { ! alpha4( X, Y ), min_precedes( X, skol4( X
% 0.82/1.21 , Y ), Y ), leaf( X, Y ) }.
% 0.82/1.21 (2093) {G0,W12,D3,L3,V2,M3} { ! alpha4( X, Y ), root( X, Y ), min_precedes
% 0.82/1.21 ( skol5( X, Y ), X, Y ) }.
% 0.82/1.21 (2094) {G0,W6,D2,L2,V2,M2} { ! root( X, Y ), alpha4( X, Y ) }.
% 0.82/1.21 (2095) {G0,W7,D2,L2,V3,M2} { ! min_precedes( Z, X, Y ), alpha4( X, Y ) }.
% 0.82/1.21 (2096) {G0,W8,D3,L2,V3,M2} { ! atocc( X, Y ), subactivity( Y, skol6( Z, Y
% 0.82/1.21 ) ) }.
% 0.82/1.21 (2097) {G0,W8,D3,L2,V2,M2} { ! atocc( X, Y ), alpha5( X, skol6( X, Y ) )
% 0.82/1.21 }.
% 0.82/1.21 (2098) {G0,W9,D2,L3,V3,M3} { ! subactivity( Y, Z ), ! alpha5( X, Z ),
% 0.82/1.21 atocc( X, Y ) }.
% 0.82/1.21 (2099) {G0,W5,D2,L2,V2,M2} { ! alpha5( X, Y ), atomic( Y ) }.
% 0.82/1.21 (2100) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), occurrence_of( X, Y ) }.
% 0.82/1.21 (2101) {G0,W8,D2,L3,V2,M3} { ! atomic( Y ), ! occurrence_of( X, Y ),
% 0.82/1.21 alpha5( X, Y ) }.
% 0.82/1.21 (2102) {G0,W8,D2,L3,V2,M3} { ! atocc( X, Y ), ! legal( X ), root( X, Y )
% 0.82/1.21 }.
% 0.82/1.21 (2103) {G0,W4,D2,L2,V1,M2} { ! legal( X ), arboreal( X ) }.
% 0.82/1.21 (2104) {G0,W5,D3,L2,V2,M2} { ! activity_occurrence( X ), activity( skol7(
% 0.82/1.21 Y ) ) }.
% 0.82/1.21 (2105) {G0,W6,D3,L2,V1,M2} { ! activity_occurrence( X ), occurrence_of( X
% 0.82/1.21 , skol7( X ) ) }.
% 0.82/1.21 (2106) {G0,W5,D2,L2,V2,M2} { ! subactivity_occurrence( X, Y ),
% 0.82/1.21 activity_occurrence( X ) }.
% 0.82/1.21 (2107) {G0,W5,D2,L2,V2,M2} { ! subactivity_occurrence( X, Y ),
% 0.82/1.21 activity_occurrence( Y ) }.
% 0.82/1.21 (2108) {G0,W10,D2,L3,V4,M3} { ! occurrence_of( Z, Y ), ! root_occ( X, Z )
% 0.82/1.21 , ! min_precedes( T, X, Y ) }.
% 0.82/1.21 (2109) {G0,W10,D2,L3,V4,M3} { ! occurrence_of( Z, Y ), ! leaf_occ( X, Z )
% 0.82/1.21 , ! min_precedes( X, T, Y ) }.
% 0.82/1.21 (2110) {G0,W9,D2,L3,V3,M3} { ! occurrence_of( Z, X ), ! occurrence_of( Z,
% 0.82/1.21 Y ), X = Y }.
% 0.82/1.21 (2111) {G0,W10,D3,L3,V3,M3} { ! leaf( X, Y ), atomic( Y ), occurrence_of(
% 0.82/1.21 skol8( Z, Y ), Y ) }.
% 0.82/1.21 (2112) {G0,W10,D3,L3,V2,M3} { ! leaf( X, Y ), atomic( Y ), leaf_occ( X,
% 0.82/1.21 skol8( X, Y ) ) }.
% 0.82/1.21 (2113) {G0,W10,D3,L2,V5,M2} { ! min_precedes( Y, Z, X ),
% 0.82/1.21 subactivity_occurrence( Z, skol9( T, U, Z ) ) }.
% 0.82/1.21 (2114) {G0,W10,D3,L2,V4,M2} { ! min_precedes( Y, Z, X ),
% 0.82/1.21 subactivity_occurrence( Y, skol9( T, Y, Z ) ) }.
% 0.82/1.21 (2115) {G0,W10,D3,L2,V3,M2} { ! min_precedes( Y, Z, X ), occurrence_of(
% 0.82/1.21 skol9( X, Y, Z ), X ) }.
% 0.82/1.21 (2116) {G0,W10,D3,L3,V3,M3} { ! leaf( X, Y ), atomic( Y ), occurrence_of(
% 0.82/1.21 skol10( Z, Y ), Y ) }.
% 0.82/1.21 (2117) {G0,W10,D3,L3,V2,M3} { ! leaf( X, Y ), atomic( Y ), leaf_occ( X,
% 0.82/1.21 skol10( X, Y ) ) }.
% 0.82/1.21 (2118) {G0,W10,D3,L2,V5,M2} { ! min_precedes( Y, Z, X ), subactivity(
% 0.82/1.21 skol11( X, T, U ), X ) }.
% 0.82/1.21 (2119) {G0,W12,D3,L2,V3,M2} { ! min_precedes( Y, Z, X ), alpha6( X, Y, Z,
% 0.82/1.21 skol11( X, Y, Z ) ) }.
% 0.82/1.21 (2120) {G0,W12,D3,L2,V7,M2} { ! alpha6( X, Y, Z, T ), atocc( Z, skol12( U
% 0.82/1.21 , W, Z, V0 ) ) }.
% 0.82/1.21 (2121) {G0,W12,D3,L2,V6,M2} { ! alpha6( X, Y, Z, T ), subactivity( skol12
% 0.82/1.21 ( X, U, Z, W ), X ) }.
% 0.82/1.21 (2122) {G0,W8,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), atocc( Y, T ) }.
% 0.82/1.21 (2123) {G0,W14,D2,L4,V5,M4} { ! subactivity( U, X ), ! atocc( Y, T ), !
% 0.82/1.21 atocc( Z, U ), alpha6( X, Y, Z, T ) }.
% 0.82/1.21 (2124) {G0,W8,D3,L2,V3,M2} { ! root( Y, X ), atocc( Y, skol13( Z, Y ) )
% 0.82/1.21 }.
% 0.82/1.21 (2125) {G0,W8,D3,L2,V2,M2} { ! root( Y, X ), subactivity( skol13( X, Y ),
% 0.82/1.21 X ) }.
% 0.82/1.21 (2126) {G0,W24,D2,L8,V4,M8} { ! occurrence_of( T, X ), ! arboreal( Y ), !
% 0.82/1.21 arboreal( Z ), ! subactivity_occurrence( Y, T ), ! subactivity_occurrence
% 0.82/1.21 ( Z, T ), min_precedes( Y, Z, X ), min_precedes( Z, Y, X ), Y = Z }.
% 0.82/1.21 (2127) {G0,W5,D2,L2,V2,M2} { ! occurrence_of( Y, X ), activity( X ) }.
% 0.82/1.21 (2128) {G0,W5,D2,L2,V2,M2} { ! occurrence_of( Y, X ), activity_occurrence
% 0.82/1.21 ( Y ) }.
% 0.82/1.21 (2129) {G0,W10,D3,L3,V3,M3} { ! occurrence_of( Y, X ), atomic( X ),
% 0.82/1.21 subactivity_occurrence( skol14( Z, Y ), Y ) }.
% 0.82/1.21 (2130) {G0,W10,D3,L3,V2,M3} { ! occurrence_of( Y, X ), atomic( X ), root(
% 0.82/1.21 skol14( X, Y ), X ) }.
% 0.82/1.21 (2131) {G0,W5,D2,L2,V1,M2} { ! activity( X ), subactivity( X, X ) }.
% 0.82/1.21 (2132) {G0,W7,D3,L2,V1,M2} { ! occurrence_of( X, tptp0 ), alpha7( X,
% 0.82/1.21 skol15( X ) ) }.
% 0.82/1.21 (2133) {G0,W8,D3,L2,V1,M2} { ! occurrence_of( X, tptp0 ), alpha9( skol15(
% 0.82/1.21 X ), skol20( X ) ) }.
% 0.82/1.21 (2134) {G0,W7,D3,L2,V1,M2} { ! occurrence_of( X, tptp0 ), alpha11( X,
% 0.82/1.21 skol20( X ) ) }.
% 0.82/1.21 (2135) {G0,W7,D3,L2,V4,M2} { ! alpha11( X, Y ), alpha13( skol16( Z, T ) )
% 0.82/1.21 }.
% 0.82/1.21 (2136) {G0,W9,D3,L2,V3,M2} { ! alpha11( X, Y ), next_subocc( Y, skol16( Z
% 0.82/1.21 , Y ), tptp0 ) }.
% 0.82/1.21 (2137) {G0,W8,D3,L2,V2,M2} { ! alpha11( X, Y ), leaf_occ( skol16( X, Y ),
% 0.82/1.21 X ) }.
% 0.82/1.21 (2138) {G0,W12,D2,L4,V3,M4} { ! alpha13( Z ), ! next_subocc( Y, Z, tptp0 )
% 0.82/1.21 , ! leaf_occ( Z, X ), alpha11( X, Y ) }.
% 0.82/1.21 (2139) {G0,W8,D2,L3,V1,M3} { ! alpha13( X ), occurrence_of( X, tptp1 ),
% 0.82/1.21 occurrence_of( X, tptp2 ) }.
% 0.82/1.21 (2140) {G0,W5,D2,L2,V1,M2} { ! occurrence_of( X, tptp1 ), alpha13( X ) }.
% 0.82/1.21 (2141) {G0,W5,D2,L2,V1,M2} { ! occurrence_of( X, tptp2 ), alpha13( X ) }.
% 0.82/1.21 (2142) {G0,W6,D2,L2,V2,M2} { ! alpha9( X, Y ), occurrence_of( Y, tptp4 )
% 0.82/1.21 }.
% 0.82/1.21 (2143) {G0,W7,D2,L2,V2,M2} { ! alpha9( X, Y ), next_subocc( X, Y, tptp0 )
% 0.82/1.21 }.
% 0.82/1.21 (2144) {G0,W10,D2,L3,V2,M3} { ! occurrence_of( Y, tptp4 ), ! next_subocc(
% 0.82/1.21 X, Y, tptp0 ), alpha9( X, Y ) }.
% 0.82/1.21 (2145) {G0,W6,D2,L2,V2,M2} { ! alpha7( X, Y ), occurrence_of( Y, tptp3 )
% 0.82/1.21 }.
% 0.82/1.21 (2146) {G0,W6,D2,L2,V2,M2} { ! alpha7( X, Y ), root_occ( Y, X ) }.
% 0.82/1.21 (2147) {G0,W9,D2,L3,V2,M3} { ! occurrence_of( Y, tptp3 ), ! root_occ( Y, X
% 0.82/1.21 ), alpha7( X, Y ) }.
% 0.82/1.21 (2148) {G0,W2,D2,L1,V0,M1} { activity( tptp0 ) }.
% 0.82/1.21 (2149) {G0,W2,D2,L1,V0,M1} { ! atomic( tptp0 ) }.
% 0.82/1.21 (2150) {G0,W2,D2,L1,V0,M1} { atomic( tptp4 ) }.
% 0.82/1.21 (2151) {G0,W2,D2,L1,V0,M1} { atomic( tptp1 ) }.
% 0.82/1.21 (2152) {G0,W2,D2,L1,V0,M1} { atomic( tptp2 ) }.
% 0.82/1.21 (2153) {G0,W2,D2,L1,V0,M1} { atomic( tptp3 ) }.
% 0.82/1.21 (2154) {G0,W3,D2,L1,V0,M1} { ! tptp4 = tptp3 }.
% 0.82/1.21 (2155) {G0,W3,D2,L1,V0,M1} { ! tptp4 = tptp1 }.
% 0.82/1.21 (2156) {G0,W3,D2,L1,V0,M1} { ! tptp4 = tptp2 }.
% 0.82/1.21 (2157) {G0,W3,D2,L1,V0,M1} { ! tptp3 = tptp1 }.
% 0.82/1.21 (2158) {G0,W3,D2,L1,V0,M1} { ! tptp3 = tptp2 }.
% 0.82/1.21 (2159) {G0,W3,D2,L1,V0,M1} { ! tptp1 = tptp2 }.
% 0.82/1.21 (2160) {G0,W3,D2,L1,V0,M1} { occurrence_of( skol17, tptp0 ) }.
% 0.82/1.21 (2161) {G0,W9,D2,L3,V2,M3} { ! leaf_occ( X, skol17 ), alpha12( X, Y ),
% 0.82/1.21 occurrence_of( X, tptp2 ) }.
% 0.82/1.21 (2162) {G0,W8,D2,L3,V2,M3} { ! leaf_occ( X, skol17 ), alpha12( X, Y ),
% 0.82/1.21 alpha10( Y ) }.
% 0.82/1.21 (2163) {G0,W6,D2,L2,V2,M2} { ! alpha12( X, Y ), occurrence_of( X, tptp1 )
% 0.82/1.21 }.
% 0.82/1.21 (2164) {G0,W5,D2,L2,V2,M2} { ! alpha12( X, Y ), alpha8( Y ) }.
% 0.82/1.21 (2165) {G0,W8,D2,L3,V2,M3} { ! occurrence_of( X, tptp1 ), ! alpha8( Y ),
% 0.82/1.21 alpha12( X, Y ) }.
% 0.82/1.21 (2166) {G0,W6,D3,L2,V2,M2} { ! alpha10( X ), occurrence_of( skol18( Y ),
% 0.82/1.21 tptp1 ) }.
% 0.82/1.21 (2167) {G0,W7,D3,L2,V1,M2} { ! alpha10( X ), min_precedes( X, skol18( X )
% 0.82/1.21 , tptp0 ) }.
% 0.82/1.21 (2168) {G0,W9,D2,L3,V2,M3} { ! occurrence_of( Y, tptp1 ), ! min_precedes(
% 0.82/1.21 X, Y, tptp0 ), alpha10( X ) }.
% 0.82/1.21 (2169) {G0,W6,D3,L2,V2,M2} { ! alpha8( X ), occurrence_of( skol19( Y ),
% 0.82/1.21 tptp2 ) }.
% 0.82/1.21 (2170) {G0,W7,D3,L2,V1,M2} { ! alpha8( X ), min_precedes( X, skol19( X ),
% 0.82/1.21 tptp0 ) }.
% 0.82/1.21 (2171) {G0,W9,D2,L3,V2,M3} { ! occurrence_of( Y, tptp2 ), ! min_precedes(
% 0.82/1.21 X, Y, tptp0 ), alpha8( X ) }.
% 0.82/1.21
% 0.82/1.21
% 0.82/1.21 Total Proof:
% 0.82/1.21
% 0.82/1.21 subsumption: (31) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), !
% 0.82/1.21 arboreal( X ), atomic( Y ) }.
% 0.82/1.21 parent0: (2088) {G0,W7,D2,L3,V2,M3} { ! occurrence_of( X, Y ), ! arboreal
% 0.82/1.21 ( X ), atomic( Y ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 2 ==> 2
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (32) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), ! atomic
% 0.82/1.21 ( Y ), arboreal( X ) }.
% 0.82/1.21 parent0: (2089) {G0,W7,D2,L3,V2,M3} { ! occurrence_of( X, Y ), ! atomic( Y
% 0.82/1.21 ), arboreal( X ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 2 ==> 2
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (40) {G0,W8,D3,L2,V2,M2} I { ! atocc( X, Y ), alpha5( X, skol6
% 0.82/1.21 ( X, Y ) ) }.
% 0.82/1.21 parent0: (2097) {G0,W8,D3,L2,V2,M2} { ! atocc( X, Y ), alpha5( X, skol6( X
% 0.82/1.21 , Y ) ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (42) {G0,W5,D2,L2,V2,M2} I { ! alpha5( X, Y ), atomic( Y ) }.
% 0.82/1.21 parent0: (2099) {G0,W5,D2,L2,V2,M2} { ! alpha5( X, Y ), atomic( Y ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (43) {G0,W6,D2,L2,V2,M2} I { ! alpha5( X, Y ), occurrence_of(
% 0.82/1.21 X, Y ) }.
% 0.82/1.21 parent0: (2100) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), occurrence_of( X,
% 0.82/1.21 Y ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (62) {G0,W12,D3,L2,V3,M2} I { ! min_precedes( Y, Z, X ),
% 0.82/1.21 alpha6( X, Y, Z, skol11( X, Y, Z ) ) }.
% 0.82/1.21 parent0: (2119) {G0,W12,D3,L2,V3,M2} { ! min_precedes( Y, Z, X ), alpha6(
% 0.82/1.21 X, Y, Z, skol11( X, Y, Z ) ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 Z := Z
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (65) {G0,W8,D2,L2,V4,M2} I { ! alpha6( X, Y, Z, T ), atocc( Y
% 0.82/1.21 , T ) }.
% 0.82/1.21 parent0: (2122) {G0,W8,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), atocc( Y, T
% 0.82/1.21 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 Z := Z
% 0.82/1.21 T := T
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (77) {G0,W7,D3,L2,V1,M2} I { ! occurrence_of( X, tptp0 ),
% 0.82/1.21 alpha11( X, skol20( X ) ) }.
% 0.82/1.21 parent0: (2134) {G0,W7,D3,L2,V1,M2} { ! occurrence_of( X, tptp0 ), alpha11
% 0.82/1.21 ( X, skol20( X ) ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (80) {G0,W8,D3,L2,V2,M2} I { ! alpha11( X, Y ), leaf_occ(
% 0.82/1.21 skol16( X, Y ), X ) }.
% 0.82/1.21 parent0: (2137) {G0,W8,D3,L2,V2,M2} { ! alpha11( X, Y ), leaf_occ( skol16
% 0.82/1.21 ( X, Y ), X ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (92) {G0,W2,D2,L1,V0,M1} I { ! atomic( tptp0 ) }.
% 0.82/1.21 parent0: (2149) {G0,W2,D2,L1,V0,M1} { ! atomic( tptp0 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (103) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol17, tptp0 )
% 0.82/1.21 }.
% 0.82/1.21 parent0: (2160) {G0,W3,D2,L1,V0,M1} { occurrence_of( skol17, tptp0 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (105) {G0,W8,D2,L3,V2,M3} I { ! leaf_occ( X, skol17 ), alpha12
% 0.82/1.21 ( X, Y ), alpha10( Y ) }.
% 0.82/1.21 parent0: (2162) {G0,W8,D2,L3,V2,M3} { ! leaf_occ( X, skol17 ), alpha12( X
% 0.82/1.21 , Y ), alpha10( Y ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 2 ==> 2
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (107) {G0,W5,D2,L2,V2,M2} I { ! alpha12( X, Y ), alpha8( Y )
% 0.82/1.21 }.
% 0.82/1.21 parent0: (2164) {G0,W5,D2,L2,V2,M2} { ! alpha12( X, Y ), alpha8( Y ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (110) {G0,W7,D3,L2,V1,M2} I { ! alpha10( X ), min_precedes( X
% 0.82/1.21 , skol18( X ), tptp0 ) }.
% 0.82/1.21 parent0: (2167) {G0,W7,D3,L2,V1,M2} { ! alpha10( X ), min_precedes( X,
% 0.82/1.21 skol18( X ), tptp0 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (113) {G0,W7,D3,L2,V1,M2} I { ! alpha8( X ), min_precedes( X,
% 0.82/1.21 skol19( X ), tptp0 ) }.
% 0.82/1.21 parent0: (2170) {G0,W7,D3,L2,V1,M2} { ! alpha8( X ), min_precedes( X,
% 0.82/1.21 skol19( X ), tptp0 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2358) {G1,W4,D2,L2,V0,M2} { ! arboreal( skol17 ), atomic(
% 0.82/1.21 tptp0 ) }.
% 0.82/1.21 parent0[0]: (31) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), !
% 0.82/1.21 arboreal( X ), atomic( Y ) }.
% 0.82/1.21 parent1[0]: (103) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol17, tptp0 )
% 0.82/1.21 }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := skol17
% 0.82/1.21 Y := tptp0
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2359) {G1,W2,D2,L1,V0,M1} { ! arboreal( skol17 ) }.
% 0.82/1.21 parent0[0]: (92) {G0,W2,D2,L1,V0,M1} I { ! atomic( tptp0 ) }.
% 0.82/1.21 parent1[1]: (2358) {G1,W4,D2,L2,V0,M2} { ! arboreal( skol17 ), atomic(
% 0.82/1.21 tptp0 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (468) {G1,W2,D2,L1,V0,M1} R(31,103);r(92) { ! arboreal( skol17
% 0.82/1.21 ) }.
% 0.82/1.21 parent0: (2359) {G1,W2,D2,L1,V0,M1} { ! arboreal( skol17 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2360) {G1,W5,D2,L2,V1,M2} { ! occurrence_of( skol17, X ), !
% 0.82/1.21 atomic( X ) }.
% 0.82/1.21 parent0[0]: (468) {G1,W2,D2,L1,V0,M1} R(31,103);r(92) { ! arboreal( skol17
% 0.82/1.21 ) }.
% 0.82/1.21 parent1[2]: (32) {G0,W7,D2,L3,V2,M3} I { ! occurrence_of( X, Y ), ! atomic
% 0.82/1.21 ( Y ), arboreal( X ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := skol17
% 0.82/1.21 Y := X
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (483) {G2,W5,D2,L2,V1,M2} R(32,468) { ! occurrence_of( skol17
% 0.82/1.21 , X ), ! atomic( X ) }.
% 0.82/1.21 parent0: (2360) {G1,W5,D2,L2,V1,M2} { ! occurrence_of( skol17, X ), !
% 0.82/1.21 atomic( X ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2361) {G1,W5,D2,L2,V1,M2} { ! atomic( X ), ! alpha5( skol17,
% 0.82/1.21 X ) }.
% 0.82/1.21 parent0[0]: (483) {G2,W5,D2,L2,V1,M2} R(32,468) { ! occurrence_of( skol17,
% 0.82/1.21 X ), ! atomic( X ) }.
% 0.82/1.21 parent1[1]: (43) {G0,W6,D2,L2,V2,M2} I { ! alpha5( X, Y ), occurrence_of( X
% 0.82/1.21 , Y ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := skol17
% 0.82/1.21 Y := X
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (582) {G3,W5,D2,L2,V1,M2} R(483,43) { ! atomic( X ), ! alpha5
% 0.82/1.21 ( skol17, X ) }.
% 0.82/1.21 parent0: (2361) {G1,W5,D2,L2,V1,M2} { ! atomic( X ), ! alpha5( skol17, X )
% 0.82/1.21 }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 1 ==> 1
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2362) {G1,W7,D3,L2,V2,M2} { atomic( skol6( X, Y ) ), ! atocc
% 0.82/1.21 ( X, Y ) }.
% 0.82/1.21 parent0[0]: (42) {G0,W5,D2,L2,V2,M2} I { ! alpha5( X, Y ), atomic( Y ) }.
% 0.82/1.21 parent1[1]: (40) {G0,W8,D3,L2,V2,M2} I { ! atocc( X, Y ), alpha5( X, skol6
% 0.82/1.21 ( X, Y ) ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := skol6( X, Y )
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (598) {G1,W7,D3,L2,V2,M2} R(40,42) { ! atocc( X, Y ), atomic(
% 0.82/1.21 skol6( X, Y ) ) }.
% 0.82/1.21 parent0: (2362) {G1,W7,D3,L2,V2,M2} { atomic( skol6( X, Y ) ), ! atocc( X
% 0.82/1.21 , Y ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 1
% 0.82/1.21 1 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2363) {G1,W7,D3,L2,V1,M2} { ! atomic( skol6( skol17, X ) ), !
% 0.82/1.21 atocc( skol17, X ) }.
% 0.82/1.21 parent0[1]: (582) {G3,W5,D2,L2,V1,M2} R(483,43) { ! atomic( X ), ! alpha5(
% 0.82/1.21 skol17, X ) }.
% 0.82/1.21 parent1[1]: (40) {G0,W8,D3,L2,V2,M2} I { ! atocc( X, Y ), alpha5( X, skol6
% 0.82/1.21 ( X, Y ) ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := skol6( skol17, X )
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := skol17
% 0.82/1.21 Y := X
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2364) {G2,W6,D2,L2,V1,M2} { ! atocc( skol17, X ), ! atocc(
% 0.82/1.21 skol17, X ) }.
% 0.82/1.21 parent0[0]: (2363) {G1,W7,D3,L2,V1,M2} { ! atomic( skol6( skol17, X ) ), !
% 0.82/1.21 atocc( skol17, X ) }.
% 0.82/1.21 parent1[1]: (598) {G1,W7,D3,L2,V2,M2} R(40,42) { ! atocc( X, Y ), atomic(
% 0.82/1.21 skol6( X, Y ) ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := skol17
% 0.82/1.21 Y := X
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 factor: (2365) {G2,W3,D2,L1,V1,M1} { ! atocc( skol17, X ) }.
% 0.82/1.21 parent0[0, 1]: (2364) {G2,W6,D2,L2,V1,M2} { ! atocc( skol17, X ), ! atocc
% 0.82/1.21 ( skol17, X ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (626) {G4,W3,D2,L1,V1,M1} R(582,40);r(598) { ! atocc( skol17,
% 0.82/1.21 X ) }.
% 0.82/1.21 parent0: (2365) {G2,W3,D2,L1,V1,M1} { ! atocc( skol17, X ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2366) {G1,W5,D2,L1,V3,M1} { ! alpha6( Y, skol17, Z, X ) }.
% 0.82/1.21 parent0[0]: (626) {G4,W3,D2,L1,V1,M1} R(582,40);r(598) { ! atocc( skol17, X
% 0.82/1.21 ) }.
% 0.82/1.21 parent1[1]: (65) {G0,W8,D2,L2,V4,M2} I { ! alpha6( X, Y, Z, T ), atocc( Y,
% 0.82/1.21 T ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := Y
% 0.82/1.21 Y := skol17
% 0.82/1.21 Z := Z
% 0.82/1.21 T := X
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (1233) {G5,W5,D2,L1,V3,M1} R(65,626) { ! alpha6( X, skol17, Y
% 0.82/1.21 , Z ) }.
% 0.82/1.21 parent0: (2366) {G1,W5,D2,L1,V3,M1} { ! alpha6( Y, skol17, Z, X ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := Z
% 0.82/1.21 Y := X
% 0.82/1.21 Z := Y
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2367) {G1,W4,D2,L1,V2,M1} { ! min_precedes( skol17, Y, X )
% 0.82/1.21 }.
% 0.82/1.21 parent0[0]: (1233) {G5,W5,D2,L1,V3,M1} R(65,626) { ! alpha6( X, skol17, Y,
% 0.82/1.21 Z ) }.
% 0.82/1.21 parent1[1]: (62) {G0,W12,D3,L2,V3,M2} I { ! min_precedes( Y, Z, X ), alpha6
% 0.82/1.21 ( X, Y, Z, skol11( X, Y, Z ) ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 Y := Y
% 0.82/1.21 Z := skol11( X, skol17, Y )
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := X
% 0.82/1.21 Y := skol17
% 0.82/1.21 Z := Y
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (1237) {G6,W4,D2,L1,V2,M1} R(1233,62) { ! min_precedes( skol17
% 0.82/1.21 , X, Y ) }.
% 0.82/1.21 parent0: (2367) {G1,W4,D2,L1,V2,M1} { ! min_precedes( skol17, Y, X ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := Y
% 0.82/1.21 Y := X
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2368) {G1,W4,D3,L1,V0,M1} { alpha11( skol17, skol20( skol17 )
% 0.82/1.21 ) }.
% 0.82/1.21 parent0[0]: (77) {G0,W7,D3,L2,V1,M2} I { ! occurrence_of( X, tptp0 ),
% 0.82/1.21 alpha11( X, skol20( X ) ) }.
% 0.82/1.21 parent1[0]: (103) {G0,W3,D2,L1,V0,M1} I { occurrence_of( skol17, tptp0 )
% 0.82/1.21 }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := skol17
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (1588) {G1,W4,D3,L1,V0,M1} R(77,103) { alpha11( skol17, skol20
% 0.82/1.21 ( skol17 ) ) }.
% 0.82/1.21 parent0: (2368) {G1,W4,D3,L1,V0,M1} { alpha11( skol17, skol20( skol17 ) )
% 0.82/1.21 }.
% 0.82/1.21 substitution0:
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2369) {G1,W2,D2,L1,V0,M1} { ! alpha10( skol17 ) }.
% 0.82/1.21 parent0[0]: (1237) {G6,W4,D2,L1,V2,M1} R(1233,62) { ! min_precedes( skol17
% 0.82/1.21 , X, Y ) }.
% 0.82/1.21 parent1[1]: (110) {G0,W7,D3,L2,V1,M2} I { ! alpha10( X ), min_precedes( X,
% 0.82/1.21 skol18( X ), tptp0 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := skol18( skol17 )
% 0.82/1.21 Y := tptp0
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := skol17
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (1943) {G7,W2,D2,L1,V0,M1} R(110,1237) { ! alpha10( skol17 )
% 0.82/1.21 }.
% 0.82/1.21 parent0: (2369) {G1,W2,D2,L1,V0,M1} { ! alpha10( skol17 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2370) {G1,W2,D2,L1,V0,M1} { ! alpha8( skol17 ) }.
% 0.82/1.21 parent0[0]: (1237) {G6,W4,D2,L1,V2,M1} R(1233,62) { ! min_precedes( skol17
% 0.82/1.21 , X, Y ) }.
% 0.82/1.21 parent1[1]: (113) {G0,W7,D3,L2,V1,M2} I { ! alpha8( X ), min_precedes( X,
% 0.82/1.21 skol19( X ), tptp0 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := skol19( skol17 )
% 0.82/1.21 Y := tptp0
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := skol17
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (2018) {G7,W2,D2,L1,V0,M1} R(113,1237) { ! alpha8( skol17 )
% 0.82/1.21 }.
% 0.82/1.21 parent0: (2370) {G1,W2,D2,L1,V0,M1} { ! alpha8( skol17 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2371) {G1,W3,D2,L1,V1,M1} { ! alpha12( X, skol17 ) }.
% 0.82/1.21 parent0[0]: (2018) {G7,W2,D2,L1,V0,M1} R(113,1237) { ! alpha8( skol17 ) }.
% 0.82/1.21 parent1[1]: (107) {G0,W5,D2,L2,V2,M2} I { ! alpha12( X, Y ), alpha8( Y )
% 0.82/1.21 }.
% 0.82/1.21 substitution0:
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := X
% 0.82/1.21 Y := skol17
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (2049) {G8,W3,D2,L1,V1,M1} R(2018,107) { ! alpha12( X, skol17
% 0.82/1.21 ) }.
% 0.82/1.21 parent0: (2371) {G1,W3,D2,L1,V1,M1} { ! alpha12( X, skol17 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2372) {G1,W5,D2,L2,V1,M2} { ! leaf_occ( X, skol17 ), alpha10
% 0.82/1.21 ( skol17 ) }.
% 0.82/1.21 parent0[0]: (2049) {G8,W3,D2,L1,V1,M1} R(2018,107) { ! alpha12( X, skol17 )
% 0.82/1.21 }.
% 0.82/1.21 parent1[1]: (105) {G0,W8,D2,L3,V2,M3} I { ! leaf_occ( X, skol17 ), alpha12
% 0.82/1.21 ( X, Y ), alpha10( Y ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := X
% 0.82/1.21 Y := skol17
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2373) {G2,W3,D2,L1,V1,M1} { ! leaf_occ( X, skol17 ) }.
% 0.82/1.21 parent0[0]: (1943) {G7,W2,D2,L1,V0,M1} R(110,1237) { ! alpha10( skol17 )
% 0.82/1.21 }.
% 0.82/1.21 parent1[1]: (2372) {G1,W5,D2,L2,V1,M2} { ! leaf_occ( X, skol17 ), alpha10
% 0.82/1.21 ( skol17 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (2050) {G9,W3,D2,L1,V1,M1} R(2049,105);r(1943) { ! leaf_occ( X
% 0.82/1.21 , skol17 ) }.
% 0.82/1.21 parent0: (2373) {G2,W3,D2,L1,V1,M1} { ! leaf_occ( X, skol17 ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2374) {G1,W3,D2,L1,V1,M1} { ! alpha11( skol17, X ) }.
% 0.82/1.21 parent0[0]: (2050) {G9,W3,D2,L1,V1,M1} R(2049,105);r(1943) { ! leaf_occ( X
% 0.82/1.21 , skol17 ) }.
% 0.82/1.21 parent1[1]: (80) {G0,W8,D3,L2,V2,M2} I { ! alpha11( X, Y ), leaf_occ(
% 0.82/1.21 skol16( X, Y ), X ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := skol16( skol17, X )
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 X := skol17
% 0.82/1.21 Y := X
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (2051) {G10,W3,D2,L1,V1,M1} R(2050,80) { ! alpha11( skol17, X
% 0.82/1.21 ) }.
% 0.82/1.21 parent0: (2374) {G1,W3,D2,L1,V1,M1} { ! alpha11( skol17, X ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := X
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 0 ==> 0
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 resolution: (2375) {G2,W0,D0,L0,V0,M0} { }.
% 0.82/1.21 parent0[0]: (2051) {G10,W3,D2,L1,V1,M1} R(2050,80) { ! alpha11( skol17, X )
% 0.82/1.21 }.
% 0.82/1.21 parent1[0]: (1588) {G1,W4,D3,L1,V0,M1} R(77,103) { alpha11( skol17, skol20
% 0.82/1.21 ( skol17 ) ) }.
% 0.82/1.21 substitution0:
% 0.82/1.21 X := skol20( skol17 )
% 0.82/1.21 end
% 0.82/1.21 substitution1:
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 subsumption: (2055) {G11,W0,D0,L0,V0,M0} R(2051,1588) { }.
% 0.82/1.21 parent0: (2375) {G2,W0,D0,L0,V0,M0} { }.
% 0.82/1.21 substitution0:
% 0.82/1.21 end
% 0.82/1.21 permutation0:
% 0.82/1.21 end
% 0.82/1.21
% 0.82/1.21 Proof check complete!
% 0.82/1.21
% 0.82/1.21 Memory use:
% 0.82/1.21
% 0.82/1.21 space for terms: 28812
% 0.82/1.21 space for clauses: 92227
% 0.82/1.21
% 0.82/1.21
% 0.82/1.21 clauses generated: 5638
% 0.82/1.21 clauses kept: 2056
% 0.82/1.21 clauses selected: 379
% 0.82/1.21 clauses deleted: 34
% 0.82/1.21 clauses inuse deleted: 28
% 0.82/1.21
% 0.82/1.21 subsentry: 8110
% 0.82/1.21 literals s-matched: 5577
% 0.82/1.21 literals matched: 5520
% 0.82/1.21 full subsumption: 1647
% 0.82/1.21
% 0.82/1.21 checksum: 991857133
% 0.82/1.21
% 0.82/1.21
% 0.82/1.21 Bliksem ended
%------------------------------------------------------------------------------