%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NLP204+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n004.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 01:04:40 EDT 2022
% Result : Theorem 0.72s 1.18s
% Output : Refutation 0.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NLP204+1 : TPTP v8.1.0. Released v2.4.0.
% 0.12/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n004.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 : Fri Jul 1 08:28:38 EDT 2022
% 0.18/0.33 % CPUTime :
% 0.72/1.12 *** allocated 10000 integers for termspace/termends
% 0.72/1.12 *** allocated 10000 integers for clauses
% 0.72/1.12 *** allocated 10000 integers for justifications
% 0.72/1.12 Bliksem 1.12
% 0.72/1.12
% 0.72/1.12
% 0.72/1.12 Automatic Strategy Selection
% 0.72/1.12
% 0.72/1.12
% 0.72/1.12 Clauses:
% 0.72/1.12
% 0.72/1.12 { ! jules_forename( X, Y ), forename( X, Y ) }.
% 0.72/1.12 { ! forename( X, Y ), relname( X, Y ) }.
% 0.72/1.12 { ! furniture( X, Y ), instrumentality( X, Y ) }.
% 0.72/1.12 { ! seat( X, Y ), furniture( X, Y ) }.
% 0.72/1.12 { ! frontseat( X, Y ), seat( X, Y ) }.
% 0.72/1.12 { ! location( X, Y ), object( X, Y ) }.
% 0.72/1.12 { ! city( X, Y ), location( X, Y ) }.
% 0.72/1.12 { ! hollywood_placename( X, Y ), placename( X, Y ) }.
% 0.72/1.12 { ! abstraction( X, Y ), unisex( X, Y ) }.
% 0.72/1.12 { ! abstraction( X, Y ), general( X, Y ) }.
% 0.72/1.12 { ! abstraction( X, Y ), nonhuman( X, Y ) }.
% 0.72/1.12 { ! abstraction( X, Y ), thing( X, Y ) }.
% 0.72/1.12 { ! relation( X, Y ), abstraction( X, Y ) }.
% 0.72/1.12 { ! relname( X, Y ), relation( X, Y ) }.
% 0.72/1.12 { ! placename( X, Y ), relname( X, Y ) }.
% 0.72/1.12 { ! transport( X, Y ), instrumentality( X, Y ) }.
% 0.72/1.12 { ! vehicle( X, Y ), transport( X, Y ) }.
% 0.72/1.12 { ! car( X, Y ), vehicle( X, Y ) }.
% 0.72/1.12 { ! chevy( X, Y ), car( X, Y ) }.
% 0.72/1.12 { ! way( X, Y ), artifact( X, Y ) }.
% 0.72/1.12 { ! street( X, Y ), way( X, Y ) }.
% 0.72/1.12 { ! barrel( X, Y ), event( X, Y ) }.
% 0.72/1.12 { ! two( X, Y ), group( X, Y ) }.
% 0.72/1.12 { ! man( X, Y ), male( X, Y ) }.
% 0.72/1.12 { ! human_person( X, Y ), animate( X, Y ) }.
% 0.72/1.12 { ! human_person( X, Y ), human( X, Y ) }.
% 0.72/1.12 { ! organism( X, Y ), living( X, Y ) }.
% 0.72/1.12 { ! organism( X, Y ), impartial( X, Y ) }.
% 0.72/1.12 { ! organism( X, Y ), entity( X, Y ) }.
% 0.72/1.12 { ! human_person( X, Y ), organism( X, Y ) }.
% 0.72/1.12 { ! man( X, Y ), human_person( X, Y ) }.
% 0.72/1.12 { ! fellow( X, Y ), man( X, Y ) }.
% 0.72/1.12 { ! wear( X, Y ), event( X, Y ) }.
% 0.72/1.12 { ! set( X, Y ), multiple( X, Y ) }.
% 0.72/1.12 { ! group( X, Y ), set( X, Y ) }.
% 0.72/1.12 { ! clothes( X, Y ), artifact( X, Y ) }.
% 0.72/1.12 { ! coat( X, Y ), clothes( X, Y ) }.
% 0.72/1.12 { ! object( X, Y ), unisex( X, Y ) }.
% 0.72/1.12 { ! object( X, Y ), impartial( X, Y ) }.
% 0.72/1.12 { ! object( X, Y ), nonliving( X, Y ) }.
% 0.72/1.12 { ! entity( X, Y ), existent( X, Y ) }.
% 0.72/1.12 { ! entity( X, Y ), specific( X, Y ) }.
% 0.72/1.12 { ! entity( X, Y ), thing( X, Y ) }.
% 0.72/1.12 { ! object( X, Y ), entity( X, Y ) }.
% 0.72/1.12 { ! artifact( X, Y ), object( X, Y ) }.
% 0.72/1.12 { ! instrumentality( X, Y ), artifact( X, Y ) }.
% 0.72/1.12 { ! device( X, Y ), instrumentality( X, Y ) }.
% 0.72/1.12 { ! wheel( X, Y ), device( X, Y ) }.
% 0.72/1.12 { ! event( X, Y ), eventuality( X, Y ) }.
% 0.72/1.12 { ! state( X, Y ), event( X, Y ) }.
% 0.72/1.12 { ! eventuality( X, Y ), unisex( X, Y ) }.
% 0.72/1.12 { ! eventuality( X, Y ), nonexistent( X, Y ) }.
% 0.72/1.12 { ! eventuality( X, Y ), specific( X, Y ) }.
% 0.72/1.12 { ! thing( X, Y ), singleton( X, Y ) }.
% 0.72/1.12 { ! eventuality( X, Y ), thing( X, Y ) }.
% 0.72/1.12 { ! state( X, Y ), eventuality( X, Y ) }.
% 0.72/1.12 { ! animate( X, Y ), ! nonliving( X, Y ) }.
% 0.72/1.12 { ! existent( X, Y ), ! nonexistent( X, Y ) }.
% 0.72/1.12 { ! nonhuman( X, Y ), ! human( X, Y ) }.
% 0.72/1.12 { ! nonliving( X, Y ), ! living( X, Y ) }.
% 0.72/1.12 { ! singleton( X, Y ), ! multiple( X, Y ) }.
% 0.72/1.12 { ! specific( X, Y ), ! general( X, Y ) }.
% 0.72/1.12 { ! unisex( X, Y ), ! male( X, Y ) }.
% 0.72/1.12 { ! white( X, Y ), ! black( X, Y ) }.
% 0.72/1.12 { ! young( X, Y ), ! old( X, Y ) }.
% 0.72/1.12 { ! entity( X, Y ), ! forename( X, Z ), ! of( X, Z, Y ), ! forename( X, T )
% 0.72/1.12 , T = Z, ! of( X, T, Y ) }.
% 0.72/1.12 { ! entity( X, Y ), ! placename( X, Z ), ! of( X, Z, Y ), ! placename( X, T
% 0.72/1.12 ), T = Z, ! of( X, T, Y ) }.
% 0.72/1.12 { ! two( X, Y ), member( X, skol1( X, Y ), Y ) }.
% 0.72/1.12 { ! two( X, Y ), alpha1( X, Y, skol1( X, Y ) ) }.
% 0.72/1.12 { ! member( X, Z, Y ), ! alpha1( X, Y, Z ), two( X, Y ) }.
% 0.72/1.12 { ! alpha1( X, Y, Z ), member( X, skol2( X, Y, T ), Y ) }.
% 0.72/1.12 { ! alpha1( X, Y, Z ), alpha3( X, Y, Z, skol2( X, Y, Z ) ) }.
% 0.72/1.12 { ! member( X, T, Y ), ! alpha3( X, Y, Z, T ), alpha1( X, Y, Z ) }.
% 0.72/1.12 { ! alpha3( X, Y, Z, T ), ! T = Z }.
% 0.72/1.12 { ! alpha3( X, Y, Z, T ), alpha4( X, Y, Z, T ) }.
% 0.72/1.12 { T = Z, ! alpha4( X, Y, Z, T ), alpha3( X, Y, Z, T ) }.
% 0.72/1.12 { ! alpha4( X, Y, Z, T ), ! member( X, U, Y ), alpha2( Z, T, U ) }.
% 0.72/1.12 { ! alpha2( Z, T, skol3( U, W, Z, T ) ), alpha4( X, Y, Z, T ) }.
% 0.72/1.12 { member( X, skol3( X, Y, Z, T ), Y ), alpha4( X, Y, Z, T ) }.
% 0.72/1.12 { ! alpha2( X, Y, Z ), Z = Y, Z = X }.
% 0.72/1.12 { ! Z = Y, alpha2( X, Y, Z ) }.
% 0.72/1.12 { ! Z = X, alpha2( X, Y, Z ) }.
% 0.72/1.12 { ! nonreflexive( Z, T ), ! agent( Z, T, X ), ! patient( Z, T, Y ), ! X = Y
% 0.72/1.12 }.
% 0.72/1.12 { ! member( X, Y, Y ) }.
% 0.72/1.12 { ! be( Z, T, X, Y ), X = Y }.
% 0.72/1.12 { actual_world( skol4 ) }.
% 0.72/1.12 { of( skol4, skol11, skol9 ) }.
% 0.72/1.12 { man( skol4, skol9 ) }.
% 0.72/1.12 { jules_forename( skol4, skol11 ) }.
% 0.72/1.12 { forename( skol4, skol11 ) }.
% 0.72/1.12 { frontseat( skol4, skol12 ) }.
% 0.72/1.12 { chevy( skol4, skol13 ) }.
% 0.72/1.12 { white( skol4, skol13 ) }.
% 0.72/1.12 { dirty( skol4, skol13 ) }.
% 0.72/1.12 { old( skol4, skol13 ) }.
% 0.72/1.12 { of( skol4, skol14, skol15 ) }.
% 0.72/1.12 { city( skol4, skol15 ) }.
% 0.72/1.12 { hollywood_placename( skol4, skol14 ) }.
% 0.72/1.12 { placename( skol4, skol14 ) }.
% 0.72/1.12 { street( skol4, skol15 ) }.
% 0.72/1.12 { lonely( skol4, skol15 ) }.
% 0.72/1.12 { event( skol4, skol16 ) }.
% 0.72/1.12 { agent( skol4, skol16, skol13 ) }.
% 0.72/1.12 { present( skol4, skol16 ) }.
% 0.72/1.12 { barrel( skol4, skol16 ) }.
% 0.72/1.12 { down( skol4, skol16, skol15 ) }.
% 0.72/1.12 { in( skol4, skol16, skol15 ) }.
% 0.72/1.12 { alpha7( skol4, skol12, skol17 ) }.
% 0.72/1.12 { ! member( skol4, X, skol18 ), ! member( skol4, Y, skol17 ), wear( skol4,
% 0.72/1.12 skol19( Z, T ) ) }.
% 0.72/1.12 { ! member( skol4, X, skol18 ), ! member( skol4, Y, skol17 ), alpha11(
% 0.72/1.12 skol4, X, Y, skol19( X, Y ) ) }.
% 0.72/1.12 { group( skol4, skol18 ) }.
% 0.72/1.12 { alpha6( skol4, skol18 ) }.
% 0.72/1.12 { wheel( skol4, skol20 ) }.
% 0.72/1.12 { state( skol4, skol21 ) }.
% 0.72/1.12 { be( skol4, skol21, skol9, skol20 ) }.
% 0.72/1.12 { behind( skol4, skol20, skol20 ) }.
% 0.72/1.12 { ! alpha11( X, Y, Z, T ), alpha13( X, Y, Z, T ) }.
% 0.72/1.12 { ! alpha11( X, Y, Z, T ), nonreflexive( X, T ) }.
% 0.72/1.12 { ! alpha13( X, Y, Z, T ), ! nonreflexive( X, T ), alpha11( X, Y, Z, T ) }
% 0.72/1.12 .
% 0.72/1.12 { ! alpha13( X, Y, Z, T ), alpha9( X, Z, T ) }.
% 0.72/1.12 { ! alpha13( X, Y, Z, T ), patient( X, T, Y ) }.
% 0.72/1.12 { ! alpha13( X, Y, Z, T ), present( X, T ) }.
% 0.72/1.12 { ! alpha9( X, Z, T ), ! patient( X, T, Y ), ! present( X, T ), alpha13( X
% 0.72/1.12 , Y, Z, T ) }.
% 0.72/1.12 { ! alpha9( X, Y, Z ), event( X, Z ) }.
% 0.72/1.12 { ! alpha9( X, Y, Z ), agent( X, Z, Y ) }.
% 0.72/1.12 { ! event( X, Z ), ! agent( X, Z, Y ), alpha9( X, Y, Z ) }.
% 0.72/1.12 { ! alpha7( X, Y, Z ), alpha10( X, Y, Z ) }.
% 0.72/1.12 { ! alpha7( X, Y, Z ), alpha5( X, Z ) }.
% 0.72/1.12 { ! alpha10( X, Y, Z ), ! alpha5( X, Z ), alpha7( X, Y, Z ) }.
% 0.72/1.12 { ! alpha10( X, Y, Z ), alpha12( X, Y, Z ) }.
% 0.72/1.12 { ! alpha10( X, Y, Z ), group( X, Z ) }.
% 0.72/1.12 { ! alpha12( X, Y, Z ), ! group( X, Z ), alpha10( X, Y, Z ) }.
% 0.72/1.12 { ! alpha12( X, Y, Z ), alpha14( X, Y, Z ) }.
% 0.72/1.12 { ! alpha12( X, Y, Z ), two( X, Z ) }.
% 0.72/1.12 { ! alpha14( X, Y, Z ), ! two( X, Z ), alpha12( X, Y, Z ) }.
% 0.72/1.12 { ! alpha14( X, Y, Z ), ! member( X, T, Z ), alpha15( X, Y, T ) }.
% 0.72/1.12 { member( X, skol5( X, T, Z ), Z ), alpha14( X, Y, Z ) }.
% 0.72/1.12 { ! alpha15( X, Y, skol5( X, Y, Z ) ), alpha14( X, Y, Z ) }.
% 0.72/1.12 { ! alpha15( X, Y, Z ), state( X, skol6( X, T, U ) ) }.
% 0.72/1.12 { ! alpha15( X, Y, Z ), in( X, skol10( X, Y, T ), Y ) }.
% 0.72/1.12 { ! alpha15( X, Y, Z ), be( X, skol6( X, Y, Z ), Z, skol10( X, Y, Z ) ) }.
% 0.72/1.12 { ! state( X, T ), ! be( X, T, Z, U ), ! in( X, U, Y ), alpha15( X, Y, Z )
% 0.72/1.12 }.
% 0.72/1.12 { ! alpha6( X, Y ), ! member( X, Z, Y ), alpha8( X, Z ) }.
% 0.72/1.12 { ! alpha8( X, skol7( X, Z ) ), alpha6( X, Y ) }.
% 0.72/1.12 { member( X, skol7( X, Y ), Y ), alpha6( X, Y ) }.
% 0.72/1.12 { ! alpha8( X, Y ), coat( X, Y ) }.
% 0.72/1.12 { ! alpha8( X, Y ), black( X, Y ) }.
% 0.72/1.12 { ! alpha8( X, Y ), cheap( X, Y ) }.
% 0.72/1.12 { ! coat( X, Y ), ! black( X, Y ), ! cheap( X, Y ), alpha8( X, Y ) }.
% 0.72/1.12 { ! alpha5( X, Y ), ! member( X, Z, Y ), fellow( X, Z ) }.
% 0.72/1.12 { ! alpha5( X, Y ), ! member( X, Z, Y ), young( X, Z ) }.
% 0.72/1.12 { ! fellow( X, skol8( X, Z ) ), ! young( X, skol8( X, Z ) ), alpha5( X, Y )
% 0.72/1.12 }.
% 0.72/1.12 { member( X, skol8( X, Y ), Y ), alpha5( X, Y ) }.
% 0.72/1.12
% 0.72/1.12 percentage equality = 0.032362, percentage horn = 0.960784
% 0.72/1.12 This is a problem with some equality
% 0.72/1.12
% 0.72/1.12
% 0.72/1.12
% 0.72/1.12 Options Used:
% 0.72/1.12
% 0.72/1.12 useres = 1
% 0.72/1.12 useparamod = 1
% 0.72/1.12 useeqrefl = 1
% 0.72/1.12 useeqfact = 1
% 0.72/1.12 usefactor = 1
% 0.72/1.12 usesimpsplitting = 0
% 0.72/1.12 usesimpdemod = 5
% 0.72/1.12 usesimpres = 3
% 0.72/1.12
% 0.72/1.12 resimpinuse = 1000
% 0.72/1.12 resimpclauses = 20000
% 0.72/1.12 substype = eqrewr
% 0.72/1.12 backwardsubs = 1
% 0.72/1.12 selectoldest = 5
% 0.72/1.12
% 0.72/1.12 litorderings [0] = split
% 0.72/1.12 litorderings [1] = extend the termordering, first sorting on arguments
% 0.72/1.12
% 0.72/1.12 termordering = kbo
% 0.72/1.12
% 0.72/1.12 litapriori = 0
% 0.72/1.12 termapriori = 1
% 0.72/1.12 litaposteriori = 0
% 0.72/1.12 termaposteriori = 0
% 0.72/1.12 demodaposteriori = 0
% 0.72/1.12 ordereqreflfact = 0
% 0.72/1.12
% 0.72/1.12 litselect = negord
% 0.72/1.12
% 0.72/1.12 maxweight = 15
% 0.72/1.12 maxdepth = 30000
% 0.72/1.12 maxlength = 115
% 0.72/1.12 maxnrvars = 195
% 0.72/1.12 excuselevel = 1
% 0.72/1.12 increasemaxweight = 1
% 0.72/1.12
% 0.72/1.12 maxselected = 10000000
% 0.72/1.12 maxnrclauses = 10000000
% 0.72/1.12
% 0.72/1.12 showgenerated = 0
% 0.72/1.12 showkept = 0
% 0.72/1.12 showselected = 0
% 0.72/1.12 showdeleted = 0
% 0.72/1.12 showresimp = 1
% 0.72/1.12 showstatus = 2000
% 0.72/1.18
% 0.72/1.18 prologoutput = 0
% 0.72/1.18 nrgoals = 5000000
% 0.72/1.18 totalproof = 1
% 0.72/1.18
% 0.72/1.18 Symbols occurring in the translation:
% 0.72/1.18
% 0.72/1.18 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.72/1.18 . [1, 2] (w:1, o:44, a:1, s:1, b:0),
% 0.72/1.18 ! [4, 1] (w:0, o:38, a:1, s:1, b:0),
% 0.72/1.18 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.72/1.18 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.72/1.18 jules_forename [37, 2] (w:1, o:81, a:1, s:1, b:0),
% 0.72/1.18 forename [38, 2] (w:1, o:84, a:1, s:1, b:0),
% 0.72/1.18 relname [39, 2] (w:1, o:85, a:1, s:1, b:0),
% 0.72/1.18 furniture [40, 2] (w:1, o:86, a:1, s:1, b:0),
% 0.72/1.18 instrumentality [41, 2] (w:1, o:80, a:1, s:1, b:0),
% 0.72/1.18 seat [42, 2] (w:1, o:88, a:1, s:1, b:0),
% 0.72/1.18 frontseat [43, 2] (w:1, o:89, a:1, s:1, b:0),
% 0.72/1.18 location [44, 2] (w:1, o:90, a:1, s:1, b:0),
% 0.72/1.18 object [45, 2] (w:1, o:100, a:1, s:1, b:0),
% 0.72/1.18 city [46, 2] (w:1, o:108, a:1, s:1, b:0),
% 0.72/1.18 hollywood_placename [47, 2] (w:1, o:76, a:1, s:1, b:0),
% 0.72/1.18 placename [48, 2] (w:1, o:111, a:1, s:1, b:0),
% 0.72/1.18 abstraction [49, 2] (w:1, o:112, a:1, s:1, b:0),
% 0.72/1.18 unisex [50, 2] (w:1, o:125, a:1, s:1, b:0),
% 0.72/1.18 general [51, 2] (w:1, o:74, a:1, s:1, b:0),
% 0.72/1.18 nonhuman [52, 2] (w:1, o:96, a:1, s:1, b:0),
% 0.72/1.18 thing [53, 2] (w:1, o:122, a:1, s:1, b:0),
% 0.72/1.18 relation [54, 2] (w:1, o:87, a:1, s:1, b:0),
% 0.72/1.18 transport [55, 2] (w:1, o:123, a:1, s:1, b:0),
% 0.72/1.18 vehicle [56, 2] (w:1, o:126, a:1, s:1, b:0),
% 0.72/1.18 car [57, 2] (w:1, o:127, a:1, s:1, b:0),
% 0.72/1.18 chevy [58, 2] (w:1, o:107, a:1, s:1, b:0),
% 0.72/1.18 way [59, 2] (w:1, o:128, a:1, s:1, b:0),
% 0.72/1.18 artifact [60, 2] (w:1, o:129, a:1, s:1, b:0),
% 0.72/1.18 street [61, 2] (w:1, o:113, a:1, s:1, b:0),
% 0.72/1.18 barrel [62, 2] (w:1, o:105, a:1, s:1, b:0),
% 0.72/1.18 event [63, 2] (w:1, o:82, a:1, s:1, b:0),
% 0.72/1.18 two [64, 2] (w:1, o:124, a:1, s:1, b:0),
% 0.72/1.18 group [65, 2] (w:1, o:75, a:1, s:1, b:0),
% 0.72/1.18 man [66, 2] (w:1, o:93, a:1, s:1, b:0),
% 0.72/1.18 male [67, 2] (w:1, o:94, a:1, s:1, b:0),
% 0.72/1.18 human_person [68, 2] (w:1, o:77, a:1, s:1, b:0),
% 0.72/1.18 animate [69, 2] (w:1, o:101, a:1, s:1, b:0),
% 0.72/1.18 human [70, 2] (w:1, o:78, a:1, s:1, b:0),
% 0.72/1.18 organism [71, 2] (w:1, o:109, a:1, s:1, b:0),
% 0.72/1.18 living [72, 2] (w:1, o:91, a:1, s:1, b:0),
% 0.72/1.18 impartial [73, 2] (w:1, o:79, a:1, s:1, b:0),
% 0.72/1.18 entity [74, 2] (w:1, o:83, a:1, s:1, b:0),
% 0.72/1.18 fellow [75, 2] (w:1, o:73, a:1, s:1, b:0),
% 0.72/1.18 wear [76, 2] (w:1, o:130, a:1, s:1, b:0),
% 0.72/1.18 set [77, 2] (w:1, o:114, a:1, s:1, b:0),
% 0.72/1.18 multiple [78, 2] (w:1, o:95, a:1, s:1, b:0),
% 0.72/1.18 clothes [79, 2] (w:1, o:131, a:1, s:1, b:0),
% 0.72/1.18 coat [80, 2] (w:1, o:132, a:1, s:1, b:0),
% 0.72/1.18 nonliving [81, 2] (w:1, o:97, a:1, s:1, b:0),
% 0.72/1.18 existent [82, 2] (w:1, o:71, a:1, s:1, b:0),
% 0.72/1.18 specific [83, 2] (w:1, o:115, a:1, s:1, b:0),
% 0.72/1.18 device [84, 2] (w:1, o:69, a:1, s:1, b:0),
% 0.72/1.18 wheel [85, 2] (w:1, o:133, a:1, s:1, b:0),
% 0.72/1.18 eventuality [86, 2] (w:1, o:72, a:1, s:1, b:0),
% 0.72/1.18 state [87, 2] (w:1, o:116, a:1, s:1, b:0),
% 0.72/1.18 nonexistent [88, 2] (w:1, o:98, a:1, s:1, b:0),
% 0.72/1.18 singleton [89, 2] (w:1, o:117, a:1, s:1, b:0),
% 0.72/1.18 white [90, 2] (w:1, o:134, a:1, s:1, b:0),
% 0.72/1.18 black [91, 2] (w:1, o:106, a:1, s:1, b:0),
% 0.72/1.18 young [92, 2] (w:1, o:135, a:1, s:1, b:0),
% 0.72/1.18 old [93, 2] (w:1, o:110, a:1, s:1, b:0),
% 0.72/1.18 of [95, 3] (w:1, o:137, a:1, s:1, b:0),
% 0.72/1.18 member [97, 3] (w:1, o:138, a:1, s:1, b:0),
% 0.72/1.18 nonreflexive [99, 2] (w:1, o:99, a:1, s:1, b:0),
% 0.72/1.18 agent [100, 3] (w:1, o:139, a:1, s:1, b:0),
% 0.72/1.18 patient [101, 3] (w:1, o:140, a:1, s:1, b:0),
% 0.72/1.18 be [102, 4] (w:1, o:160, a:1, s:1, b:0),
% 0.72/1.18 actual_world [103, 1] (w:1, o:43, a:1, s:1, b:0),
% 0.72/1.18 dirty [111, 2] (w:1, o:70, a:1, s:1, b:0),
% 0.72/1.18 lonely [112, 2] (w:1, o:92, a:1, s:1, b:0),
% 0.72/1.18 present [113, 2] (w:1, o:136, a:1, s:1, b:0),
% 0.72/1.18 down [114, 3] (w:1, o:141, a:1, s:1, b:0),
% 0.72/1.18 in [115, 3] (w:1, o:142, a:1, s:1, b:0),
% 0.72/1.18 cheap [124, 2] (w:1, o:68, a:1, s:1, b:0),
% 0.72/1.18 behind [125, 3] (w:1, o:151, a:1, s:1, b:0),
% 0.72/1.18 alpha1 [126, 3] (w:1, o:143, a:1, s:1, b:1),
% 0.72/1.18 alpha2 [127, 3] (w:1, o:148, a:1, s:1, b:1),
% 0.72/1.18 alpha3 [128, 4] (w:1, o:156, a:1, s:1, b:1),
% 0.72/1.18 alpha4 [129, 4] (w:1, o:157, a:1, s:1, b:1),
% 0.72/1.18 alpha5 [130, 2] (w:1, o:102, a:1, s:1, b:1),
% 0.72/1.18 alpha6 [131, 2] (w:1, o:103, a:1, s:1, b:1),
% 0.72/1.18 alpha7 [132, 3] (w:1, o:149, a:1, s:1, b:1),
% 0.72/1.18 alpha8 [133, 2] (w:1, o:104, a:1, s:1, b:1),
% 0.72/1.18 alpha9 [134, 3] (w:1, o:150, a:1, s:1, b:1),
% 0.72/1.18 alpha10 [135, 3] (w:1, o:144, a:1, s:1, b:1),
% 0.72/1.18 alpha11 [136, 4] (w:1, o:158, a:1, s:1, b:1),
% 0.72/1.18 alpha12 [137, 3] (w:1, o:145, a:1, s:1, b:1),
% 0.72/1.18 alpha13 [138, 4] (w:1, o:159, a:1, s:1, b:1),
% 0.72/1.18 alpha14 [139, 3] (w:1, o:146, a:1, s:1, b:1),
% 0.72/1.18 alpha15 [140, 3] (w:1, o:147, a:1, s:1, b:1),
% 0.72/1.18 skol1 [141, 2] (w:1, o:118, a:1, s:1, b:1),
% 0.72/1.18 skol2 [142, 3] (w:1, o:153, a:1, s:1, b:1),
% 0.72/1.18 skol3 [143, 4] (w:1, o:161, a:1, s:1, b:1),
% 0.72/1.18 skol4 [144, 0] (w:1, o:26, a:1, s:1, b:1),
% 0.72/1.18 skol5 [145, 3] (w:1, o:154, a:1, s:1, b:1),
% 0.72/1.18 skol6 [146, 3] (w:1, o:155, a:1, s:1, b:1),
% 0.72/1.18 skol7 [147, 2] (w:1, o:119, a:1, s:1, b:1),
% 0.72/1.18 skol8 [148, 2] (w:1, o:120, a:1, s:1, b:1),
% 0.72/1.18 skol9 [149, 0] (w:1, o:27, a:1, s:1, b:1),
% 0.72/1.18 skol10 [150, 3] (w:1, o:152, a:1, s:1, b:1),
% 0.72/1.18 skol11 [151, 0] (w:1, o:28, a:1, s:1, b:1),
% 0.72/1.18 skol12 [152, 0] (w:1, o:29, a:1, s:1, b:1),
% 0.72/1.18 skol13 [153, 0] (w:1, o:30, a:1, s:1, b:1),
% 0.72/1.18 skol14 [154, 0] (w:1, o:31, a:1, s:1, b:1),
% 0.72/1.18 skol15 [155, 0] (w:1, o:32, a:1, s:1, b:1),
% 0.72/1.18 skol16 [156, 0] (w:1, o:33, a:1, s:1, b:1),
% 0.72/1.18 skol17 [157, 0] (w:1, o:34, a:1, s:1, b:1),
% 0.72/1.18 skol18 [158, 0] (w:1, o:35, a:1, s:1, b:1),
% 0.72/1.18 skol19 [159, 2] (w:1, o:121, a:1, s:1, b:1),
% 0.72/1.18 skol20 [160, 0] (w:1, o:36, a:1, s:1, b:1),
% 0.72/1.18 skol21 [161, 0] (w:1, o:37, a:1, s:1, b:1).
% 0.72/1.18
% 0.72/1.18
% 0.72/1.18 Starting Search:
% 0.72/1.18
% 0.72/1.18 *** allocated 15000 integers for clauses
% 0.72/1.18 *** allocated 22500 integers for clauses
% 0.72/1.18 *** allocated 33750 integers for clauses
% 0.72/1.18 *** allocated 50625 integers for clauses
% 0.72/1.18 *** allocated 15000 integers for termspace/termends
% 0.72/1.18 *** allocated 75937 integers for clauses
% 0.72/1.18 *** allocated 22500 integers for termspace/termends
% 0.72/1.18 *** allocated 113905 integers for clauses
% 0.72/1.18 Resimplifying inuse:
% 0.72/1.18 Done
% 0.72/1.18
% 0.72/1.18 *** allocated 33750 integers for termspace/termends
% 0.72/1.18 *** allocated 170857 integers for clauses
% 0.72/1.18 *** allocated 50625 integers for termspace/termends
% 0.72/1.18
% 0.72/1.18 Intermediate Status:
% 0.72/1.18 Generated: 5745
% 0.72/1.18 Kept: 3440
% 0.72/1.18 Inuse: 386
% 0.72/1.18 Deleted: 0
% 0.72/1.18 Deletedinuse: 0
% 0.72/1.18
% 0.72/1.18 Resimplifying inuse:
% 0.72/1.18 Done
% 0.72/1.18
% 0.72/1.18 *** allocated 256285 integers for clauses
% 0.72/1.18 *** allocated 75937 integers for termspace/termends
% 0.72/1.18 Resimplifying inuse:
% 0.72/1.18
% 0.72/1.18 Bliksems!, er is een bewijs:
% 0.72/1.18 % SZS status Theorem
% 0.72/1.18 % SZS output start Refutation
% 0.72/1.18
% 0.72/1.18 (23) {G0,W6,D2,L2,V2,M2} I { ! man( X, Y ), male( X, Y ) }.
% 0.72/1.18 (37) {G0,W6,D2,L2,V2,M2} I { ! object( X, Y ), unisex( X, Y ) }.
% 0.72/1.18 (44) {G0,W6,D2,L2,V2,M2} I { ! artifact( X, Y ), object( X, Y ) }.
% 0.72/1.18 (45) {G0,W6,D2,L2,V2,M2} I { ! instrumentality( X, Y ), artifact( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 (46) {G0,W6,D2,L2,V2,M2} I { ! device( X, Y ), instrumentality( X, Y ) }.
% 0.72/1.18 (47) {G0,W6,D2,L2,V2,M2} I { ! wheel( X, Y ), device( X, Y ) }.
% 0.72/1.18 (62) {G0,W6,D2,L2,V2,M2} I { ! unisex( X, Y ), ! male( X, Y ) }.
% 0.72/1.18 (84) {G0,W8,D2,L2,V4,M2} I { ! be( Z, T, X, Y ), X = Y }.
% 0.72/1.18 (87) {G0,W3,D2,L1,V0,M1} I { man( skol4, skol9 ) }.
% 0.72/1.18 (112) {G0,W3,D2,L1,V0,M1} I { wheel( skol4, skol20 ) }.
% 0.72/1.18 (114) {G0,W5,D2,L1,V0,M1} I { be( skol4, skol21, skol9, skol20 ) }.
% 0.72/1.18 (227) {G1,W3,D2,L1,V0,M1} R(23,87) { male( skol4, skol9 ) }.
% 0.72/1.18 (238) {G2,W3,D2,L1,V0,M1} R(62,227) { ! unisex( skol4, skol9 ) }.
% 0.72/1.18 (296) {G3,W3,D2,L1,V0,M1} R(37,238) { ! object( skol4, skol9 ) }.
% 0.72/1.18 (373) {G1,W3,D2,L1,V0,M1} R(47,112) { device( skol4, skol20 ) }.
% 0.72/1.18 (374) {G2,W3,D2,L1,V0,M1} R(373,46) { instrumentality( skol4, skol20 ) }.
% 0.72/1.18 (375) {G3,W3,D2,L1,V0,M1} R(374,45) { artifact( skol4, skol20 ) }.
% 0.72/1.18 (376) {G4,W3,D2,L1,V0,M1} R(375,44) { object( skol4, skol20 ) }.
% 0.72/1.18 (3681) {G1,W3,D2,L1,V0,M1} R(84,114) { skol20 ==> skol9 }.
% 0.72/1.18 (4592) {G5,W0,D0,L0,V0,M0} S(376);d(3681);r(296) { }.
% 0.72/1.18
% 0.72/1.18
% 0.72/1.18 % SZS output end Refutation
% 0.72/1.18 found a proof!
% 0.72/1.18
% 0.72/1.18
% 0.72/1.18 Unprocessed initial clauses:
% 0.72/1.18
% 0.72/1.18 (4594) {G0,W6,D2,L2,V2,M2} { ! jules_forename( X, Y ), forename( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 (4595) {G0,W6,D2,L2,V2,M2} { ! forename( X, Y ), relname( X, Y ) }.
% 0.72/1.18 (4596) {G0,W6,D2,L2,V2,M2} { ! furniture( X, Y ), instrumentality( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 (4597) {G0,W6,D2,L2,V2,M2} { ! seat( X, Y ), furniture( X, Y ) }.
% 0.72/1.18 (4598) {G0,W6,D2,L2,V2,M2} { ! frontseat( X, Y ), seat( X, Y ) }.
% 0.72/1.18 (4599) {G0,W6,D2,L2,V2,M2} { ! location( X, Y ), object( X, Y ) }.
% 0.72/1.18 (4600) {G0,W6,D2,L2,V2,M2} { ! city( X, Y ), location( X, Y ) }.
% 0.72/1.18 (4601) {G0,W6,D2,L2,V2,M2} { ! hollywood_placename( X, Y ), placename( X,
% 0.72/1.18 Y ) }.
% 0.72/1.18 (4602) {G0,W6,D2,L2,V2,M2} { ! abstraction( X, Y ), unisex( X, Y ) }.
% 0.72/1.18 (4603) {G0,W6,D2,L2,V2,M2} { ! abstraction( X, Y ), general( X, Y ) }.
% 0.72/1.18 (4604) {G0,W6,D2,L2,V2,M2} { ! abstraction( X, Y ), nonhuman( X, Y ) }.
% 0.72/1.18 (4605) {G0,W6,D2,L2,V2,M2} { ! abstraction( X, Y ), thing( X, Y ) }.
% 0.72/1.18 (4606) {G0,W6,D2,L2,V2,M2} { ! relation( X, Y ), abstraction( X, Y ) }.
% 0.72/1.18 (4607) {G0,W6,D2,L2,V2,M2} { ! relname( X, Y ), relation( X, Y ) }.
% 0.72/1.18 (4608) {G0,W6,D2,L2,V2,M2} { ! placename( X, Y ), relname( X, Y ) }.
% 0.72/1.18 (4609) {G0,W6,D2,L2,V2,M2} { ! transport( X, Y ), instrumentality( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 (4610) {G0,W6,D2,L2,V2,M2} { ! vehicle( X, Y ), transport( X, Y ) }.
% 0.72/1.18 (4611) {G0,W6,D2,L2,V2,M2} { ! car( X, Y ), vehicle( X, Y ) }.
% 0.72/1.18 (4612) {G0,W6,D2,L2,V2,M2} { ! chevy( X, Y ), car( X, Y ) }.
% 0.72/1.18 (4613) {G0,W6,D2,L2,V2,M2} { ! way( X, Y ), artifact( X, Y ) }.
% 0.72/1.18 (4614) {G0,W6,D2,L2,V2,M2} { ! street( X, Y ), way( X, Y ) }.
% 0.72/1.18 (4615) {G0,W6,D2,L2,V2,M2} { ! barrel( X, Y ), event( X, Y ) }.
% 0.72/1.18 (4616) {G0,W6,D2,L2,V2,M2} { ! two( X, Y ), group( X, Y ) }.
% 0.72/1.18 (4617) {G0,W6,D2,L2,V2,M2} { ! man( X, Y ), male( X, Y ) }.
% 0.72/1.18 (4618) {G0,W6,D2,L2,V2,M2} { ! human_person( X, Y ), animate( X, Y ) }.
% 0.72/1.18 (4619) {G0,W6,D2,L2,V2,M2} { ! human_person( X, Y ), human( X, Y ) }.
% 0.72/1.18 (4620) {G0,W6,D2,L2,V2,M2} { ! organism( X, Y ), living( X, Y ) }.
% 0.72/1.18 (4621) {G0,W6,D2,L2,V2,M2} { ! organism( X, Y ), impartial( X, Y ) }.
% 0.72/1.18 (4622) {G0,W6,D2,L2,V2,M2} { ! organism( X, Y ), entity( X, Y ) }.
% 0.72/1.18 (4623) {G0,W6,D2,L2,V2,M2} { ! human_person( X, Y ), organism( X, Y ) }.
% 0.72/1.18 (4624) {G0,W6,D2,L2,V2,M2} { ! man( X, Y ), human_person( X, Y ) }.
% 0.72/1.18 (4625) {G0,W6,D2,L2,V2,M2} { ! fellow( X, Y ), man( X, Y ) }.
% 0.72/1.18 (4626) {G0,W6,D2,L2,V2,M2} { ! wear( X, Y ), event( X, Y ) }.
% 0.72/1.18 (4627) {G0,W6,D2,L2,V2,M2} { ! set( X, Y ), multiple( X, Y ) }.
% 0.72/1.18 (4628) {G0,W6,D2,L2,V2,M2} { ! group( X, Y ), set( X, Y ) }.
% 0.72/1.18 (4629) {G0,W6,D2,L2,V2,M2} { ! clothes( X, Y ), artifact( X, Y ) }.
% 0.72/1.18 (4630) {G0,W6,D2,L2,V2,M2} { ! coat( X, Y ), clothes( X, Y ) }.
% 0.72/1.18 (4631) {G0,W6,D2,L2,V2,M2} { ! object( X, Y ), unisex( X, Y ) }.
% 0.72/1.18 (4632) {G0,W6,D2,L2,V2,M2} { ! object( X, Y ), impartial( X, Y ) }.
% 0.72/1.18 (4633) {G0,W6,D2,L2,V2,M2} { ! object( X, Y ), nonliving( X, Y ) }.
% 0.72/1.18 (4634) {G0,W6,D2,L2,V2,M2} { ! entity( X, Y ), existent( X, Y ) }.
% 0.72/1.18 (4635) {G0,W6,D2,L2,V2,M2} { ! entity( X, Y ), specific( X, Y ) }.
% 0.72/1.18 (4636) {G0,W6,D2,L2,V2,M2} { ! entity( X, Y ), thing( X, Y ) }.
% 0.72/1.18 (4637) {G0,W6,D2,L2,V2,M2} { ! object( X, Y ), entity( X, Y ) }.
% 0.72/1.18 (4638) {G0,W6,D2,L2,V2,M2} { ! artifact( X, Y ), object( X, Y ) }.
% 0.72/1.18 (4639) {G0,W6,D2,L2,V2,M2} { ! instrumentality( X, Y ), artifact( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 (4640) {G0,W6,D2,L2,V2,M2} { ! device( X, Y ), instrumentality( X, Y ) }.
% 0.72/1.18 (4641) {G0,W6,D2,L2,V2,M2} { ! wheel( X, Y ), device( X, Y ) }.
% 0.72/1.18 (4642) {G0,W6,D2,L2,V2,M2} { ! event( X, Y ), eventuality( X, Y ) }.
% 0.72/1.18 (4643) {G0,W6,D2,L2,V2,M2} { ! state( X, Y ), event( X, Y ) }.
% 0.72/1.18 (4644) {G0,W6,D2,L2,V2,M2} { ! eventuality( X, Y ), unisex( X, Y ) }.
% 0.72/1.18 (4645) {G0,W6,D2,L2,V2,M2} { ! eventuality( X, Y ), nonexistent( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 (4646) {G0,W6,D2,L2,V2,M2} { ! eventuality( X, Y ), specific( X, Y ) }.
% 0.72/1.18 (4647) {G0,W6,D2,L2,V2,M2} { ! thing( X, Y ), singleton( X, Y ) }.
% 0.72/1.18 (4648) {G0,W6,D2,L2,V2,M2} { ! eventuality( X, Y ), thing( X, Y ) }.
% 0.72/1.18 (4649) {G0,W6,D2,L2,V2,M2} { ! state( X, Y ), eventuality( X, Y ) }.
% 0.72/1.18 (4650) {G0,W6,D2,L2,V2,M2} { ! animate( X, Y ), ! nonliving( X, Y ) }.
% 0.72/1.18 (4651) {G0,W6,D2,L2,V2,M2} { ! existent( X, Y ), ! nonexistent( X, Y ) }.
% 0.72/1.18 (4652) {G0,W6,D2,L2,V2,M2} { ! nonhuman( X, Y ), ! human( X, Y ) }.
% 0.72/1.18 (4653) {G0,W6,D2,L2,V2,M2} { ! nonliving( X, Y ), ! living( X, Y ) }.
% 0.72/1.18 (4654) {G0,W6,D2,L2,V2,M2} { ! singleton( X, Y ), ! multiple( X, Y ) }.
% 0.72/1.18 (4655) {G0,W6,D2,L2,V2,M2} { ! specific( X, Y ), ! general( X, Y ) }.
% 0.72/1.18 (4656) {G0,W6,D2,L2,V2,M2} { ! unisex( X, Y ), ! male( X, Y ) }.
% 0.72/1.18 (4657) {G0,W6,D2,L2,V2,M2} { ! white( X, Y ), ! black( X, Y ) }.
% 0.72/1.18 (4658) {G0,W6,D2,L2,V2,M2} { ! young( X, Y ), ! old( X, Y ) }.
% 0.72/1.18 (4659) {G0,W20,D2,L6,V4,M6} { ! entity( X, Y ), ! forename( X, Z ), ! of(
% 0.72/1.18 X, Z, Y ), ! forename( X, T ), T = Z, ! of( X, T, Y ) }.
% 0.72/1.18 (4660) {G0,W20,D2,L6,V4,M6} { ! entity( X, Y ), ! placename( X, Z ), ! of
% 0.72/1.18 ( X, Z, Y ), ! placename( X, T ), T = Z, ! of( X, T, Y ) }.
% 0.72/1.18 (4661) {G0,W9,D3,L2,V2,M2} { ! two( X, Y ), member( X, skol1( X, Y ), Y )
% 0.72/1.18 }.
% 0.72/1.18 (4662) {G0,W9,D3,L2,V2,M2} { ! two( X, Y ), alpha1( X, Y, skol1( X, Y ) )
% 0.72/1.18 }.
% 0.72/1.18 (4663) {G0,W11,D2,L3,V3,M3} { ! member( X, Z, Y ), ! alpha1( X, Y, Z ),
% 0.72/1.18 two( X, Y ) }.
% 0.72/1.18 (4664) {G0,W11,D3,L2,V4,M2} { ! alpha1( X, Y, Z ), member( X, skol2( X, Y
% 0.72/1.18 , T ), Y ) }.
% 0.72/1.18 (4665) {G0,W12,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), alpha3( X, Y, Z, skol2
% 0.72/1.18 ( X, Y, Z ) ) }.
% 0.72/1.18 (4666) {G0,W13,D2,L3,V4,M3} { ! member( X, T, Y ), ! alpha3( X, Y, Z, T )
% 0.72/1.18 , alpha1( X, Y, Z ) }.
% 0.72/1.18 (4667) {G0,W8,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), ! T = Z }.
% 0.72/1.18 (4668) {G0,W10,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), alpha4( X, Y, Z, T )
% 0.72/1.18 }.
% 0.72/1.18 (4669) {G0,W13,D2,L3,V4,M3} { T = Z, ! alpha4( X, Y, Z, T ), alpha3( X, Y
% 0.72/1.18 , Z, T ) }.
% 0.72/1.18 (4670) {G0,W13,D2,L3,V5,M3} { ! alpha4( X, Y, Z, T ), ! member( X, U, Y )
% 0.72/1.18 , alpha2( Z, T, U ) }.
% 0.72/1.18 (4671) {G0,W13,D3,L2,V6,M2} { ! alpha2( Z, T, skol3( U, W, Z, T ) ),
% 0.72/1.18 alpha4( X, Y, Z, T ) }.
% 0.72/1.18 (4672) {G0,W13,D3,L2,V4,M2} { member( X, skol3( X, Y, Z, T ), Y ), alpha4
% 0.72/1.18 ( X, Y, Z, T ) }.
% 0.72/1.18 (4673) {G0,W10,D2,L3,V3,M3} { ! alpha2( X, Y, Z ), Z = Y, Z = X }.
% 0.72/1.18 (4674) {G0,W7,D2,L2,V3,M2} { ! Z = Y, alpha2( X, Y, Z ) }.
% 0.72/1.18 (4675) {G0,W7,D2,L2,V3,M2} { ! Z = X, alpha2( X, Y, Z ) }.
% 0.72/1.18 (4676) {G0,W14,D2,L4,V4,M4} { ! nonreflexive( Z, T ), ! agent( Z, T, X ),
% 0.72/1.18 ! patient( Z, T, Y ), ! X = Y }.
% 0.72/1.18 (4677) {G0,W4,D2,L1,V2,M1} { ! member( X, Y, Y ) }.
% 0.72/1.18 (4678) {G0,W8,D2,L2,V4,M2} { ! be( Z, T, X, Y ), X = Y }.
% 0.72/1.18 (4679) {G0,W2,D2,L1,V0,M1} { actual_world( skol4 ) }.
% 0.72/1.18 (4680) {G0,W4,D2,L1,V0,M1} { of( skol4, skol11, skol9 ) }.
% 0.72/1.18 (4681) {G0,W3,D2,L1,V0,M1} { man( skol4, skol9 ) }.
% 0.72/1.18 (4682) {G0,W3,D2,L1,V0,M1} { jules_forename( skol4, skol11 ) }.
% 0.72/1.18 (4683) {G0,W3,D2,L1,V0,M1} { forename( skol4, skol11 ) }.
% 0.72/1.18 (4684) {G0,W3,D2,L1,V0,M1} { frontseat( skol4, skol12 ) }.
% 0.72/1.18 (4685) {G0,W3,D2,L1,V0,M1} { chevy( skol4, skol13 ) }.
% 0.72/1.18 (4686) {G0,W3,D2,L1,V0,M1} { white( skol4, skol13 ) }.
% 0.72/1.18 (4687) {G0,W3,D2,L1,V0,M1} { dirty( skol4, skol13 ) }.
% 0.72/1.18 (4688) {G0,W3,D2,L1,V0,M1} { old( skol4, skol13 ) }.
% 0.72/1.18 (4689) {G0,W4,D2,L1,V0,M1} { of( skol4, skol14, skol15 ) }.
% 0.72/1.18 (4690) {G0,W3,D2,L1,V0,M1} { city( skol4, skol15 ) }.
% 0.72/1.18 (4691) {G0,W3,D2,L1,V0,M1} { hollywood_placename( skol4, skol14 ) }.
% 0.72/1.18 (4692) {G0,W3,D2,L1,V0,M1} { placename( skol4, skol14 ) }.
% 0.72/1.18 (4693) {G0,W3,D2,L1,V0,M1} { street( skol4, skol15 ) }.
% 0.72/1.18 (4694) {G0,W3,D2,L1,V0,M1} { lonely( skol4, skol15 ) }.
% 0.72/1.18 (4695) {G0,W3,D2,L1,V0,M1} { event( skol4, skol16 ) }.
% 0.72/1.18 (4696) {G0,W4,D2,L1,V0,M1} { agent( skol4, skol16, skol13 ) }.
% 0.72/1.18 (4697) {G0,W3,D2,L1,V0,M1} { present( skol4, skol16 ) }.
% 0.72/1.18 (4698) {G0,W3,D2,L1,V0,M1} { barrel( skol4, skol16 ) }.
% 0.72/1.18 (4699) {G0,W4,D2,L1,V0,M1} { down( skol4, skol16, skol15 ) }.
% 0.72/1.18 (4700) {G0,W4,D2,L1,V0,M1} { in( skol4, skol16, skol15 ) }.
% 0.72/1.18 (4701) {G0,W4,D2,L1,V0,M1} { alpha7( skol4, skol12, skol17 ) }.
% 0.72/1.18 (4702) {G0,W13,D3,L3,V4,M3} { ! member( skol4, X, skol18 ), ! member(
% 0.72/1.18 skol4, Y, skol17 ), wear( skol4, skol19( Z, T ) ) }.
% 0.72/1.18 (4703) {G0,W15,D3,L3,V2,M3} { ! member( skol4, X, skol18 ), ! member(
% 0.72/1.18 skol4, Y, skol17 ), alpha11( skol4, X, Y, skol19( X, Y ) ) }.
% 0.72/1.18 (4704) {G0,W3,D2,L1,V0,M1} { group( skol4, skol18 ) }.
% 0.72/1.18 (4705) {G0,W3,D2,L1,V0,M1} { alpha6( skol4, skol18 ) }.
% 0.72/1.18 (4706) {G0,W3,D2,L1,V0,M1} { wheel( skol4, skol20 ) }.
% 0.72/1.18 (4707) {G0,W3,D2,L1,V0,M1} { state( skol4, skol21 ) }.
% 0.72/1.18 (4708) {G0,W5,D2,L1,V0,M1} { be( skol4, skol21, skol9, skol20 ) }.
% 0.72/1.18 (4709) {G0,W4,D2,L1,V0,M1} { behind( skol4, skol20, skol20 ) }.
% 0.72/1.18 (4710) {G0,W10,D2,L2,V4,M2} { ! alpha11( X, Y, Z, T ), alpha13( X, Y, Z, T
% 0.72/1.18 ) }.
% 0.72/1.18 (4711) {G0,W8,D2,L2,V4,M2} { ! alpha11( X, Y, Z, T ), nonreflexive( X, T )
% 0.72/1.18 }.
% 0.72/1.18 (4712) {G0,W13,D2,L3,V4,M3} { ! alpha13( X, Y, Z, T ), ! nonreflexive( X,
% 0.72/1.18 T ), alpha11( X, Y, Z, T ) }.
% 0.72/1.18 (4713) {G0,W9,D2,L2,V4,M2} { ! alpha13( X, Y, Z, T ), alpha9( X, Z, T )
% 0.72/1.18 }.
% 0.72/1.18 (4714) {G0,W9,D2,L2,V4,M2} { ! alpha13( X, Y, Z, T ), patient( X, T, Y )
% 0.72/1.18 }.
% 0.72/1.18 (4715) {G0,W8,D2,L2,V4,M2} { ! alpha13( X, Y, Z, T ), present( X, T ) }.
% 0.72/1.18 (4716) {G0,W16,D2,L4,V4,M4} { ! alpha9( X, Z, T ), ! patient( X, T, Y ), !
% 0.72/1.18 present( X, T ), alpha13( X, Y, Z, T ) }.
% 0.72/1.18 (4717) {G0,W7,D2,L2,V3,M2} { ! alpha9( X, Y, Z ), event( X, Z ) }.
% 0.72/1.18 (4718) {G0,W8,D2,L2,V3,M2} { ! alpha9( X, Y, Z ), agent( X, Z, Y ) }.
% 0.72/1.18 (4719) {G0,W11,D2,L3,V3,M3} { ! event( X, Z ), ! agent( X, Z, Y ), alpha9
% 0.72/1.18 ( X, Y, Z ) }.
% 0.72/1.18 (4720) {G0,W8,D2,L2,V3,M2} { ! alpha7( X, Y, Z ), alpha10( X, Y, Z ) }.
% 0.72/1.18 (4721) {G0,W7,D2,L2,V3,M2} { ! alpha7( X, Y, Z ), alpha5( X, Z ) }.
% 0.72/1.18 (4722) {G0,W11,D2,L3,V3,M3} { ! alpha10( X, Y, Z ), ! alpha5( X, Z ),
% 0.72/1.18 alpha7( X, Y, Z ) }.
% 0.72/1.18 (4723) {G0,W8,D2,L2,V3,M2} { ! alpha10( X, Y, Z ), alpha12( X, Y, Z ) }.
% 0.72/1.18 (4724) {G0,W7,D2,L2,V3,M2} { ! alpha10( X, Y, Z ), group( X, Z ) }.
% 0.72/1.18 (4725) {G0,W11,D2,L3,V3,M3} { ! alpha12( X, Y, Z ), ! group( X, Z ),
% 0.72/1.18 alpha10( X, Y, Z ) }.
% 0.72/1.18 (4726) {G0,W8,D2,L2,V3,M2} { ! alpha12( X, Y, Z ), alpha14( X, Y, Z ) }.
% 0.72/1.18 (4727) {G0,W7,D2,L2,V3,M2} { ! alpha12( X, Y, Z ), two( X, Z ) }.
% 0.72/1.18 (4728) {G0,W11,D2,L3,V3,M3} { ! alpha14( X, Y, Z ), ! two( X, Z ), alpha12
% 0.72/1.18 ( X, Y, Z ) }.
% 0.72/1.18 (4729) {G0,W12,D2,L3,V4,M3} { ! alpha14( X, Y, Z ), ! member( X, T, Z ),
% 0.72/1.18 alpha15( X, Y, T ) }.
% 0.72/1.18 (4730) {G0,W11,D3,L2,V4,M2} { member( X, skol5( X, T, Z ), Z ), alpha14( X
% 0.72/1.18 , Y, Z ) }.
% 0.72/1.18 (4731) {G0,W11,D3,L2,V3,M2} { ! alpha15( X, Y, skol5( X, Y, Z ) ), alpha14
% 0.72/1.18 ( X, Y, Z ) }.
% 0.72/1.18 (4732) {G0,W10,D3,L2,V5,M2} { ! alpha15( X, Y, Z ), state( X, skol6( X, T
% 0.72/1.18 , U ) ) }.
% 0.72/1.18 (4733) {G0,W11,D3,L2,V4,M2} { ! alpha15( X, Y, Z ), in( X, skol10( X, Y, T
% 0.72/1.18 ), Y ) }.
% 0.72/1.18 (4734) {G0,W15,D3,L2,V3,M2} { ! alpha15( X, Y, Z ), be( X, skol6( X, Y, Z
% 0.72/1.18 ), Z, skol10( X, Y, Z ) ) }.
% 0.72/1.18 (4735) {G0,W16,D2,L4,V5,M4} { ! state( X, T ), ! be( X, T, Z, U ), ! in( X
% 0.72/1.18 , U, Y ), alpha15( X, Y, Z ) }.
% 0.72/1.18 (4736) {G0,W10,D2,L3,V3,M3} { ! alpha6( X, Y ), ! member( X, Z, Y ),
% 0.72/1.18 alpha8( X, Z ) }.
% 0.72/1.18 (4737) {G0,W8,D3,L2,V3,M2} { ! alpha8( X, skol7( X, Z ) ), alpha6( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 (4738) {G0,W9,D3,L2,V2,M2} { member( X, skol7( X, Y ), Y ), alpha6( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 (4739) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), coat( X, Y ) }.
% 0.72/1.18 (4740) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), black( X, Y ) }.
% 0.72/1.18 (4741) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), cheap( X, Y ) }.
% 0.72/1.18 (4742) {G0,W12,D2,L4,V2,M4} { ! coat( X, Y ), ! black( X, Y ), ! cheap( X
% 0.72/1.18 , Y ), alpha8( X, Y ) }.
% 0.72/1.18 (4743) {G0,W10,D2,L3,V3,M3} { ! alpha5( X, Y ), ! member( X, Z, Y ),
% 0.72/1.18 fellow( X, Z ) }.
% 0.72/1.18 (4744) {G0,W10,D2,L3,V3,M3} { ! alpha5( X, Y ), ! member( X, Z, Y ), young
% 0.72/1.18 ( X, Z ) }.
% 0.72/1.18 (4745) {G0,W13,D3,L3,V3,M3} { ! fellow( X, skol8( X, Z ) ), ! young( X,
% 0.72/1.18 skol8( X, Z ) ), alpha5( X, Y ) }.
% 0.72/1.18 (4746) {G0,W9,D3,L2,V2,M2} { member( X, skol8( X, Y ), Y ), alpha5( X, Y )
% 0.72/1.18 }.
% 0.72/1.18
% 0.72/1.18
% 0.72/1.18 Total Proof:
% 0.72/1.18
% 0.72/1.18 subsumption: (23) {G0,W6,D2,L2,V2,M2} I { ! man( X, Y ), male( X, Y ) }.
% 0.72/1.18 parent0: (4617) {G0,W6,D2,L2,V2,M2} { ! man( X, Y ), male( X, Y ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := X
% 0.72/1.18 Y := Y
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 1 ==> 1
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (37) {G0,W6,D2,L2,V2,M2} I { ! object( X, Y ), unisex( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 parent0: (4631) {G0,W6,D2,L2,V2,M2} { ! object( X, Y ), unisex( X, Y ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := X
% 0.72/1.18 Y := Y
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 1 ==> 1
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (44) {G0,W6,D2,L2,V2,M2} I { ! artifact( X, Y ), object( X, Y
% 0.72/1.18 ) }.
% 0.72/1.18 parent0: (4638) {G0,W6,D2,L2,V2,M2} { ! artifact( X, Y ), object( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := X
% 0.72/1.18 Y := Y
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 1 ==> 1
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (45) {G0,W6,D2,L2,V2,M2} I { ! instrumentality( X, Y ),
% 0.72/1.18 artifact( X, Y ) }.
% 0.72/1.18 parent0: (4639) {G0,W6,D2,L2,V2,M2} { ! instrumentality( X, Y ), artifact
% 0.72/1.18 ( X, Y ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := X
% 0.72/1.18 Y := Y
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 1 ==> 1
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (46) {G0,W6,D2,L2,V2,M2} I { ! device( X, Y ), instrumentality
% 0.72/1.18 ( X, Y ) }.
% 0.72/1.18 parent0: (4640) {G0,W6,D2,L2,V2,M2} { ! device( X, Y ), instrumentality( X
% 0.72/1.18 , Y ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := X
% 0.72/1.18 Y := Y
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 1 ==> 1
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (47) {G0,W6,D2,L2,V2,M2} I { ! wheel( X, Y ), device( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 parent0: (4641) {G0,W6,D2,L2,V2,M2} { ! wheel( X, Y ), device( X, Y ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := X
% 0.72/1.18 Y := Y
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 1 ==> 1
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (62) {G0,W6,D2,L2,V2,M2} I { ! unisex( X, Y ), ! male( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 parent0: (4656) {G0,W6,D2,L2,V2,M2} { ! unisex( X, Y ), ! male( X, Y ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := X
% 0.72/1.18 Y := Y
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 1 ==> 1
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (84) {G0,W8,D2,L2,V4,M2} I { ! be( Z, T, X, Y ), X = Y }.
% 0.72/1.18 parent0: (4678) {G0,W8,D2,L2,V4,M2} { ! be( Z, T, X, Y ), X = Y }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := X
% 0.72/1.18 Y := Y
% 0.72/1.18 Z := Z
% 0.72/1.18 T := T
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 1 ==> 1
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (87) {G0,W3,D2,L1,V0,M1} I { man( skol4, skol9 ) }.
% 0.72/1.18 parent0: (4681) {G0,W3,D2,L1,V0,M1} { man( skol4, skol9 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (112) {G0,W3,D2,L1,V0,M1} I { wheel( skol4, skol20 ) }.
% 0.72/1.18 parent0: (4706) {G0,W3,D2,L1,V0,M1} { wheel( skol4, skol20 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (114) {G0,W5,D2,L1,V0,M1} I { be( skol4, skol21, skol9, skol20
% 0.72/1.18 ) }.
% 0.72/1.18 parent0: (4708) {G0,W5,D2,L1,V0,M1} { be( skol4, skol21, skol9, skol20 )
% 0.72/1.18 }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 resolution: (4815) {G1,W3,D2,L1,V0,M1} { male( skol4, skol9 ) }.
% 0.72/1.18 parent0[0]: (23) {G0,W6,D2,L2,V2,M2} I { ! man( X, Y ), male( X, Y ) }.
% 0.72/1.18 parent1[0]: (87) {G0,W3,D2,L1,V0,M1} I { man( skol4, skol9 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := skol4
% 0.72/1.18 Y := skol9
% 0.72/1.18 end
% 0.72/1.18 substitution1:
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (227) {G1,W3,D2,L1,V0,M1} R(23,87) { male( skol4, skol9 ) }.
% 0.72/1.18 parent0: (4815) {G1,W3,D2,L1,V0,M1} { male( skol4, skol9 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 resolution: (4816) {G1,W3,D2,L1,V0,M1} { ! unisex( skol4, skol9 ) }.
% 0.72/1.18 parent0[1]: (62) {G0,W6,D2,L2,V2,M2} I { ! unisex( X, Y ), ! male( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 parent1[0]: (227) {G1,W3,D2,L1,V0,M1} R(23,87) { male( skol4, skol9 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := skol4
% 0.72/1.18 Y := skol9
% 0.72/1.18 end
% 0.72/1.18 substitution1:
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (238) {G2,W3,D2,L1,V0,M1} R(62,227) { ! unisex( skol4, skol9 )
% 0.72/1.18 }.
% 0.72/1.18 parent0: (4816) {G1,W3,D2,L1,V0,M1} { ! unisex( skol4, skol9 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 resolution: (4817) {G1,W3,D2,L1,V0,M1} { ! object( skol4, skol9 ) }.
% 0.72/1.18 parent0[0]: (238) {G2,W3,D2,L1,V0,M1} R(62,227) { ! unisex( skol4, skol9 )
% 0.72/1.18 }.
% 0.72/1.18 parent1[1]: (37) {G0,W6,D2,L2,V2,M2} I { ! object( X, Y ), unisex( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 substitution1:
% 0.72/1.18 X := skol4
% 0.72/1.18 Y := skol9
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (296) {G3,W3,D2,L1,V0,M1} R(37,238) { ! object( skol4, skol9 )
% 0.72/1.18 }.
% 0.72/1.18 parent0: (4817) {G1,W3,D2,L1,V0,M1} { ! object( skol4, skol9 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 resolution: (4818) {G1,W3,D2,L1,V0,M1} { device( skol4, skol20 ) }.
% 0.72/1.18 parent0[0]: (47) {G0,W6,D2,L2,V2,M2} I { ! wheel( X, Y ), device( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 parent1[0]: (112) {G0,W3,D2,L1,V0,M1} I { wheel( skol4, skol20 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := skol4
% 0.72/1.18 Y := skol20
% 0.72/1.18 end
% 0.72/1.18 substitution1:
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (373) {G1,W3,D2,L1,V0,M1} R(47,112) { device( skol4, skol20 )
% 0.72/1.18 }.
% 0.72/1.18 parent0: (4818) {G1,W3,D2,L1,V0,M1} { device( skol4, skol20 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 resolution: (4819) {G1,W3,D2,L1,V0,M1} { instrumentality( skol4, skol20 )
% 0.72/1.18 }.
% 0.72/1.18 parent0[0]: (46) {G0,W6,D2,L2,V2,M2} I { ! device( X, Y ), instrumentality
% 0.72/1.18 ( X, Y ) }.
% 0.72/1.18 parent1[0]: (373) {G1,W3,D2,L1,V0,M1} R(47,112) { device( skol4, skol20 )
% 0.72/1.18 }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := skol4
% 0.72/1.18 Y := skol20
% 0.72/1.18 end
% 0.72/1.18 substitution1:
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (374) {G2,W3,D2,L1,V0,M1} R(373,46) { instrumentality( skol4,
% 0.72/1.18 skol20 ) }.
% 0.72/1.18 parent0: (4819) {G1,W3,D2,L1,V0,M1} { instrumentality( skol4, skol20 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 resolution: (4820) {G1,W3,D2,L1,V0,M1} { artifact( skol4, skol20 ) }.
% 0.72/1.18 parent0[0]: (45) {G0,W6,D2,L2,V2,M2} I { ! instrumentality( X, Y ),
% 0.72/1.18 artifact( X, Y ) }.
% 0.72/1.18 parent1[0]: (374) {G2,W3,D2,L1,V0,M1} R(373,46) { instrumentality( skol4,
% 0.72/1.18 skol20 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := skol4
% 0.72/1.18 Y := skol20
% 0.72/1.18 end
% 0.72/1.18 substitution1:
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (375) {G3,W3,D2,L1,V0,M1} R(374,45) { artifact( skol4, skol20
% 0.72/1.18 ) }.
% 0.72/1.18 parent0: (4820) {G1,W3,D2,L1,V0,M1} { artifact( skol4, skol20 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 resolution: (4821) {G1,W3,D2,L1,V0,M1} { object( skol4, skol20 ) }.
% 0.72/1.18 parent0[0]: (44) {G0,W6,D2,L2,V2,M2} I { ! artifact( X, Y ), object( X, Y )
% 0.72/1.18 }.
% 0.72/1.18 parent1[0]: (375) {G3,W3,D2,L1,V0,M1} R(374,45) { artifact( skol4, skol20 )
% 0.72/1.18 }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := skol4
% 0.72/1.18 Y := skol20
% 0.72/1.18 end
% 0.72/1.18 substitution1:
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (376) {G4,W3,D2,L1,V0,M1} R(375,44) { object( skol4, skol20 )
% 0.72/1.18 }.
% 0.72/1.18 parent0: (4821) {G1,W3,D2,L1,V0,M1} { object( skol4, skol20 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 eqswap: (4822) {G0,W8,D2,L2,V4,M2} { Y = X, ! be( Z, T, X, Y ) }.
% 0.72/1.18 parent0[1]: (84) {G0,W8,D2,L2,V4,M2} I { ! be( Z, T, X, Y ), X = Y }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := X
% 0.72/1.18 Y := Y
% 0.72/1.18 Z := Z
% 0.72/1.18 T := T
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 resolution: (4823) {G1,W3,D2,L1,V0,M1} { skol20 = skol9 }.
% 0.72/1.18 parent0[1]: (4822) {G0,W8,D2,L2,V4,M2} { Y = X, ! be( Z, T, X, Y ) }.
% 0.72/1.18 parent1[0]: (114) {G0,W5,D2,L1,V0,M1} I { be( skol4, skol21, skol9, skol20
% 0.72/1.18 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 X := skol9
% 0.72/1.18 Y := skol20
% 0.72/1.18 Z := skol4
% 0.72/1.18 T := skol21
% 0.72/1.18 end
% 0.72/1.18 substitution1:
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (3681) {G1,W3,D2,L1,V0,M1} R(84,114) { skol20 ==> skol9 }.
% 0.72/1.18 parent0: (4823) {G1,W3,D2,L1,V0,M1} { skol20 = skol9 }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 0 ==> 0
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 paramod: (4826) {G2,W3,D2,L1,V0,M1} { object( skol4, skol9 ) }.
% 0.72/1.18 parent0[0]: (3681) {G1,W3,D2,L1,V0,M1} R(84,114) { skol20 ==> skol9 }.
% 0.72/1.18 parent1[0; 2]: (376) {G4,W3,D2,L1,V0,M1} R(375,44) { object( skol4, skol20
% 0.72/1.18 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 substitution1:
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 resolution: (4827) {G3,W0,D0,L0,V0,M0} { }.
% 0.72/1.18 parent0[0]: (296) {G3,W3,D2,L1,V0,M1} R(37,238) { ! object( skol4, skol9 )
% 0.72/1.18 }.
% 0.72/1.18 parent1[0]: (4826) {G2,W3,D2,L1,V0,M1} { object( skol4, skol9 ) }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 substitution1:
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 subsumption: (4592) {G5,W0,D0,L0,V0,M0} S(376);d(3681);r(296) { }.
% 0.72/1.18 parent0: (4827) {G3,W0,D0,L0,V0,M0} { }.
% 0.72/1.18 substitution0:
% 0.72/1.18 end
% 0.72/1.18 permutation0:
% 0.72/1.18 end
% 0.72/1.18
% 0.72/1.18 Proof check complete!
% 0.72/1.18
% 0.72/1.18 Memory use:
% 0.72/1.18
% 0.72/1.18 space for terms: 56494
% 0.72/1.18 space for clauses: 204754
% 0.72/1.18
% 0.72/1.18
% 0.72/1.18 clauses generated: 7117
% 0.72/1.18 clauses kept: 4593
% 0.72/1.18 clauses selected: 406
% 0.72/1.18 clauses deleted: 14
% 0.72/1.18 clauses inuse deleted: 14
% 0.72/1.18
% 0.72/1.18 subsentry: 4919
% 0.72/1.18 literals s-matched: 3586
% 0.72/1.18 literals matched: 3586
% 0.72/1.18 full subsumption: 2265
% 0.72/1.18
% 0.72/1.18 checksum: -17165963
% 0.72/1.18
% 0.72/1.18
% 0.72/1.18 Bliksem ended
%------------------------------------------------------------------------------