%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : BOO016-1 : TPTP v8.1.0. Released v1.0.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 14 23:30:40 EDT 2022
% Result : Unsatisfiable 22.84s 23.28s
% Output : Refutation 22.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : BOO016-1 : TPTP v8.1.0. Released v1.0.0.
% 0.12/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 : Wed Jun 1 22:45:56 EDT 2022
% 0.12/0.33 % CPUTime :
% 16.79/17.21 *** allocated 10000 integers for termspace/termends
% 16.79/17.21 *** allocated 10000 integers for clauses
% 16.79/17.21 *** allocated 10000 integers for justifications
% 16.79/17.21 Bliksem 1.12
% 16.79/17.21
% 16.79/17.21
% 16.79/17.21 Automatic Strategy Selection
% 16.79/17.21
% 16.79/17.21 Clauses:
% 16.79/17.21 [
% 16.79/17.21 [ sum( X, Y, add( X, Y ) ) ],
% 16.79/17.21 [ product( X, Y, multiply( X, Y ) ) ],
% 16.79/17.21 [ ~( sum( X, Y, Z ) ), sum( Y, X, Z ) ],
% 16.79/17.21 [ ~( product( X, Y, Z ) ), product( Y, X, Z ) ],
% 16.79/17.21 [ sum( 'additive_identity', X, X ) ],
% 16.79/17.21 [ sum( X, 'additive_identity', X ) ],
% 16.79/17.21 [ product( 'multiplicative_identity', X, X ) ],
% 16.79/17.21 [ product( X, 'multiplicative_identity', X ) ],
% 16.79/17.21 [ ~( product( X, Y, Z ) ), ~( product( X, T, U ) ), ~( sum( Y, T, W ) )
% 16.79/17.21 , ~( product( X, W, V0 ) ), sum( Z, U, V0 ) ],
% 16.79/17.21 [ ~( product( X, Y, Z ) ), ~( product( X, T, U ) ), ~( sum( Y, T, W ) )
% 16.79/17.21 , ~( sum( Z, U, V0 ) ), product( X, W, V0 ) ],
% 16.79/17.21 [ ~( product( X, Y, Z ) ), ~( product( T, Y, U ) ), ~( sum( X, T, W ) )
% 16.79/17.21 , ~( product( W, Y, V0 ) ), sum( Z, U, V0 ) ],
% 16.79/17.21 [ ~( product( X, Y, Z ) ), ~( product( T, Y, U ) ), ~( sum( X, T, W ) )
% 16.79/17.21 , ~( sum( Z, U, V0 ) ), product( W, Y, V0 ) ],
% 16.79/17.21 [ ~( sum( X, Y, Z ) ), ~( sum( X, T, U ) ), ~( product( Y, T, W ) ), ~(
% 16.79/17.21 sum( X, W, V0 ) ), product( Z, U, V0 ) ],
% 16.79/17.21 [ ~( sum( X, Y, Z ) ), ~( sum( X, T, U ) ), ~( product( Y, T, W ) ), ~(
% 16.79/17.21 product( Z, U, V0 ) ), sum( X, W, V0 ) ],
% 16.79/17.21 [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X, T, W ) ), ~(
% 16.79/17.21 sum( W, Y, V0 ) ), product( Z, U, V0 ) ],
% 16.79/17.21 [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X, T, W ) ), ~(
% 16.79/17.21 product( Z, U, V0 ) ), sum( W, Y, V0 ) ],
% 16.79/17.21 [ sum( inverse( X ), X, 'multiplicative_identity' ) ],
% 16.79/17.21 [ sum( X, inverse( X ), 'multiplicative_identity' ) ],
% 16.79/17.21 [ product( inverse( X ), X, 'additive_identity' ) ],
% 16.79/17.21 [ product( X, inverse( X ), 'additive_identity' ) ],
% 16.79/17.21 [ ~( sum( X, Y, Z ) ), ~( sum( X, Y, T ) ), =( Z, T ) ],
% 16.79/17.21 [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z, T ) ],
% 16.79/17.21 [ product( x, y, z ) ],
% 16.79/17.21 [ ~( sum( x, z, x ) ) ]
% 16.79/17.21 ] .
% 16.79/17.21
% 16.79/17.21
% 16.79/17.21 percentage equality = 0.032258, percentage horn = 1.000000
% 16.79/17.21 This is a problem with some equality
% 16.79/17.21
% 16.79/17.21
% 16.79/17.21
% 16.79/17.21 Options Used:
% 16.79/17.21
% 16.79/17.21 useres = 1
% 16.79/17.21 useparamod = 1
% 16.79/17.21 useeqrefl = 1
% 16.79/17.21 useeqfact = 1
% 16.79/17.21 usefactor = 1
% 16.79/17.21 usesimpsplitting = 0
% 16.79/17.21 usesimpdemod = 5
% 16.79/17.21 usesimpres = 3
% 16.79/17.21
% 16.79/17.21 resimpinuse = 1000
% 16.79/17.21 resimpclauses = 20000
% 16.79/17.21 substype = eqrewr
% 16.79/17.21 backwardsubs = 1
% 16.79/17.21 selectoldest = 5
% 16.79/17.21
% 16.79/17.21 litorderings [0] = split
% 16.79/17.21 litorderings [1] = extend the termordering, first sorting on arguments
% 16.79/17.21
% 16.79/17.21 termordering = kbo
% 16.79/17.21
% 16.79/17.21 litapriori = 0
% 16.79/17.21 termapriori = 1
% 16.79/17.21 litaposteriori = 0
% 16.79/17.21 termaposteriori = 0
% 16.79/17.21 demodaposteriori = 0
% 16.79/17.21 ordereqreflfact = 0
% 16.79/17.21
% 16.79/17.21 litselect = negord
% 16.79/17.21
% 16.79/17.21 maxweight = 15
% 16.79/17.21 maxdepth = 30000
% 16.79/17.21 maxlength = 115
% 16.79/17.21 maxnrvars = 195
% 16.79/17.21 excuselevel = 1
% 16.79/17.21 increasemaxweight = 1
% 16.79/17.21
% 16.79/17.21 maxselected = 10000000
% 16.79/17.21 maxnrclauses = 10000000
% 16.79/17.21
% 16.79/17.21 showgenerated = 0
% 16.79/17.21 showkept = 0
% 16.79/17.21 showselected = 0
% 16.79/17.21 showdeleted = 0
% 16.79/17.21 showresimp = 1
% 16.79/17.21 showstatus = 2000
% 16.79/17.21
% 16.79/17.21 prologoutput = 1
% 16.79/17.21 nrgoals = 5000000
% 16.79/17.21 totalproof = 1
% 16.79/17.21
% 16.79/17.21 Symbols occurring in the translation:
% 16.79/17.21
% 16.79/17.21 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 16.79/17.21 . [1, 2] (w:1, o:29, a:1, s:1, b:0),
% 16.79/17.21 ! [4, 1] (w:0, o:23, a:1, s:1, b:0),
% 16.79/17.21 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 16.79/17.21 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 16.79/17.21 add [41, 2] (w:1, o:54, a:1, s:1, b:0),
% 16.79/17.21 sum [42, 3] (w:1, o:56, a:1, s:1, b:0),
% 16.79/17.21 multiply [43, 2] (w:1, o:55, a:1, s:1, b:0),
% 16.79/17.21 product [44, 3] (w:1, o:57, a:1, s:1, b:0),
% 16.79/17.21 'additive_identity' [46, 0] (w:1, o:12, a:1, s:1, b:0),
% 16.79/17.21 'multiplicative_identity' [47, 0] (w:1, o:13, a:1, s:1, b:0),
% 16.79/17.21 inverse [52, 1] (w:1, o:28, a:1, s:1, b:0),
% 16.79/17.21 x [55, 0] (w:1, o:20, a:1, s:1, b:0),
% 16.79/17.21 y [56, 0] (w:1, o:21, a:1, s:1, b:0),
% 16.79/17.21 z [57, 0] (w:1, o:22, a:1, s:1, b:0).
% 16.79/17.21
% 16.79/17.21
% 16.79/17.21 Starting Search:
% 16.79/17.21
% 16.79/17.21 Resimplifying inuse:
% 16.79/17.21 Done
% 16.79/17.21
% 16.79/17.21
% 16.79/17.21 Intermediate Status:
% 16.79/17.21 Generated: 6355
% 16.79/17.21 Kept: 2022
% 16.79/17.21 Inuse: 84
% 16.79/17.21 Deleted: 0
% 16.79/17.21 Deletedinuse: 0
% 16.79/17.21
% 16.79/17.21 Resimplifying inuse:
% 16.79/17.21 Done
% 16.79/17.21
% 16.79/17.21 Resimplifying inuse:
% 16.79/17.21 Done
% 16.79/17.21
% 16.79/17.21
% 16.79/17.21 Intermediate Status:
% 16.79/17.21 Generated: 17534
% 16.79/17.21 Kept: 4038
% 16.79/17.21 Inuse: 170
% 22.84/23.28 Deleted: 1
% 22.84/23.28 Deletedinuse: 1
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 25772
% 22.84/23.28 Kept: 6201
% 22.84/23.28 Inuse: 215
% 22.84/23.28 Deleted: 3
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 31634
% 22.84/23.28 Kept: 8206
% 22.84/23.28 Inuse: 245
% 22.84/23.28 Deleted: 3
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 39895
% 22.84/23.28 Kept: 10206
% 22.84/23.28 Inuse: 292
% 22.84/23.28 Deleted: 3
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 49341
% 22.84/23.28 Kept: 12217
% 22.84/23.28 Inuse: 342
% 22.84/23.28 Deleted: 3
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 62678
% 22.84/23.28 Kept: 14271
% 22.84/23.28 Inuse: 378
% 22.84/23.28 Deleted: 3
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 70344
% 22.84/23.28 Kept: 16395
% 22.84/23.28 Inuse: 410
% 22.84/23.28 Deleted: 3
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 80753
% 22.84/23.28 Kept: 18470
% 22.84/23.28 Inuse: 447
% 22.84/23.28 Deleted: 5
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying clauses:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 89367
% 22.84/23.28 Kept: 20480
% 22.84/23.28 Inuse: 483
% 22.84/23.28 Deleted: 726
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 97889
% 22.84/23.28 Kept: 22521
% 22.84/23.28 Inuse: 515
% 22.84/23.28 Deleted: 726
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 110092
% 22.84/23.28 Kept: 24573
% 22.84/23.28 Inuse: 564
% 22.84/23.28 Deleted: 726
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 125644
% 22.84/23.28 Kept: 27019
% 22.84/23.28 Inuse: 597
% 22.84/23.28 Deleted: 726
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 140308
% 22.84/23.28 Kept: 29031
% 22.84/23.28 Inuse: 641
% 22.84/23.28 Deleted: 726
% 22.84/23.28 Deletedinuse: 2
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 155407
% 22.84/23.28 Kept: 31104
% 22.84/23.28 Inuse: 690
% 22.84/23.28 Deleted: 728
% 22.84/23.28 Deletedinuse: 4
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 164421
% 22.84/23.28 Kept: 33190
% 22.84/23.28 Inuse: 718
% 22.84/23.28 Deleted: 730
% 22.84/23.28 Deletedinuse: 6
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 172873
% 22.84/23.28 Kept: 35229
% 22.84/23.28 Inuse: 744
% 22.84/23.28 Deleted: 731
% 22.84/23.28 Deletedinuse: 7
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 180222
% 22.84/23.28 Kept: 37235
% 22.84/23.28 Inuse: 774
% 22.84/23.28 Deleted: 774
% 22.84/23.28 Deletedinuse: 50
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 187734
% 22.84/23.28 Kept: 39236
% 22.84/23.28 Inuse: 805
% 22.84/23.28 Deleted: 807
% 22.84/23.28 Deletedinuse: 83
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying clauses:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 194067
% 22.84/23.28 Kept: 41239
% 22.84/23.28 Inuse: 833
% 22.84/23.28 Deleted: 12461
% 22.84/23.28 Deletedinuse: 214
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 201052
% 22.84/23.28 Kept: 43308
% 22.84/23.28 Inuse: 865
% 22.84/23.28 Deleted: 12494
% 22.84/23.28 Deletedinuse: 245
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 209678
% 22.84/23.28 Kept: 45466
% 22.84/23.28 Inuse: 885
% 22.84/23.28 Deleted: 12502
% 22.84/23.28 Deletedinuse: 253
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 217122
% 22.84/23.28 Kept: 47566
% 22.84/23.28 Inuse: 902
% 22.84/23.28 Deleted: 12579
% 22.84/23.28 Deletedinuse: 323
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 226094
% 22.84/23.28 Kept: 49815
% 22.84/23.28 Inuse: 908
% 22.84/23.28 Deleted: 12579
% 22.84/23.28 Deletedinuse: 323
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 237074
% 22.84/23.28 Kept: 51863
% 22.84/23.28 Inuse: 925
% 22.84/23.28 Deleted: 12579
% 22.84/23.28 Deletedinuse: 323
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 243175
% 22.84/23.28 Kept: 54375
% 22.84/23.28 Inuse: 934
% 22.84/23.28 Deleted: 12585
% 22.84/23.28 Deletedinuse: 329
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 252028
% 22.84/23.28 Kept: 56520
% 22.84/23.28 Inuse: 948
% 22.84/23.28 Deleted: 12589
% 22.84/23.28 Deletedinuse: 332
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 257825
% 22.84/23.28 Kept: 58530
% 22.84/23.28 Inuse: 964
% 22.84/23.28 Deleted: 12593
% 22.84/23.28 Deletedinuse: 334
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28 Resimplifying clauses:
% 22.84/23.28 Done
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 Intermediate Status:
% 22.84/23.28 Generated: 270918
% 22.84/23.28 Kept: 60595
% 22.84/23.28 Inuse: 984
% 22.84/23.28 Deleted: 22680
% 22.84/23.28 Deletedinuse: 335
% 22.84/23.28
% 22.84/23.28 Resimplifying inuse:
% 22.84/23.28
% 22.84/23.28 Bliksems!, er is een bewijs:
% 22.84/23.28 % SZS status Unsatisfiable
% 22.84/23.28 % SZS output start Refutation
% 22.84/23.28
% 22.84/23.28 clause( 0, [ sum( X, Y, add( X, Y ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 1, [ product( X, Y, multiply( X, Y ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 2, [ ~( sum( X, Y, Z ) ), sum( Y, X, Z ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 3, [ ~( product( X, Y, Z ) ), product( Y, X, Z ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 4, [ sum( 'additive_identity', X, X ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 5, [ sum( X, 'additive_identity', X ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 6, [ product( 'multiplicative_identity', X, X ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 7, [ product( X, 'multiplicative_identity', X ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 8, [ ~( product( X, Y, Z ) ), ~( product( X, T, U ) ), ~( sum( Y, T
% 22.84/23.28 , W ) ), ~( product( X, W, V0 ) ), sum( Z, U, V0 ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 14, [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X, T, W
% 22.84/23.28 ) ), ~( sum( W, Y, V0 ) ), product( Z, U, V0 ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 19, [ product( X, inverse( X ), 'additive_identity' ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 20, [ ~( sum( X, Y, Z ) ), ~( sum( X, Y, T ) ), =( Z, T ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 21, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z, T ) ]
% 22.84/23.28 )
% 22.84/23.28 .
% 22.84/23.28 clause( 22, [ product( x, y, z ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 23, [ ~( sum( x, z, x ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 47, [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X, T, T
% 22.84/23.28 ) ), product( Z, U, U ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 52, [ product( X, Y, multiply( Y, X ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 54, [ sum( X, Y, add( Y, X ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 63, [ ~( product( 'multiplicative_identity', X, Y ) ), =( X, Y ) ]
% 22.84/23.28 )
% 22.84/23.28 .
% 22.84/23.28 clause( 92, [ =( multiply( 'multiplicative_identity', X ), X ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 98, [ sum( Y, X, Z ), ~( product( 'multiplicative_identity', Z, add(
% 22.84/23.28 X, Y ) ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 104, [ product( Y, X, Z ), ~( product( 'multiplicative_identity', Z
% 22.84/23.28 , multiply( X, Y ) ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 168, [ ~( product( x, X, Y ) ), ~( sum( X, y, Z ) ), ~( product( x
% 22.84/23.28 , Z, T ) ), sum( Y, z, T ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 172, [ ~( product( X, 'additive_identity', Y ) ), ~( product( X, Z
% 22.84/23.28 , T ) ), ~( product( X, Z, U ) ), sum( Y, T, U ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 190, [ ~( product( X, 'additive_identity', Y ) ), ~( product( X, Z
% 22.84/23.28 , T ) ), sum( Y, T, T ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 194, [ ~( product( x, X, Y ) ), ~( sum( X, y, X ) ), sum( Y, z, Y )
% 22.84/23.28 ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 1120, [ ~( sum( X, 'additive_identity', Y ) ), =( X, Y ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 4306, [ ~( sum( X, Y, Z ) ), ~( product( X, 'additive_identity',
% 22.84/23.28 'additive_identity' ) ), product( Z, Y, Y ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 16391, [ product( X, 'multiplicative_identity', Y ), ~( product(
% 22.84/23.28 'multiplicative_identity', Y, X ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 16461, [ product( X, 'multiplicative_identity', Y ), ~( product( Y
% 22.84/23.28 , 'multiplicative_identity', X ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 16535, [ ~( product( X, 'multiplicative_identity', Y ) ), product(
% 22.84/23.28 'multiplicative_identity', Y, X ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 38101, [ ~( product( X, 'additive_identity', Y ) ), sum( Y,
% 22.84/23.28 'additive_identity', 'additive_identity' ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 38538, [ sum( multiply( 'additive_identity', X ),
% 22.84/23.28 'additive_identity', 'additive_identity' ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 39350, [ ~( sum( 'multiplicative_identity', y,
% 22.84/23.28 'multiplicative_identity' ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 39362, [ ~( product( 'multiplicative_identity',
% 22.84/23.28 'multiplicative_identity', add( y, 'multiplicative_identity' ) ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 44220, [ =( multiply( 'additive_identity', X ), 'additive_identity'
% 22.84/23.28 ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 44264, [ product( X, 'additive_identity', 'additive_identity' ) ]
% 22.84/23.28 )
% 22.84/23.28 .
% 22.84/23.28 clause( 49819, [ ~( product( add( y, 'multiplicative_identity' ),
% 22.84/23.28 'multiplicative_identity', 'multiplicative_identity' ) ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 60255, [ ~( sum( X, Y, Z ) ), product( Z, Y, Y ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 60593, [ product( add( X, Y ), Y, Y ) ] )
% 22.84/23.28 .
% 22.84/23.28 clause( 60650, [] )
% 22.84/23.28 .
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 % SZS output end Refutation
% 22.84/23.28 found a proof!
% 22.84/23.28
% 22.84/23.28 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 22.84/23.28
% 22.84/23.28 initialclauses(
% 22.84/23.28 [ clause( 60652, [ sum( X, Y, add( X, Y ) ) ] )
% 22.84/23.28 , clause( 60653, [ product( X, Y, multiply( X, Y ) ) ] )
% 22.84/23.28 , clause( 60654, [ ~( sum( X, Y, Z ) ), sum( Y, X, Z ) ] )
% 22.84/23.28 , clause( 60655, [ ~( product( X, Y, Z ) ), product( Y, X, Z ) ] )
% 22.84/23.28 , clause( 60656, [ sum( 'additive_identity', X, X ) ] )
% 22.84/23.28 , clause( 60657, [ sum( X, 'additive_identity', X ) ] )
% 22.84/23.28 , clause( 60658, [ product( 'multiplicative_identity', X, X ) ] )
% 22.84/23.28 , clause( 60659, [ product( X, 'multiplicative_identity', X ) ] )
% 22.84/23.28 , clause( 60660, [ ~( product( X, Y, Z ) ), ~( product( X, T, U ) ), ~( sum(
% 22.84/23.28 Y, T, W ) ), ~( product( X, W, V0 ) ), sum( Z, U, V0 ) ] )
% 22.84/23.28 , clause( 60661, [ ~( product( X, Y, Z ) ), ~( product( X, T, U ) ), ~( sum(
% 22.84/23.28 Y, T, W ) ), ~( sum( Z, U, V0 ) ), product( X, W, V0 ) ] )
% 22.84/23.28 , clause( 60662, [ ~( product( X, Y, Z ) ), ~( product( T, Y, U ) ), ~( sum(
% 22.84/23.28 X, T, W ) ), ~( product( W, Y, V0 ) ), sum( Z, U, V0 ) ] )
% 22.84/23.28 , clause( 60663, [ ~( product( X, Y, Z ) ), ~( product( T, Y, U ) ), ~( sum(
% 22.84/23.28 X, T, W ) ), ~( sum( Z, U, V0 ) ), product( W, Y, V0 ) ] )
% 22.84/23.28 , clause( 60664, [ ~( sum( X, Y, Z ) ), ~( sum( X, T, U ) ), ~( product( Y
% 22.84/23.28 , T, W ) ), ~( sum( X, W, V0 ) ), product( Z, U, V0 ) ] )
% 22.84/23.28 , clause( 60665, [ ~( sum( X, Y, Z ) ), ~( sum( X, T, U ) ), ~( product( Y
% 22.84/23.28 , T, W ) ), ~( product( Z, U, V0 ) ), sum( X, W, V0 ) ] )
% 22.84/23.28 , clause( 60666, [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X
% 22.84/23.28 , T, W ) ), ~( sum( W, Y, V0 ) ), product( Z, U, V0 ) ] )
% 22.84/23.28 , clause( 60667, [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X
% 22.84/23.28 , T, W ) ), ~( product( Z, U, V0 ) ), sum( W, Y, V0 ) ] )
% 22.84/23.28 , clause( 60668, [ sum( inverse( X ), X, 'multiplicative_identity' ) ] )
% 22.84/23.28 , clause( 60669, [ sum( X, inverse( X ), 'multiplicative_identity' ) ] )
% 22.84/23.28 , clause( 60670, [ product( inverse( X ), X, 'additive_identity' ) ] )
% 22.84/23.28 , clause( 60671, [ product( X, inverse( X ), 'additive_identity' ) ] )
% 22.84/23.28 , clause( 60672, [ ~( sum( X, Y, Z ) ), ~( sum( X, Y, T ) ), =( Z, T ) ] )
% 22.84/23.28 , clause( 60673, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z,
% 22.84/23.28 T ) ] )
% 22.84/23.28 , clause( 60674, [ product( x, y, z ) ] )
% 22.84/23.28 , clause( 60675, [ ~( sum( x, z, x ) ) ] )
% 22.84/23.28 ] ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 0, [ sum( X, Y, add( X, Y ) ) ] )
% 22.84/23.28 , clause( 60652, [ sum( X, Y, add( X, Y ) ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 22.84/23.28 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 1, [ product( X, Y, multiply( X, Y ) ) ] )
% 22.84/23.28 , clause( 60653, [ product( X, Y, multiply( X, Y ) ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 22.84/23.28 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 2, [ ~( sum( X, Y, Z ) ), sum( Y, X, Z ) ] )
% 22.84/23.28 , clause( 60654, [ ~( sum( X, Y, Z ) ), sum( Y, X, Z ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 22.84/23.28 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 3, [ ~( product( X, Y, Z ) ), product( Y, X, Z ) ] )
% 22.84/23.28 , clause( 60655, [ ~( product( X, Y, Z ) ), product( Y, X, Z ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 22.84/23.28 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 4, [ sum( 'additive_identity', X, X ) ] )
% 22.84/23.28 , clause( 60656, [ sum( 'additive_identity', X, X ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 5, [ sum( X, 'additive_identity', X ) ] )
% 22.84/23.28 , clause( 60657, [ sum( X, 'additive_identity', X ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 6, [ product( 'multiplicative_identity', X, X ) ] )
% 22.84/23.28 , clause( 60658, [ product( 'multiplicative_identity', X, X ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 7, [ product( X, 'multiplicative_identity', X ) ] )
% 22.84/23.28 , clause( 60659, [ product( X, 'multiplicative_identity', X ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 8, [ ~( product( X, Y, Z ) ), ~( product( X, T, U ) ), ~( sum( Y, T
% 22.84/23.28 , W ) ), ~( product( X, W, V0 ) ), sum( Z, U, V0 ) ] )
% 22.84/23.28 , clause( 60660, [ ~( product( X, Y, Z ) ), ~( product( X, T, U ) ), ~( sum(
% 22.84/23.28 Y, T, W ) ), ~( product( X, W, V0 ) ), sum( Z, U, V0 ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 22.84/23.28 , U ), :=( W, W ), :=( V0, V0 )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1
% 22.84/23.28 , 1 ), ==>( 2, 2 ), ==>( 3, 3 ), ==>( 4, 4 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 14, [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X, T, W
% 22.84/23.28 ) ), ~( sum( W, Y, V0 ) ), product( Z, U, V0 ) ] )
% 22.84/23.28 , clause( 60666, [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X
% 22.84/23.28 , T, W ) ), ~( sum( W, Y, V0 ) ), product( Z, U, V0 ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 22.84/23.28 , U ), :=( W, W ), :=( V0, V0 )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1
% 22.84/23.28 , 1 ), ==>( 2, 2 ), ==>( 3, 3 ), ==>( 4, 4 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 19, [ product( X, inverse( X ), 'additive_identity' ) ] )
% 22.84/23.28 , clause( 60671, [ product( X, inverse( X ), 'additive_identity' ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 20, [ ~( sum( X, Y, Z ) ), ~( sum( X, Y, T ) ), =( Z, T ) ] )
% 22.84/23.28 , clause( 60672, [ ~( sum( X, Y, Z ) ), ~( sum( X, Y, T ) ), =( Z, T ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 22.84/23.28 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 21, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z, T ) ]
% 22.84/23.28 )
% 22.84/23.28 , clause( 60673, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z,
% 22.84/23.28 T ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 22.84/23.28 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 22, [ product( x, y, z ) ] )
% 22.84/23.28 , clause( 60674, [ product( x, y, z ) ] )
% 22.84/23.28 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 23, [ ~( sum( x, z, x ) ) ] )
% 22.84/23.28 , clause( 60675, [ ~( sum( x, z, x ) ) ] )
% 22.84/23.28 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 factor(
% 22.84/23.28 clause( 60854, [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X, T
% 22.84/23.28 , T ) ), product( Z, U, U ) ] )
% 22.84/23.28 , clause( 14, [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X, T
% 22.84/23.28 , W ) ), ~( sum( W, Y, V0 ) ), product( Z, U, V0 ) ] )
% 22.84/23.28 , 1, 3, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ),
% 22.84/23.28 :=( U, U ), :=( W, T ), :=( V0, U )] )).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 47, [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X, T, T
% 22.84/23.28 ) ), product( Z, U, U ) ] )
% 22.84/23.28 , clause( 60854, [ ~( sum( X, Y, Z ) ), ~( sum( T, Y, U ) ), ~( product( X
% 22.84/23.28 , T, T ) ), product( Z, U, U ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 22.84/23.28 , U )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3
% 22.84/23.28 , 3 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 resolution(
% 22.84/23.28 clause( 60856, [ product( Y, X, multiply( X, Y ) ) ] )
% 22.84/23.28 , clause( 3, [ ~( product( X, Y, Z ) ), product( Y, X, Z ) ] )
% 22.84/23.28 , 0, clause( 1, [ product( X, Y, multiply( X, Y ) ) ] )
% 22.84/23.28 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, multiply( X, Y ) )] )
% 22.84/23.28 , substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 52, [ product( X, Y, multiply( Y, X ) ) ] )
% 22.84/23.28 , clause( 60856, [ product( Y, X, multiply( X, Y ) ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 22.84/23.28 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 resolution(
% 22.84/23.28 clause( 60857, [ sum( Y, X, add( X, Y ) ) ] )
% 22.84/23.28 , clause( 2, [ ~( sum( X, Y, Z ) ), sum( Y, X, Z ) ] )
% 22.84/23.28 , 0, clause( 0, [ sum( X, Y, add( X, Y ) ) ] )
% 22.84/23.28 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, add( X, Y ) )] ),
% 22.84/23.28 substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 subsumption(
% 22.84/23.28 clause( 54, [ sum( X, Y, add( Y, X ) ) ] )
% 22.84/23.28 , clause( 60857, [ sum( Y, X, add( X, Y ) ) ] )
% 22.84/23.28 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 22.84/23.28 )] ) ).
% 22.84/23.28
% 22.84/23.28
% 22.84/23.28 resolution(
% 22.84/23.28 clause( 60858, [ ~( product( 'multiplicative_identity', X, Y ) ), =( X, Y )
% 22.84/23.28 ] )
% 22.84/23.28 , clause( 21, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z, T )
% 22.84/23.28 ] )
% 22.84/23.28 , 0, clause( 6, [ product( 'multiplicative_identity', X, X ) ] )
% 22.84/23.28 , 0, substitution( 0, [ :=( X, 'multiplicative_identity' ), :=( Y, X ),
% 22.84/23.28 :=(Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------