%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN709-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Thu Jul 21 02:54:06 EDT 2022
% Result : Unsatisfiable 0.74s 1.14s
% Output : Refutation 0.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN709-1 : TPTP v8.1.0. Released v2.5.0.
% 0.03/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Mon Jul 11 16:50:57 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.74/1.13 *** allocated 10000 integers for termspace/termends
% 0.74/1.13 *** allocated 10000 integers for clauses
% 0.74/1.13 *** allocated 10000 integers for justifications
% 0.74/1.13 Bliksem 1.12
% 0.74/1.13
% 0.74/1.13
% 0.74/1.13 Automatic Strategy Selection
% 0.74/1.13
% 0.74/1.13 Clauses:
% 0.74/1.13 [
% 0.74/1.13 [ p10( X, X ) ],
% 0.74/1.13 [ p9( X, X ) ],
% 0.74/1.13 [ p7( X, X ) ],
% 0.74/1.13 [ p6( X, X ) ],
% 0.74/1.13 [ p42( X, X ) ],
% 0.74/1.13 [ p40( X, X ) ],
% 0.74/1.13 [ p4( X, X ) ],
% 0.74/1.13 [ p38( X, X ) ],
% 0.74/1.13 [ p36( X, X ) ],
% 0.74/1.13 [ p35( X, X ) ],
% 0.74/1.13 [ p32( X, X ) ],
% 0.74/1.13 [ p30( X, X ) ],
% 0.74/1.13 [ p3( X, X ) ],
% 0.74/1.13 [ p29( X, X ) ],
% 0.74/1.13 [ p27( X, X ) ],
% 0.74/1.13 [ p26( X, X ) ],
% 0.74/1.13 [ p24( X, X ) ],
% 0.74/1.13 [ p22( X, X ) ],
% 0.74/1.13 [ p21( X, X ) ],
% 0.74/1.13 [ p2( X, X ) ],
% 0.74/1.13 [ p19( X, X ) ],
% 0.74/1.13 [ p18( X, X ) ],
% 0.74/1.13 [ p16( X, X ) ],
% 0.74/1.13 [ p15( X, X ) ],
% 0.74/1.13 [ p13( X, X ) ],
% 0.74/1.13 [ p11( X, X ) ],
% 0.74/1.13 [ p44( c48, c49 ) ],
% 0.74/1.13 [ p44( c50, c49 ) ],
% 0.74/1.13 [ p46( f23( c58, c56 ), f20( c59, c60 ) ) ],
% 0.74/1.13 [ p44( f5( c51, f8( c52, c53 ) ), c49 ) ],
% 0.74/1.13 [ p45( f12( f14( c54, f17( c61, c49 ) ), c56 ), c57 ) ],
% 0.74/1.13 [ ~( p45( f12( f14( c54, f17( c55, c49 ) ), c56 ), c57 ) ) ],
% 0.74/1.13 [ p10( X, Y ), ~( p10( Z, Y ) ), ~( p10( Z, X ) ) ],
% 0.74/1.13 [ p9( X, Y ), ~( p9( Z, X ) ), ~( p9( Z, Y ) ) ],
% 0.74/1.13 [ p7( X, Y ), ~( p7( Z, X ) ), ~( p7( Z, Y ) ) ],
% 0.74/1.13 [ p6( X, Y ), ~( p6( Z, X ) ), ~( p6( Z, Y ) ) ],
% 0.74/1.13 [ p42( X, Y ), ~( p42( Z, X ) ), ~( p42( Z, Y ) ) ],
% 0.74/1.13 [ p40( X, Y ), ~( p40( Z, X ) ), ~( p40( Z, Y ) ) ],
% 0.74/1.13 [ p4( X, Y ), ~( p4( Z, X ) ), ~( p4( Z, Y ) ) ],
% 0.74/1.13 [ p38( X, Y ), ~( p38( Z, X ) ), ~( p38( Z, Y ) ) ],
% 0.74/1.13 [ p36( X, Y ), ~( p36( Z, X ) ), ~( p36( Z, Y ) ) ],
% 0.74/1.13 [ p35( X, Y ), ~( p35( Z, X ) ), ~( p35( Z, Y ) ) ],
% 0.74/1.13 [ p32( X, Y ), ~( p32( Z, X ) ), ~( p32( Z, Y ) ) ],
% 0.74/1.13 [ p30( X, Y ), ~( p30( Z, X ) ), ~( p30( Z, Y ) ) ],
% 0.74/1.13 [ p3( X, Y ), ~( p3( Z, X ) ), ~( p3( Z, Y ) ) ],
% 0.74/1.13 [ p29( X, Y ), ~( p29( Z, X ) ), ~( p29( Z, Y ) ) ],
% 0.74/1.13 [ p27( X, Y ), ~( p27( Z, X ) ), ~( p27( Z, Y ) ) ],
% 0.74/1.13 [ p26( X, Y ), ~( p26( Z, X ) ), ~( p26( Z, Y ) ) ],
% 0.74/1.13 [ p24( X, Y ), ~( p24( Z, X ) ), ~( p24( Z, Y ) ) ],
% 0.74/1.13 [ p22( X, Y ), ~( p22( Z, X ) ), ~( p22( Z, Y ) ) ],
% 0.74/1.13 [ p21( X, Y ), ~( p21( Z, X ) ), ~( p21( Z, Y ) ) ],
% 0.74/1.13 [ p2( X, Y ), ~( p2( Z, X ) ), ~( p2( Z, Y ) ) ],
% 0.74/1.13 [ p19( X, Y ), ~( p19( Z, X ) ), ~( p19( Z, Y ) ) ],
% 0.74/1.13 [ p18( X, Y ), ~( p18( Z, X ) ), ~( p18( Z, Y ) ) ],
% 0.74/1.13 [ p16( X, Y ), ~( p16( Z, X ) ), ~( p16( Z, Y ) ) ],
% 0.74/1.13 [ p15( X, Y ), ~( p15( Z, X ) ), ~( p15( Z, Y ) ) ],
% 0.74/1.13 [ p13( X, Y ), ~( p13( Z, X ) ), ~( p13( Z, Y ) ) ],
% 0.74/1.13 [ p11( X, Y ), ~( p11( Z, X ) ), ~( p11( Z, Y ) ) ],
% 0.74/1.13 [ p19( f25( f28( c64, X ), f34( c66, Y ) ), f34( X, Y ) ) ],
% 0.74/1.13 [ p47( X, Y ), ~( p30( Z, X ) ), ~( p47( Z, T ) ), ~( p19( T, Y ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p44( X, Y ), ~( p4( Z, X ) ), ~( p44( Z, T ) ), ~( p16( T, Y ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p45( X, Y ), ~( p11( Z, X ) ), ~( p45( Z, T ) ), ~( p10( T, Y ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p46( X, Y ), ~( p22( Z, X ) ), ~( p46( Z, T ) ), ~( p11( T, Y ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ ~( p47( f31( f33( c62, c63 ), f34( c65, c56 ) ), f25( f28( c64, c65 )
% 0.74/1.13 , c60 ) ) ) ],
% 0.74/1.13 [ p11( f12( X, Y ), f12( Z, T ) ), ~( p10( Y, T ) ), ~( p9( X, Z ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p9( f17( X, Y ), f17( Z, T ) ), ~( p15( X, Z ) ), ~( p16( Y, T ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p9( f14( X, Y ), f14( Z, T ) ), ~( p13( X, Z ) ), ~( p9( Y, T ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p4( f5( X, Y ), f5( Z, T ) ), ~( p2( X, Z ) ), ~( p3( Y, T ) ) ],
% 0.74/1.13 [ p38( f41( X, Y ), f41( Z, T ) ), ~( p24( Y, T ) ), ~( p40( X, Z ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p36( f39( X, Y ), f39( Z, T ) ), ~( p36( Y, T ) ), ~( p38( X, Z ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p35( f43( X, Y ), f43( Z, T ) ), ~( p10( Y, T ) ), ~( p42( X, Z ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p30( f31( X, Y ), f31( Z, T ) ), ~( p19( Y, T ) ), ~( p29( X, Z ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p3( f8( X, Y ), f8( Z, T ) ), ~( p6( X, Z ) ), ~( p7( Y, T ) ) ],
% 0.74/1.13 [ p29( f33( X, Y ), f33( Z, T ) ), ~( p29( Y, T ) ), ~( p32( X, Z ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p24( f28( X, Y ), f28( Z, T ) ), ~( p26( X, Z ) ), ~( p27( Y, T ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p22( f23( X, Y ), f23( Z, T ) ), ~( p10( Y, T ) ), ~( p21( X, Z ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p19( f37( X, Y ), f37( Z, T ) ), ~( p35( X, Z ) ), ~( p36( Y, T ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p19( f34( X, Y ), f34( Z, T ) ), ~( p10( Y, T ) ), ~( p27( X, Z ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p19( f25( X, Y ), f25( Z, T ) ), ~( p19( Y, T ) ), ~( p24( X, Z ) ) ]
% 0.74/1.13 ,
% 0.74/1.13 [ p11( f20( X, Y ), f20( Z, T ) ), ~( p18( X, Z ) ), ~( p19( Y, T ) ) ]
% 0.74/1.14 ,
% 0.74/1.14 [ p47( f31( f33( c62, c63 ), f34( c66, X ) ), Y ), ~( p46( f23( c58, X )
% 0.74/1.14 , f20( c59, Y ) ) ) ],
% 0.74/1.14 [ p19( f25( f28( c64, X ), f37( f43( c67, Y ), Z ) ), f37( f43( c67, Y )
% 0.74/1.14 , f39( f41( c68, f28( c64, X ) ), Z ) ) ) ],
% 0.74/1.14 [ p47( f31( f33( c62, c63 ), f25( f28( c64, c65 ), X ) ), f25( f28( c64
% 0.74/1.14 , c65 ), Y ) ), ~( p47( f31( f33( c62, c63 ), X ), Y ) ) ]
% 0.74/1.14 ] .
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 percentage equality = 0.000000, percentage horn = 1.000000
% 0.74/1.14 This is a near-Horn, non-equality problem
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 Options Used:
% 0.74/1.14
% 0.74/1.14 useres = 1
% 0.74/1.14 useparamod = 0
% 0.74/1.14 useeqrefl = 0
% 0.74/1.14 useeqfact = 0
% 0.74/1.14 usefactor = 1
% 0.74/1.14 usesimpsplitting = 0
% 0.74/1.14 usesimpdemod = 0
% 0.74/1.14 usesimpres = 4
% 0.74/1.14
% 0.74/1.14 resimpinuse = 1000
% 0.74/1.14 resimpclauses = 20000
% 0.74/1.14 substype = standard
% 0.74/1.14 backwardsubs = 1
% 0.74/1.14 selectoldest = 5
% 0.74/1.14
% 0.74/1.14 litorderings [0] = split
% 0.74/1.14 litorderings [1] = liftord
% 0.74/1.14
% 0.74/1.14 termordering = none
% 0.74/1.14
% 0.74/1.14 litapriori = 1
% 0.74/1.14 termapriori = 0
% 0.74/1.14 litaposteriori = 0
% 0.74/1.14 termaposteriori = 0
% 0.74/1.14 demodaposteriori = 0
% 0.74/1.14 ordereqreflfact = 0
% 0.74/1.14
% 0.74/1.14 litselect = negative
% 0.74/1.14
% 0.74/1.14 maxweight = 30000
% 0.74/1.14 maxdepth = 30000
% 0.74/1.14 maxlength = 115
% 0.74/1.14 maxnrvars = 195
% 0.74/1.14 excuselevel = 0
% 0.74/1.14 increasemaxweight = 0
% 0.74/1.14
% 0.74/1.14 maxselected = 10000000
% 0.74/1.14 maxnrclauses = 10000000
% 0.74/1.14
% 0.74/1.14 showgenerated = 0
% 0.74/1.14 showkept = 0
% 0.74/1.14 showselected = 0
% 0.74/1.14 showdeleted = 0
% 0.74/1.14 showresimp = 1
% 0.74/1.14 showstatus = 2000
% 0.74/1.14
% 0.74/1.14 prologoutput = 1
% 0.74/1.14 nrgoals = 5000000
% 0.74/1.14 totalproof = 1
% 0.74/1.14
% 0.74/1.14 Symbols occurring in the translation:
% 0.74/1.14
% 0.74/1.14 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.74/1.14 . [1, 2] (w:1, o:202, a:1, s:1, b:0),
% 0.74/1.14 ! [4, 1] (w:1, o:197, a:1, s:1, b:0),
% 0.74/1.14 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.74/1.14 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.74/1.14 p10 [40, 2] (w:1, o:227, a:1, s:1, b:0),
% 0.74/1.14 p9 [42, 2] (w:1, o:228, a:1, s:1, b:0),
% 0.74/1.14 p7 [44, 2] (w:1, o:230, a:1, s:1, b:0),
% 0.74/1.14 p6 [46, 2] (w:1, o:229, a:1, s:1, b:0),
% 0.74/1.14 p42 [48, 2] (w:1, o:250, a:1, s:1, b:0),
% 0.74/1.14 p40 [50, 2] (w:1, o:251, a:1, s:1, b:0),
% 0.74/1.14 p4 [52, 2] (w:1, o:252, a:1, s:1, b:0),
% 0.74/1.14 p38 [54, 2] (w:1, o:244, a:1, s:1, b:0),
% 0.74/1.14 p36 [56, 2] (w:1, o:246, a:1, s:1, b:0),
% 0.74/1.14 p35 [58, 2] (w:1, o:245, a:1, s:1, b:0),
% 0.74/1.14 p32 [60, 2] (w:1, o:247, a:1, s:1, b:0),
% 0.74/1.14 p30 [62, 2] (w:1, o:248, a:1, s:1, b:0),
% 0.74/1.14 p3 [64, 2] (w:1, o:249, a:1, s:1, b:0),
% 0.74/1.14 p29 [66, 2] (w:1, o:237, a:1, s:1, b:0),
% 0.74/1.14 p27 [68, 2] (w:1, o:239, a:1, s:1, b:0),
% 0.74/1.14 p26 [70, 2] (w:1, o:238, a:1, s:1, b:0),
% 0.74/1.14 p24 [72, 2] (w:1, o:240, a:1, s:1, b:0),
% 0.74/1.14 p22 [74, 2] (w:1, o:242, a:1, s:1, b:0),
% 0.74/1.14 p21 [76, 2] (w:1, o:241, a:1, s:1, b:0),
% 0.74/1.14 p2 [78, 2] (w:1, o:243, a:1, s:1, b:0),
% 0.74/1.14 p19 [80, 2] (w:1, o:232, a:1, s:1, b:0),
% 0.74/1.14 p18 [82, 2] (w:1, o:231, a:1, s:1, b:0),
% 0.74/1.14 p16 [84, 2] (w:1, o:234, a:1, s:1, b:0),
% 0.74/1.14 p15 [86, 2] (w:1, o:233, a:1, s:1, b:0),
% 0.74/1.14 p13 [88, 2] (w:1, o:235, a:1, s:1, b:0),
% 0.74/1.14 p11 [90, 2] (w:1, o:236, a:1, s:1, b:0),
% 0.74/1.14 c48 [91, 0] (w:1, o:169, a:1, s:1, b:0),
% 0.74/1.14 c49 [92, 0] (w:1, o:170, a:1, s:1, b:0),
% 0.74/1.14 p44 [93, 2] (w:1, o:253, a:1, s:1, b:0),
% 0.74/1.14 c50 [94, 0] (w:1, o:171, a:1, s:1, b:0),
% 0.74/1.14 c58 [95, 0] (w:1, o:173, a:1, s:1, b:0),
% 0.74/1.14 c56 [96, 0] (w:1, o:175, a:1, s:1, b:0),
% 0.74/1.14 f23 [97, 2] (w:1, o:257, a:1, s:1, b:0),
% 0.74/1.14 c59 [98, 0] (w:1, o:176, a:1, s:1, b:0),
% 0.74/1.14 c60 [99, 0] (w:1, o:181, a:1, s:1, b:0),
% 0.74/1.14 f20 [100, 2] (w:1, o:258, a:1, s:1, b:0),
% 0.74/1.14 p46 [101, 2] (w:1, o:260, a:1, s:1, b:0),
% 0.74/1.14 c51 [102, 0] (w:1, o:177, a:1, s:1, b:0),
% 0.74/1.14 c52 [103, 0] (w:1, o:178, a:1, s:1, b:0),
% 0.74/1.14 c53 [104, 0] (w:1, o:179, a:1, s:1, b:0),
% 0.74/1.14 f8 [105, 2] (w:1, o:261, a:1, s:1, b:0),
% 0.74/1.14 f5 [106, 2] (w:1, o:266, a:1, s:1, b:0),
% 0.74/1.14 c54 [107, 0] (w:1, o:180, a:1, s:1, b:0),
% 0.74/1.14 c61 [108, 0] (w:1, o:182, a:1, s:1, b:0),
% 0.74/1.14 f17 [109, 2] (w:1, o:254, a:1, s:1, b:0),
% 0.74/1.14 f14 [110, 2] (w:1, o:255, a:1, s:1, b:0),
% 0.74/1.14 f12 [111, 2] (w:1, o:256, a:1, s:1, b:0),
% 0.74/1.14 c57 [112, 0] (w:1, o:172, a:1, s:1, b:0),
% 0.74/1.14 p45 [113, 2] (w:1, o:259, a:1, s:1, b:0),
% 0.74/1.14 c55 [114, 0] (w:1, o:174, a:1, s:1, b:0),
% 0.74/1.14 c64 [167, 0] (w:1, o:187, a:1, s:1, b:0),
% 0.74/1.14 f28 [169, 2] (w:1, o:267, a:1, s:1, b:0),
% 0.74/1.14 c66 [170, 0] (w:1, o:189, a:1, s:1, b:0),
% 0.74/1.14 f34 [172, 2] (w:1, o:270, a:1, s:1, b:0),
% 0.74/1.14 f25 [173, 2] (w:1, o:268, a:1, s:1, b:0),
% 0.74/1.14 p47 [176, 2] (w:1, o:271, a:1, s:1, b:0),
% 0.74/1.14 c62 [191, 0] (w:1, o:190, a:1, s:1, b:0),
% 0.74/1.14 c63 [192, 0] (w:1, o:186, a:1, s:1, b:0),
% 0.74/1.14 f33 [193, 2] (w:1, o:269, a:1, s:1, b:0),
% 0.74/1.14 c65 [194, 0] (w:1, o:188, a:1, s:1, b:0),
% 0.74/1.14 f31 [195, 2] (w:1, o:272, a:1, s:1, b:0),
% 0.74/1.14 f41 [214, 2] (w:1, o:264, a:1, s:1, b:0),
% 0.74/1.14 f39 [219, 2] (w:1, o:262, a:1, s:1, b:0),
% 0.74/1.14 f43 [224, 2] (w:1, o:265, a:1, s:1, b:0),
% 0.74/1.14 f37 [249, 2] (w:1, o:263, a:1, s:1, b:0),
% 0.74/1.14 c67 [267, 0] (w:1, o:195, a:1, s:1, b:0),
% 0.74/1.14 c68 [270, 0] (w:1, o:196, a:1, s:1, b:0).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 Starting Search:
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 Bliksems!, er is een bewijs:
% 0.74/1.14 % SZS status Unsatisfiable
% 0.74/1.14 % SZS output start Refutation
% 0.74/1.14
% 0.74/1.14 clause( 13, [ p29( X, X ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 20, [ p19( X, X ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 28, [ p46( f23( c58, c56 ), f20( c59, c60 ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 58, [ p19( f25( f28( c64, X ), f34( c66, Y ) ), f34( X, Y ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 59, [ ~( p47( Z, T ) ), ~( p19( T, Y ) ), p47( X, Y ), ~( p30( Z, X
% 0.74/1.14 ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 63, [ ~( p47( f31( f33( c62, c63 ), f34( c65, c56 ) ), f25( f28(
% 0.74/1.14 c64, c65 ), c60 ) ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 71, [ ~( p19( Y, T ) ), p30( f31( X, Y ), f31( Z, T ) ), ~( p29( X
% 0.74/1.14 , Z ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 80, [ p47( f31( f33( c62, c63 ), f34( c66, X ) ), Y ), ~( p46( f23(
% 0.74/1.14 c58, X ), f20( c59, Y ) ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 82, [ p47( f31( f33( c62, c63 ), f25( f28( c64, c65 ), X ) ), f25(
% 0.74/1.14 f28( c64, c65 ), Y ) ), ~( p47( f31( f33( c62, c63 ), X ), Y ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 136, [ p30( f31( Z, X ), f31( Z, Y ) ), ~( p19( X, Y ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 138, [ p30( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), f31( X,
% 0.74/1.14 f34( Y, Z ) ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 140, [ p47( f31( f33( c62, c63 ), f34( c66, c56 ) ), c60 ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 143, [ ~( p47( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), T ) )
% 0.74/1.14 , p47( f31( X, f34( Y, Z ) ), U ), ~( p19( T, U ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 173, [ p47( f31( f33( c62, c63 ), f25( f28( c64, c65 ), f34( c66,
% 0.74/1.14 c56 ) ) ), f25( f28( c64, c65 ), c60 ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 200, [ p47( f31( X, f34( Y, Z ) ), T ), ~( p47( f31( X, f25( f28(
% 0.74/1.14 c64, Y ), f34( c66, Z ) ) ), T ) ) ] )
% 0.74/1.14 .
% 0.74/1.14 clause( 201, [] )
% 0.74/1.14 .
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 % SZS output end Refutation
% 0.74/1.14 found a proof!
% 0.74/1.14
% 0.74/1.14 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 0.74/1.14
% 0.74/1.14 initialclauses(
% 0.74/1.14 [ clause( 203, [ p10( X, X ) ] )
% 0.74/1.14 , clause( 204, [ p9( X, X ) ] )
% 0.74/1.14 , clause( 205, [ p7( X, X ) ] )
% 0.74/1.14 , clause( 206, [ p6( X, X ) ] )
% 0.74/1.14 , clause( 207, [ p42( X, X ) ] )
% 0.74/1.14 , clause( 208, [ p40( X, X ) ] )
% 0.74/1.14 , clause( 209, [ p4( X, X ) ] )
% 0.74/1.14 , clause( 210, [ p38( X, X ) ] )
% 0.74/1.14 , clause( 211, [ p36( X, X ) ] )
% 0.74/1.14 , clause( 212, [ p35( X, X ) ] )
% 0.74/1.14 , clause( 213, [ p32( X, X ) ] )
% 0.74/1.14 , clause( 214, [ p30( X, X ) ] )
% 0.74/1.14 , clause( 215, [ p3( X, X ) ] )
% 0.74/1.14 , clause( 216, [ p29( X, X ) ] )
% 0.74/1.14 , clause( 217, [ p27( X, X ) ] )
% 0.74/1.14 , clause( 218, [ p26( X, X ) ] )
% 0.74/1.14 , clause( 219, [ p24( X, X ) ] )
% 0.74/1.14 , clause( 220, [ p22( X, X ) ] )
% 0.74/1.14 , clause( 221, [ p21( X, X ) ] )
% 0.74/1.14 , clause( 222, [ p2( X, X ) ] )
% 0.74/1.14 , clause( 223, [ p19( X, X ) ] )
% 0.74/1.14 , clause( 224, [ p18( X, X ) ] )
% 0.74/1.14 , clause( 225, [ p16( X, X ) ] )
% 0.74/1.14 , clause( 226, [ p15( X, X ) ] )
% 0.74/1.14 , clause( 227, [ p13( X, X ) ] )
% 0.74/1.14 , clause( 228, [ p11( X, X ) ] )
% 0.74/1.14 , clause( 229, [ p44( c48, c49 ) ] )
% 0.74/1.14 , clause( 230, [ p44( c50, c49 ) ] )
% 0.74/1.14 , clause( 231, [ p46( f23( c58, c56 ), f20( c59, c60 ) ) ] )
% 0.74/1.14 , clause( 232, [ p44( f5( c51, f8( c52, c53 ) ), c49 ) ] )
% 0.74/1.14 , clause( 233, [ p45( f12( f14( c54, f17( c61, c49 ) ), c56 ), c57 ) ] )
% 0.74/1.14 , clause( 234, [ ~( p45( f12( f14( c54, f17( c55, c49 ) ), c56 ), c57 ) ) ]
% 0.74/1.14 )
% 0.74/1.14 , clause( 235, [ p10( X, Y ), ~( p10( Z, Y ) ), ~( p10( Z, X ) ) ] )
% 0.74/1.14 , clause( 236, [ p9( X, Y ), ~( p9( Z, X ) ), ~( p9( Z, Y ) ) ] )
% 0.74/1.14 , clause( 237, [ p7( X, Y ), ~( p7( Z, X ) ), ~( p7( Z, Y ) ) ] )
% 0.74/1.14 , clause( 238, [ p6( X, Y ), ~( p6( Z, X ) ), ~( p6( Z, Y ) ) ] )
% 0.74/1.14 , clause( 239, [ p42( X, Y ), ~( p42( Z, X ) ), ~( p42( Z, Y ) ) ] )
% 0.74/1.14 , clause( 240, [ p40( X, Y ), ~( p40( Z, X ) ), ~( p40( Z, Y ) ) ] )
% 0.74/1.14 , clause( 241, [ p4( X, Y ), ~( p4( Z, X ) ), ~( p4( Z, Y ) ) ] )
% 0.74/1.14 , clause( 242, [ p38( X, Y ), ~( p38( Z, X ) ), ~( p38( Z, Y ) ) ] )
% 0.74/1.14 , clause( 243, [ p36( X, Y ), ~( p36( Z, X ) ), ~( p36( Z, Y ) ) ] )
% 0.74/1.14 , clause( 244, [ p35( X, Y ), ~( p35( Z, X ) ), ~( p35( Z, Y ) ) ] )
% 0.74/1.14 , clause( 245, [ p32( X, Y ), ~( p32( Z, X ) ), ~( p32( Z, Y ) ) ] )
% 0.74/1.14 , clause( 246, [ p30( X, Y ), ~( p30( Z, X ) ), ~( p30( Z, Y ) ) ] )
% 0.74/1.14 , clause( 247, [ p3( X, Y ), ~( p3( Z, X ) ), ~( p3( Z, Y ) ) ] )
% 0.74/1.14 , clause( 248, [ p29( X, Y ), ~( p29( Z, X ) ), ~( p29( Z, Y ) ) ] )
% 0.74/1.14 , clause( 249, [ p27( X, Y ), ~( p27( Z, X ) ), ~( p27( Z, Y ) ) ] )
% 0.74/1.14 , clause( 250, [ p26( X, Y ), ~( p26( Z, X ) ), ~( p26( Z, Y ) ) ] )
% 0.74/1.14 , clause( 251, [ p24( X, Y ), ~( p24( Z, X ) ), ~( p24( Z, Y ) ) ] )
% 0.74/1.14 , clause( 252, [ p22( X, Y ), ~( p22( Z, X ) ), ~( p22( Z, Y ) ) ] )
% 0.74/1.14 , clause( 253, [ p21( X, Y ), ~( p21( Z, X ) ), ~( p21( Z, Y ) ) ] )
% 0.74/1.14 , clause( 254, [ p2( X, Y ), ~( p2( Z, X ) ), ~( p2( Z, Y ) ) ] )
% 0.74/1.14 , clause( 255, [ p19( X, Y ), ~( p19( Z, X ) ), ~( p19( Z, Y ) ) ] )
% 0.74/1.14 , clause( 256, [ p18( X, Y ), ~( p18( Z, X ) ), ~( p18( Z, Y ) ) ] )
% 0.74/1.14 , clause( 257, [ p16( X, Y ), ~( p16( Z, X ) ), ~( p16( Z, Y ) ) ] )
% 0.74/1.14 , clause( 258, [ p15( X, Y ), ~( p15( Z, X ) ), ~( p15( Z, Y ) ) ] )
% 0.74/1.14 , clause( 259, [ p13( X, Y ), ~( p13( Z, X ) ), ~( p13( Z, Y ) ) ] )
% 0.74/1.14 , clause( 260, [ p11( X, Y ), ~( p11( Z, X ) ), ~( p11( Z, Y ) ) ] )
% 0.74/1.14 , clause( 261, [ p19( f25( f28( c64, X ), f34( c66, Y ) ), f34( X, Y ) ) ]
% 0.74/1.14 )
% 0.74/1.14 , clause( 262, [ p47( X, Y ), ~( p30( Z, X ) ), ~( p47( Z, T ) ), ~( p19( T
% 0.74/1.14 , Y ) ) ] )
% 0.74/1.14 , clause( 263, [ p44( X, Y ), ~( p4( Z, X ) ), ~( p44( Z, T ) ), ~( p16( T
% 0.74/1.14 , Y ) ) ] )
% 0.74/1.14 , clause( 264, [ p45( X, Y ), ~( p11( Z, X ) ), ~( p45( Z, T ) ), ~( p10( T
% 0.74/1.14 , Y ) ) ] )
% 0.74/1.14 , clause( 265, [ p46( X, Y ), ~( p22( Z, X ) ), ~( p46( Z, T ) ), ~( p11( T
% 0.74/1.14 , Y ) ) ] )
% 0.74/1.14 , clause( 266, [ ~( p47( f31( f33( c62, c63 ), f34( c65, c56 ) ), f25( f28(
% 0.74/1.14 c64, c65 ), c60 ) ) ) ] )
% 0.74/1.14 , clause( 267, [ p11( f12( X, Y ), f12( Z, T ) ), ~( p10( Y, T ) ), ~( p9(
% 0.74/1.14 X, Z ) ) ] )
% 0.74/1.14 , clause( 268, [ p9( f17( X, Y ), f17( Z, T ) ), ~( p15( X, Z ) ), ~( p16(
% 0.74/1.14 Y, T ) ) ] )
% 0.74/1.14 , clause( 269, [ p9( f14( X, Y ), f14( Z, T ) ), ~( p13( X, Z ) ), ~( p9( Y
% 0.74/1.14 , T ) ) ] )
% 0.74/1.14 , clause( 270, [ p4( f5( X, Y ), f5( Z, T ) ), ~( p2( X, Z ) ), ~( p3( Y, T
% 0.74/1.14 ) ) ] )
% 0.74/1.14 , clause( 271, [ p38( f41( X, Y ), f41( Z, T ) ), ~( p24( Y, T ) ), ~( p40(
% 0.74/1.14 X, Z ) ) ] )
% 0.74/1.14 , clause( 272, [ p36( f39( X, Y ), f39( Z, T ) ), ~( p36( Y, T ) ), ~( p38(
% 0.74/1.14 X, Z ) ) ] )
% 0.74/1.14 , clause( 273, [ p35( f43( X, Y ), f43( Z, T ) ), ~( p10( Y, T ) ), ~( p42(
% 0.74/1.14 X, Z ) ) ] )
% 0.74/1.14 , clause( 274, [ p30( f31( X, Y ), f31( Z, T ) ), ~( p19( Y, T ) ), ~( p29(
% 0.74/1.14 X, Z ) ) ] )
% 0.74/1.14 , clause( 275, [ p3( f8( X, Y ), f8( Z, T ) ), ~( p6( X, Z ) ), ~( p7( Y, T
% 0.74/1.14 ) ) ] )
% 0.74/1.14 , clause( 276, [ p29( f33( X, Y ), f33( Z, T ) ), ~( p29( Y, T ) ), ~( p32(
% 0.74/1.14 X, Z ) ) ] )
% 0.74/1.14 , clause( 277, [ p24( f28( X, Y ), f28( Z, T ) ), ~( p26( X, Z ) ), ~( p27(
% 0.74/1.14 Y, T ) ) ] )
% 0.74/1.14 , clause( 278, [ p22( f23( X, Y ), f23( Z, T ) ), ~( p10( Y, T ) ), ~( p21(
% 0.74/1.14 X, Z ) ) ] )
% 0.74/1.14 , clause( 279, [ p19( f37( X, Y ), f37( Z, T ) ), ~( p35( X, Z ) ), ~( p36(
% 0.74/1.14 Y, T ) ) ] )
% 0.74/1.14 , clause( 280, [ p19( f34( X, Y ), f34( Z, T ) ), ~( p10( Y, T ) ), ~( p27(
% 0.74/1.14 X, Z ) ) ] )
% 0.74/1.14 , clause( 281, [ p19( f25( X, Y ), f25( Z, T ) ), ~( p19( Y, T ) ), ~( p24(
% 0.74/1.14 X, Z ) ) ] )
% 0.74/1.14 , clause( 282, [ p11( f20( X, Y ), f20( Z, T ) ), ~( p18( X, Z ) ), ~( p19(
% 0.74/1.14 Y, T ) ) ] )
% 0.74/1.14 , clause( 283, [ p47( f31( f33( c62, c63 ), f34( c66, X ) ), Y ), ~( p46(
% 0.74/1.14 f23( c58, X ), f20( c59, Y ) ) ) ] )
% 0.74/1.14 , clause( 284, [ p19( f25( f28( c64, X ), f37( f43( c67, Y ), Z ) ), f37(
% 0.74/1.14 f43( c67, Y ), f39( f41( c68, f28( c64, X ) ), Z ) ) ) ] )
% 0.74/1.14 , clause( 285, [ p47( f31( f33( c62, c63 ), f25( f28( c64, c65 ), X ) ),
% 0.74/1.14 f25( f28( c64, c65 ), Y ) ), ~( p47( f31( f33( c62, c63 ), X ), Y ) ) ]
% 0.74/1.14 )
% 0.74/1.14 ] ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 13, [ p29( X, X ) ] )
% 0.74/1.14 , clause( 216, [ p29( X, X ) ] )
% 0.74/1.14 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 20, [ p19( X, X ) ] )
% 0.74/1.14 , clause( 223, [ p19( X, X ) ] )
% 0.74/1.14 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 28, [ p46( f23( c58, c56 ), f20( c59, c60 ) ) ] )
% 0.74/1.14 , clause( 231, [ p46( f23( c58, c56 ), f20( c59, c60 ) ) ] )
% 0.74/1.14 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 58, [ p19( f25( f28( c64, X ), f34( c66, Y ) ), f34( X, Y ) ) ] )
% 0.74/1.14 , clause( 261, [ p19( f25( f28( c64, X ), f34( c66, Y ) ), f34( X, Y ) ) ]
% 0.74/1.14 )
% 0.74/1.14 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 0.74/1.14 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 59, [ ~( p47( Z, T ) ), ~( p19( T, Y ) ), p47( X, Y ), ~( p30( Z, X
% 0.74/1.14 ) ) ] )
% 0.74/1.14 , clause( 262, [ p47( X, Y ), ~( p30( Z, X ) ), ~( p47( Z, T ) ), ~( p19( T
% 0.74/1.14 , Y ) ) ] )
% 0.74/1.14 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 0.74/1.14 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 3 ), ==>( 2, 0 ), ==>( 3, 1 )] )
% 0.74/1.14 ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 63, [ ~( p47( f31( f33( c62, c63 ), f34( c65, c56 ) ), f25( f28(
% 0.74/1.14 c64, c65 ), c60 ) ) ) ] )
% 0.74/1.14 , clause( 266, [ ~( p47( f31( f33( c62, c63 ), f34( c65, c56 ) ), f25( f28(
% 0.74/1.14 c64, c65 ), c60 ) ) ) ] )
% 0.74/1.14 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 71, [ ~( p19( Y, T ) ), p30( f31( X, Y ), f31( Z, T ) ), ~( p29( X
% 0.74/1.14 , Z ) ) ] )
% 0.74/1.14 , clause( 274, [ p30( f31( X, Y ), f31( Z, T ) ), ~( p19( Y, T ) ), ~( p29(
% 0.74/1.14 X, Z ) ) ] )
% 0.74/1.14 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 0.74/1.14 permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 ), ==>( 2, 2 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 80, [ p47( f31( f33( c62, c63 ), f34( c66, X ) ), Y ), ~( p46( f23(
% 0.74/1.14 c58, X ), f20( c59, Y ) ) ) ] )
% 0.74/1.14 , clause( 283, [ p47( f31( f33( c62, c63 ), f34( c66, X ) ), Y ), ~( p46(
% 0.74/1.14 f23( c58, X ), f20( c59, Y ) ) ) ] )
% 0.74/1.14 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 0.74/1.14 ), ==>( 1, 1 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 82, [ p47( f31( f33( c62, c63 ), f25( f28( c64, c65 ), X ) ), f25(
% 0.74/1.14 f28( c64, c65 ), Y ) ), ~( p47( f31( f33( c62, c63 ), X ), Y ) ) ] )
% 0.74/1.14 , clause( 285, [ p47( f31( f33( c62, c63 ), f25( f28( c64, c65 ), X ) ),
% 0.74/1.14 f25( f28( c64, c65 ), Y ) ), ~( p47( f31( f33( c62, c63 ), X ), Y ) ) ]
% 0.74/1.14 )
% 0.74/1.14 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 0.74/1.14 ), ==>( 1, 1 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 resolution(
% 0.74/1.14 clause( 442, [ ~( p19( X, Y ) ), p30( f31( Z, X ), f31( Z, Y ) ) ] )
% 0.74/1.14 , clause( 71, [ ~( p19( Y, T ) ), p30( f31( X, Y ), f31( Z, T ) ), ~( p29(
% 0.74/1.14 X, Z ) ) ] )
% 0.74/1.14 , 2, clause( 13, [ p29( X, X ) ] )
% 0.74/1.14 , 0, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Z ), :=( T, Y )] ),
% 0.74/1.14 substitution( 1, [ :=( X, Z )] )).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 136, [ p30( f31( Z, X ), f31( Z, Y ) ), ~( p19( X, Y ) ) ] )
% 0.74/1.14 , clause( 442, [ ~( p19( X, Y ) ), p30( f31( Z, X ), f31( Z, Y ) ) ] )
% 0.74/1.14 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 0.74/1.14 permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 resolution(
% 0.74/1.14 clause( 443, [ p30( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), f31( X,
% 0.74/1.14 f34( Y, Z ) ) ) ] )
% 0.74/1.14 , clause( 136, [ p30( f31( Z, X ), f31( Z, Y ) ), ~( p19( X, Y ) ) ] )
% 0.74/1.14 , 1, clause( 58, [ p19( f25( f28( c64, X ), f34( c66, Y ) ), f34( X, Y ) )
% 0.74/1.14 ] )
% 0.74/1.14 , 0, substitution( 0, [ :=( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), :=( Y
% 0.74/1.14 , f34( Y, Z ) ), :=( Z, X )] ), substitution( 1, [ :=( X, Y ), :=( Y, Z )] )
% 0.74/1.14 ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 138, [ p30( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), f31( X,
% 0.74/1.14 f34( Y, Z ) ) ) ] )
% 0.74/1.14 , clause( 443, [ p30( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), f31( X
% 0.74/1.14 , f34( Y, Z ) ) ) ] )
% 0.74/1.14 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 0.74/1.14 permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 resolution(
% 0.74/1.14 clause( 444, [ p47( f31( f33( c62, c63 ), f34( c66, c56 ) ), c60 ) ] )
% 0.74/1.14 , clause( 80, [ p47( f31( f33( c62, c63 ), f34( c66, X ) ), Y ), ~( p46(
% 0.74/1.14 f23( c58, X ), f20( c59, Y ) ) ) ] )
% 0.74/1.14 , 1, clause( 28, [ p46( f23( c58, c56 ), f20( c59, c60 ) ) ] )
% 0.74/1.14 , 0, substitution( 0, [ :=( X, c56 ), :=( Y, c60 )] ), substitution( 1, [] )
% 0.74/1.14 ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 140, [ p47( f31( f33( c62, c63 ), f34( c66, c56 ) ), c60 ) ] )
% 0.74/1.14 , clause( 444, [ p47( f31( f33( c62, c63 ), f34( c66, c56 ) ), c60 ) ] )
% 0.74/1.14 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 resolution(
% 0.74/1.14 clause( 445, [ ~( p47( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), T ) )
% 0.74/1.14 , ~( p19( T, U ) ), p47( f31( X, f34( Y, Z ) ), U ) ] )
% 0.74/1.14 , clause( 59, [ ~( p47( Z, T ) ), ~( p19( T, Y ) ), p47( X, Y ), ~( p30( Z
% 0.74/1.14 , X ) ) ] )
% 0.74/1.14 , 3, clause( 138, [ p30( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), f31(
% 0.74/1.14 X, f34( Y, Z ) ) ) ] )
% 0.74/1.14 , 0, substitution( 0, [ :=( X, f31( X, f34( Y, Z ) ) ), :=( Y, U ), :=( Z,
% 0.74/1.14 f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ) ), :=( T, T )] ),
% 0.74/1.14 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 143, [ ~( p47( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), T ) )
% 0.74/1.14 , p47( f31( X, f34( Y, Z ) ), U ), ~( p19( T, U ) ) ] )
% 0.74/1.14 , clause( 445, [ ~( p47( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), T )
% 0.74/1.14 ), ~( p19( T, U ) ), p47( f31( X, f34( Y, Z ) ), U ) ] )
% 0.74/1.14 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 0.74/1.14 , U )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 2 ), ==>( 2, 1 )] )
% 0.74/1.14 ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 resolution(
% 0.74/1.14 clause( 446, [ p47( f31( f33( c62, c63 ), f25( f28( c64, c65 ), f34( c66,
% 0.74/1.14 c56 ) ) ), f25( f28( c64, c65 ), c60 ) ) ] )
% 0.74/1.14 , clause( 82, [ p47( f31( f33( c62, c63 ), f25( f28( c64, c65 ), X ) ), f25(
% 0.74/1.14 f28( c64, c65 ), Y ) ), ~( p47( f31( f33( c62, c63 ), X ), Y ) ) ] )
% 0.74/1.14 , 1, clause( 140, [ p47( f31( f33( c62, c63 ), f34( c66, c56 ) ), c60 ) ]
% 0.74/1.14 )
% 0.74/1.14 , 0, substitution( 0, [ :=( X, f34( c66, c56 ) ), :=( Y, c60 )] ),
% 0.74/1.14 substitution( 1, [] )).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 173, [ p47( f31( f33( c62, c63 ), f25( f28( c64, c65 ), f34( c66,
% 0.74/1.14 c56 ) ) ), f25( f28( c64, c65 ), c60 ) ) ] )
% 0.74/1.14 , clause( 446, [ p47( f31( f33( c62, c63 ), f25( f28( c64, c65 ), f34( c66
% 0.74/1.14 , c56 ) ) ), f25( f28( c64, c65 ), c60 ) ) ] )
% 0.74/1.14 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 resolution(
% 0.74/1.14 clause( 447, [ ~( p47( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), T ) )
% 0.74/1.14 , p47( f31( X, f34( Y, Z ) ), T ) ] )
% 0.74/1.14 , clause( 143, [ ~( p47( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), T )
% 0.74/1.14 ), p47( f31( X, f34( Y, Z ) ), U ), ~( p19( T, U ) ) ] )
% 0.74/1.14 , 2, clause( 20, [ p19( X, X ) ] )
% 0.74/1.14 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ),
% 0.74/1.14 :=( U, T )] ), substitution( 1, [ :=( X, T )] )).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 200, [ p47( f31( X, f34( Y, Z ) ), T ), ~( p47( f31( X, f25( f28(
% 0.74/1.14 c64, Y ), f34( c66, Z ) ) ), T ) ) ] )
% 0.74/1.14 , clause( 447, [ ~( p47( f31( X, f25( f28( c64, Y ), f34( c66, Z ) ) ), T )
% 0.74/1.14 ), p47( f31( X, f34( Y, Z ) ), T ) ] )
% 0.74/1.14 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 0.74/1.14 permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 resolution(
% 0.74/1.14 clause( 448, [ p47( f31( f33( c62, c63 ), f34( c65, c56 ) ), f25( f28( c64
% 0.74/1.14 , c65 ), c60 ) ) ] )
% 0.74/1.14 , clause( 200, [ p47( f31( X, f34( Y, Z ) ), T ), ~( p47( f31( X, f25( f28(
% 0.74/1.14 c64, Y ), f34( c66, Z ) ) ), T ) ) ] )
% 0.74/1.14 , 1, clause( 173, [ p47( f31( f33( c62, c63 ), f25( f28( c64, c65 ), f34(
% 0.74/1.14 c66, c56 ) ) ), f25( f28( c64, c65 ), c60 ) ) ] )
% 0.74/1.14 , 0, substitution( 0, [ :=( X, f33( c62, c63 ) ), :=( Y, c65 ), :=( Z, c56
% 0.74/1.14 ), :=( T, f25( f28( c64, c65 ), c60 ) )] ), substitution( 1, [] )).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 resolution(
% 0.74/1.14 clause( 449, [] )
% 0.74/1.14 , clause( 63, [ ~( p47( f31( f33( c62, c63 ), f34( c65, c56 ) ), f25( f28(
% 0.74/1.14 c64, c65 ), c60 ) ) ) ] )
% 0.74/1.14 , 0, clause( 448, [ p47( f31( f33( c62, c63 ), f34( c65, c56 ) ), f25( f28(
% 0.74/1.14 c64, c65 ), c60 ) ) ] )
% 0.74/1.14 , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 subsumption(
% 0.74/1.14 clause( 201, [] )
% 0.74/1.14 , clause( 449, [] )
% 0.74/1.14 , substitution( 0, [] ), permutation( 0, [] ) ).
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 end.
% 0.74/1.14
% 0.74/1.14 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 0.74/1.14
% 0.74/1.14 Memory use:
% 0.74/1.14
% 0.74/1.14 space for terms: 4830
% 0.74/1.14 space for clauses: 17048
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 clauses generated: 308
% 0.74/1.14 clauses kept: 202
% 0.74/1.14 clauses selected: 167
% 0.74/1.14 clauses deleted: 0
% 0.74/1.14 clauses inuse deleted: 0
% 0.74/1.14
% 0.74/1.14 subsentry: 278
% 0.74/1.14 literals s-matched: 159
% 0.74/1.14 literals matched: 159
% 0.74/1.14 full subsumption: 0
% 0.74/1.14
% 0.74/1.14 checksum: 1795896883
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 Bliksem ended
%------------------------------------------------------------------------------