%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : MED001+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n019.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 : Sun Jul 17 16:51:40 EDT 2022
% Result : Theorem 0.73s 1.38s
% Output : Refutation 0.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : MED001+1 : TPTP v8.1.0. Released v3.2.0.
% 0.07/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Tue Jul 5 01:42:53 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.73/1.38 *** allocated 10000 integers for termspace/termends
% 0.73/1.38 *** allocated 10000 integers for clauses
% 0.73/1.38 *** allocated 10000 integers for justifications
% 0.73/1.38 Bliksem 1.12
% 0.73/1.38
% 0.73/1.38
% 0.73/1.38 Automatic Strategy Selection
% 0.73/1.38
% 0.73/1.38
% 0.73/1.38 Clauses:
% 0.73/1.38
% 0.73/1.38 { ! gt( X, X ) }.
% 0.73/1.38 { ! gt( X, Z ), ! gt( Z, Y ), gt( X, Y ) }.
% 0.73/1.38 { bcapacityne( X ), bcapacityex( X ), bcapacitysn( X ) }.
% 0.73/1.38 { ! bcapacityne( X ), ! bcapacityex( X ) }.
% 0.73/1.38 { ! bcapacityne( X ), ! bcapacitysn( X ) }.
% 0.73/1.38 { ! bcapacityex( X ), ! bcapacitysn( X ) }.
% 0.73/1.38 { conditionhyper( X ), conditionhypo( X ), conditionnormo( X ) }.
% 0.73/1.38 { ! conditionhyper( X ), ! conditionhypo( X ) }.
% 0.73/1.38 { ! conditionhyper( X ), ! conditionnormo( X ) }.
% 0.73/1.38 { ! conditionhypo( X ), ! conditionnormo( X ) }.
% 0.73/1.38 { alpha1( X ), gt( X, Y ), uptakelg( Y ) }.
% 0.73/1.38 { alpha1( X ), gt( X, Y ), uptakepg( Y ) }.
% 0.73/1.38 { ! alpha1( X ), ! drugi( skol1( Y ) ) }.
% 0.73/1.38 { ! alpha1( X ), ! gt( X, skol1( X ) ) }.
% 0.73/1.38 { gt( X, Y ), drugi( Y ), alpha1( X ) }.
% 0.73/1.38 { gt( Y, X ), ! uptakelg( X ), ! releaselg( X ) }.
% 0.73/1.38 { ! drugsu( skol2( Y ) ), bcapacityex( X ), gt( X, Z ), bsecretioni( Z ) }
% 0.73/1.38 .
% 0.73/1.38 { ! gt( X, skol2( X ) ), bcapacityex( X ), gt( X, Y ), bsecretioni( Y ) }.
% 0.73/1.38 { ! drugbg( skol3( Y ) ), gt( X, Z ), ! releaselg( Z ) }.
% 0.73/1.38 { ! gt( X, skol3( X ) ), gt( X, Y ), ! releaselg( Y ) }.
% 0.73/1.38 { alpha2( X ), ! qilt27( X ), ! conditionhyper( skol4( Y ) ), gt( X, Z ),
% 0.73/1.38 conditionnormo( Z ) }.
% 0.73/1.38 { alpha2( X ), ! qilt27( X ), gt( X, skol4( X ) ), gt( X, Y ),
% 0.73/1.38 conditionnormo( Y ) }.
% 0.73/1.38 { ! alpha2( X ), ! bsecretioni( skol5( Y ) ), ! bcapacitysn( X ) }.
% 0.73/1.38 { ! alpha2( X ), ! gt( X, skol5( X ) ), ! bcapacitysn( X ) }.
% 0.73/1.38 { gt( X, Y ), bsecretioni( Y ), alpha2( X ) }.
% 0.73/1.38 { bcapacitysn( X ), alpha2( X ) }.
% 0.73/1.38 { alpha3( X ), qilt27( X ), ! conditionhyper( skol6( Y ) ), gt( X, Z ),
% 0.73/1.38 conditionnormo( Z ) }.
% 0.73/1.38 { alpha3( X ), qilt27( X ), gt( X, skol6( X ) ), gt( X, Y ), conditionnormo
% 0.73/1.38 ( Y ) }.
% 0.73/1.38 { ! alpha3( X ), releaselg( skol7( Y ) ), ! bcapacitysn( X ) }.
% 0.73/1.38 { ! alpha3( X ), ! gt( X, skol7( X ) ), ! bcapacitysn( X ) }.
% 0.73/1.38 { gt( X, Y ), ! releaselg( Y ), alpha3( X ) }.
% 0.73/1.38 { bcapacitysn( X ), alpha3( X ) }.
% 0.73/1.38 { alpha4( X ), ! conditionhyper( skol8( Y ) ), gt( X, Z ), conditionnormo(
% 0.73/1.38 Z ) }.
% 0.73/1.38 { alpha4( X ), gt( X, skol8( X ) ), gt( X, Y ), conditionnormo( Y ) }.
% 0.73/1.38 { ! alpha4( X ), alpha6( X ), ! bsecretioni( skol9( Y ) ) }.
% 0.73/1.38 { ! alpha4( X ), alpha6( X ), ! gt( X, skol9( X ) ) }.
% 0.73/1.38 { ! alpha6( X ), alpha4( X ) }.
% 0.73/1.38 { gt( X, Y ), bsecretioni( Y ), alpha4( X ) }.
% 0.73/1.38 { ! alpha6( X ), alpha8( X ), ! bcapacityne( X ) }.
% 0.73/1.38 { ! alpha8( X ), alpha6( X ) }.
% 0.73/1.38 { bcapacityne( X ), alpha6( X ) }.
% 0.73/1.38 { ! alpha8( X ), alpha10( X ) }.
% 0.73/1.38 { ! alpha8( X ), ! uptakepg( skol10( Y ) ) }.
% 0.73/1.38 { ! alpha8( X ), ! gt( X, skol10( X ) ) }.
% 0.73/1.38 { ! alpha10( X ), gt( X, Y ), uptakepg( Y ), alpha8( X ) }.
% 0.73/1.38 { ! alpha10( X ), releaselg( skol11( Y ) ) }.
% 0.73/1.38 { ! alpha10( X ), ! gt( X, skol11( X ) ) }.
% 0.73/1.38 { gt( X, Y ), ! releaselg( Y ), alpha10( X ) }.
% 0.73/1.38 { alpha5( X ), ! conditionhyper( skol12( Y ) ), gt( X, Z ), conditionnormo
% 0.73/1.38 ( Z ), conditionhypo( Z ) }.
% 0.73/1.38 { alpha5( X ), gt( X, skol12( X ) ), gt( X, Y ), conditionnormo( Y ),
% 0.73/1.38 conditionhypo( Y ) }.
% 0.73/1.38 { ! alpha5( X ), alpha7( X ), ! bcapacityex( X ) }.
% 0.73/1.38 { ! alpha7( X ), alpha5( X ) }.
% 0.73/1.38 { bcapacityex( X ), alpha5( X ) }.
% 0.73/1.38 { ! alpha7( X ), alpha9( X ), ! uptakepg( skol13( Y ) ) }.
% 0.73/1.38 { ! alpha7( X ), alpha9( X ), ! gt( X, skol13( X ) ) }.
% 0.73/1.38 { ! alpha9( X ), alpha7( X ) }.
% 0.73/1.38 { gt( X, Y ), uptakepg( Y ), alpha7( X ) }.
% 0.73/1.38 { ! alpha9( X ), ! uptakelg( skol14( Y ) ) }.
% 0.73/1.38 { ! alpha9( X ), ! gt( X, skol14( X ) ) }.
% 0.73/1.38 { gt( X, Y ), uptakelg( Y ), alpha9( X ) }.
% 0.73/1.38 { gt( n0, X ), drugsu( X ) }.
% 0.73/1.38 { ! gt( n0, X ), conditionhyper( X ) }.
% 0.73/1.38 { bcapacitysn( n0 ) }.
% 0.73/1.38 { qilt27( n0 ) }.
% 0.73/1.38 { ! gt( n0, skol15 ) }.
% 0.73/1.38 { ! conditionnormo( skol15 ) }.
% 0.73/1.38
% 0.73/1.38 percentage equality = 0.000000, percentage horn = 0.590909
% 0.73/1.38 This a non-horn, non-equality problem
% 0.73/1.38
% 0.73/1.38
% 0.73/1.38 Options Used:
% 0.73/1.38
% 0.73/1.38 useres = 1
% 0.73/1.38 useparamod = 0
% 0.73/1.38 useeqrefl = 0
% 0.73/1.38 useeqfact = 0
% 0.73/1.38 usefactor = 1
% 0.73/1.38 usesimpsplitting = 0
% 0.73/1.38 usesimpdemod = 0
% 0.73/1.38 usesimpres = 3
% 0.73/1.38
% 0.73/1.38 resimpinuse = 1000
% 0.73/1.38 resimpclauses = 20000
% 0.73/1.38 substype = standard
% 0.73/1.38 backwardsubs = 1
% 0.73/1.38 selectoldest = 5
% 0.73/1.38
% 0.73/1.38 litorderings [0] = split
% 0.73/1.38 litorderings [1] = liftord
% 0.73/1.38
% 0.73/1.38 termordering = none
% 0.73/1.38
% 0.73/1.38 litapriori = 1
% 0.73/1.38 termapriori = 0
% 0.73/1.38 litaposteriori = 0
% 0.73/1.38 termaposteriori = 0
% 0.73/1.38 demodaposteriori = 0
% 0.73/1.38 ordereqreflfact = 0
% 0.73/1.38
% 0.73/1.38 litselect = none
% 0.73/1.38
% 0.73/1.38 maxweight = 15
% 0.73/1.38 maxdepth = 30000
% 0.73/1.38 maxlength = 115
% 0.73/1.38 maxnrvars = 195
% 0.73/1.38 excuselevel = 1
% 0.73/1.38 increasemaxweight = 1
% 0.73/1.38
% 0.73/1.38 maxselected = 10000000
% 0.73/1.38 maxnrclauses = 10000000
% 0.73/1.38
% 0.73/1.38 showgenerated = 0
% 0.73/1.38 showkept = 0
% 0.73/1.38 showselected = 0
% 0.73/1.38 showdeleted = 0
% 0.73/1.38 showresimp = 1
% 0.73/1.38 showstatus = 2000
% 0.73/1.38
% 0.73/1.38 prologoutput = 0
% 0.73/1.38 nrgoals = 5000000
% 0.73/1.38 totalproof = 1
% 0.73/1.38
% 0.73/1.38 Symbols occurring in the translation:
% 0.73/1.38
% 0.73/1.38 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.73/1.38 . [1, 2] (w:1, o:56, a:1, s:1, b:0),
% 0.73/1.38 ! [4, 1] (w:0, o:13, a:1, s:1, b:0),
% 0.73/1.38 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.38 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.38 gt [36, 2] (w:1, o:80, a:1, s:1, b:0),
% 0.73/1.38 bcapacityne [40, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.73/1.38 bcapacityex [41, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.73/1.38 bcapacitysn [42, 1] (w:1, o:30, a:1, s:1, b:0),
% 0.73/1.38 conditionhyper [43, 1] (w:1, o:32, a:1, s:1, b:0),
% 0.73/1.38 conditionhypo [44, 1] (w:1, o:33, a:1, s:1, b:0),
% 0.73/1.38 conditionnormo [45, 1] (w:1, o:34, a:1, s:1, b:0),
% 0.73/1.38 drugi [47, 1] (w:1, o:35, a:1, s:1, b:0),
% 0.73/1.38 uptakelg [48, 1] (w:1, o:36, a:1, s:1, b:0),
% 0.73/1.38 uptakepg [49, 1] (w:1, o:37, a:1, s:1, b:0),
% 0.73/1.38 releaselg [50, 1] (w:1, o:39, a:1, s:1, b:0),
% 0.73/1.38 drugsu [51, 1] (w:1, o:40, a:1, s:1, b:0),
% 0.73/1.38 bsecretioni [52, 1] (w:1, o:31, a:1, s:1, b:0),
% 0.73/1.38 drugbg [53, 1] (w:1, o:41, a:1, s:1, b:0),
% 0.73/1.38 qilt27 [54, 1] (w:1, o:38, a:1, s:1, b:0),
% 0.73/1.38 n0 [55, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.73/1.38 alpha1 [56, 1] (w:1, o:18, a:1, s:1, b:0),
% 0.73/1.38 alpha2 [57, 1] (w:1, o:20, a:1, s:1, b:0),
% 0.73/1.38 alpha3 [58, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.73/1.38 alpha4 [59, 1] (w:1, o:22, a:1, s:1, b:0),
% 0.73/1.38 alpha5 [60, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.73/1.38 alpha6 [61, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.73/1.38 alpha7 [62, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.73/1.38 alpha8 [63, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.73/1.38 alpha9 [64, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.73/1.38 alpha10 [65, 1] (w:1, o:19, a:1, s:1, b:0),
% 0.73/1.38 skol1 [66, 1] (w:1, o:42, a:1, s:1, b:0),
% 0.73/1.38 skol2 [67, 1] (w:1, o:48, a:1, s:1, b:0),
% 0.73/1.38 skol3 [68, 1] (w:1, o:49, a:1, s:1, b:0),
% 0.73/1.38 skol4 [69, 1] (w:1, o:50, a:1, s:1, b:0),
% 0.73/1.38 skol5 [70, 1] (w:1, o:51, a:1, s:1, b:0),
% 0.73/1.38 skol6 [71, 1] (w:1, o:52, a:1, s:1, b:0),
% 0.73/1.38 skol7 [72, 1] (w:1, o:53, a:1, s:1, b:0),
% 0.73/1.38 skol8 [73, 1] (w:1, o:54, a:1, s:1, b:0),
% 0.73/1.38 skol9 [74, 1] (w:1, o:55, a:1, s:1, b:0),
% 0.73/1.38 skol10 [75, 1] (w:1, o:43, a:1, s:1, b:0),
% 0.73/1.38 skol11 [76, 1] (w:1, o:44, a:1, s:1, b:0),
% 0.73/1.38 skol12 [77, 1] (w:1, o:45, a:1, s:1, b:0),
% 0.73/1.38 skol13 [78, 1] (w:1, o:46, a:1, s:1, b:0),
% 0.73/1.38 skol14 [79, 1] (w:1, o:47, a:1, s:1, b:0),
% 0.73/1.38 skol15 [80, 0] (w:1, o:12, a:1, s:1, b:0).
% 0.73/1.38
% 0.73/1.38
% 0.73/1.38 Starting Search:
% 0.73/1.38
% 0.73/1.38 *** allocated 15000 integers for clauses
% 0.73/1.38 *** allocated 22500 integers for clauses
% 0.73/1.38 *** allocated 33750 integers for clauses
% 0.73/1.38 *** allocated 15000 integers for termspace/termends
% 0.73/1.38 *** allocated 50625 integers for clauses
% 0.73/1.38 Resimplifying inuse:
% 0.73/1.38 Done
% 0.73/1.38
% 0.73/1.38 *** allocated 22500 integers for termspace/termends
% 0.73/1.38 *** allocated 75937 integers for clauses
% 0.73/1.38 *** allocated 33750 integers for termspace/termends
% 0.73/1.38
% 0.73/1.38 Intermediate Status:
% 0.73/1.38 Generated: 4550
% 0.73/1.38 Kept: 2000
% 0.73/1.38 Inuse: 353
% 0.73/1.38 Deleted: 40
% 0.73/1.38 Deletedinuse: 5
% 0.73/1.38
% 0.73/1.38 Resimplifying inuse:
% 0.73/1.38 Done
% 0.73/1.38
% 0.73/1.38 *** allocated 113905 integers for clauses
% 0.73/1.38 *** allocated 50625 integers for termspace/termends
% 0.73/1.38 Resimplifying inuse:
% 0.73/1.38 Done
% 0.73/1.38
% 0.73/1.38 *** allocated 170857 integers for clauses
% 0.73/1.38 *** allocated 75937 integers for termspace/termends
% 0.73/1.38
% 0.73/1.38 Intermediate Status:
% 0.73/1.38 Generated: 11949
% 0.73/1.38 Kept: 4011
% 0.73/1.38 Inuse: 545
% 0.73/1.38 Deleted: 135
% 0.73/1.38 Deletedinuse: 33
% 0.73/1.38
% 0.73/1.38 Resimplifying inuse:
% 0.73/1.38 Done
% 0.73/1.38
% 0.73/1.38 *** allocated 256285 integers for clauses
% 0.73/1.38 Resimplifying inuse:
% 0.73/1.38 Done
% 0.73/1.38
% 0.73/1.38 *** allocated 113905 integers for termspace/termends
% 0.73/1.38
% 0.73/1.38 Bliksems!, er is een bewijs:
% 0.73/1.38 % SZS status Theorem
% 0.73/1.38 % SZS output start Refutation
% 0.73/1.38
% 0.73/1.38 (5) {G0,W4,D2,L2,V1,M1} I { ! bcapacityex( X ), ! bcapacitysn( X ) }.
% 0.73/1.38 (16) {G0,W10,D3,L4,V3,M1} I { bcapacityex( X ), ! drugsu( skol2( Y ) ),
% 0.73/1.38 bsecretioni( Z ), gt( X, Z ) }.
% 0.73/1.38 (17) {G0,W11,D3,L4,V2,M2} I { bcapacityex( X ), bsecretioni( Y ), ! gt( X,
% 0.73/1.38 skol2( X ) ), gt( X, Y ) }.
% 0.73/1.38 (20) {G0,W12,D3,L5,V3,M1} I { alpha2( X ), ! conditionhyper( skol4( Y ) ),
% 0.73/1.38 ! qilt27( X ), conditionnormo( Z ), gt( X, Z ) }.
% 0.73/1.38 (21) {G0,W13,D3,L5,V2,M2} I { alpha2( X ), ! qilt27( X ), conditionnormo( Y
% 0.73/1.38 ), gt( X, skol4( X ) ), gt( X, Y ) }.
% 0.73/1.38 (22) {G0,W7,D3,L3,V2,M1} I { ! alpha2( X ), ! bcapacitysn( X ), !
% 0.73/1.38 bsecretioni( skol5( Y ) ) }.
% 0.73/1.38 (23) {G0,W8,D3,L3,V1,M1} I { ! alpha2( X ), ! bcapacitysn( X ), ! gt( X,
% 0.73/1.38 skol5( X ) ) }.
% 0.73/1.38 (60) {G0,W5,D2,L2,V1,M1} I { drugsu( X ), gt( n0, X ) }.
% 0.73/1.38 (61) {G0,W5,D2,L2,V1,M1} I { conditionhyper( X ), ! gt( n0, X ) }.
% 0.73/1.38 (62) {G0,W2,D2,L1,V0,M1} I { bcapacitysn( n0 ) }.
% 0.73/1.38 (63) {G0,W2,D2,L1,V0,M1} I { qilt27( n0 ) }.
% 0.73/1.38 (64) {G0,W3,D2,L1,V0,M1} I { ! gt( n0, skol15 ) }.
% 0.73/1.38 (65) {G0,W2,D2,L1,V0,M1} I { ! conditionnormo( skol15 ) }.
% 0.73/1.38 (84) {G1,W2,D2,L1,V0,M1} R(5,62) { ! bcapacityex( n0 ) }.
% 0.73/1.38 (172) {G2,W8,D3,L3,V1,M1} R(17,60);r(84) { bsecretioni( X ), drugsu( skol2
% 0.73/1.38 ( n0 ) ), gt( n0, X ) }.
% 0.73/1.38 (226) {G1,W7,D3,L3,V1,M1} R(20,64);r(63) { alpha2( n0 ), ! conditionhyper(
% 0.73/1.38 skol4( X ) ), conditionnormo( skol15 ) }.
% 0.73/1.38 (261) {G1,W8,D3,L3,V0,M1} R(21,64);r(63) { alpha2( n0 ), conditionnormo(
% 0.73/1.38 skol15 ), gt( n0, skol4( n0 ) ) }.
% 0.73/1.38 (304) {G1,W10,D3,L4,V2,M1} R(23,16);r(5) { ! alpha2( X ), ! bcapacitysn( X
% 0.73/1.38 ), bsecretioni( skol5( X ) ), ! drugsu( skol2( Y ) ) }.
% 0.73/1.38 (1929) {G2,W5,D3,L2,V1,M1} S(226);r(65) { alpha2( n0 ), ! conditionhyper(
% 0.73/1.38 skol4( X ) ) }.
% 0.73/1.38 (1983) {G3,W8,D3,L3,V0,M1} R(172,23);r(62) { bsecretioni( skol5( n0 ) ), !
% 0.73/1.38 alpha2( n0 ), drugsu( skol2( n0 ) ) }.
% 0.73/1.38 (3469) {G2,W6,D3,L2,V0,M1} S(261);r(65) { alpha2( n0 ), gt( n0, skol4( n0 )
% 0.73/1.38 ) }.
% 0.73/1.38 (3506) {G3,W2,D2,L1,V0,M1} R(3469,61);r(1929) { alpha2( n0 ) }.
% 0.73/1.38 (4065) {G4,W6,D3,L2,V0,M1} S(1983);r(3506) { bsecretioni( skol5( n0 ) ),
% 0.73/1.38 drugsu( skol2( n0 ) ) }.
% 0.73/1.38 (5942) {G5,W10,D3,L4,V1,M2} R(304,4065) { ! alpha2( X ), ! bcapacitysn( X )
% 0.73/1.38 , bsecretioni( skol5( n0 ) ), bsecretioni( skol5( X ) ) }.
% 0.73/1.38 (5970) {G6,W5,D3,L2,V0,M1} F(5942);r(3506) { ! bcapacitysn( n0 ),
% 0.73/1.38 bsecretioni( skol5( n0 ) ) }.
% 0.73/1.38 (5971) {G7,W3,D3,L1,V0,M1} S(5970);r(62) { bsecretioni( skol5( n0 ) ) }.
% 0.73/1.38 (5972) {G8,W4,D2,L2,V1,M1} R(5971,22) { ! alpha2( X ), ! bcapacitysn( X )
% 0.73/1.38 }.
% 0.73/1.38 (5975) {G9,W0,D0,L0,V0,M0} R(5972,62);r(3506) { }.
% 0.73/1.38
% 0.73/1.38
% 0.73/1.38 % SZS output end Refutation
% 0.73/1.38 found a proof!
% 0.73/1.38
% 0.73/1.38
% 0.73/1.38 Unprocessed initial clauses:
% 0.73/1.38
% 0.73/1.38 (5977) {G0,W3,D2,L1,V1,M1} { ! gt( X, X ) }.
% 0.73/1.38 (5978) {G0,W9,D2,L3,V3,M3} { ! gt( X, Z ), ! gt( Z, Y ), gt( X, Y ) }.
% 0.73/1.38 (5979) {G0,W6,D2,L3,V1,M3} { bcapacityne( X ), bcapacityex( X ),
% 0.73/1.38 bcapacitysn( X ) }.
% 0.73/1.38 (5980) {G0,W4,D2,L2,V1,M2} { ! bcapacityne( X ), ! bcapacityex( X ) }.
% 0.73/1.38 (5981) {G0,W4,D2,L2,V1,M2} { ! bcapacityne( X ), ! bcapacitysn( X ) }.
% 0.73/1.38 (5982) {G0,W4,D2,L2,V1,M2} { ! bcapacityex( X ), ! bcapacitysn( X ) }.
% 0.73/1.38 (5983) {G0,W6,D2,L3,V1,M3} { conditionhyper( X ), conditionhypo( X ),
% 0.73/1.38 conditionnormo( X ) }.
% 0.73/1.38 (5984) {G0,W4,D2,L2,V1,M2} { ! conditionhyper( X ), ! conditionhypo( X )
% 0.73/1.38 }.
% 0.73/1.38 (5985) {G0,W4,D2,L2,V1,M2} { ! conditionhyper( X ), ! conditionnormo( X )
% 0.73/1.38 }.
% 0.73/1.38 (5986) {G0,W4,D2,L2,V1,M2} { ! conditionhypo( X ), ! conditionnormo( X )
% 0.73/1.38 }.
% 0.73/1.38 (5987) {G0,W7,D2,L3,V2,M3} { alpha1( X ), gt( X, Y ), uptakelg( Y ) }.
% 0.73/1.38 (5988) {G0,W7,D2,L3,V2,M3} { alpha1( X ), gt( X, Y ), uptakepg( Y ) }.
% 0.73/1.38 (5989) {G0,W5,D3,L2,V2,M2} { ! alpha1( X ), ! drugi( skol1( Y ) ) }.
% 0.73/1.38 (5990) {G0,W6,D3,L2,V1,M2} { ! alpha1( X ), ! gt( X, skol1( X ) ) }.
% 0.73/1.38 (5991) {G0,W7,D2,L3,V2,M3} { gt( X, Y ), drugi( Y ), alpha1( X ) }.
% 0.73/1.38 (5992) {G0,W7,D2,L3,V2,M3} { gt( Y, X ), ! uptakelg( X ), ! releaselg( X )
% 0.73/1.38 }.
% 0.73/1.38 (5993) {G0,W10,D3,L4,V3,M4} { ! drugsu( skol2( Y ) ), bcapacityex( X ), gt
% 0.73/1.38 ( X, Z ), bsecretioni( Z ) }.
% 0.73/1.38 (5994) {G0,W11,D3,L4,V2,M4} { ! gt( X, skol2( X ) ), bcapacityex( X ), gt
% 0.73/1.38 ( X, Y ), bsecretioni( Y ) }.
% 0.73/1.38 (5995) {G0,W8,D3,L3,V3,M3} { ! drugbg( skol3( Y ) ), gt( X, Z ), !
% 0.73/1.38 releaselg( Z ) }.
% 0.73/1.38 (5996) {G0,W9,D3,L3,V2,M3} { ! gt( X, skol3( X ) ), gt( X, Y ), !
% 0.73/1.38 releaselg( Y ) }.
% 0.73/1.38 (5997) {G0,W12,D3,L5,V3,M5} { alpha2( X ), ! qilt27( X ), ! conditionhyper
% 0.73/1.38 ( skol4( Y ) ), gt( X, Z ), conditionnormo( Z ) }.
% 0.73/1.38 (5998) {G0,W13,D3,L5,V2,M5} { alpha2( X ), ! qilt27( X ), gt( X, skol4( X
% 0.73/1.38 ) ), gt( X, Y ), conditionnormo( Y ) }.
% 0.73/1.38 (5999) {G0,W7,D3,L3,V2,M3} { ! alpha2( X ), ! bsecretioni( skol5( Y ) ), !
% 0.73/1.38 bcapacitysn( X ) }.
% 0.73/1.38 (6000) {G0,W8,D3,L3,V1,M3} { ! alpha2( X ), ! gt( X, skol5( X ) ), !
% 0.73/1.38 bcapacitysn( X ) }.
% 0.73/1.38 (6001) {G0,W7,D2,L3,V2,M3} { gt( X, Y ), bsecretioni( Y ), alpha2( X ) }.
% 0.73/1.38 (6002) {G0,W4,D2,L2,V1,M2} { bcapacitysn( X ), alpha2( X ) }.
% 0.73/1.38 (6003) {G0,W12,D3,L5,V3,M5} { alpha3( X ), qilt27( X ), ! conditionhyper(
% 0.73/1.38 skol6( Y ) ), gt( X, Z ), conditionnormo( Z ) }.
% 0.73/1.38 (6004) {G0,W13,D3,L5,V2,M5} { alpha3( X ), qilt27( X ), gt( X, skol6( X )
% 0.73/1.38 ), gt( X, Y ), conditionnormo( Y ) }.
% 0.73/1.38 (6005) {G0,W7,D3,L3,V2,M3} { ! alpha3( X ), releaselg( skol7( Y ) ), !
% 0.73/1.38 bcapacitysn( X ) }.
% 0.73/1.38 (6006) {G0,W8,D3,L3,V1,M3} { ! alpha3( X ), ! gt( X, skol7( X ) ), !
% 0.73/1.38 bcapacitysn( X ) }.
% 0.73/1.38 (6007) {G0,W7,D2,L3,V2,M3} { gt( X, Y ), ! releaselg( Y ), alpha3( X ) }.
% 0.73/1.38 (6008) {G0,W4,D2,L2,V1,M2} { bcapacitysn( X ), alpha3( X ) }.
% 0.73/1.38 (6009) {G0,W10,D3,L4,V3,M4} { alpha4( X ), ! conditionhyper( skol8( Y ) )
% 0.73/1.38 , gt( X, Z ), conditionnormo( Z ) }.
% 0.73/1.38 (6010) {G0,W11,D3,L4,V2,M4} { alpha4( X ), gt( X, skol8( X ) ), gt( X, Y )
% 0.73/1.38 , conditionnormo( Y ) }.
% 0.73/1.38 (6011) {G0,W7,D3,L3,V2,M3} { ! alpha4( X ), alpha6( X ), ! bsecretioni(
% 0.73/1.38 skol9( Y ) ) }.
% 0.73/1.38 (6012) {G0,W8,D3,L3,V1,M3} { ! alpha4( X ), alpha6( X ), ! gt( X, skol9( X
% 0.73/1.38 ) ) }.
% 0.73/1.38 (6013) {G0,W4,D2,L2,V1,M2} { ! alpha6( X ), alpha4( X ) }.
% 0.73/1.38 (6014) {G0,W7,D2,L3,V2,M3} { gt( X, Y ), bsecretioni( Y ), alpha4( X ) }.
% 0.73/1.38 (6015) {G0,W6,D2,L3,V1,M3} { ! alpha6( X ), alpha8( X ), ! bcapacityne( X
% 0.73/1.38 ) }.
% 0.73/1.38 (6016) {G0,W4,D2,L2,V1,M2} { ! alpha8( X ), alpha6( X ) }.
% 0.73/1.38 (6017) {G0,W4,D2,L2,V1,M2} { bcapacityne( X ), alpha6( X ) }.
% 0.73/1.38 (6018) {G0,W4,D2,L2,V1,M2} { ! alpha8( X ), alpha10( X ) }.
% 0.73/1.38 (6019) {G0,W5,D3,L2,V2,M2} { ! alpha8( X ), ! uptakepg( skol10( Y ) ) }.
% 0.73/1.38 (6020) {G0,W6,D3,L2,V1,M2} { ! alpha8( X ), ! gt( X, skol10( X ) ) }.
% 0.73/1.38 (6021) {G0,W9,D2,L4,V2,M4} { ! alpha10( X ), gt( X, Y ), uptakepg( Y ),
% 0.73/1.38 alpha8( X ) }.
% 0.73/1.38 (6022) {G0,W5,D3,L2,V2,M2} { ! alpha10( X ), releaselg( skol11( Y ) ) }.
% 0.73/1.38 (6023) {G0,W6,D3,L2,V1,M2} { ! alpha10( X ), ! gt( X, skol11( X ) ) }.
% 0.73/1.38 (6024) {G0,W7,D2,L3,V2,M3} { gt( X, Y ), ! releaselg( Y ), alpha10( X )
% 0.73/1.38 }.
% 0.73/1.38 (6025) {G0,W12,D3,L5,V3,M5} { alpha5( X ), ! conditionhyper( skol12( Y ) )
% 0.73/1.38 , gt( X, Z ), conditionnormo( Z ), conditionhypo( Z ) }.
% 0.73/1.38 (6026) {G0,W13,D3,L5,V2,M5} { alpha5( X ), gt( X, skol12( X ) ), gt( X, Y
% 0.73/1.38 ), conditionnormo( Y ), conditionhypo( Y ) }.
% 0.73/1.38 (6027) {G0,W6,D2,L3,V1,M3} { ! alpha5( X ), alpha7( X ), ! bcapacityex( X
% 0.73/1.38 ) }.
% 0.73/1.38 (6028) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), alpha5( X ) }.
% 0.73/1.38 (6029) {G0,W4,D2,L2,V1,M2} { bcapacityex( X ), alpha5( X ) }.
% 0.73/1.38 (6030) {G0,W7,D3,L3,V2,M3} { ! alpha7( X ), alpha9( X ), ! uptakepg(
% 0.73/1.38 skol13( Y ) ) }.
% 0.73/1.38 (6031) {G0,W8,D3,L3,V1,M3} { ! alpha7( X ), alpha9( X ), ! gt( X, skol13(
% 0.73/1.38 X ) ) }.
% 0.73/1.38 (6032) {G0,W4,D2,L2,V1,M2} { ! alpha9( X ), alpha7( X ) }.
% 0.73/1.38 (6033) {G0,W7,D2,L3,V2,M3} { gt( X, Y ), uptakepg( Y ), alpha7( X ) }.
% 0.73/1.38 (6034) {G0,W5,D3,L2,V2,M2} { ! alpha9( X ), ! uptakelg( skol14( Y ) ) }.
% 0.73/1.38 (6035) {G0,W6,D3,L2,V1,M2} { ! alpha9( X ), ! gt( X, skol14( X ) ) }.
% 0.73/1.38 (6036) {G0,W7,D2,L3,V2,M3} { gt( X, Y ), uptakelg( Y ), alpha9( X ) }.
% 0.73/1.38 (6037) {G0,W5,D2,L2,V1,M2} { gt( n0, X ), drugsu( X ) }.
% 0.73/1.38 (6038) {G0,W5,D2,L2,V1,M2} { ! gt( n0, X ), conditionhyper( X ) }.
% 0.73/1.38 (6039) {G0,W2,D2,L1,V0,M1} { bcapacitysn( n0 ) }.
% 0.73/1.38 (6040) {G0,W2,D2,L1,V0,M1} { qilt27( n0 ) }.
% 0.73/1.38 (6041) {G0,W3,D2,L1,V0,M1} { ! gt( n0, skol15 ) }.
% 0.73/1.38 (6042) {G0,W2,D2,L1,V0,M1} { ! conditionnormo( skol15 ) }.
% 0.73/1.38
% 0.73/1.38
% 0.73/1.38 Total Proof:
% 0.73/1.38
% 0.73/1.38 subsumption: (5) {G0,W4,D2,L2,V1,M1} I { ! bcapacityex( X ), ! bcapacitysn
% 0.73/1.38 ( X ) }.
% 0.73/1.38 parent0: (5982) {G0,W4,D2,L2,V1,M2} { ! bcapacityex( X ), ! bcapacitysn( X
% 0.73/1.38 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (16) {G0,W10,D3,L4,V3,M1} I { bcapacityex( X ), ! drugsu(
% 0.73/1.38 skol2( Y ) ), bsecretioni( Z ), gt( X, Z ) }.
% 0.73/1.38 parent0: (5993) {G0,W10,D3,L4,V3,M4} { ! drugsu( skol2( Y ) ), bcapacityex
% 0.73/1.38 ( X ), gt( X, Z ), bsecretioni( Z ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 Y := Y
% 0.73/1.38 Z := Z
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 1
% 0.73/1.38 1 ==> 0
% 0.73/1.38 2 ==> 3
% 0.73/1.38 3 ==> 2
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (17) {G0,W11,D3,L4,V2,M2} I { bcapacityex( X ), bsecretioni( Y
% 0.73/1.38 ), ! gt( X, skol2( X ) ), gt( X, Y ) }.
% 0.73/1.38 parent0: (5994) {G0,W11,D3,L4,V2,M4} { ! gt( X, skol2( X ) ), bcapacityex
% 0.73/1.38 ( X ), gt( X, Y ), bsecretioni( Y ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 Y := Y
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 2
% 0.73/1.38 1 ==> 0
% 0.73/1.38 2 ==> 3
% 0.73/1.38 3 ==> 1
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (20) {G0,W12,D3,L5,V3,M1} I { alpha2( X ), ! conditionhyper(
% 0.73/1.38 skol4( Y ) ), ! qilt27( X ), conditionnormo( Z ), gt( X, Z ) }.
% 0.73/1.38 parent0: (5997) {G0,W12,D3,L5,V3,M5} { alpha2( X ), ! qilt27( X ), !
% 0.73/1.38 conditionhyper( skol4( Y ) ), gt( X, Z ), conditionnormo( Z ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 Y := Y
% 0.73/1.38 Z := Z
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 2
% 0.73/1.38 2 ==> 1
% 0.73/1.38 3 ==> 4
% 0.73/1.38 4 ==> 3
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (21) {G0,W13,D3,L5,V2,M2} I { alpha2( X ), ! qilt27( X ),
% 0.73/1.38 conditionnormo( Y ), gt( X, skol4( X ) ), gt( X, Y ) }.
% 0.73/1.38 parent0: (5998) {G0,W13,D3,L5,V2,M5} { alpha2( X ), ! qilt27( X ), gt( X,
% 0.73/1.38 skol4( X ) ), gt( X, Y ), conditionnormo( Y ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 Y := Y
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 2 ==> 3
% 0.73/1.38 3 ==> 4
% 0.73/1.38 4 ==> 2
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (22) {G0,W7,D3,L3,V2,M1} I { ! alpha2( X ), ! bcapacitysn( X )
% 0.73/1.38 , ! bsecretioni( skol5( Y ) ) }.
% 0.73/1.38 parent0: (5999) {G0,W7,D3,L3,V2,M3} { ! alpha2( X ), ! bsecretioni( skol5
% 0.73/1.38 ( Y ) ), ! bcapacitysn( X ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 Y := Y
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 2
% 0.73/1.38 2 ==> 1
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (23) {G0,W8,D3,L3,V1,M1} I { ! alpha2( X ), ! bcapacitysn( X )
% 0.73/1.38 , ! gt( X, skol5( X ) ) }.
% 0.73/1.38 parent0: (6000) {G0,W8,D3,L3,V1,M3} { ! alpha2( X ), ! gt( X, skol5( X ) )
% 0.73/1.38 , ! bcapacitysn( X ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 2
% 0.73/1.38 2 ==> 1
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (60) {G0,W5,D2,L2,V1,M1} I { drugsu( X ), gt( n0, X ) }.
% 0.73/1.38 parent0: (6037) {G0,W5,D2,L2,V1,M2} { gt( n0, X ), drugsu( X ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 1
% 0.73/1.38 1 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (61) {G0,W5,D2,L2,V1,M1} I { conditionhyper( X ), ! gt( n0, X
% 0.73/1.38 ) }.
% 0.73/1.38 parent0: (6038) {G0,W5,D2,L2,V1,M2} { ! gt( n0, X ), conditionhyper( X )
% 0.73/1.38 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 1
% 0.73/1.38 1 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (62) {G0,W2,D2,L1,V0,M1} I { bcapacitysn( n0 ) }.
% 0.73/1.38 parent0: (6039) {G0,W2,D2,L1,V0,M1} { bcapacitysn( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (63) {G0,W2,D2,L1,V0,M1} I { qilt27( n0 ) }.
% 0.73/1.38 parent0: (6040) {G0,W2,D2,L1,V0,M1} { qilt27( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (64) {G0,W3,D2,L1,V0,M1} I { ! gt( n0, skol15 ) }.
% 0.73/1.38 parent0: (6041) {G0,W3,D2,L1,V0,M1} { ! gt( n0, skol15 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (65) {G0,W2,D2,L1,V0,M1} I { ! conditionnormo( skol15 ) }.
% 0.73/1.38 parent0: (6042) {G0,W2,D2,L1,V0,M1} { ! conditionnormo( skol15 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6083) {G1,W2,D2,L1,V0,M1} { ! bcapacityex( n0 ) }.
% 0.73/1.38 parent0[1]: (5) {G0,W4,D2,L2,V1,M1} I { ! bcapacityex( X ), ! bcapacitysn(
% 0.73/1.38 X ) }.
% 0.73/1.38 parent1[0]: (62) {G0,W2,D2,L1,V0,M1} I { bcapacitysn( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := n0
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (84) {G1,W2,D2,L1,V0,M1} R(5,62) { ! bcapacityex( n0 ) }.
% 0.73/1.38 parent0: (6083) {G1,W2,D2,L1,V0,M1} { ! bcapacityex( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6084) {G1,W10,D3,L4,V1,M4} { bcapacityex( n0 ), bsecretioni(
% 0.73/1.38 X ), gt( n0, X ), drugsu( skol2( n0 ) ) }.
% 0.73/1.38 parent0[2]: (17) {G0,W11,D3,L4,V2,M2} I { bcapacityex( X ), bsecretioni( Y
% 0.73/1.38 ), ! gt( X, skol2( X ) ), gt( X, Y ) }.
% 0.73/1.38 parent1[1]: (60) {G0,W5,D2,L2,V1,M1} I { drugsu( X ), gt( n0, X ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := n0
% 0.73/1.38 Y := X
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 X := skol2( n0 )
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6085) {G2,W8,D3,L3,V1,M3} { bsecretioni( X ), gt( n0, X ),
% 0.73/1.38 drugsu( skol2( n0 ) ) }.
% 0.73/1.38 parent0[0]: (84) {G1,W2,D2,L1,V0,M1} R(5,62) { ! bcapacityex( n0 ) }.
% 0.73/1.38 parent1[0]: (6084) {G1,W10,D3,L4,V1,M4} { bcapacityex( n0 ), bsecretioni(
% 0.73/1.38 X ), gt( n0, X ), drugsu( skol2( n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (172) {G2,W8,D3,L3,V1,M1} R(17,60);r(84) { bsecretioni( X ),
% 0.73/1.38 drugsu( skol2( n0 ) ), gt( n0, X ) }.
% 0.73/1.38 parent0: (6085) {G2,W8,D3,L3,V1,M3} { bsecretioni( X ), gt( n0, X ),
% 0.73/1.38 drugsu( skol2( n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 2
% 0.73/1.38 2 ==> 1
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6086) {G1,W9,D3,L4,V1,M4} { alpha2( n0 ), ! conditionhyper(
% 0.73/1.38 skol4( X ) ), ! qilt27( n0 ), conditionnormo( skol15 ) }.
% 0.73/1.38 parent0[0]: (64) {G0,W3,D2,L1,V0,M1} I { ! gt( n0, skol15 ) }.
% 0.73/1.38 parent1[4]: (20) {G0,W12,D3,L5,V3,M1} I { alpha2( X ), ! conditionhyper(
% 0.73/1.38 skol4( Y ) ), ! qilt27( X ), conditionnormo( Z ), gt( X, Z ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 X := n0
% 0.73/1.38 Y := X
% 0.73/1.38 Z := skol15
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6087) {G1,W7,D3,L3,V1,M3} { alpha2( n0 ), ! conditionhyper(
% 0.73/1.38 skol4( X ) ), conditionnormo( skol15 ) }.
% 0.73/1.38 parent0[2]: (6086) {G1,W9,D3,L4,V1,M4} { alpha2( n0 ), ! conditionhyper(
% 0.73/1.38 skol4( X ) ), ! qilt27( n0 ), conditionnormo( skol15 ) }.
% 0.73/1.38 parent1[0]: (63) {G0,W2,D2,L1,V0,M1} I { qilt27( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (226) {G1,W7,D3,L3,V1,M1} R(20,64);r(63) { alpha2( n0 ), !
% 0.73/1.38 conditionhyper( skol4( X ) ), conditionnormo( skol15 ) }.
% 0.73/1.38 parent0: (6087) {G1,W7,D3,L3,V1,M3} { alpha2( n0 ), ! conditionhyper(
% 0.73/1.38 skol4( X ) ), conditionnormo( skol15 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 2 ==> 2
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6088) {G1,W10,D3,L4,V0,M4} { alpha2( n0 ), ! qilt27( n0 ),
% 0.73/1.38 conditionnormo( skol15 ), gt( n0, skol4( n0 ) ) }.
% 0.73/1.38 parent0[0]: (64) {G0,W3,D2,L1,V0,M1} I { ! gt( n0, skol15 ) }.
% 0.73/1.38 parent1[4]: (21) {G0,W13,D3,L5,V2,M2} I { alpha2( X ), ! qilt27( X ),
% 0.73/1.38 conditionnormo( Y ), gt( X, skol4( X ) ), gt( X, Y ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 X := n0
% 0.73/1.38 Y := skol15
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6089) {G1,W8,D3,L3,V0,M3} { alpha2( n0 ), conditionnormo(
% 0.73/1.38 skol15 ), gt( n0, skol4( n0 ) ) }.
% 0.73/1.38 parent0[1]: (6088) {G1,W10,D3,L4,V0,M4} { alpha2( n0 ), ! qilt27( n0 ),
% 0.73/1.38 conditionnormo( skol15 ), gt( n0, skol4( n0 ) ) }.
% 0.73/1.38 parent1[0]: (63) {G0,W2,D2,L1,V0,M1} I { qilt27( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (261) {G1,W8,D3,L3,V0,M1} R(21,64);r(63) { alpha2( n0 ),
% 0.73/1.38 conditionnormo( skol15 ), gt( n0, skol4( n0 ) ) }.
% 0.73/1.38 parent0: (6089) {G1,W8,D3,L3,V0,M3} { alpha2( n0 ), conditionnormo( skol15
% 0.73/1.38 ), gt( n0, skol4( n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 2 ==> 2
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6090) {G1,W12,D3,L5,V2,M5} { ! alpha2( X ), ! bcapacitysn( X
% 0.73/1.38 ), bcapacityex( X ), ! drugsu( skol2( Y ) ), bsecretioni( skol5( X ) )
% 0.73/1.38 }.
% 0.73/1.38 parent0[2]: (23) {G0,W8,D3,L3,V1,M1} I { ! alpha2( X ), ! bcapacitysn( X )
% 0.73/1.38 , ! gt( X, skol5( X ) ) }.
% 0.73/1.38 parent1[3]: (16) {G0,W10,D3,L4,V3,M1} I { bcapacityex( X ), ! drugsu( skol2
% 0.73/1.38 ( Y ) ), bsecretioni( Z ), gt( X, Z ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 X := X
% 0.73/1.38 Y := Y
% 0.73/1.38 Z := skol5( X )
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6091) {G1,W12,D3,L5,V2,M5} { ! bcapacitysn( X ), ! alpha2( X
% 0.73/1.38 ), ! bcapacitysn( X ), ! drugsu( skol2( Y ) ), bsecretioni( skol5( X ) )
% 0.73/1.38 }.
% 0.73/1.38 parent0[0]: (5) {G0,W4,D2,L2,V1,M1} I { ! bcapacityex( X ), ! bcapacitysn(
% 0.73/1.38 X ) }.
% 0.73/1.38 parent1[2]: (6090) {G1,W12,D3,L5,V2,M5} { ! alpha2( X ), ! bcapacitysn( X
% 0.73/1.38 ), bcapacityex( X ), ! drugsu( skol2( Y ) ), bsecretioni( skol5( X ) )
% 0.73/1.38 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 X := X
% 0.73/1.38 Y := Y
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 factor: (6092) {G1,W10,D3,L4,V2,M4} { ! bcapacitysn( X ), ! alpha2( X ), !
% 0.73/1.38 drugsu( skol2( Y ) ), bsecretioni( skol5( X ) ) }.
% 0.73/1.38 parent0[0, 2]: (6091) {G1,W12,D3,L5,V2,M5} { ! bcapacitysn( X ), ! alpha2
% 0.73/1.38 ( X ), ! bcapacitysn( X ), ! drugsu( skol2( Y ) ), bsecretioni( skol5( X
% 0.73/1.38 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 Y := Y
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (304) {G1,W10,D3,L4,V2,M1} R(23,16);r(5) { ! alpha2( X ), !
% 0.73/1.38 bcapacitysn( X ), bsecretioni( skol5( X ) ), ! drugsu( skol2( Y ) ) }.
% 0.73/1.38 parent0: (6092) {G1,W10,D3,L4,V2,M4} { ! bcapacitysn( X ), ! alpha2( X ),
% 0.73/1.38 ! drugsu( skol2( Y ) ), bsecretioni( skol5( X ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 Y := Y
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 1
% 0.73/1.38 1 ==> 0
% 0.73/1.38 2 ==> 3
% 0.73/1.38 3 ==> 2
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6093) {G1,W5,D3,L2,V1,M2} { alpha2( n0 ), ! conditionhyper(
% 0.73/1.38 skol4( X ) ) }.
% 0.73/1.38 parent0[0]: (65) {G0,W2,D2,L1,V0,M1} I { ! conditionnormo( skol15 ) }.
% 0.73/1.38 parent1[2]: (226) {G1,W7,D3,L3,V1,M1} R(20,64);r(63) { alpha2( n0 ), !
% 0.73/1.38 conditionhyper( skol4( X ) ), conditionnormo( skol15 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (1929) {G2,W5,D3,L2,V1,M1} S(226);r(65) { alpha2( n0 ), !
% 0.73/1.38 conditionhyper( skol4( X ) ) }.
% 0.73/1.38 parent0: (6093) {G1,W5,D3,L2,V1,M2} { alpha2( n0 ), ! conditionhyper(
% 0.73/1.38 skol4( X ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6094) {G1,W10,D3,L4,V0,M4} { ! alpha2( n0 ), ! bcapacitysn(
% 0.73/1.38 n0 ), bsecretioni( skol5( n0 ) ), drugsu( skol2( n0 ) ) }.
% 0.73/1.38 parent0[2]: (23) {G0,W8,D3,L3,V1,M1} I { ! alpha2( X ), ! bcapacitysn( X )
% 0.73/1.38 , ! gt( X, skol5( X ) ) }.
% 0.73/1.38 parent1[2]: (172) {G2,W8,D3,L3,V1,M1} R(17,60);r(84) { bsecretioni( X ),
% 0.73/1.38 drugsu( skol2( n0 ) ), gt( n0, X ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := n0
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 X := skol5( n0 )
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6095) {G1,W8,D3,L3,V0,M3} { ! alpha2( n0 ), bsecretioni(
% 0.73/1.38 skol5( n0 ) ), drugsu( skol2( n0 ) ) }.
% 0.73/1.38 parent0[1]: (6094) {G1,W10,D3,L4,V0,M4} { ! alpha2( n0 ), ! bcapacitysn(
% 0.73/1.38 n0 ), bsecretioni( skol5( n0 ) ), drugsu( skol2( n0 ) ) }.
% 0.73/1.38 parent1[0]: (62) {G0,W2,D2,L1,V0,M1} I { bcapacitysn( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (1983) {G3,W8,D3,L3,V0,M1} R(172,23);r(62) { bsecretioni(
% 0.73/1.38 skol5( n0 ) ), ! alpha2( n0 ), drugsu( skol2( n0 ) ) }.
% 0.73/1.38 parent0: (6095) {G1,W8,D3,L3,V0,M3} { ! alpha2( n0 ), bsecretioni( skol5(
% 0.73/1.38 n0 ) ), drugsu( skol2( n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 1
% 0.73/1.38 1 ==> 0
% 0.73/1.38 2 ==> 2
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6096) {G1,W6,D3,L2,V0,M2} { alpha2( n0 ), gt( n0, skol4( n0 )
% 0.73/1.38 ) }.
% 0.73/1.38 parent0[0]: (65) {G0,W2,D2,L1,V0,M1} I { ! conditionnormo( skol15 ) }.
% 0.73/1.38 parent1[1]: (261) {G1,W8,D3,L3,V0,M1} R(21,64);r(63) { alpha2( n0 ),
% 0.73/1.38 conditionnormo( skol15 ), gt( n0, skol4( n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (3469) {G2,W6,D3,L2,V0,M1} S(261);r(65) { alpha2( n0 ), gt( n0
% 0.73/1.38 , skol4( n0 ) ) }.
% 0.73/1.38 parent0: (6096) {G1,W6,D3,L2,V0,M2} { alpha2( n0 ), gt( n0, skol4( n0 ) )
% 0.73/1.38 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6097) {G1,W5,D3,L2,V0,M2} { conditionhyper( skol4( n0 ) ),
% 0.73/1.38 alpha2( n0 ) }.
% 0.73/1.38 parent0[1]: (61) {G0,W5,D2,L2,V1,M1} I { conditionhyper( X ), ! gt( n0, X )
% 0.73/1.38 }.
% 0.73/1.38 parent1[1]: (3469) {G2,W6,D3,L2,V0,M1} S(261);r(65) { alpha2( n0 ), gt( n0
% 0.73/1.38 , skol4( n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := skol4( n0 )
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6098) {G2,W4,D2,L2,V0,M2} { alpha2( n0 ), alpha2( n0 ) }.
% 0.73/1.38 parent0[1]: (1929) {G2,W5,D3,L2,V1,M1} S(226);r(65) { alpha2( n0 ), !
% 0.73/1.38 conditionhyper( skol4( X ) ) }.
% 0.73/1.38 parent1[0]: (6097) {G1,W5,D3,L2,V0,M2} { conditionhyper( skol4( n0 ) ),
% 0.73/1.38 alpha2( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := n0
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 factor: (6099) {G2,W2,D2,L1,V0,M1} { alpha2( n0 ) }.
% 0.73/1.38 parent0[0, 1]: (6098) {G2,W4,D2,L2,V0,M2} { alpha2( n0 ), alpha2( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (3506) {G3,W2,D2,L1,V0,M1} R(3469,61);r(1929) { alpha2( n0 )
% 0.73/1.38 }.
% 0.73/1.38 parent0: (6099) {G2,W2,D2,L1,V0,M1} { alpha2( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6100) {G4,W6,D3,L2,V0,M2} { bsecretioni( skol5( n0 ) ),
% 0.73/1.38 drugsu( skol2( n0 ) ) }.
% 0.73/1.38 parent0[1]: (1983) {G3,W8,D3,L3,V0,M1} R(172,23);r(62) { bsecretioni( skol5
% 0.73/1.38 ( n0 ) ), ! alpha2( n0 ), drugsu( skol2( n0 ) ) }.
% 0.73/1.38 parent1[0]: (3506) {G3,W2,D2,L1,V0,M1} R(3469,61);r(1929) { alpha2( n0 )
% 0.73/1.38 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (4065) {G4,W6,D3,L2,V0,M1} S(1983);r(3506) { bsecretioni(
% 0.73/1.38 skol5( n0 ) ), drugsu( skol2( n0 ) ) }.
% 0.73/1.38 parent0: (6100) {G4,W6,D3,L2,V0,M2} { bsecretioni( skol5( n0 ) ), drugsu(
% 0.73/1.38 skol2( n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6101) {G2,W10,D3,L4,V1,M4} { ! alpha2( X ), ! bcapacitysn( X
% 0.73/1.38 ), bsecretioni( skol5( X ) ), bsecretioni( skol5( n0 ) ) }.
% 0.73/1.38 parent0[3]: (304) {G1,W10,D3,L4,V2,M1} R(23,16);r(5) { ! alpha2( X ), !
% 0.73/1.38 bcapacitysn( X ), bsecretioni( skol5( X ) ), ! drugsu( skol2( Y ) ) }.
% 0.73/1.38 parent1[1]: (4065) {G4,W6,D3,L2,V0,M1} S(1983);r(3506) { bsecretioni( skol5
% 0.73/1.38 ( n0 ) ), drugsu( skol2( n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 Y := n0
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (5942) {G5,W10,D3,L4,V1,M2} R(304,4065) { ! alpha2( X ), !
% 0.73/1.38 bcapacitysn( X ), bsecretioni( skol5( n0 ) ), bsecretioni( skol5( X ) )
% 0.73/1.38 }.
% 0.73/1.38 parent0: (6101) {G2,W10,D3,L4,V1,M4} { ! alpha2( X ), ! bcapacitysn( X ),
% 0.73/1.38 bsecretioni( skol5( X ) ), bsecretioni( skol5( n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 2 ==> 3
% 0.73/1.38 3 ==> 2
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 factor: (6103) {G5,W7,D3,L3,V0,M3} { ! alpha2( n0 ), ! bcapacitysn( n0 ),
% 0.73/1.38 bsecretioni( skol5( n0 ) ) }.
% 0.73/1.38 parent0[2, 3]: (5942) {G5,W10,D3,L4,V1,M2} R(304,4065) { ! alpha2( X ), !
% 0.73/1.38 bcapacitysn( X ), bsecretioni( skol5( n0 ) ), bsecretioni( skol5( X ) )
% 0.73/1.38 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := n0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6104) {G4,W5,D3,L2,V0,M2} { ! bcapacitysn( n0 ), bsecretioni
% 0.73/1.38 ( skol5( n0 ) ) }.
% 0.73/1.38 parent0[0]: (6103) {G5,W7,D3,L3,V0,M3} { ! alpha2( n0 ), ! bcapacitysn( n0
% 0.73/1.38 ), bsecretioni( skol5( n0 ) ) }.
% 0.73/1.38 parent1[0]: (3506) {G3,W2,D2,L1,V0,M1} R(3469,61);r(1929) { alpha2( n0 )
% 0.73/1.38 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (5970) {G6,W5,D3,L2,V0,M1} F(5942);r(3506) { ! bcapacitysn( n0
% 0.73/1.38 ), bsecretioni( skol5( n0 ) ) }.
% 0.73/1.38 parent0: (6104) {G4,W5,D3,L2,V0,M2} { ! bcapacitysn( n0 ), bsecretioni(
% 0.73/1.38 skol5( n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6105) {G1,W3,D3,L1,V0,M1} { bsecretioni( skol5( n0 ) ) }.
% 0.73/1.38 parent0[0]: (5970) {G6,W5,D3,L2,V0,M1} F(5942);r(3506) { ! bcapacitysn( n0
% 0.73/1.38 ), bsecretioni( skol5( n0 ) ) }.
% 0.73/1.38 parent1[0]: (62) {G0,W2,D2,L1,V0,M1} I { bcapacitysn( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (5971) {G7,W3,D3,L1,V0,M1} S(5970);r(62) { bsecretioni( skol5
% 0.73/1.38 ( n0 ) ) }.
% 0.73/1.38 parent0: (6105) {G1,W3,D3,L1,V0,M1} { bsecretioni( skol5( n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6106) {G1,W4,D2,L2,V1,M2} { ! alpha2( X ), ! bcapacitysn( X )
% 0.73/1.38 }.
% 0.73/1.38 parent0[2]: (22) {G0,W7,D3,L3,V2,M1} I { ! alpha2( X ), ! bcapacitysn( X )
% 0.73/1.38 , ! bsecretioni( skol5( Y ) ) }.
% 0.73/1.38 parent1[0]: (5971) {G7,W3,D3,L1,V0,M1} S(5970);r(62) { bsecretioni( skol5(
% 0.73/1.38 n0 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 Y := n0
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (5972) {G8,W4,D2,L2,V1,M1} R(5971,22) { ! alpha2( X ), !
% 0.73/1.38 bcapacitysn( X ) }.
% 0.73/1.38 parent0: (6106) {G1,W4,D2,L2,V1,M2} { ! alpha2( X ), ! bcapacitysn( X )
% 0.73/1.38 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := X
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6107) {G1,W2,D2,L1,V0,M1} { ! alpha2( n0 ) }.
% 0.73/1.38 parent0[1]: (5972) {G8,W4,D2,L2,V1,M1} R(5971,22) { ! alpha2( X ), !
% 0.73/1.38 bcapacitysn( X ) }.
% 0.73/1.38 parent1[0]: (62) {G0,W2,D2,L1,V0,M1} I { bcapacitysn( n0 ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 X := n0
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 resolution: (6108) {G2,W0,D0,L0,V0,M0} { }.
% 0.73/1.38 parent0[0]: (6107) {G1,W2,D2,L1,V0,M1} { ! alpha2( n0 ) }.
% 0.73/1.38 parent1[0]: (3506) {G3,W2,D2,L1,V0,M1} R(3469,61);r(1929) { alpha2( n0 )
% 0.73/1.38 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (5975) {G9,W0,D0,L0,V0,M0} R(5972,62);r(3506) { }.
% 0.73/1.38 parent0: (6108) {G2,W0,D0,L0,V0,M0} { }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 Proof check complete!
% 0.73/1.38
% 0.73/1.38 Memory use:
% 0.73/1.38
% 0.73/1.38 space for terms: 82489
% 0.73/1.38 space for clauses: 207768
% 0.73/1.38
% 0.73/1.38
% 0.73/1.38 clauses generated: 23205
% 0.73/1.38 clauses kept: 5976
% 0.73/1.38 clauses selected: 690
% 0.73/1.38 clauses deleted: 207
% 0.73/1.38 clauses inuse deleted: 73
% 0.73/1.38
% 0.73/1.38 subsentry: 107929
% 0.73/1.38 literals s-matched: 89897
% 0.73/1.38 literals matched: 89819
% 0.73/1.38 full subsumption: 29700
% 0.73/1.38
% 0.73/1.38 checksum: -1864998619
% 0.73/1.38
% 0.73/1.38
% 0.73/1.38 Bliksem ended
%------------------------------------------------------------------------------