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