%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : KRS011-1 : TPTP v8.1.0. Released v2.0.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 02:41:57 EDT 2022
% Result : Satisfiable 0.76s 1.39s
% Output : Saturation 0.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS011-1 : TPTP v8.1.0. Released v2.0.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 Jun 7 07:51:10 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.76/1.20 *** allocated 10000 integers for termspace/termends
% 0.76/1.20 *** allocated 10000 integers for clauses
% 0.76/1.20 *** allocated 10000 integers for justifications
% 0.76/1.20 Bliksem 1.12
% 0.76/1.20
% 0.76/1.20
% 0.76/1.20 Automatic Strategy Selection
% 0.76/1.20
% 0.76/1.20 Clauses:
% 0.76/1.20 [
% 0.76/1.20 [ f( exists ) ],
% 0.76/1.20 [ ~( g( exists ) ) ],
% 0.76/1.20 [ r( X, Y ), ~( r1( X, Y ) ) ],
% 0.76/1.20 [ r( X, Y ), ~( r2( X, Y ) ) ],
% 0.76/1.20 [ r( X, Y ), ~( r3( X, Y ) ) ],
% 0.76/1.20 [ t( X, Y ), ~( t1( X, Y ) ) ],
% 0.76/1.20 [ t( X, Y ), ~( t2( X, Y ) ) ],
% 0.76/1.20 [ t( X, Y ), ~( t3( X, Y ) ) ],
% 0.76/1.20 [ ~( c( X ) ), ~( e( X ) ) ],
% 0.76/1.20 [ ~( c( X ) ), ~( d( X ) ) ],
% 0.76/1.20 [ ~( d( X ) ), ~( e( X ) ) ],
% 0.76/1.20 [ ~( d( X ) ), ~( c( X ) ) ],
% 0.76/1.20 [ ~( e( X ) ), ~( d( X ) ) ],
% 0.76/1.20 [ ~( e( X ) ), ~( c( X ) ) ],
% 0.76/1.20 [ c( u9r5( X ) ), ~( f1( X ) ) ],
% 0.76/1.20 [ t1( u9r4( X ), u9r5( X ) ), ~( f1( X ) ) ],
% 0.76/1.20 [ equalish( X, Y ), equalish( X, Z ), equalish( Y, Z ), ~( f1( T ) ),
% 0.76/1.20 ~( t( u9r4( T ), X ) ), ~( t( u9r4( T ), Y ) ), ~( t( u9r4( T ), Z ) ) ]
% 0.76/1.20 ,
% 0.76/1.20 [ r1( X, u9r4( X ) ), ~( f1( X ) ) ],
% 0.76/1.20 [ f1( X ), ~( r1( X, Y ) ), ~( equalish( u9r2( Y, X ), u9r1( Y, X ) ) )
% 0.76/1.20 , ~( t1( Y, Z ) ), ~( c( Z ) ) ],
% 0.76/1.20 [ f1( X ), ~( r1( X, Y ) ), ~( equalish( u9r3( Y, X ), u9r1( Y, X ) ) )
% 0.76/1.20 , ~( t1( Y, Z ) ), ~( c( Z ) ) ],
% 0.76/1.20 [ f1( X ), ~( r1( X, Y ) ), ~( equalish( u9r3( Y, X ), u9r2( Y, X ) ) )
% 0.76/1.20 , ~( t1( Y, Z ) ), ~( c( Z ) ) ],
% 0.76/1.20 [ f1( X ), t( Y, u9r1( Y, X ) ), ~( r1( X, Y ) ), ~( t1( Y, Z ) ), ~( c(
% 0.76/1.20 Z ) ) ],
% 0.76/1.20 [ f1( X ), t( Y, u9r2( Y, X ) ), ~( r1( X, Y ) ), ~( t1( Y, Z ) ), ~( c(
% 0.76/1.20 Z ) ) ],
% 0.76/1.20 [ f1( X ), t( Y, u9r3( Y, X ) ), ~( r1( X, Y ) ), ~( t1( Y, Z ) ), ~( c(
% 0.76/1.20 Z ) ) ],
% 0.76/1.20 [ d( u10r5( X ) ), ~( f2( X ) ) ],
% 0.76/1.20 [ t2( u10r4( X ), u10r5( X ) ), ~( f2( X ) ) ],
% 0.76/1.20 [ equalish( X, Y ), equalish( X, Z ), equalish( Y, Z ), ~( f2( T ) ),
% 0.76/1.20 ~( t( u10r4( T ), X ) ), ~( t( u10r4( T ), Y ) ), ~( t( u10r4( T ), Z ) )
% 0.76/1.20 ],
% 0.76/1.20 [ r2( X, u10r4( X ) ), ~( f2( X ) ) ],
% 0.76/1.20 [ f2( X ), ~( r2( X, Y ) ), ~( equalish( u10r2( Y, X ), u10r1( Y, X ) )
% 0.76/1.20 ), ~( t2( Y, Z ) ), ~( d( Z ) ) ],
% 0.76/1.20 [ f2( X ), ~( r2( X, Y ) ), ~( equalish( u10r3( Y, X ), u10r1( Y, X ) )
% 0.76/1.20 ), ~( t2( Y, Z ) ), ~( d( Z ) ) ],
% 0.76/1.20 [ f2( X ), ~( r2( X, Y ) ), ~( equalish( u10r3( Y, X ), u10r2( Y, X ) )
% 0.76/1.20 ), ~( t2( Y, Z ) ), ~( d( Z ) ) ],
% 0.76/1.20 [ f2( X ), t( Y, u10r1( Y, X ) ), ~( r2( X, Y ) ), ~( t2( Y, Z ) ), ~( d(
% 0.76/1.20 Z ) ) ],
% 0.76/1.20 [ f2( X ), t( Y, u10r2( Y, X ) ), ~( r2( X, Y ) ), ~( t2( Y, Z ) ), ~( d(
% 0.76/1.20 Z ) ) ],
% 0.76/1.20 [ f2( X ), t( Y, u10r3( Y, X ) ), ~( r2( X, Y ) ), ~( t2( Y, Z ) ), ~( d(
% 0.76/1.20 Z ) ) ],
% 0.76/1.20 [ e( u11r5( X ) ), ~( f3( X ) ) ],
% 0.76/1.20 [ t3( u11r4( X ), u11r5( X ) ), ~( f3( X ) ) ],
% 0.76/1.20 [ equalish( X, Y ), equalish( X, Z ), equalish( Y, Z ), ~( f3( T ) ),
% 0.76/1.20 ~( t( u11r4( T ), X ) ), ~( t( u11r4( T ), Y ) ), ~( t( u11r4( T ), Z ) )
% 0.76/1.20 ],
% 0.76/1.20 [ r3( X, u11r4( X ) ), ~( f3( X ) ) ],
% 0.76/1.20 [ f3( X ), ~( r3( X, Y ) ), ~( equalish( u11r2( Y, X ), u11r1( Y, X ) )
% 0.76/1.20 ), ~( t3( Y, Z ) ), ~( e( Z ) ) ],
% 0.76/1.20 [ f3( X ), ~( r3( X, Y ) ), ~( equalish( u11r3( Y, X ), u11r1( Y, X ) )
% 0.76/1.20 ), ~( t3( Y, Z ) ), ~( e( Z ) ) ],
% 0.76/1.20 [ f3( X ), ~( r3( X, Y ) ), ~( equalish( u11r3( Y, X ), u11r2( Y, X ) )
% 0.76/1.20 ), ~( t3( Y, Z ) ), ~( e( Z ) ) ],
% 0.76/1.20 [ f3( X ), t( Y, u11r1( Y, X ) ), ~( r3( X, Y ) ), ~( t3( Y, Z ) ), ~( e(
% 0.76/1.20 Z ) ) ],
% 0.76/1.20 [ f3( X ), t( Y, u11r2( Y, X ) ), ~( r3( X, Y ) ), ~( t3( Y, Z ) ), ~( e(
% 0.76/1.20 Z ) ) ],
% 0.76/1.20 [ f3( X ), t( Y, u11r3( Y, X ) ), ~( r3( X, Y ) ), ~( t3( Y, Z ) ), ~( e(
% 0.76/1.20 Z ) ) ],
% 0.76/1.20 [ f3( X ), ~( f( X ) ) ],
% 0.76/1.20 [ f2( X ), ~( f( X ) ) ],
% 0.76/1.20 [ f1( X ), ~( f( X ) ) ],
% 0.76/1.20 [ f( X ), ~( f1( X ) ), ~( f2( X ) ), ~( f3( X ) ) ],
% 0.76/1.20 [ r2least( X ), ~( g( X ) ) ],
% 0.76/1.20 [ g( X ), ~( r2least( X ) ) ],
% 0.76/1.20 [ ~( r2least( X ) ), ~( equalish( u14r2( X ), u14r1( X ) ) ) ],
% 0.76/1.20 [ r( X, u14r1( X ) ), ~( r2least( X ) ) ],
% 0.76/1.20 [ r( X, u14r2( X ) ), ~( r2least( X ) ) ],
% 0.76/1.20 [ r2least( X ), equalish( Y, Z ), ~( r( X, Y ) ), ~( r( X, Z ) ) ]
% 0.76/1.20 ] .
% 0.76/1.20
% 0.76/1.20
% 0.76/1.20 percentage equality = 0.000000, percentage horn = 0.745098
% 0.76/1.20 This a non-horn, non-equality problem
% 0.76/1.20
% 0.76/1.20
% 0.76/1.20 Options Used:
% 0.76/1.20
% 0.76/1.20 useres = 1
% 0.76/1.20 useparamod = 0
% 0.76/1.20 useeqrefl = 0
% 0.76/1.20 useeqfact = 0
% 0.76/1.20 usefactor = 1
% 0.76/1.20 usesimpsplitting = 0
% 0.76/1.20 usesimpdemod = 0
% 0.76/1.20 usesimpres = 3
% 0.76/1.20
% 0.76/1.20 resimpinuse = 1000
% 0.76/1.20 resimpclauses = 20000
% 0.76/1.38 substype = standard
% 0.76/1.38 backwardsubs = 1
% 0.76/1.38 selectoldest = 5
% 0.76/1.38
% 0.76/1.38 litorderings [0] = split
% 0.76/1.38 litorderings [1] = liftord
% 0.76/1.38
% 0.76/1.38 termordering = none
% 0.76/1.38
% 0.76/1.38 litapriori = 1
% 0.76/1.38 termapriori = 0
% 0.76/1.38 litaposteriori = 0
% 0.76/1.38 termaposteriori = 0
% 0.76/1.38 demodaposteriori = 0
% 0.76/1.38 ordereqreflfact = 0
% 0.76/1.38
% 0.76/1.38 litselect = none
% 0.76/1.38
% 0.76/1.38 maxweight = 15
% 0.76/1.38 maxdepth = 30000
% 0.76/1.38 maxlength = 115
% 0.76/1.38 maxnrvars = 195
% 0.76/1.38 excuselevel = 1
% 0.76/1.38 increasemaxweight = 1
% 0.76/1.38
% 0.76/1.38 maxselected = 10000000
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38
% 0.76/1.38 showgenerated = 0
% 0.76/1.38 showkept = 0
% 0.76/1.38 showselected = 0
% 0.76/1.38 showdeleted = 0
% 0.76/1.38 showresimp = 1
% 0.76/1.38 showstatus = 2000
% 0.76/1.38
% 0.76/1.38 prologoutput = 1
% 0.76/1.38 nrgoals = 5000000
% 0.76/1.38 totalproof = 1
% 0.76/1.38
% 0.76/1.38 Symbols occurring in the translation:
% 0.76/1.38
% 0.76/1.38 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.76/1.38 . [1, 2] (w:1, o:38, a:1, s:1, b:0),
% 0.76/1.38 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 0.76/1.38 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.76/1.38 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.76/1.38 exists [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.76/1.38 f [40, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.76/1.38 g [41, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.76/1.38 r [44, 2] (w:1, o:63, a:1, s:1, b:0),
% 0.76/1.38 r1 [45, 2] (w:1, o:64, a:1, s:1, b:0),
% 0.76/1.38 r2 [46, 2] (w:1, o:65, a:1, s:1, b:0),
% 0.76/1.38 r3 [47, 2] (w:1, o:66, a:1, s:1, b:0),
% 0.76/1.38 t [48, 2] (w:1, o:67, a:1, s:1, b:0),
% 0.76/1.38 t1 [49, 2] (w:1, o:68, a:1, s:1, b:0),
% 0.76/1.38 t2 [50, 2] (w:1, o:69, a:1, s:1, b:0),
% 0.76/1.38 t3 [51, 2] (w:1, o:70, a:1, s:1, b:0),
% 0.76/1.38 c [52, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.76/1.38 e [53, 1] (w:1, o:22, a:1, s:1, b:0),
% 0.76/1.38 d [54, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.76/1.38 u9r5 [55, 1] (w:1, o:30, a:1, s:1, b:0),
% 0.76/1.38 f1 [56, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.76/1.38 u9r4 [57, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.76/1.38 equalish [60, 2] (w:1, o:71, a:1, s:1, b:0),
% 0.76/1.38 u9r2 [62, 2] (w:1, o:73, a:1, s:1, b:0),
% 0.76/1.38 u9r1 [63, 2] (w:1, o:72, a:1, s:1, b:0),
% 0.76/1.38 u9r3 [65, 2] (w:1, o:74, a:1, s:1, b:0),
% 0.76/1.38 u10r5 [66, 1] (w:1, o:32, a:1, s:1, b:0),
% 0.76/1.38 f2 [67, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.76/1.38 u10r4 [68, 1] (w:1, o:31, a:1, s:1, b:0),
% 0.76/1.38 u10r2 [69, 2] (w:1, o:76, a:1, s:1, b:0),
% 0.76/1.38 u10r1 [70, 2] (w:1, o:75, a:1, s:1, b:0),
% 0.76/1.38 u10r3 [71, 2] (w:1, o:77, a:1, s:1, b:0),
% 0.76/1.38 u11r5 [72, 1] (w:1, o:34, a:1, s:1, b:0),
% 0.76/1.38 f3 [73, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.76/1.38 u11r4 [74, 1] (w:1, o:33, a:1, s:1, b:0),
% 0.76/1.38 u11r2 [75, 2] (w:1, o:79, a:1, s:1, b:0),
% 0.76/1.38 u11r1 [76, 2] (w:1, o:78, a:1, s:1, b:0),
% 0.76/1.38 u11r3 [77, 2] (w:1, o:80, a:1, s:1, b:0),
% 0.76/1.38 r2least [78, 1] (w:1, o:35, a:1, s:1, b:0),
% 0.76/1.38 u14r2 [79, 1] (w:1, o:37, a:1, s:1, b:0),
% 0.76/1.38 u14r1 [80, 1] (w:1, o:36, a:1, s:1, b:0).
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 15
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 550
% 0.76/1.38 Kept: 184
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 16
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 16
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 550
% 0.76/1.38 Kept: 184
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 17
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 17
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 550
% 0.76/1.38 Kept: 184
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 18
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 18
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 550
% 0.76/1.38 Kept: 184
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 19
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 19
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 550
% 0.76/1.38 Kept: 184
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 20
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 20
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 550
% 0.76/1.38 Kept: 184
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 21
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 21
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 550
% 0.76/1.38 Kept: 184
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 22
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 22
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 23
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 23
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 24
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 24
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 25
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 25
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 26
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 26
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 27
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 27
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 28
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 28
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 29
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 29
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 30
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 30
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 31
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 31
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 32
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 32
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 33
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 33
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 34
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 34
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 35
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 35
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 36
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 36
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.38 Generated: 559
% 0.76/1.38 Kept: 193
% 0.76/1.38
% 0.76/1.38
% 0.76/1.38 The strategy used was not complete!
% 0.76/1.38
% 0.76/1.38 Increased maxweight to 37
% 0.76/1.38
% 0.76/1.38 Starting Search:
% 0.76/1.38
% 0.76/1.38 Resimplifying inuse:
% 0.76/1.38 Done
% 0.76/1.38
% 0.76/1.38 Failed to find proof!
% 0.76/1.38 maxweight = 37
% 0.76/1.38 maxnrclauses = 10000000
% 0.76/1.39 Generated: 559
% 0.76/1.39 Kept: 193
% 0.76/1.39
% 0.76/1.39
% 0.76/1.39 The strategy used was not complete!
% 0.76/1.39
% 0.76/1.39 Increased maxweight to 38
% 0.76/1.39
% 0.76/1.39 Starting Search:
% 0.76/1.39
% 0.76/1.39 Resimplifying inuse:
% 0.76/1.39 Done
% 0.76/1.39
% 0.76/1.39 Failed to find proof!
% 0.76/1.39 maxweight = 38
% 0.76/1.39 maxnrclauses = 10000000
% 0.76/1.39 Generated: 559
% 0.76/1.39 Kept: 193
% 0.76/1.39
% 0.76/1.39
% 0.76/1.39 The strategy used was not complete!
% 0.76/1.39
% 0.76/1.39 Increased maxweight to 39
% 0.76/1.39
% 0.76/1.39 Starting Search:
% 0.76/1.39
% 0.76/1.39 Resimplifying inuse:
% 0.76/1.39 Done
% 0.76/1.39
% 0.76/1.39 Failed to find proof!
% 0.76/1.39 maxweight = 39
% 0.76/1.39 maxnrclauses = 10000000
% 0.76/1.39 Generated: 559
% 0.76/1.39 Kept: 193
% 0.76/1.39
% 0.76/1.39
% 0.76/1.39 The strategy used was not complete!
% 0.76/1.39
% 0.76/1.39 Increased maxweight to 40
% 0.76/1.39
% 0.76/1.39 Starting Search:
% 0.76/1.39
% 0.76/1.39 Resimplifying inuse:
% 0.76/1.39 Done
% 0.76/1.39
% 0.76/1.39 Failed to find proof!
% 0.76/1.39 maxweight = 40
% 0.76/1.39 maxnrclauses = 10000000
% 0.76/1.39 Generated: 559
% 0.76/1.39 Kept: 193
% 0.76/1.39
% 0.76/1.39
% 0.76/1.39 The strategy used was not complete!
% 0.76/1.39
% 0.76/1.39 Increased maxweight to 41
% 0.76/1.39
% 0.76/1.39 Starting Search:
% 0.76/1.39
% 0.76/1.39 Resimplifying inuse:
% 0.76/1.39 Done
% 0.76/1.39
% 0.76/1.39 Failed to find proof!
% 0.76/1.39 maxweight = 41
% 0.76/1.39 maxnrclauses = 10000000
% 0.76/1.39 Generated: 559
% 0.76/1.39 Kept: 193
% 0.76/1.39
% 0.76/1.39
% 0.76/1.39 The strategy used was not complete!
% 0.76/1.39
% 0.76/1.39 Increased maxweight to 42
% 0.76/1.39
% 0.76/1.39 Starting Search:
% 0.76/1.39
% 0.76/1.39 Resimplifying inuse:
% 0.76/1.39 Done
% 0.76/1.39
% 0.76/1.39
% 0.76/1.39
% 0.76/1.39 found a saturation!
% 0.76/1.39 % SZS status Satisfiable
% 0.76/1.39 % SZS output start Saturation
% 0.76/1.39
% 0.76/1.39 clause( 125, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u10r3( Y, X ) ) ), ~( t( u9r4( T ), U ) ), ~( t( u9r4( T ),
% 0.76/1.39 u10r1( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( u10r3( Y, X ), U ),
% 0.76/1.39 equalish( U, u10r1( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 124, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u10r3( Y, X ) ) ), ~( t( u9r4( T ), u10r1( Y, X ) ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t2( Y, Z ) ), equalish( u10r1( Y, X ), U ), equalish(
% 0.76/1.39 u10r3( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 123, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t( u9r4( T ), u10r3( Y, X ) ) ), ~( t( u9r4( T ),
% 0.76/1.39 u10r1( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( U, u10r1( Y, X ) ),
% 0.76/1.39 equalish( U, u10r3( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 132, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u10r3( Y, X ) ) ), ~( t( u9r4( T ), U ) ), ~( t( u9r4( T ),
% 0.76/1.39 u10r2( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( u10r3( Y, X ), U ),
% 0.76/1.39 equalish( U, u10r2( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 131, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u10r3( Y, X ) ) ), ~( t( u9r4( T ), u10r2( Y, X ) ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t2( Y, Z ) ), equalish( u10r2( Y, X ), U ), equalish(
% 0.76/1.39 u10r3( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 130, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t( u9r4( T ), u10r3( Y, X ) ) ), ~( t( u9r4( T ),
% 0.76/1.39 u10r2( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( U, u10r2( Y, X ) ),
% 0.76/1.39 equalish( U, u10r3( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 121, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u10r3( Y, X ) ) ), ~( t( u10r4( T ), U ) ), ~( t( u10r4( T )
% 0.76/1.39 , u10r1( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( u10r3( Y, X ), U ),
% 0.76/1.39 equalish( U, u10r1( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 128, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u10r3( Y, X ) ) ), ~( t( u10r4( T ), U ) ), ~( t( u10r4( T )
% 0.76/1.39 , u10r2( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( u10r3( Y, X ), U ),
% 0.76/1.39 equalish( U, u10r2( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 127, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u10r3( Y, X ) ) ), ~( t( u10r4( T ), u10r2( Y, X ) ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t2( Y, Z ) ), equalish( u10r2( Y, X ), U ),
% 0.76/1.39 equalish( u10r3( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 126, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t( u10r4( T ), u10r3( Y, X ) ) ), ~( t( u10r4( T )
% 0.76/1.39 , u10r2( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( U, u10r2( Y, X ) ),
% 0.76/1.39 equalish( U, u10r3( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 139, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u11r3( Y, X ) ) ), ~( t( u9r4( T ), U ) ), ~( t( u9r4( T ),
% 0.76/1.39 u11r2( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( u11r3( Y, X ), U ),
% 0.76/1.39 equalish( U, u11r2( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 120, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u10r3( Y, X ) ) ), ~( t( u10r4( T ), u10r1( Y, X ) ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t2( Y, Z ) ), equalish( u10r1( Y, X ), U ),
% 0.76/1.39 equalish( u10r3( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 138, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u11r3( Y, X ) ) ), ~( t( u9r4( T ), u11r2( Y, X ) ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t3( Y, Z ) ), equalish( u11r2( Y, X ), U ), equalish(
% 0.76/1.39 u11r3( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 137, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t( u9r4( T ), u11r3( Y, X ) ) ), ~( t( u9r4( T ),
% 0.76/1.39 u11r2( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( U, u11r2( Y, X ) ),
% 0.76/1.39 equalish( U, u11r3( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 135, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u11r3( Y, X ) ) ), ~( t( u10r4( T ), U ) ), ~( t( u10r4( T )
% 0.76/1.39 , u11r2( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( u11r3( Y, X ), U ),
% 0.76/1.39 equalish( U, u11r2( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 134, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u11r3( Y, X ) ) ), ~( t( u10r4( T ), u11r2( Y, X ) ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t3( Y, Z ) ), equalish( u11r2( Y, X ), U ),
% 0.76/1.39 equalish( u11r3( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 119, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t( u10r4( T ), u10r3( Y, X ) ) ), ~( t( u10r4( T )
% 0.76/1.39 , u10r1( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( U, u10r1( Y, X ) ),
% 0.76/1.39 equalish( U, u10r3( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 133, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t( u10r4( T ), u11r3( Y, X ) ) ), ~( t( u10r4( T )
% 0.76/1.39 , u11r2( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( U, u11r2( Y, X ) ),
% 0.76/1.39 equalish( U, u11r3( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 146, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u11r3( Y, X ) ) ), ~( t( u9r4( T ), U ) ), ~( t( u9r4( T ),
% 0.76/1.39 u11r1( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( u11r3( Y, X ), U ),
% 0.76/1.39 equalish( U, u11r1( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 145, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u11r3( Y, X ) ) ), ~( t( u9r4( T ), u11r1( Y, X ) ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t3( Y, Z ) ), equalish( u11r1( Y, X ), U ), equalish(
% 0.76/1.39 u11r3( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 144, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t( u9r4( T ), u11r3( Y, X ) ) ), ~( t( u9r4( T ),
% 0.76/1.39 u11r1( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( U, u11r1( Y, X ) ),
% 0.76/1.39 equalish( U, u11r3( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 118, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u10r2( Y, X ) ) ), ~( t( u9r4( T ), U ) ), ~( t( u9r4( T ),
% 0.76/1.39 u10r1( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( u10r2( Y, X ), U ),
% 0.76/1.39 equalish( U, u10r1( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 142, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u11r3( Y, X ) ) ), ~( t( u10r4( T ), U ) ), ~( t( u10r4( T )
% 0.76/1.39 , u11r1( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( u11r3( Y, X ), U ),
% 0.76/1.39 equalish( U, u11r1( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 141, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u11r3( Y, X ) ) ), ~( t( u10r4( T ), u11r1( Y, X ) ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t3( Y, Z ) ), equalish( u11r1( Y, X ), U ),
% 0.76/1.39 equalish( u11r3( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 140, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t( u10r4( T ), u11r3( Y, X ) ) ), ~( t( u10r4( T )
% 0.76/1.39 , u11r1( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( U, u11r1( Y, X ) ),
% 0.76/1.39 equalish( U, u11r3( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 153, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u11r2( Y, X ) ) ), ~( t( u9r4( T ), U ) ), ~( t( u9r4( T ),
% 0.76/1.39 u11r1( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( u11r2( Y, X ), U ),
% 0.76/1.39 equalish( U, u11r1( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 117, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u10r2( Y, X ) ) ), ~( t( u9r4( T ), u10r1( Y, X ) ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t2( Y, Z ) ), equalish( u10r1( Y, X ), U ), equalish(
% 0.76/1.39 u10r2( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 152, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u11r2( Y, X ) ) ), ~( t( u9r4( T ), u11r1( Y, X ) ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t3( Y, Z ) ), equalish( u11r1( Y, X ), U ), equalish(
% 0.76/1.39 u11r2( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 246, [ ~( d( X ) ), ~( f1( Y ) ), f2( Z ), ~( r2( Z, T ) ), ~( t(
% 0.76/1.39 u9r4( Y ), u10r1( T, Z ) ) ), ~( t( u9r4( Y ), u10r2( T, Z ) ) ), ~( t(
% 0.76/1.39 u9r4( Y ), u10r3( T, Z ) ) ), ~( t2( T, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 116, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t( u9r4( T ), u10r2( Y, X ) ) ), ~( t( u9r4( T ),
% 0.76/1.39 u10r1( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( U, u10r1( Y, X ) ),
% 0.76/1.39 equalish( U, u10r2( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 242, [ ~( e( X ) ), ~( f1( Y ) ), f3( Z ), ~( r3( Z, T ) ), ~( t(
% 0.76/1.39 u9r4( Y ), u11r1( T, Z ) ) ), ~( t( u9r4( Y ), u11r2( T, Z ) ) ), ~( t(
% 0.76/1.39 u9r4( Y ), u11r3( T, Z ) ) ), ~( t3( T, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 151, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t( u9r4( T ), u11r2( Y, X ) ) ), ~( t( u9r4( T ),
% 0.76/1.39 u11r1( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( U, u11r1( Y, X ) ),
% 0.76/1.39 equalish( U, u11r2( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 114, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u10r2( Y, X ) ) ), ~( t( u10r4( T ), U ) ), ~( t( u10r4( T )
% 0.76/1.39 , u10r1( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( u10r2( Y, X ), U ),
% 0.76/1.39 equalish( U, u10r1( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 238, [ f2( X ), ~( f2( Y ) ), ~( r2( X, u10r4( Y ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 113, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u10r2( Y, X ) ) ), ~( t( u10r4( T ), u10r1( Y, X ) ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t2( Y, Z ) ), equalish( u10r1( Y, X ), U ),
% 0.76/1.39 equalish( u10r2( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 233, [ ~( d( X ) ), f2( Y ), ~( f2( Z ) ), ~( r2( Y, T ) ), ~( t(
% 0.76/1.39 u10r4( Z ), u10r1( T, Y ) ) ), ~( t( u10r4( Z ), u10r2( T, Y ) ) ), ~( t(
% 0.76/1.39 u10r4( Z ), u10r3( T, Y ) ) ), ~( t2( T, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 112, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t( u10r4( T ), u10r2( Y, X ) ) ), ~( t( u10r4( T )
% 0.76/1.39 , u10r1( Y, X ) ) ), ~( t2( Y, Z ) ), equalish( U, u10r1( Y, X ) ),
% 0.76/1.39 equalish( U, u10r2( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 149, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u11r2( Y, X ) ) ), ~( t( u10r4( T ), U ) ), ~( t( u10r4( T )
% 0.76/1.39 , u11r1( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( u11r2( Y, X ), U ),
% 0.76/1.39 equalish( U, u11r1( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 148, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), u11r2( Y, X ) ) ), ~( t( u10r4( T ), u11r1( Y, X ) ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t3( Y, Z ) ), equalish( u11r1( Y, X ), U ),
% 0.76/1.39 equalish( u11r2( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 229, [ ~( e( X ) ), ~( f2( Y ) ), f3( Z ), ~( r3( Z, T ) ), ~( t(
% 0.76/1.39 u10r4( Y ), u11r1( T, Z ) ) ), ~( t( u10r4( Y ), u11r2( T, Z ) ) ), ~( t(
% 0.76/1.39 u10r4( Y ), u11r3( T, Z ) ) ), ~( t3( T, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 111, [ ~( f2( X ) ), ~( t( u10r4( X ), u9r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u10r4( X ), T ) ), ~( t( u10r4( X ), u9r2( Y, Z ) ) ), f1( Z ), ~( r1( Z
% 0.76/1.39 , Y ) ), ~( t1( Y, U ) ), ~( c( U ) ), equalish( u9r2( Y, Z ), T ),
% 0.76/1.39 equalish( T, u9r1( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 147, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), ~( f2( T ) ), ~( t(
% 0.76/1.39 u10r4( T ), U ) ), ~( t( u10r4( T ), u11r2( Y, X ) ) ), ~( t( u10r4( T )
% 0.76/1.39 , u11r1( Y, X ) ) ), ~( t3( Y, Z ) ), equalish( U, u11r1( Y, X ) ),
% 0.76/1.39 equalish( U, u11r2( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 184, [ ~( f3( X ) ), ~( t( u11r4( X ), u9r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), T ) ), ~( t( u11r4( X ), u9r2( Y, Z ) ) ), f1( Z ), ~( r1( Z
% 0.76/1.39 , Y ) ), ~( t1( Y, U ) ), ~( c( U ) ), equalish( u9r2( Y, Z ), T ),
% 0.76/1.39 equalish( T, u9r1( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 183, [ ~( f3( X ) ), ~( t( u11r4( X ), u9r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u9r2( Y, Z ) ) ), ~( t( u11r4( X ), T ) ), equalish( u9r1( Y
% 0.76/1.39 , Z ), T ), f1( Z ), ~( r1( Z, Y ) ), ~( t1( Y, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( u9r2( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 110, [ ~( f2( X ) ), ~( t( u10r4( X ), u9r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u10r4( X ), u9r2( Y, Z ) ) ), ~( t( u10r4( X ), T ) ), equalish( u9r1( Y
% 0.76/1.39 , Z ), T ), f1( Z ), ~( r1( Z, Y ) ), ~( t1( Y, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( u9r2( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 182, [ ~( f3( X ) ), ~( t( u11r4( X ), Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u9r1( Z, T ) ) ), ~( t( u11r4( X ), u9r2( Z, T ) ) ), equalish( Y, u9r1(
% 0.76/1.39 Z, T ) ), f1( T ), ~( r1( T, Z ) ), ~( t1( Z, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( Y, u9r2( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 178, [ ~( f3( X ) ), ~( t( u11r4( X ), u9r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), T ) ), ~( t( u11r4( X ), u9r3( Y, Z ) ) ), f1( Z ), ~( r1( Z
% 0.76/1.39 , Y ) ), ~( t1( Y, U ) ), ~( c( U ) ), equalish( u9r3( Y, Z ), T ),
% 0.76/1.39 equalish( T, u9r1( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 177, [ ~( f3( X ) ), ~( t( u11r4( X ), u9r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u9r3( Y, Z ) ) ), ~( t( u11r4( X ), T ) ), equalish( u9r1( Y
% 0.76/1.39 , Z ), T ), f1( Z ), ~( r1( Z, Y ) ), ~( t1( Y, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( u9r3( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 176, [ ~( f3( X ) ), ~( t( u11r4( X ), Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u9r1( Z, T ) ) ), ~( t( u11r4( X ), u9r3( Z, T ) ) ), equalish( Y, u9r1(
% 0.76/1.39 Z, T ) ), f1( T ), ~( r1( T, Z ) ), ~( t1( Z, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( Y, u9r3( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 109, [ ~( f2( X ) ), ~( t( u10r4( X ), Y ) ), ~( t( u10r4( X ),
% 0.76/1.39 u9r1( Z, T ) ) ), ~( t( u10r4( X ), u9r2( Z, T ) ) ), equalish( Y, u9r1(
% 0.76/1.39 Z, T ) ), f1( T ), ~( r1( T, Z ) ), ~( t1( Z, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( Y, u9r2( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 175, [ ~( f3( X ) ), ~( t( u11r4( X ), u9r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), T ) ), ~( t( u11r4( X ), u9r3( Y, Z ) ) ), f1( Z ), ~( r1( Z
% 0.76/1.39 , Y ) ), ~( t1( Y, U ) ), ~( c( U ) ), equalish( u9r3( Y, Z ), T ),
% 0.76/1.39 equalish( T, u9r2( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 225, [ ~( f3( X ) ), f1( Z ), ~( r1( Z, Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u9r1( Y, Z ) ) ), ~( c( T ) ), ~( t( u11r4( X ), u9r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u9r3( Y, Z ) ) ), ~( t1( Y, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 105, [ ~( f2( X ) ), ~( t( u10r4( X ), u9r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u10r4( X ), T ) ), ~( t( u10r4( X ), u9r3( Y, Z ) ) ), f1( Z ), ~( r1( Z
% 0.76/1.39 , Y ) ), ~( t1( Y, U ) ), ~( c( U ) ), equalish( u9r3( Y, Z ), T ),
% 0.76/1.39 equalish( T, u9r1( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 174, [ ~( f3( X ) ), ~( t( u11r4( X ), u9r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u9r3( Y, Z ) ) ), ~( t( u11r4( X ), T ) ), equalish( u9r2( Y
% 0.76/1.39 , Z ), T ), f1( Z ), ~( r1( Z, Y ) ), ~( t1( Y, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( u9r3( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 173, [ ~( f3( X ) ), ~( t( u11r4( X ), Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u9r2( Z, T ) ) ), ~( t( u11r4( X ), u9r3( Z, T ) ) ), equalish( Y, u9r2(
% 0.76/1.39 Z, T ) ), f1( T ), ~( r1( T, Z ) ), ~( t1( Z, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( Y, u9r3( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 172, [ ~( f3( X ) ), ~( t( u11r4( X ), u10r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), T ) ), ~( t( u11r4( X ), u10r2( Y, Z ) ) ), f2( Z ), ~( r2( Z
% 0.76/1.39 , Y ) ), ~( t2( Y, U ) ), ~( d( U ) ), equalish( u10r2( Y, Z ), T ),
% 0.76/1.39 equalish( T, u10r1( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 171, [ ~( f3( X ) ), ~( t( u11r4( X ), u10r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u10r2( Y, Z ) ) ), ~( t( u11r4( X ), T ) ), equalish( u10r1(
% 0.76/1.39 Y, Z ), T ), f2( Z ), ~( r2( Z, Y ) ), ~( t2( Y, U ) ), ~( d( U ) ),
% 0.76/1.39 equalish( u10r2( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 104, [ ~( f2( X ) ), ~( t( u10r4( X ), u9r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u10r4( X ), u9r3( Y, Z ) ) ), ~( t( u10r4( X ), T ) ), equalish( u9r1( Y
% 0.76/1.39 , Z ), T ), f1( Z ), ~( r1( Z, Y ) ), ~( t1( Y, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( u9r3( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 170, [ ~( f3( X ) ), ~( t( u11r4( X ), Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u10r1( Z, T ) ) ), ~( t( u11r4( X ), u10r2( Z, T ) ) ), equalish( Y,
% 0.76/1.39 u10r1( Z, T ) ), f2( T ), ~( r2( T, Z ) ), ~( t2( Z, U ) ), ~( d( U ) ),
% 0.76/1.39 equalish( Y, u10r2( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 169, [ ~( f3( X ) ), ~( t( u11r4( X ), u10r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), T ) ), ~( t( u11r4( X ), u10r3( Y, Z ) ) ), f2( Z ), ~( r2( Z
% 0.76/1.39 , Y ) ), ~( t2( Y, U ) ), ~( d( U ) ), equalish( u10r3( Y, Z ), T ),
% 0.76/1.39 equalish( T, u10r1( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 168, [ ~( f3( X ) ), ~( t( u11r4( X ), u10r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u10r3( Y, Z ) ) ), ~( t( u11r4( X ), T ) ), equalish( u10r1(
% 0.76/1.39 Y, Z ), T ), f2( Z ), ~( r2( Z, Y ) ), ~( t2( Y, U ) ), ~( d( U ) ),
% 0.76/1.39 equalish( u10r3( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 167, [ ~( f3( X ) ), ~( t( u11r4( X ), Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u10r1( Z, T ) ) ), ~( t( u11r4( X ), u10r3( Z, T ) ) ), equalish( Y,
% 0.76/1.39 u10r1( Z, T ) ), f2( T ), ~( r2( T, Z ) ), ~( t2( Z, U ) ), ~( d( U ) ),
% 0.76/1.39 equalish( Y, u10r3( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 103, [ ~( f2( X ) ), ~( t( u10r4( X ), Y ) ), ~( t( u10r4( X ),
% 0.76/1.39 u9r1( Z, T ) ) ), ~( t( u10r4( X ), u9r3( Z, T ) ) ), equalish( Y, u9r1(
% 0.76/1.39 Z, T ) ), f1( T ), ~( r1( T, Z ) ), ~( t1( Z, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( Y, u9r3( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 166, [ ~( f3( X ) ), ~( t( u11r4( X ), u10r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), T ) ), ~( t( u11r4( X ), u10r3( Y, Z ) ) ), f2( Z ), ~( r2( Z
% 0.76/1.39 , Y ) ), ~( t2( Y, U ) ), ~( d( U ) ), equalish( u10r3( Y, Z ), T ),
% 0.76/1.39 equalish( T, u10r2( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 220, [ ~( f3( X ) ), f2( Z ), ~( r2( Z, Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u10r1( Y, Z ) ) ), ~( d( T ) ), ~( t( u11r4( X ), u10r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u10r3( Y, Z ) ) ), ~( t2( Y, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 102, [ ~( f2( X ) ), ~( t( u10r4( X ), u9r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u10r4( X ), T ) ), ~( t( u10r4( X ), u9r3( Y, Z ) ) ), f1( Z ), ~( r1( Z
% 0.76/1.39 , Y ) ), ~( t1( Y, U ) ), ~( c( U ) ), equalish( u9r3( Y, Z ), T ),
% 0.76/1.39 equalish( T, u9r2( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 218, [ ~( f2( X ) ), f1( Z ), ~( r1( Z, Y ) ), ~( t( u10r4( X ),
% 0.76/1.39 u9r1( Y, Z ) ) ), ~( c( T ) ), ~( t( u10r4( X ), u9r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u10r4( X ), u9r3( Y, Z ) ) ), ~( t1( Y, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 101, [ ~( f2( X ) ), ~( t( u10r4( X ), u9r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u10r4( X ), u9r3( Y, Z ) ) ), ~( t( u10r4( X ), T ) ), equalish( u9r2( Y
% 0.76/1.39 , Z ), T ), f1( Z ), ~( r1( Z, Y ) ), ~( t1( Y, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( u9r3( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 165, [ ~( f3( X ) ), ~( t( u11r4( X ), u10r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u10r3( Y, Z ) ) ), ~( t( u11r4( X ), T ) ), equalish( u10r2(
% 0.76/1.39 Y, Z ), T ), f2( Z ), ~( r2( Z, Y ) ), ~( t2( Y, U ) ), ~( d( U ) ),
% 0.76/1.39 equalish( u10r3( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 164, [ ~( f3( X ) ), ~( t( u11r4( X ), Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u10r2( Z, T ) ) ), ~( t( u11r4( X ), u10r3( Z, T ) ) ), equalish( Y,
% 0.76/1.39 u10r2( Z, T ) ), f2( T ), ~( r2( T, Z ) ), ~( t2( Z, U ) ), ~( d( U ) ),
% 0.76/1.39 equalish( Y, u10r3( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 163, [ ~( f3( X ) ), ~( t( u11r4( X ), u11r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), T ) ), ~( t( u11r4( X ), u11r3( Y, Z ) ) ), f3( Z ), ~( r3( Z
% 0.76/1.39 , Y ) ), ~( t3( Y, U ) ), ~( e( U ) ), equalish( u11r3( Y, Z ), T ),
% 0.76/1.39 equalish( T, u11r2( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 162, [ ~( f3( X ) ), ~( t( u11r4( X ), u11r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u11r3( Y, Z ) ) ), ~( t( u11r4( X ), T ) ), equalish( u11r2(
% 0.76/1.39 Y, Z ), T ), f3( Z ), ~( r3( Z, Y ) ), ~( t3( Y, U ) ), ~( e( U ) ),
% 0.76/1.39 equalish( u11r3( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 100, [ ~( f2( X ) ), ~( t( u10r4( X ), Y ) ), ~( t( u10r4( X ),
% 0.76/1.39 u9r2( Z, T ) ) ), ~( t( u10r4( X ), u9r3( Z, T ) ) ), equalish( Y, u9r2(
% 0.76/1.39 Z, T ) ), f1( T ), ~( r1( T, Z ) ), ~( t1( Z, U ) ), ~( c( U ) ),
% 0.76/1.39 equalish( Y, u9r3( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 161, [ ~( f3( X ) ), ~( t( u11r4( X ), Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u11r2( Z, T ) ) ), ~( t( u11r4( X ), u11r3( Z, T ) ) ), equalish( Y,
% 0.76/1.39 u11r2( Z, T ) ), f3( T ), ~( r3( T, Z ) ), ~( t3( Z, U ) ), ~( e( U ) ),
% 0.76/1.39 equalish( Y, u11r3( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 160, [ ~( f3( X ) ), ~( t( u11r4( X ), u11r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), T ) ), ~( t( u11r4( X ), u11r3( Y, Z ) ) ), f3( Z ), ~( r3( Z
% 0.76/1.39 , Y ) ), ~( t3( Y, U ) ), ~( e( U ) ), equalish( u11r3( Y, Z ), T ),
% 0.76/1.39 equalish( T, u11r1( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 159, [ ~( f3( X ) ), ~( t( u11r4( X ), u11r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u11r3( Y, Z ) ) ), ~( t( u11r4( X ), T ) ), equalish( u11r1(
% 0.76/1.39 Y, Z ), T ), f3( Z ), ~( r3( Z, Y ) ), ~( t3( Y, U ) ), ~( e( U ) ),
% 0.76/1.39 equalish( u11r3( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 158, [ ~( f3( X ) ), ~( t( u11r4( X ), Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u11r1( Z, T ) ) ), ~( t( u11r4( X ), u11r3( Z, T ) ) ), equalish( Y,
% 0.76/1.39 u11r1( Z, T ) ), f3( T ), ~( r3( T, Z ) ), ~( t3( Z, U ) ), ~( e( U ) ),
% 0.76/1.39 equalish( Y, u11r3( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 86, [ f1( X ), ~( r1( X, Y ) ), ~( c( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u9r3( Y, X ) ) ), ~( t( u9r4( T ), U ) ), ~( t( u9r4( T ),
% 0.76/1.39 u9r2( Y, X ) ) ), ~( t1( Y, Z ) ), equalish( u9r3( Y, X ), U ), equalish(
% 0.76/1.39 U, u9r2( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 157, [ ~( f3( X ) ), ~( t( u11r4( X ), u11r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), T ) ), ~( t( u11r4( X ), u11r2( Y, Z ) ) ), f3( Z ), ~( r3( Z
% 0.76/1.39 , Y ) ), ~( t3( Y, U ) ), ~( e( U ) ), equalish( u11r2( Y, Z ), T ),
% 0.76/1.39 equalish( T, u11r1( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 156, [ ~( f3( X ) ), ~( t( u11r4( X ), u11r1( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u11r2( Y, Z ) ) ), ~( t( u11r4( X ), T ) ), equalish( u11r1(
% 0.76/1.39 Y, Z ), T ), f3( Z ), ~( r3( Z, Y ) ), ~( t3( Y, U ) ), ~( e( U ) ),
% 0.76/1.39 equalish( u11r2( Y, Z ), T ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 85, [ f1( X ), ~( r1( X, Y ) ), ~( c( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u9r3( Y, X ) ) ), ~( t( u9r4( T ), u9r2( Y, X ) ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t1( Y, Z ) ), equalish( u9r2( Y, X ), U ), equalish(
% 0.76/1.39 u9r3( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 212, [ ~( f3( X ) ), f3( Y ), ~( r3( Y, u11r4( X ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 84, [ f1( X ), ~( r1( X, Y ) ), ~( c( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t( u9r4( T ), u9r3( Y, X ) ) ), ~( t( u9r4( T ),
% 0.76/1.39 u9r2( Y, X ) ) ), ~( t1( Y, Z ) ), equalish( U, u9r2( Y, X ) ), equalish(
% 0.76/1.39 U, u9r3( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 207, [ ~( f3( X ) ), f3( Z ), ~( r3( Z, Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u11r1( Y, Z ) ) ), ~( e( T ) ), ~( t( u11r4( X ), u11r2( Y, Z ) ) ), ~( t(
% 0.76/1.39 u11r4( X ), u11r3( Y, Z ) ) ), ~( t3( Y, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 155, [ ~( f3( X ) ), ~( t( u11r4( X ), Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u11r1( Z, T ) ) ), ~( t( u11r4( X ), u11r2( Z, T ) ) ), equalish( Y,
% 0.76/1.39 u11r1( Z, T ) ), f3( T ), ~( r3( T, Z ) ), ~( t3( Z, U ) ), ~( e( U ) ),
% 0.76/1.39 equalish( Y, u11r2( Z, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 82, [ f1( X ), ~( r1( X, Y ) ), ~( c( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u9r3( Y, X ) ) ), ~( t( u9r4( T ), U ) ), ~( t( u9r4( T ),
% 0.76/1.39 u9r1( Y, X ) ) ), ~( t1( Y, Z ) ), equalish( u9r3( Y, X ), U ), equalish(
% 0.76/1.39 U, u9r1( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 203, [ f1( X ), ~( f1( Y ) ), ~( r1( X, u9r4( Y ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 81, [ f1( X ), ~( r1( X, Y ) ), ~( c( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u9r3( Y, X ) ) ), ~( t( u9r4( T ), u9r1( Y, X ) ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t1( Y, Z ) ), equalish( u9r1( Y, X ), U ), equalish(
% 0.76/1.39 u9r3( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 198, [ f1( X ), ~( f1( Y ) ), ~( c( Z ) ), ~( r1( X, T ) ), ~( t(
% 0.76/1.39 u9r4( Y ), u9r1( T, X ) ) ), ~( t( u9r4( Y ), u9r2( T, X ) ) ), ~( t(
% 0.76/1.39 u9r4( Y ), u9r3( T, X ) ) ), ~( t1( T, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 80, [ f1( X ), ~( r1( X, Y ) ), ~( c( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t( u9r4( T ), u9r3( Y, X ) ) ), ~( t( u9r4( T ),
% 0.76/1.39 u9r1( Y, X ) ) ), ~( t1( Y, Z ) ), equalish( U, u9r1( Y, X ) ), equalish(
% 0.76/1.39 U, u9r3( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 78, [ ~( f1( Y ) ), ~( r2least( X ) ), ~( t( u9r4( Y ), u14r1( X )
% 0.76/1.39 ) ), ~( t( u9r4( Y ), Z ) ), ~( t( u9r4( Y ), u14r2( X ) ) ), equalish(
% 0.76/1.39 u14r2( X ), Z ), equalish( Z, u14r1( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 108, [ ~( f2( X ) ), ~( t( u10r4( X ), u14r1( Y ) ) ), ~( t( u10r4(
% 0.76/1.39 X ), Z ) ), ~( t( u10r4( X ), u14r2( Y ) ) ), ~( r2least( Y ) ), equalish(
% 0.76/1.39 Z, u14r1( Y ) ), equalish( u14r2( Y ), Z ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 107, [ ~( f2( X ) ), ~( t( u10r4( X ), u14r1( Y ) ) ), ~( t( u10r4(
% 0.76/1.39 X ), u14r2( Y ) ) ), ~( t( u10r4( X ), Z ) ), equalish( u14r1( Y ), Z ),
% 0.76/1.39 ~( r2least( Y ) ), equalish( u14r2( Y ), Z ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 106, [ ~( f2( X ) ), ~( t( u10r4( X ), Y ) ), ~( t( u10r4( X ),
% 0.76/1.39 u14r1( Z ) ) ), ~( t( u10r4( X ), u14r2( Z ) ) ), equalish( Y, u14r1( Z )
% 0.76/1.39 ), ~( r2least( Z ) ), equalish( Y, u14r2( Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 77, [ ~( f1( Y ) ), ~( r2least( X ) ), ~( t( u9r4( Y ), u14r1( X )
% 0.76/1.39 ) ), ~( t( u9r4( Y ), u14r2( X ) ) ), ~( t( u9r4( Y ), Z ) ), equalish(
% 0.76/1.39 u14r1( X ), Z ), equalish( u14r2( X ), Z ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 181, [ ~( f3( X ) ), ~( t( u11r4( X ), u14r1( Y ) ) ), ~( t( u11r4(
% 0.76/1.39 X ), Z ) ), ~( t( u11r4( X ), u14r2( Y ) ) ), ~( r2least( Y ) ), equalish(
% 0.76/1.39 Z, u14r1( Y ) ), equalish( u14r2( Y ), Z ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 180, [ ~( f3( X ) ), ~( t( u11r4( X ), u14r1( Y ) ) ), ~( t( u11r4(
% 0.76/1.39 X ), u14r2( Y ) ) ), ~( t( u11r4( X ), Z ) ), equalish( u14r1( Y ), Z ),
% 0.76/1.39 ~( r2least( Y ) ), equalish( u14r2( Y ), Z ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 179, [ ~( f3( X ) ), ~( t( u11r4( X ), Y ) ), ~( t( u11r4( X ),
% 0.76/1.39 u14r1( Z ) ) ), ~( t( u11r4( X ), u14r2( Z ) ) ), equalish( Y, u14r1( Z )
% 0.76/1.39 ), ~( r2least( Z ) ), equalish( Y, u14r2( Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 76, [ ~( f1( Y ) ), ~( r2least( X ) ), ~( t( u9r4( Y ), Z ) ), ~( t(
% 0.76/1.39 u9r4( Y ), u14r1( X ) ) ), ~( t( u9r4( Y ), u14r2( X ) ) ), equalish( Z,
% 0.76/1.39 u14r1( X ) ), equalish( Z, u14r2( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 75, [ f1( X ), ~( r1( X, Y ) ), ~( c( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u9r2( Y, X ) ) ), ~( t( u9r4( T ), U ) ), ~( t( u9r4( T ),
% 0.76/1.39 u9r1( Y, X ) ) ), ~( t1( Y, Z ) ), equalish( u9r2( Y, X ), U ), equalish(
% 0.76/1.39 U, u9r1( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 74, [ f1( X ), ~( r1( X, Y ) ), ~( c( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), u9r2( Y, X ) ) ), ~( t( u9r4( T ), u9r1( Y, X ) ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t1( Y, Z ) ), equalish( u9r1( Y, X ), U ), equalish(
% 0.76/1.39 u9r2( Y, X ), U ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 90, [ r2least( X ), ~( r( X, u9r1( Y, Z ) ) ), f1( Z ), ~( r( X,
% 0.76/1.39 u9r2( Y, Z ) ) ), ~( r1( Z, Y ) ), ~( c( T ) ), ~( t1( Y, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 88, [ r2least( X ), ~( r( X, u9r1( Y, Z ) ) ), f1( Z ), ~( r( X,
% 0.76/1.39 u9r3( Y, Z ) ) ), ~( r1( Z, Y ) ), ~( c( T ) ), ~( t1( Y, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 87, [ r2least( X ), ~( r( X, u9r2( Y, Z ) ) ), f1( Z ), ~( r( X,
% 0.76/1.39 u9r3( Y, Z ) ) ), ~( r1( Z, Y ) ), ~( c( T ) ), ~( t1( Y, T ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 115, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), r2least( T ), ~( r( T
% 0.76/1.39 , u10r2( Y, X ) ) ), ~( r( T, u10r1( Y, X ) ) ), ~( t2( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 73, [ f1( X ), ~( r1( X, Y ) ), ~( c( Z ) ), ~( f1( T ) ), ~( t(
% 0.76/1.39 u9r4( T ), U ) ), ~( t( u9r4( T ), u9r2( Y, X ) ) ), ~( t( u9r4( T ),
% 0.76/1.39 u9r1( Y, X ) ) ), ~( t1( Y, Z ) ), equalish( U, u9r1( Y, X ) ), equalish(
% 0.76/1.39 U, u9r2( Y, X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 122, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), r2least( T ), ~( r( T
% 0.76/1.39 , u10r3( Y, X ) ) ), ~( r( T, u10r1( Y, X ) ) ), ~( t2( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 129, [ f2( X ), ~( r2( X, Y ) ), ~( d( Z ) ), r2least( T ), ~( r( T
% 0.76/1.39 , u10r3( Y, X ) ) ), ~( r( T, u10r2( Y, X ) ) ), ~( t2( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 136, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), r2least( T ), ~( r( T
% 0.76/1.39 , u11r3( Y, X ) ) ), ~( r( T, u11r2( Y, X ) ) ), ~( t3( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 143, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), r2least( T ), ~( r( T
% 0.76/1.39 , u11r3( Y, X ) ) ), ~( r( T, u11r1( Y, X ) ) ), ~( t3( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 33, [ ~( f3( T ) ), ~( t( u11r4( T ), X ) ), ~( t( u11r4( T ), Y )
% 0.76/1.39 ), ~( t( u11r4( T ), Z ) ), equalish( Y, Z ), equalish( X, Y ), equalish(
% 0.76/1.39 X, Z ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 150, [ f3( X ), ~( r3( X, Y ) ), ~( e( Z ) ), r2least( T ), ~( r( T
% 0.76/1.39 , u11r2( Y, X ) ) ), ~( r( T, u11r1( Y, X ) ) ), ~( t3( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 35, [ f3( X ), ~( r3( X, Y ) ), ~( t3( Y, Z ) ), ~( e( Z ) ), ~(
% 0.76/1.39 equalish( u11r2( Y, X ), u11r1( Y, X ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 36, [ f3( X ), ~( r3( X, Y ) ), ~( t3( Y, Z ) ), ~( e( Z ) ), ~(
% 0.76/1.39 equalish( u11r3( Y, X ), u11r1( Y, X ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 37, [ f3( X ), ~( r3( X, Y ) ), ~( t3( Y, Z ) ), ~( e( Z ) ), ~(
% 0.76/1.39 equalish( u11r3( Y, X ), u11r2( Y, X ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 27, [ f2( X ), ~( r2( X, Y ) ), ~( t2( Y, Z ) ), ~( d( Z ) ), ~(
% 0.76/1.39 equalish( u10r3( Y, X ), u10r2( Y, X ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 26, [ f2( X ), ~( r2( X, Y ) ), ~( t2( Y, Z ) ), ~( d( Z ) ), ~(
% 0.76/1.39 equalish( u10r3( Y, X ), u10r1( Y, X ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 25, [ f2( X ), ~( r2( X, Y ) ), ~( t2( Y, Z ) ), ~( d( Z ) ), ~(
% 0.76/1.39 equalish( u10r2( Y, X ), u10r1( Y, X ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 23, [ ~( f2( T ) ), ~( t( u10r4( T ), X ) ), ~( t( u10r4( T ), Y )
% 0.76/1.39 ), ~( t( u10r4( T ), Z ) ), equalish( Y, Z ), equalish( X, Y ), equalish(
% 0.76/1.39 X, Z ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 20, [ f1( X ), ~( r1( X, Y ) ), t( Y, u9r3( Y, X ) ), ~( c( Z ) ),
% 0.76/1.39 ~( t1( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 28, [ f2( X ), ~( r2( X, Y ) ), t( Y, u10r1( Y, X ) ), ~( d( Z ) )
% 0.76/1.39 , ~( t2( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 29, [ f2( X ), ~( r2( X, Y ) ), t( Y, u10r2( Y, X ) ), ~( d( Z ) )
% 0.76/1.39 , ~( t2( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 30, [ f2( X ), ~( r2( X, Y ) ), t( Y, u10r3( Y, X ) ), ~( d( Z ) )
% 0.76/1.39 , ~( t2( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 19, [ f1( X ), ~( r1( X, Y ) ), t( Y, u9r2( Y, X ) ), ~( c( Z ) ),
% 0.76/1.39 ~( t1( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 38, [ f3( X ), ~( r3( X, Y ) ), t( Y, u11r1( Y, X ) ), ~( e( Z ) )
% 0.76/1.39 , ~( t3( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 39, [ f3( X ), ~( r3( X, Y ) ), t( Y, u11r2( Y, X ) ), ~( e( Z ) )
% 0.76/1.39 , ~( t3( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 40, [ f3( X ), ~( r3( X, Y ) ), t( Y, u11r3( Y, X ) ), ~( e( Z ) )
% 0.76/1.39 , ~( t3( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 89, [ r2least( X ), ~( r( X, u14r1( Y ) ) ), ~( r2least( Y ) ), ~(
% 0.76/1.39 r( X, u14r2( Y ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 18, [ f1( X ), ~( r1( X, Y ) ), t( Y, u9r1( Y, X ) ), ~( c( Z ) ),
% 0.76/1.39 ~( t1( Y, Z ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 50, [ r2least( X ), ~( r( X, Y ) ), ~( r( X, Z ) ), equalish( Y, Z
% 0.76/1.39 ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 52, [ ~( f1( X ) ), ~( t( u9r4( X ), Y ) ), equalish( Y, Y ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 54, [ ~( f2( X ) ), ~( t( u10r4( X ), Y ) ), equalish( Y, Y ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 56, [ ~( f3( X ) ), ~( t( u11r4( X ), Y ) ), equalish( Y, Y ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 17, [ f1( X ), ~( r1( X, Y ) ), ~( t1( Y, Z ) ), ~( c( Z ) ), ~(
% 0.76/1.39 equalish( u9r3( Y, X ), u9r2( Y, X ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 44, [ f( X ), ~( f1( X ) ), ~( f2( X ) ), ~( f3( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 57, [ r2least( X ), ~( r( X, Y ) ), equalish( Y, Y ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 83, [ ~( f2( X ) ), t( u10r4( X ), u10r5( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 22, [ ~( f2( X ) ), t2( u10r4( X ), u10r5( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 16, [ f1( X ), ~( r1( X, Y ) ), ~( t1( Y, Z ) ), ~( c( Z ) ), ~(
% 0.76/1.39 equalish( u9r3( Y, X ), u9r1( Y, X ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 79, [ ~( f3( X ) ), t( u11r4( X ), u11r5( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 32, [ ~( f3( X ) ), t3( u11r4( X ), u11r5( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 47, [ ~( r2least( X ) ), ~( equalish( u14r2( X ), u14r1( X ) ) ) ]
% 0.76/1.39 )
% 0.76/1.39 .
% 0.76/1.39 clause( 69, [ ~( f1( X ) ), t( u9r4( X ), u9r5( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 15, [ f1( X ), ~( r1( X, Y ) ), ~( t1( Y, Z ) ), ~( c( Z ) ), ~(
% 0.76/1.39 equalish( u9r2( Y, X ), u9r1( Y, X ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 72, [ ~( f1( X ) ), r( X, u9r4( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 14, [ ~( f1( X ) ), r1( X, u9r4( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 71, [ ~( f2( X ) ), r( X, u10r4( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 24, [ ~( f2( X ) ), r2( X, u10r4( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 13, [ ~( f1( T ) ), ~( t( u9r4( T ), X ) ), ~( t( u9r4( T ), Y ) )
% 0.76/1.39 , ~( t( u9r4( T ), Z ) ), equalish( Y, Z ), equalish( X, Y ), equalish( X
% 0.76/1.39 , Z ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 70, [ ~( f3( X ) ), r( X, u11r4( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 34, [ ~( f3( X ) ), r3( X, u11r4( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 48, [ ~( r2least( X ) ), r( X, u14r1( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 49, [ ~( r2least( X ) ), r( X, u14r2( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 12, [ ~( f1( X ) ), t1( u9r4( X ), u9r5( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 7, [ t( X, Y ), ~( t3( X, Y ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 68, [ ~( d( u9r5( exists ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 67, [ ~( d( u9r5( X ) ) ), ~( f( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 64, [ ~( d( u9r5( X ) ) ), ~( f1( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 6, [ t( X, Y ), ~( t2( X, Y ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 66, [ ~( e( u9r5( exists ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 65, [ ~( e( u9r5( X ) ) ), ~( f( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 63, [ ~( e( u9r5( X ) ) ), ~( f1( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 11, [ ~( f1( X ) ), c( u9r5( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 5, [ t( X, Y ), ~( t1( X, Y ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 62, [ d( u10r5( exists ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 61, [ d( u10r5( X ) ), ~( f( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 21, [ d( u10r5( X ) ), ~( f2( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 60, [ ~( d( u11r5( exists ) ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 4, [ r( X, Y ), ~( r3( X, Y ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 59, [ e( u11r5( exists ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 58, [ e( u11r5( X ) ), ~( f( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 31, [ e( u11r5( X ) ), ~( f3( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 8, [ ~( e( X ) ), ~( c( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 3, [ r( X, Y ), ~( r2( X, Y ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 9, [ ~( d( X ) ), ~( c( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 10, [ ~( d( X ) ), ~( e( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 41, [ ~( f( X ) ), f3( X ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 42, [ ~( f( X ) ), f2( X ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 2, [ r( X, Y ), ~( r1( X, Y ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 43, [ ~( f( X ) ), f1( X ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 45, [ ~( g( X ) ), r2least( X ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 46, [ g( X ), ~( r2least( X ) ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 0, [ f( exists ) ] )
% 0.76/1.39 .
% 0.76/1.39 clause( 1, [ ~( g( exists ) ) ] )
% 0.76/1.39 .
% 0.76/1.39
% 0.76/1.39
% 0.76/1.39 % SZS output end Saturation
% 0.76/1.39 end of saturation!
% 0.76/1.39
% 0.76/1.39 Memory use:
% 0.76/1.39
% 0.76/1.39 space for terms: 9267
% 0.76/1.39 space for clauses: 11689
% 0.76/1.39
% 0.76/1.39
% 0.76/1.39 clauses generated: 630
% 0.76/1.39 clauses kept: 247
% 0.76/1.39 clauses selected: 222
% 0.76/1.39 clauses deleted: 63
% 0.76/1.39 clauses inuse deleted: 38
% 0.76/1.39
% 0.76/1.39 subsentry: 2985
% 0.76/1.39 literals s-matched: 2768
% 0.76/1.39 literals matched: 1563
% 0.76/1.39 full subsumption: 1279
% 0.76/1.39
% 0.76/1.39 checksum: -530429056
% 0.76/1.39
% 0.76/1.39
% 0.76/1.39 Bliksem ended
%------------------------------------------------------------------------------