%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN622-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n023.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 : Thu Jul 21 02:53:27 EDT 2022
% Result : Unsatisfiable 6.80s 7.19s
% Output : Refutation 6.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYN622-1 : TPTP v8.1.0. Released v2.5.0.
% 0.00/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Mon Jul 11 13:23:54 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.64/2.06 *** allocated 10000 integers for termspace/termends
% 1.64/2.06 *** allocated 10000 integers for clauses
% 1.64/2.06 *** allocated 10000 integers for justifications
% 1.64/2.06 Bliksem 1.12
% 1.64/2.06
% 1.64/2.06
% 1.64/2.06 Automatic Strategy Selection
% 1.64/2.06
% 1.64/2.06 Clauses:
% 1.64/2.06 [
% 1.64/2.06 [ p11( X, X ) ],
% 1.64/2.06 [ p9( X, X ) ],
% 1.64/2.06 [ p8( X, X ) ],
% 1.64/2.06 [ p3( X, X ) ],
% 1.64/2.06 [ p2( X, X ) ],
% 1.64/2.06 [ p3( f4( c23 ), c24 ) ],
% 1.64/2.06 [ p19( f5( f6( f7( c25 ) ) ), c24 ) ],
% 1.64/2.06 [ p8( f16( X, f17( Y, X ) ), Y ) ],
% 1.64/2.06 [ p21( X ), ~( p21( Y ) ), ~( p11( Y, X ) ) ],
% 1.64/2.06 [ p11( f13( X ), f13( Y ) ), ~( p2( X, Y ) ) ],
% 1.64/2.06 [ p9( f15( X ), f15( Y ) ), ~( p3( X, Y ) ) ],
% 1.64/2.06 [ p9( f10( X ), f10( Y ) ), ~( p8( X, Y ) ) ],
% 1.64/2.06 [ p8( f14( X ), f14( Y ) ), ~( p9( X, Y ) ) ],
% 1.64/2.06 [ p3( f7( X ), f7( Y ) ), ~( p3( X, Y ) ) ],
% 1.64/2.06 [ p3( f6( X ), f6( Y ) ), ~( p3( X, Y ) ) ],
% 1.64/2.06 [ p3( f5( X ), f5( Y ) ), ~( p3( X, Y ) ) ],
% 1.64/2.06 [ p3( f4( X ), f4( Y ) ), ~( p2( X, Y ) ) ],
% 1.64/2.06 [ ~( p8( f12( f13( c26 ), c27 ), f14( f15( f5( c25 ) ) ) ) ) ],
% 1.64/2.06 [ p11( X, Y ), ~( p11( Z, X ) ), ~( p11( Z, Y ) ) ],
% 1.64/2.06 [ p9( X, Y ), ~( p9( Z, X ) ), ~( p9( Z, Y ) ) ],
% 1.64/2.06 [ p8( X, Y ), ~( p8( Z, X ) ), ~( p8( Z, Y ) ) ],
% 1.64/2.06 [ p3( X, Y ), ~( p3( Z, X ) ), ~( p3( Z, Y ) ) ],
% 1.64/2.06 [ p2( X, Y ), ~( p2( Z, X ) ), ~( p2( Z, Y ) ) ],
% 1.64/2.06 [ p8( f12( f13( c23 ), X ), f12( f13( c26 ), f16( c27, X ) ) ) ],
% 1.64/2.06 [ p20( f10( f12( f13( c26 ), c27 ) ), f10( f12( f13( c26 ), X ) ) ) ]
% 1.64/2.06 ,
% 1.64/2.06 [ ~( p8( f12( f13( c23 ), f17( c28, c27 ) ), f12( f13( c26 ), c28 ) ) )
% 1.64/2.06 ],
% 1.64/2.06 [ p19( X, Y ), ~( p3( Z, X ) ), ~( p3( T, Y ) ), ~( p19( Z, T ) ) ],
% 1.64/2.06 [ p22( X, Y ), ~( p3( Z, X ) ), ~( p3( T, Y ) ), ~( p22( Z, T ) ) ],
% 1.64/2.06 [ p20( X, Y ), ~( p9( Z, X ) ), ~( p9( T, Y ) ), ~( p20( Z, T ) ) ],
% 1.64/2.06 [ p8( f18( X, Y ), f18( Z, T ) ), ~( p2( Y, T ) ), ~( p3( X, Z ) ) ]
% 1.64/2.06 ,
% 1.64/2.06 [ p8( f12( X, Y ), f12( Z, T ) ), ~( p11( X, Z ) ), ~( p8( Y, T ) ) ]
% 1.64/2.06 ,
% 1.64/2.06 [ p8( f16( X, Y ), f16( Z, T ) ), ~( p8( X, Z ) ), ~( p8( Y, T ) ) ]
% 1.64/2.06 ,
% 1.64/2.06 [ p8( f17( X, Y ), f17( Z, T ) ), ~( p8( X, Z ) ), ~( p8( Y, T ) ) ]
% 1.64/2.06 ,
% 1.64/2.06 [ p21( f13( X ) ), p8( f12( f13( X ), f18( Y, X ) ), f14( f15( f5( c25 )
% 1.64/2.06 ) ) ), ~( p22( Y, c24 ) ), ~( p3( f4( X ), Y ) ) ]
% 1.64/2.06 ] .
% 1.64/2.06
% 1.64/2.06
% 1.64/2.06 percentage equality = 0.000000, percentage horn = 0.970588
% 1.64/2.06 This is a near-Horn, non-equality problem
% 1.64/2.06
% 1.64/2.06
% 1.64/2.06 Options Used:
% 1.64/2.06
% 1.64/2.06 useres = 1
% 1.64/2.06 useparamod = 0
% 1.64/2.06 useeqrefl = 0
% 1.64/2.06 useeqfact = 0
% 1.64/2.06 usefactor = 1
% 1.64/2.06 usesimpsplitting = 0
% 1.64/2.06 usesimpdemod = 0
% 1.64/2.06 usesimpres = 4
% 1.64/2.06
% 1.64/2.06 resimpinuse = 1000
% 1.64/2.06 resimpclauses = 20000
% 1.64/2.06 substype = standard
% 1.64/2.06 backwardsubs = 1
% 1.64/2.06 selectoldest = 5
% 1.64/2.06
% 1.64/2.06 litorderings [0] = split
% 1.64/2.06 litorderings [1] = liftord
% 1.64/2.06
% 1.64/2.06 termordering = none
% 1.64/2.06
% 1.64/2.06 litapriori = 1
% 1.64/2.06 termapriori = 0
% 1.64/2.06 litaposteriori = 0
% 1.64/2.06 termaposteriori = 0
% 1.64/2.06 demodaposteriori = 0
% 1.64/2.06 ordereqreflfact = 0
% 1.64/2.06
% 1.64/2.06 litselect = negative
% 1.64/2.06
% 1.64/2.06 maxweight = 30000
% 1.64/2.06 maxdepth = 30000
% 1.64/2.06 maxlength = 115
% 1.64/2.06 maxnrvars = 195
% 1.64/2.06 excuselevel = 0
% 1.64/2.06 increasemaxweight = 0
% 1.64/2.06
% 1.64/2.06 maxselected = 10000000
% 1.64/2.06 maxnrclauses = 10000000
% 1.64/2.06
% 1.64/2.06 showgenerated = 0
% 1.64/2.06 showkept = 0
% 1.64/2.06 showselected = 0
% 1.64/2.06 showdeleted = 0
% 1.64/2.06 showresimp = 1
% 1.64/2.06 showstatus = 2000
% 1.64/2.06
% 1.64/2.06 prologoutput = 1
% 1.64/2.06 nrgoals = 5000000
% 1.64/2.06 totalproof = 1
% 1.64/2.06
% 1.64/2.06 Symbols occurring in the translation:
% 1.64/2.06
% 1.64/2.06 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.64/2.06 . [1, 2] (w:1, o:96, a:1, s:1, b:0),
% 1.64/2.06 ! [4, 1] (w:1, o:82, a:1, s:1, b:0),
% 1.64/2.06 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.64/2.06 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.64/2.06 p11 [40, 2] (w:1, o:121, a:1, s:1, b:0),
% 1.64/2.06 p9 [42, 2] (w:1, o:123, a:1, s:1, b:0),
% 1.64/2.06 p8 [44, 2] (w:1, o:122, a:1, s:1, b:0),
% 1.64/2.06 p3 [46, 2] (w:1, o:128, a:1, s:1, b:0),
% 1.64/2.06 p2 [48, 2] (w:1, o:125, a:1, s:1, b:0),
% 1.64/2.06 c23 [49, 0] (w:1, o:67, a:1, s:1, b:0),
% 1.64/2.06 f4 [50, 1] (w:1, o:87, a:1, s:1, b:0),
% 1.64/2.06 c24 [51, 0] (w:1, o:68, a:1, s:1, b:0),
% 1.64/2.06 c25 [52, 0] (w:1, o:69, a:1, s:1, b:0),
% 1.64/2.06 f7 [53, 1] (w:1, o:90, a:1, s:1, b:0),
% 1.64/2.06 f6 [54, 1] (w:1, o:89, a:1, s:1, b:0),
% 1.64/2.06 f5 [55, 1] (w:1, o:88, a:1, s:1, b:0),
% 1.64/2.06 p19 [56, 2] (w:1, o:124, a:1, s:1, b:0),
% 1.64/2.06 f17 [59, 2] (w:1, o:130, a:1, s:1, b:0),
% 1.64/2.06 f16 [60, 2] (w:1, o:129, a:1, s:1, b:0),
% 3.53/3.96 p21 [62, 1] (w:1, o:91, a:1, s:1, b:0),
% 3.53/3.96 f13 [65, 1] (w:1, o:92, a:1, s:1, b:0),
% 3.53/3.96 f15 [68, 1] (w:1, o:94, a:1, s:1, b:0),
% 3.53/3.96 f10 [71, 1] (w:1, o:95, a:1, s:1, b:0),
% 3.53/3.96 f14 [74, 1] (w:1, o:93, a:1, s:1, b:0),
% 3.53/3.96 c26 [84, 0] (w:1, o:76, a:1, s:1, b:0),
% 3.53/3.96 c27 [85, 0] (w:1, o:77, a:1, s:1, b:0),
% 3.53/3.96 f12 [86, 2] (w:1, o:131, a:1, s:1, b:0),
% 3.53/3.96 p20 [99, 2] (w:1, o:126, a:1, s:1, b:0),
% 3.53/3.96 c28 [100, 0] (w:1, o:79, a:1, s:1, b:0),
% 3.53/3.96 p22 [107, 2] (w:1, o:127, a:1, s:1, b:0),
% 3.53/3.96 f18 [116, 2] (w:1, o:132, a:1, s:1, b:0).
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Starting Search:
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 2288
% 3.53/3.96 Kept: 2009
% 3.53/3.96 Inuse: 353
% 3.53/3.96 Deleted: 0
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 4363
% 3.53/3.96 Kept: 4015
% 3.53/3.96 Inuse: 431
% 3.53/3.96 Deleted: 0
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 6427
% 3.53/3.96 Kept: 6038
% 3.53/3.96 Inuse: 490
% 3.53/3.96 Deleted: 0
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 8508
% 3.53/3.96 Kept: 8084
% 3.53/3.96 Inuse: 536
% 3.53/3.96 Deleted: 0
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 10568
% 3.53/3.96 Kept: 10114
% 3.53/3.96 Inuse: 580
% 3.53/3.96 Deleted: 0
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 12595
% 3.53/3.96 Kept: 12114
% 3.53/3.96 Inuse: 617
% 3.53/3.96 Deleted: 0
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 14708
% 3.53/3.96 Kept: 14182
% 3.53/3.96 Inuse: 661
% 3.53/3.96 Deleted: 0
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 16745
% 3.53/3.96 Kept: 16185
% 3.53/3.96 Inuse: 701
% 3.53/3.96 Deleted: 0
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 18824
% 3.53/3.96 Kept: 18230
% 3.53/3.96 Inuse: 737
% 3.53/3.96 Deleted: 0
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying clauses:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 21035
% 3.53/3.96 Kept: 20413
% 3.53/3.96 Inuse: 771
% 3.53/3.96 Deleted: 2
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 23158
% 3.53/3.96 Kept: 22485
% 3.53/3.96 Inuse: 996
% 3.53/3.96 Deleted: 2
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 25266
% 3.53/3.96 Kept: 24569
% 3.53/3.96 Inuse: 1091
% 3.53/3.96 Deleted: 2
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 27356
% 3.53/3.96 Kept: 26587
% 3.53/3.96 Inuse: 1146
% 3.53/3.96 Deleted: 2
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 29515
% 3.53/3.96 Kept: 28703
% 3.53/3.96 Inuse: 1206
% 3.53/3.96 Deleted: 2
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 31605
% 3.53/3.96 Kept: 30774
% 3.53/3.96 Inuse: 1306
% 3.53/3.96 Deleted: 2
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 33781
% 3.53/3.96 Kept: 32781
% 3.53/3.96 Inuse: 1542
% 3.53/3.96 Deleted: 2
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 35852
% 3.53/3.96 Kept: 34797
% 3.53/3.96 Inuse: 1604
% 3.53/3.96 Deleted: 2
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 37915
% 3.53/3.96 Kept: 36802
% 3.53/3.96 Inuse: 1670
% 3.53/3.96 Deleted: 2
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 39979
% 3.53/3.96 Kept: 38840
% 3.53/3.96 Inuse: 1703
% 3.53/3.96 Deleted: 2
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying clauses:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 42106
% 3.53/3.96 Kept: 40942
% 3.53/3.96 Inuse: 1734
% 3.53/3.96 Deleted: 8
% 3.53/3.96 Deletedinuse: 0
% 3.53/3.96
% 3.53/3.96 Resimplifying inuse:
% 3.53/3.96 Done
% 3.53/3.96
% 3.53/3.96
% 3.53/3.96 Intermediate Status:
% 3.53/3.96 Generated: 44167
% 3.53/3.96 Kept: 42977
% 3.53/3.96 Inuse: 1767
% 3.53/3.96 Deleted: 8
% 3.53/3.96 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 46195
% 6.80/7.19 Kept: 44983
% 6.80/7.19 Inuse: 1795
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 48325
% 6.80/7.19 Kept: 47091
% 6.80/7.19 Inuse: 1823
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 50383
% 6.80/7.19 Kept: 49125
% 6.80/7.19 Inuse: 1853
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 52488
% 6.80/7.19 Kept: 51204
% 6.80/7.19 Inuse: 1885
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 54508
% 6.80/7.19 Kept: 53206
% 6.80/7.19 Inuse: 1909
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 56573
% 6.80/7.19 Kept: 55253
% 6.80/7.19 Inuse: 1933
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 58677
% 6.80/7.19 Kept: 57339
% 6.80/7.19 Inuse: 1957
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 60796
% 6.80/7.19 Kept: 59441
% 6.80/7.19 Inuse: 1979
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying clauses:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 63096
% 6.80/7.19 Kept: 61716
% 6.80/7.19 Inuse: 2006
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 65209
% 6.80/7.19 Kept: 63812
% 6.80/7.19 Inuse: 2026
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 67482
% 6.80/7.19 Kept: 66063
% 6.80/7.19 Inuse: 2051
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 69569
% 6.80/7.19 Kept: 68126
% 6.80/7.19 Inuse: 2077
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 71710
% 6.80/7.19 Kept: 70246
% 6.80/7.19 Inuse: 2101
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 73770
% 6.80/7.19 Kept: 72287
% 6.80/7.19 Inuse: 2124
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 76214
% 6.80/7.19 Kept: 74712
% 6.80/7.19 Inuse: 2146
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 78560
% 6.80/7.19 Kept: 77037
% 6.80/7.19 Inuse: 2171
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 80612
% 6.80/7.19 Kept: 79070
% 6.80/7.19 Inuse: 2194
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying clauses:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 82731
% 6.80/7.19 Kept: 81176
% 6.80/7.19 Inuse: 2210
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 84955
% 6.80/7.19 Kept: 83382
% 6.80/7.19 Inuse: 2231
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 87058
% 6.80/7.19 Kept: 85467
% 6.80/7.19 Inuse: 2253
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 89164
% 6.80/7.19 Kept: 87560
% 6.80/7.19 Inuse: 2269
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 91434
% 6.80/7.19 Kept: 89815
% 6.80/7.19 Inuse: 2286
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 93515
% 6.80/7.19 Kept: 91877
% 6.80/7.19 Inuse: 2310
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 95541
% 6.80/7.19 Kept: 93891
% 6.80/7.19 Inuse: 2324
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 97658
% 6.80/7.19 Kept: 95988
% 6.80/7.19 Inuse: 2348
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 99733
% 6.80/7.19 Kept: 98052
% 6.80/7.19 Inuse: 2362
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 101779
% 6.80/7.19 Kept: 100078
% 6.80/7.19 Inuse: 2385
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying clauses:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 103875
% 6.80/7.19 Kept: 102164
% 6.80/7.19 Inuse: 2398
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 106367
% 6.80/7.19 Kept: 104640
% 6.80/7.19 Inuse: 2416
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 108435
% 6.80/7.19 Kept: 106690
% 6.80/7.19 Inuse: 2439
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 110608
% 6.80/7.19 Kept: 108852
% 6.80/7.19 Inuse: 2451
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 112680
% 6.80/7.19 Kept: 110907
% 6.80/7.19 Inuse: 2473
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 114835
% 6.80/7.19 Kept: 113049
% 6.80/7.19 Inuse: 2488
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 117151
% 6.80/7.19 Kept: 115345
% 6.80/7.19 Inuse: 2506
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 119592
% 6.80/7.19 Kept: 117768
% 6.80/7.19 Inuse: 2526
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 121725
% 6.80/7.19 Kept: 119889
% 6.80/7.19 Inuse: 2541
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying clauses:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 124060
% 6.80/7.19 Kept: 122207
% 6.80/7.19 Inuse: 2561
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 126114
% 6.80/7.19 Kept: 124247
% 6.80/7.19 Inuse: 2579
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 128351
% 6.80/7.19 Kept: 126473
% 6.80/7.19 Inuse: 2591
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 130869
% 6.80/7.19 Kept: 128974
% 6.80/7.19 Inuse: 2611
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 133001
% 6.80/7.19 Kept: 131091
% 6.80/7.19 Inuse: 2628
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 135089
% 6.80/7.19 Kept: 133162
% 6.80/7.19 Inuse: 2643
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Intermediate Status:
% 6.80/7.19 Generated: 137186
% 6.80/7.19 Kept: 135242
% 6.80/7.19 Inuse: 2658
% 6.80/7.19 Deleted: 8
% 6.80/7.19 Deletedinuse: 0
% 6.80/7.19
% 6.80/7.19 Resimplifying inuse:
% 6.80/7.19 Done
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 Bliksems!, er is een bewijs:
% 6.80/7.19 % SZS status Unsatisfiable
% 6.80/7.19 % SZS output start Refutation
% 6.80/7.19
% 6.80/7.19 clause( 0, [ p11( X, X ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 2, [ p8( X, X ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 7, [ p8( f16( X, f17( Y, X ) ), Y ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 20, [ ~( p8( Z, X ) ), p8( X, Y ), ~( p8( Z, Y ) ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 23, [ p8( f12( f13( c23 ), X ), f12( f13( c26 ), f16( c27, X ) ) )
% 6.80/7.19 ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 25, [ ~( p8( f12( f13( c23 ), f17( c28, c27 ) ), f12( f13( c26 ),
% 6.80/7.19 c28 ) ) ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 30, [ p8( f12( X, Y ), f12( Z, T ) ), ~( p8( Y, T ) ), ~( p11( X, Z
% 6.80/7.19 ) ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 125, [ p8( Y, X ), ~( p8( X, Y ) ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 166, [ p8( f12( f13( c26 ), f16( c27, X ) ), f12( f13( c23 ), X ) )
% 6.80/7.19 ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 375, [ p8( f12( X, Y ), f12( X, Z ) ), ~( p8( Y, Z ) ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 1314, [ p8( f12( X, f16( Y, f17( Z, Y ) ) ), f12( X, Z ) ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 1331, [ p8( Y, f12( f13( c23 ), X ) ), ~( p8( f12( f13( c26 ), f16(
% 6.80/7.19 c27, X ) ), Y ) ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 135623, [ p8( f12( f13( c26 ), X ), f12( f13( c23 ), f17( X, c27 )
% 6.80/7.19 ) ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 135657, [ p8( f12( f13( c23 ), f17( X, c27 ) ), f12( f13( c26 ), X
% 6.80/7.19 ) ) ] )
% 6.80/7.19 .
% 6.80/7.19 clause( 135690, [] )
% 6.80/7.19 .
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 % SZS output end Refutation
% 6.80/7.19 found a proof!
% 6.80/7.19
% 6.80/7.19 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 6.80/7.19
% 6.80/7.19 initialclauses(
% 6.80/7.19 [ clause( 135692, [ p11( X, X ) ] )
% 6.80/7.19 , clause( 135693, [ p9( X, X ) ] )
% 6.80/7.19 , clause( 135694, [ p8( X, X ) ] )
% 6.80/7.19 , clause( 135695, [ p3( X, X ) ] )
% 6.80/7.19 , clause( 135696, [ p2( X, X ) ] )
% 6.80/7.19 , clause( 135697, [ p3( f4( c23 ), c24 ) ] )
% 6.80/7.19 , clause( 135698, [ p19( f5( f6( f7( c25 ) ) ), c24 ) ] )
% 6.80/7.19 , clause( 135699, [ p8( f16( X, f17( Y, X ) ), Y ) ] )
% 6.80/7.19 , clause( 135700, [ p21( X ), ~( p21( Y ) ), ~( p11( Y, X ) ) ] )
% 6.80/7.19 , clause( 135701, [ p11( f13( X ), f13( Y ) ), ~( p2( X, Y ) ) ] )
% 6.80/7.19 , clause( 135702, [ p9( f15( X ), f15( Y ) ), ~( p3( X, Y ) ) ] )
% 6.80/7.19 , clause( 135703, [ p9( f10( X ), f10( Y ) ), ~( p8( X, Y ) ) ] )
% 6.80/7.19 , clause( 135704, [ p8( f14( X ), f14( Y ) ), ~( p9( X, Y ) ) ] )
% 6.80/7.19 , clause( 135705, [ p3( f7( X ), f7( Y ) ), ~( p3( X, Y ) ) ] )
% 6.80/7.19 , clause( 135706, [ p3( f6( X ), f6( Y ) ), ~( p3( X, Y ) ) ] )
% 6.80/7.19 , clause( 135707, [ p3( f5( X ), f5( Y ) ), ~( p3( X, Y ) ) ] )
% 6.80/7.19 , clause( 135708, [ p3( f4( X ), f4( Y ) ), ~( p2( X, Y ) ) ] )
% 6.80/7.19 , clause( 135709, [ ~( p8( f12( f13( c26 ), c27 ), f14( f15( f5( c25 ) ) )
% 6.80/7.19 ) ) ] )
% 6.80/7.19 , clause( 135710, [ p11( X, Y ), ~( p11( Z, X ) ), ~( p11( Z, Y ) ) ] )
% 6.80/7.19 , clause( 135711, [ p9( X, Y ), ~( p9( Z, X ) ), ~( p9( Z, Y ) ) ] )
% 6.80/7.19 , clause( 135712, [ p8( X, Y ), ~( p8( Z, X ) ), ~( p8( Z, Y ) ) ] )
% 6.80/7.19 , clause( 135713, [ p3( X, Y ), ~( p3( Z, X ) ), ~( p3( Z, Y ) ) ] )
% 6.80/7.19 , clause( 135714, [ p2( X, Y ), ~( p2( Z, X ) ), ~( p2( Z, Y ) ) ] )
% 6.80/7.19 , clause( 135715, [ p8( f12( f13( c23 ), X ), f12( f13( c26 ), f16( c27, X
% 6.80/7.19 ) ) ) ] )
% 6.80/7.19 , clause( 135716, [ p20( f10( f12( f13( c26 ), c27 ) ), f10( f12( f13( c26
% 6.80/7.19 ), X ) ) ) ] )
% 6.80/7.19 , clause( 135717, [ ~( p8( f12( f13( c23 ), f17( c28, c27 ) ), f12( f13(
% 6.80/7.19 c26 ), c28 ) ) ) ] )
% 6.80/7.19 , clause( 135718, [ p19( X, Y ), ~( p3( Z, X ) ), ~( p3( T, Y ) ), ~( p19(
% 6.80/7.19 Z, T ) ) ] )
% 6.80/7.19 , clause( 135719, [ p22( X, Y ), ~( p3( Z, X ) ), ~( p3( T, Y ) ), ~( p22(
% 6.80/7.19 Z, T ) ) ] )
% 6.80/7.19 , clause( 135720, [ p20( X, Y ), ~( p9( Z, X ) ), ~( p9( T, Y ) ), ~( p20(
% 6.80/7.19 Z, T ) ) ] )
% 6.80/7.19 , clause( 135721, [ p8( f18( X, Y ), f18( Z, T ) ), ~( p2( Y, T ) ), ~( p3(
% 6.80/7.19 X, Z ) ) ] )
% 6.80/7.19 , clause( 135722, [ p8( f12( X, Y ), f12( Z, T ) ), ~( p11( X, Z ) ), ~( p8(
% 6.80/7.19 Y, T ) ) ] )
% 6.80/7.19 , clause( 135723, [ p8( f16( X, Y ), f16( Z, T ) ), ~( p8( X, Z ) ), ~( p8(
% 6.80/7.19 Y, T ) ) ] )
% 6.80/7.19 , clause( 135724, [ p8( f17( X, Y ), f17( Z, T ) ), ~( p8( X, Z ) ), ~( p8(
% 6.80/7.19 Y, T ) ) ] )
% 6.80/7.19 , clause( 135725, [ p21( f13( X ) ), p8( f12( f13( X ), f18( Y, X ) ), f14(
% 6.80/7.19 f15( f5( c25 ) ) ) ), ~( p22( Y, c24 ) ), ~( p3( f4( X ), Y ) ) ] )
% 6.80/7.19 ] ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 0, [ p11( X, X ) ] )
% 6.80/7.19 , clause( 135692, [ p11( X, X ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 2, [ p8( X, X ) ] )
% 6.80/7.19 , clause( 135694, [ p8( X, X ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 7, [ p8( f16( X, f17( Y, X ) ), Y ) ] )
% 6.80/7.19 , clause( 135699, [ p8( f16( X, f17( Y, X ) ), Y ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.80/7.19 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 20, [ ~( p8( Z, X ) ), p8( X, Y ), ~( p8( Z, Y ) ) ] )
% 6.80/7.19 , clause( 135712, [ p8( X, Y ), ~( p8( Z, X ) ), ~( p8( Z, Y ) ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 6.80/7.19 permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 ), ==>( 2, 2 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 23, [ p8( f12( f13( c23 ), X ), f12( f13( c26 ), f16( c27, X ) ) )
% 6.80/7.19 ] )
% 6.80/7.19 , clause( 135715, [ p8( f12( f13( c23 ), X ), f12( f13( c26 ), f16( c27, X
% 6.80/7.19 ) ) ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 25, [ ~( p8( f12( f13( c23 ), f17( c28, c27 ) ), f12( f13( c26 ),
% 6.80/7.19 c28 ) ) ) ] )
% 6.80/7.19 , clause( 135717, [ ~( p8( f12( f13( c23 ), f17( c28, c27 ) ), f12( f13(
% 6.80/7.19 c26 ), c28 ) ) ) ] )
% 6.80/7.19 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 30, [ p8( f12( X, Y ), f12( Z, T ) ), ~( p8( Y, T ) ), ~( p11( X, Z
% 6.80/7.19 ) ) ] )
% 6.80/7.19 , clause( 135722, [ p8( f12( X, Y ), f12( Z, T ) ), ~( p11( X, Z ) ), ~( p8(
% 6.80/7.19 Y, T ) ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 6.80/7.19 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 2 ), ==>( 2, 1 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 resolution(
% 6.80/7.19 clause( 135748, [ ~( p8( X, Y ) ), p8( Y, X ) ] )
% 6.80/7.19 , clause( 20, [ ~( p8( Z, X ) ), p8( X, Y ), ~( p8( Z, Y ) ) ] )
% 6.80/7.19 , 2, clause( 2, [ p8( X, X ) ] )
% 6.80/7.19 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, X )] ),
% 6.80/7.19 substitution( 1, [ :=( X, X )] )).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 125, [ p8( Y, X ), ~( p8( X, Y ) ) ] )
% 6.80/7.19 , clause( 135748, [ ~( p8( X, Y ) ), p8( Y, X ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 1
% 6.80/7.19 ), ==>( 1, 0 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 resolution(
% 6.80/7.19 clause( 135749, [ p8( f12( f13( c26 ), f16( c27, X ) ), f12( f13( c23 ), X
% 6.80/7.19 ) ) ] )
% 6.80/7.19 , clause( 125, [ p8( Y, X ), ~( p8( X, Y ) ) ] )
% 6.80/7.19 , 1, clause( 23, [ p8( f12( f13( c23 ), X ), f12( f13( c26 ), f16( c27, X )
% 6.80/7.19 ) ) ] )
% 6.80/7.19 , 0, substitution( 0, [ :=( X, f12( f13( c23 ), X ) ), :=( Y, f12( f13( c26
% 6.80/7.19 ), f16( c27, X ) ) )] ), substitution( 1, [ :=( X, X )] )).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 166, [ p8( f12( f13( c26 ), f16( c27, X ) ), f12( f13( c23 ), X ) )
% 6.80/7.19 ] )
% 6.80/7.19 , clause( 135749, [ p8( f12( f13( c26 ), f16( c27, X ) ), f12( f13( c23 ),
% 6.80/7.19 X ) ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 resolution(
% 6.80/7.19 clause( 135750, [ p8( f12( X, Y ), f12( X, Z ) ), ~( p8( Y, Z ) ) ] )
% 6.80/7.19 , clause( 30, [ p8( f12( X, Y ), f12( Z, T ) ), ~( p8( Y, T ) ), ~( p11( X
% 6.80/7.19 , Z ) ) ] )
% 6.80/7.19 , 2, clause( 0, [ p11( X, X ) ] )
% 6.80/7.19 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, X ), :=( T, Z )] ),
% 6.80/7.19 substitution( 1, [ :=( X, X )] )).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 375, [ p8( f12( X, Y ), f12( X, Z ) ), ~( p8( Y, Z ) ) ] )
% 6.80/7.19 , clause( 135750, [ p8( f12( X, Y ), f12( X, Z ) ), ~( p8( Y, Z ) ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 6.80/7.19 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 resolution(
% 6.80/7.19 clause( 135751, [ p8( f12( X, f16( Y, f17( Z, Y ) ) ), f12( X, Z ) ) ] )
% 6.80/7.19 , clause( 375, [ p8( f12( X, Y ), f12( X, Z ) ), ~( p8( Y, Z ) ) ] )
% 6.80/7.19 , 1, clause( 7, [ p8( f16( X, f17( Y, X ) ), Y ) ] )
% 6.80/7.19 , 0, substitution( 0, [ :=( X, X ), :=( Y, f16( Y, f17( Z, Y ) ) ), :=( Z,
% 6.80/7.19 Z )] ), substitution( 1, [ :=( X, Y ), :=( Y, Z )] )).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 1314, [ p8( f12( X, f16( Y, f17( Z, Y ) ) ), f12( X, Z ) ) ] )
% 6.80/7.19 , clause( 135751, [ p8( f12( X, f16( Y, f17( Z, Y ) ) ), f12( X, Z ) ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 6.80/7.19 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 resolution(
% 6.80/7.19 clause( 135753, [ ~( p8( f12( f13( c26 ), f16( c27, X ) ), Y ) ), p8( Y,
% 6.80/7.19 f12( f13( c23 ), X ) ) ] )
% 6.80/7.19 , clause( 20, [ ~( p8( Z, X ) ), p8( X, Y ), ~( p8( Z, Y ) ) ] )
% 6.80/7.19 , 2, clause( 166, [ p8( f12( f13( c26 ), f16( c27, X ) ), f12( f13( c23 ),
% 6.80/7.19 X ) ) ] )
% 6.80/7.19 , 0, substitution( 0, [ :=( X, Y ), :=( Y, f12( f13( c23 ), X ) ), :=( Z,
% 6.80/7.19 f12( f13( c26 ), f16( c27, X ) ) )] ), substitution( 1, [ :=( X, X )] )
% 6.80/7.19 ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 1331, [ p8( Y, f12( f13( c23 ), X ) ), ~( p8( f12( f13( c26 ), f16(
% 6.80/7.19 c27, X ) ), Y ) ) ] )
% 6.80/7.19 , clause( 135753, [ ~( p8( f12( f13( c26 ), f16( c27, X ) ), Y ) ), p8( Y,
% 6.80/7.19 f12( f13( c23 ), X ) ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 1
% 6.80/7.19 ), ==>( 1, 0 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 resolution(
% 6.80/7.19 clause( 135754, [ p8( f12( f13( c26 ), X ), f12( f13( c23 ), f17( X, c27 )
% 6.80/7.19 ) ) ] )
% 6.80/7.19 , clause( 1331, [ p8( Y, f12( f13( c23 ), X ) ), ~( p8( f12( f13( c26 ),
% 6.80/7.19 f16( c27, X ) ), Y ) ) ] )
% 6.80/7.19 , 1, clause( 1314, [ p8( f12( X, f16( Y, f17( Z, Y ) ) ), f12( X, Z ) ) ]
% 6.80/7.19 )
% 6.80/7.19 , 0, substitution( 0, [ :=( X, f17( X, c27 ) ), :=( Y, f12( f13( c26 ), X )
% 6.80/7.19 )] ), substitution( 1, [ :=( X, f13( c26 ) ), :=( Y, c27 ), :=( Z, X )] )
% 6.80/7.19 ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 subsumption(
% 6.80/7.19 clause( 135623, [ p8( f12( f13( c26 ), X ), f12( f13( c23 ), f17( X, c27 )
% 6.80/7.19 ) ) ] )
% 6.80/7.19 , clause( 135754, [ p8( f12( f13( c26 ), X ), f12( f13( c23 ), f17( X, c27
% 6.80/7.19 ) ) ) ] )
% 6.80/7.19 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.80/7.19
% 6.80/7.19
% 6.80/7.19 resolution(
% 6.80/7.19 clause( 135755, [ p8( f12( f13( c23 ), f17( X, c27 ) ), f12( f13( c26 ), X
% 6.80/7.20 ) ) ] )
% 6.80/7.20 , clause( 125, [ p8( Y, X ), ~( p8( X, Y ) ) ] )
% 6.80/7.20 , 1, clause( 135623, [ p8( f12( f13( c26 ), X ), f12( f13( c23 ), f17( X,
% 6.80/7.20 c27 ) ) ) ] )
% 6.80/7.20 , 0, substitution( 0, [ :=( X, f12( f13( c26 ), X ) ), :=( Y, f12( f13( c23
% 6.80/7.20 ), f17( X, c27 ) ) )] ), substitution( 1, [ :=( X, X )] )).
% 6.80/7.20
% 6.80/7.20
% 6.80/7.20 subsumption(
% 6.80/7.20 clause( 135657, [ p8( f12( f13( c23 ), f17( X, c27 ) ), f12( f13( c26 ), X
% 6.80/7.20 ) ) ] )
% 6.80/7.20 , clause( 135755, [ p8( f12( f13( c23 ), f17( X, c27 ) ), f12( f13( c26 ),
% 6.80/7.20 X ) ) ] )
% 6.80/7.20 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.80/7.20
% 6.80/7.20
% 6.80/7.20 resolution(
% 6.80/7.20 clause( 135756, [] )
% 6.80/7.20 , clause( 25, [ ~( p8( f12( f13( c23 ), f17( c28, c27 ) ), f12( f13( c26 )
% 6.80/7.20 , c28 ) ) ) ] )
% 6.80/7.20 , 0, clause( 135657, [ p8( f12( f13( c23 ), f17( X, c27 ) ), f12( f13( c26
% 6.80/7.20 ), X ) ) ] )
% 6.80/7.20 , 0, substitution( 0, [] ), substitution( 1, [ :=( X, c28 )] )).
% 6.80/7.20
% 6.80/7.20
% 6.80/7.20 subsumption(
% 6.80/7.20 clause( 135690, [] )
% 6.80/7.20 , clause( 135756, [] )
% 6.80/7.20 , substitution( 0, [] ), permutation( 0, [] ) ).
% 6.80/7.20
% 6.80/7.20
% 6.80/7.20 end.
% 6.80/7.20
% 6.80/7.20 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 6.80/7.20
% 6.80/7.20 Memory use:
% 6.80/7.20
% 6.80/7.20 space for terms: 3073492
% 6.80/7.20 space for clauses: 9887837
% 6.80/7.20
% 6.80/7.20
% 6.80/7.20 clauses generated: 137681
% 6.80/7.20 clauses kept: 135691
% 6.80/7.20 clauses selected: 2667
% 6.80/7.20 clauses deleted: 8
% 6.80/7.20 clauses inuse deleted: 0
% 6.80/7.20
% 6.80/7.20 subsentry: 1303799
% 6.80/7.20 literals s-matched: 956777
% 6.80/7.20 literals matched: 956741
% 6.80/7.20 full subsumption: 2616
% 6.80/7.20
% 6.80/7.20 checksum: 1459589554
% 6.80/7.20
% 6.80/7.20
% 6.84/7.20 Bliksem ended
%------------------------------------------------------------------------------