%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SET675+3 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n025.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 05:28:01 EDT 2022
% Result : Theorem 0.18s 0.47s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 14
% Syntax : Number of clauses : 43 ( 13 unt; 0 nHn; 43 RR)
% Number of literals : 97 ( 0 equ; 62 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 9 con; 0-4 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(4,axiom,
ilf_type(u,set_type),
file('SET675+3.p',unknown),
[] ).
cnf(9,axiom,
ilf_type(skc6,relation_type(skc5,skc4)),
file('SET675+3.p',unknown),
[] ).
cnf(20,axiom,
( ~ relation_like(u)
| ~ ilf_type(u,set_type)
| ilf_type(u,binary_relation_type) ),
file('SET675+3.p',unknown),
[] ).
cnf(23,axiom,
( ~ ilf_type(u,binary_relation_type)
| equal(image(u,domain_of(u)),range_of(u)) ),
file('SET675+3.p',unknown),
[] ).
cnf(24,axiom,
( ~ ilf_type(u,binary_relation_type)
| equal(inverse2(u,range_of(u)),domain_of(u)) ),
file('SET675+3.p',unknown),
[] ).
cnf(37,axiom,
( ~ ilf_type(u,set_type)
| ~ ilf_type(v,set_type)
| ~ ilf_type(w,subset_type(cross_product(u,v)))
| relation_like(w) ),
file('SET675+3.p',unknown),
[] ).
cnf(44,axiom,
( ~ ilf_type(u,relation_type(v,w))
| ~ ilf_type(v,set_type)
| ~ ilf_type(w,set_type)
| ilf_type(u,subset_type(cross_product(v,w))) ),
file('SET675+3.p',unknown),
[] ).
cnf(47,axiom,
( ~ ilf_type(u,set_type)
| ~ ilf_type(v,set_type)
| ~ ilf_type(w,relation_type(u,v))
| equal(range__dfg(u,v,w),range_of(w)) ),
file('SET675+3.p',unknown),
[] ).
cnf(49,axiom,
( ~ ilf_type(u,set_type)
| ~ ilf_type(v,set_type)
| ~ ilf_type(w,relation_type(u,v))
| equal(domain__dfg(u,v,w),domain_of(w)) ),
file('SET675+3.p',unknown),
[] ).
cnf(54,axiom,
( ~ ilf_type(u,set_type)
| ~ ilf_type(v,set_type)
| ~ ilf_type(w,relation_type(u,v))
| equal(inverse4(u,v,w,v),domain__dfg(u,v,w)) ),
file('SET675+3.p',unknown),
[] ).
cnf(55,axiom,
( ~ ilf_type(u,set_type)
| ~ ilf_type(v,set_type)
| ~ ilf_type(w,relation_type(u,v))
| equal(image4(u,v,w,u),range__dfg(u,v,w)) ),
file('SET675+3.p',unknown),
[] ).
cnf(58,axiom,
( ~ ilf_type(u,set_type)
| ~ ilf_type(v,set_type)
| ~ ilf_type(w,relation_type(u,v))
| ~ ilf_type(x,set_type)
| equal(inverse4(u,v,w,x),inverse2(w,x)) ),
file('SET675+3.p',unknown),
[] ).
cnf(59,axiom,
( ~ ilf_type(u,set_type)
| ~ ilf_type(v,set_type)
| ~ ilf_type(w,relation_type(u,v))
| ~ ilf_type(x,set_type)
| equal(image4(u,v,w,x),image(w,x)) ),
file('SET675+3.p',unknown),
[] ).
cnf(60,axiom,
( ~ equal(image4(skc5,skc4,skc6,inverse4(skc5,skc4,skc6,skc4)),range__dfg(skc5,skc4,skc6))
| ~ equal(inverse4(skc5,skc4,skc6,image4(skc5,skc4,skc6,skc5)),domain__dfg(skc5,skc4,skc6)) ),
file('SET675+3.p',unknown),
[] ).
cnf(67,plain,
( ~ relation_like(u)
| ilf_type(u,binary_relation_type) ),
inference(mrr,[status(thm)],[20,4]),
[iquote('0:MRR:20.1,4.0')] ).
cnf(74,plain,
( ~ ilf_type(u,subset_type(cross_product(v,w)))
| relation_like(u) ),
inference(mrr,[status(thm)],[37,4]),
[iquote('0:MRR:37.0,37.1,4.0,4.0')] ).
cnf(83,plain,
( ~ ilf_type(u,relation_type(v,w))
| ilf_type(u,subset_type(cross_product(v,w))) ),
inference(mrr,[status(thm)],[44,4]),
[iquote('0:MRR:44.1,44.2,4.0,4.0')] ).
cnf(86,plain,
( ~ ilf_type(u,relation_type(v,w))
| equal(range__dfg(v,w,u),range_of(u)) ),
inference(mrr,[status(thm)],[47,4]),
[iquote('0:MRR:47.0,47.1,4.0,4.0')] ).
cnf(89,plain,
( ~ ilf_type(u,relation_type(v,w))
| equal(domain__dfg(v,w,u),domain_of(u)) ),
inference(mrr,[status(thm)],[49,4]),
[iquote('0:MRR:49.0,49.1,4.0,4.0')] ).
cnf(95,plain,
( ~ ilf_type(u,set_type)
| ~ ilf_type(v,set_type)
| ~ ilf_type(w,relation_type(u,v))
| equal(inverse4(u,v,w,v),domain_of(w)) ),
inference(rew,[status(thm),theory(equality)],[89,54]),
[iquote('0:Rew:89.1,54.3')] ).
cnf(96,plain,
( ~ ilf_type(u,relation_type(v,w))
| equal(inverse4(v,w,u,w),domain_of(u)) ),
inference(mrr,[status(thm)],[95,4]),
[iquote('0:MRR:95.0,95.1,4.0,4.0')] ).
cnf(97,plain,
( ~ ilf_type(u,set_type)
| ~ ilf_type(v,set_type)
| ~ ilf_type(w,relation_type(u,v))
| equal(image4(u,v,w,u),range_of(w)) ),
inference(rew,[status(thm),theory(equality)],[86,55]),
[iquote('0:Rew:86.1,55.3')] ).
cnf(98,plain,
( ~ ilf_type(u,relation_type(v,w))
| equal(image4(v,w,u,v),range_of(u)) ),
inference(mrr,[status(thm)],[97,4]),
[iquote('0:MRR:97.0,97.1,4.0,4.0')] ).
cnf(101,plain,
( ~ ilf_type(u,relation_type(v,w))
| equal(inverse4(v,w,u,x),inverse2(u,x)) ),
inference(mrr,[status(thm)],[58,4]),
[iquote('0:MRR:58.0,58.1,58.3,4.0,4.0,4.0')] ).
cnf(103,plain,
( ~ ilf_type(u,relation_type(v,w))
| equal(inverse2(u,w),domain_of(u)) ),
inference(rew,[status(thm),theory(equality)],[101,96]),
[iquote('0:Rew:101.1,96.1')] ).
cnf(104,plain,
( ~ ilf_type(u,relation_type(v,w))
| equal(image4(v,w,u,x),image(u,x)) ),
inference(mrr,[status(thm)],[59,4]),
[iquote('0:MRR:59.0,59.1,59.3,4.0,4.0,4.0')] ).
cnf(106,plain,
( ~ ilf_type(u,relation_type(v,w))
| equal(image(u,v),range_of(u)) ),
inference(rew,[status(thm),theory(equality)],[104,98]),
[iquote('0:Rew:104.1,98.1')] ).
cnf(107,plain,
equal(image(skc6,skc5),range_of(skc6)),
inference(res,[status(thm),theory(equality)],[9,106]),
[iquote('0:Res:9.0,106.0')] ).
cnf(109,plain,
equal(image4(skc5,skc4,skc6,u),image(skc6,u)),
inference(res,[status(thm),theory(equality)],[9,104]),
[iquote('0:Res:9.0,104.0')] ).
cnf(110,plain,
equal(inverse2(skc6,skc4),domain_of(skc6)),
inference(res,[status(thm),theory(equality)],[9,103]),
[iquote('0:Res:9.0,103.0')] ).
cnf(112,plain,
equal(inverse4(skc5,skc4,skc6,u),inverse2(skc6,u)),
inference(res,[status(thm),theory(equality)],[9,101]),
[iquote('0:Res:9.0,101.0')] ).
cnf(114,plain,
equal(domain__dfg(skc5,skc4,skc6),domain_of(skc6)),
inference(res,[status(thm),theory(equality)],[9,89]),
[iquote('0:Res:9.0,89.0')] ).
cnf(116,plain,
equal(range__dfg(skc5,skc4,skc6),range_of(skc6)),
inference(res,[status(thm),theory(equality)],[9,86]),
[iquote('0:Res:9.0,86.0')] ).
cnf(117,plain,
ilf_type(skc6,subset_type(cross_product(skc5,skc4))),
inference(res,[status(thm),theory(equality)],[9,83]),
[iquote('0:Res:9.0,83.0')] ).
cnf(118,plain,
( ~ equal(image4(skc5,skc4,skc6,inverse4(skc5,skc4,skc6,skc4)),range__dfg(skc5,skc4,skc6))
| ~ equal(inverse4(skc5,skc4,skc6,image4(skc5,skc4,skc6,skc5)),domain_of(skc6)) ),
inference(rew,[status(thm),theory(equality)],[114,60]),
[iquote('0:Rew:114.0,60.1')] ).
cnf(119,plain,
( ~ equal(inverse2(skc6,range_of(skc6)),domain_of(skc6))
| ~ equal(image(skc6,domain_of(skc6)),range_of(skc6)) ),
inference(rew,[status(thm),theory(equality)],[107,118,109,112,110,116]),
[iquote('0:Rew:107.0,118.1,109.0,118.1,112.0,118.1,110.0,118.0,112.0,118.0,109.0,118.0,116.0,118.0')] ).
cnf(134,plain,
relation_like(skc6),
inference(res,[status(thm),theory(equality)],[117,74]),
[iquote('0:Res:117.0,74.0')] ).
cnf(415,plain,
( ~ ilf_type(skc6,binary_relation_type)
| ~ equal(domain_of(skc6),domain_of(skc6))
| ~ equal(image(skc6,domain_of(skc6)),range_of(skc6)) ),
inference(spl,[status(thm),theory(equality)],[24,119]),
[iquote('0:SpL:24.1,119.0')] ).
cnf(420,plain,
( ~ ilf_type(skc6,binary_relation_type)
| ~ equal(image(skc6,domain_of(skc6)),range_of(skc6)) ),
inference(obv,[status(thm),theory(equality)],[415]),
[iquote('0:Obv:415.1')] ).
cnf(421,plain,
( ~ ilf_type(skc6,binary_relation_type)
| ~ equal(range_of(skc6),range_of(skc6)) ),
inference(rew,[status(thm),theory(equality)],[23,420]),
[iquote('0:Rew:23.1,420.1')] ).
cnf(422,plain,
~ ilf_type(skc6,binary_relation_type),
inference(obv,[status(thm),theory(equality)],[421]),
[iquote('0:Obv:421.1')] ).
cnf(424,plain,
~ relation_like(skc6),
inference(res,[status(thm),theory(equality)],[67,422]),
[iquote('0:Res:67.1,422.0')] ).
cnf(425,plain,
$false,
inference(ssi,[status(thm)],[424,134]),
[iquote('0:SSi:424.0,134.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SET675+3 : TPTP v8.1.0. Released v2.2.0.
% 0.06/0.12 % Command : run_spass %d %s
% 0.11/0.33 % Computer : n025.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Mon Jul 11 08:11:47 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.18/0.47
% 0.18/0.47 SPASS V 3.9
% 0.18/0.47 SPASS beiseite: Proof found.
% 0.18/0.47 % SZS status Theorem
% 0.18/0.47 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.47 SPASS derived 305 clauses, backtracked 0 clauses, performed 0 splits and kept 257 clauses.
% 0.18/0.47 SPASS allocated 98056 KBytes.
% 0.18/0.47 SPASS spent 0:00:00.13 on the problem.
% 0.18/0.47 0:00:00.04 for the input.
% 0.18/0.47 0:00:00.04 for the FLOTTER CNF translation.
% 0.18/0.47 0:00:00.01 for inferences.
% 0.18/0.47 0:00:00.00 for the backtracking.
% 0.18/0.47 0:00:00.03 for the reduction.
% 0.18/0.47
% 0.18/0.47
% 0.18/0.47 Here is a proof with depth 2, length 43 :
% 0.18/0.47 % SZS output start Refutation
% See solution above
% 0.18/0.47 Formulae used in the proof : p35 prove_relset_1_39 p12 p1 p2 p23 p4 p29 p27 p3 p33 p31
% 0.18/0.47
%------------------------------------------------------------------------------