%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU245+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n013.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:23 EDT 2022
% Result : Theorem 0.37s 1.40s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU245+1 : TPTP v8.1.0. Released v3.3.0.
% 0.12/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n013.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 % WCLimit : 600
% 0.12/0.34 % DateTime : Mon Jun 20 11:33:29 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.37/1.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.41
% 0.37/1.41 %-----------------------------------------------------
% 0.37/1.41 fof(t16_wellord1, conjecture, ! [_41046, _41049, _41052] : (relation(_41052) => (in(_41046, relation_restriction(_41052, _41049)) <=> in(_41046, _41052) & in(_41046, cartesian_product2(_41049, _41049)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t16_wellord1)).
% 0.37/1.41 fof(d6_wellord1, axiom, ! [_41419] : (relation(_41419) => ! [_41434] : relation_restriction(_41419, _41434) = set_intersection2(_41419, cartesian_product2(_41434, _41434))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d6_wellord1)).
% 0.37/1.41 fof(d3_xboole_0, axiom, ! [_41621, _41624, _41627] : (_41627 = set_intersection2(_41621, _41624) <=> ! [_41648] : (in(_41648, _41627) <=> in(_41648, _41621) & in(_41648, _41624))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d3_xboole_0)).
% 0.37/1.41
% 0.37/1.41 cnf(1, plain, [-(12 ^ []), in(8 ^ [], relation_restriction(10 ^ [], 9 ^ []))], clausify(t16_wellord1)).
% 0.37/1.41 cnf(2, plain, [-(12 ^ []), -(in(8 ^ [], cartesian_product2(9 ^ [], 9 ^ [])))], clausify(t16_wellord1)).
% 0.37/1.41 cnf(3, plain, [-(12 ^ []), -(in(8 ^ [], 10 ^ []))], clausify(t16_wellord1)).
% 0.37/1.41 cnf(4, plain, [-(11 ^ []), in(8 ^ [], 10 ^ []), in(8 ^ [], cartesian_product2(9 ^ [], 9 ^ []))], clausify(t16_wellord1)).
% 0.37/1.41 cnf(5, plain, [-(11 ^ []), -(in(8 ^ [], relation_restriction(10 ^ [], 9 ^ [])))], clausify(t16_wellord1)).
% 0.37/1.41 cnf(6, plain, [-(relation(10 ^ []))], clausify(t16_wellord1)).
% 0.37/1.41 cnf(7, plain, [12 ^ [], 11 ^ []], clausify(t16_wellord1)).
% 0.37/1.41 cnf(8, plain, [-(set_intersection2(_14870, _15003) = set_intersection2(_14937, _15068)), _14870 = _14937, _15003 = _15068], theory(equality)).
% 0.37/1.41 cnf(9, plain, [-(_10080 = _10080)], theory(equality)).
% 0.37/1.41 cnf(10, plain, [-(in(_12337, _12468)), in(_12270, _12403), _12270 = _12337, _12403 = _12468], theory(equality)).
% 0.37/1.41 cnf(11, plain, [relation(_21194), -(relation_restriction(_21194, _21285) = set_intersection2(_21194, cartesian_product2(_21285, _21285)))], clausify(d6_wellord1)).
% 0.37/1.41 cnf(12, plain, [_21734 = set_intersection2(_21595, _21665), in(_21898, _21734), -(in(_21898, _21595))], clausify(d3_xboole_0)).
% 0.37/1.41 cnf(13, plain, [_21734 = set_intersection2(_21595, _21665), in(_21898, _21734), -(in(_21898, _21665))], clausify(d3_xboole_0)).
% 0.37/1.41 cnf(14, plain, [_21734 = set_intersection2(_21595, _21665), -(in(_21898, _21734)), in(_21898, _21595), in(_21898, _21665)], clausify(d3_xboole_0)).
% 0.37/1.41
% 0.37/1.41 cnf('1',plain,[12 ^ [], 11 ^ []],start(7)).
% 0.37/1.41 cnf('1.1',plain,[-(12 ^ []), -(in(8 ^ [], cartesian_product2(9 ^ [], 9 ^ [])))],extension(2)).
% 0.37/1.41 cnf('1.1.1',plain,[in(8 ^ [], cartesian_product2(9 ^ [], 9 ^ [])), set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ [])) = set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ [])), -(in(8 ^ [], set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ [])))), in(8 ^ [], relation_restriction(10 ^ [], 9 ^ []))],extension(14,bind([[_21595, _21734, _21898, _21665], [cartesian_product2(9 ^ [], 9 ^ []), set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ [])), 8 ^ [], relation_restriction(10 ^ [], 9 ^ [])]]))).
% 0.37/1.41 cnf('1.1.1.1',plain,[-(set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ [])) = set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ []))), cartesian_product2(9 ^ [], 9 ^ []) = cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ []) = relation_restriction(10 ^ [], 9 ^ [])],extension(8,bind([[_14870, _14937, _15003, _15068], [cartesian_product2(9 ^ [], 9 ^ []), cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ [])]]))).
% 0.37/1.41 cnf('1.1.1.1.1',plain,[-(cartesian_product2(9 ^ [], 9 ^ []) = cartesian_product2(9 ^ [], 9 ^ []))],extension(9,bind([[_10080], [cartesian_product2(9 ^ [], 9 ^ [])]]))).
% 0.37/1.41 cnf('1.1.1.1.2',plain,[-(relation_restriction(10 ^ [], 9 ^ []) = relation_restriction(10 ^ [], 9 ^ []))],extension(9,bind([[_10080], [relation_restriction(10 ^ [], 9 ^ [])]]))).
% 0.37/1.41 cnf('1.1.1.2',plain,[in(8 ^ [], set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ []))), set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ [])) = set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ [])), -(in(8 ^ [], relation_restriction(10 ^ [], 9 ^ [])))],extension(13,bind([[_21734, _21595, _21898, _21665], [set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ [])), cartesian_product2(9 ^ [], 9 ^ []), 8 ^ [], relation_restriction(10 ^ [], 9 ^ [])]]))).
% 0.37/1.41 cnf('1.1.1.2.1',plain,[-(set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ [])) = set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ [])))],extension(9,bind([[_10080], [set_intersection2(cartesian_product2(9 ^ [], 9 ^ []), relation_restriction(10 ^ [], 9 ^ []))]]))).
% 0.37/1.41 cnf('1.1.1.2.2',plain,[in(8 ^ [], relation_restriction(10 ^ [], 9 ^ [])), -(12 ^ [])],extension(1)).
% 0.37/1.41 cnf('1.1.1.2.2.1',plain,[12 ^ []],reduction('1')).
% 0.37/1.41 cnf('1.1.1.3',plain,[-(in(8 ^ [], relation_restriction(10 ^ [], 9 ^ []))), relation_restriction(10 ^ [], 9 ^ []) = set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ [])), in(8 ^ [], 10 ^ []), in(8 ^ [], cartesian_product2(9 ^ [], 9 ^ []))],extension(14,bind([[_21734, _21595, _21898, _21665], [relation_restriction(10 ^ [], 9 ^ []), 10 ^ [], 8 ^ [], cartesian_product2(9 ^ [], 9 ^ [])]]))).
% 0.37/1.41 cnf('1.1.1.3.1',plain,[-(relation_restriction(10 ^ [], 9 ^ []) = set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ []))), relation(10 ^ [])],extension(11,bind([[_21285, _21194], [9 ^ [], 10 ^ []]]))).
% 0.37/1.41 cnf('1.1.1.3.1.1',plain,[-(relation(10 ^ []))],extension(6)).
% 0.37/1.41 cnf('1.1.1.3.2',plain,[-(in(8 ^ [], 10 ^ [])), -(12 ^ [])],extension(3)).
% 0.37/1.41 cnf('1.1.1.3.2.1',plain,[12 ^ []],reduction('1')).
% 0.37/1.41 cnf('1.1.1.3.3',plain,[-(in(8 ^ [], cartesian_product2(9 ^ [], 9 ^ [])))],reduction('1.1')).
% 0.37/1.41 cnf('1.2',plain,[-(11 ^ []), in(8 ^ [], 10 ^ []), in(8 ^ [], cartesian_product2(9 ^ [], 9 ^ []))],extension(4)).
% 0.37/1.41 cnf('1.2.1',plain,[-(in(8 ^ [], 10 ^ [])), set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ [])) = set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ [])), in(8 ^ [], set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ [])))],extension(12,bind([[_21595, _21665, _21898, _21734], [10 ^ [], cartesian_product2(9 ^ [], 9 ^ []), 8 ^ [], set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ []))]]))).
% 0.37/1.41 cnf('1.2.1.1',plain,[-(set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ [])) = set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ []))), 10 ^ [] = 10 ^ [], cartesian_product2(9 ^ [], 9 ^ []) = cartesian_product2(9 ^ [], 9 ^ [])],extension(8,bind([[_14870, _14937, _15003, _15068], [10 ^ [], 10 ^ [], cartesian_product2(9 ^ [], 9 ^ []), cartesian_product2(9 ^ [], 9 ^ [])]]))).
% 0.37/1.41 cnf('1.2.1.1.1',plain,[-(10 ^ [] = 10 ^ [])],extension(9,bind([[_10080], [10 ^ []]]))).
% 0.37/1.41 cnf('1.2.1.1.2',plain,[-(cartesian_product2(9 ^ [], 9 ^ []) = cartesian_product2(9 ^ [], 9 ^ []))],extension(9,bind([[_10080], [cartesian_product2(9 ^ [], 9 ^ [])]]))).
% 0.37/1.41 cnf('1.2.1.2',plain,[-(in(8 ^ [], set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ [])))), in(8 ^ [], relation_restriction(10 ^ [], 9 ^ [])), 8 ^ [] = 8 ^ [], relation_restriction(10 ^ [], 9 ^ []) = set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ []))],extension(10,bind([[_12270, _12337, _12403, _12468], [8 ^ [], 8 ^ [], relation_restriction(10 ^ [], 9 ^ []), set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ []))]]))).
% 0.37/1.41 cnf('1.2.1.2.1',plain,[-(in(8 ^ [], relation_restriction(10 ^ [], 9 ^ []))), -(11 ^ [])],extension(5)).
% 0.37/1.41 cnf('1.2.1.2.1.1',plain,[11 ^ []],reduction('1')).
% 0.37/1.41 cnf('1.2.1.2.2',plain,[-(8 ^ [] = 8 ^ [])],extension(9,bind([[_10080], [8 ^ []]]))).
% 0.37/1.41 cnf('1.2.1.2.3',plain,[-(relation_restriction(10 ^ [], 9 ^ []) = set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ []))), relation(10 ^ [])],extension(11,bind([[_21285, _21194], [9 ^ [], 10 ^ []]]))).
% 0.37/1.41 cnf('1.2.1.2.3.1',plain,[-(relation(10 ^ []))],extension(6)).
% 0.37/1.41 cnf('1.2.2',plain,[-(in(8 ^ [], cartesian_product2(9 ^ [], 9 ^ []))), set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ [])) = set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ [])), in(8 ^ [], set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ [])))],extension(13,bind([[_21595, _21665, _21898, _21734], [10 ^ [], cartesian_product2(9 ^ [], 9 ^ []), 8 ^ [], set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ []))]]))).
% 0.37/1.41 cnf('1.2.2.1',plain,[-(set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ [])) = set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ []))), 10 ^ [] = 10 ^ [], cartesian_product2(9 ^ [], 9 ^ []) = cartesian_product2(9 ^ [], 9 ^ [])],extension(8,bind([[_14870, _14937, _15003, _15068], [10 ^ [], 10 ^ [], cartesian_product2(9 ^ [], 9 ^ []), cartesian_product2(9 ^ [], 9 ^ [])]]))).
% 0.37/1.41 cnf('1.2.2.1.1',plain,[-(10 ^ [] = 10 ^ [])],extension(9,bind([[_10080], [10 ^ []]]))).
% 0.37/1.41 cnf('1.2.2.1.2',plain,[-(cartesian_product2(9 ^ [], 9 ^ []) = cartesian_product2(9 ^ [], 9 ^ []))],extension(9,bind([[_10080], [cartesian_product2(9 ^ [], 9 ^ [])]]))).
% 0.37/1.41 cnf('1.2.2.2',plain,[-(in(8 ^ [], set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ [])))), in(8 ^ [], relation_restriction(10 ^ [], 9 ^ [])), 8 ^ [] = 8 ^ [], relation_restriction(10 ^ [], 9 ^ []) = set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ []))],extension(10,bind([[_12270, _12337, _12403, _12468], [8 ^ [], 8 ^ [], relation_restriction(10 ^ [], 9 ^ []), set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ []))]]))).
% 0.37/1.41 cnf('1.2.2.2.1',plain,[-(in(8 ^ [], relation_restriction(10 ^ [], 9 ^ []))), -(11 ^ [])],extension(5)).
% 0.37/1.41 cnf('1.2.2.2.1.1',plain,[11 ^ []],reduction('1')).
% 0.37/1.41 cnf('1.2.2.2.2',plain,[-(8 ^ [] = 8 ^ [])],extension(9,bind([[_10080], [8 ^ []]]))).
% 0.37/1.41 cnf('1.2.2.2.3',plain,[-(relation_restriction(10 ^ [], 9 ^ []) = set_intersection2(10 ^ [], cartesian_product2(9 ^ [], 9 ^ []))), relation(10 ^ [])],extension(11,bind([[_21285, _21194], [9 ^ [], 10 ^ []]]))).
% 0.37/1.41 cnf('1.2.2.2.3.1',plain,[-(relation(10 ^ []))],extension(6)).
% 0.37/1.41 %-----------------------------------------------------
% 0.37/1.42
% 0.37/1.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------