%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SET013-2 : TPTP v9.0.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n029.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 : 300s
% DateTime : Fri Jul 25 03:31:05 PM UTC 2025
% Result : Unsatisfiable 252.58s 32.06s
% Output : CNFRefutation 252.58s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named prove_c_equals_d)
% Comments :
%------------------------------------------------------------------------------
cnf(23,plain,
~ equal_sets(cs,ds),
inference(cnf,[status(esa)],[prove_c_equals_d]) ).
cnf(l0,plain,
~ equal_sets(cs,ds),
inference(instantiation,[status(thm)],[23]) ).
cnf(17,plain,
( ~ equal_sets(X0,X1)
| ~ equal_sets(X1,X2)
| equal_sets(X0,X2) ),
inference(cnf,[status(esa)],[transitivity_for_set_equal]) ).
cnf(l1,plain,
( ~ equal_sets(cs,intersection(as,bs))
| ~ equal_sets(intersection(as,bs),ds)
| equal_sets(cs,ds) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(16,plain,
( ~ equal_sets(X0,X1)
| equal_sets(X1,X0) ),
inference(cnf,[status(esa)],[symmetry_for_set_equal]) ).
cnf(l2,plain,
( ~ equal_sets(intersection(as,bs),cs)
| equal_sets(cs,intersection(as,bs)) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(21,plain,
equal_sets(intersection(as,bs),cs),
inference(cnf,[status(esa)],[intersection_of_a_and_b_is_c]) ).
cnf(l4,plain,
equal_sets(intersection(as,bs),cs),
inference(instantiation,[status(thm)],[21]) ).
cnf(l3,plain,
( ~ equal_sets(ds,intersection(as,bs))
| equal_sets(intersection(as,bs),ds) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8,plain,
( ~ equal_sets(ds,intersection(ds,ds))
| ~ equal_sets(intersection(ds,ds),intersection(as,bs))
| equal_sets(ds,intersection(as,bs)) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l526,plain,
( ~ equal_sets(intersection(ds,ds),intersection(bs,as))
| ~ equal_sets(intersection(bs,as),intersection(as,bs))
| equal_sets(intersection(ds,ds),intersection(as,bs)) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l634,plain,
( ~ equal_sets(intersection(bs,as),intersection(ds,ds))
| equal_sets(intersection(ds,ds),intersection(bs,as)) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l527,plain,
( ~ equal_sets(intersection(as,bs),intersection(bs,as))
| equal_sets(intersection(bs,as),intersection(as,bs)) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l636,plain,
( ~ equal_sets(intersection(bs,as),ds)
| ~ equal_sets(ds,intersection(ds,ds))
| equal_sets(intersection(bs,as),intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(22,plain,
equal_sets(intersection(bs,as),ds),
inference(cnf,[status(esa)],[intersection_of_b_and_a_is_d]) ).
cnf(l638,plain,
equal_sets(intersection(bs,as),ds),
inference(instantiation,[status(thm)],[22]) ).
cnf(14,plain,
( ~ subset(X0,X1)
| ~ subset(X1,X0)
| equal_sets(X1,X0) ),
inference(cnf,[status(esa)],[subsets_are_set_equal_sets]) ).
cnf(l77,plain,
( ~ subset(intersection(ds,ds),ds)
| ~ subset(ds,intersection(ds,ds))
| equal_sets(ds,intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(12,plain,
( ~ equal_sets(X0,X1)
| subset(X0,X1) ),
inference(cnf,[status(esa)],[set_equal_sets_are_subsets1]) ).
cnf(l79,plain,
( ~ equal_sets(intersection(ds,ds),ds)
| subset(intersection(ds,ds),ds) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l730,plain,
( ~ equal_sets(ds,union(intersection(ds,ds),ds))
| ~ equal_sets(union(intersection(ds,ds),ds),intersection(ds,ds))
| equal_sets(ds,intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l733,plain,
( ~ subset(union(intersection(ds,ds),ds),ds)
| ~ subset(ds,union(intersection(ds,ds),ds))
| equal_sets(ds,union(intersection(ds,ds),ds)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l740,plain,
( ~ subset(intersection(ds,ds),union(intersection(ds,ds),ds))
| ~ subset(union(intersection(ds,ds),ds),intersection(ds,ds))
| equal_sets(union(intersection(ds,ds),ds),intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l101,plain,
( ~ equal_sets(intersection(ds,ds),union(ds,ds))
| ~ equal_sets(union(ds,ds),ds)
| equal_sets(intersection(ds,ds),ds) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(3,plain,
( ~ member(member_of_1_not_of_2(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf,[status(esa)],[subsets_axiom2]) ).
cnf(l743,plain,
( ~ member(member_of_1_not_of_2(intersection(ds,ds),union(intersection(ds,ds),ds)),union(intersection(ds,ds),ds))
| subset(intersection(ds,ds),union(intersection(ds,ds),ds)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(2,plain,
( member(member_of_1_not_of_2(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf,[status(esa)],[subsets_axiom1]) ).
cnf(l736,plain,
( member(member_of_1_not_of_2(ds,union(intersection(ds,ds),ds)),ds)
| subset(ds,union(intersection(ds,ds),ds)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l107,plain,
( member(member_of_1_not_of_2(ds,intersection(ds,ds)),ds)
| subset(ds,intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1858,plain,
( ~ member(member_of_1_not_of_2(union(intersection(ds,ds),ds),intersection(ds,ds)),intersection(ds,ds))
| subset(union(intersection(ds,ds),ds),intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(8,plain,
( ~ member(X0,union(X1,X2))
| member(X0,X1)
| member(X0,X2) ),
inference(cnf,[status(esa)],[member_of_union_is_member_of_one_set]) ).
cnf(l1859,plain,
( ~ member(member_of_1_not_of_2(union(intersection(ds,ds),ds),intersection(ds,ds)),union(intersection(ds,ds),ds))
| member(member_of_1_not_of_2(union(intersection(ds,ds),ds),intersection(ds,ds)),intersection(ds,ds))
| member(member_of_1_not_of_2(union(intersection(ds,ds),ds),intersection(ds,ds)),ds) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(6,plain,
( ~ member(X0,X1)
| member(X0,union(X1,X2)) ),
inference(cnf,[status(esa)],[member_of_set1_is_member_of_union]) ).
cnf(l113,plain,
( ~ member(member_of_1_not_of_2(ds,intersection(ds,ds)),ds)
| member(member_of_1_not_of_2(ds,intersection(ds,ds)),union(ds,X2_113)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1868,plain,
( member(member_of_1_not_of_2(union(intersection(ds,ds),ds),intersection(ds,ds)),union(intersection(ds,ds),ds))
| subset(union(intersection(ds,ds),ds),intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(7,plain,
( ~ member(X0,X1)
| member(X0,union(X2,X1)) ),
inference(cnf,[status(esa)],[member_of_set2_is_member_of_union]) ).
cnf(l1862,plain,
( ~ member(member_of_1_not_of_2(ds,union(intersection(ds,ds),ds)),ds)
| member(member_of_1_not_of_2(ds,union(intersection(ds,ds),ds)),union(intersection(ds,ds),ds)) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1867,plain,
( ~ member(member_of_1_not_of_2(ds,union(intersection(ds,ds),ds)),union(intersection(ds,ds),ds))
| subset(ds,union(intersection(ds,ds),ds)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l130,plain,
( ~ subset(union(ds,ds),intersection(ds,ds))
| ~ subset(intersection(ds,ds),union(ds,ds))
| equal_sets(intersection(ds,ds),union(ds,ds)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1857,plain,
( ~ member(member_of_1_not_of_2(intersection(ds,ds),union(intersection(ds,ds),ds)),intersection(ds,ds))
| member(member_of_1_not_of_2(intersection(ds,ds),union(intersection(ds,ds),ds)),union(intersection(ds,ds),ds)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l103,plain,
( ~ equal_sets(ds,union(ds,ds))
| equal_sets(union(ds,ds),ds) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l105,plain,
( ~ subset(union(ds,ds),ds)
| ~ subset(ds,union(ds,ds))
| equal_sets(ds,union(ds,ds)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(9,plain,
( ~ member(X0,X1)
| ~ member(X0,X2)
| member(X0,intersection(X1,X2)) ),
inference(cnf,[status(esa)],[member_of_both_is_member_of_intersection]) ).
cnf(l1907,plain,
( ~ member(member_of_1_not_of_2(union(intersection(ds,ds),ds),intersection(ds,ds)),ds)
| ~ member(member_of_1_not_of_2(union(intersection(ds,ds),ds),intersection(ds,ds)),ds)
| member(member_of_1_not_of_2(union(intersection(ds,ds),ds),intersection(ds,ds)),intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l183,plain,
( member(member_of_1_not_of_2(intersection(ds,ds),union(ds,ds)),intersection(ds,ds))
| subset(intersection(ds,ds),union(ds,ds)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1852,plain,
( ~ subset(intersection(bs,as),intersection(as,bs))
| ~ subset(intersection(as,bs),intersection(bs,as))
| equal_sets(intersection(as,bs),intersection(bs,as)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l157,plain,
( member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),union(ds,ds))
| subset(union(ds,ds),intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1870,plain,
( member(member_of_1_not_of_2(intersection(ds,ds),union(intersection(ds,ds),ds)),intersection(ds,ds))
| subset(intersection(ds,ds),union(intersection(ds,ds),ds)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l122,plain,
( ~ member(member_of_1_not_of_2(ds,intersection(ds,ds)),union(ds,X2_113))
| ~ member(member_of_1_not_of_2(ds,intersection(ds,ds)),union(ds,X2_113))
| member(member_of_1_not_of_2(ds,intersection(ds,ds)),intersection(union(ds,X2_113),union(ds,X2_113))) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l250,plain,
( member(member_of_1_not_of_2(union(ds,ds),ds),union(ds,ds))
| subset(union(ds,ds),ds) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1914,plain,
( ~ member(member_of_1_not_of_2(ds,intersection(ds,ds)),intersection(union(ds,X2_113),union(ds,X2_113)))
| member(member_of_1_not_of_2(ds,intersection(ds,ds)),union(intersection(union(ds,X2_113),union(ds,X2_113)),X2_1914)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1850,plain,
( ~ member(member_of_1_not_of_2(union(intersection(ds,ds),ds),ds),ds)
| subset(union(intersection(ds,ds),ds),ds) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1853,plain,
( member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(bs,as))
| subset(intersection(bs,as),intersection(as,bs)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l329,plain,
( ~ member(member_of_1_not_of_2(intersection(ds,ds),union(ds,ds)),union(ds,ds))
| ~ member(member_of_1_not_of_2(intersection(ds,ds),union(ds,ds)),intersection(ds,ds))
| member(member_of_1_not_of_2(intersection(ds,ds),union(ds,ds)),intersection(union(ds,ds),intersection(ds,ds))) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1854,plain,
( member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),intersection(as,bs))
| subset(intersection(as,bs),intersection(bs,as)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l167,plain,
( ~ member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),intersection(ds,ds))
| ~ member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),union(ds,ds))
| member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),intersection(intersection(ds,ds),union(ds,ds))) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l123,plain,
( ~ member(member_of_1_not_of_2(ds,union(ds,ds)),union(ds,ds))
| subset(ds,union(ds,ds)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1351,plain,
( ~ member(member_of_1_not_of_2(ds,union(ds,ds)),ds)
| member(member_of_1_not_of_2(ds,union(ds,ds)),union(ds,ds)) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1855,plain,
( ~ member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),intersection(as,bs))
| member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),union(intersection(as,bs),X2_1855)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1851,plain,
( ~ member(member_of_1_not_of_2(union(intersection(ds,ds),ds),ds),union(intersection(ds,ds),ds))
| member(member_of_1_not_of_2(union(intersection(ds,ds),ds),ds),intersection(ds,ds))
| member(member_of_1_not_of_2(union(intersection(ds,ds),ds),ds),ds) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(11,plain,
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
inference(cnf,[status(esa)],[member_of_intersection_is_member_of_set2]) ).
cnf(l1856,plain,
( ~ member(member_of_1_not_of_2(union(intersection(ds,ds),ds),ds),intersection(ds,ds))
| member(member_of_1_not_of_2(union(intersection(ds,ds),ds),ds),ds) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l255,plain,
( ~ member(member_of_1_not_of_2(union(ds,ds),ds),union(ds,ds))
| member(member_of_1_not_of_2(union(ds,ds),ds),ds)
| member(member_of_1_not_of_2(union(ds,ds),ds),ds) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1866,plain,
( member(member_of_1_not_of_2(union(intersection(ds,ds),ds),ds),union(intersection(ds,ds),ds))
| subset(union(intersection(ds,ds),ds),ds) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l262,plain,
( ~ member(member_of_1_not_of_2(union(ds,ds),ds),ds)
| subset(union(ds,ds),ds) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l370,plain,
( ~ member(member_of_1_not_of_2(intersection(ds,ds),union(ds,ds)),ds)
| member(member_of_1_not_of_2(intersection(ds,ds),union(ds,ds)),union(ds,ds)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1429,plain,
( ~ member(member_of_1_not_of_2(union(ds,ds),ds),ds)
| subset(union(ds,ds),ds) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(10,plain,
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
inference(cnf,[status(esa)],[member_of_intersection_is_member_of_set1]) ).
cnf(l1881,plain,
( ~ member(member_of_1_not_of_2(intersection(ds,ds),union(ds,ds)),intersection(union(ds,ds),intersection(ds,ds)))
| member(member_of_1_not_of_2(intersection(ds,ds),union(ds,ds)),union(ds,ds)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1861,plain,
( ~ member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(bs,as))
| ~ member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(bs,as))
| member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(intersection(bs,as),intersection(bs,as))) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l385,plain,
( ~ member(member_of_1_not_of_2(intersection(ds,ds),union(ds,ds)),intersection(ds,ds))
| member(member_of_1_not_of_2(intersection(ds,ds),union(ds,ds)),ds) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1525,plain,
( ~ member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),intersection(intersection(ds,ds),union(ds,ds)))
| member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1556,plain,
( ~ member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),intersection(ds,ds))
| subset(union(ds,ds),intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1915,plain,
( ~ member(member_of_1_not_of_2(ds,intersection(ds,ds)),union(intersection(union(ds,X2_113),union(ds,X2_113)),X2_1914))
| ~ member(member_of_1_not_of_2(ds,intersection(ds,ds)),intersection(ds,ds))
| member(member_of_1_not_of_2(ds,intersection(ds,ds)),intersection(union(intersection(union(ds,X2_113),union(ds,X2_113)),X2_1914),intersection(ds,ds))) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1886,plain,
( ~ member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(intersection(bs,as),intersection(bs,as)))
| ~ member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(as,bs))
| member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(intersection(intersection(bs,as),intersection(bs,as)),intersection(as,bs))) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l168,plain,
( ~ member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),ds)
| ~ member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),ds)
| member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1882,plain,
( ~ member(member_of_1_not_of_2(intersection(ds,ds),union(ds,ds)),union(ds,ds))
| subset(intersection(ds,ds),union(ds,ds)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l374,plain,
( ~ member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),union(ds,ds))
| member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),ds)
| member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),ds) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1892,plain,
( ~ member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(intersection(intersection(bs,as),intersection(bs,as)),intersection(as,bs)))
| member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(as,bs)) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1434,plain,
( member(member_of_1_not_of_2(ds,union(ds,ds)),ds)
| subset(ds,union(ds,ds)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1900,plain,
( ~ member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(as,bs))
| subset(intersection(bs,as),intersection(as,bs)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1916,plain,
( ~ member(member_of_1_not_of_2(ds,intersection(ds,ds)),intersection(union(intersection(union(ds,X2_113),union(ds,X2_113)),X2_1914),intersection(ds,ds)))
| member(member_of_1_not_of_2(ds,intersection(ds,ds)),intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1917,plain,
( ~ member(member_of_1_not_of_2(ds,intersection(ds,ds)),intersection(ds,ds))
| subset(ds,intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1919,plain,
( ~ member(member_of_1_not_of_2(ds,intersection(ds,ds)),ds)
| ~ member(member_of_1_not_of_2(ds,intersection(ds,ds)),ds)
| member(member_of_1_not_of_2(ds,intersection(ds,ds)),intersection(ds,ds)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1888,plain,
( ~ member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),as)
| ~ member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),bs)
| member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(as,bs)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1865,plain,
( ~ member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),intersection(bs,as))
| ~ member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),union(intersection(as,bs),X2_1855))
| member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),intersection(intersection(bs,as),union(intersection(as,bs),X2_1855))) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l665,plain,
( ~ member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),union(ds,ds))
| member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),ds)
| member(member_of_1_not_of_2(union(ds,ds),intersection(ds,ds)),ds) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1910,plain,
( ~ member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),bs)
| ~ member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),as)
| member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),intersection(bs,as)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1869,plain,
( ~ member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),intersection(intersection(bs,as),union(intersection(as,bs),X2_1855)))
| member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),intersection(bs,as)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1902,plain,
( ~ member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(bs,as))
| member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),as) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1873,plain,
( ~ member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),intersection(bs,as))
| subset(intersection(as,bs),intersection(bs,as)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1921,plain,
( ~ member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),intersection(as,bs))
| member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),bs) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1904,plain,
( ~ member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),intersection(bs,as))
| member(member_of_1_not_of_2(intersection(bs,as),intersection(as,bs)),bs) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1911,plain,
( ~ member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),intersection(as,bs))
| member(member_of_1_not_of_2(intersection(as,bs),intersection(bs,as)),as) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l4,l3,l8,l526,l634,l527,l636,l638,l77,l79,l730,l733,l740,l101,l743,l736,l107,l1858,l1859,l113,l1868,l1862,l1867,l130,l1857,l103,l105,l1907,l183,l1852,l157,l1870,l122,l250,l1914,l1850,l1853,l329,l1854,l167,l123,l1351,l1855,l1851,l1856,l255,l1866,l262,l370,l1429,l1881,l1861,l385,l1525,l1556,l1915,l1886,l168,l1882,l374,l1892,l1434,l1900,l1916,l1917,l1919,l1888,l1865,l665,l1910,l1869,l1902,l1873,l1921,l1904,l1911]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SET013-2 : TPTP v9.0.0. Bugfixed v2.1.0.
% 0.03/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n029.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Mon Jul 21 19:13:34 EDT 2025
% 0.13/0.33 % CPUTime :
% 0.13/0.33 % launching worker at depth: 1
% 0.13/0.33 % launching worker at depth: 2
% 0.13/0.33 % launching worker at depth: 3
% 0.13/0.33 % launching worker at depth: 7
% 0.13/0.33 % launching worker at depth: 8
% 0.13/0.33 % launching worker at depth: 5
% 0.13/0.33 % launching worker at depth: 6
% 0.13/0.33 % launching worker at depth: 4
% 0.13/0.33 % launching worker at depth: 9
% 0.13/0.33 % launching worker at depth: 10
% 0.13/0.34 % launching worker at depth: 11
% 0.13/0.36 % launching worker at depth: 12
% 2.75/0.73 % launching worker at depth: 13
% 252.58/32.06 % SZS status Theorem for theBenchmark
% 252.58/32.06 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------