%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NLP059-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n008.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:02:51 EDT 2022
% Result : Satisfiable 0.77s 1.34s
% Output : Saturation 0.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : NLP059-1 : TPTP v8.1.0. Released v2.4.0.
% 0.04/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n008.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 : Thu Jun 30 23:45:23 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.72/1.13 *** allocated 10000 integers for termspace/termends
% 0.72/1.13 *** allocated 10000 integers for clauses
% 0.72/1.13 *** allocated 10000 integers for justifications
% 0.72/1.13 Bliksem 1.12
% 0.72/1.13
% 0.72/1.13
% 0.72/1.13 Automatic Strategy Selection
% 0.72/1.13
% 0.72/1.13 Clauses:
% 0.72/1.13 [
% 0.72/1.13 [ 'actual_world'( skc50 ) ],
% 0.72/1.13 [ 'actual_world'( skc6 ) ],
% 0.72/1.13 [ ssSkC0, six( skc50, skc51 ) ],
% 0.72/1.13 [ ssSkC0, group( skc50, skc51 ) ],
% 0.72/1.13 [ ssSkC0, male( skc50, skc52 ) ],
% 0.72/1.13 [ ~( ssSkC0 ), six( skc6, skc7 ) ],
% 0.72/1.13 [ ~( ssSkC0 ), group( skc6, skc7 ) ],
% 0.72/1.13 [ ~( ssSkC0 ), male( skc6, skc8 ) ],
% 0.72/1.13 [ ssSkC0, ssSkP1( skc51, skc52, skc50 ) ],
% 0.72/1.13 [ ~( ssSkC0 ), ssSkP0( skc7, skc8, skc6 ) ],
% 0.72/1.13 [ ~( member( skc50, X, skc51 ) ), ssSkC0, shot( skc50, X ) ],
% 0.72/1.13 [ ~( member( skc6, X, skc7 ) ), ~( ssSkC0 ), shot( skc6, X ) ],
% 0.72/1.13 [ ssSkP0( X, Y, Z ), cannon( Z, skf12( Z, T, U ) ) ],
% 0.72/1.13 [ ssSkP0( X, Y, Z ), man( Z, skf14( Z, T, U ) ) ],
% 0.72/1.13 [ ssSkP1( X, Y, Z ), cannon( Z, skf19( Z, T, U ) ) ],
% 0.72/1.13 [ ssSkP0( X, Y, Z ), of( Z, skf12( Z, Y, T ), Y ) ],
% 0.72/1.13 [ ssSkP0( X, Y, Z ), member( Z, skf12( Z, Y, X ), X ) ],
% 0.72/1.13 [ ssSkP1( X, Y, Z ), member( Z, skf19( Z, X, T ), X ) ],
% 0.72/1.13 [ ssSkP1( X, Y, Z ), of( Z, skf19( Z, X, Y ), Y ) ],
% 0.72/1.13 [ ~( member( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( of( X, Y, T ) ), ~(
% 0.72/1.13 ssSkP1( Z, T, X ) ), man( X, skf16( X, U ) ) ],
% 0.72/1.13 [ ~( member( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( of( X, Y, T ) ), ~(
% 0.72/1.13 ssSkP1( Z, T, X ) ), fire( X, skf15( X, U ) ) ],
% 0.72/1.13 [ ~( member( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( of( X, Y, T ) ), ~(
% 0.72/1.13 ssSkP1( Z, T, X ) ), nonreflexive( X, skf15( X, U ) ) ],
% 0.72/1.13 [ ~( member( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( of( X, Y, T ) ), ~(
% 0.72/1.13 ssSkP1( Z, T, X ) ), present( X, skf15( X, U ) ) ],
% 0.72/1.13 [ ~( member( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( of( X, Y, T ) ), ~(
% 0.72/1.13 ssSkP1( Z, T, X ) ), event( X, skf15( X, U ) ) ],
% 0.72/1.13 [ ~( member( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( of( X, Y, T ) ), ~(
% 0.72/1.13 ssSkP1( Z, T, X ) ), patient( X, skf15( X, Y ), Y ) ],
% 0.72/1.13 [ ~( member( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( of( X, Y, T ) ), ~(
% 0.72/1.13 ssSkP1( Z, T, X ) ), 'from_loc'( X, skf15( X, Y ), Y ) ],
% 0.72/1.13 [ ~( six( X, Y ) ), ~( group( X, Y ) ), ~( shot( X, skf21( X, Z ) ) ),
% 0.72/1.13 ~( ssSkP0( Y, T, X ) ), ~( male( X, T ) ), ~( 'actual_world'( X ) ),
% 0.72/1.13 ssSkC0 ],
% 0.72/1.13 [ ~( six( X, Y ) ), ~( group( X, Y ) ), ~( ssSkP0( Y, Z, X ) ), ~( male(
% 0.72/1.13 X, Z ) ), ~( 'actual_world'( X ) ), ssSkC0, member( X, skf21( X, Y ), Y )
% 0.72/1.13 ],
% 0.72/1.13 [ ~( member( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( of( X, Y, T ) ), ~(
% 0.72/1.13 ssSkP1( Z, T, X ) ), agent( X, skf15( X, U ), skf16( X, U ) ) ],
% 0.72/1.13 [ ~( six( X, Y ) ), ~( group( X, Y ) ), ~( shot( X, skf9( X, Z ) ) ),
% 0.72/1.13 ~( ssSkP1( Y, T, X ) ), ~( male( X, T ) ), ~( 'actual_world'( X ) ), ~(
% 0.72/1.13 ssSkC0 ) ],
% 0.72/1.13 [ ~( six( X, Y ) ), ~( group( X, Y ) ), ~( ssSkP1( Y, Z, X ) ), ~( male(
% 0.72/1.13 X, Z ) ), ~( 'actual_world'( X ) ), ~( ssSkC0 ), member( X, skf9( X, Y )
% 0.72/1.13 , Y ) ],
% 0.72/1.13 [ ~( of( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~(
% 0.72/1.13 man( X, U ) ), ~( ssSkP0( T, Z, X ) ), fire( X, skf10( X, W, V0 ) ) ]
% 0.72/1.13 ,
% 0.72/1.13 [ ~( of( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~(
% 0.72/1.13 man( X, U ) ), ~( ssSkP0( T, Z, X ) ), nonreflexive( X, skf10( X, W, V0 )
% 0.72/1.13 ) ],
% 0.72/1.13 [ ~( of( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~(
% 0.72/1.13 man( X, U ) ), ~( ssSkP0( T, Z, X ) ), present( X, skf10( X, W, V0 ) ) ]
% 0.72/1.13 ,
% 0.72/1.13 [ ~( of( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~(
% 0.72/1.13 man( X, U ) ), ~( ssSkP0( T, Z, X ) ), event( X, skf10( X, W, V0 ) ) ]
% 0.72/1.13 ,
% 0.72/1.13 [ ~( of( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~(
% 0.72/1.13 man( X, U ) ), ~( ssSkP0( T, Z, X ) ), patient( X, skf10( X, U, Y ), Y )
% 0.72/1.13 ],
% 0.72/1.13 [ ~( of( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~(
% 0.72/1.13 man( X, U ) ), ~( ssSkP0( T, Z, X ) ), agent( X, skf10( X, U, W ), U ) ]
% 0.72/1.13 ,
% 0.72/1.13 [ ~( of( X, Y, Z ) ), ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~(
% 0.72/1.13 man( X, U ) ), ~( ssSkP0( T, Z, X ) ), 'from_loc'( X, skf10( X, U, Y ), Y
% 0.72/1.13 ) ],
% 0.72/1.13 [ ~( 'from_loc'( X, Y, skf12( X, Z, T ) ) ), ~( fire( X, Y ) ), ~(
% 0.72/1.13 nonreflexive( X, Y ) ), ~( present( X, Y ) ), ~( patient( X, Y, skf12( X
% 0.72/1.13 , Z, T ) ) ), ~( agent( X, Y, skf14( X, T, Z ) ) ), ~( event( X, Y ) ),
% 0.77/1.17 ssSkP0( U, W, X ) ],
% 0.77/1.17 [ ~( event( X, Y ) ), ~( patient( X, Y, skf19( X, Z, T ) ) ), ~( present(
% 0.77/1.17 X, Y ) ), ~( nonreflexive( X, Y ) ), ~( fire( X, Y ) ), ~( 'from_loc'( X
% 0.77/1.17 , Y, skf19( X, Z, T ) ) ), ~( agent( X, Y, U ) ), ~( man( X, U ) ),
% 0.77/1.17 ssSkP1( W, V0, X ) ]
% 0.77/1.17 ] .
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 percentage equality = 0.000000, percentage horn = 0.675000
% 0.77/1.17 This a non-horn, non-equality problem
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Options Used:
% 0.77/1.17
% 0.77/1.17 useres = 1
% 0.77/1.17 useparamod = 0
% 0.77/1.17 useeqrefl = 0
% 0.77/1.17 useeqfact = 0
% 0.77/1.17 usefactor = 1
% 0.77/1.17 usesimpsplitting = 0
% 0.77/1.17 usesimpdemod = 0
% 0.77/1.17 usesimpres = 3
% 0.77/1.17
% 0.77/1.17 resimpinuse = 1000
% 0.77/1.17 resimpclauses = 20000
% 0.77/1.17 substype = standard
% 0.77/1.17 backwardsubs = 1
% 0.77/1.17 selectoldest = 5
% 0.77/1.17
% 0.77/1.17 litorderings [0] = split
% 0.77/1.17 litorderings [1] = liftord
% 0.77/1.17
% 0.77/1.17 termordering = none
% 0.77/1.17
% 0.77/1.17 litapriori = 1
% 0.77/1.17 termapriori = 0
% 0.77/1.17 litaposteriori = 0
% 0.77/1.17 termaposteriori = 0
% 0.77/1.17 demodaposteriori = 0
% 0.77/1.17 ordereqreflfact = 0
% 0.77/1.17
% 0.77/1.17 litselect = none
% 0.77/1.17
% 0.77/1.17 maxweight = 15
% 0.77/1.17 maxdepth = 30000
% 0.77/1.17 maxlength = 115
% 0.77/1.17 maxnrvars = 195
% 0.77/1.17 excuselevel = 1
% 0.77/1.17 increasemaxweight = 1
% 0.77/1.17
% 0.77/1.17 maxselected = 10000000
% 0.77/1.17 maxnrclauses = 10000000
% 0.77/1.17
% 0.77/1.17 showgenerated = 0
% 0.77/1.17 showkept = 0
% 0.77/1.17 showselected = 0
% 0.77/1.17 showdeleted = 0
% 0.77/1.17 showresimp = 1
% 0.77/1.17 showstatus = 2000
% 0.77/1.17
% 0.77/1.17 prologoutput = 1
% 0.77/1.17 nrgoals = 5000000
% 0.77/1.17 totalproof = 1
% 0.77/1.17
% 0.77/1.17 Symbols occurring in the translation:
% 0.77/1.17
% 0.77/1.17 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.77/1.17 . [1, 2] (w:1, o:29, a:1, s:1, b:0),
% 0.77/1.17 ! [4, 1] (w:0, o:23, a:1, s:1, b:0),
% 0.77/1.17 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.77/1.17 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.77/1.17 skc50 [39, 0] (w:1, o:5, a:1, s:1, b:0),
% 0.77/1.17 'actual_world' [40, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.77/1.17 skc6 [41, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.77/1.17 ssSkC0 [42, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.77/1.17 skc51 [43, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.77/1.17 six [44, 2] (w:1, o:55, a:1, s:1, b:0),
% 0.77/1.17 group [45, 2] (w:1, o:58, a:1, s:1, b:0),
% 0.77/1.17 skc52 [46, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.77/1.17 male [47, 2] (w:1, o:59, a:1, s:1, b:0),
% 0.77/1.17 skc7 [48, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.77/1.17 skc8 [49, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.77/1.17 ssSkP1 [50, 3] (w:1, o:69, a:1, s:1, b:0),
% 0.77/1.17 ssSkP0 [51, 3] (w:1, o:68, a:1, s:1, b:0),
% 0.77/1.17 member [53, 3] (w:1, o:70, a:1, s:1, b:0),
% 0.77/1.17 shot [54, 2] (w:1, o:54, a:1, s:1, b:0),
% 0.77/1.17 skf12 [59, 3] (w:1, o:71, a:1, s:1, b:0),
% 0.77/1.17 cannon [60, 2] (w:1, o:60, a:1, s:1, b:0),
% 0.77/1.17 skf14 [61, 3] (w:1, o:72, a:1, s:1, b:0),
% 0.77/1.17 man [62, 2] (w:1, o:61, a:1, s:1, b:0),
% 0.77/1.17 skf19 [63, 3] (w:1, o:73, a:1, s:1, b:0),
% 0.77/1.17 of [64, 3] (w:1, o:74, a:1, s:1, b:0),
% 0.77/1.17 skf16 [65, 2] (w:1, o:63, a:1, s:1, b:0),
% 0.77/1.17 skf15 [66, 2] (w:1, o:62, a:1, s:1, b:0),
% 0.77/1.17 fire [67, 2] (w:1, o:57, a:1, s:1, b:0),
% 0.77/1.17 nonreflexive [68, 2] (w:1, o:64, a:1, s:1, b:0),
% 0.77/1.17 present [69, 2] (w:1, o:65, a:1, s:1, b:0),
% 0.77/1.17 event [70, 2] (w:1, o:56, a:1, s:1, b:0),
% 0.77/1.17 patient [71, 3] (w:1, o:75, a:1, s:1, b:0),
% 0.77/1.17 'from_loc' [72, 3] (w:1, o:76, a:1, s:1, b:0),
% 0.77/1.17 skf21 [73, 2] (w:1, o:66, a:1, s:1, b:0),
% 0.77/1.17 agent [74, 3] (w:1, o:77, a:1, s:1, b:0),
% 0.77/1.17 skf9 [75, 2] (w:1, o:67, a:1, s:1, b:0),
% 0.77/1.17 skf10 [78, 3] (w:1, o:78, a:1, s:1, b:0).
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Starting Search:
% 0.77/1.17
% 0.77/1.17 Resimplifying inuse:
% 0.77/1.17 Done
% 0.77/1.17
% 0.77/1.17 Failed to find proof!
% 0.77/1.17 maxweight = 15
% 0.77/1.17 maxnrclauses = 10000000
% 0.77/1.17 Generated: 93
% 0.77/1.17 Kept: 71
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 The strategy used was not complete!
% 0.77/1.17
% 0.77/1.17 Increased maxweight to 16
% 0.77/1.17
% 0.77/1.17 Starting Search:
% 0.77/1.17
% 0.77/1.17 Resimplifying inuse:
% 0.77/1.17 Done
% 0.77/1.17
% 0.77/1.17 Failed to find proof!
% 0.77/1.17 maxweight = 16
% 0.77/1.17 maxnrclauses = 10000000
% 0.77/1.17 Generated: 93
% 0.77/1.17 Kept: 71
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 The strategy used was not complete!
% 0.77/1.17
% 0.77/1.17 Increased maxweight to 17
% 0.77/1.17
% 0.77/1.17 Starting Search:
% 0.77/1.17
% 0.77/1.17 Resimplifying inuse:
% 0.77/1.17 Done
% 0.77/1.17
% 0.77/1.17 Failed to find proof!
% 0.77/1.17 maxweight = 17
% 0.77/1.17 maxnrclauses = 10000000
% 0.77/1.17 Generated: 93
% 0.77/1.17 Kept: 71
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 The strategy used was not complete!
% 0.77/1.17
% 0.77/1.17 Increased maxweight to 18
% 0.77/1.17
% 0.77/1.17 Starting Search:
% 0.77/1.17
% 0.77/1.17 Resimplifying inuse:
% 0.77/1.17 Done
% 0.77/1.17
% 0.77/1.17 Failed to find proof!
% 0.77/1.17 maxweight = 18
% 0.77/1.17 maxnrclauses = 10000000
% 0.77/1.17 Generated: 93
% 0.77/1.17 Kept: 71
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 The strategy used was not complete!
% 0.77/1.17
% 0.77/1.17 Increased maxweight to 19
% 0.77/1.17
% 0.77/1.17 Starting Search:
% 0.77/1.17
% 0.77/1.17 Resimplifying inuse:
% 0.77/1.17 Done
% 0.77/1.17
% 0.77/1.17 Failed to find proof!
% 0.77/1.17 maxweight = 19
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 93
% 0.77/1.21 Kept: 71
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 20
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 20
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 96
% 0.77/1.21 Kept: 75
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 21
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 21
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 96
% 0.77/1.21 Kept: 75
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 22
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 22
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 96
% 0.77/1.21 Kept: 75
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 23
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 23
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 152
% 0.77/1.21 Kept: 109
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 24
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 24
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 152
% 0.77/1.21 Kept: 109
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 25
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 25
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 167
% 0.77/1.21 Kept: 129
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 26
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 26
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 167
% 0.77/1.21 Kept: 135
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 27
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 27
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 191
% 0.77/1.21 Kept: 143
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 28
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 28
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 191
% 0.77/1.21 Kept: 143
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 29
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 29
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 191
% 0.77/1.21 Kept: 143
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 30
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 30
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 191
% 0.77/1.21 Kept: 143
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 31
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 31
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 194
% 0.77/1.21 Kept: 151
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 32
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 32
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 194
% 0.77/1.21 Kept: 151
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 33
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 33
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 194
% 0.77/1.21 Kept: 151
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 34
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 34
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 194
% 0.77/1.21 Kept: 156
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 35
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 35
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 194
% 0.77/1.21 Kept: 156
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 36
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 36
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 194
% 0.77/1.21 Kept: 156
% 0.77/1.21
% 0.77/1.21
% 0.77/1.21 The strategy used was not complete!
% 0.77/1.21
% 0.77/1.21 Increased maxweight to 37
% 0.77/1.21
% 0.77/1.21 Starting Search:
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Resimplifying inuse:
% 0.77/1.21 Done
% 0.77/1.21
% 0.77/1.21 Failed to find proof!
% 0.77/1.21 maxweight = 37
% 0.77/1.21 maxnrclauses = 10000000
% 0.77/1.21 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 38
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 38
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 39
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 39
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 40
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 40
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 41
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 41
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 42
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 42
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 43
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 43
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 44
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 44
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 45
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 45
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 46
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 46
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 47
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 47
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 48
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 48
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 49
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 49
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 50
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 50
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 51
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 51
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 52
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 52
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 53
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 53
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 54
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 54
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.26
% 0.77/1.26 Increased maxweight to 55
% 0.77/1.26
% 0.77/1.26 Starting Search:
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Resimplifying inuse:
% 0.77/1.26 Done
% 0.77/1.26
% 0.77/1.26 Failed to find proof!
% 0.77/1.26 maxweight = 55
% 0.77/1.26 maxnrclauses = 10000000
% 0.77/1.26 Generated: 194
% 0.77/1.26 Kept: 156
% 0.77/1.26
% 0.77/1.26
% 0.77/1.26 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 56
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 56
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 57
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 57
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 58
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 58
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 59
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 59
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 60
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 60
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 61
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 61
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 62
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 62
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 63
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 63
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 64
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 64
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 65
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 65
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 66
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 66
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 67
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 67
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 68
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 68
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 69
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 69
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 70
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 70
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 71
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 71
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 72
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 72
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.29
% 0.77/1.29 Increased maxweight to 73
% 0.77/1.29
% 0.77/1.29 Starting Search:
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Resimplifying inuse:
% 0.77/1.29 Done
% 0.77/1.29
% 0.77/1.29 Failed to find proof!
% 0.77/1.29 maxweight = 73
% 0.77/1.29 maxnrclauses = 10000000
% 0.77/1.29 Generated: 194
% 0.77/1.29 Kept: 156
% 0.77/1.29
% 0.77/1.29
% 0.77/1.29 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 74
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 74
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 75
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 75
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 76
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 76
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 77
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 77
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 78
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 78
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 79
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 79
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 80
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 80
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 81
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 81
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 82
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 82
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 83
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 83
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 84
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 84
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 85
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 85
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 86
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 86
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 87
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 87
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 88
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 88
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 89
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 89
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 90
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 90
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 91
% 0.77/1.32
% 0.77/1.32 Starting Search:
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Resimplifying inuse:
% 0.77/1.32 Done
% 0.77/1.32
% 0.77/1.32 Failed to find proof!
% 0.77/1.32 maxweight = 91
% 0.77/1.32 maxnrclauses = 10000000
% 0.77/1.32 Generated: 194
% 0.77/1.32 Kept: 156
% 0.77/1.32
% 0.77/1.32
% 0.77/1.32 The strategy used was not complete!
% 0.77/1.32
% 0.77/1.32 Increased maxweight to 92
% 0.77/1.32
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 92
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 194
% 0.77/1.34 Kept: 156
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 93
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 93
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 194
% 0.77/1.34 Kept: 156
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 94
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 94
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 194
% 0.77/1.34 Kept: 156
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 95
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 95
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 230
% 0.77/1.34 Kept: 174
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 96
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 96
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 230
% 0.77/1.34 Kept: 174
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 97
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 97
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 230
% 0.77/1.34 Kept: 174
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 98
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 98
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 99
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 99
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 100
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 100
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 101
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 101
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 102
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 102
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 103
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 103
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 104
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 104
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 105
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 105
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 106
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 106
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 107
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 107
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 108
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 108
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 109
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 109
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 110
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 110
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 111
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 111
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 112
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 112
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 236
% 0.77/1.34 Kept: 176
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 113
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 113
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 251
% 0.77/1.34 Kept: 184
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 114
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 114
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 251
% 0.77/1.34 Kept: 184
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 115
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Failed to find proof!
% 0.77/1.34 maxweight = 115
% 0.77/1.34 maxnrclauses = 10000000
% 0.77/1.34 Generated: 251
% 0.77/1.34 Kept: 184
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 The strategy used was not complete!
% 0.77/1.34
% 0.77/1.34 Increased maxweight to 116
% 0.77/1.34
% 0.77/1.34 Starting Search:
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34 Resimplifying inuse:
% 0.77/1.34 Done
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 found a saturation!
% 0.77/1.34 % SZS status Satisfiable
% 0.77/1.34 % SZS output start Saturation
% 0.77/1.34
% 0.77/1.34 clause( 184, [ ssSkC0, shot( skc50, skf12( skc50, skc52, skc51 ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 183, [ ~( event( X, skf10( X, skf14( X, Y, Z ), skf12( X, Z, Y ) )
% 0.77/1.34 ) ), ~( fire( X, skf10( X, skf14( X, Y, Z ), skf12( X, Z, Y ) ) ) ), ~(
% 0.77/1.34 cannon( X, skf12( X, Z, Y ) ) ), ~( man( X, skf14( X, Y, Z ) ) ), ~(
% 0.77/1.34 nonreflexive( X, skf10( X, skf14( X, Y, Z ), skf12( X, Z, Y ) ) ) ), ~(
% 0.77/1.34 present( X, skf10( X, skf14( X, Y, Z ), skf12( X, Z, Y ) ) ) ), ssSkP0( T
% 0.77/1.34 , Z, X ), ~( ssSkP0( U, Z, X ) ), ~( member( X, skf12( X, Z, Y ), U ) ) ]
% 0.77/1.34 )
% 0.77/1.34 .
% 0.77/1.34 clause( 181, [ ~( event( X, skf10( X, skf14( X, Y, Z ), skf12( X, Z, Y ) )
% 0.77/1.34 ) ), ~( fire( X, skf10( X, skf14( X, Y, Z ), skf12( X, Z, Y ) ) ) ), ~(
% 0.77/1.34 cannon( X, skf12( X, Z, Y ) ) ), ~( man( X, skf14( X, Y, Z ) ) ), ~(
% 0.77/1.34 nonreflexive( X, skf10( X, skf14( X, Y, Z ), skf12( X, Z, Y ) ) ) ), ~(
% 0.77/1.34 present( X, skf10( X, skf14( X, Y, Z ), skf12( X, Z, Y ) ) ) ), ssSkP0( T
% 0.77/1.34 , U, X ), ~( ssSkP0( W, V0, X ) ), ~( member( X, skf12( X, Z, Y ), W ) )
% 0.77/1.34 , ~( of( X, skf12( X, Z, Y ), V0 ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 178, [ ~( event( X, skf15( X, skf19( X, Y, Z ) ) ) ), ~( fire( X,
% 0.77/1.34 skf15( X, skf19( X, Y, Z ) ) ) ), ~( cannon( X, skf19( X, Y, Z ) ) ), ~(
% 0.77/1.34 man( X, skf16( X, skf19( X, Y, Z ) ) ) ), ~( nonreflexive( X, skf15( X,
% 0.77/1.34 skf19( X, Y, Z ) ) ) ), ~( present( X, skf15( X, skf19( X, Y, Z ) ) ) ),
% 0.77/1.34 ssSkP1( Y, Z, X ), ~( ssSkP1( T, Z, X ) ), ~( member( X, skf19( X, Y, Z )
% 0.77/1.34 , T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 176, [ ~( event( X, skf15( X, skf19( X, Y, Z ) ) ) ), ~( fire( X,
% 0.77/1.34 skf15( X, skf19( X, Y, Z ) ) ) ), ~( cannon( X, skf19( X, Y, Z ) ) ), ~(
% 0.77/1.34 man( X, skf16( X, skf19( X, Y, Z ) ) ) ), ~( nonreflexive( X, skf15( X,
% 0.77/1.34 skf19( X, Y, Z ) ) ) ), ~( present( X, skf15( X, skf19( X, Y, Z ) ) ) ),
% 0.77/1.34 ssSkP1( T, U, X ), ~( ssSkP1( W, V0, X ) ), ~( member( X, skf19( X, Y, Z
% 0.77/1.34 ), W ) ), ~( of( X, skf19( X, Y, Z ), V0 ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 173, [ ~( event( X, skf10( X, Y, skf19( X, Z, T ) ) ) ), ~( fire( X
% 0.77/1.34 , skf10( X, Y, skf19( X, Z, T ) ) ) ), ~( cannon( X, skf19( X, Z, T ) ) )
% 0.77/1.34 , ~( man( X, Y ) ), ~( nonreflexive( X, skf10( X, Y, skf19( X, Z, T ) ) )
% 0.77/1.34 ), ~( present( X, skf10( X, Y, skf19( X, Z, T ) ) ) ), ~( ssSkP0( Z, T,
% 0.77/1.34 X ) ), ssSkP1( Z, T, X ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 171, [ ~( event( X, skf10( X, Y, skf19( X, Z, T ) ) ) ), ~( fire( X
% 0.77/1.34 , skf10( X, Y, skf19( X, Z, T ) ) ) ), ~( cannon( X, skf19( X, Z, T ) ) )
% 0.77/1.34 , ~( man( X, Y ) ), ~( nonreflexive( X, skf10( X, Y, skf19( X, Z, T ) ) )
% 0.77/1.34 ), ~( present( X, skf10( X, Y, skf19( X, Z, T ) ) ) ), ~( ssSkP0( U, T,
% 0.77/1.34 X ) ), ssSkP1( Z, T, X ), ~( member( X, skf19( X, Z, T ), U ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 169, [ ~( event( X, skf10( X, Y, skf19( X, Z, T ) ) ) ), ~( fire( X
% 0.77/1.34 , skf10( X, Y, skf19( X, Z, T ) ) ) ), ~( cannon( X, skf19( X, Z, T ) ) )
% 0.77/1.34 , ~( man( X, Y ) ), ~( nonreflexive( X, skf10( X, Y, skf19( X, Z, T ) ) )
% 0.77/1.34 ), ~( present( X, skf10( X, Y, skf19( X, Z, T ) ) ) ), ~( ssSkP0( U, W,
% 0.77/1.34 X ) ), ssSkP1( V0, V1, X ), ~( member( X, skf19( X, Z, T ), U ) ), ~( of(
% 0.77/1.34 X, skf19( X, Z, T ), W ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 85, [ ~( event( X, skf15( X, Y ) ) ), ~( nonreflexive( X, skf15( X
% 0.77/1.34 , Y ) ) ), ~( fire( X, skf15( X, Y ) ) ), ~( present( X, skf15( X, Y ) )
% 0.77/1.34 ), ~( patient( X, skf15( X, Y ), skf19( X, Z, T ) ) ), ~( man( X, skf16(
% 0.77/1.34 X, Y ) ) ), ssSkP1( U, W, X ), ~( cannon( X, V0 ) ), ~( member( X, V0, V1
% 0.77/1.34 ) ), ~( ssSkP1( V1, V2, X ) ), ~( of( X, V0, V2 ) ), ~( 'from_loc'( X,
% 0.77/1.34 skf15( X, Y ), skf19( X, Z, T ) ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 99, [ ~( cannon( X, skf12( X, Y, Z ) ) ), cannon( X, skf19( X, U, W
% 0.77/1.34 ) ), ~( six( X, Z ) ), ~( shot( X, skf21( X, V0 ) ) ), ~( group( X, Z )
% 0.77/1.34 ), ~( male( X, Y ) ), ~( 'actual_world'( X ) ), ssSkC0, man( X, skf16( X
% 0.77/1.34 , T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 113, [ event( X, skf15( X, Y ) ), ~( cannon( X, skf12( X, Z, T ) )
% 0.77/1.34 ), ~( six( X, T ) ), ~( shot( X, skf21( X, V0 ) ) ), ~( group( X, T ) )
% 0.77/1.34 , ~( male( X, Z ) ), ~( 'actual_world'( X ) ), ssSkC0, cannon( X, skf19(
% 0.77/1.34 X, U, W ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 123, [ ~( cannon( X, skf12( X, Y, Z ) ) ), cannon( X, skf19( X, U,
% 0.77/1.34 W ) ), ~( six( X, Z ) ), ~( shot( X, skf21( X, V0 ) ) ), ~( group( X, Z )
% 0.77/1.34 ), ~( male( X, Y ) ), ~( 'actual_world'( X ) ), ssSkC0, present( X,
% 0.77/1.34 skf15( X, T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 84, [ ~( event( X, skf10( X, Y, Z ) ) ), ~( nonreflexive( X, skf10(
% 0.77/1.34 X, Y, Z ) ) ), ~( fire( X, skf10( X, Y, Z ) ) ), ~( present( X, skf10( X
% 0.77/1.34 , Y, Z ) ) ), ~( patient( X, skf10( X, Y, Z ), skf19( X, T, U ) ) ), ~(
% 0.77/1.34 man( X, Y ) ), ssSkP1( W, V0, X ), ~( cannon( X, V1 ) ), ~( member( X, V1
% 0.77/1.34 , V2 ) ), ~( ssSkP0( V2, V3, X ) ), ~( of( X, V1, V3 ) ), ~( 'from_loc'(
% 0.77/1.34 X, skf10( X, Y, Z ), skf19( X, T, U ) ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 135, [ ~( cannon( X, skf12( X, Y, Z ) ) ), cannon( X, skf19( X, U,
% 0.77/1.34 W ) ), ~( six( X, Z ) ), ~( shot( X, skf21( X, V0 ) ) ), ~( group( X, Z )
% 0.77/1.34 ), ~( male( X, Y ) ), ~( 'actual_world'( X ) ), ssSkC0, nonreflexive( X
% 0.77/1.34 , skf15( X, T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 158, [ ssSkC0, shot( skc50, skf19( skc50, skc51, Z ) ), ~( shot(
% 0.77/1.34 skc50, skf21( skc50, T ) ) ), ~( male( skc50, X ) ), ~( cannon( skc50,
% 0.77/1.34 skf12( skc50, X, skc51 ) ) ), man( skc50, skf16( skc50, Y ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 82, [ fire( X, skf15( X, Y ) ), ~( cannon( X, skf12( X, Z, T ) ) )
% 0.77/1.34 , ~( six( X, T ) ), ~( shot( X, skf21( X, V0 ) ) ), ~( group( X, T ) ),
% 0.77/1.34 ~( male( X, Z ) ), ~( 'actual_world'( X ) ), ssSkC0, cannon( X, skf19( X
% 0.77/1.34 , U, W ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 157, [ ssSkC0, shot( skc50, skf19( skc50, skc51, Z ) ), ~( shot(
% 0.77/1.34 skc50, skf21( skc50, T ) ) ), ~( male( skc50, X ) ), ~( cannon( skc50,
% 0.77/1.34 skf12( skc50, X, skc51 ) ) ), present( skc50, skf15( skc50, Y ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 152, [ ssSkC0, shot( skc50, skf19( skc50, skc51, Z ) ), ~( shot(
% 0.77/1.34 skc50, skf21( skc50, T ) ) ), ~( male( skc50, X ) ), ~( cannon( skc50,
% 0.77/1.34 skf12( skc50, X, skc51 ) ) ), nonreflexive( skc50, skf15( skc50, Y ) ) ]
% 0.77/1.34 )
% 0.77/1.34 .
% 0.77/1.34 clause( 80, [ ~( fire( X, skf10( X, skf14( X, Y, Z ), T ) ) ), ~(
% 0.77/1.34 nonreflexive( X, skf10( X, skf14( X, Y, Z ), T ) ) ), ~( present( X,
% 0.77/1.34 skf10( X, skf14( X, Y, Z ), T ) ) ), ~( patient( X, skf10( X, skf14( X, Y
% 0.77/1.34 , Z ), T ), skf12( X, Z, Y ) ) ), ~( event( X, skf10( X, skf14( X, Y, Z )
% 0.77/1.34 , T ) ) ), ssSkP0( U, W, X ), ~( cannon( X, V0 ) ), ~( member( X, V0, V1
% 0.77/1.34 ) ), ~( man( X, skf14( X, Y, Z ) ) ), ~( ssSkP0( V1, V2, X ) ), ~( of( X
% 0.77/1.34 , V0, V2 ) ), ~( 'from_loc'( X, skf10( X, skf14( X, Y, Z ), T ), skf12( X
% 0.77/1.34 , Z, Y ) ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 151, [ ~( cannon( X, skf19( X, Y, Z ) ) ), ~( man( X, T ) ),
% 0.77/1.34 nonreflexive( X, skf10( X, U, W ) ), ~( ssSkP0( Y, Z, X ) ), ssSkP1( Y, Z
% 0.77/1.34 , X ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 69, [ ~( cannon( X, skf19( X, Y, Z ) ) ), ~( man( X, U ) ), ~(
% 0.77/1.34 ssSkP0( T, Z, X ) ), nonreflexive( X, skf10( X, W, V0 ) ), ssSkP1( Y, Z,
% 0.77/1.34 X ), ~( member( X, skf19( X, Y, Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 68, [ ~( cannon( X, skf12( X, Y, Z ) ) ), ~( man( X, U ) ), ~(
% 0.77/1.34 ssSkP0( T, Y, X ) ), present( X, skf10( X, W, V0 ) ), ssSkP0( V1, Y, X )
% 0.77/1.34 , ~( member( X, skf12( X, Y, Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 70, [ ~( cannon( X, skf12( X, Y, Z ) ) ), ~( man( X, U ) ), ~(
% 0.77/1.34 ssSkP0( T, Y, X ) ), nonreflexive( X, skf10( X, W, V0 ) ), ssSkP0( V1, Y
% 0.77/1.34 , X ), ~( member( X, skf12( X, Y, Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 149, [ ~( cannon( X, skf19( X, Y, Z ) ) ), ~( man( X, T ) ),
% 0.77/1.34 present( X, skf10( X, U, W ) ), ~( ssSkP0( Y, Z, X ) ), ssSkP1( Y, Z, X )
% 0.77/1.34 ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 67, [ ~( cannon( X, skf19( X, Y, Z ) ) ), ~( man( X, U ) ), ~(
% 0.77/1.34 ssSkP0( T, Z, X ) ), present( X, skf10( X, W, V0 ) ), ssSkP1( Y, Z, X ),
% 0.77/1.34 ~( member( X, skf19( X, Y, Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 100, [ ~( cannon( skc50, skf12( skc50, X, skc51 ) ) ), ssSkC0, shot(
% 0.77/1.34 skc50, skf19( skc50, skc51, Z ) ), shot( skc50, skf21( skc50, skc51 ) ),
% 0.77/1.34 ~( male( skc50, X ) ), man( skc50, skf16( skc50, Y ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 124, [ ~( cannon( skc50, skf12( skc50, X, skc51 ) ) ), ssSkC0, shot(
% 0.77/1.34 skc50, skf19( skc50, skc51, Z ) ), shot( skc50, skf21( skc50, skc51 ) ),
% 0.77/1.34 ~( male( skc50, X ) ), present( skc50, skf15( skc50, Y ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 136, [ ~( cannon( skc50, skf12( skc50, X, skc51 ) ) ), ssSkC0, shot(
% 0.77/1.34 skc50, skf19( skc50, skc51, Z ) ), shot( skc50, skf21( skc50, skc51 ) ),
% 0.77/1.34 ~( male( skc50, X ) ), nonreflexive( skc50, skf15( skc50, Y ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 66, [ ~( cannon( X, skf12( X, Y, Z ) ) ), ~( man( X, U ) ), ~(
% 0.77/1.34 ssSkP0( T, Y, X ) ), fire( X, skf10( X, W, V0 ) ), ssSkP0( V1, Y, X ),
% 0.77/1.34 ~( member( X, skf12( X, Y, Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 98, [ ~( cannon( skc50, skf12( skc50, X, skc51 ) ) ), cannon( skc50
% 0.77/1.34 , skf19( skc50, Z, T ) ), ssSkC0, shot( skc50, skf21( skc50, skc51 ) ),
% 0.77/1.34 ~( male( skc50, X ) ), man( skc50, skf16( skc50, Y ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 122, [ ~( cannon( skc50, skf12( skc50, X, skc51 ) ) ), cannon(
% 0.77/1.34 skc50, skf19( skc50, Z, T ) ), ssSkC0, shot( skc50, skf21( skc50, skc51 )
% 0.77/1.34 ), ~( male( skc50, X ) ), present( skc50, skf15( skc50, Y ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 134, [ ~( cannon( skc50, skf12( skc50, X, skc51 ) ) ), cannon(
% 0.77/1.34 skc50, skf19( skc50, Z, T ) ), ssSkC0, shot( skc50, skf21( skc50, skc51 )
% 0.77/1.34 ), ~( male( skc50, X ) ), nonreflexive( skc50, skf15( skc50, Y ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 147, [ ~( cannon( X, skf19( X, Y, Z ) ) ), fire( X, skf10( X, U, W
% 0.77/1.34 ) ), ~( man( X, T ) ), ~( ssSkP0( Y, Z, X ) ), ssSkP1( Y, Z, X ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 65, [ ~( cannon( X, skf19( X, Y, Z ) ) ), ~( man( X, U ) ), ~(
% 0.77/1.34 ssSkP0( T, Z, X ) ), fire( X, skf10( X, W, V0 ) ), ssSkP1( Y, Z, X ), ~(
% 0.77/1.34 member( X, skf19( X, Y, Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 145, [ ssSkC0, ~( shot( skc50, skf21( skc50, X ) ) ), event( skc50
% 0.77/1.34 , skf15( skc50, Y ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 64, [ ~( cannon( X, skf12( X, Y, Z ) ) ), ~( man( X, U ) ), ~(
% 0.77/1.34 ssSkP0( T, Y, X ) ), event( X, skf10( X, W, V0 ) ), ssSkP0( V1, Y, X ),
% 0.77/1.34 ~( member( X, skf12( X, Y, Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 140, [ ~( cannon( X, skf19( X, Y, Z ) ) ), event( X, skf10( X, U, W
% 0.77/1.34 ) ), ~( man( X, T ) ), ~( ssSkP0( Y, Z, X ) ), ssSkP1( Y, Z, X ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 138, [ ssSkC0, ~( shot( skc50, skf21( skc50, Y ) ) ), ~( cannon(
% 0.77/1.34 skc50, skf12( skc50, skc52, skc51 ) ) ), nonreflexive( skc50, skf15(
% 0.77/1.34 skc50, X ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 63, [ ~( cannon( X, skf19( X, Y, Z ) ) ), ~( man( X, U ) ), ~(
% 0.77/1.34 ssSkP0( T, Z, X ) ), event( X, skf10( X, W, V0 ) ), ssSkP1( Y, Z, X ),
% 0.77/1.34 ~( member( X, skf19( X, Y, Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 129, [ ~( cannon( skc50, skf12( skc50, X, skc51 ) ) ), nonreflexive(
% 0.77/1.34 skc50, skf15( skc50, Y ) ), ssSkC0, shot( skc50, skf19( skc50, skc51, Z )
% 0.77/1.34 ), ssSkP0( skc51, X, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 130, [ ~( cannon( X, skf12( X, Y, Z ) ) ), nonreflexive( X, skf15(
% 0.77/1.34 X, T ) ), cannon( X, skf19( X, U, W ) ), ssSkP0( Z, Y, X ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 50, [ ~( cannon( X, skf19( X, Y, Z ) ) ), ~( ssSkP1( T, Z, X ) ),
% 0.77/1.34 fire( X, skf15( X, U ) ), ssSkP1( Y, Z, X ), ~( member( X, skf19( X, Y, Z
% 0.77/1.34 ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 132, [ ~( cannon( skc50, skf12( skc50, skc52, skc51 ) ) ), ssSkC0,
% 0.77/1.34 shot( skc50, skf21( skc50, skc51 ) ), nonreflexive( skc50, skf15( skc50,
% 0.77/1.34 X ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 131, [ ~( cannon( skc50, skf12( skc50, skc52, skc51 ) ) ),
% 0.77/1.34 nonreflexive( skc50, skf15( skc50, X ) ), ssSkC0, ssSkP0( skc51, skc52,
% 0.77/1.34 skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 128, [ ~( cannon( X, skf12( X, Y, Z ) ) ), nonreflexive( X, skf15(
% 0.77/1.34 X, T ) ), ssSkP0( Z, Y, X ), ~( ssSkP1( Z, Y, X ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 126, [ ssSkC0, ~( shot( skc50, skf21( skc50, Y ) ) ), ~( cannon(
% 0.77/1.34 skc50, skf12( skc50, skc52, skc51 ) ) ), present( skc50, skf15( skc50, X
% 0.77/1.34 ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 49, [ ~( cannon( X, skf12( X, Y, Z ) ) ), ~( ssSkP1( T, Y, X ) ),
% 0.77/1.34 nonreflexive( X, skf15( X, U ) ), ssSkP0( W, Y, X ), ~( member( X, skf12(
% 0.77/1.34 X, Y, Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 117, [ ~( cannon( skc50, skf12( skc50, X, skc51 ) ) ), present(
% 0.77/1.34 skc50, skf15( skc50, Y ) ), ssSkC0, shot( skc50, skf19( skc50, skc51, Z )
% 0.77/1.34 ), ssSkP0( skc51, X, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 48, [ ~( cannon( X, skf19( X, Y, Z ) ) ), ~( ssSkP1( T, Z, X ) ),
% 0.77/1.34 nonreflexive( X, skf15( X, U ) ), ssSkP1( Y, Z, X ), ~( member( X, skf19(
% 0.77/1.34 X, Y, Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 118, [ ~( cannon( X, skf12( X, Y, Z ) ) ), present( X, skf15( X, T
% 0.77/1.34 ) ), cannon( X, skf19( X, U, W ) ), ssSkP0( Z, Y, X ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 120, [ ~( cannon( skc50, skf12( skc50, skc52, skc51 ) ) ), ssSkC0,
% 0.77/1.34 shot( skc50, skf21( skc50, skc51 ) ), present( skc50, skf15( skc50, X ) )
% 0.77/1.34 ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 119, [ ~( cannon( skc50, skf12( skc50, skc52, skc51 ) ) ), present(
% 0.77/1.34 skc50, skf15( skc50, X ) ), ssSkC0, ssSkP0( skc51, skc52, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 116, [ ~( cannon( X, skf12( X, Y, Z ) ) ), present( X, skf15( X, T
% 0.77/1.34 ) ), ssSkP0( Z, Y, X ), ~( ssSkP1( Z, Y, X ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 47, [ ~( cannon( X, skf12( X, Y, Z ) ) ), ~( ssSkP1( T, Y, X ) ),
% 0.77/1.34 present( X, skf15( X, U ) ), ssSkP0( W, Y, X ), ~( member( X, skf12( X, Y
% 0.77/1.34 , Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 105, [ event( skc50, skf15( skc50, X ) ), ~( cannon( skc50, skf12(
% 0.77/1.34 skc50, Y, skc51 ) ) ), ssSkC0, shot( skc50, skf19( skc50, skc51, Z ) ),
% 0.77/1.34 ssSkP0( skc51, Y, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 106, [ event( X, skf15( X, Y ) ), ~( cannon( X, skf12( X, Z, T ) )
% 0.77/1.34 ), cannon( X, skf19( X, U, W ) ), ssSkP0( T, Z, X ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 112, [ ssSkC0, shot( skc50, skf21( skc50, skc51 ) ), event( skc50,
% 0.77/1.34 skf15( skc50, X ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 46, [ ~( cannon( X, skf19( X, Y, Z ) ) ), ~( ssSkP1( T, Z, X ) ),
% 0.77/1.34 present( X, skf15( X, U ) ), ssSkP1( Y, Z, X ), ~( member( X, skf19( X, Y
% 0.77/1.34 , Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 107, [ event( skc50, skf15( skc50, X ) ), ~( cannon( skc50, skf12(
% 0.77/1.34 skc50, skc52, skc51 ) ) ), ssSkC0, ssSkP0( skc51, skc52, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 104, [ event( X, skf15( X, T ) ), ~( cannon( X, skf12( X, Y, Z ) )
% 0.77/1.34 ), ssSkP0( Z, Y, X ), ~( ssSkP1( Z, Y, X ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 45, [ ~( cannon( X, skf12( X, Y, Z ) ) ), ~( ssSkP1( T, Y, X ) ),
% 0.77/1.34 event( X, skf15( X, U ) ), ssSkP0( W, Y, X ), ~( member( X, skf12( X, Y,
% 0.77/1.34 Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 102, [ ssSkC0, ~( shot( skc50, skf21( skc50, Y ) ) ), ~( cannon(
% 0.77/1.34 skc50, skf12( skc50, skc52, skc51 ) ) ), man( skc50, skf16( skc50, X ) )
% 0.77/1.34 ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 93, [ ~( cannon( skc50, skf12( skc50, X, skc51 ) ) ), man( skc50,
% 0.77/1.34 skf16( skc50, Y ) ), ssSkC0, shot( skc50, skf19( skc50, skc51, Z ) ),
% 0.77/1.34 ssSkP0( skc51, X, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 44, [ ~( cannon( X, skf19( X, Y, Z ) ) ), ~( ssSkP1( T, Z, X ) ),
% 0.77/1.34 event( X, skf15( X, U ) ), ssSkP1( Y, Z, X ), ~( member( X, skf19( X, Y,
% 0.77/1.34 Z ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 94, [ ~( cannon( X, skf12( X, Y, Z ) ) ), man( X, skf16( X, T ) ),
% 0.77/1.34 cannon( X, skf19( X, U, W ) ), ssSkP0( Z, Y, X ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 96, [ ~( cannon( skc50, skf12( skc50, skc52, skc51 ) ) ), ssSkC0,
% 0.77/1.34 shot( skc50, skf21( skc50, skc51 ) ), man( skc50, skf16( skc50, X ) ) ]
% 0.77/1.34 )
% 0.77/1.34 .
% 0.77/1.34 clause( 95, [ ~( cannon( skc50, skf12( skc50, skc52, skc51 ) ) ), man(
% 0.77/1.34 skc50, skf16( skc50, X ) ), ssSkC0, ssSkP0( skc51, skc52, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 92, [ ~( cannon( X, skf12( X, Y, Z ) ) ), man( X, skf16( X, T ) ),
% 0.77/1.34 ssSkP0( Z, Y, X ), ~( ssSkP1( Z, Y, X ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 43, [ ~( cannon( X, skf12( X, Y, Z ) ) ), ~( ssSkP1( T, Y, X ) ),
% 0.77/1.34 man( X, skf16( X, U ) ), ssSkP0( W, Y, X ), ~( member( X, skf12( X, Y, Z
% 0.77/1.34 ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 90, [ ssSkC0, ~( shot( skc50, skf21( skc50, X ) ) ), fire( skc50,
% 0.77/1.34 skf15( skc50, Y ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 42, [ ~( cannon( X, skf19( X, Y, Z ) ) ), ~( ssSkP1( T, Z, X ) ),
% 0.77/1.34 man( X, skf16( X, U ) ), ssSkP1( Y, Z, X ), ~( member( X, skf19( X, Y, Z
% 0.77/1.34 ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 39, [ ~( event( X, Y ) ), ~( present( X, Y ) ), ~( nonreflexive( X
% 0.77/1.34 , Y ) ), ~( fire( X, Y ) ), ~( patient( X, Y, skf19( X, Z, T ) ) ), ~(
% 0.77/1.34 'from_loc'( X, Y, skf19( X, Z, T ) ) ), ~( man( X, U ) ), ssSkP1( W, V0,
% 0.77/1.34 X ), ~( agent( X, Y, U ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 73, [ fire( skc50, skf15( skc50, X ) ), ~( cannon( skc50, skf12(
% 0.77/1.34 skc50, Y, skc51 ) ) ), ssSkC0, shot( skc50, skf19( skc50, skc51, Z ) ),
% 0.77/1.34 ssSkP0( skc51, Y, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 74, [ fire( X, skf15( X, Y ) ), ~( cannon( X, skf12( X, Z, T ) ) )
% 0.77/1.34 , cannon( X, skf19( X, U, W ) ), ssSkP0( T, Z, X ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 81, [ ssSkC0, shot( skc50, skf21( skc50, skc51 ) ), fire( skc50,
% 0.77/1.34 skf15( skc50, X ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 38, [ ~( fire( X, Y ) ), ~( nonreflexive( X, Y ) ), ~( present( X,
% 0.77/1.34 Y ) ), ~( patient( X, Y, skf12( X, Z, T ) ) ), ~( 'from_loc'( X, Y, skf12(
% 0.77/1.34 X, Z, T ) ) ), ~( event( X, Y ) ), ssSkP0( U, W, X ), ~( agent( X, Y,
% 0.77/1.34 skf14( X, T, Z ) ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 75, [ fire( skc50, skf15( skc50, X ) ), ~( cannon( skc50, skf12(
% 0.77/1.34 skc50, skc52, skc51 ) ) ), ssSkC0, ssSkP0( skc51, skc52, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 72, [ fire( X, skf15( X, T ) ), ~( cannon( X, skf12( X, Y, Z ) ) )
% 0.77/1.34 , ssSkP0( Z, Y, X ), ~( ssSkP1( Z, Y, X ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 51, [ ~( cannon( X, skf12( X, Y, Z ) ) ), ~( ssSkP1( T, Y, X ) ),
% 0.77/1.34 fire( X, skf15( X, U ) ), ssSkP0( W, Y, X ), ~( member( X, skf12( X, Y, Z
% 0.77/1.34 ), T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 35, [ ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~( man( X, U ) )
% 0.77/1.34 , ~( ssSkP0( T, Z, X ) ), ~( of( X, Y, Z ) ), patient( X, skf10( X, U, Y
% 0.77/1.34 ), Y ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 37, [ ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~( man( X, U ) )
% 0.77/1.34 , ~( ssSkP0( T, Z, X ) ), ~( of( X, Y, Z ) ), 'from_loc'( X, skf10( X, U
% 0.77/1.34 , Y ), Y ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 36, [ ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~( man( X, U ) )
% 0.77/1.34 , ~( ssSkP0( T, Z, X ) ), ~( of( X, Y, Z ) ), agent( X, skf10( X, U, W )
% 0.77/1.34 , U ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 32, [ ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~( man( X, U ) )
% 0.77/1.34 , ~( ssSkP0( T, Z, X ) ), nonreflexive( X, skf10( X, W, V0 ) ), ~( of( X
% 0.77/1.34 , Y, Z ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 33, [ ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~( man( X, U ) )
% 0.77/1.34 , ~( ssSkP0( T, Z, X ) ), present( X, skf10( X, W, V0 ) ), ~( of( X, Y, Z
% 0.77/1.34 ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 31, [ ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~( man( X, U ) )
% 0.77/1.34 , ~( ssSkP0( T, Z, X ) ), fire( X, skf10( X, W, V0 ) ), ~( of( X, Y, Z )
% 0.77/1.34 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 34, [ ~( cannon( X, Y ) ), ~( member( X, Y, T ) ), ~( man( X, U ) )
% 0.77/1.34 , ~( ssSkP0( T, Z, X ) ), event( X, skf10( X, W, V0 ) ), ~( of( X, Y, Z )
% 0.77/1.34 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 54, [ ~( shot( X, skf21( X, Z ) ) ), ~( six( X, Y ) ), ~( group( X
% 0.77/1.34 , Y ) ), ~( 'actual_world'( X ) ), ssSkC0, ~( male( X, T ) ), man( X,
% 0.77/1.34 skf14( X, U, W ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 53, [ ~( shot( X, skf21( X, Z ) ) ), ~( six( X, Y ) ), ~( group( X
% 0.77/1.34 , Y ) ), ~( 'actual_world'( X ) ), ssSkC0, ~( male( X, T ) ), cannon( X,
% 0.77/1.34 skf12( X, U, W ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 30, [ ~( six( X, Y ) ), ~( group( X, Y ) ), ~( male( X, Z ) ), ~(
% 0.77/1.34 'actual_world'( X ) ), ~( ssSkP1( Y, Z, X ) ), member( X, skf9( X, Y ), Y
% 0.77/1.34 ), ~( ssSkC0 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 61, [ ssSkC0, ~( shot( skc50, skf21( skc50, X ) ) ), shot( skc50,
% 0.77/1.34 skf12( skc50, Y, skc51 ) ), ~( male( skc50, Y ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 57, [ ssSkC0, shot( skc50, skf21( skc50, skc51 ) ), shot( skc50,
% 0.77/1.34 skf12( skc50, X, skc51 ) ), ~( male( skc50, X ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 28, [ ~( cannon( X, Y ) ), ~( member( X, Y, Z ) ), ~( ssSkP1( Z, T
% 0.77/1.34 , X ) ), ~( of( X, Y, T ) ), agent( X, skf15( X, U ), skf16( X, U ) ) ]
% 0.77/1.34 )
% 0.77/1.34 .
% 0.77/1.34 clause( 59, [ ssSkC0, shot( skc50, skf21( skc50, skc51 ) ), ~( male( skc50
% 0.77/1.34 , X ) ), man( skc50, skf14( skc50, Y, Z ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 58, [ ssSkC0, shot( skc50, skf21( skc50, skc51 ) ), ~( male( skc50
% 0.77/1.34 , X ) ), cannon( skc50, skf12( skc50, Y, Z ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 56, [ ssSkC0, shot( skc50, skf21( skc50, skc51 ) ), ~( male( skc50
% 0.77/1.34 , X ) ), ~( ssSkP0( skc51, X, skc50 ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 27, [ ~( six( X, Y ) ), ~( group( X, Y ) ), ~( male( X, Z ) ), ~(
% 0.77/1.34 'actual_world'( X ) ), ssSkC0, ~( ssSkP0( Y, Z, X ) ), member( X, skf21(
% 0.77/1.34 X, Y ), Y ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 26, [ ~( six( X, Y ) ), ~( shot( X, skf21( X, Z ) ) ), ~( group( X
% 0.77/1.34 , Y ) ), ~( male( X, T ) ), ~( 'actual_world'( X ) ), ssSkC0, ~( ssSkP0(
% 0.77/1.34 Y, T, X ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 29, [ ~( six( X, Y ) ), ~( shot( X, skf9( X, Z ) ) ), ~( group( X,
% 0.77/1.34 Y ) ), ~( male( X, T ) ), ~( 'actual_world'( X ) ), ~( ssSkP1( Y, T, X )
% 0.77/1.34 ), ~( ssSkC0 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 24, [ ~( cannon( X, Y ) ), ~( member( X, Y, Z ) ), ~( ssSkP1( Z, T
% 0.77/1.34 , X ) ), ~( of( X, Y, T ) ), patient( X, skf15( X, Y ), Y ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 25, [ ~( cannon( X, Y ) ), ~( member( X, Y, Z ) ), ~( ssSkP1( Z, T
% 0.77/1.34 , X ) ), ~( of( X, Y, T ) ), 'from_loc'( X, skf15( X, Y ), Y ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 20, [ ~( cannon( X, Y ) ), ~( member( X, Y, Z ) ), ~( ssSkP1( Z, T
% 0.77/1.34 , X ) ), fire( X, skf15( X, U ) ), ~( of( X, Y, T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 21, [ ~( cannon( X, Y ) ), ~( member( X, Y, Z ) ), ~( ssSkP1( Z, T
% 0.77/1.34 , X ) ), nonreflexive( X, skf15( X, U ) ), ~( of( X, Y, T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 22, [ ~( cannon( X, Y ) ), ~( member( X, Y, Z ) ), ~( ssSkP1( Z, T
% 0.77/1.34 , X ) ), present( X, skf15( X, U ) ), ~( of( X, Y, T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 23, [ ~( cannon( X, Y ) ), ~( member( X, Y, Z ) ), ~( ssSkP1( Z, T
% 0.77/1.34 , X ) ), event( X, skf15( X, U ) ), ~( of( X, Y, T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 41, [ ssSkC0, shot( skc50, skf12( skc50, X, skc51 ) ), ssSkP0(
% 0.77/1.34 skc51, X, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 19, [ ~( cannon( X, Y ) ), ~( member( X, Y, Z ) ), ~( ssSkP1( Z, T
% 0.77/1.34 , X ) ), man( X, skf16( X, U ) ), ~( of( X, Y, T ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 40, [ ssSkC0, shot( skc50, skf19( skc50, skc51, Y ) ), ssSkP1(
% 0.77/1.34 skc51, X, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 16, [ ssSkP0( X, Y, Z ), member( Z, skf12( Z, Y, X ), X ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 18, [ ssSkP1( X, Y, Z ), of( Z, skf19( Z, X, Y ), Y ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 17, [ ssSkP1( X, Y, Z ), member( Z, skf19( Z, X, T ), X ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 15, [ ssSkP0( X, Y, Z ), of( Z, skf12( Z, Y, T ), Y ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 12, [ cannon( Z, skf12( Z, T, U ) ), ssSkP0( X, Y, Z ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 13, [ man( Z, skf14( Z, T, U ) ), ssSkP0( X, Y, Z ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 14, [ cannon( Z, skf19( Z, T, U ) ), ssSkP1( X, Y, Z ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 11, [ ~( member( skc6, X, skc7 ) ), shot( skc6, X ), ~( ssSkC0 ) ]
% 0.77/1.34 )
% 0.77/1.34 .
% 0.77/1.34 clause( 10, [ ssSkC0, shot( skc50, X ), ~( member( skc50, X, skc51 ) ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 8, [ ssSkC0, ssSkP1( skc51, skc52, skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 9, [ ssSkP0( skc7, skc8, skc6 ), ~( ssSkC0 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 3, [ ssSkC0, group( skc50, skc51 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 4, [ ssSkC0, male( skc50, skc52 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 2, [ ssSkC0, six( skc50, skc51 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 5, [ six( skc6, skc7 ), ~( ssSkC0 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 6, [ group( skc6, skc7 ), ~( ssSkC0 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 7, [ male( skc6, skc8 ), ~( ssSkC0 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 0, [ 'actual_world'( skc50 ) ] )
% 0.77/1.34 .
% 0.77/1.34 clause( 1, [ 'actual_world'( skc6 ) ] )
% 0.77/1.34 .
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 % SZS output end Saturation
% 0.77/1.34 end of saturation!
% 0.77/1.34
% 0.77/1.34 Memory use:
% 0.77/1.34
% 0.77/1.34 space for terms: 8785
% 0.77/1.34 space for clauses: 8346
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 clauses generated: 254
% 0.77/1.34 clauses kept: 185
% 0.77/1.34 clauses selected: 141
% 0.77/1.34 clauses deleted: 59
% 0.77/1.34 clauses inuse deleted: 15
% 0.77/1.34
% 0.77/1.34 subsentry: 243
% 0.77/1.34 literals s-matched: 109
% 0.77/1.34 literals matched: 109
% 0.77/1.34 full subsumption: 19
% 0.77/1.34
% 0.77/1.34 checksum: 2029842493
% 0.77/1.34
% 0.77/1.34
% 0.77/1.34 Bliksem ended
%------------------------------------------------------------------------------