%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SEU241+1 : TPTP v8.1.0. Released v3.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 Jul 19 07:11:48 EDT 2022
% Result : Theorem 9.93s 10.29s
% Output : Refutation 9.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU241+1 : TPTP v8.1.0. Released v3.3.0.
% 0.03/0.13 % Command : bliksem %s
% 0.12/0.34 % Computer : n011.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % DateTime : Sun Jun 19 23:03:39 EDT 2022
% 0.12/0.34 % CPUTime :
% 2.10/2.44 *** allocated 10000 integers for termspace/termends
% 2.10/2.44 *** allocated 10000 integers for clauses
% 2.10/2.44 *** allocated 10000 integers for justifications
% 2.10/2.44 Bliksem 1.12
% 2.10/2.44
% 2.10/2.44
% 2.10/2.44 Automatic Strategy Selection
% 2.10/2.44
% 2.10/2.44
% 2.10/2.44 Clauses:
% 2.10/2.44
% 2.10/2.44 { ! in( X, Y ), ! in( Y, X ) }.
% 2.10/2.44 { ! empty( X ), function( X ) }.
% 2.10/2.44 { ! relation( X ), ! empty( X ), ! function( X ), relation( X ) }.
% 2.10/2.44 { ! relation( X ), ! empty( X ), ! function( X ), function( X ) }.
% 2.10/2.44 { ! relation( X ), ! empty( X ), ! function( X ), one_to_one( X ) }.
% 2.10/2.44 { unordered_pair( X, Y ) = unordered_pair( Y, X ) }.
% 2.10/2.44 { set_union2( X, Y ) = set_union2( Y, X ) }.
% 2.10/2.44 { ! relation( X ), ! antisymmetric( X ), is_antisymmetric_in( X,
% 2.10/2.44 relation_field( X ) ) }.
% 2.10/2.44 { ! relation( X ), ! is_antisymmetric_in( X, relation_field( X ) ),
% 2.10/2.44 antisymmetric( X ) }.
% 2.10/2.44 { ! relation( X ), ! is_antisymmetric_in( X, Y ), ! alpha3( X, Y, Z, T ), Z
% 2.10/2.44 = T }.
% 2.10/2.44 { ! relation( X ), alpha3( X, Y, skol1( X, Y ), skol10( X, Y ) ),
% 2.10/2.44 is_antisymmetric_in( X, Y ) }.
% 2.10/2.44 { ! relation( X ), ! skol1( X, Y ) = skol10( X, Y ), is_antisymmetric_in( X
% 2.10/2.44 , Y ) }.
% 2.10/2.44 { ! alpha3( X, Y, Z, T ), in( Z, Y ) }.
% 2.10/2.44 { ! alpha3( X, Y, Z, T ), alpha4( X, Y, Z, T ) }.
% 2.10/2.44 { ! in( Z, Y ), ! alpha4( X, Y, Z, T ), alpha3( X, Y, Z, T ) }.
% 2.10/2.44 { ! alpha4( X, Y, Z, T ), in( T, Y ) }.
% 2.10/2.44 { ! alpha4( X, Y, Z, T ), alpha1( X, Z, T ) }.
% 2.10/2.44 { ! in( T, Y ), ! alpha1( X, Z, T ), alpha4( X, Y, Z, T ) }.
% 2.10/2.44 { ! alpha1( X, Y, Z ), in( ordered_pair( Y, Z ), X ) }.
% 2.10/2.44 { ! alpha1( X, Y, Z ), in( ordered_pair( Z, Y ), X ) }.
% 2.10/2.44 { ! in( ordered_pair( Y, Z ), X ), ! in( ordered_pair( Z, Y ), X ), alpha1
% 2.10/2.44 ( X, Y, Z ) }.
% 2.10/2.44 { ordered_pair( X, Y ) = unordered_pair( unordered_pair( X, Y ), singleton
% 2.10/2.44 ( X ) ) }.
% 2.10/2.44 { ! relation( X ), relation_field( X ) = set_union2( relation_dom( X ),
% 2.10/2.44 relation_rng( X ) ) }.
% 2.10/2.44 { && }.
% 2.10/2.44 { && }.
% 2.10/2.44 { && }.
% 2.10/2.44 { && }.
% 2.10/2.44 { && }.
% 2.10/2.44 { && }.
% 2.10/2.44 { && }.
% 2.10/2.44 { && }.
% 2.10/2.44 { && }.
% 2.10/2.44 { element( skol2( X ), X ) }.
% 2.10/2.44 { empty( empty_set ) }.
% 2.10/2.44 { ! empty( ordered_pair( X, Y ) ) }.
% 2.10/2.44 { empty( X ), ! empty( set_union2( X, Y ) ) }.
% 2.10/2.44 { empty( X ), ! empty( set_union2( Y, X ) ) }.
% 2.10/2.44 { set_union2( X, X ) = X }.
% 2.10/2.44 { relation( skol3 ) }.
% 2.10/2.44 { alpha5( skol3 ), ! alpha2( skol3, X, Y ), X = Y }.
% 2.10/2.44 { alpha5( skol3 ), ! antisymmetric( skol3 ) }.
% 2.10/2.44 { ! alpha5( X ), antisymmetric( X ) }.
% 2.10/2.44 { ! alpha5( X ), alpha2( X, skol4( X ), skol11( X ) ) }.
% 2.10/2.44 { ! alpha5( X ), ! skol4( X ) = skol11( X ) }.
% 2.10/2.44 { ! antisymmetric( X ), ! alpha2( X, Y, Z ), Y = Z, alpha5( X ) }.
% 2.10/2.44 { ! alpha2( X, Y, Z ), in( ordered_pair( Y, Z ), X ) }.
% 2.10/2.44 { ! alpha2( X, Y, Z ), in( ordered_pair( Z, Y ), X ) }.
% 2.10/2.44 { ! in( ordered_pair( Y, Z ), X ), ! in( ordered_pair( Z, Y ), X ), alpha2
% 2.10/2.44 ( X, Y, Z ) }.
% 2.10/2.44 { relation( skol5 ) }.
% 2.10/2.44 { function( skol5 ) }.
% 2.10/2.44 { empty( skol6 ) }.
% 2.10/2.44 { relation( skol7 ) }.
% 2.10/2.44 { empty( skol7 ) }.
% 2.10/2.44 { function( skol7 ) }.
% 2.10/2.44 { ! empty( skol8 ) }.
% 2.10/2.44 { relation( skol9 ) }.
% 2.10/2.44 { function( skol9 ) }.
% 2.10/2.44 { one_to_one( skol9 ) }.
% 2.10/2.44 { set_union2( X, empty_set ) = X }.
% 2.10/2.44 { ! in( X, Y ), element( X, Y ) }.
% 2.10/2.44 { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 2.10/2.44 { ! relation( X ), ! in( ordered_pair( Y, Z ), X ), in( Y, relation_field(
% 2.10/2.44 X ) ) }.
% 2.10/2.44 { ! relation( X ), ! in( ordered_pair( Y, Z ), X ), in( Z, relation_field(
% 2.10/2.44 X ) ) }.
% 2.10/2.44 { ! empty( X ), X = empty_set }.
% 2.10/2.44 { ! in( X, Y ), ! empty( Y ) }.
% 2.10/2.44 { ! empty( X ), X = Y, ! empty( Y ) }.
% 2.10/2.44
% 2.10/2.44 percentage equality = 0.117117, percentage horn = 0.928571
% 2.10/2.44 This is a problem with some equality
% 2.10/2.44
% 2.10/2.44
% 2.10/2.44
% 2.10/2.44 Options Used:
% 2.10/2.44
% 2.10/2.44 useres = 1
% 2.10/2.44 useparamod = 1
% 2.10/2.44 useeqrefl = 1
% 2.10/2.44 useeqfact = 1
% 2.10/2.44 usefactor = 1
% 2.10/2.44 usesimpsplitting = 0
% 2.10/2.44 usesimpdemod = 5
% 2.10/2.44 usesimpres = 3
% 2.10/2.44
% 2.10/2.44 resimpinuse = 1000
% 2.10/2.44 resimpclauses = 20000
% 2.10/2.44 substype = eqrewr
% 2.10/2.44 backwardsubs = 1
% 2.10/2.44 selectoldest = 5
% 2.10/2.44
% 2.10/2.44 litorderings [0] = split
% 2.10/2.44 litorderings [1] = extend the termordering, first sorting on arguments
% 2.10/2.44
% 2.10/2.44 termordering = kbo
% 2.10/2.44
% 2.10/2.44 litapriori = 0
% 2.10/2.44 termapriori = 1
% 2.10/2.44 litaposteriori = 0
% 2.10/2.44 termaposteriori = 0
% 2.10/2.44 demodaposteriori = 0
% 2.10/2.44 ordereqreflfact = 0
% 2.10/2.44
% 2.10/2.44 litselect = negord
% 2.10/2.44
% 2.10/2.44 maxweight = 15
% 2.10/2.44 maxdepth = 30000
% 2.10/2.44 maxlength = 115
% 2.10/2.44 maxnrvars = 195
% 2.10/2.44 excuselevel = 1
% 2.10/2.44 increasemaxweight = 1
% 2.10/2.44
% 2.10/2.44 maxselected = 10000000
% 2.10/2.44 maxnrclauses = 10000000
% 2.10/2.44
% 2.10/2.44 showgenerated = 0
% 2.10/2.44 showkept = 0
% 9.93/10.29 showselected = 0
% 9.93/10.29 showdeleted = 0
% 9.93/10.29 showresimp = 1
% 9.93/10.29 showstatus = 2000
% 9.93/10.29
% 9.93/10.29 prologoutput = 0
% 9.93/10.29 nrgoals = 5000000
% 9.93/10.29 totalproof = 1
% 9.93/10.29
% 9.93/10.29 Symbols occurring in the translation:
% 9.93/10.29
% 9.93/10.29 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 9.93/10.29 . [1, 2] (w:1, o:35, a:1, s:1, b:0),
% 9.93/10.29 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 9.93/10.29 ! [4, 1] (w:0, o:17, a:1, s:1, b:0),
% 9.93/10.29 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 9.93/10.29 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 9.93/10.29 in [37, 2] (w:1, o:59, a:1, s:1, b:0),
% 9.93/10.29 empty [38, 1] (w:1, o:22, a:1, s:1, b:0),
% 9.93/10.29 function [39, 1] (w:1, o:23, a:1, s:1, b:0),
% 9.93/10.29 relation [40, 1] (w:1, o:24, a:1, s:1, b:0),
% 9.93/10.29 one_to_one [41, 1] (w:1, o:25, a:1, s:1, b:0),
% 9.93/10.29 unordered_pair [42, 2] (w:1, o:60, a:1, s:1, b:0),
% 9.93/10.29 set_union2 [43, 2] (w:1, o:61, a:1, s:1, b:0),
% 9.93/10.29 antisymmetric [44, 1] (w:1, o:26, a:1, s:1, b:0),
% 9.93/10.29 relation_field [45, 1] (w:1, o:27, a:1, s:1, b:0),
% 9.93/10.29 is_antisymmetric_in [46, 2] (w:1, o:62, a:1, s:1, b:0),
% 9.93/10.29 ordered_pair [49, 2] (w:1, o:63, a:1, s:1, b:0),
% 9.93/10.29 singleton [50, 1] (w:1, o:30, a:1, s:1, b:0),
% 9.93/10.29 relation_dom [51, 1] (w:1, o:28, a:1, s:1, b:0),
% 9.93/10.29 relation_rng [52, 1] (w:1, o:29, a:1, s:1, b:0),
% 9.93/10.29 element [53, 2] (w:1, o:64, a:1, s:1, b:0),
% 9.93/10.29 empty_set [54, 0] (w:1, o:10, a:1, s:1, b:0),
% 9.93/10.29 alpha1 [55, 3] (w:1, o:67, a:1, s:1, b:1),
% 9.93/10.29 alpha2 [56, 3] (w:1, o:68, a:1, s:1, b:1),
% 9.93/10.29 alpha3 [57, 4] (w:1, o:69, a:1, s:1, b:1),
% 9.93/10.29 alpha4 [58, 4] (w:1, o:70, a:1, s:1, b:1),
% 9.93/10.29 alpha5 [59, 1] (w:1, o:31, a:1, s:1, b:1),
% 9.93/10.29 skol1 [60, 2] (w:1, o:65, a:1, s:1, b:1),
% 9.93/10.29 skol2 [61, 1] (w:1, o:33, a:1, s:1, b:1),
% 9.93/10.29 skol3 [62, 0] (w:1, o:11, a:1, s:1, b:1),
% 9.93/10.29 skol4 [63, 1] (w:1, o:34, a:1, s:1, b:1),
% 9.93/10.29 skol5 [64, 0] (w:1, o:12, a:1, s:1, b:1),
% 9.93/10.29 skol6 [65, 0] (w:1, o:13, a:1, s:1, b:1),
% 9.93/10.29 skol7 [66, 0] (w:1, o:14, a:1, s:1, b:1),
% 9.93/10.29 skol8 [67, 0] (w:1, o:15, a:1, s:1, b:1),
% 9.93/10.29 skol9 [68, 0] (w:1, o:16, a:1, s:1, b:1),
% 9.93/10.29 skol10 [69, 2] (w:1, o:66, a:1, s:1, b:1),
% 9.93/10.29 skol11 [70, 1] (w:1, o:32, a:1, s:1, b:1).
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Starting Search:
% 9.93/10.29
% 9.93/10.29 *** allocated 15000 integers for clauses
% 9.93/10.29 *** allocated 22500 integers for clauses
% 9.93/10.29 *** allocated 33750 integers for clauses
% 9.93/10.29 *** allocated 50625 integers for clauses
% 9.93/10.29 *** allocated 15000 integers for termspace/termends
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 22500 integers for termspace/termends
% 9.93/10.29 *** allocated 75937 integers for clauses
% 9.93/10.29 *** allocated 33750 integers for termspace/termends
% 9.93/10.29 *** allocated 113905 integers for clauses
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 5164
% 9.93/10.29 Kept: 2240
% 9.93/10.29 Inuse: 205
% 9.93/10.29 Deleted: 37
% 9.93/10.29 Deletedinuse: 26
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 50625 integers for termspace/termends
% 9.93/10.29 *** allocated 170857 integers for clauses
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 75937 integers for termspace/termends
% 9.93/10.29 *** allocated 256285 integers for clauses
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 13515
% 9.93/10.29 Kept: 4275
% 9.93/10.29 Inuse: 277
% 9.93/10.29 Deleted: 58
% 9.93/10.29 Deletedinuse: 26
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 113905 integers for termspace/termends
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 384427 integers for clauses
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 26840
% 9.93/10.29 Kept: 6280
% 9.93/10.29 Inuse: 442
% 9.93/10.29 Deleted: 75
% 9.93/10.29 Deletedinuse: 28
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 170857 integers for termspace/termends
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 41539
% 9.93/10.29 Kept: 8283
% 9.93/10.29 Inuse: 597
% 9.93/10.29 Deleted: 81
% 9.93/10.29 Deletedinuse: 28
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 576640 integers for clauses
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 51596
% 9.93/10.29 Kept: 10285
% 9.93/10.29 Inuse: 669
% 9.93/10.29 Deleted: 86
% 9.93/10.29 Deletedinuse: 28
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 256285 integers for termspace/termends
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 63037
% 9.93/10.29 Kept: 12314
% 9.93/10.29 Inuse: 730
% 9.93/10.29 Deleted: 129
% 9.93/10.29 Deletedinuse: 28
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 864960 integers for clauses
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 75751
% 9.93/10.29 Kept: 14340
% 9.93/10.29 Inuse: 812
% 9.93/10.29 Deleted: 137
% 9.93/10.29 Deletedinuse: 28
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 87938
% 9.93/10.29 Kept: 16365
% 9.93/10.29 Inuse: 909
% 9.93/10.29 Deleted: 161
% 9.93/10.29 Deletedinuse: 44
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 384427 integers for termspace/termends
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 103312
% 9.93/10.29 Kept: 18424
% 9.93/10.29 Inuse: 966
% 9.93/10.29 Deleted: 163
% 9.93/10.29 Deletedinuse: 44
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying clauses:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 118365
% 9.93/10.29 Kept: 20435
% 9.93/10.29 Inuse: 1014
% 9.93/10.29 Deleted: 1550
% 9.93/10.29 Deletedinuse: 60
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 1297440 integers for clauses
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 130373
% 9.93/10.29 Kept: 22490
% 9.93/10.29 Inuse: 1060
% 9.93/10.29 Deleted: 1550
% 9.93/10.29 Deletedinuse: 60
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 142655
% 9.93/10.29 Kept: 25868
% 9.93/10.29 Inuse: 1095
% 9.93/10.29 Deleted: 1550
% 9.93/10.29 Deletedinuse: 60
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 576640 integers for termspace/termends
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 156278
% 9.93/10.29 Kept: 29391
% 9.93/10.29 Inuse: 1141
% 9.93/10.29 Deleted: 1550
% 9.93/10.29 Deletedinuse: 60
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 166191
% 9.93/10.29 Kept: 31503
% 9.93/10.29 Inuse: 1191
% 9.93/10.29 Deleted: 1550
% 9.93/10.29 Deletedinuse: 60
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 1946160 integers for clauses
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 179590
% 9.93/10.29 Kept: 33547
% 9.93/10.29 Inuse: 1274
% 9.93/10.29 Deleted: 1550
% 9.93/10.29 Deletedinuse: 60
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 192713
% 9.93/10.29 Kept: 35744
% 9.93/10.29 Inuse: 1331
% 9.93/10.29 Deleted: 1550
% 9.93/10.29 Deletedinuse: 60
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 196649
% 9.93/10.29 Kept: 38150
% 9.93/10.29 Inuse: 1332
% 9.93/10.29 Deleted: 1550
% 9.93/10.29 Deletedinuse: 60
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 864960 integers for termspace/termends
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying clauses:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 222817
% 9.93/10.29 Kept: 40222
% 9.93/10.29 Inuse: 1409
% 9.93/10.29 Deleted: 2504
% 9.93/10.29 Deletedinuse: 60
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 258003
% 9.93/10.29 Kept: 42239
% 9.93/10.29 Inuse: 1495
% 9.93/10.29 Deleted: 2504
% 9.93/10.29 Deletedinuse: 60
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 277246
% 9.93/10.29 Kept: 44274
% 9.93/10.29 Inuse: 1573
% 9.93/10.29 Deleted: 3084
% 9.93/10.29 Deletedinuse: 634
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 285609
% 9.93/10.29 Kept: 46278
% 9.93/10.29 Inuse: 1647
% 9.93/10.29 Deleted: 3141
% 9.93/10.29 Deletedinuse: 674
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29 *** allocated 2919240 integers for clauses
% 9.93/10.29
% 9.93/10.29 Intermediate Status:
% 9.93/10.29 Generated: 294268
% 9.93/10.29 Kept: 48965
% 9.93/10.29 Inuse: 1674
% 9.93/10.29 Deleted: 3146
% 9.93/10.29 Deletedinuse: 674
% 9.93/10.29
% 9.93/10.29 Resimplifying inuse:
% 9.93/10.29 Done
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Bliksems!, er is een bewijs:
% 9.93/10.29 % SZS status Theorem
% 9.93/10.29 % SZS output start Refutation
% 9.93/10.29
% 9.93/10.29 (5) {G0,W8,D3,L3,V1,M3} I { ! relation( X ), ! antisymmetric( X ),
% 9.93/10.29 is_antisymmetric_in( X, relation_field( X ) ) }.
% 9.93/10.29 (6) {G0,W8,D3,L3,V1,M3} I { ! relation( X ), ! is_antisymmetric_in( X,
% 9.93/10.29 relation_field( X ) ), antisymmetric( X ) }.
% 9.93/10.29 (7) {G0,W13,D2,L4,V4,M4} I { ! relation( X ), ! is_antisymmetric_in( X, Y )
% 9.93/10.29 , ! alpha3( X, Y, Z, T ), Z = T }.
% 9.93/10.29 (8) {G0,W14,D3,L3,V2,M3} I { ! relation( X ), alpha3( X, Y, skol1( X, Y ),
% 9.93/10.29 skol10( X, Y ) ), is_antisymmetric_in( X, Y ) }.
% 9.93/10.29 (9) {G0,W12,D3,L3,V2,M3} I { ! relation( X ), ! skol10( X, Y ) ==> skol1( X
% 9.93/10.29 , Y ), is_antisymmetric_in( X, Y ) }.
% 9.93/10.29 (11) {G0,W10,D2,L2,V4,M2} I { ! alpha3( X, Y, Z, T ), alpha4( X, Y, Z, T )
% 9.93/10.29 }.
% 9.93/10.29 (12) {G0,W13,D2,L3,V4,M3} I { ! in( Z, Y ), ! alpha4( X, Y, Z, T ), alpha3
% 9.93/10.29 ( X, Y, Z, T ) }.
% 9.93/10.29 (14) {G0,W9,D2,L2,V4,M2} I { ! alpha4( X, Y, Z, T ), alpha1( X, Z, T ) }.
% 9.93/10.29 (15) {G0,W12,D2,L3,V4,M3} I { ! in( T, Y ), ! alpha1( X, Z, T ), alpha4( X
% 9.93/10.29 , Y, Z, T ) }.
% 9.93/10.29 (16) {G0,W9,D3,L2,V3,M2} I { ! alpha1( X, Y, Z ), in( ordered_pair( Y, Z )
% 9.93/10.29 , X ) }.
% 9.93/10.29 (17) {G0,W9,D3,L2,V3,M2} I { ! alpha1( X, Y, Z ), in( ordered_pair( Z, Y )
% 9.93/10.29 , X ) }.
% 9.93/10.29 (18) {G0,W14,D3,L3,V3,M3} I { ! in( ordered_pair( Y, Z ), X ), ! in(
% 9.93/10.29 ordered_pair( Z, Y ), X ), alpha1( X, Y, Z ) }.
% 9.93/10.29 (28) {G0,W2,D2,L1,V0,M1} I { relation( skol3 ) }.
% 9.93/10.29 (29) {G0,W9,D2,L3,V2,M3} I { alpha5( skol3 ), ! alpha2( skol3, X, Y ), X =
% 9.93/10.29 Y }.
% 9.93/10.29 (30) {G0,W4,D2,L2,V0,M2} I { alpha5( skol3 ), ! antisymmetric( skol3 ) }.
% 9.93/10.29 (31) {G0,W4,D2,L2,V1,M2} I { ! alpha5( X ), antisymmetric( X ) }.
% 9.93/10.29 (32) {G0,W8,D3,L2,V1,M2} I { ! alpha5( X ), alpha2( X, skol4( X ), skol11(
% 9.93/10.29 X ) ) }.
% 9.93/10.29 (33) {G0,W7,D3,L2,V1,M2} I { ! alpha5( X ), ! skol4( X ) ==> skol11( X )
% 9.93/10.29 }.
% 9.93/10.29 (35) {G0,W9,D3,L2,V3,M2} I { ! alpha2( X, Y, Z ), in( ordered_pair( Y, Z )
% 9.93/10.29 , X ) }.
% 9.93/10.29 (36) {G0,W9,D3,L2,V3,M2} I { ! alpha2( X, Y, Z ), in( ordered_pair( Z, Y )
% 9.93/10.29 , X ) }.
% 9.93/10.29 (37) {G0,W14,D3,L3,V3,M3} I { ! in( ordered_pair( Y, Z ), X ), ! in(
% 9.93/10.29 ordered_pair( Z, Y ), X ), alpha2( X, Y, Z ) }.
% 9.93/10.29 (51) {G0,W11,D3,L3,V3,M3} I { ! relation( X ), ! in( ordered_pair( Y, Z ),
% 9.93/10.29 X ), in( Y, relation_field( X ) ) }.
% 9.93/10.29 (52) {G0,W11,D3,L3,V3,M3} I { ! relation( X ), ! in( ordered_pair( Y, Z ),
% 9.93/10.29 X ), in( Z, relation_field( X ) ) }.
% 9.93/10.29 (75) {G1,W6,D3,L2,V0,M2} R(6,28) { ! is_antisymmetric_in( skol3,
% 9.93/10.29 relation_field( skol3 ) ), antisymmetric( skol3 ) }.
% 9.93/10.29 (98) {G1,W13,D3,L4,V3,M4} R(7,5);f { ! relation( X ), ! alpha3( X,
% 9.93/10.29 relation_field( X ), Y, Z ), Y = Z, ! antisymmetric( X ) }.
% 9.93/10.29 (151) {G1,W12,D3,L2,V1,M2} R(8,28) { alpha3( skol3, X, skol1( skol3, X ),
% 9.93/10.29 skol10( skol3, X ) ), is_antisymmetric_in( skol3, X ) }.
% 9.93/10.29 (242) {G1,W9,D2,L2,V4,M2} R(14,11) { alpha1( X, Y, Z ), ! alpha3( X, T, Y,
% 9.93/10.29 Z ) }.
% 9.93/10.29 (551) {G1,W18,D3,L5,V3,M5} P(29,9) { ! relation( X ), ! Z = skol1( X, Y ),
% 9.93/10.29 is_antisymmetric_in( X, Y ), alpha5( skol3 ), ! alpha2( skol3, Z, skol10
% 9.93/10.29 ( X, Y ) ) }.
% 9.93/10.29 (594) {G2,W15,D3,L4,V2,M4} Q(551) { ! relation( X ), is_antisymmetric_in( X
% 9.93/10.29 , Y ), alpha5( skol3 ), ! alpha2( skol3, skol1( X, Y ), skol10( X, Y ) )
% 9.93/10.29 }.
% 9.93/10.29 (617) {G1,W8,D3,L2,V0,M2} R(32,30) { alpha2( skol3, skol4( skol3 ), skol11
% 9.93/10.29 ( skol3 ) ), ! antisymmetric( skol3 ) }.
% 9.93/10.29 (644) {G1,W7,D3,L2,V0,M2} R(33,30) { ! skol4( skol3 ) ==> skol11( skol3 ),
% 9.93/10.29 ! antisymmetric( skol3 ) }.
% 9.93/10.29 (928) {G1,W8,D2,L2,V3,M2} R(35,18);r(36) { ! alpha2( X, Y, Z ), alpha1( X,
% 9.93/10.29 Y, Z ) }.
% 9.93/10.29 (998) {G1,W8,D2,L2,V3,M2} R(37,17);r(16) { alpha2( Z, X, Y ), ! alpha1( Z,
% 9.93/10.29 X, Y ) }.
% 9.93/10.29 (4824) {G2,W8,D3,L2,V1,M2} R(928,32) { alpha1( X, skol4( X ), skol11( X ) )
% 9.93/10.29 , ! alpha5( X ) }.
% 9.93/10.29 (10025) {G3,W8,D3,L2,V0,M2} R(4824,30) { alpha1( skol3, skol4( skol3 ),
% 9.93/10.29 skol11( skol3 ) ), ! antisymmetric( skol3 ) }.
% 9.93/10.29 (10814) {G2,W9,D2,L2,V4,M2} R(242,998) { ! alpha3( X, Y, Z, T ), alpha2( X
% 9.93/10.29 , Z, T ) }.
% 9.93/10.29 (26922) {G3,W11,D3,L2,V1,M2} R(10814,151) { alpha2( skol3, skol1( skol3, X
% 9.93/10.29 ), skol10( skol3, X ) ), is_antisymmetric_in( skol3, X ) }.
% 9.93/10.29 (43361) {G4,W5,D2,L2,V1,M2} R(594,28);r(26922) { is_antisymmetric_in( skol3
% 9.93/10.29 , X ), alpha5( skol3 ) }.
% 9.93/10.29 (43374) {G5,W2,D2,L1,V0,M1} R(43361,75);r(31) { antisymmetric( skol3 ) }.
% 9.93/10.29 (43393) {G6,W6,D3,L1,V0,M1} R(43374,617) { alpha2( skol3, skol4( skol3 ),
% 9.93/10.29 skol11( skol3 ) ) }.
% 9.93/10.29 (43395) {G6,W6,D3,L1,V0,M1} R(43374,10025) { alpha1( skol3, skol4( skol3 )
% 9.93/10.29 , skol11( skol3 ) ) }.
% 9.93/10.29 (43397) {G6,W5,D3,L1,V0,M1} R(43374,644) { ! skol4( skol3 ) ==> skol11(
% 9.93/10.29 skol3 ) }.
% 9.93/10.29 (43400) {G6,W9,D3,L2,V2,M2} R(43374,98);r(28) { ! alpha3( skol3,
% 9.93/10.29 relation_field( skol3 ), X, Y ), X = Y }.
% 9.93/10.29 (43584) {G7,W7,D4,L1,V0,M1} R(43393,36) { in( ordered_pair( skol11( skol3 )
% 9.93/10.29 , skol4( skol3 ) ), skol3 ) }.
% 9.93/10.29 (44201) {G8,W5,D3,L1,V0,M1} R(43584,52);r(28) { in( skol4( skol3 ),
% 9.93/10.29 relation_field( skol3 ) ) }.
% 9.93/10.29 (44202) {G8,W5,D3,L1,V0,M1} R(43584,51);r(28) { in( skol11( skol3 ),
% 9.93/10.29 relation_field( skol3 ) ) }.
% 9.93/10.29 (46903) {G7,W11,D3,L2,V1,M2} P(43400,43397) { ! X = skol11( skol3 ), !
% 9.93/10.29 alpha3( skol3, relation_field( skol3 ), skol4( skol3 ), X ) }.
% 9.93/10.29 (48948) {G8,W8,D3,L1,V0,M1} Q(46903) { ! alpha3( skol3, relation_field(
% 9.93/10.29 skol3 ), skol4( skol3 ), skol11( skol3 ) ) }.
% 9.93/10.29 (48980) {G9,W8,D3,L1,V0,M1} R(48948,12);r(44201) { ! alpha4( skol3,
% 9.93/10.29 relation_field( skol3 ), skol4( skol3 ), skol11( skol3 ) ) }.
% 9.93/10.29 (48985) {G10,W6,D3,L1,V0,M1} R(48980,15);r(44202) { ! alpha1( skol3, skol4
% 9.93/10.29 ( skol3 ), skol11( skol3 ) ) }.
% 9.93/10.29 (48986) {G11,W0,D0,L0,V0,M0} S(48985);r(43395) { }.
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 % SZS output end Refutation
% 9.93/10.29 found a proof!
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Unprocessed initial clauses:
% 9.93/10.29
% 9.93/10.29 (48988) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), ! in( Y, X ) }.
% 9.93/10.29 (48989) {G0,W4,D2,L2,V1,M2} { ! empty( X ), function( X ) }.
% 9.93/10.29 (48990) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 9.93/10.29 ), relation( X ) }.
% 9.93/10.29 (48991) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 9.93/10.29 ), function( X ) }.
% 9.93/10.29 (48992) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 9.93/10.29 ), one_to_one( X ) }.
% 9.93/10.29 (48993) {G0,W7,D3,L1,V2,M1} { unordered_pair( X, Y ) = unordered_pair( Y,
% 9.93/10.29 X ) }.
% 9.93/10.29 (48994) {G0,W7,D3,L1,V2,M1} { set_union2( X, Y ) = set_union2( Y, X ) }.
% 9.93/10.29 (48995) {G0,W8,D3,L3,V1,M3} { ! relation( X ), ! antisymmetric( X ),
% 9.93/10.29 is_antisymmetric_in( X, relation_field( X ) ) }.
% 9.93/10.29 (48996) {G0,W8,D3,L3,V1,M3} { ! relation( X ), ! is_antisymmetric_in( X,
% 9.93/10.29 relation_field( X ) ), antisymmetric( X ) }.
% 9.93/10.29 (48997) {G0,W13,D2,L4,V4,M4} { ! relation( X ), ! is_antisymmetric_in( X,
% 9.93/10.29 Y ), ! alpha3( X, Y, Z, T ), Z = T }.
% 9.93/10.29 (48998) {G0,W14,D3,L3,V2,M3} { ! relation( X ), alpha3( X, Y, skol1( X, Y
% 9.93/10.29 ), skol10( X, Y ) ), is_antisymmetric_in( X, Y ) }.
% 9.93/10.29 (48999) {G0,W12,D3,L3,V2,M3} { ! relation( X ), ! skol1( X, Y ) = skol10(
% 9.93/10.29 X, Y ), is_antisymmetric_in( X, Y ) }.
% 9.93/10.29 (49000) {G0,W8,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), in( Z, Y ) }.
% 9.93/10.29 (49001) {G0,W10,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), alpha4( X, Y, Z, T
% 9.93/10.29 ) }.
% 9.93/10.29 (49002) {G0,W13,D2,L3,V4,M3} { ! in( Z, Y ), ! alpha4( X, Y, Z, T ),
% 9.93/10.29 alpha3( X, Y, Z, T ) }.
% 9.93/10.29 (49003) {G0,W8,D2,L2,V4,M2} { ! alpha4( X, Y, Z, T ), in( T, Y ) }.
% 9.93/10.29 (49004) {G0,W9,D2,L2,V4,M2} { ! alpha4( X, Y, Z, T ), alpha1( X, Z, T )
% 9.93/10.29 }.
% 9.93/10.29 (49005) {G0,W12,D2,L3,V4,M3} { ! in( T, Y ), ! alpha1( X, Z, T ), alpha4(
% 9.93/10.29 X, Y, Z, T ) }.
% 9.93/10.29 (49006) {G0,W9,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), in( ordered_pair( Y, Z
% 9.93/10.29 ), X ) }.
% 9.93/10.29 (49007) {G0,W9,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), in( ordered_pair( Z, Y
% 9.93/10.29 ), X ) }.
% 9.93/10.29 (49008) {G0,W14,D3,L3,V3,M3} { ! in( ordered_pair( Y, Z ), X ), ! in(
% 9.93/10.29 ordered_pair( Z, Y ), X ), alpha1( X, Y, Z ) }.
% 9.93/10.29 (49009) {G0,W10,D4,L1,V2,M1} { ordered_pair( X, Y ) = unordered_pair(
% 9.93/10.29 unordered_pair( X, Y ), singleton( X ) ) }.
% 9.93/10.29 (49010) {G0,W10,D4,L2,V1,M2} { ! relation( X ), relation_field( X ) =
% 9.93/10.29 set_union2( relation_dom( X ), relation_rng( X ) ) }.
% 9.93/10.29 (49011) {G0,W1,D1,L1,V0,M1} { && }.
% 9.93/10.29 (49012) {G0,W1,D1,L1,V0,M1} { && }.
% 9.93/10.29 (49013) {G0,W1,D1,L1,V0,M1} { && }.
% 9.93/10.29 (49014) {G0,W1,D1,L1,V0,M1} { && }.
% 9.93/10.29 (49015) {G0,W1,D1,L1,V0,M1} { && }.
% 9.93/10.29 (49016) {G0,W1,D1,L1,V0,M1} { && }.
% 9.93/10.29 (49017) {G0,W1,D1,L1,V0,M1} { && }.
% 9.93/10.29 (49018) {G0,W1,D1,L1,V0,M1} { && }.
% 9.93/10.29 (49019) {G0,W1,D1,L1,V0,M1} { && }.
% 9.93/10.29 (49020) {G0,W4,D3,L1,V1,M1} { element( skol2( X ), X ) }.
% 9.93/10.29 (49021) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 9.93/10.29 (49022) {G0,W4,D3,L1,V2,M1} { ! empty( ordered_pair( X, Y ) ) }.
% 9.93/10.29 (49023) {G0,W6,D3,L2,V2,M2} { empty( X ), ! empty( set_union2( X, Y ) )
% 9.93/10.29 }.
% 9.93/10.29 (49024) {G0,W6,D3,L2,V2,M2} { empty( X ), ! empty( set_union2( Y, X ) )
% 9.93/10.29 }.
% 9.93/10.29 (49025) {G0,W5,D3,L1,V1,M1} { set_union2( X, X ) = X }.
% 9.93/10.29 (49026) {G0,W2,D2,L1,V0,M1} { relation( skol3 ) }.
% 9.93/10.29 (49027) {G0,W9,D2,L3,V2,M3} { alpha5( skol3 ), ! alpha2( skol3, X, Y ), X
% 9.93/10.29 = Y }.
% 9.93/10.29 (49028) {G0,W4,D2,L2,V0,M2} { alpha5( skol3 ), ! antisymmetric( skol3 )
% 9.93/10.29 }.
% 9.93/10.29 (49029) {G0,W4,D2,L2,V1,M2} { ! alpha5( X ), antisymmetric( X ) }.
% 9.93/10.29 (49030) {G0,W8,D3,L2,V1,M2} { ! alpha5( X ), alpha2( X, skol4( X ), skol11
% 9.93/10.29 ( X ) ) }.
% 9.93/10.29 (49031) {G0,W7,D3,L2,V1,M2} { ! alpha5( X ), ! skol4( X ) = skol11( X )
% 9.93/10.29 }.
% 9.93/10.29 (49032) {G0,W11,D2,L4,V3,M4} { ! antisymmetric( X ), ! alpha2( X, Y, Z ),
% 9.93/10.29 Y = Z, alpha5( X ) }.
% 9.93/10.29 (49033) {G0,W9,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), in( ordered_pair( Y, Z
% 9.93/10.29 ), X ) }.
% 9.93/10.29 (49034) {G0,W9,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), in( ordered_pair( Z, Y
% 9.93/10.29 ), X ) }.
% 9.93/10.29 (49035) {G0,W14,D3,L3,V3,M3} { ! in( ordered_pair( Y, Z ), X ), ! in(
% 9.93/10.29 ordered_pair( Z, Y ), X ), alpha2( X, Y, Z ) }.
% 9.93/10.29 (49036) {G0,W2,D2,L1,V0,M1} { relation( skol5 ) }.
% 9.93/10.29 (49037) {G0,W2,D2,L1,V0,M1} { function( skol5 ) }.
% 9.93/10.29 (49038) {G0,W2,D2,L1,V0,M1} { empty( skol6 ) }.
% 9.93/10.29 (49039) {G0,W2,D2,L1,V0,M1} { relation( skol7 ) }.
% 9.93/10.29 (49040) {G0,W2,D2,L1,V0,M1} { empty( skol7 ) }.
% 9.93/10.29 (49041) {G0,W2,D2,L1,V0,M1} { function( skol7 ) }.
% 9.93/10.29 (49042) {G0,W2,D2,L1,V0,M1} { ! empty( skol8 ) }.
% 9.93/10.29 (49043) {G0,W2,D2,L1,V0,M1} { relation( skol9 ) }.
% 9.93/10.29 (49044) {G0,W2,D2,L1,V0,M1} { function( skol9 ) }.
% 9.93/10.29 (49045) {G0,W2,D2,L1,V0,M1} { one_to_one( skol9 ) }.
% 9.93/10.29 (49046) {G0,W5,D3,L1,V1,M1} { set_union2( X, empty_set ) = X }.
% 9.93/10.29 (49047) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), element( X, Y ) }.
% 9.93/10.29 (49048) {G0,W8,D2,L3,V2,M3} { ! element( X, Y ), empty( Y ), in( X, Y )
% 9.93/10.29 }.
% 9.93/10.29 (49049) {G0,W11,D3,L3,V3,M3} { ! relation( X ), ! in( ordered_pair( Y, Z )
% 9.93/10.29 , X ), in( Y, relation_field( X ) ) }.
% 9.93/10.29 (49050) {G0,W11,D3,L3,V3,M3} { ! relation( X ), ! in( ordered_pair( Y, Z )
% 9.93/10.29 , X ), in( Z, relation_field( X ) ) }.
% 9.93/10.29 (49051) {G0,W5,D2,L2,V1,M2} { ! empty( X ), X = empty_set }.
% 9.93/10.29 (49052) {G0,W5,D2,L2,V2,M2} { ! in( X, Y ), ! empty( Y ) }.
% 9.93/10.29 (49053) {G0,W7,D2,L3,V2,M3} { ! empty( X ), X = Y, ! empty( Y ) }.
% 9.93/10.29
% 9.93/10.29
% 9.93/10.29 Total Proof:
% 9.93/10.29
% 9.93/10.29 subsumption: (5) {G0,W8,D3,L3,V1,M3} I { ! relation( X ), ! antisymmetric(
% 9.93/10.29 X ), is_antisymmetric_in( X, relation_field( X ) ) }.
% 9.93/10.29 parent0: (48995) {G0,W8,D3,L3,V1,M3} { ! relation( X ), ! antisymmetric( X
% 9.93/10.29 ), is_antisymmetric_in( X, relation_field( X ) ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 2 ==> 2
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (6) {G0,W8,D3,L3,V1,M3} I { ! relation( X ), !
% 9.93/10.29 is_antisymmetric_in( X, relation_field( X ) ), antisymmetric( X ) }.
% 9.93/10.29 parent0: (48996) {G0,W8,D3,L3,V1,M3} { ! relation( X ), !
% 9.93/10.29 is_antisymmetric_in( X, relation_field( X ) ), antisymmetric( X ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 2 ==> 2
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (7) {G0,W13,D2,L4,V4,M4} I { ! relation( X ), !
% 9.93/10.29 is_antisymmetric_in( X, Y ), ! alpha3( X, Y, Z, T ), Z = T }.
% 9.93/10.29 parent0: (48997) {G0,W13,D2,L4,V4,M4} { ! relation( X ), !
% 9.93/10.29 is_antisymmetric_in( X, Y ), ! alpha3( X, Y, Z, T ), Z = T }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 T := T
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 2 ==> 2
% 9.93/10.29 3 ==> 3
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (8) {G0,W14,D3,L3,V2,M3} I { ! relation( X ), alpha3( X, Y,
% 9.93/10.29 skol1( X, Y ), skol10( X, Y ) ), is_antisymmetric_in( X, Y ) }.
% 9.93/10.29 parent0: (48998) {G0,W14,D3,L3,V2,M3} { ! relation( X ), alpha3( X, Y,
% 9.93/10.29 skol1( X, Y ), skol10( X, Y ) ), is_antisymmetric_in( X, Y ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 2 ==> 2
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 eqswap: (49062) {G0,W12,D3,L3,V2,M3} { ! skol10( X, Y ) = skol1( X, Y ), !
% 9.93/10.29 relation( X ), is_antisymmetric_in( X, Y ) }.
% 9.93/10.29 parent0[1]: (48999) {G0,W12,D3,L3,V2,M3} { ! relation( X ), ! skol1( X, Y
% 9.93/10.29 ) = skol10( X, Y ), is_antisymmetric_in( X, Y ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (9) {G0,W12,D3,L3,V2,M3} I { ! relation( X ), ! skol10( X, Y )
% 9.93/10.29 ==> skol1( X, Y ), is_antisymmetric_in( X, Y ) }.
% 9.93/10.29 parent0: (49062) {G0,W12,D3,L3,V2,M3} { ! skol10( X, Y ) = skol1( X, Y ),
% 9.93/10.29 ! relation( X ), is_antisymmetric_in( X, Y ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 1
% 9.93/10.29 1 ==> 0
% 9.93/10.29 2 ==> 2
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (11) {G0,W10,D2,L2,V4,M2} I { ! alpha3( X, Y, Z, T ), alpha4(
% 9.93/10.29 X, Y, Z, T ) }.
% 9.93/10.29 parent0: (49001) {G0,W10,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), alpha4( X
% 9.93/10.29 , Y, Z, T ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 T := T
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (12) {G0,W13,D2,L3,V4,M3} I { ! in( Z, Y ), ! alpha4( X, Y, Z
% 9.93/10.29 , T ), alpha3( X, Y, Z, T ) }.
% 9.93/10.29 parent0: (49002) {G0,W13,D2,L3,V4,M3} { ! in( Z, Y ), ! alpha4( X, Y, Z, T
% 9.93/10.29 ), alpha3( X, Y, Z, T ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 T := T
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 2 ==> 2
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (14) {G0,W9,D2,L2,V4,M2} I { ! alpha4( X, Y, Z, T ), alpha1( X
% 9.93/10.29 , Z, T ) }.
% 9.93/10.29 parent0: (49004) {G0,W9,D2,L2,V4,M2} { ! alpha4( X, Y, Z, T ), alpha1( X,
% 9.93/10.29 Z, T ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 T := T
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (15) {G0,W12,D2,L3,V4,M3} I { ! in( T, Y ), ! alpha1( X, Z, T
% 9.93/10.29 ), alpha4( X, Y, Z, T ) }.
% 9.93/10.29 parent0: (49005) {G0,W12,D2,L3,V4,M3} { ! in( T, Y ), ! alpha1( X, Z, T )
% 9.93/10.29 , alpha4( X, Y, Z, T ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 T := T
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 2 ==> 2
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (16) {G0,W9,D3,L2,V3,M2} I { ! alpha1( X, Y, Z ), in(
% 9.93/10.29 ordered_pair( Y, Z ), X ) }.
% 9.93/10.29 parent0: (49006) {G0,W9,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), in(
% 9.93/10.29 ordered_pair( Y, Z ), X ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (17) {G0,W9,D3,L2,V3,M2} I { ! alpha1( X, Y, Z ), in(
% 9.93/10.29 ordered_pair( Z, Y ), X ) }.
% 9.93/10.29 parent0: (49007) {G0,W9,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), in(
% 9.93/10.29 ordered_pair( Z, Y ), X ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (18) {G0,W14,D3,L3,V3,M3} I { ! in( ordered_pair( Y, Z ), X )
% 9.93/10.29 , ! in( ordered_pair( Z, Y ), X ), alpha1( X, Y, Z ) }.
% 9.93/10.29 parent0: (49008) {G0,W14,D3,L3,V3,M3} { ! in( ordered_pair( Y, Z ), X ), !
% 9.93/10.29 in( ordered_pair( Z, Y ), X ), alpha1( X, Y, Z ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 2 ==> 2
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (28) {G0,W2,D2,L1,V0,M1} I { relation( skol3 ) }.
% 9.93/10.29 parent0: (49026) {G0,W2,D2,L1,V0,M1} { relation( skol3 ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (29) {G0,W9,D2,L3,V2,M3} I { alpha5( skol3 ), ! alpha2( skol3
% 9.93/10.29 , X, Y ), X = Y }.
% 9.93/10.29 parent0: (49027) {G0,W9,D2,L3,V2,M3} { alpha5( skol3 ), ! alpha2( skol3, X
% 9.93/10.29 , Y ), X = Y }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 2 ==> 2
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (30) {G0,W4,D2,L2,V0,M2} I { alpha5( skol3 ), ! antisymmetric
% 9.93/10.29 ( skol3 ) }.
% 9.93/10.29 parent0: (49028) {G0,W4,D2,L2,V0,M2} { alpha5( skol3 ), ! antisymmetric(
% 9.93/10.29 skol3 ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (31) {G0,W4,D2,L2,V1,M2} I { ! alpha5( X ), antisymmetric( X )
% 9.93/10.29 }.
% 9.93/10.29 parent0: (49029) {G0,W4,D2,L2,V1,M2} { ! alpha5( X ), antisymmetric( X )
% 9.93/10.29 }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (32) {G0,W8,D3,L2,V1,M2} I { ! alpha5( X ), alpha2( X, skol4(
% 9.93/10.29 X ), skol11( X ) ) }.
% 9.93/10.29 parent0: (49030) {G0,W8,D3,L2,V1,M2} { ! alpha5( X ), alpha2( X, skol4( X
% 9.93/10.29 ), skol11( X ) ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (33) {G0,W7,D3,L2,V1,M2} I { ! alpha5( X ), ! skol4( X ) ==>
% 9.93/10.29 skol11( X ) }.
% 9.93/10.29 parent0: (49031) {G0,W7,D3,L2,V1,M2} { ! alpha5( X ), ! skol4( X ) =
% 9.93/10.29 skol11( X ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (35) {G0,W9,D3,L2,V3,M2} I { ! alpha2( X, Y, Z ), in(
% 9.93/10.29 ordered_pair( Y, Z ), X ) }.
% 9.93/10.29 parent0: (49033) {G0,W9,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), in(
% 9.93/10.29 ordered_pair( Y, Z ), X ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (36) {G0,W9,D3,L2,V3,M2} I { ! alpha2( X, Y, Z ), in(
% 9.93/10.29 ordered_pair( Z, Y ), X ) }.
% 9.93/10.29 parent0: (49034) {G0,W9,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), in(
% 9.93/10.29 ordered_pair( Z, Y ), X ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (37) {G0,W14,D3,L3,V3,M3} I { ! in( ordered_pair( Y, Z ), X )
% 9.93/10.29 , ! in( ordered_pair( Z, Y ), X ), alpha2( X, Y, Z ) }.
% 9.93/10.29 parent0: (49035) {G0,W14,D3,L3,V3,M3} { ! in( ordered_pair( Y, Z ), X ), !
% 9.93/10.29 in( ordered_pair( Z, Y ), X ), alpha2( X, Y, Z ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 2 ==> 2
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (51) {G0,W11,D3,L3,V3,M3} I { ! relation( X ), ! in(
% 9.93/10.29 ordered_pair( Y, Z ), X ), in( Y, relation_field( X ) ) }.
% 9.93/10.29 parent0: (49049) {G0,W11,D3,L3,V3,M3} { ! relation( X ), ! in(
% 9.93/10.29 ordered_pair( Y, Z ), X ), in( Y, relation_field( X ) ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 2 ==> 2
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (52) {G0,W11,D3,L3,V3,M3} I { ! relation( X ), ! in(
% 9.93/10.29 ordered_pair( Y, Z ), X ), in( Z, relation_field( X ) ) }.
% 9.93/10.29 parent0: (49050) {G0,W11,D3,L3,V3,M3} { ! relation( X ), ! in(
% 9.93/10.29 ordered_pair( Y, Z ), X ), in( Z, relation_field( X ) ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.29 Z := Z
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 2 ==> 2
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 resolution: (49188) {G1,W6,D3,L2,V0,M2} { ! is_antisymmetric_in( skol3,
% 9.93/10.29 relation_field( skol3 ) ), antisymmetric( skol3 ) }.
% 9.93/10.29 parent0[0]: (6) {G0,W8,D3,L3,V1,M3} I { ! relation( X ), !
% 9.93/10.29 is_antisymmetric_in( X, relation_field( X ) ), antisymmetric( X ) }.
% 9.93/10.29 parent1[0]: (28) {G0,W2,D2,L1,V0,M1} I { relation( skol3 ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := skol3
% 9.93/10.29 end
% 9.93/10.29 substitution1:
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 subsumption: (75) {G1,W6,D3,L2,V0,M2} R(6,28) { ! is_antisymmetric_in(
% 9.93/10.29 skol3, relation_field( skol3 ) ), antisymmetric( skol3 ) }.
% 9.93/10.29 parent0: (49188) {G1,W6,D3,L2,V0,M2} { ! is_antisymmetric_in( skol3,
% 9.93/10.29 relation_field( skol3 ) ), antisymmetric( skol3 ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 end
% 9.93/10.29 permutation0:
% 9.93/10.29 0 ==> 0
% 9.93/10.29 1 ==> 1
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 eqswap: (49189) {G0,W13,D2,L4,V4,M4} { Y = X, ! relation( Z ), !
% 9.93/10.29 is_antisymmetric_in( Z, T ), ! alpha3( Z, T, X, Y ) }.
% 9.93/10.29 parent0[3]: (7) {G0,W13,D2,L4,V4,M4} I { ! relation( X ), !
% 9.93/10.29 is_antisymmetric_in( X, Y ), ! alpha3( X, Y, Z, T ), Z = T }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := Z
% 9.93/10.29 Y := T
% 9.93/10.29 Z := X
% 9.93/10.29 T := Y
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 resolution: (49190) {G1,W15,D3,L5,V3,M5} { X = Y, ! relation( Z ), !
% 9.93/10.29 alpha3( Z, relation_field( Z ), Y, X ), ! relation( Z ), ! antisymmetric
% 9.93/10.29 ( Z ) }.
% 9.93/10.29 parent0[2]: (49189) {G0,W13,D2,L4,V4,M4} { Y = X, ! relation( Z ), !
% 9.93/10.29 is_antisymmetric_in( Z, T ), ! alpha3( Z, T, X, Y ) }.
% 9.93/10.29 parent1[2]: (5) {G0,W8,D3,L3,V1,M3} I { ! relation( X ), ! antisymmetric( X
% 9.93/10.29 ), is_antisymmetric_in( X, relation_field( X ) ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := Y
% 9.93/10.29 Y := X
% 9.93/10.29 Z := Z
% 9.93/10.29 T := relation_field( Z )
% 9.93/10.29 end
% 9.93/10.29 substitution1:
% 9.93/10.29 X := Z
% 9.93/10.29 end
% 9.93/10.29
% 9.93/10.29 factor: (49191) {G1,W13,D3,L4,V3,M4} { X = Y, ! relation( Z ), ! alpha3( Z
% 9.93/10.29 , relation_field( Z ), Y, X ), ! antisymmetric( Z ) }.
% 9.93/10.29 parent0[1, 3]: (49190) {G1,W15,D3,L5,V3,M5} { X = Y, ! relation( Z ), !
% 9.93/10.29 alpha3( Z, relation_field( Z ), Y, X ), ! relation( Z ), ! antisymmetric
% 9.93/10.29 ( Z ) }.
% 9.93/10.29 substitution0:
% 9.93/10.29 X := X
% 9.93/10.29 Y := Y
% 9.93/10.30 Z := Z
% 9.93/10.30 end
% 9.93/10.30
% 9.93/10.30 eqswap: (49192) {G1,W13,D3,L4,V3,M4} { Y = X, ! relation( Z ), ! alpha3( Z
% 9.93/10.30 , relation_field( Z ), Y, X ), ! antisymmetric( Z ) }.
% 9.93/10.30 parent0[0]: (49191) {G1,W13,D3,L4,V3,M4} { X = Y, ! relation( Z ), !
% 9.93/10.30 alpha3( Z, relation_field( Z ), Y, X ), ! antisymmetric( Z ) }.
% 9.93/10.30 substitution0:
% 9.93/10.30 X := X
% 9.93/10.30 Y := Y
% 9.93/10.30 Z := Z
% 9.93/10.30 end
% 9.93/10.30
% 9.93/10.30 subsumption: (98) {G1,W13,D3,L4,V3,M4} R(7,5);f { ! relation( X ), ! alpha3
% 9.93/10.30 ( X, relation_field( X ), Y, Z ), Y = Z, ! antisymmetric( X ) }.
% 9.93/10.30 parent0: (49192) {G1,W13,D3,L4,V3,M4} { Y = X, ! relation( Z ), ! alpha3(
% 9.93/10.30 Z, relation_field( Z ), Y, X ), ! antisymmetric( Z ) }.
% 9.93/10.30 substitution0:
% 9.93/10.30 X := Z
% 9.93/10.30 Y := Y
% 9.93/10.30 Z := X
% 9.93/10.30 end
% 9.93/10.30 permutation0:
% 9.93/10.30 0 ==> 2
% 9.93/10.30 1 ==> 0
% 9.93/10.30 2 ==> 1
% 9.93/10.30 3 ==> 3
% 9.93/10.30 end
% 9.93/10.30
% 9.93/10.30 resolution: (49194) {G1,W12,D3,L2,V1,M2} { alpha3( skol3, X, skol1( skol3
% 9.93/10.30 , X ), skol10( skol3, X ) ), is_antisymmetric_in( skol3, X ) }.
% 9.93/10.30 parent0[0]: (8) {G0,W14,D3,L3,V2,M3} I { ! relation( X ), alpha3( X, Y,
% 9.93/10.30 skol1( X, Y ), skol10( X, Y ) ), is_antisymmetric_in( X, Y ) }.
% 9.93/10.30 parent1[0]: (28) {G0,W2,D2,L1,V0,M1} I { relation( skol3 ) }.
% 9.93/10.30 substitution0:
% 9.93/10.30 X := skol3
% 9.93/10.30 Y := X
% 9.93/10.30 end
% 9.93/10.30 substitution1:
% 9.93/10.30 end
% 9.93/10.30
% 9.93/10.30 subsumption: (151) {G1,W12,D3,L2,V1,M2} R(8,28) { alpha3( skol3, X, skol1(
% 9.93/10.30 skol3, X ), skol10( skol3, X ) ), is_antisymmetric_in( skol3, X ) }.
% 9.93/10.30 parent0: (49194) {G1,W12,D3,L2,V1,M2} { alpha3( skol3, X, skol1( skol3, X
% 9.93/10.30 ), skol10( skol3, X ) ), is_antisymmetric_in( skol3, X ) }.
% 9.93/10.30 substitution0:
% 9.93/10.30 X := X
% 9.93/10.30 end
% 9.93/10.30 permutation0:
% 9.93/10.30 0 ==> 0
% 9.93/10.30 1 ==> 1
% 9.93/10.30 end
% 9.93/10.30
% 9.93/10.30 resolution: (49195) {G1,W9,D2,L2,V4,M2} { alpha1( X, Z, T ), ! alpha3( X,
% 9.93/10.30 Y, Z, T ) }.
% 9.93/10.30 parent0[0]: (14) {G0,W9,D2,L2,V4,M2} I { ! alpha4( X, Y, Z, T ), alpha1( X
% 9.93/10.30 , Z, T ) }.
% 9.93/10.30 parent1[1]: (11) {G0,W10,D2,L2,V4,M2} I { ! alpha3( X, Y, Z, T ), alpha4( X
% 9.93/10.30 , Y, Z, T ) }.
% 9.93/10.30 substitution0:
% 9.93/10.30 X := X
% 9.93/10.30 Y := Y
% 9.93/10.30 Z := Z
% 9.93/10.30 T := T
% 9.93/10.30 end
% 9.93/10.30 substitution1:
% 9.93/10.30 X := X
% 9.93/10.30 Y := Y
% 9.93/10.30 Z := Z
% 9.93/10.30 T := T
% 9.93/10.30 end
% 9.93/10.30
% 9.93/10.30 subsumption: (242) {G1,W9,D2,L2,V4,M2} R(14,11) { alpha1( X, Y, Z ), !
% 9.93/10.30 alpha3( X, T, Y, Z ) }.
% 9.93/10.30 parent0: (49195) {G1,W9,D2,L2,V4,M2} { alpha1( X, Z, T ), ! alphaCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------