%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU241+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n018.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 : 600s
% DateTime : Tue Jul 19 12:01:21 EDT 2022
% Result : Theorem 1.06s 1.39s
% Output : Proof 1.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SEU241+1 : TPTP v8.1.0. Released v3.3.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sun Jun 19 23:11:20 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.06/1.39 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.06/1.39 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.06/1.40
% 1.06/1.40 %-----------------------------------------------------
% 1.06/1.40 fof(l3_wellord1, conjecture, ! [_51598] : (relation(_51598) => (antisymmetric(_51598) <=> ! [_51620, _51623] : (in(ordered_pair(_51620, _51623), _51598) & in(ordered_pair(_51623, _51620), _51598) => _51620 = _51623))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l3_wellord1)).
% 1.06/1.40 fof(d12_relat_2, axiom, ! [_52005] : (relation(_52005) => (antisymmetric(_52005) <=> is_antisymmetric_in(_52005, relation_field(_52005)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d12_relat_2)).
% 1.06/1.40 fof(d4_relat_2, axiom, ! [_52177] : (relation(_52177) => ! [_52192] : (is_antisymmetric_in(_52177, _52192) <=> ! [_52210, _52213] : (in(_52210, _52192) & in(_52213, _52192) & in(ordered_pair(_52210, _52213), _52177) & in(ordered_pair(_52213, _52210), _52177) => _52210 = _52213))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d4_relat_2)).
% 1.06/1.40 fof(t30_relat_1, axiom, ! [_52601, _52604, _52607] : (relation(_52607) => in(ordered_pair(_52601, _52604), _52607) => in(_52601, relation_field(_52607)) & in(_52604, relation_field(_52607))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t30_relat_1)).
% 1.06/1.40
% 1.06/1.40 cnf(1, plain, [-(13 ^ []), -(_37981 = _37986), in(ordered_pair(_37981, _37986), 9 ^ []), in(ordered_pair(_37986, _37981), 9 ^ [])], clausify(l3_wellord1)).
% 1.06/1.40 cnf(2, plain, [-(13 ^ []), antisymmetric(9 ^ [])], clausify(l3_wellord1)).
% 1.06/1.40 cnf(3, plain, [-(12 ^ []), 10 ^ [] = 11 ^ []], clausify(l3_wellord1)).
% 1.06/1.40 cnf(4, plain, [-(12 ^ []), -(in(ordered_pair(11 ^ [], 10 ^ []), 9 ^ []))], clausify(l3_wellord1)).
% 1.06/1.40 cnf(5, plain, [-(12 ^ []), -(in(ordered_pair(10 ^ [], 11 ^ []), 9 ^ []))], clausify(l3_wellord1)).
% 1.06/1.40 cnf(6, plain, [-(12 ^ []), -(antisymmetric(9 ^ []))], clausify(l3_wellord1)).
% 1.06/1.40 cnf(7, plain, [-(relation(9 ^ []))], clausify(l3_wellord1)).
% 1.06/1.40 cnf(8, plain, [12 ^ [], 13 ^ []], clausify(l3_wellord1)).
% 1.06/1.40 cnf(9, plain, [-(_13359 = _13359)], theory(equality)).
% 1.06/1.40 cnf(10, plain, [_13512 = _13557, -(_13557 = _13512)], theory(equality)).
% 1.06/1.40 cnf(11, plain, [-(is_antisymmetric_in(_16569, _16700)), is_antisymmetric_in(_16502, _16635), _16502 = _16569, _16635 = _16700], theory(equality)).
% 1.06/1.40 cnf(12, plain, [relation(_22800), antisymmetric(_22800), -(is_antisymmetric_in(_22800, relation_field(_22800)))], clausify(d12_relat_2)).
% 1.06/1.40 cnf(13, plain, [relation(_22800), -(antisymmetric(_22800)), is_antisymmetric_in(_22800, relation_field(_22800))], clausify(d12_relat_2)).
% 1.06/1.40 cnf(14, plain, [relation(_23108), -(is_antisymmetric_in(_23108, _23236)), -(in(ordered_pair(1 ^ [_23236, _23108], 2 ^ [_23236, _23108]), _23108))], clausify(d4_relat_2)).
% 1.06/1.40 cnf(15, plain, [relation(_23108), -(is_antisymmetric_in(_23108, _23236)), -(in(ordered_pair(2 ^ [_23236, _23108], 1 ^ [_23236, _23108]), _23108))], clausify(d4_relat_2)).
% 1.06/1.40 cnf(16, plain, [relation(_23108), -(is_antisymmetric_in(_23108, _23236)), 1 ^ [_23236, _23108] = 2 ^ [_23236, _23108]], clausify(d4_relat_2)).
% 1.06/1.40 cnf(17, plain, [relation(_23108), is_antisymmetric_in(_23108, _23236), -(_23379 = _23456), in(_23379, _23236), in(_23456, _23236), in(ordered_pair(_23379, _23456), _23108), in(ordered_pair(_23456, _23379), _23108)], clausify(d4_relat_2)).
% 1.06/1.40 cnf(18, plain, [relation(_29656), in(ordered_pair(_29521, _29589), _29656), -(in(_29521, relation_field(_29656)))], clausify(t30_relat_1)).
% 1.06/1.40
% 1.06/1.40 cnf('1',plain,[12 ^ [], 13 ^ []],start(8)).
% 1.06/1.40 cnf('1.1',plain,[-(12 ^ []), 10 ^ [] = 11 ^ []],extension(3)).
% 1.06/1.40 cnf('1.1.1',plain,[-(10 ^ [] = 11 ^ []), 11 ^ [] = 10 ^ []],extension(10,bind([[_13512, _13557], [11 ^ [], 10 ^ []]]))).
% 1.06/1.40 cnf('1.1.1.1',plain,[-(11 ^ [] = 10 ^ []), relation(9 ^ []), is_antisymmetric_in(9 ^ [], relation_field(9 ^ [])), in(11 ^ [], relation_field(9 ^ [])), in(10 ^ [], relation_field(9 ^ [])), in(ordered_pair(11 ^ [], 10 ^ []), 9 ^ []), in(ordered_pair(10 ^ [], 11 ^ []), 9 ^ [])],extension(17,bind([[_23236, _23456, _23379, _23108], [relation_field(9 ^ []), 10 ^ [], 11 ^ [], 9 ^ []]]))).
% 1.06/1.40 cnf('1.1.1.1.1',plain,[-(relation(9 ^ []))],extension(7)).
% 1.06/1.40 cnf('1.1.1.1.2',plain,[-(is_antisymmetric_in(9 ^ [], relation_field(9 ^ []))), is_antisymmetric_in(9 ^ [], relation_field(9 ^ [])), 9 ^ [] = 9 ^ [], relation_field(9 ^ []) = relation_field(9 ^ [])],extension(11,bind([[_16502, _16569, _16635, _16700], [9 ^ [], 9 ^ [], relation_field(9 ^ []), relation_field(9 ^ [])]]))).
% 1.06/1.40 cnf('1.1.1.1.2.1',plain,[-(is_antisymmetric_in(9 ^ [], relation_field(9 ^ []))), relation(9 ^ []), antisymmetric(9 ^ [])],extension(12,bind([[_22800], [9 ^ []]]))).
% 1.06/1.40 cnf('1.1.1.1.2.1.1',plain,[-(relation(9 ^ []))],extension(7)).
% 1.06/1.40 cnf('1.1.1.1.2.1.2',plain,[-(antisymmetric(9 ^ [])), -(12 ^ [])],extension(6)).
% 1.06/1.40 cnf('1.1.1.1.2.1.2.1',plain,[12 ^ []],reduction('1')).
% 1.06/1.40 cnf('1.1.1.1.2.2',plain,[-(9 ^ [] = 9 ^ [])],extension(9,bind([[_13359], [9 ^ []]]))).
% 1.06/1.40 cnf('1.1.1.1.2.3',plain,[-(relation_field(9 ^ []) = relation_field(9 ^ []))],extension(9,bind([[_13359], [relation_field(9 ^ [])]]))).
% 1.06/1.40 cnf('1.1.1.1.3',plain,[-(in(11 ^ [], relation_field(9 ^ []))), relation(9 ^ []), in(ordered_pair(11 ^ [], 10 ^ []), 9 ^ [])],extension(18,bind([[_29521, _29589, _29656], [11 ^ [], 10 ^ [], 9 ^ []]]))).
% 1.06/1.40 cnf('1.1.1.1.3.1',plain,[-(relation(9 ^ []))],extension(7)).
% 1.06/1.40 cnf('1.1.1.1.3.2',plain,[-(in(ordered_pair(11 ^ [], 10 ^ []), 9 ^ [])), -(12 ^ [])],extension(4)).
% 1.06/1.40 cnf('1.1.1.1.3.2.1',plain,[12 ^ []],reduction('1')).
% 1.06/1.40 cnf('1.1.1.1.4',plain,[-(in(10 ^ [], relation_field(9 ^ []))), relation(9 ^ []), in(ordered_pair(10 ^ [], 11 ^ []), 9 ^ [])],extension(18,bind([[_29521, _29589, _29656], [10 ^ [], 11 ^ [], 9 ^ []]]))).
% 1.06/1.40 cnf('1.1.1.1.4.1',plain,[-(relation(9 ^ []))],extension(7)).
% 1.06/1.40 cnf('1.1.1.1.4.2',plain,[-(in(ordered_pair(10 ^ [], 11 ^ []), 9 ^ [])), -(12 ^ [])],extension(5)).
% 1.06/1.40 cnf('1.1.1.1.4.2.1',plain,[12 ^ []],reduction('1')).
% 1.06/1.40 cnf('1.1.1.1.5',plain,[-(in(ordered_pair(11 ^ [], 10 ^ []), 9 ^ [])), -(12 ^ [])],extension(4)).
% 1.06/1.40 cnf('1.1.1.1.5.1',plain,[12 ^ []],reduction('1')).
% 1.06/1.40 cnf('1.1.1.1.6',plain,[-(in(ordered_pair(10 ^ [], 11 ^ []), 9 ^ [])), -(12 ^ [])],extension(5)).
% 1.06/1.40 cnf('1.1.1.1.6.1',plain,[12 ^ []],reduction('1')).
% 1.06/1.40 cnf('1.2',plain,[-(13 ^ []), antisymmetric(9 ^ [])],extension(2)).
% 1.06/1.40 cnf('1.2.1',plain,[-(antisymmetric(9 ^ [])), relation(9 ^ []), is_antisymmetric_in(9 ^ [], relation_field(9 ^ []))],extension(13,bind([[_22800], [9 ^ []]]))).
% 1.06/1.40 cnf('1.2.1.1',plain,[-(relation(9 ^ []))],extension(7)).
% 1.06/1.40 cnf('1.2.1.2',plain,[-(is_antisymmetric_in(9 ^ [], relation_field(9 ^ []))), relation(9 ^ []), -(in(ordered_pair(1 ^ [relation_field(9 ^ []), 9 ^ []], 2 ^ [relation_field(9 ^ []), 9 ^ []]), 9 ^ []))],extension(14,bind([[_23236, _23108], [relation_field(9 ^ []), 9 ^ []]]))).
% 1.06/1.40 cnf('1.2.1.2.1',plain,[-(relation(9 ^ []))],extension(7)).
% 1.06/1.40 cnf('1.2.1.2.2',plain,[in(ordered_pair(1 ^ [relation_field(9 ^ []), 9 ^ []], 2 ^ [relation_field(9 ^ []), 9 ^ []]), 9 ^ []), -(13 ^ []), -(1 ^ [relation_field(9 ^ []), 9 ^ []] = 2 ^ [relation_field(9 ^ []), 9 ^ []]), in(ordered_pair(2 ^ [relation_field(9 ^ []), 9 ^ []], 1 ^ [relation_field(9 ^ []), 9 ^ []]), 9 ^ [])],extension(1,bind([[_37986, _37981], [2 ^ [relation_field(9 ^ []), 9 ^ []], 1 ^ [relation_field(9 ^ []), 9 ^ []]]]))).
% 1.06/1.40 cnf('1.2.1.2.2.1',plain,[13 ^ []],reduction('1')).
% 1.06/1.40 cnf('1.2.1.2.2.2',plain,[1 ^ [relation_field(9 ^ []), 9 ^ []] = 2 ^ [relation_field(9 ^ []), 9 ^ []], relation(9 ^ []), -(is_antisymmetric_in(9 ^ [], relation_field(9 ^ [])))],extension(16,bind([[_23108, _23236], [9 ^ [], relation_field(9 ^ [])]]))).
% 1.06/1.40 cnf('1.2.1.2.2.2.1',plain,[-(relation(9 ^ []))],extension(7)).
% 1.06/1.40 cnf('1.2.1.2.2.2.2',plain,[is_antisymmetric_in(9 ^ [], relation_field(9 ^ []))],reduction('1.2.1')).
% 1.06/1.40 cnf('1.2.1.2.2.3',plain,[-(in(ordered_pair(2 ^ [relation_field(9 ^ []), 9 ^ []], 1 ^ [relation_field(9 ^ []), 9 ^ []]), 9 ^ [])), relation(9 ^ []), -(is_antisymmetric_in(9 ^ [], relation_field(9 ^ [])))],extension(15,bind([[_23108, _23236], [9 ^ [], relation_field(9 ^ [])]]))).
% 1.06/1.40 cnf('1.2.1.2.2.3.1',plain,[-(relation(9 ^ []))],extension(7)).
% 1.06/1.40 cnf('1.2.1.2.2.3.2',plain,[is_antisymmetric_in(9 ^ [], relation_field(9 ^ []))],reduction('1.2.1')).
% 1.06/1.40 %-----------------------------------------------------
% 1.06/1.40
% 1.06/1.40 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------