%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU373+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n014.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:02:22 EDT 2022
% Result : Theorem 0.32s 1.40s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU373+1 : TPTP v8.1.0. Released v3.3.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n014.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 : Mon Jun 20 02:04:48 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.32/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/1.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/1.42
% 0.32/1.42 %-----------------------------------------------------
% 0.32/1.42 fof(t19_yellow_6, conjecture, ! [_81350] : (one_sorted_str(_81350) => ! [_81365] : (net_str(_81365, _81350) => ! [_81383] : (subnetstr(_81383, _81350, _81365) => subset(the_carrier(_81383), the_carrier(_81365))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t19_yellow_6)).
% 0.32/1.42 fof(d13_yellow_0, axiom, ! [_81683] : (rel_str(_81683) => ! [_81698] : (rel_str(_81698) => (subrelstr(_81698, _81683) <=> subset(the_carrier(_81698), the_carrier(_81683)) & subset(the_InternalRel(_81698), the_InternalRel(_81683))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d13_yellow_0)).
% 0.32/1.42 fof(d8_yellow_6, axiom, ! [_81956] : (one_sorted_str(_81956) => ! [_81971] : (net_str(_81971, _81956) => ! [_81989] : (net_str(_81989, _81956) => (subnetstr(_81989, _81956, _81971) <=> subrelstr(_81989, _81971) & the_mapping(_81956, _81989) = relation_dom_restr_as_relation_of(the_carrier(_81971), the_carrier(_81956), the_mapping(_81956, _81971), the_carrier(_81989)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d8_yellow_6)).
% 0.32/1.42 fof(dt_l1_waybel_0, axiom, ! [_82353] : (one_sorted_str(_82353) => ! [_82368] : (net_str(_82368, _82353) => rel_str(_82368))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_l1_waybel_0)).
% 0.32/1.42 fof(dt_m1_yellow_6, axiom, ! [_82533, _82536] : (one_sorted_str(_82533) & net_str(_82536, _82533) => ! [_82561] : (subnetstr(_82561, _82533, _82536) => net_str(_82561, _82533))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_m1_yellow_6)).
% 0.32/1.42
% 0.32/1.42 cnf(1, plain, [-(one_sorted_str(19 ^ []))], clausify(t19_yellow_6)).
% 0.32/1.42 cnf(2, plain, [-(net_str(20 ^ [], 19 ^ []))], clausify(t19_yellow_6)).
% 0.32/1.42 cnf(3, plain, [-(subnetstr(21 ^ [], 19 ^ [], 20 ^ []))], clausify(t19_yellow_6)).
% 0.32/1.42 cnf(4, plain, [subset(the_carrier(21 ^ []), the_carrier(20 ^ []))], clausify(t19_yellow_6)).
% 0.32/1.42 cnf(5, plain, [rel_str(_40409), rel_str(_40516), subrelstr(_40516, _40409), -(subset(the_carrier(_40516), the_carrier(_40409)))], clausify(d13_yellow_0)).
% 0.32/1.42 cnf(6, plain, [one_sorted_str(_41006), net_str(_41135, _41006), net_str(_41279, _41006), subnetstr(_41279, _41006, _41135), -(subrelstr(_41279, _41135))], clausify(d8_yellow_6)).
% 0.32/1.42 cnf(7, plain, [one_sorted_str(_43765), net_str(_43852, _43765), -(rel_str(_43852))], clausify(dt_l1_waybel_0)).
% 0.32/1.42 cnf(8, plain, [net_str(_44783, _44721), one_sorted_str(_44721), subnetstr(_44956, _44721, _44783), -(net_str(_44956, _44721))], clausify(dt_m1_yellow_6)).
% 0.32/1.42
% 0.32/1.42 cnf('1',plain,[subset(the_carrier(21 ^ []), the_carrier(20 ^ []))],start(4)).
% 0.32/1.42 cnf('1.1',plain,[-(subset(the_carrier(21 ^ []), the_carrier(20 ^ []))), rel_str(20 ^ []), rel_str(21 ^ []), subrelstr(21 ^ [], 20 ^ [])],extension(5,bind([[_40516, _40409], [21 ^ [], 20 ^ []]]))).
% 0.32/1.42 cnf('1.1.1',plain,[-(rel_str(20 ^ [])), one_sorted_str(19 ^ []), net_str(20 ^ [], 19 ^ [])],extension(7,bind([[_43852, _43765], [20 ^ [], 19 ^ []]]))).
% 0.32/1.42 cnf('1.1.1.1',plain,[-(one_sorted_str(19 ^ []))],extension(1)).
% 0.32/1.42 cnf('1.1.1.2',plain,[-(net_str(20 ^ [], 19 ^ []))],extension(2)).
% 0.32/1.42 cnf('1.1.2',plain,[-(rel_str(21 ^ [])), one_sorted_str(19 ^ []), net_str(21 ^ [], 19 ^ [])],extension(7,bind([[_43852, _43765], [21 ^ [], 19 ^ []]]))).
% 0.32/1.42 cnf('1.1.2.1',plain,[-(one_sorted_str(19 ^ []))],extension(1)).
% 0.32/1.42 cnf('1.1.2.2',plain,[-(net_str(21 ^ [], 19 ^ [])), net_str(20 ^ [], 19 ^ []), one_sorted_str(19 ^ []), subnetstr(21 ^ [], 19 ^ [], 20 ^ [])],extension(8,bind([[_44956, _44721, _44783], [21 ^ [], 19 ^ [], 20 ^ []]]))).
% 0.32/1.42 cnf('1.1.2.2.1',plain,[-(net_str(20 ^ [], 19 ^ []))],extension(2)).
% 0.32/1.42 cnf('1.1.2.2.2',plain,[-(one_sorted_str(19 ^ []))],extension(1)).
% 0.32/1.42 cnf('1.1.2.2.3',plain,[-(subnetstr(21 ^ [], 19 ^ [], 20 ^ []))],extension(3)).
% 0.32/1.42 cnf('1.1.3',plain,[-(subrelstr(21 ^ [], 20 ^ [])), one_sorted_str(19 ^ []), net_str(20 ^ [], 19 ^ []), net_str(21 ^ [], 19 ^ []), subnetstr(21 ^ [], 19 ^ [], 20 ^ [])],extension(6,bind([[_41279, _41006, _41135], [21 ^ [], 19 ^ [], 20 ^ []]]))).
% 0.32/1.42 cnf('1.1.3.1',plain,[-(one_sorted_str(19 ^ []))],extension(1)).
% 0.32/1.42 cnf('1.1.3.2',plain,[-(net_str(20 ^ [], 19 ^ []))],extension(2)).
% 0.32/1.42 cnf('1.1.3.3',plain,[-(net_str(21 ^ [], 19 ^ [])), net_str(20 ^ [], 19 ^ []), one_sorted_str(19 ^ []), subnetstr(21 ^ [], 19 ^ [], 20 ^ [])],extension(8,bind([[_44956, _44721, _44783], [21 ^ [], 19 ^ [], 20 ^ []]]))).
% 0.32/1.42 cnf('1.1.3.3.1',plain,[-(net_str(20 ^ [], 19 ^ []))],extension(2)).
% 0.32/1.42 cnf('1.1.3.3.2',plain,[-(one_sorted_str(19 ^ []))],extension(1)).
% 0.32/1.42 cnf('1.1.3.3.3',plain,[-(subnetstr(21 ^ [], 19 ^ [], 20 ^ []))],extension(3)).
% 0.32/1.42 cnf('1.1.3.4',plain,[-(subnetstr(21 ^ [], 19 ^ [], 20 ^ []))],extension(3)).
% 0.32/1.42 %-----------------------------------------------------
% 0.32/1.42
% 0.32/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------