%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : HEN005-2 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n020.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 : Sat Jul 16 12:47:02 EDT 2022
% Result : Unsatisfiable 140.73s 141.08s
% Output : Refutation 140.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : HEN005-2 : TPTP v8.1.0. Released v1.0.0.
% 0.11/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n020.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 : Fri Jul 1 13:23:30 EDT 2022
% 0.12/0.33 % CPUTime :
% 61.10/61.49 *** allocated 10000 integers for termspace/termends
% 61.10/61.49 *** allocated 10000 integers for clauses
% 61.10/61.49 *** allocated 10000 integers for justifications
% 61.10/61.49 Bliksem 1.12
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 Automatic Strategy Selection
% 61.10/61.49
% 61.10/61.49 Clauses:
% 61.10/61.49 [
% 61.10/61.49 [ ~( 'less_equal'( X, Y ) ), quotient( X, Y, zero ) ],
% 61.10/61.49 [ ~( quotient( X, Y, zero ) ), 'less_equal'( X, Y ) ],
% 61.10/61.49 [ ~( quotient( X, Y, Z ) ), 'less_equal'( Z, X ) ],
% 61.10/61.49 [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~( quotient( X, T
% 61.10/61.49 , W ) ), ~( quotient( W, U, V0 ) ), ~( quotient( Z, T, V1 ) ),
% 61.10/61.49 'less_equal'( V0, V1 ) ],
% 61.10/61.49 [ 'less_equal'( zero, X ) ],
% 61.10/61.49 [ ~( 'less_equal'( X, Y ) ), ~( 'less_equal'( Y, X ) ), =( X, Y ) ],
% 61.10/61.49 [ 'less_equal'( X, identity ) ],
% 61.10/61.49 [ quotient( X, Y, divide( X, Y ) ) ],
% 61.10/61.49 [ ~( quotient( X, Y, Z ) ), ~( quotient( X, Y, T ) ), =( Z, T ) ],
% 61.10/61.49 [ quotient( X, identity, zero ) ],
% 61.10/61.49 [ quotient( zero, X, zero ) ],
% 61.10/61.49 [ quotient( X, X, zero ) ],
% 61.10/61.49 [ quotient( X, zero, X ) ],
% 61.10/61.49 [ 'less_equal'( x, y ) ],
% 61.10/61.49 [ 'less_equal'( y, z ) ],
% 61.10/61.49 [ ~( 'less_equal'( x, z ) ) ]
% 61.10/61.49 ] .
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 percentage equality = 0.071429, percentage horn = 1.000000
% 61.10/61.49 This is a problem with some equality
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 Options Used:
% 61.10/61.49
% 61.10/61.49 useres = 1
% 61.10/61.49 useparamod = 1
% 61.10/61.49 useeqrefl = 1
% 61.10/61.49 useeqfact = 1
% 61.10/61.49 usefactor = 1
% 61.10/61.49 usesimpsplitting = 0
% 61.10/61.49 usesimpdemod = 5
% 61.10/61.49 usesimpres = 3
% 61.10/61.49
% 61.10/61.49 resimpinuse = 1000
% 61.10/61.49 resimpclauses = 20000
% 61.10/61.49 substype = eqrewr
% 61.10/61.49 backwardsubs = 1
% 61.10/61.49 selectoldest = 5
% 61.10/61.49
% 61.10/61.49 litorderings [0] = split
% 61.10/61.49 litorderings [1] = extend the termordering, first sorting on arguments
% 61.10/61.49
% 61.10/61.49 termordering = kbo
% 61.10/61.49
% 61.10/61.49 litapriori = 0
% 61.10/61.49 termapriori = 1
% 61.10/61.49 litaposteriori = 0
% 61.10/61.49 termaposteriori = 0
% 61.10/61.49 demodaposteriori = 0
% 61.10/61.49 ordereqreflfact = 0
% 61.10/61.49
% 61.10/61.49 litselect = negord
% 61.10/61.49
% 61.10/61.49 maxweight = 15
% 61.10/61.49 maxdepth = 30000
% 61.10/61.49 maxlength = 115
% 61.10/61.49 maxnrvars = 195
% 61.10/61.49 excuselevel = 1
% 61.10/61.49 increasemaxweight = 1
% 61.10/61.49
% 61.10/61.49 maxselected = 10000000
% 61.10/61.49 maxnrclauses = 10000000
% 61.10/61.49
% 61.10/61.49 showgenerated = 0
% 61.10/61.49 showkept = 0
% 61.10/61.49 showselected = 0
% 61.10/61.49 showdeleted = 0
% 61.10/61.49 showresimp = 1
% 61.10/61.49 showstatus = 2000
% 61.10/61.49
% 61.10/61.49 prologoutput = 1
% 61.10/61.49 nrgoals = 5000000
% 61.10/61.49 totalproof = 1
% 61.10/61.49
% 61.10/61.49 Symbols occurring in the translation:
% 61.10/61.49
% 61.10/61.49 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 61.10/61.49 . [1, 2] (w:1, o:28, a:1, s:1, b:0),
% 61.10/61.49 ! [4, 1] (w:0, o:23, a:1, s:1, b:0),
% 61.10/61.49 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 61.10/61.49 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 61.10/61.49 'less_equal' [41, 2] (w:1, o:53, a:1, s:1, b:0),
% 61.10/61.49 zero [42, 0] (w:1, o:13, a:1, s:1, b:0),
% 61.10/61.49 quotient [43, 3] (w:1, o:55, a:1, s:1, b:0),
% 61.10/61.49 identity [50, 0] (w:1, o:20, a:1, s:1, b:0),
% 61.10/61.49 divide [51, 2] (w:1, o:54, a:1, s:1, b:0),
% 61.10/61.49 x [53, 0] (w:1, o:21, a:1, s:1, b:0),
% 61.10/61.49 y [54, 0] (w:1, o:12, a:1, s:1, b:0),
% 61.10/61.49 z [55, 0] (w:1, o:22, a:1, s:1, b:0).
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 Starting Search:
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 Intermediate Status:
% 61.10/61.49 Generated: 13732
% 61.10/61.49 Kept: 2002
% 61.10/61.49 Inuse: 196
% 61.10/61.49 Deleted: 47
% 61.10/61.49 Deletedinuse: 9
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 Intermediate Status:
% 61.10/61.49 Generated: 27344
% 61.10/61.49 Kept: 4014
% 61.10/61.49 Inuse: 297
% 61.10/61.49 Deleted: 92
% 61.10/61.49 Deletedinuse: 29
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 Intermediate Status:
% 61.10/61.49 Generated: 60822
% 61.10/61.49 Kept: 6299
% 61.10/61.49 Inuse: 440
% 61.10/61.49 Deleted: 147
% 61.10/61.49 Deletedinuse: 31
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 Intermediate Status:
% 61.10/61.49 Generated: 75643
% 61.10/61.49 Kept: 8307
% 61.10/61.49 Inuse: 497
% 61.10/61.49 Deleted: 155
% 61.10/61.49 Deletedinuse: 31
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 Intermediate Status:
% 61.10/61.49 Generated: 98898
% 61.10/61.49 Kept: 10813
% 61.10/61.49 Inuse: 574
% 61.10/61.49 Deleted: 173
% 61.10/61.49 Deletedinuse: 31
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 Intermediate Status:
% 61.10/61.49 Generated: 123336
% 61.10/61.49 Kept: 12825
% 61.10/61.49 Inuse: 653
% 61.10/61.49 Deleted: 189
% 61.10/61.49 Deletedinuse: 31
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 Intermediate Status:
% 61.10/61.49 Generated: 159004
% 61.10/61.49 Kept: 14840
% 61.10/61.49 Inuse: 762
% 61.10/61.49 Deleted: 204
% 61.10/61.49 Deletedinuse: 31
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49 Resimplifying inuse:
% 61.10/61.49 Done
% 61.10/61.49
% 61.10/61.49
% 61.10/61.49 Intermediate Status:
% 61.10/61.49 Generated: 186553
% 61.10/61.49 Kept: 16843
% 61.10/61.49 Inuse: 845
% 61.10/61.49 Deleted: 254
% 140.73/141.08 Deletedinuse: 37
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 210786
% 140.73/141.08 Kept: 18865
% 140.73/141.08 Inuse: 906
% 140.73/141.08 Deleted: 308
% 140.73/141.08 Deletedinuse: 37
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying clauses:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 236469
% 140.73/141.08 Kept: 21175
% 140.73/141.08 Inuse: 987
% 140.73/141.08 Deleted: 2405
% 140.73/141.08 Deletedinuse: 37
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 270377
% 140.73/141.08 Kept: 23299
% 140.73/141.08 Inuse: 1044
% 140.73/141.08 Deleted: 2405
% 140.73/141.08 Deletedinuse: 37
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 292401
% 140.73/141.08 Kept: 25550
% 140.73/141.08 Inuse: 1084
% 140.73/141.08 Deleted: 2405
% 140.73/141.08 Deletedinuse: 37
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 325360
% 140.73/141.08 Kept: 27558
% 140.73/141.08 Inuse: 1156
% 140.73/141.08 Deleted: 2409
% 140.73/141.08 Deletedinuse: 40
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 355700
% 140.73/141.08 Kept: 29598
% 140.73/141.08 Inuse: 1206
% 140.73/141.08 Deleted: 2456
% 140.73/141.08 Deletedinuse: 87
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 386219
% 140.73/141.08 Kept: 32099
% 140.73/141.08 Inuse: 1229
% 140.73/141.08 Deleted: 2456
% 140.73/141.08 Deletedinuse: 87
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 418825
% 140.73/141.08 Kept: 34131
% 140.73/141.08 Inuse: 1293
% 140.73/141.08 Deleted: 2457
% 140.73/141.08 Deletedinuse: 87
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 449397
% 140.73/141.08 Kept: 36587
% 140.73/141.08 Inuse: 1338
% 140.73/141.08 Deleted: 2458
% 140.73/141.08 Deletedinuse: 87
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 471769
% 140.73/141.08 Kept: 38655
% 140.73/141.08 Inuse: 1369
% 140.73/141.08 Deleted: 2458
% 140.73/141.08 Deletedinuse: 87
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying clauses:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 506171
% 140.73/141.08 Kept: 40662
% 140.73/141.08 Inuse: 1439
% 140.73/141.08 Deleted: 5672
% 140.73/141.08 Deletedinuse: 87
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 539103
% 140.73/141.08 Kept: 42705
% 140.73/141.08 Inuse: 1508
% 140.73/141.08 Deleted: 5672
% 140.73/141.08 Deletedinuse: 87
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 571560
% 140.73/141.08 Kept: 44726
% 140.73/141.08 Inuse: 1559
% 140.73/141.08 Deleted: 5672
% 140.73/141.08 Deletedinuse: 87
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 624510
% 140.73/141.08 Kept: 46734
% 140.73/141.08 Inuse: 1629
% 140.73/141.08 Deleted: 5672
% 140.73/141.08 Deletedinuse: 87
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 670952
% 140.73/141.08 Kept: 48794
% 140.73/141.08 Inuse: 1659
% 140.73/141.08 Deleted: 5672
% 140.73/141.08 Deletedinuse: 87
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 722707
% 140.73/141.08 Kept: 50811
% 140.73/141.08 Inuse: 1718
% 140.73/141.08 Deleted: 5673
% 140.73/141.08 Deletedinuse: 88
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 787876
% 140.73/141.08 Kept: 52824
% 140.73/141.08 Inuse: 1787
% 140.73/141.08 Deleted: 5674
% 140.73/141.08 Deletedinuse: 89
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 823671
% 140.73/141.08 Kept: 54849
% 140.73/141.08 Inuse: 1839
% 140.73/141.08 Deleted: 5676
% 140.73/141.08 Deletedinuse: 91
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 857371
% 140.73/141.08 Kept: 57094
% 140.73/141.08 Inuse: 1858
% 140.73/141.08 Deleted: 5676
% 140.73/141.08 Deletedinuse: 91
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 880724
% 140.73/141.08 Kept: 59458
% 140.73/141.08 Inuse: 1871
% 140.73/141.08 Deleted: 5685
% 140.73/141.08 Deletedinuse: 100
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying clauses:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 907311
% 140.73/141.08 Kept: 61511
% 140.73/141.08 Inuse: 1896
% 140.73/141.08 Deleted: 7966
% 140.73/141.08 Deletedinuse: 100
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 942943
% 140.73/141.08 Kept: 63530
% 140.73/141.08 Inuse: 1925
% 140.73/141.08 Deleted: 7967
% 140.73/141.08 Deletedinuse: 101
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 979724
% 140.73/141.08 Kept: 66073
% 140.73/141.08 Inuse: 1969
% 140.73/141.08 Deleted: 7971
% 140.73/141.08 Deletedinuse: 101
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 1026627
% 140.73/141.08 Kept: 68083
% 140.73/141.08 Inuse: 2002
% 140.73/141.08 Deleted: 7972
% 140.73/141.08 Deletedinuse: 102
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 1080351
% 140.73/141.08 Kept: 70144
% 140.73/141.08 Inuse: 2014
% 140.73/141.08 Deleted: 7972
% 140.73/141.08 Deletedinuse: 102
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 1195282
% 140.73/141.08 Kept: 72211
% 140.73/141.08 Inuse: 2055
% 140.73/141.08 Deleted: 7972
% 140.73/141.08 Deletedinuse: 102
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 1214395
% 140.73/141.08 Kept: 74687
% 140.73/141.08 Inuse: 2058
% 140.73/141.08 Deleted: 7972
% 140.73/141.08 Deletedinuse: 102
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 1334259
% 140.73/141.08 Kept: 76866
% 140.73/141.08 Inuse: 2098
% 140.73/141.08 Deleted: 7972
% 140.73/141.08 Deletedinuse: 102
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 1428768
% 140.73/141.08 Kept: 78873
% 140.73/141.08 Inuse: 2120
% 140.73/141.08 Deleted: 7972
% 140.73/141.08 Deletedinuse: 102
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying clauses:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 1476616
% 140.73/141.08 Kept: 80880
% 140.73/141.08 Inuse: 2145
% 140.73/141.08 Deleted: 10135
% 140.73/141.08 Deletedinuse: 102
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 1643868
% 140.73/141.08 Kept: 82906
% 140.73/141.08 Inuse: 2225
% 140.73/141.08 Deleted: 10135
% 140.73/141.08 Deletedinuse: 102
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Intermediate Status:
% 140.73/141.08 Generated: 1697565
% 140.73/141.08 Kept: 84971
% 140.73/141.08 Inuse: 2251
% 140.73/141.08 Deleted: 10135
% 140.73/141.08 Deletedinuse: 102
% 140.73/141.08
% 140.73/141.08 Resimplifying inuse:
% 140.73/141.08 Done
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 Bliksems!, er is een bewijs:
% 140.73/141.08 % SZS status Unsatisfiable
% 140.73/141.08 % SZS output start Refutation
% 140.73/141.08
% 140.73/141.08 clause( 0, [ ~( 'less_equal'( X, Y ) ), quotient( X, Y, zero ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 1, [ ~( quotient( X, Y, zero ) ), 'less_equal'( X, Y ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 2, [ ~( quotient( X, Y, Z ) ), 'less_equal'( Z, X ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 3, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~(
% 140.73/141.08 quotient( X, T, W ) ), ~( quotient( W, U, V0 ) ), ~( quotient( Z, T, V1 )
% 140.73/141.08 ), 'less_equal'( V0, V1 ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 4, [ 'less_equal'( zero, X ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 5, [ ~( 'less_equal'( X, Y ) ), ~( 'less_equal'( Y, X ) ), =( X, Y
% 140.73/141.08 ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 7, [ quotient( X, Y, divide( X, Y ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 8, [ ~( quotient( X, Y, Z ) ), ~( quotient( X, Y, T ) ), =( Z, T )
% 140.73/141.08 ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 11, [ quotient( X, X, zero ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 12, [ quotient( X, zero, X ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 13, [ 'less_equal'( x, y ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 14, [ 'less_equal'( y, z ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 15, [ ~( 'less_equal'( x, z ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 38, [ quotient( x, y, zero ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 39, [ quotient( y, z, zero ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 41, [ ~( quotient( x, z, zero ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 44, [ 'less_equal'( divide( X, Y ), X ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 49, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~(
% 140.73/141.08 quotient( X, T, W ) ), ~( quotient( Z, T, V0 ) ), 'less_equal'( divide( W
% 140.73/141.08 , U ), V0 ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 66, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, zero ) ), ~(
% 140.73/141.08 quotient( X, T, U ) ), ~( quotient( Z, T, W ) ), 'less_equal'( U, W ) ]
% 140.73/141.08 )
% 140.73/141.08 .
% 140.73/141.08 clause( 69, [ ~( quotient( X, Y, Z ) ), ~( quotient( X, T, U ) ), ~(
% 140.73/141.08 quotient( U, zero, W ) ), ~( quotient( Z, T, V0 ) ), 'less_equal'( W, V0
% 140.73/141.08 ), ~( 'less_equal'( Y, T ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 78, [ ~( quotient( X, zero, Y ) ), ~( quotient( X, Z, X ) ), ~(
% 140.73/141.08 quotient( Y, Z, T ) ), 'less_equal'( Y, T ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 81, [ ~( quotient( X, zero, Y ) ), 'less_equal'( X, Y ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 89, [ ~( quotient( X, Y, Y ) ), ~( quotient( Y, Z, zero ) ), ~(
% 140.73/141.08 quotient( X, Z, T ) ), 'less_equal'( T, zero ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 90, [ ~( quotient( X, Y, Y ) ), 'less_equal'( Y, zero ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 125, [ 'less_equal'( X, divide( X, zero ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 129, [ =( divide( X, zero ), X ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 131, [ =( X, zero ), ~( quotient( Y, X, X ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 138, [ ~( 'less_equal'( X, zero ) ), =( zero, X ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 160, [ ~( quotient( x, z, X ) ), ~( 'less_equal'( X, zero ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 174, [ 'less_equal'( X, Y ), ~( 'less_equal'( X, zero ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 178, [ 'less_equal'( X, Y ), ~( quotient( X, zero, zero ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 181, [ 'less_equal'( X, Y ), ~( quotient( zero, Z, X ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 182, [ ~( 'less_equal'( X, zero ) ), quotient( X, Y, zero ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 193, [ ~( quotient( x, y, X ) ), =( zero, X ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 796, [ ~( quotient( zero, X, Y ) ), quotient( Y, Z, zero ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 1130, [ ~( quotient( X, y, Y ) ), ~( quotient( X, z, Z ) ), ~(
% 140.73/141.08 quotient( Y, z, T ) ), 'less_equal'( Z, T ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 1698, [ 'less_equal'( Y, Z ), ~( quotient( Y, X, X ) ), ~( quotient(
% 140.73/141.08 T, X, X ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 1764, [ 'less_equal'( X, Y ), ~( quotient( X, Z, Z ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 1807, [ ~( quotient( X, Y, Y ) ), =( zero, X ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 4359, [ 'less_equal'( X, Y ), ~( quotient( x, y, X ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 5121, [ ~( quotient( X, Y, Z ) ), quotient( Z, T, X ), ~( quotient(
% 140.73/141.08 X, U, U ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 5128, [ ~( quotient( X, Y, Y ) ), quotient( Y, Z, X ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 5135, [ quotient( zero, X, Y ), ~( 'less_equal'( Y, zero ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 5137, [ quotient( zero, X, Y ), ~( quotient( x, y, Y ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 85641, [ ~( quotient( X, y, zero ) ), ~( quotient( X, z, Y ) ),
% 140.73/141.08 'less_equal'( Y, Z ), ~( quotient( x, y, Z ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 85705, [ ~( quotient( x, z, X ) ), 'less_equal'( X, zero ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 85707, [ ~( quotient( x, z, X ) ) ] )
% 140.73/141.08 .
% 140.73/141.08 clause( 85712, [] )
% 140.73/141.08 .
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 % SZS output end Refutation
% 140.73/141.08 found a proof!
% 140.73/141.08
% 140.73/141.08 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 140.73/141.08
% 140.73/141.08 initialclauses(
% 140.73/141.08 [ clause( 85714, [ ~( 'less_equal'( X, Y ) ), quotient( X, Y, zero ) ] )
% 140.73/141.08 , clause( 85715, [ ~( quotient( X, Y, zero ) ), 'less_equal'( X, Y ) ] )
% 140.73/141.08 , clause( 85716, [ ~( quotient( X, Y, Z ) ), 'less_equal'( Z, X ) ] )
% 140.73/141.08 , clause( 85717, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~(
% 140.73/141.08 quotient( X, T, W ) ), ~( quotient( W, U, V0 ) ), ~( quotient( Z, T, V1 )
% 140.73/141.08 ), 'less_equal'( V0, V1 ) ] )
% 140.73/141.08 , clause( 85718, [ 'less_equal'( zero, X ) ] )
% 140.73/141.08 , clause( 85719, [ ~( 'less_equal'( X, Y ) ), ~( 'less_equal'( Y, X ) ),
% 140.73/141.08 =( X, Y ) ] )
% 140.73/141.08 , clause( 85720, [ 'less_equal'( X, identity ) ] )
% 140.73/141.08 , clause( 85721, [ quotient( X, Y, divide( X, Y ) ) ] )
% 140.73/141.08 , clause( 85722, [ ~( quotient( X, Y, Z ) ), ~( quotient( X, Y, T ) ), =( Z
% 140.73/141.08 , T ) ] )
% 140.73/141.08 , clause( 85723, [ quotient( X, identity, zero ) ] )
% 140.73/141.08 , clause( 85724, [ quotient( zero, X, zero ) ] )
% 140.73/141.08 , clause( 85725, [ quotient( X, X, zero ) ] )
% 140.73/141.08 , clause( 85726, [ quotient( X, zero, X ) ] )
% 140.73/141.08 , clause( 85727, [ 'less_equal'( x, y ) ] )
% 140.73/141.08 , clause( 85728, [ 'less_equal'( y, z ) ] )
% 140.73/141.08 , clause( 85729, [ ~( 'less_equal'( x, z ) ) ] )
% 140.73/141.08 ] ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 0, [ ~( 'less_equal'( X, Y ) ), quotient( X, Y, zero ) ] )
% 140.73/141.08 , clause( 85714, [ ~( 'less_equal'( X, Y ) ), quotient( X, Y, zero ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 140.73/141.08 ), ==>( 1, 1 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 1, [ ~( quotient( X, Y, zero ) ), 'less_equal'( X, Y ) ] )
% 140.73/141.08 , clause( 85715, [ ~( quotient( X, Y, zero ) ), 'less_equal'( X, Y ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 140.73/141.08 ), ==>( 1, 1 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 2, [ ~( quotient( X, Y, Z ) ), 'less_equal'( Z, X ) ] )
% 140.73/141.08 , clause( 85716, [ ~( quotient( X, Y, Z ) ), 'less_equal'( Z, X ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 140.73/141.08 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 3, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~(
% 140.73/141.08 quotient( X, T, W ) ), ~( quotient( W, U, V0 ) ), ~( quotient( Z, T, V1 )
% 140.73/141.08 ), 'less_equal'( V0, V1 ) ] )
% 140.73/141.08 , clause( 85717, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~(
% 140.73/141.08 quotient( X, T, W ) ), ~( quotient( W, U, V0 ) ), ~( quotient( Z, T, V1 )
% 140.73/141.08 ), 'less_equal'( V0, V1 ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 140.73/141.08 , U ), :=( W, W ), :=( V0, V0 ), :=( V1, V1 )] ), permutation( 0, [ ==>(
% 140.73/141.08 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3, 3 ), ==>( 4, 4 ), ==>( 5, 5 )] )
% 140.73/141.08 ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 4, [ 'less_equal'( zero, X ) ] )
% 140.73/141.08 , clause( 85718, [ 'less_equal'( zero, X ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 5, [ ~( 'less_equal'( X, Y ) ), ~( 'less_equal'( Y, X ) ), =( X, Y
% 140.73/141.08 ) ] )
% 140.73/141.08 , clause( 85719, [ ~( 'less_equal'( X, Y ) ), ~( 'less_equal'( Y, X ) ),
% 140.73/141.08 =( X, Y ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 140.73/141.08 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 7, [ quotient( X, Y, divide( X, Y ) ) ] )
% 140.73/141.08 , clause( 85721, [ quotient( X, Y, divide( X, Y ) ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 140.73/141.08 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 8, [ ~( quotient( X, Y, Z ) ), ~( quotient( X, Y, T ) ), =( Z, T )
% 140.73/141.08 ] )
% 140.73/141.08 , clause( 85722, [ ~( quotient( X, Y, Z ) ), ~( quotient( X, Y, T ) ), =( Z
% 140.73/141.08 , T ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 140.73/141.08 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 11, [ quotient( X, X, zero ) ] )
% 140.73/141.08 , clause( 85725, [ quotient( X, X, zero ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 12, [ quotient( X, zero, X ) ] )
% 140.73/141.08 , clause( 85726, [ quotient( X, zero, X ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 13, [ 'less_equal'( x, y ) ] )
% 140.73/141.08 , clause( 85727, [ 'less_equal'( x, y ) ] )
% 140.73/141.08 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 14, [ 'less_equal'( y, z ) ] )
% 140.73/141.08 , clause( 85728, [ 'less_equal'( y, z ) ] )
% 140.73/141.08 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 15, [ ~( 'less_equal'( x, z ) ) ] )
% 140.73/141.08 , clause( 85729, [ ~( 'less_equal'( x, z ) ) ] )
% 140.73/141.08 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86104, [ quotient( x, y, zero ) ] )
% 140.73/141.08 , clause( 0, [ ~( 'less_equal'( X, Y ) ), quotient( X, Y, zero ) ] )
% 140.73/141.08 , 0, clause( 13, [ 'less_equal'( x, y ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, x ), :=( Y, y )] ), substitution( 1, [] )
% 140.73/141.08 ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 38, [ quotient( x, y, zero ) ] )
% 140.73/141.08 , clause( 86104, [ quotient( x, y, zero ) ] )
% 140.73/141.08 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86105, [ quotient( y, z, zero ) ] )
% 140.73/141.08 , clause( 0, [ ~( 'less_equal'( X, Y ) ), quotient( X, Y, zero ) ] )
% 140.73/141.08 , 0, clause( 14, [ 'less_equal'( y, z ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, y ), :=( Y, z )] ), substitution( 1, [] )
% 140.73/141.08 ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 39, [ quotient( y, z, zero ) ] )
% 140.73/141.08 , clause( 86105, [ quotient( y, z, zero ) ] )
% 140.73/141.08 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86106, [ ~( quotient( x, z, zero ) ) ] )
% 140.73/141.08 , clause( 15, [ ~( 'less_equal'( x, z ) ) ] )
% 140.73/141.08 , 0, clause( 1, [ ~( quotient( X, Y, zero ) ), 'less_equal'( X, Y ) ] )
% 140.73/141.08 , 1, substitution( 0, [] ), substitution( 1, [ :=( X, x ), :=( Y, z )] )
% 140.73/141.08 ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 41, [ ~( quotient( x, z, zero ) ) ] )
% 140.73/141.08 , clause( 86106, [ ~( quotient( x, z, zero ) ) ] )
% 140.73/141.08 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86107, [ 'less_equal'( divide( X, Y ), X ) ] )
% 140.73/141.08 , clause( 2, [ ~( quotient( X, Y, Z ) ), 'less_equal'( Z, X ) ] )
% 140.73/141.08 , 0, clause( 7, [ quotient( X, Y, divide( X, Y ) ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, divide( X, Y ) )] )
% 140.73/141.08 , substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 44, [ 'less_equal'( divide( X, Y ), X ) ] )
% 140.73/141.08 , clause( 86107, [ 'less_equal'( divide( X, Y ), X ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 140.73/141.08 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86111, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~(
% 140.73/141.08 quotient( X, T, W ) ), ~( quotient( Z, T, V0 ) ), 'less_equal'( divide( W
% 140.73/141.08 , U ), V0 ) ] )
% 140.73/141.08 , clause( 3, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~(
% 140.73/141.08 quotient( X, T, W ) ), ~( quotient( W, U, V0 ) ), ~( quotient( Z, T, V1 )
% 140.73/141.08 ), 'less_equal'( V0, V1 ) ] )
% 140.73/141.08 , 3, clause( 7, [ quotient( X, Y, divide( X, Y ) ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ),
% 140.73/141.08 :=( U, U ), :=( W, W ), :=( V0, divide( W, U ) ), :=( V1, V0 )] ),
% 140.73/141.08 substitution( 1, [ :=( X, W ), :=( Y, U )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 49, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~(
% 140.73/141.08 quotient( X, T, W ) ), ~( quotient( Z, T, V0 ) ), 'less_equal'( divide( W
% 140.73/141.08 , U ), V0 ) ] )
% 140.73/141.08 , clause( 86111, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~(
% 140.73/141.08 quotient( X, T, W ) ), ~( quotient( Z, T, V0 ) ), 'less_equal'( divide( W
% 140.73/141.08 , U ), V0 ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 140.73/141.08 , U ), :=( W, W ), :=( V0, V0 )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1
% 140.73/141.08 , 1 ), ==>( 2, 2 ), ==>( 3, 3 ), ==>( 4, 4 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86159, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, zero ) ), ~(
% 140.73/141.08 quotient( X, T, U ) ), ~( quotient( Z, T, W ) ), 'less_equal'( U, W ) ]
% 140.73/141.08 )
% 140.73/141.08 , clause( 3, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~(
% 140.73/141.08 quotient( X, T, W ) ), ~( quotient( W, U, V0 ) ), ~( quotient( Z, T, V1 )
% 140.73/141.08 ), 'less_equal'( V0, V1 ) ] )
% 140.73/141.08 , 3, clause( 12, [ quotient( X, zero, X ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ),
% 140.73/141.08 :=( U, zero ), :=( W, U ), :=( V0, U ), :=( V1, W )] ), substitution( 1
% 140.73/141.08 , [ :=( X, U )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 66, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, zero ) ), ~(
% 140.73/141.08 quotient( X, T, U ) ), ~( quotient( Z, T, W ) ), 'less_equal'( U, W ) ]
% 140.73/141.08 )
% 140.73/141.08 , clause( 86159, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, zero ) ),
% 140.73/141.08 ~( quotient( X, T, U ) ), ~( quotient( Z, T, W ) ), 'less_equal'( U, W )
% 140.73/141.08 ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 140.73/141.08 , U ), :=( W, W )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2
% 140.73/141.08 , 2 ), ==>( 3, 3 ), ==>( 4, 4 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86207, [ ~( quotient( X, Y, Z ) ), ~( quotient( X, T, U ) ), ~(
% 140.73/141.08 quotient( U, zero, W ) ), ~( quotient( Z, T, V0 ) ), 'less_equal'( W, V0
% 140.73/141.08 ), ~( 'less_equal'( Y, T ) ) ] )
% 140.73/141.08 , clause( 3, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, U ) ), ~(
% 140.73/141.08 quotient( X, T, W ) ), ~( quotient( W, U, V0 ) ), ~( quotient( Z, T, V1 )
% 140.73/141.08 ), 'less_equal'( V0, V1 ) ] )
% 140.73/141.08 , 1, clause( 0, [ ~( 'less_equal'( X, Y ) ), quotient( X, Y, zero ) ] )
% 140.73/141.08 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ),
% 140.73/141.08 :=( U, zero ), :=( W, U ), :=( V0, W ), :=( V1, V0 )] ), substitution( 1
% 140.73/141.08 , [ :=( X, Y ), :=( Y, T )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 69, [ ~( quotient( X, Y, Z ) ), ~( quotient( X, T, U ) ), ~(
% 140.73/141.08 quotient( U, zero, W ) ), ~( quotient( Z, T, V0 ) ), 'less_equal'( W, V0
% 140.73/141.08 ), ~( 'less_equal'( Y, T ) ) ] )
% 140.73/141.08 , clause( 86207, [ ~( quotient( X, Y, Z ) ), ~( quotient( X, T, U ) ), ~(
% 140.73/141.08 quotient( U, zero, W ) ), ~( quotient( Z, T, V0 ) ), 'less_equal'( W, V0
% 140.73/141.08 ), ~( 'less_equal'( Y, T ) ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 140.73/141.08 , U ), :=( W, W ), :=( V0, V0 )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1
% 140.73/141.08 , 1 ), ==>( 2, 2 ), ==>( 3, 3 ), ==>( 4, 4 ), ==>( 5, 5 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 factor(
% 140.73/141.08 clause( 86274, [ ~( quotient( X, zero, Y ) ), ~( quotient( X, Z, X ) ), ~(
% 140.73/141.08 quotient( Y, Z, T ) ), 'less_equal'( Y, T ), ~( 'less_equal'( zero, Z ) )
% 140.73/141.08 ] )
% 140.73/141.08 , clause( 69, [ ~( quotient( X, Y, Z ) ), ~( quotient( X, T, U ) ), ~(
% 140.73/141.08 quotient( U, zero, W ) ), ~( quotient( Z, T, V0 ) ), 'less_equal'( W, V0
% 140.73/141.08 ), ~( 'less_equal'( Y, T ) ) ] )
% 140.73/141.08 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, zero ), :=( Z, Y ), :=( T, Z
% 140.73/141.08 ), :=( U, X ), :=( W, Y ), :=( V0, T )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86285, [ ~( quotient( X, zero, Y ) ), ~( quotient( X, Z, X ) ), ~(
% 140.73/141.08 quotient( Y, Z, T ) ), 'less_equal'( Y, T ) ] )
% 140.73/141.08 , clause( 86274, [ ~( quotient( X, zero, Y ) ), ~( quotient( X, Z, X ) ),
% 140.73/141.08 ~( quotient( Y, Z, T ) ), 'less_equal'( Y, T ), ~( 'less_equal'( zero, Z
% 140.73/141.08 ) ) ] )
% 140.73/141.08 , 4, clause( 4, [ 'less_equal'( zero, X ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 140.73/141.08 substitution( 1, [ :=( X, Z )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 78, [ ~( quotient( X, zero, Y ) ), ~( quotient( X, Z, X ) ), ~(
% 140.73/141.08 quotient( Y, Z, T ) ), 'less_equal'( Y, T ) ] )
% 140.73/141.08 , clause( 86285, [ ~( quotient( X, zero, Y ) ), ~( quotient( X, Z, X ) ),
% 140.73/141.08 ~( quotient( Y, Z, T ) ), 'less_equal'( Y, T ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 140.73/141.08 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3, 3 )] )
% 140.73/141.08 ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 factor(
% 140.73/141.08 clause( 86288, [ ~( quotient( X, zero, X ) ), ~( quotient( X, zero, Y ) ),
% 140.73/141.08 'less_equal'( X, Y ) ] )
% 140.73/141.08 , clause( 78, [ ~( quotient( X, zero, Y ) ), ~( quotient( X, Z, X ) ), ~(
% 140.73/141.08 quotient( Y, Z, T ) ), 'less_equal'( Y, T ) ] )
% 140.73/141.08 , 0, 1, substitution( 0, [ :=( X, X ), :=( Y, X ), :=( Z, zero ), :=( T, Y
% 140.73/141.08 )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86291, [ ~( quotient( X, zero, Y ) ), 'less_equal'( X, Y ) ] )
% 140.73/141.08 , clause( 86288, [ ~( quotient( X, zero, X ) ), ~( quotient( X, zero, Y ) )
% 140.73/141.08 , 'less_equal'( X, Y ) ] )
% 140.73/141.08 , 0, clause( 12, [ quotient( X, zero, X ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [ :=( X
% 140.73/141.08 , X )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 81, [ ~( quotient( X, zero, Y ) ), 'less_equal'( X, Y ) ] )
% 140.73/141.08 , clause( 86291, [ ~( quotient( X, zero, Y ) ), 'less_equal'( X, Y ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 140.73/141.08 ), ==>( 1, 1 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 factor(
% 140.73/141.08 clause( 86296, [ ~( quotient( X, Y, Y ) ), ~( quotient( Y, Z, zero ) ), ~(
% 140.73/141.08 quotient( X, Z, T ) ), 'less_equal'( T, zero ) ] )
% 140.73/141.08 , clause( 66, [ ~( quotient( X, Y, Z ) ), ~( quotient( Y, T, zero ) ), ~(
% 140.73/141.08 quotient( X, T, U ) ), ~( quotient( Z, T, W ) ), 'less_equal'( U, W ) ]
% 140.73/141.08 )
% 140.73/141.08 , 1, 3, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Y ), :=( T, Z ),
% 140.73/141.08 :=( U, T ), :=( W, zero )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 89, [ ~( quotient( X, Y, Y ) ), ~( quotient( Y, Z, zero ) ), ~(
% 140.73/141.08 quotient( X, Z, T ) ), 'less_equal'( T, zero ) ] )
% 140.73/141.08 , clause( 86296, [ ~( quotient( X, Y, Y ) ), ~( quotient( Y, Z, zero ) ),
% 140.73/141.08 ~( quotient( X, Z, T ) ), 'less_equal'( T, zero ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 140.73/141.08 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3, 3 )] )
% 140.73/141.08 ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 factor(
% 140.73/141.08 clause( 86307, [ ~( quotient( X, Y, Y ) ), ~( quotient( Y, Y, zero ) ),
% 140.73/141.08 'less_equal'( Y, zero ) ] )
% 140.73/141.08 , clause( 89, [ ~( quotient( X, Y, Y ) ), ~( quotient( Y, Z, zero ) ), ~(
% 140.73/141.08 quotient( X, Z, T ) ), 'less_equal'( T, zero ) ] )
% 140.73/141.08 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Y ), :=( T, Y )] )
% 140.73/141.08 ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86311, [ ~( quotient( X, Y, Y ) ), 'less_equal'( Y, zero ) ] )
% 140.73/141.08 , clause( 86307, [ ~( quotient( X, Y, Y ) ), ~( quotient( Y, Y, zero ) ),
% 140.73/141.08 'less_equal'( Y, zero ) ] )
% 140.73/141.08 , 1, clause( 11, [ quotient( X, X, zero ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [ :=( X
% 140.73/141.08 , Y )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 90, [ ~( quotient( X, Y, Y ) ), 'less_equal'( Y, zero ) ] )
% 140.73/141.08 , clause( 86311, [ ~( quotient( X, Y, Y ) ), 'less_equal'( Y, zero ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 140.73/141.08 ), ==>( 1, 1 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86312, [ 'less_equal'( X, divide( X, zero ) ) ] )
% 140.73/141.08 , clause( 81, [ ~( quotient( X, zero, Y ) ), 'less_equal'( X, Y ) ] )
% 140.73/141.08 , 0, clause( 7, [ quotient( X, Y, divide( X, Y ) ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, X ), :=( Y, divide( X, zero ) )] ),
% 140.73/141.08 substitution( 1, [ :=( X, X ), :=( Y, zero )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 125, [ 'less_equal'( X, divide( X, zero ) ) ] )
% 140.73/141.08 , clause( 86312, [ 'less_equal'( X, divide( X, zero ) ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86313, [ ~( 'less_equal'( divide( X, zero ), X ) ), =( X, divide( X
% 140.73/141.08 , zero ) ) ] )
% 140.73/141.08 , clause( 5, [ ~( 'less_equal'( X, Y ) ), ~( 'less_equal'( Y, X ) ), =( X,
% 140.73/141.08 Y ) ] )
% 140.73/141.08 , 0, clause( 125, [ 'less_equal'( X, divide( X, zero ) ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, X ), :=( Y, divide( X, zero ) )] ),
% 140.73/141.08 substitution( 1, [ :=( X, X )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86315, [ =( X, divide( X, zero ) ) ] )
% 140.73/141.08 , clause( 86313, [ ~( 'less_equal'( divide( X, zero ), X ) ), =( X, divide(
% 140.73/141.08 X, zero ) ) ] )
% 140.73/141.08 , 0, clause( 44, [ 'less_equal'( divide( X, Y ), X ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ), :=( Y
% 140.73/141.08 , zero )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 eqswap(
% 140.73/141.08 clause( 86316, [ =( divide( X, zero ), X ) ] )
% 140.73/141.08 , clause( 86315, [ =( X, divide( X, zero ) ) ] )
% 140.73/141.08 , 0, substitution( 0, [ :=( X, X )] )).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 subsumption(
% 140.73/141.08 clause( 129, [ =( divide( X, zero ), X ) ] )
% 140.73/141.08 , clause( 86316, [ =( divide( X, zero ), X ) ] )
% 140.73/141.08 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 140.73/141.08
% 140.73/141.08
% 140.73/141.08 resolution(
% 140.73/141.08 clause( 86317, [ ~( 'less_equal'( zero, XCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------