%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NLP145+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n012.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:00 EDT 2022
% Result : Theorem 3.17s 3.54s
% Output : Refutation 3.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.10 % Problem : NLP145+1 : TPTP v8.1.0. Released v2.4.0.
% 0.05/0.11 % Command : bliksem %s
% 0.11/0.32 % Computer : n012.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % DateTime : Thu Jun 30 20:04:17 EDT 2022
% 0.11/0.32 % CPUTime :
% 0.68/1.06 *** allocated 10000 integers for termspace/termends
% 0.68/1.06 *** allocated 10000 integers for clauses
% 0.68/1.06 *** allocated 10000 integers for justifications
% 0.68/1.06 Bliksem 1.12
% 0.68/1.06
% 0.68/1.06
% 0.68/1.06 Automatic Strategy Selection
% 0.68/1.06
% 0.68/1.06
% 0.68/1.06 Clauses:
% 0.68/1.06
% 0.68/1.06 { ! furniture( X, Y ), instrumentality( X, Y ) }.
% 0.68/1.06 { ! seat( X, Y ), furniture( X, Y ) }.
% 0.68/1.06 { ! frontseat( X, Y ), seat( X, Y ) }.
% 0.68/1.06 { ! location( X, Y ), object( X, Y ) }.
% 0.68/1.06 { ! city( X, Y ), location( X, Y ) }.
% 0.68/1.06 { ! hollywood_placename( X, Y ), placename( X, Y ) }.
% 0.68/1.06 { ! abstraction( X, Y ), unisex( X, Y ) }.
% 0.68/1.06 { ! abstraction( X, Y ), general( X, Y ) }.
% 0.68/1.06 { ! abstraction( X, Y ), nonhuman( X, Y ) }.
% 0.68/1.06 { ! abstraction( X, Y ), thing( X, Y ) }.
% 0.68/1.06 { ! relation( X, Y ), abstraction( X, Y ) }.
% 0.68/1.06 { ! relname( X, Y ), relation( X, Y ) }.
% 0.68/1.06 { ! placename( X, Y ), relname( X, Y ) }.
% 0.68/1.06 { ! way( X, Y ), artifact( X, Y ) }.
% 0.68/1.06 { ! street( X, Y ), way( X, Y ) }.
% 0.68/1.06 { ! object( X, Y ), unisex( X, Y ) }.
% 0.68/1.06 { ! object( X, Y ), impartial( X, Y ) }.
% 0.68/1.06 { ! object( X, Y ), nonliving( X, Y ) }.
% 0.68/1.06 { ! object( X, Y ), entity( X, Y ) }.
% 0.68/1.06 { ! artifact( X, Y ), object( X, Y ) }.
% 0.68/1.06 { ! instrumentality( X, Y ), artifact( X, Y ) }.
% 0.68/1.06 { ! transport( X, Y ), instrumentality( X, Y ) }.
% 0.68/1.06 { ! vehicle( X, Y ), transport( X, Y ) }.
% 0.68/1.06 { ! car( X, Y ), vehicle( X, Y ) }.
% 0.68/1.06 { ! chevy( X, Y ), car( X, Y ) }.
% 0.68/1.06 { ! barrel( X, Y ), event( X, Y ) }.
% 0.68/1.06 { ! event( X, Y ), eventuality( X, Y ) }.
% 0.68/1.06 { ! state( X, Y ), event( X, Y ) }.
% 0.68/1.06 { ! eventuality( X, Y ), unisex( X, Y ) }.
% 0.68/1.06 { ! eventuality( X, Y ), nonexistent( X, Y ) }.
% 0.68/1.06 { ! eventuality( X, Y ), specific( X, Y ) }.
% 0.68/1.06 { ! eventuality( X, Y ), thing( X, Y ) }.
% 0.68/1.06 { ! state( X, Y ), eventuality( X, Y ) }.
% 0.68/1.06 { ! two( X, Y ), group( X, Y ) }.
% 0.68/1.06 { ! set( X, Y ), multiple( X, Y ) }.
% 0.68/1.06 { ! group( X, Y ), set( X, Y ) }.
% 0.68/1.06 { ! man( X, Y ), male( X, Y ) }.
% 0.68/1.06 { ! human_person( X, Y ), animate( X, Y ) }.
% 0.68/1.06 { ! human_person( X, Y ), human( X, Y ) }.
% 0.68/1.06 { ! organism( X, Y ), living( X, Y ) }.
% 0.68/1.06 { ! organism( X, Y ), impartial( X, Y ) }.
% 0.68/1.06 { ! entity( X, Y ), existent( X, Y ) }.
% 0.68/1.06 { ! entity( X, Y ), specific( X, Y ) }.
% 0.68/1.06 { ! thing( X, Y ), singleton( X, Y ) }.
% 0.68/1.06 { ! entity( X, Y ), thing( X, Y ) }.
% 0.68/1.06 { ! organism( X, Y ), entity( X, Y ) }.
% 0.68/1.06 { ! human_person( X, Y ), organism( X, Y ) }.
% 0.68/1.06 { ! man( X, Y ), human_person( X, Y ) }.
% 0.68/1.06 { ! fellow( X, Y ), man( X, Y ) }.
% 0.68/1.06 { ! animate( X, Y ), ! nonliving( X, Y ) }.
% 0.68/1.06 { ! existent( X, Y ), ! nonexistent( X, Y ) }.
% 0.68/1.06 { ! nonhuman( X, Y ), ! human( X, Y ) }.
% 0.68/1.06 { ! nonliving( X, Y ), ! living( X, Y ) }.
% 0.68/1.06 { ! singleton( X, Y ), ! multiple( X, Y ) }.
% 0.68/1.06 { ! specific( X, Y ), ! general( X, Y ) }.
% 0.68/1.06 { ! unisex( X, Y ), ! male( X, Y ) }.
% 0.68/1.06 { ! young( X, Y ), ! old( X, Y ) }.
% 0.68/1.06 { ! entity( X, Y ), ! placename( X, Z ), ! of( X, Z, Y ), ! placename( X, T
% 0.68/1.06 ), T = Z, ! of( X, T, Y ) }.
% 0.68/1.06 { ! be( Z, T, X, Y ), X = Y }.
% 0.68/1.06 { ! two( X, Y ), member( X, skol1( X, Y ), Y ) }.
% 0.68/1.06 { ! two( X, Y ), alpha1( X, Y, skol1( X, Y ) ) }.
% 0.68/1.06 { ! member( X, Z, Y ), ! alpha1( X, Y, Z ), two( X, Y ) }.
% 0.68/1.06 { ! alpha1( X, Y, Z ), member( X, skol2( X, Y, T ), Y ) }.
% 0.68/1.06 { ! alpha1( X, Y, Z ), alpha3( X, Y, Z, skol2( X, Y, Z ) ) }.
% 0.68/1.06 { ! member( X, T, Y ), ! alpha3( X, Y, Z, T ), alpha1( X, Y, Z ) }.
% 0.68/1.06 { ! alpha3( X, Y, Z, T ), ! T = Z }.
% 0.68/1.06 { ! alpha3( X, Y, Z, T ), alpha4( X, Y, Z, T ) }.
% 0.68/1.06 { T = Z, ! alpha4( X, Y, Z, T ), alpha3( X, Y, Z, T ) }.
% 0.68/1.06 { ! alpha4( X, Y, Z, T ), ! member( X, U, Y ), alpha2( Z, T, U ) }.
% 0.68/1.06 { ! alpha2( Z, T, skol3( U, W, Z, T ) ), alpha4( X, Y, Z, T ) }.
% 0.68/1.06 { member( X, skol3( X, Y, Z, T ), Y ), alpha4( X, Y, Z, T ) }.
% 0.68/1.06 { ! alpha2( X, Y, Z ), Z = Y, Z = X }.
% 0.68/1.06 { ! Z = Y, alpha2( X, Y, Z ) }.
% 0.68/1.06 { ! Z = X, alpha2( X, Y, Z ) }.
% 0.68/1.06 { ! member( X, Y, Y ) }.
% 0.68/1.06 { actual_world( skol4 ) }.
% 0.68/1.06 { of( skol4, skol8, skol7 ) }.
% 0.68/1.06 { city( skol4, skol7 ) }.
% 0.68/1.06 { hollywood_placename( skol4, skol8 ) }.
% 0.68/1.06 { placename( skol4, skol8 ) }.
% 0.68/1.06 { chevy( skol4, skol9 ) }.
% 0.68/1.06 { white( skol4, skol9 ) }.
% 0.68/1.06 { dirty( skol4, skol9 ) }.
% 0.68/1.06 { old( skol4, skol9 ) }.
% 0.68/1.06 { street( skol4, skol10 ) }.
% 0.68/1.06 { lonely( skol4, skol10 ) }.
% 0.68/1.06 { event( skol4, skol11 ) }.
% 0.68/1.06 { agent( skol4, skol11, skol9 ) }.
% 0.68/1.06 { present( skol4, skol11 ) }.
% 0.68/1.06 { barrel( skol4, skol11 ) }.
% 0.68/1.06 { down( skol4, skol11, skol10 ) }.
% 0.68/1.06 { in( skol4, skol11, skol7 ) }.
% 0.68/1.06 { ! member( skol4, X, skol12 ), alpha5( skol4, X ) }.
% 0.68/1.06 { two( skol4, skol12 ) }.
% 0.68/1.06 { group( skol4, skol12 ) }.
% 2.18/2.57 { ! member( skol4, X, skol12 ), fellow( skol4, X ) }.
% 2.18/2.57 { ! member( skol4, X, skol12 ), young( skol4, X ) }.
% 2.18/2.57 { ! alpha5( X, Y ), frontseat( X, skol5( X, Z ) ) }.
% 2.18/2.57 { ! alpha5( X, Y ), alpha6( X, Y, skol5( X, Y ) ) }.
% 2.18/2.57 { ! frontseat( X, Z ), ! alpha6( X, Y, Z ), alpha5( X, Y ) }.
% 2.18/2.57 { ! alpha6( X, Y, Z ), state( X, skol6( X, T, U ) ) }.
% 2.18/2.57 { ! alpha6( X, Y, Z ), in( X, Z, Z ) }.
% 2.18/2.57 { ! alpha6( X, Y, Z ), be( X, skol6( X, Y, Z ), Y, Z ) }.
% 2.18/2.57 { ! state( X, T ), ! be( X, T, Y, Z ), ! in( X, Z, Z ), alpha6( X, Y, Z ) }
% 2.18/2.57 .
% 2.18/2.57
% 2.18/2.57 percentage equality = 0.040000, percentage horn = 0.971154
% 2.18/2.57 This is a problem with some equality
% 2.18/2.57
% 2.18/2.57
% 2.18/2.57
% 2.18/2.57 Options Used:
% 2.18/2.57
% 2.18/2.57 useres = 1
% 2.18/2.57 useparamod = 1
% 2.18/2.57 useeqrefl = 1
% 2.18/2.57 useeqfact = 1
% 2.18/2.57 usefactor = 1
% 2.18/2.57 usesimpsplitting = 0
% 2.18/2.57 usesimpdemod = 5
% 2.18/2.57 usesimpres = 3
% 2.18/2.57
% 2.18/2.57 resimpinuse = 1000
% 2.18/2.57 resimpclauses = 20000
% 2.18/2.57 substype = eqrewr
% 2.18/2.57 backwardsubs = 1
% 2.18/2.57 selectoldest = 5
% 2.18/2.57
% 2.18/2.57 litorderings [0] = split
% 2.18/2.57 litorderings [1] = extend the termordering, first sorting on arguments
% 2.18/2.57
% 2.18/2.57 termordering = kbo
% 2.18/2.57
% 2.18/2.57 litapriori = 0
% 2.18/2.57 termapriori = 1
% 2.18/2.57 litaposteriori = 0
% 2.18/2.57 termaposteriori = 0
% 2.18/2.57 demodaposteriori = 0
% 2.18/2.57 ordereqreflfact = 0
% 2.18/2.57
% 2.18/2.57 litselect = negord
% 2.18/2.57
% 2.18/2.57 maxweight = 15
% 2.18/2.57 maxdepth = 30000
% 2.18/2.57 maxlength = 115
% 2.18/2.57 maxnrvars = 195
% 2.18/2.57 excuselevel = 1
% 2.18/2.57 increasemaxweight = 1
% 2.18/2.57
% 2.18/2.57 maxselected = 10000000
% 2.18/2.57 maxnrclauses = 10000000
% 2.18/2.57
% 2.18/2.57 showgenerated = 0
% 2.18/2.57 showkept = 0
% 2.18/2.57 showselected = 0
% 2.18/2.57 showdeleted = 0
% 2.18/2.57 showresimp = 1
% 2.18/2.57 showstatus = 2000
% 2.18/2.57
% 2.18/2.57 prologoutput = 0
% 2.18/2.57 nrgoals = 5000000
% 2.18/2.57 totalproof = 1
% 2.18/2.57
% 2.18/2.57 Symbols occurring in the translation:
% 2.18/2.57
% 2.18/2.57 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.18/2.57 . [1, 2] (w:1, o:30, a:1, s:1, b:0),
% 2.18/2.57 ! [4, 1] (w:0, o:24, a:1, s:1, b:0),
% 2.18/2.57 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.18/2.57 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.18/2.57 furniture [37, 2] (w:1, o:59, a:1, s:1, b:0),
% 2.18/2.57 instrumentality [38, 2] (w:1, o:67, a:1, s:1, b:0),
% 2.18/2.57 seat [39, 2] (w:1, o:70, a:1, s:1, b:0),
% 2.18/2.57 frontseat [40, 2] (w:1, o:71, a:1, s:1, b:0),
% 2.18/2.57 location [41, 2] (w:1, o:72, a:1, s:1, b:0),
% 2.18/2.57 object [42, 2] (w:1, o:81, a:1, s:1, b:0),
% 2.18/2.57 city [43, 2] (w:1, o:86, a:1, s:1, b:0),
% 2.18/2.57 hollywood_placename [44, 2] (w:1, o:63, a:1, s:1, b:0),
% 2.18/2.57 placename [45, 2] (w:1, o:89, a:1, s:1, b:0),
% 2.18/2.57 abstraction [46, 2] (w:1, o:90, a:1, s:1, b:0),
% 2.18/2.57 unisex [47, 2] (w:1, o:101, a:1, s:1, b:0),
% 2.18/2.57 general [48, 2] (w:1, o:61, a:1, s:1, b:0),
% 2.18/2.57 nonhuman [49, 2] (w:1, o:78, a:1, s:1, b:0),
% 2.18/2.57 thing [50, 2] (w:1, o:98, a:1, s:1, b:0),
% 2.18/2.57 relation [51, 2] (w:1, o:68, a:1, s:1, b:0),
% 2.18/2.57 relname [52, 2] (w:1, o:69, a:1, s:1, b:0),
% 2.18/2.57 way [53, 2] (w:1, o:103, a:1, s:1, b:0),
% 2.18/2.57 artifact [54, 2] (w:1, o:104, a:1, s:1, b:0),
% 2.18/2.57 street [55, 2] (w:1, o:91, a:1, s:1, b:0),
% 2.18/2.57 impartial [56, 2] (w:1, o:66, a:1, s:1, b:0),
% 2.18/2.57 nonliving [57, 2] (w:1, o:79, a:1, s:1, b:0),
% 2.18/2.57 entity [58, 2] (w:1, o:55, a:1, s:1, b:0),
% 2.18/2.57 transport [59, 2] (w:1, o:99, a:1, s:1, b:0),
% 2.18/2.57 vehicle [60, 2] (w:1, o:102, a:1, s:1, b:0),
% 2.18/2.57 car [61, 2] (w:1, o:105, a:1, s:1, b:0),
% 2.18/2.57 chevy [62, 2] (w:1, o:85, a:1, s:1, b:0),
% 2.18/2.57 barrel [63, 2] (w:1, o:84, a:1, s:1, b:0),
% 2.18/2.57 event [64, 2] (w:1, o:56, a:1, s:1, b:0),
% 2.18/2.57 eventuality [65, 2] (w:1, o:57, a:1, s:1, b:0),
% 2.18/2.57 state [66, 2] (w:1, o:92, a:1, s:1, b:0),
% 2.18/2.57 nonexistent [67, 2] (w:1, o:80, a:1, s:1, b:0),
% 2.18/2.57 specific [68, 2] (w:1, o:93, a:1, s:1, b:0),
% 2.18/2.57 two [69, 2] (w:1, o:100, a:1, s:1, b:0),
% 2.18/2.57 group [70, 2] (w:1, o:62, a:1, s:1, b:0),
% 2.18/2.57 set [71, 2] (w:1, o:94, a:1, s:1, b:0),
% 2.18/2.57 multiple [72, 2] (w:1, o:75, a:1, s:1, b:0),
% 2.18/2.57 man [73, 2] (w:1, o:76, a:1, s:1, b:0),
% 2.18/2.57 male [74, 2] (w:1, o:77, a:1, s:1, b:0),
% 2.18/2.57 human_person [75, 2] (w:1, o:64, a:1, s:1, b:0),
% 2.18/2.57 animate [76, 2] (w:1, o:82, a:1, s:1, b:0),
% 2.18/2.57 human [77, 2] (w:1, o:65, a:1, s:1, b:0),
% 2.18/2.57 organism [78, 2] (w:1, o:87, a:1, s:1, b:0),
% 2.18/2.57 living [79, 2] (w:1, o:73, a:1, s:1, b:0),
% 2.18/2.57 existent [80, 2] (w:1, o:58, a:1, s:1, b:0),
% 3.17/3.53 singleton [81, 2] (w:1, o:95, a:1, s:1, b:0),
% 3.17/3.53 fellow [82, 2] (w:1, o:60, a:1, s:1, b:0),
% 3.17/3.53 young [83, 2] (w:1, o:106, a:1, s:1, b:0),
% 3.17/3.53 old [84, 2] (w:1, o:88, a:1, s:1, b:0),
% 3.17/3.53 of [86, 3] (w:1, o:109, a:1, s:1, b:0),
% 3.17/3.53 be [88, 4] (w:1, o:121, a:1, s:1, b:0),
% 3.17/3.53 member [89, 3] (w:1, o:110, a:1, s:1, b:0),
% 3.17/3.53 actual_world [91, 1] (w:1, o:29, a:1, s:1, b:0),
% 3.17/3.53 white [94, 2] (w:1, o:107, a:1, s:1, b:0),
% 3.17/3.53 dirty [95, 2] (w:1, o:54, a:1, s:1, b:0),
% 3.17/3.53 lonely [96, 2] (w:1, o:74, a:1, s:1, b:0),
% 3.17/3.53 agent [97, 3] (w:1, o:111, a:1, s:1, b:0),
% 3.17/3.53 present [98, 2] (w:1, o:108, a:1, s:1, b:0),
% 3.17/3.53 down [99, 3] (w:1, o:112, a:1, s:1, b:0),
% 3.17/3.53 in [100, 3] (w:1, o:113, a:1, s:1, b:0),
% 3.17/3.53 alpha1 [105, 3] (w:1, o:114, a:1, s:1, b:1),
% 3.17/3.53 alpha2 [106, 3] (w:1, o:115, a:1, s:1, b:1),
% 3.17/3.53 alpha3 [107, 4] (w:1, o:119, a:1, s:1, b:1),
% 3.17/3.53 alpha4 [108, 4] (w:1, o:120, a:1, s:1, b:1),
% 3.17/3.53 alpha5 [109, 2] (w:1, o:83, a:1, s:1, b:1),
% 3.17/3.53 alpha6 [110, 3] (w:1, o:116, a:1, s:1, b:1),
% 3.17/3.53 skol1 [111, 2] (w:1, o:96, a:1, s:1, b:1),
% 3.17/3.53 skol2 [112, 3] (w:1, o:117, a:1, s:1, b:1),
% 3.17/3.53 skol3 [113, 4] (w:1, o:122, a:1, s:1, b:1),
% 3.17/3.53 skol4 [114, 0] (w:1, o:17, a:1, s:1, b:1),
% 3.17/3.53 skol5 [115, 2] (w:1, o:97, a:1, s:1, b:1),
% 3.17/3.53 skol6 [116, 3] (w:1, o:118, a:1, s:1, b:1),
% 3.17/3.53 skol7 [117, 0] (w:1, o:18, a:1, s:1, b:1),
% 3.17/3.53 skol8 [118, 0] (w:1, o:19, a:1, s:1, b:1),
% 3.17/3.53 skol9 [119, 0] (w:1, o:20, a:1, s:1, b:1),
% 3.17/3.53 skol10 [120, 0] (w:1, o:21, a:1, s:1, b:1),
% 3.17/3.53 skol11 [121, 0] (w:1, o:22, a:1, s:1, b:1),
% 3.17/3.53 skol12 [122, 0] (w:1, o:23, a:1, s:1, b:1).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Starting Search:
% 3.17/3.53
% 3.17/3.53 *** allocated 15000 integers for clauses
% 3.17/3.53 *** allocated 22500 integers for clauses
% 3.17/3.53 *** allocated 33750 integers for clauses
% 3.17/3.53 *** allocated 50625 integers for clauses
% 3.17/3.53 *** allocated 15000 integers for termspace/termends
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 *** allocated 75937 integers for clauses
% 3.17/3.53 *** allocated 22500 integers for termspace/termends
% 3.17/3.53 *** allocated 113905 integers for clauses
% 3.17/3.53 *** allocated 33750 integers for termspace/termends
% 3.17/3.53 *** allocated 170857 integers for clauses
% 3.17/3.53 *** allocated 50625 integers for termspace/termends
% 3.17/3.53
% 3.17/3.53 Intermediate Status:
% 3.17/3.53 Generated: 4319
% 3.17/3.53 Kept: 3394
% 3.17/3.53 Inuse: 306
% 3.17/3.53 Deleted: 0
% 3.17/3.53 Deletedinuse: 0
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 *** allocated 256285 integers for clauses
% 3.17/3.53 *** allocated 75937 integers for termspace/termends
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Intermediate Status:
% 3.17/3.53 Generated: 6684
% 3.17/3.53 Kept: 5421
% 3.17/3.53 Inuse: 374
% 3.17/3.53 Deleted: 0
% 3.17/3.53 Deletedinuse: 0
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 *** allocated 384427 integers for clauses
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 *** allocated 113905 integers for termspace/termends
% 3.17/3.53
% 3.17/3.53 Intermediate Status:
% 3.17/3.53 Generated: 10841
% 3.17/3.53 Kept: 7506
% 3.17/3.53 Inuse: 381
% 3.17/3.53 Deleted: 0
% 3.17/3.53 Deletedinuse: 0
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 *** allocated 576640 integers for clauses
% 3.17/3.53 *** allocated 170857 integers for termspace/termends
% 3.17/3.53
% 3.17/3.53 Intermediate Status:
% 3.17/3.53 Generated: 14048
% 3.17/3.53 Kept: 9519
% 3.17/3.53 Inuse: 473
% 3.17/3.53 Deleted: 0
% 3.17/3.53 Deletedinuse: 0
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Intermediate Status:
% 3.17/3.53 Generated: 29286
% 3.17/3.53 Kept: 11820
% 3.17/3.53 Inuse: 1142
% 3.17/3.53 Deleted: 1
% 3.17/3.53 Deletedinuse: 0
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Intermediate Status:
% 3.17/3.53 Generated: 36529
% 3.17/3.53 Kept: 13820
% 3.17/3.53 Inuse: 1300
% 3.17/3.53 Deleted: 2
% 3.17/3.53 Deletedinuse: 1
% 3.17/3.53
% 3.17/3.53 *** allocated 256285 integers for termspace/termends
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 *** allocated 864960 integers for clauses
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Intermediate Status:
% 3.17/3.53 Generated: 41603
% 3.17/3.53 Kept: 15828
% 3.17/3.53 Inuse: 1430
% 3.17/3.53 Deleted: 2
% 3.17/3.53 Deletedinuse: 1
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Intermediate Status:
% 3.17/3.53 Generated: 46688
% 3.17/3.53 Kept: 17842
% 3.17/3.53 Inuse: 1551
% 3.17/3.53 Deleted: 2
% 3.17/3.53 Deletedinuse: 1
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 *** allocated 384427 integers for termspace/termends
% 3.17/3.53
% 3.17/3.53 Intermediate Status:
% 3.17/3.53 Generated: 51616
% 3.17/3.53 Kept: 19846
% 3.17/3.53 Inuse: 1669
% 3.17/3.53 Deleted: 2
% 3.17/3.53 Deletedinuse: 1
% 3.17/3.54
% 3.17/3.54 Resimplifying inuse:
% 3.17/3.54 Done
% 3.17/3.54
% 3.17/3.54 Resimplifying clauses:
% 3.17/3.54 Done
% 3.17/3.54
% 3.17/3.54
% 3.17/3.54 Bliksems!, er is een bewijs:
% 3.17/3.54 % SZS status Theorem
% 3.17/3.54 % SZS output start Refutation
% 3.17/3.54
% 3.17/3.54 (0) {G0,W6,D2,L2,V2,M2} I { ! furniture( X, Y ), instrumentality( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 (1) {G0,W6,D2,L2,V2,M2} I { ! seat( X, Y ), furniture( X, Y ) }.
% 3.17/3.54 (2) {G0,W6,D2,L2,V2,M2} I { ! frontseat( X, Y ), seat( X, Y ) }.
% 3.17/3.54 (17) {G0,W6,D2,L2,V2,M2} I { ! object( X, Y ), nonliving( X, Y ) }.
% 3.17/3.54 (19) {G0,W6,D2,L2,V2,M2} I { ! artifact( X, Y ), object( X, Y ) }.
% 3.17/3.54 (20) {G0,W6,D2,L2,V2,M2} I { ! instrumentality( X, Y ), artifact( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 (39) {G0,W6,D2,L2,V2,M2} I { ! organism( X, Y ), living( X, Y ) }.
% 3.17/3.54 (46) {G0,W6,D2,L2,V2,M2} I { ! human_person( X, Y ), organism( X, Y ) }.
% 3.17/3.54 (47) {G0,W6,D2,L2,V2,M2} I { ! man( X, Y ), human_person( X, Y ) }.
% 3.17/3.54 (48) {G0,W6,D2,L2,V2,M2} I { ! fellow( X, Y ), man( X, Y ) }.
% 3.17/3.54 (52) {G0,W6,D2,L2,V2,M2} I { ! nonliving( X, Y ), ! living( X, Y ) }.
% 3.17/3.54 (58) {G0,W8,D2,L2,V4,M2} I { ! be( Z, T, X, Y ), X = Y }.
% 3.17/3.54 (59) {G0,W9,D3,L2,V2,M2} I { ! two( X, Y ), member( X, skol1( X, Y ), Y )
% 3.17/3.54 }.
% 3.17/3.54 (92) {G0,W7,D2,L2,V1,M2} I { ! member( skol4, X, skol12 ), alpha5( skol4, X
% 3.17/3.54 ) }.
% 3.17/3.54 (93) {G0,W3,D2,L1,V0,M1} I { two( skol4, skol12 ) }.
% 3.17/3.54 (95) {G0,W7,D2,L2,V1,M2} I { ! member( skol4, X, skol12 ), fellow( skol4, X
% 3.17/3.54 ) }.
% 3.17/3.54 (97) {G0,W8,D3,L2,V3,M2} I { ! alpha5( X, Y ), frontseat( X, skol5( X, Z )
% 3.17/3.54 ) }.
% 3.17/3.54 (98) {G0,W9,D3,L2,V2,M2} I { ! alpha5( X, Y ), alpha6( X, Y, skol5( X, Y )
% 3.17/3.54 ) }.
% 3.17/3.54 (102) {G0,W12,D3,L2,V3,M2} I { ! alpha6( X, Y, Z ), be( X, skol6( X, Y, Z )
% 3.17/3.54 , Y, Z ) }.
% 3.17/3.54 (111) {G1,W6,D2,L2,V2,M2} R(2,1) { ! frontseat( X, Y ), furniture( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 (115) {G2,W6,D2,L2,V2,M2} R(111,0) { ! frontseat( X, Y ), instrumentality(
% 3.17/3.54 X, Y ) }.
% 3.17/3.54 (120) {G1,W6,D2,L2,V2,M2} R(47,48) { human_person( X, Y ), ! fellow( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 (121) {G2,W6,D2,L2,V2,M2} R(46,120) { organism( X, Y ), ! fellow( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 (165) {G1,W6,D2,L2,V2,M2} R(17,52) { ! object( X, Y ), ! living( X, Y ) }.
% 3.17/3.54 (983) {G1,W6,D3,L1,V0,M1} R(59,93) { member( skol4, skol1( skol4, skol12 )
% 3.17/3.54 , skol12 ) }.
% 3.17/3.54 (3614) {G1,W5,D3,L1,V0,M1} R(92,59);r(93) { alpha5( skol4, skol1( skol4,
% 3.17/3.54 skol12 ) ) }.
% 3.17/3.54 (3961) {G1,W10,D3,L2,V1,M2} R(98,92) { alpha6( skol4, X, skol5( skol4, X )
% 3.17/3.54 ), ! member( skol4, X, skol12 ) }.
% 3.17/3.54 (4256) {G1,W7,D2,L2,V3,M2} R(102,58) { ! alpha6( X, Y, Z ), Y = Z }.
% 3.17/3.54 (8771) {G2,W5,D3,L1,V1,M1} R(3614,97) { frontseat( skol4, skol5( skol4, X )
% 3.17/3.54 ) }.
% 3.17/3.54 (8773) {G3,W5,D3,L1,V1,M1} R(8771,115) { instrumentality( skol4, skol5(
% 3.17/3.54 skol4, X ) ) }.
% 3.17/3.54 (8803) {G4,W5,D3,L1,V1,M1} R(8773,20) { artifact( skol4, skol5( skol4, X )
% 3.17/3.54 ) }.
% 3.17/3.54 (8830) {G5,W5,D3,L1,V1,M1} R(8803,19) { object( skol4, skol5( skol4, X ) )
% 3.17/3.54 }.
% 3.17/3.54 (9243) {G6,W5,D3,L1,V1,M1} R(165,8830) { ! living( skol4, skol5( skol4, X )
% 3.17/3.54 ) }.
% 3.17/3.54 (9249) {G7,W5,D3,L1,V1,M1} R(9243,39) { ! organism( skol4, skol5( skol4, X
% 3.17/3.54 ) ) }.
% 3.17/3.54 (9277) {G8,W5,D3,L1,V1,M1} R(9249,121) { ! fellow( skol4, skol5( skol4, X )
% 3.17/3.54 ) }.
% 3.17/3.54 (9331) {G9,W6,D3,L1,V1,M1} R(9277,95) { ! member( skol4, skol5( skol4, X )
% 3.17/3.54 , skol12 ) }.
% 3.17/3.54 (10510) {G10,W10,D3,L2,V3,M2} P(4256,9331) { ! member( skol4, Y, skol12 ),
% 3.17/3.54 ! alpha6( Z, Y, skol5( skol4, X ) ) }.
% 3.17/3.54 (20030) {G11,W4,D2,L1,V1,M1} S(3961);r(10510) { ! member( skol4, X, skol12
% 3.17/3.54 ) }.
% 3.17/3.54 (20060) {G12,W0,D0,L0,V0,M0} R(20030,983) { }.
% 3.17/3.54
% 3.17/3.54
% 3.17/3.54 % SZS output end Refutation
% 3.17/3.54 found a proof!
% 3.17/3.54
% 3.17/3.54
% 3.17/3.54 Unprocessed initial clauses:
% 3.17/3.54
% 3.17/3.54 (20062) {G0,W6,D2,L2,V2,M2} { ! furniture( X, Y ), instrumentality( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 (20063) {G0,W6,D2,L2,V2,M2} { ! seat( X, Y ), furniture( X, Y ) }.
% 3.17/3.54 (20064) {G0,W6,D2,L2,V2,M2} { ! frontseat( X, Y ), seat( X, Y ) }.
% 3.17/3.54 (20065) {G0,W6,D2,L2,V2,M2} { ! location( X, Y ), object( X, Y ) }.
% 3.17/3.54 (20066) {G0,W6,D2,L2,V2,M2} { ! city( X, Y ), location( X, Y ) }.
% 3.17/3.54 (20067) {G0,W6,D2,L2,V2,M2} { ! hollywood_placename( X, Y ), placename( X
% 3.17/3.54 , Y ) }.
% 3.17/3.54 (20068) {G0,W6,D2,L2,V2,M2} { ! abstraction( X, Y ), unisex( X, Y ) }.
% 3.17/3.54 (20069) {G0,W6,D2,L2,V2,M2} { ! abstraction( X, Y ), general( X, Y ) }.
% 3.17/3.54 (20070) {G0,W6,D2,L2,V2,M2} { ! abstraction( X, Y ), nonhuman( X, Y ) }.
% 3.17/3.54 (20071) {G0,W6,D2,L2,V2,M2} { ! abstraction( X, Y ), thing( X, Y ) }.
% 3.17/3.54 (20072) {G0,W6,D2,L2,V2,M2} { ! relation( X, Y ), abstraction( X, Y ) }.
% 3.17/3.54 (20073) {G0,W6,D2,L2,V2,M2} { ! relname( X, Y ), relation( X, Y ) }.
% 3.17/3.54 (20074) {G0,W6,D2,L2,V2,M2} { ! placename( X, Y ), relname( X, Y ) }.
% 3.17/3.54 (20075) {G0,W6,D2,L2,V2,M2} { ! way( X, Y ), artifact( X, Y ) }.
% 3.17/3.54 (20076) {G0,W6,D2,L2,V2,M2} { ! street( X, Y ), way( X, Y ) }.
% 3.17/3.54 (20077) {G0,W6,D2,L2,V2,M2} { ! object( X, Y ), unisex( X, Y ) }.
% 3.17/3.54 (20078) {G0,W6,D2,L2,V2,M2} { ! object( X, Y ), impartial( X, Y ) }.
% 3.17/3.54 (20079) {G0,W6,D2,L2,V2,M2} { ! object( X, Y ), nonliving( X, Y ) }.
% 3.17/3.54 (20080) {G0,W6,D2,L2,V2,M2} { ! object( X, Y ), entity( X, Y ) }.
% 3.17/3.54 (20081) {G0,W6,D2,L2,V2,M2} { ! artifact( X, Y ), object( X, Y ) }.
% 3.17/3.54 (20082) {G0,W6,D2,L2,V2,M2} { ! instrumentality( X, Y ), artifact( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 (20083) {G0,W6,D2,L2,V2,M2} { ! transport( X, Y ), instrumentality( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 (20084) {G0,W6,D2,L2,V2,M2} { ! vehicle( X, Y ), transport( X, Y ) }.
% 3.17/3.54 (20085) {G0,W6,D2,L2,V2,M2} { ! car( X, Y ), vehicle( X, Y ) }.
% 3.17/3.54 (20086) {G0,W6,D2,L2,V2,M2} { ! chevy( X, Y ), car( X, Y ) }.
% 3.17/3.54 (20087) {G0,W6,D2,L2,V2,M2} { ! barrel( X, Y ), event( X, Y ) }.
% 3.17/3.54 (20088) {G0,W6,D2,L2,V2,M2} { ! event( X, Y ), eventuality( X, Y ) }.
% 3.17/3.54 (20089) {G0,W6,D2,L2,V2,M2} { ! state( X, Y ), event( X, Y ) }.
% 3.17/3.54 (20090) {G0,W6,D2,L2,V2,M2} { ! eventuality( X, Y ), unisex( X, Y ) }.
% 3.17/3.54 (20091) {G0,W6,D2,L2,V2,M2} { ! eventuality( X, Y ), nonexistent( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 (20092) {G0,W6,D2,L2,V2,M2} { ! eventuality( X, Y ), specific( X, Y ) }.
% 3.17/3.54 (20093) {G0,W6,D2,L2,V2,M2} { ! eventuality( X, Y ), thing( X, Y ) }.
% 3.17/3.54 (20094) {G0,W6,D2,L2,V2,M2} { ! state( X, Y ), eventuality( X, Y ) }.
% 3.17/3.54 (20095) {G0,W6,D2,L2,V2,M2} { ! two( X, Y ), group( X, Y ) }.
% 3.17/3.54 (20096) {G0,W6,D2,L2,V2,M2} { ! set( X, Y ), multiple( X, Y ) }.
% 3.17/3.54 (20097) {G0,W6,D2,L2,V2,M2} { ! group( X, Y ), set( X, Y ) }.
% 3.17/3.54 (20098) {G0,W6,D2,L2,V2,M2} { ! man( X, Y ), male( X, Y ) }.
% 3.17/3.54 (20099) {G0,W6,D2,L2,V2,M2} { ! human_person( X, Y ), animate( X, Y ) }.
% 3.17/3.54 (20100) {G0,W6,D2,L2,V2,M2} { ! human_person( X, Y ), human( X, Y ) }.
% 3.17/3.54 (20101) {G0,W6,D2,L2,V2,M2} { ! organism( X, Y ), living( X, Y ) }.
% 3.17/3.54 (20102) {G0,W6,D2,L2,V2,M2} { ! organism( X, Y ), impartial( X, Y ) }.
% 3.17/3.54 (20103) {G0,W6,D2,L2,V2,M2} { ! entity( X, Y ), existent( X, Y ) }.
% 3.17/3.54 (20104) {G0,W6,D2,L2,V2,M2} { ! entity( X, Y ), specific( X, Y ) }.
% 3.17/3.54 (20105) {G0,W6,D2,L2,V2,M2} { ! thing( X, Y ), singleton( X, Y ) }.
% 3.17/3.54 (20106) {G0,W6,D2,L2,V2,M2} { ! entity( X, Y ), thing( X, Y ) }.
% 3.17/3.54 (20107) {G0,W6,D2,L2,V2,M2} { ! organism( X, Y ), entity( X, Y ) }.
% 3.17/3.54 (20108) {G0,W6,D2,L2,V2,M2} { ! human_person( X, Y ), organism( X, Y ) }.
% 3.17/3.54 (20109) {G0,W6,D2,L2,V2,M2} { ! man( X, Y ), human_person( X, Y ) }.
% 3.17/3.54 (20110) {G0,W6,D2,L2,V2,M2} { ! fellow( X, Y ), man( X, Y ) }.
% 3.17/3.54 (20111) {G0,W6,D2,L2,V2,M2} { ! animate( X, Y ), ! nonliving( X, Y ) }.
% 3.17/3.54 (20112) {G0,W6,D2,L2,V2,M2} { ! existent( X, Y ), ! nonexistent( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 (20113) {G0,W6,D2,L2,V2,M2} { ! nonhuman( X, Y ), ! human( X, Y ) }.
% 3.17/3.54 (20114) {G0,W6,D2,L2,V2,M2} { ! nonliving( X, Y ), ! living( X, Y ) }.
% 3.17/3.54 (20115) {G0,W6,D2,L2,V2,M2} { ! singleton( X, Y ), ! multiple( X, Y ) }.
% 3.17/3.54 (20116) {G0,W6,D2,L2,V2,M2} { ! specific( X, Y ), ! general( X, Y ) }.
% 3.17/3.54 (20117) {G0,W6,D2,L2,V2,M2} { ! unisex( X, Y ), ! male( X, Y ) }.
% 3.17/3.54 (20118) {G0,W6,D2,L2,V2,M2} { ! young( X, Y ), ! old( X, Y ) }.
% 3.17/3.54 (20119) {G0,W20,D2,L6,V4,M6} { ! entity( X, Y ), ! placename( X, Z ), ! of
% 3.17/3.54 ( X, Z, Y ), ! placename( X, T ), T = Z, ! of( X, T, Y ) }.
% 3.17/3.54 (20120) {G0,W8,D2,L2,V4,M2} { ! be( Z, T, X, Y ), X = Y }.
% 3.17/3.54 (20121) {G0,W9,D3,L2,V2,M2} { ! two( X, Y ), member( X, skol1( X, Y ), Y )
% 3.17/3.54 }.
% 3.17/3.54 (20122) {G0,W9,D3,L2,V2,M2} { ! two( X, Y ), alpha1( X, Y, skol1( X, Y ) )
% 3.17/3.54 }.
% 3.17/3.54 (20123) {G0,W11,D2,L3,V3,M3} { ! member( X, Z, Y ), ! alpha1( X, Y, Z ),
% 3.17/3.54 two( X, Y ) }.
% 3.17/3.54 (20124) {G0,W11,D3,L2,V4,M2} { ! alpha1( X, Y, Z ), member( X, skol2( X, Y
% 3.17/3.54 , T ), Y ) }.
% 3.17/3.54 (20125) {G0,W12,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), alpha3( X, Y, Z, skol2
% 3.17/3.54 ( X, Y, Z ) ) }.
% 3.17/3.54 (20126) {G0,W13,D2,L3,V4,M3} { ! member( X, T, Y ), ! alpha3( X, Y, Z, T )
% 3.17/3.54 , alpha1( X, Y, Z ) }.
% 3.17/3.54 (20127) {G0,W8,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), ! T = Z }.
% 3.17/3.54 (20128) {G0,W10,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), alpha4( X, Y, Z, T
% 3.17/3.54 ) }.
% 3.17/3.54 (20129) {G0,W13,D2,L3,V4,M3} { T = Z, ! alpha4( X, Y, Z, T ), alpha3( X, Y
% 3.17/3.54 , Z, T ) }.
% 3.17/3.54 (20130) {G0,W13,D2,L3,V5,M3} { ! alpha4( X, Y, Z, T ), ! member( X, U, Y )
% 3.17/3.54 , alpha2( Z, T, U ) }.
% 3.17/3.54 (20131) {G0,W13,D3,L2,V6,M2} { ! alpha2( Z, T, skol3( U, W, Z, T ) ),
% 3.17/3.54 alpha4( X, Y, Z, T ) }.
% 3.17/3.54 (20132) {G0,W13,D3,L2,V4,M2} { member( X, skol3( X, Y, Z, T ), Y ), alpha4
% 3.17/3.54 ( X, Y, Z, T ) }.
% 3.17/3.54 (20133) {G0,W10,D2,L3,V3,M3} { ! alpha2( X, Y, Z ), Z = Y, Z = X }.
% 3.17/3.54 (20134) {G0,W7,D2,L2,V3,M2} { ! Z = Y, alpha2( X, Y, Z ) }.
% 3.17/3.54 (20135) {G0,W7,D2,L2,V3,M2} { ! Z = X, alpha2( X, Y, Z ) }.
% 3.17/3.54 (20136) {G0,W4,D2,L1,V2,M1} { ! member( X, Y, Y ) }.
% 3.17/3.54 (20137) {G0,W2,D2,L1,V0,M1} { actual_world( skol4 ) }.
% 3.17/3.54 (20138) {G0,W4,D2,L1,V0,M1} { of( skol4, skol8, skol7 ) }.
% 3.17/3.54 (20139) {G0,W3,D2,L1,V0,M1} { city( skol4, skol7 ) }.
% 3.17/3.54 (20140) {G0,W3,D2,L1,V0,M1} { hollywood_placename( skol4, skol8 ) }.
% 3.17/3.54 (20141) {G0,W3,D2,L1,V0,M1} { placename( skol4, skol8 ) }.
% 3.17/3.54 (20142) {G0,W3,D2,L1,V0,M1} { chevy( skol4, skol9 ) }.
% 3.17/3.54 (20143) {G0,W3,D2,L1,V0,M1} { white( skol4, skol9 ) }.
% 3.17/3.54 (20144) {G0,W3,D2,L1,V0,M1} { dirty( skol4, skol9 ) }.
% 3.17/3.54 (20145) {G0,W3,D2,L1,V0,M1} { old( skol4, skol9 ) }.
% 3.17/3.54 (20146) {G0,W3,D2,L1,V0,M1} { street( skol4, skol10 ) }.
% 3.17/3.54 (20147) {G0,W3,D2,L1,V0,M1} { lonely( skol4, skol10 ) }.
% 3.17/3.54 (20148) {G0,W3,D2,L1,V0,M1} { event( skol4, skol11 ) }.
% 3.17/3.54 (20149) {G0,W4,D2,L1,V0,M1} { agent( skol4, skol11, skol9 ) }.
% 3.17/3.54 (20150) {G0,W3,D2,L1,V0,M1} { present( skol4, skol11 ) }.
% 3.17/3.54 (20151) {G0,W3,D2,L1,V0,M1} { barrel( skol4, skol11 ) }.
% 3.17/3.54 (20152) {G0,W4,D2,L1,V0,M1} { down( skol4, skol11, skol10 ) }.
% 3.17/3.54 (20153) {G0,W4,D2,L1,V0,M1} { in( skol4, skol11, skol7 ) }.
% 3.17/3.54 (20154) {G0,W7,D2,L2,V1,M2} { ! member( skol4, X, skol12 ), alpha5( skol4
% 3.17/3.54 , X ) }.
% 3.17/3.54 (20155) {G0,W3,D2,L1,V0,M1} { two( skol4, skol12 ) }.
% 3.17/3.54 (20156) {G0,W3,D2,L1,V0,M1} { group( skol4, skol12 ) }.
% 3.17/3.54 (20157) {G0,W7,D2,L2,V1,M2} { ! member( skol4, X, skol12 ), fellow( skol4
% 3.17/3.54 , X ) }.
% 3.17/3.54 (20158) {G0,W7,D2,L2,V1,M2} { ! member( skol4, X, skol12 ), young( skol4,
% 3.17/3.54 X ) }.
% 3.17/3.54 (20159) {G0,W8,D3,L2,V3,M2} { ! alpha5( X, Y ), frontseat( X, skol5( X, Z
% 3.17/3.54 ) ) }.
% 3.17/3.54 (20160) {G0,W9,D3,L2,V2,M2} { ! alpha5( X, Y ), alpha6( X, Y, skol5( X, Y
% 3.17/3.54 ) ) }.
% 3.17/3.54 (20161) {G0,W10,D2,L3,V3,M3} { ! frontseat( X, Z ), ! alpha6( X, Y, Z ),
% 3.17/3.54 alpha5( X, Y ) }.
% 3.17/3.54 (20162) {G0,W10,D3,L2,V5,M2} { ! alpha6( X, Y, Z ), state( X, skol6( X, T
% 3.17/3.54 , U ) ) }.
% 3.17/3.54 (20163) {G0,W8,D2,L2,V3,M2} { ! alpha6( X, Y, Z ), in( X, Z, Z ) }.
% 3.17/3.54 (20164) {G0,W12,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), be( X, skol6( X, Y, Z
% 3.17/3.54 ), Y, Z ) }.
% 3.17/3.54 (20165) {G0,W16,D2,L4,V4,M4} { ! state( X, T ), ! be( X, T, Y, Z ), ! in(
% 3.17/3.54 X, Z, Z ), alpha6( X, Y, Z ) }.
% 3.17/3.54
% 3.17/3.54
% 3.17/3.54 Total Proof:
% 3.17/3.54
% 3.17/3.54 subsumption: (0) {G0,W6,D2,L2,V2,M2} I { ! furniture( X, Y ),
% 3.17/3.54 instrumentality( X, Y ) }.
% 3.17/3.54 parent0: (20062) {G0,W6,D2,L2,V2,M2} { ! furniture( X, Y ),
% 3.17/3.54 instrumentality( X, Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (1) {G0,W6,D2,L2,V2,M2} I { ! seat( X, Y ), furniture( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 parent0: (20063) {G0,W6,D2,L2,V2,M2} { ! seat( X, Y ), furniture( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (2) {G0,W6,D2,L2,V2,M2} I { ! frontseat( X, Y ), seat( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 parent0: (20064) {G0,W6,D2,L2,V2,M2} { ! frontseat( X, Y ), seat( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (17) {G0,W6,D2,L2,V2,M2} I { ! object( X, Y ), nonliving( X, Y
% 3.17/3.54 ) }.
% 3.17/3.54 parent0: (20079) {G0,W6,D2,L2,V2,M2} { ! object( X, Y ), nonliving( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (19) {G0,W6,D2,L2,V2,M2} I { ! artifact( X, Y ), object( X, Y
% 3.17/3.54 ) }.
% 3.17/3.54 parent0: (20081) {G0,W6,D2,L2,V2,M2} { ! artifact( X, Y ), object( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (20) {G0,W6,D2,L2,V2,M2} I { ! instrumentality( X, Y ),
% 3.17/3.54 artifact( X, Y ) }.
% 3.17/3.54 parent0: (20082) {G0,W6,D2,L2,V2,M2} { ! instrumentality( X, Y ), artifact
% 3.17/3.54 ( X, Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (39) {G0,W6,D2,L2,V2,M2} I { ! organism( X, Y ), living( X, Y
% 3.17/3.54 ) }.
% 3.17/3.54 parent0: (20101) {G0,W6,D2,L2,V2,M2} { ! organism( X, Y ), living( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (46) {G0,W6,D2,L2,V2,M2} I { ! human_person( X, Y ), organism
% 3.17/3.54 ( X, Y ) }.
% 3.17/3.54 parent0: (20108) {G0,W6,D2,L2,V2,M2} { ! human_person( X, Y ), organism( X
% 3.17/3.54 , Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (47) {G0,W6,D2,L2,V2,M2} I { ! man( X, Y ), human_person( X, Y
% 3.17/3.54 ) }.
% 3.17/3.54 parent0: (20109) {G0,W6,D2,L2,V2,M2} { ! man( X, Y ), human_person( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (48) {G0,W6,D2,L2,V2,M2} I { ! fellow( X, Y ), man( X, Y ) }.
% 3.17/3.54 parent0: (20110) {G0,W6,D2,L2,V2,M2} { ! fellow( X, Y ), man( X, Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (52) {G0,W6,D2,L2,V2,M2} I { ! nonliving( X, Y ), ! living( X
% 3.17/3.54 , Y ) }.
% 3.17/3.54 parent0: (20114) {G0,W6,D2,L2,V2,M2} { ! nonliving( X, Y ), ! living( X, Y
% 3.17/3.54 ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (58) {G0,W8,D2,L2,V4,M2} I { ! be( Z, T, X, Y ), X = Y }.
% 3.17/3.54 parent0: (20120) {G0,W8,D2,L2,V4,M2} { ! be( Z, T, X, Y ), X = Y }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 Z := Z
% 3.17/3.54 T := T
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (59) {G0,W9,D3,L2,V2,M2} I { ! two( X, Y ), member( X, skol1(
% 3.17/3.54 X, Y ), Y ) }.
% 3.17/3.54 parent0: (20121) {G0,W9,D3,L2,V2,M2} { ! two( X, Y ), member( X, skol1( X
% 3.17/3.54 , Y ), Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (92) {G0,W7,D2,L2,V1,M2} I { ! member( skol4, X, skol12 ),
% 3.17/3.54 alpha5( skol4, X ) }.
% 3.17/3.54 parent0: (20154) {G0,W7,D2,L2,V1,M2} { ! member( skol4, X, skol12 ),
% 3.17/3.54 alpha5( skol4, X ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (93) {G0,W3,D2,L1,V0,M1} I { two( skol4, skol12 ) }.
% 3.17/3.54 parent0: (20155) {G0,W3,D2,L1,V0,M1} { two( skol4, skol12 ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (95) {G0,W7,D2,L2,V1,M2} I { ! member( skol4, X, skol12 ),
% 3.17/3.54 fellow( skol4, X ) }.
% 3.17/3.54 parent0: (20157) {G0,W7,D2,L2,V1,M2} { ! member( skol4, X, skol12 ),
% 3.17/3.54 fellow( skol4, X ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (97) {G0,W8,D3,L2,V3,M2} I { ! alpha5( X, Y ), frontseat( X,
% 3.17/3.54 skol5( X, Z ) ) }.
% 3.17/3.54 parent0: (20159) {G0,W8,D3,L2,V3,M2} { ! alpha5( X, Y ), frontseat( X,
% 3.17/3.54 skol5( X, Z ) ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 Z := Z
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (98) {G0,W9,D3,L2,V2,M2} I { ! alpha5( X, Y ), alpha6( X, Y,
% 3.17/3.54 skol5( X, Y ) ) }.
% 3.17/3.54 parent0: (20160) {G0,W9,D3,L2,V2,M2} { ! alpha5( X, Y ), alpha6( X, Y,
% 3.17/3.54 skol5( X, Y ) ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (102) {G0,W12,D3,L2,V3,M2} I { ! alpha6( X, Y, Z ), be( X,
% 3.17/3.54 skol6( X, Y, Z ), Y, Z ) }.
% 3.17/3.54 parent0: (20164) {G0,W12,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), be( X, skol6
% 3.17/3.54 ( X, Y, Z ), Y, Z ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 Z := Z
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20252) {G1,W6,D2,L2,V2,M2} { furniture( X, Y ), ! frontseat(
% 3.17/3.54 X, Y ) }.
% 3.17/3.54 parent0[0]: (1) {G0,W6,D2,L2,V2,M2} I { ! seat( X, Y ), furniture( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 parent1[1]: (2) {G0,W6,D2,L2,V2,M2} I { ! frontseat( X, Y ), seat( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (111) {G1,W6,D2,L2,V2,M2} R(2,1) { ! frontseat( X, Y ),
% 3.17/3.54 furniture( X, Y ) }.
% 3.17/3.54 parent0: (20252) {G1,W6,D2,L2,V2,M2} { furniture( X, Y ), ! frontseat( X,
% 3.17/3.54 Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 1
% 3.17/3.54 1 ==> 0
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20253) {G1,W6,D2,L2,V2,M2} { instrumentality( X, Y ), !
% 3.17/3.54 frontseat( X, Y ) }.
% 3.17/3.54 parent0[0]: (0) {G0,W6,D2,L2,V2,M2} I { ! furniture( X, Y ),
% 3.17/3.54 instrumentality( X, Y ) }.
% 3.17/3.54 parent1[1]: (111) {G1,W6,D2,L2,V2,M2} R(2,1) { ! frontseat( X, Y ),
% 3.17/3.54 furniture( X, Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (115) {G2,W6,D2,L2,V2,M2} R(111,0) { ! frontseat( X, Y ),
% 3.17/3.54 instrumentality( X, Y ) }.
% 3.17/3.54 parent0: (20253) {G1,W6,D2,L2,V2,M2} { instrumentality( X, Y ), !
% 3.17/3.54 frontseat( X, Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 1
% 3.17/3.54 1 ==> 0
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20254) {G1,W6,D2,L2,V2,M2} { human_person( X, Y ), ! fellow(
% 3.17/3.54 X, Y ) }.
% 3.17/3.54 parent0[0]: (47) {G0,W6,D2,L2,V2,M2} I { ! man( X, Y ), human_person( X, Y
% 3.17/3.54 ) }.
% 3.17/3.54 parent1[1]: (48) {G0,W6,D2,L2,V2,M2} I { ! fellow( X, Y ), man( X, Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (120) {G1,W6,D2,L2,V2,M2} R(47,48) { human_person( X, Y ), !
% 3.17/3.54 fellow( X, Y ) }.
% 3.17/3.54 parent0: (20254) {G1,W6,D2,L2,V2,M2} { human_person( X, Y ), ! fellow( X,
% 3.17/3.54 Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20255) {G1,W6,D2,L2,V2,M2} { organism( X, Y ), ! fellow( X, Y
% 3.17/3.54 ) }.
% 3.17/3.54 parent0[0]: (46) {G0,W6,D2,L2,V2,M2} I { ! human_person( X, Y ), organism(
% 3.17/3.54 X, Y ) }.
% 3.17/3.54 parent1[0]: (120) {G1,W6,D2,L2,V2,M2} R(47,48) { human_person( X, Y ), !
% 3.17/3.54 fellow( X, Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (121) {G2,W6,D2,L2,V2,M2} R(46,120) { organism( X, Y ), !
% 3.17/3.54 fellow( X, Y ) }.
% 3.17/3.54 parent0: (20255) {G1,W6,D2,L2,V2,M2} { organism( X, Y ), ! fellow( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20256) {G1,W6,D2,L2,V2,M2} { ! living( X, Y ), ! object( X, Y
% 3.17/3.54 ) }.
% 3.17/3.54 parent0[0]: (52) {G0,W6,D2,L2,V2,M2} I { ! nonliving( X, Y ), ! living( X,
% 3.17/3.54 Y ) }.
% 3.17/3.54 parent1[1]: (17) {G0,W6,D2,L2,V2,M2} I { ! object( X, Y ), nonliving( X, Y
% 3.17/3.54 ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (165) {G1,W6,D2,L2,V2,M2} R(17,52) { ! object( X, Y ), !
% 3.17/3.54 living( X, Y ) }.
% 3.17/3.54 parent0: (20256) {G1,W6,D2,L2,V2,M2} { ! living( X, Y ), ! object( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 1
% 3.17/3.54 1 ==> 0
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20257) {G1,W6,D3,L1,V0,M1} { member( skol4, skol1( skol4,
% 3.17/3.54 skol12 ), skol12 ) }.
% 3.17/3.54 parent0[0]: (59) {G0,W9,D3,L2,V2,M2} I { ! two( X, Y ), member( X, skol1( X
% 3.17/3.54 , Y ), Y ) }.
% 3.17/3.54 parent1[0]: (93) {G0,W3,D2,L1,V0,M1} I { two( skol4, skol12 ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := skol4
% 3.17/3.54 Y := skol12
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (983) {G1,W6,D3,L1,V0,M1} R(59,93) { member( skol4, skol1(
% 3.17/3.54 skol4, skol12 ), skol12 ) }.
% 3.17/3.54 parent0: (20257) {G1,W6,D3,L1,V0,M1} { member( skol4, skol1( skol4, skol12
% 3.17/3.54 ), skol12 ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20258) {G1,W8,D3,L2,V0,M2} { alpha5( skol4, skol1( skol4,
% 3.17/3.54 skol12 ) ), ! two( skol4, skol12 ) }.
% 3.17/3.54 parent0[0]: (92) {G0,W7,D2,L2,V1,M2} I { ! member( skol4, X, skol12 ),
% 3.17/3.54 alpha5( skol4, X ) }.
% 3.17/3.54 parent1[1]: (59) {G0,W9,D3,L2,V2,M2} I { ! two( X, Y ), member( X, skol1( X
% 3.17/3.54 , Y ), Y ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := skol1( skol4, skol12 )
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 X := skol4
% 3.17/3.54 Y := skol12
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20259) {G1,W5,D3,L1,V0,M1} { alpha5( skol4, skol1( skol4,
% 3.17/3.54 skol12 ) ) }.
% 3.17/3.54 parent0[1]: (20258) {G1,W8,D3,L2,V0,M2} { alpha5( skol4, skol1( skol4,
% 3.17/3.54 skol12 ) ), ! two( skol4, skol12 ) }.
% 3.17/3.54 parent1[0]: (93) {G0,W3,D2,L1,V0,M1} I { two( skol4, skol12 ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (3614) {G1,W5,D3,L1,V0,M1} R(92,59);r(93) { alpha5( skol4,
% 3.17/3.54 skol1( skol4, skol12 ) ) }.
% 3.17/3.54 parent0: (20259) {G1,W5,D3,L1,V0,M1} { alpha5( skol4, skol1( skol4, skol12
% 3.17/3.54 ) ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20260) {G1,W10,D3,L2,V1,M2} { alpha6( skol4, X, skol5( skol4
% 3.17/3.54 , X ) ), ! member( skol4, X, skol12 ) }.
% 3.17/3.54 parent0[0]: (98) {G0,W9,D3,L2,V2,M2} I { ! alpha5( X, Y ), alpha6( X, Y,
% 3.17/3.54 skol5( X, Y ) ) }.
% 3.17/3.54 parent1[1]: (92) {G0,W7,D2,L2,V1,M2} I { ! member( skol4, X, skol12 ),
% 3.17/3.54 alpha5( skol4, X ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := skol4
% 3.17/3.54 Y := X
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 X := X
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (3961) {G1,W10,D3,L2,V1,M2} R(98,92) { alpha6( skol4, X, skol5
% 3.17/3.54 ( skol4, X ) ), ! member( skol4, X, skol12 ) }.
% 3.17/3.54 parent0: (20260) {G1,W10,D3,L2,V1,M2} { alpha6( skol4, X, skol5( skol4, X
% 3.17/3.54 ) ), ! member( skol4, X, skol12 ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 1 ==> 1
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 eqswap: (20261) {G0,W8,D2,L2,V4,M2} { Y = X, ! be( Z, T, X, Y ) }.
% 3.17/3.54 parent0[1]: (58) {G0,W8,D2,L2,V4,M2} I { ! be( Z, T, X, Y ), X = Y }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 Z := Z
% 3.17/3.54 T := T
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20262) {G1,W7,D2,L2,V3,M2} { X = Y, ! alpha6( Z, Y, X ) }.
% 3.17/3.54 parent0[1]: (20261) {G0,W8,D2,L2,V4,M2} { Y = X, ! be( Z, T, X, Y ) }.
% 3.17/3.54 parent1[1]: (102) {G0,W12,D3,L2,V3,M2} I { ! alpha6( X, Y, Z ), be( X,
% 3.17/3.54 skol6( X, Y, Z ), Y, Z ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := Y
% 3.17/3.54 Y := X
% 3.17/3.54 Z := Z
% 3.17/3.54 T := skol6( Z, Y, X )
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 X := Z
% 3.17/3.54 Y := Y
% 3.17/3.54 Z := X
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 eqswap: (20263) {G1,W7,D2,L2,V3,M2} { Y = X, ! alpha6( Z, Y, X ) }.
% 3.17/3.54 parent0[0]: (20262) {G1,W7,D2,L2,V3,M2} { X = Y, ! alpha6( Z, Y, X ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 Y := Y
% 3.17/3.54 Z := Z
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (4256) {G1,W7,D2,L2,V3,M2} R(102,58) { ! alpha6( X, Y, Z ), Y
% 3.17/3.54 = Z }.
% 3.17/3.54 parent0: (20263) {G1,W7,D2,L2,V3,M2} { Y = X, ! alpha6( Z, Y, X ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := Z
% 3.17/3.54 Y := Y
% 3.17/3.54 Z := X
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 1
% 3.17/3.54 1 ==> 0
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20264) {G1,W5,D3,L1,V1,M1} { frontseat( skol4, skol5( skol4,
% 3.17/3.54 X ) ) }.
% 3.17/3.54 parent0[0]: (97) {G0,W8,D3,L2,V3,M2} I { ! alpha5( X, Y ), frontseat( X,
% 3.17/3.54 skol5( X, Z ) ) }.
% 3.17/3.54 parent1[0]: (3614) {G1,W5,D3,L1,V0,M1} R(92,59);r(93) { alpha5( skol4,
% 3.17/3.54 skol1( skol4, skol12 ) ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := skol4
% 3.17/3.54 Y := skol1( skol4, skol12 )
% 3.17/3.54 Z := X
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (8771) {G2,W5,D3,L1,V1,M1} R(3614,97) { frontseat( skol4,
% 3.17/3.54 skol5( skol4, X ) ) }.
% 3.17/3.54 parent0: (20264) {G1,W5,D3,L1,V1,M1} { frontseat( skol4, skol5( skol4, X )
% 3.17/3.54 ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20265) {G3,W5,D3,L1,V1,M1} { instrumentality( skol4, skol5(
% 3.17/3.54 skol4, X ) ) }.
% 3.17/3.54 parent0[0]: (115) {G2,W6,D2,L2,V2,M2} R(111,0) { ! frontseat( X, Y ),
% 3.17/3.54 instrumentality( X, Y ) }.
% 3.17/3.54 parent1[0]: (8771) {G2,W5,D3,L1,V1,M1} R(3614,97) { frontseat( skol4, skol5
% 3.17/3.54 ( skol4, X ) ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := skol4
% 3.17/3.54 Y := skol5( skol4, X )
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 X := X
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (8773) {G3,W5,D3,L1,V1,M1} R(8771,115) { instrumentality(
% 3.17/3.54 skol4, skol5( skol4, X ) ) }.
% 3.17/3.54 parent0: (20265) {G3,W5,D3,L1,V1,M1} { instrumentality( skol4, skol5(
% 3.17/3.54 skol4, X ) ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20266) {G1,W5,D3,L1,V1,M1} { artifact( skol4, skol5( skol4, X
% 3.17/3.54 ) ) }.
% 3.17/3.54 parent0[0]: (20) {G0,W6,D2,L2,V2,M2} I { ! instrumentality( X, Y ),
% 3.17/3.54 artifact( X, Y ) }.
% 3.17/3.54 parent1[0]: (8773) {G3,W5,D3,L1,V1,M1} R(8771,115) { instrumentality( skol4
% 3.17/3.54 , skol5( skol4, X ) ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := skol4
% 3.17/3.54 Y := skol5( skol4, X )
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 X := X
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (8803) {G4,W5,D3,L1,V1,M1} R(8773,20) { artifact( skol4, skol5
% 3.17/3.54 ( skol4, X ) ) }.
% 3.17/3.54 parent0: (20266) {G1,W5,D3,L1,V1,M1} { artifact( skol4, skol5( skol4, X )
% 3.17/3.54 ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20267) {G1,W5,D3,L1,V1,M1} { object( skol4, skol5( skol4, X )
% 3.17/3.54 ) }.
% 3.17/3.54 parent0[0]: (19) {G0,W6,D2,L2,V2,M2} I { ! artifact( X, Y ), object( X, Y )
% 3.17/3.54 }.
% 3.17/3.54 parent1[0]: (8803) {G4,W5,D3,L1,V1,M1} R(8773,20) { artifact( skol4, skol5
% 3.17/3.54 ( skol4, X ) ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := skol4
% 3.17/3.54 Y := skol5( skol4, X )
% 3.17/3.54 end
% 3.17/3.54 substitution1:
% 3.17/3.54 X := X
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 subsumption: (8830) {G5,W5,D3,L1,V1,M1} R(8803,19) { object( skol4, skol5(
% 3.17/3.54 skol4, X ) ) }.
% 3.17/3.54 parent0: (20267) {G1,W5,D3,L1,V1,M1} { object( skol4, skol5( skol4, X ) )
% 3.17/3.54 }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := X
% 3.17/3.54 end
% 3.17/3.54 permutation0:
% 3.17/3.54 0 ==> 0
% 3.17/3.54 end
% 3.17/3.54
% 3.17/3.54 resolution: (20268) {G2,W5,D3,L1,V1,M1} { ! living( skol4, skol5( skol4, X
% 3.17/3.54 ) ) }.
% 3.17/3.54 parent0[0]: (165) {G1,W6,D2,L2,V2,M2} R(17,52) { ! object( X, Y ), ! living
% 3.17/3.54 ( X, Y ) }.
% 3.17/3.54 parent1[0]: (8830) {G5,W5,D3,L1,V1,M1} R(8803,19) { object( skol4, skol5(
% 3.17/3.54 skol4, X ) ) }.
% 3.17/3.54 substitution0:
% 3.17/3.54 X := skol4
% 3.17/3.54 Y := skol5( skol4, X )Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------