%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SEU309+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n006.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 14:36:08 EDT 2022
% Result : Theorem 0.46s 0.70s
% Output : Refutation 0.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 11
% Syntax : Number of clauses : 35 ( 13 unt; 0 nHn; 35 RR)
% Number of literals : 72 ( 0 equ; 46 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
one_sorted_str(skc4),
file('SEU309+1.p',unknown),
[] ).
cnf(19,axiom,
element(skc5,powerset(the_carrier(skc4))),
file('SEU309+1.p',unknown),
[] ).
cnf(37,axiom,
equal(set_intersection2(u,v),set_intersection2(v,u)),
file('SEU309+1.p',unknown),
[] ).
cnf(86,axiom,
( ~ one_sorted_str(u)
| equal(the_carrier(u),cast_as_carrier_subset(u)) ),
file('SEU309+1.p',unknown),
[] ).
cnf(104,axiom,
( ~ one_sorted_str(u)
| element(cast_as_carrier_subset(u),powerset(the_carrier(u))) ),
file('SEU309+1.p',unknown),
[] ).
cnf(106,axiom,
equal(set_difference(u,set_difference(u,v)),set_intersection2(u,v)),
file('SEU309+1.p',unknown),
[] ).
cnf(126,axiom,
~ equal(subset_difference(the_carrier(skc4),cast_as_carrier_subset(skc4),subset_difference(the_carrier(skc4),cast_as_carrier_subset(skc4),skc5)),skc5),
file('SEU309+1.p',unknown),
[] ).
cnf(128,axiom,
( ~ element(u,powerset(v))
| ~ element(w,powerset(v))
| element(subset_difference(v,u,w),powerset(v)) ),
file('SEU309+1.p',unknown),
[] ).
cnf(129,axiom,
( ~ one_sorted_str(u)
| ~ element(v,powerset(the_carrier(u)))
| equal(subset_intersection2(the_carrier(u),v,cast_as_carrier_subset(u)),v) ),
file('SEU309+1.p',unknown),
[] ).
cnf(130,axiom,
( ~ element(u,powerset(v))
| ~ element(w,powerset(v))
| equal(subset_intersection2(v,w,u),set_intersection2(w,u)) ),
file('SEU309+1.p',unknown),
[] ).
cnf(131,axiom,
( ~ element(u,powerset(v))
| ~ element(w,powerset(v))
| equal(subset_difference(v,w,u),set_difference(w,u)) ),
file('SEU309+1.p',unknown),
[] ).
cnf(133,plain,
( ~ one_sorted_str(u)
| element(cast_as_carrier_subset(u),powerset(cast_as_carrier_subset(u))) ),
inference(rew,[status(thm),theory(equality)],[86,104]),
[iquote('0:Rew:86.1,104.1')] ).
cnf(134,plain,
( ~ one_sorted_str(u)
| ~ element(v,powerset(cast_as_carrier_subset(u)))
| equal(subset_intersection2(cast_as_carrier_subset(u),v,cast_as_carrier_subset(u)),v) ),
inference(rew,[status(thm),theory(equality)],[86,129]),
[iquote('0:Rew:86.1,129.2,86.1,129.1')] ).
cnf(135,plain,
( ~ element(u,powerset(v))
| ~ element(w,powerset(v))
| element(set_difference(w,u),powerset(v)) ),
inference(rew,[status(thm),theory(equality)],[131,128]),
[iquote('0:Rew:131.2,128.2')] ).
cnf(139,plain,
element(cast_as_carrier_subset(skc4),powerset(cast_as_carrier_subset(skc4))),
inference(res,[status(thm),theory(equality)],[1,133]),
[iquote('0:Res:1.0,133.0')] ).
cnf(140,plain,
equal(the_carrier(skc4),cast_as_carrier_subset(skc4)),
inference(res,[status(thm),theory(equality)],[1,86]),
[iquote('0:Res:1.0,86.0')] ).
cnf(180,plain,
( ~ element(u,powerset(the_carrier(skc4)))
| element(set_difference(u,skc5),powerset(the_carrier(skc4))) ),
inference(res,[status(thm),theory(equality)],[19,135]),
[iquote('0:Res:19.0,135.1')] ).
cnf(181,plain,
( ~ element(u,powerset(the_carrier(skc4)))
| equal(subset_difference(the_carrier(skc4),u,skc5),set_difference(u,skc5)) ),
inference(res,[status(thm),theory(equality)],[19,131]),
[iquote('0:Res:19.0,131.1')] ).
cnf(186,plain,
element(skc5,powerset(cast_as_carrier_subset(skc4))),
inference(rew,[status(thm),theory(equality)],[140,19]),
[iquote('0:Rew:140.0,19.0')] ).
cnf(187,plain,
~ equal(subset_difference(cast_as_carrier_subset(skc4),cast_as_carrier_subset(skc4),subset_difference(cast_as_carrier_subset(skc4),cast_as_carrier_subset(skc4),skc5)),skc5),
inference(rew,[status(thm),theory(equality)],[140,126]),
[iquote('0:Rew:140.0,126.0')] ).
cnf(196,plain,
( ~ element(u,powerset(cast_as_carrier_subset(skc4)))
| element(set_difference(u,skc5),powerset(cast_as_carrier_subset(skc4))) ),
inference(rew,[status(thm),theory(equality)],[140,180]),
[iquote('0:Rew:140.0,180.1,140.0,180.0')] ).
cnf(200,plain,
( ~ element(u,powerset(cast_as_carrier_subset(skc4)))
| equal(subset_difference(cast_as_carrier_subset(skc4),u,skc5),set_difference(u,skc5)) ),
inference(rew,[status(thm),theory(equality)],[140,181]),
[iquote('0:Rew:140.0,181.1,140.0,181.0')] ).
cnf(1180,plain,
( ~ element(subset_difference(cast_as_carrier_subset(skc4),cast_as_carrier_subset(skc4),skc5),powerset(cast_as_carrier_subset(skc4)))
| ~ element(cast_as_carrier_subset(skc4),powerset(cast_as_carrier_subset(skc4)))
| ~ equal(set_difference(cast_as_carrier_subset(skc4),subset_difference(cast_as_carrier_subset(skc4),cast_as_carrier_subset(skc4),skc5)),skc5) ),
inference(spl,[status(thm),theory(equality)],[131,187]),
[iquote('0:SpL:131.2,187.0')] ).
cnf(1182,plain,
( ~ element(set_difference(cast_as_carrier_subset(skc4),skc5),powerset(cast_as_carrier_subset(skc4)))
| ~ element(cast_as_carrier_subset(skc4),powerset(cast_as_carrier_subset(skc4)))
| ~ equal(set_difference(cast_as_carrier_subset(skc4),set_difference(cast_as_carrier_subset(skc4),skc5)),skc5) ),
inference(rew,[status(thm),theory(equality)],[200,1180]),
[iquote('0:Rew:200.1,1180.2,200.1,1180.0')] ).
cnf(1183,plain,
( ~ element(set_difference(cast_as_carrier_subset(skc4),skc5),powerset(cast_as_carrier_subset(skc4)))
| ~ element(cast_as_carrier_subset(skc4),powerset(cast_as_carrier_subset(skc4)))
| ~ equal(set_intersection2(skc5,cast_as_carrier_subset(skc4)),skc5) ),
inference(rew,[status(thm),theory(equality)],[37,1182,106]),
[iquote('0:Rew:37.0,1182.2,106.0,1182.2')] ).
cnf(1184,plain,
( ~ element(set_difference(cast_as_carrier_subset(skc4),skc5),powerset(cast_as_carrier_subset(skc4)))
| ~ equal(set_intersection2(skc5,cast_as_carrier_subset(skc4)),skc5) ),
inference(mrr,[status(thm)],[1183,139]),
[iquote('0:MRR:1183.1,139.0')] ).
cnf(1196,plain,
( ~ one_sorted_str(u)
| ~ element(cast_as_carrier_subset(u),powerset(cast_as_carrier_subset(u)))
| ~ element(v,powerset(cast_as_carrier_subset(u)))
| ~ element(v,powerset(cast_as_carrier_subset(u)))
| equal(set_intersection2(v,cast_as_carrier_subset(u)),v) ),
inference(spr,[status(thm),theory(equality)],[130,134]),
[iquote('0:SpR:130.2,134.2')] ).
cnf(1201,plain,
( ~ one_sorted_str(u)
| ~ element(cast_as_carrier_subset(u),powerset(cast_as_carrier_subset(u)))
| ~ element(v,powerset(cast_as_carrier_subset(u)))
| equal(set_intersection2(v,cast_as_carrier_subset(u)),v) ),
inference(obv,[status(thm),theory(equality)],[1196]),
[iquote('0:Obv:1196.2')] ).
cnf(1202,plain,
( ~ one_sorted_str(u)
| ~ element(v,powerset(cast_as_carrier_subset(u)))
| equal(set_intersection2(v,cast_as_carrier_subset(u)),v) ),
inference(mrr,[status(thm)],[1201,133]),
[iquote('0:MRR:1201.1,133.1')] ).
cnf(2789,plain,
( ~ one_sorted_str(skc4)
| equal(set_intersection2(skc5,cast_as_carrier_subset(skc4)),skc5) ),
inference(res,[status(thm),theory(equality)],[186,1202]),
[iquote('0:Res:186.0,1202.1')] ).
cnf(2802,plain,
equal(set_intersection2(skc5,cast_as_carrier_subset(skc4)),skc5),
inference(ssi,[status(thm)],[2789,1]),
[iquote('0:SSi:2789.0,1.0')] ).
cnf(2803,plain,
( ~ element(set_difference(cast_as_carrier_subset(skc4),skc5),powerset(cast_as_carrier_subset(skc4)))
| ~ equal(skc5,skc5) ),
inference(rew,[status(thm),theory(equality)],[2802,1184]),
[iquote('0:Rew:2802.0,1184.1')] ).
cnf(2805,plain,
~ element(set_difference(cast_as_carrier_subset(skc4),skc5),powerset(cast_as_carrier_subset(skc4))),
inference(obv,[status(thm),theory(equality)],[2803]),
[iquote('0:Obv:2803.1')] ).
cnf(2892,plain,
~ element(cast_as_carrier_subset(skc4),powerset(cast_as_carrier_subset(skc4))),
inference(res,[status(thm),theory(equality)],[196,2805]),
[iquote('0:Res:196.1,2805.0')] ).
cnf(2896,plain,
$false,
inference(mrr,[status(thm)],[2892,139]),
[iquote('0:MRR:2892.0,139.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU309+1 : TPTP v8.1.0. Released v3.3.0.
% 0.06/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n006.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 13:55:55 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.46/0.70
% 0.46/0.70 SPASS V 3.9
% 0.46/0.70 SPASS beiseite: Proof found.
% 0.46/0.70 % SZS status Theorem
% 0.46/0.70 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.46/0.70 SPASS derived 2616 clauses, backtracked 0 clauses, performed 0 splits and kept 1195 clauses.
% 0.46/0.70 SPASS allocated 99361 KBytes.
% 0.46/0.70 SPASS spent 0:00:00.34 on the problem.
% 0.46/0.70 0:00:00.04 for the input.
% 0.46/0.70 0:00:00.04 for the FLOTTER CNF translation.
% 0.46/0.70 0:00:00.03 for inferences.
% 0.46/0.70 0:00:00.00 for the backtracking.
% 0.46/0.70 0:00:00.20 for the reduction.
% 0.46/0.70
% 0.46/0.70
% 0.46/0.70 Here is a proof with depth 2, length 35 :
% 0.46/0.70 % SZS output start Refutation
% See solution above
% 0.46/0.70 Formulae used in the proof : t22_pre_topc commutativity_k3_xboole_0 d3_pre_topc dt_k2_pre_topc t48_xboole_1 dt_k6_subset_1 t15_pre_topc redefinition_k5_subset_1 redefinition_k6_subset_1
% 0.46/0.70
%------------------------------------------------------------------------------