%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX195-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n029.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 : Tue May 5 06:56:46 PM UTC 2026
% Result : Timeout 299.36s 300.01s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX195-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.16/0.33 % Computer : n029.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.34 % DateTime : Tue May 5 10:56:44 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.72/1.12 *** allocated 10000 integers for termspace/termends
% 0.72/1.12 *** allocated 10000 integers for clauses
% 0.72/1.12 *** allocated 10000 integers for justifications
% 0.72/1.12 Bliksem 1.12
% 0.72/1.12
% 0.72/1.12
% 0.72/1.12 Automatic Strategy Selection
% 0.72/1.12
% 0.72/1.12 Clauses:
% 0.72/1.12 [
% 0.72/1.12 [ =( aux( X, Y, btrue ), mul( n( suc( suc( zero ) ) ), X ) ) ],
% 0.72/1.12 [ =( aux( add( X, Y ), Z, bfalse ), add( X, add( Y, Z ) ) ) ],
% 0.72/1.12 [ =( aux( n( X ), Y, bfalse ), add( n( X ), Y ) ) ],
% 0.72/1.12 [ =( aux( mul( X, Y ), Z, bfalse ), add( mul( X, Y ), Z ) ) ],
% 0.72/1.12 [ =( aux( eq( X, Y ), Z, bfalse ), add( eq( X, Y ), Z ) ) ],
% 0.72/1.12 [ =( aux( v( X ), Y, bfalse ), add( v( X ), Y ) ) ],
% 0.72/1.12 [ =( aux2( X, Y, btrue ), mul( n( suc( suc( zero ) ) ), X ) ) ],
% 0.72/1.12 [ =( aux2( add( X, Y ), Z, bfalse ), add( X, add( Y, Z ) ) ) ],
% 0.72/1.12 [ =( aux2( n( X ), Y, bfalse ), add( n( X ), Y ) ) ],
% 0.72/1.12 [ =( aux2( mul( X, Y ), Z, bfalse ), add( mul( X, Y ), Z ) ) ],
% 0.72/1.12 [ =( aux2( eq( X, Y ), Z, bfalse ), add( eq( X, Y ), Z ) ) ],
% 0.72/1.12 [ =( aux2( v( X ), Y, bfalse ), add( v( X ), Y ) ) ],
% 0.72/1.12 [ =( aux3( X, Y, btrue ), n( suc( zero ) ) ) ],
% 0.72/1.12 [ =( aux3( X, Y, bfalse ), eq( X, Y ) ) ],
% 0.72/1.12 [ =( aux4( X, Y, n( zero ) ), b( Y ) ) ],
% 0.72/1.12 [ =( aux4( X, Y, n( suc( Z ) ) ), fail4( y( X ), b( Y ) ) ) ],
% 0.72/1.12 [ =( aux4( X, Y, add( Z, T ) ), fail4( y( X ), b( Y ) ) ) ],
% 0.72/1.12 [ =( aux4( X, Y, mul( Z, T ) ), fail4( y( X ), b( Y ) ) ) ],
% 0.72/1.12 [ =( aux4( X, Y, eq( Z, T ) ), fail4( y( X ), b( Y ) ) ) ],
% 0.72/1.12 [ =( aux4( X, Y, v( Z ) ), fail4( y( X ), b( Y ) ) ) ],
% 0.72/1.12 [ =( aux5( X, Y, n( zero ) ), n( zero ) ) ],
% 0.72/1.12 [ =( aux5( X, Y, n( suc( Z ) ) ), fail23( x5( X ), b2( Y ) ) ) ],
% 0.72/1.12 [ =( aux5( X, Y, add( Z, T ) ), fail23( x5( X ), b2( Y ) ) ) ],
% 0.72/1.12 [ =( aux5( X, Y, mul( Z, T ) ), fail23( x5( X ), b2( Y ) ) ) ],
% 0.72/1.12 [ =( aux5( X, Y, eq( Z, T ) ), fail23( x5( X ), b2( Y ) ) ) ],
% 0.72/1.12 [ =( aux5( X, Y, v( Z ) ), fail23( x5( X ), b2( Y ) ) ) ],
% 0.72/1.12 [ =( aux6( X, Y, btrue ), n( suc( zero ) ) ) ],
% 0.72/1.12 [ =( aux6( X, Y, bfalse ), eq( a3( X ), b3( Y ) ) ) ],
% 0.72/1.12 [ =( aux7( X, Y, Z, btrue ), suc( zero ) ) ],
% 0.72/1.12 [ =( aux7( X, Y, Z, bfalse ), zero ) ],
% 0.72/1.12 [ =( fail1( X, Y ), aux( X, Y, eq3( X, Y ) ) ) ],
% 0.72/1.12 [ =( fail( X, n( zero ) ), X ) ],
% 0.72/1.12 [ =( fail( X, n( suc( Y ) ) ), fail1( X, n( suc( Y ) ) ) ) ],
% 0.72/1.12 [ =( fail( X, add( Y, Z ) ), fail1( X, add( Y, Z ) ) ) ],
% 0.72/1.12 [ =( fail( X, mul( Y, Z ) ), fail1( X, mul( Y, Z ) ) ) ],
% 0.72/1.12 [ =( fail( X, eq( Y, Z ) ), fail1( X, eq( Y, Z ) ) ) ],
% 0.72/1.12 [ =( fail( X, v( Y ) ), fail1( X, v( Y ) ) ) ],
% 0.72/1.12 [ =( fail3( mul( X, Y ), Z ), mul( X, mul( Y, Z ) ) ) ],
% 0.72/1.12 [ =( fail3( n( X ), Y ), mul( n( X ), Y ) ) ],
% 0.72/1.12 [ =( fail3( add( X, Y ), Z ), mul( add( X, Y ), Z ) ) ],
% 0.72/1.12 [ =( fail3( eq( X, Y ), Z ), mul( eq( X, Y ), Z ) ) ],
% 0.72/1.12 [ =( fail3( v( X ), Y ), mul( v( X ), Y ) ) ],
% 0.72/1.12 [ =( fail22( X, n( zero ) ), fail3( X, n( zero ) ) ) ],
% 0.72/1.12 [ =( fail22( X, n( suc( zero ) ) ), X ) ],
% 0.72/1.12 [ =( fail22( X, n( suc( suc( Y ) ) ) ), fail3( X, n( suc( suc( Y ) ) ) )
% 0.72/1.12 ) ],
% 0.72/1.12 [ =( fail22( X, add( Y, Z ) ), fail3( X, add( Y, Z ) ) ) ],
% 0.72/1.12 [ =( fail22( X, mul( Y, Z ) ), fail3( X, mul( Y, Z ) ) ) ],
% 0.72/1.12 [ =( fail22( X, eq( Y, Z ) ), fail3( X, eq( Y, Z ) ) ) ],
% 0.72/1.12 [ =( fail22( X, v( Y ) ), fail3( X, v( Y ) ) ) ],
% 0.75/1.12 [ =( fail12( n( zero ), X ), fail22( n( zero ), X ) ) ],
% 0.75/1.12 [ =( fail12( n( suc( zero ) ), X ), X ) ],
% 0.75/1.12 [ =( fail12( n( suc( suc( X ) ) ), Y ), fail22( n( suc( suc( X ) ) ), Y
% 0.75/1.12 ) ) ],
% 0.75/1.12 [ =( fail12( add( X, Y ), Z ), fail22( add( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( fail12( mul( X, Y ), Z ), fail22( mul( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( fail12( eq( X, Y ), Z ), fail22( eq( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( fail12( v( X ), Y ), fail22( v( X ), Y ) ) ],
% 0.75/1.12 [ =( fail2( X, n( zero ) ), n( zero ) ) ],
% 0.75/1.12 [ =( fail2( X, n( suc( Y ) ) ), fail12( X, n( suc( Y ) ) ) ) ],
% 0.75/1.12 [ =( fail2( X, add( Y, Z ) ), fail12( X, add( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail2( X, mul( Y, Z ) ), fail12( X, mul( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail2( X, eq( Y, Z ) ), fail12( X, eq( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail2( X, v( Y ) ), fail12( X, v( Y ) ) ) ],
% 0.75/1.12 [ =( fail13( X, Y ), aux2( X, Y, eq3( X, Y ) ) ) ],
% 0.75/1.12 [ =( fail4( X, n( zero ) ), X ) ],
% 0.75/1.12 [ =( fail4( X, n( suc( Y ) ) ), fail13( X, n( suc( Y ) ) ) ) ],
% 0.75/1.12 [ =( fail4( X, add( Y, Z ) ), fail13( X, add( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail4( X, mul( Y, Z ) ), fail13( X, mul( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail4( X, eq( Y, Z ) ), fail13( X, eq( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail4( X, v( Y ) ), fail13( X, v( Y ) ) ) ],
% 0.75/1.12 [ =( b( X ), simp2( X ) ) ],
% 0.75/1.12 [ =( y( X ), simp2( X ) ) ],
% 0.75/1.12 [ =( fail32( mul( X, Y ), Z ), mul( X, mul( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail32( n( X ), Y ), mul( n( X ), Y ) ) ],
% 0.75/1.12 [ =( fail32( add( X, Y ), Z ), mul( add( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( fail32( eq( X, Y ), Z ), mul( eq( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( fail32( v( X ), Y ), mul( v( X ), Y ) ) ],
% 0.75/1.12 [ =( fail222( X, n( zero ) ), fail32( X, n( zero ) ) ) ],
% 0.75/1.12 [ =( fail222( X, n( suc( zero ) ) ), X ) ],
% 0.75/1.12 [ =( fail222( X, n( suc( suc( Y ) ) ) ), fail32( X, n( suc( suc( Y ) ) )
% 0.75/1.12 ) ) ],
% 0.75/1.12 [ =( fail222( X, add( Y, Z ) ), fail32( X, add( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail222( X, mul( Y, Z ) ), fail32( X, mul( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail222( X, eq( Y, Z ) ), fail32( X, eq( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail222( X, v( Y ) ), fail32( X, v( Y ) ) ) ],
% 0.75/1.12 [ =( fail122( n( zero ), X ), fail222( n( zero ), X ) ) ],
% 0.75/1.12 [ =( fail122( n( suc( zero ) ), X ), X ) ],
% 0.75/1.12 [ =( fail122( n( suc( suc( X ) ) ), Y ), fail222( n( suc( suc( X ) ) ),
% 0.75/1.12 Y ) ) ],
% 0.75/1.12 [ =( fail122( add( X, Y ), Z ), fail222( add( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( fail122( mul( X, Y ), Z ), fail222( mul( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( fail122( eq( X, Y ), Z ), fail222( eq( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( fail122( v( X ), Y ), fail222( v( X ), Y ) ) ],
% 0.75/1.12 [ =( fail23( X, n( zero ) ), n( zero ) ) ],
% 0.75/1.12 [ =( fail23( X, n( suc( Y ) ) ), fail122( X, n( suc( Y ) ) ) ) ],
% 0.75/1.12 [ =( fail23( X, add( Y, Z ) ), fail122( X, add( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail23( X, mul( Y, Z ) ), fail122( X, mul( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail23( X, eq( Y, Z ) ), fail122( X, eq( Y, Z ) ) ) ],
% 0.75/1.12 [ =( fail23( X, v( Y ) ), fail122( X, v( Y ) ) ) ],
% 0.75/1.12 [ =( b2( X ), simp2( X ) ) ],
% 0.75/1.12 [ =( x5( X ), simp2( X ) ) ],
% 0.75/1.12 [ =( b3( X ), simp2( X ) ) ],
% 0.75/1.12 [ =( a3( X ), simp2( X ) ) ],
% 0.75/1.12 [ =( step2( add( n( zero ), X ) ), X ) ],
% 0.75/1.12 [ =( step2( add( n( suc( X ) ), Y ) ), fail( n( suc( X ) ), Y ) ) ],
% 0.75/1.12 [ =( step2( add( add( X, Y ), Z ) ), fail( add( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( step2( add( mul( X, Y ), Z ) ), fail( mul( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( step2( add( eq( X, Y ), Z ) ), fail( eq( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( step2( add( v( X ), Y ) ), fail( v( X ), Y ) ) ],
% 0.75/1.12 [ =( step2( mul( n( zero ), X ) ), n( zero ) ) ],
% 0.75/1.12 [ =( step2( mul( n( suc( X ) ), Y ) ), fail2( n( suc( X ) ), Y ) ) ]
% 0.75/1.12 ,
% 0.75/1.12 [ =( step2( mul( add( X, Y ), Z ) ), fail2( add( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( step2( mul( mul( X, Y ), Z ) ), fail2( mul( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( step2( mul( eq( X, Y ), Z ) ), fail2( eq( X, Y ), Z ) ) ],
% 0.75/1.12 [ =( step2( mul( v( X ), Y ) ), fail2( v( X ), Y ) ) ],
% 0.75/1.12 [ =( step2( eq( X, Y ) ), aux3( X, Y, eq3( X, Y ) ) ) ],
% 0.75/1.12 [ =( step2( n( X ) ), n( X ) ) ],
% 0.75/1.12 [ =( step2( v( X ) ), v( X ) ) ],
% 0.75/1.12 [ =( simp2( add( X, Y ) ), aux4( X, Y, y( X ) ) ) ],
% 0.75/1.12 [ =( simp2( mul( X, Y ) ), aux5( X, Y, x5( X ) ) ) ],
% 0.75/1.12 [ =( simp2( eq( X, Y ) ), aux6( X, Y, eq3( a3( X ), b3( Y ) ) ) ) ],
% 0.75/1.12 [ =( simp2( n( X ) ), n( X ) ) ],
% 0.75/1.12 [ =( simp2( v( X ) ), v( X ) ) ],
% 0.75/1.12 [ =( fetch( nil, X ), zero ) ],
% 0.75/1.12 [ =( fetch( cons( X, Y ), zero ), X ) ],
% 0.75/1.12 [ =( fetch( cons( X, Y ), suc( Z ) ), fetch( Y, Z ) ) ],
% 0.75/1.12 [ =( addNat( zero, X ), X ) ],
% 0.75/1.12 [ =( addNat( suc( X ), Y ), suc( addNat( X, Y ) ) ) ],
% 0.75/1.12 [ =( mulNat( zero, X ), zero ) ],
% 0.75/1.12 [ =( mulNat( suc( X ), Y ), addNat( Y, mulNat( X, Y ) ) ) ],
% 0.75/1.12 [ =( eval( X, n( Y ) ), Y ) ],
% 0.75/1.12 [ =( eval( X, add( Y, Z ) ), addNat( eval( X, Y ), eval( X, Z ) ) ) ]
% 0.75/1.12 ,
% 0.75/1.12 [ =( eval( X, mul( Y, Z ) ), mulNat( eval( X, Y ), eval( X, Z ) ) ) ]
% 0.75/1.12 ,
% 0.75/1.12 [ =( eval( X, eq( Y, Z ) ), aux7( X, Y, Z, eq2( eval( X, Y ), eval( X, Z
% 0.75/1.12 ) ) ) ) ],
% 0.75/1.12 [ =( eval( X, v( Y ) ), fetch( X, Y ) ) ],
% 0.75/1.12 [ =( prop2( X, Y ), eq4( eq2( eval( X, Y ), eval( X, simp2( Y ) ) ),
% 0.75/1.12 btrue ) ) ],
% 0.75/1.12 [ =( eq4( bfalse, btrue ), bfalse ) ],
% 0.75/1.12 [ =( eq4( btrue, bfalse ), bfalse ) ],
% 0.75/1.12 [ =( eq3( n( X ), n( Y ) ), eq2( X, Y ) ) ],
% 0.75/1.12 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( add( X, Z ), add( Y, T ) ),
% 0.75/1.12 bfalse ) ],
% 0.75/1.12 [ ~( =( eq3( X, Y ), btrue ) ), =( eq3( add( X, Z ), add( Y, T ) ), eq3(
% 28.22/28.69 Z, T ) ) ],
% 28.22/28.69 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( mul( X, Z ), mul( Y, T ) ),
% 28.22/28.69 bfalse ) ],
% 28.22/28.69 [ ~( =( eq3( X, Y ), btrue ) ), =( eq3( mul( X, Z ), mul( Y, T ) ), eq3(
% 28.22/28.69 Z, T ) ) ],
% 28.22/28.69 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( eq( X, Z ), eq( Y, T ) ),
% 28.22/28.69 bfalse ) ],
% 28.22/28.69 [ ~( =( eq3( X, Y ), btrue ) ), =( eq3( eq( X, Z ), eq( Y, T ) ), eq3( Z
% 28.22/28.69 , T ) ) ],
% 28.22/28.69 [ =( eq3( v( X ), v( Y ) ), eq2( X, Y ) ) ],
% 28.22/28.69 [ =( eq3( n( X ), add( Y, Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( n( X ), mul( Y, Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( n( X ), eq( Y, Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( n( X ), v( Y ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( add( X, Y ), n( Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( add( X, Y ), mul( Z, T ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( add( X, Y ), eq( Z, T ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( add( X, Y ), v( Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( mul( X, Y ), n( Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( mul( X, Y ), add( Z, T ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( mul( X, Y ), eq( Z, T ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( mul( X, Y ), v( Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( eq( X, Y ), n( Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( eq( X, Y ), add( Z, T ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( eq( X, Y ), mul( Z, T ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( eq( X, Y ), v( Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( v( X ), n( Y ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( v( X ), add( Y, Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( v( X ), mul( Y, Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq3( v( X ), eq( Y, Z ) ), bfalse ) ],
% 28.22/28.69 [ =( eq2( suc( X ), suc( Y ) ), eq2( X, Y ) ) ],
% 28.22/28.69 [ =( eq2( zero, suc( X ) ), bfalse ) ],
% 28.22/28.69 [ =( eq2( suc( X ), zero ), bfalse ) ],
% 28.22/28.69 [ =( eq2( X, X ), btrue ) ],
% 28.22/28.69 [ =( eq3( X, X ), btrue ) ],
% 28.22/28.69 [ =( eq4( X, X ), btrue ) ],
% 28.22/28.69 [ ~( =( eq4( prop2( X, Y ), bfalse ), btrue ) ) ]
% 28.22/28.69 ] .
% 28.22/28.69
% 28.22/28.69
% 28.22/28.69 percentage equality = 1.000000, percentage horn = 1.000000
% 28.22/28.69 This is a pure equality problem
% 28.22/28.69
% 28.22/28.69
% 28.22/28.69
% 28.22/28.69 Options Used:
% 28.22/28.69
% 28.22/28.69 useres = 1
% 28.22/28.69 useparamod = 1
% 28.22/28.69 useeqrefl = 1
% 28.22/28.69 useeqfact = 1
% 28.22/28.69 usefactor = 1
% 28.22/28.69 usesimpsplitting = 0
% 28.22/28.69 usesimpdemod = 5
% 28.22/28.69 usesimpres = 3
% 28.22/28.69
% 28.22/28.69 resimpinuse = 1000
% 28.22/28.69 resimpclauses = 20000
% 28.22/28.69 substype = eqrewr
% 28.22/28.69 backwardsubs = 1
% 28.22/28.69 selectoldest = 5
% 28.22/28.69
% 28.22/28.69 litorderings [0] = split
% 28.22/28.69 litorderings [1] = extend the termordering, first sorting on arguments
% 28.22/28.69
% 28.22/28.69 termordering = kbo
% 28.22/28.69
% 28.22/28.69 litapriori = 0
% 28.22/28.69 termapriori = 1
% 28.22/28.69 litaposteriori = 0
% 28.22/28.69 termaposteriori = 0
% 28.22/28.69 demodaposteriori = 0
% 28.22/28.69 ordereqreflfact = 0
% 28.22/28.69
% 28.22/28.69 litselect = negord
% 28.22/28.69
% 28.22/28.69 maxweight = 15
% 28.22/28.69 maxdepth = 30000
% 28.22/28.69 maxlength = 115
% 28.22/28.69 maxnrvars = 195
% 28.22/28.69 excuselevel = 1
% 28.22/28.69 increasemaxweight = 1
% 28.22/28.69
% 28.22/28.69 maxselected = 10000000
% 28.22/28.69 maxnrclauses = 10000000
% 28.22/28.69
% 28.22/28.69 showgenerated = 0
% 28.22/28.69 showkept = 0
% 28.22/28.69 showselected = 0
% 28.22/28.69 showdeleted = 0
% 28.22/28.69 showresimp = 1
% 28.22/28.69 showstatus = 2000
% 28.22/28.69
% 28.22/28.69 prologoutput = 1
% 28.22/28.69 nrgoals = 5000000
% 28.22/28.69 totalproof = 1
% 28.22/28.69
% 28.22/28.69 Symbols occurring in the translation:
% 28.22/28.69
% 28.22/28.69 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 28.22/28.69 . [1, 2] (w:1, o:50, a:1, s:1, b:0),
% 28.22/28.69 ! [4, 1] (w:0, o:34, a:1, s:1, b:0),
% 28.22/28.69 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 28.22/28.69 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 28.22/28.69 btrue [41, 0] (w:1, o:22, a:1, s:1, b:0),
% 28.22/28.69 aux [42, 3] (w:1, o:99, a:1, s:1, b:0),
% 28.22/28.69 zero [43, 0] (w:1, o:23, a:1, s:1, b:0),
% 28.22/28.69 suc [44, 1] (w:1, o:40, a:1, s:1, b:0),
% 28.22/28.69 n [45, 1] (w:1, o:41, a:1, s:1, b:0),
% 28.22/28.69 mul [46, 2] (w:1, o:75, a:1, s:1, b:0),
% 28.22/28.69 add [49, 2] (w:1, o:76, a:1, s:1, b:0),
% 28.22/28.69 bfalse [50, 0] (w:1, o:29, a:1, s:1, b:0),
% 28.22/28.69 eq [53, 2] (w:1, o:77, a:1, s:1, b:0),
% 28.22/28.69 v [54, 1] (w:1, o:42, a:1, s:1, b:0),
% 28.22/28.69 aux2 [55, 3] (w:1, o:100, a:1, s:1, b:0),
% 28.22/28.69 aux3 [58, 3] (w:1, o:101, a:1, s:1, b:0),
% 28.22/28.69 aux4 [60, 3] (w:1, o:102, a:1, s:1, b:0),
% 28.22/28.69 b [61, 1] (w:1, o:44, a:1, s:1, b:0),
% 28.22/28.69 y [63, 1] (w:1, o:46, a:1, s:1, b:0),
% 28.22/28.69 fail4 [64, 2] (w:1, o:90, a:1, s:1, b:0),
% 28.22/28.69 aux5 [66, 3] (w:1, o:103, a:1, s:1, b:0),
% 28.22/28.69 x5 [68, 1] (w:1, o:45, a:1, s:1, b:0),
% 28.22/28.69 b2 [69, 1] (w:1, o:47, a:1, s:1, b:0),
% 28.22/28.69 fail23 [70, 2] (w:1, o:92, a:1, s:1, b:0),
% 28.22/28.69 aux6 [72, 3] (w:1, o:104, a:1, s:1, b:0),
% 28.22/28.69 a3 [73, 1] (w:1, o:43, a:1, s:1, b:0),
% 28.22/28.69 b3 [74, 1] (w:1, o:48, a:1, s:1, b:0),
% 156.82/157.25 aux7 [75, 4] (w:1, o:105, a:1, s:1, b:0),
% 156.82/157.25 fail1 [76, 2] (w:1, o:91, a:1, s:1, b:0),
% 156.82/157.25 eq3 [77, 2] (w:1, o:79, a:1, s:1, b:0),
% 156.82/157.25 fail [78, 2] (w:1, o:93, a:1, s:1, b:0),
% 156.82/157.25 fail3 [80, 2] (w:1, o:88, a:1, s:1, b:0),
% 156.82/157.25 fail22 [82, 2] (w:1, o:85, a:1, s:1, b:0),
% 156.82/157.25 fail12 [84, 2] (w:1, o:82, a:1, s:1, b:0),
% 156.82/157.25 fail2 [86, 2] (w:1, o:86, a:1, s:1, b:0),
% 156.82/157.25 fail13 [88, 2] (w:1, o:84, a:1, s:1, b:0),
% 156.82/157.25 simp2 [89, 1] (w:1, o:49, a:1, s:1, b:0),
% 156.82/157.25 fail32 [90, 2] (w:1, o:89, a:1, s:1, b:0),
% 156.82/157.25 fail222 [91, 2] (w:1, o:87, a:1, s:1, b:0),
% 156.82/157.25 fail122 [92, 2] (w:1, o:83, a:1, s:1, b:0),
% 156.82/157.25 step2 [93, 1] (w:1, o:39, a:1, s:1, b:0),
% 156.82/157.25 nil [94, 0] (w:1, o:30, a:1, s:1, b:0),
% 156.82/157.25 fetch [95, 2] (w:1, o:94, a:1, s:1, b:0),
% 156.82/157.25 cons [98, 2] (w:1, o:95, a:1, s:1, b:0),
% 156.82/157.25 addNat [100, 2] (w:1, o:96, a:1, s:1, b:0),
% 156.82/157.25 mulNat [101, 2] (w:1, o:97, a:1, s:1, b:0),
% 156.82/157.25 eval [102, 2] (w:1, o:80, a:1, s:1, b:0),
% 156.82/157.25 eq2 [103, 2] (w:1, o:78, a:1, s:1, b:0),
% 156.82/157.25 prop2 [104, 2] (w:1, o:98, a:1, s:1, b:0),
% 156.82/157.25 eq4 [105, 2] (w:1, o:81, a:1, s:1, b:0).
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Starting Search:
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 15526
% 156.82/157.25 Kept: 2000
% 156.82/157.25 Inuse: 919
% 156.82/157.25 Deleted: 55
% 156.82/157.25 Deletedinuse: 15
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 160871
% 156.82/157.25 Kept: 4040
% 156.82/157.25 Inuse: 1984
% 156.82/157.25 Deleted: 88
% 156.82/157.25 Deletedinuse: 19
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Failed to find proof!
% 156.82/157.25 maxweight = 15
% 156.82/157.25 maxnrclauses = 10000000
% 156.82/157.25 Generated: 405104
% 156.82/157.25 Kept: 4572
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 The strategy used was not complete!
% 156.82/157.25
% 156.82/157.25 Increased maxweight to 16
% 156.82/157.25
% 156.82/157.25 Starting Search:
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 9049
% 156.82/157.25 Kept: 2048
% 156.82/157.25 Inuse: 676
% 156.82/157.25 Deleted: 50
% 156.82/157.25 Deletedinuse: 14
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 28697
% 156.82/157.25 Kept: 4061
% 156.82/157.25 Inuse: 1340
% 156.82/157.25 Deleted: 79
% 156.82/157.25 Deletedinuse: 17
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 127037
% 156.82/157.25 Kept: 6062
% 156.82/157.25 Inuse: 1885
% 156.82/157.25 Deleted: 92
% 156.82/157.25 Deletedinuse: 19
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 242289
% 156.82/157.25 Kept: 8072
% 156.82/157.25 Inuse: 2773
% 156.82/157.25 Deleted: 160
% 156.82/157.25 Deletedinuse: 24
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Failed to find proof!
% 156.82/157.25 maxweight = 16
% 156.82/157.25 maxnrclauses = 10000000
% 156.82/157.25 Generated: 1231680
% 156.82/157.25 Kept: 9750
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 The strategy used was not complete!
% 156.82/157.25
% 156.82/157.25 Increased maxweight to 17
% 156.82/157.25
% 156.82/157.25 Starting Search:
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 8028
% 156.82/157.25 Kept: 2004
% 156.82/157.25 Inuse: 640
% 156.82/157.25 Deleted: 46
% 156.82/157.25 Deletedinuse: 14
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 18378
% 156.82/157.25 Kept: 4007
% 156.82/157.25 Inuse: 1006
% 156.82/157.25 Deleted: 64
% 156.82/157.25 Deletedinuse: 16
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 32925
% 156.82/157.25 Kept: 6056
% 156.82/157.25 Inuse: 1446
% 156.82/157.25 Deleted: 85
% 156.82/157.25 Deletedinuse: 18
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 101445
% 156.82/157.25 Kept: 8059
% 156.82/157.25 Inuse: 1842
% 156.82/157.25 Deleted: 106
% 156.82/157.25 Deletedinuse: 19
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 178589
% 156.82/157.25 Kept: 10062
% 156.82/157.25 Inuse: 2182
% 156.82/157.25 Deleted: 162
% 156.82/157.25 Deletedinuse: 24
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 237118
% 156.82/157.25 Kept: 12066
% 156.82/157.25 Inuse: 2744
% 156.82/157.25 Deleted: 185
% 156.82/157.25 Deletedinuse: 24
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 347091
% 156.82/157.25 Kept: 14069
% 156.82/157.25 Inuse: 3552
% 156.82/157.25 Deleted: 242
% 156.82/157.25 Deletedinuse: 24
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 436082
% 156.82/157.25 Kept: 16075
% 156.82/157.25 Inuse: 4459
% 156.82/157.25 Deleted: 371
% 156.82/157.25 Deletedinuse: 36
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25 Resimplifying inuse:
% 156.82/157.25 Done
% 156.82/157.25
% 156.82/157.25
% 156.82/157.25 Intermediate Status:
% 156.82/157.25 Generated: 996295
% 156.82/157.25 Kept: 180Terminated
% 299.36/300.01 Bliksem ended
%------------------------------------------------------------------------------