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