%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SET503-6 : TPTP v8.1.0. Bugfixed v2.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n017.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:26:38 EDT 2022 % Result : Unsatisfiable 4.36s 4.57s % Output : Refutation 4.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SET503-6 : TPTP v8.1.0. Bugfixed v2.1.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n017.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 : Sat Jul 9 23:17:02 EDT 2022 % 0.12/0.33 % CPUTime : % 4.36/4.57 % 4.36/4.57 SPASS V 3.9 % 4.36/4.57 SPASS beiseite: Proof found. % 4.36/4.57 % SZS status Theorem % 4.36/4.57 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.36/4.57 SPASS derived 14515 clauses, backtracked 610 clauses, performed 5 splits and kept 6334 clauses. % 4.36/4.57 SPASS allocated 89829 KBytes. % 4.36/4.57 SPASS spent 0:00:04.22 on the problem. % 4.36/4.57 0:00:00.04 for the input. % 4.36/4.57 0:00:00.00 for the FLOTTER CNF translation. % 4.36/4.57 0:00:00.14 for inferences. % 4.36/4.57 0:00:00.26 for the backtracking. % 4.36/4.57 0:00:03.68 for the reduction. % 4.36/4.57 % 4.36/4.57 % 4.36/4.57 Here is a proof with depth 12, length 130 : % 4.36/4.57 % SZS output start Refutation % 4.36/4.57 1[0:Inp] || -> member(universal_class,x__dfg)*. % 4.36/4.57 2[0:Inp] || member(u,v)*+ subclass(v,w)* -> member(u,w)*. % 4.36/4.57 3[0:Inp] || -> subclass(u,v) member(not_subclass_element(u,v),u)*. % 4.36/4.57 4[0:Inp] || member(not_subclass_element(u,v),v)* -> subclass(u,v). % 4.36/4.57 5[0:Inp] || -> subclass(u,universal_class)*. % 4.36/4.57 7[0:Inp] || equal(u,v) -> subclass(v,u)*. % 4.36/4.57 8[0:Inp] || subclass(u,v)*+ subclass(v,u)* -> equal(v,u). % 4.36/4.57 9[0:Inp] || member(u,unordered_pair(v,w))* -> equal(u,w) equal(u,v). % 4.36/4.57 11[0:Inp] || member(u,universal_class) -> member(u,unordered_pair(v,u))*. % 4.36/4.57 12[0:Inp] || -> member(unordered_pair(u,v),universal_class)*. % 4.36/4.57 13[0:Inp] || -> equal(unordered_pair(u,u),singleton(u))**. % 4.36/4.57 22[0:Inp] || member(u,intersection(v,w))* -> member(u,v). % 4.36/4.57 23[0:Inp] || member(u,intersection(v,w))* -> member(u,w). % 4.36/4.57 24[0:Inp] || member(u,v) member(u,w) -> member(u,intersection(w,v))*. % 4.36/4.57 25[0:Inp] || member(u,v) member(u,complement(v))* -> . % 4.36/4.57 26[0:Inp] || member(u,universal_class) -> member(u,v) member(u,complement(v))*. % 4.36/4.57 27[0:Inp] || -> equal(complement(intersection(complement(u),complement(v))),union(u,v))**. % 4.36/4.57 28[0:Inp] || -> equal(intersection(complement(intersection(u,v)),complement(intersection(complement(u),complement(v)))),symmetric_difference(u,v))**. % 4.36/4.57 44[0:Inp] || -> equal(union(u,singleton(u)),successor(u))**. % 4.36/4.57 67[0:Inp] || -> equal(u,null_class) member(regular(u),u)*. % 4.36/4.57 68[0:Inp] || -> equal(u,null_class) equal(intersection(u,regular(u)),null_class)**. % 4.36/4.57 71[0:Inp] || member(u,universal_class) -> equal(u,null_class) member(apply(choice,u),u)*. % 4.36/4.57 114[0:Rew:27.0,28.0] || -> equal(intersection(complement(intersection(u,v)),union(u,v)),symmetric_difference(u,v))**. % 4.36/4.57 116[0:Res:1.0,2.1] || subclass(x__dfg,u)* -> member(universal_class,u). % 4.36/4.57 129[0:SpR:13.0,12.0] || -> member(singleton(u),universal_class)*. % 4.36/4.57 131[0:Res:5.0,116.0] || -> member(universal_class,universal_class)*. % 4.36/4.57 163[0:SpR:13.0,11.1] || member(u,universal_class) -> member(u,singleton(u))*. % 4.36/4.57 169[0:Res:67.1,25.1] || member(regular(complement(u)),u)* -> equal(complement(u),null_class). % 4.36/4.57 200[0:Res:3.1,23.0] || -> subclass(intersection(u,v),w) member(not_subclass_element(intersection(u,v),w),v)*. % 4.36/4.57 216[0:Res:67.1,22.0] || -> equal(intersection(u,v),null_class) member(regular(intersection(u,v)),u)*. % 4.36/4.57 217[0:Res:3.1,22.0] || -> subclass(intersection(u,v),w) member(not_subclass_element(intersection(u,v),w),u)*. % 4.36/4.57 373[0:Res:26.2,4.0] || member(not_subclass_element(u,complement(v)),universal_class)*+ -> member(not_subclass_element(u,complement(v)),v)* subclass(u,complement(v)). % 4.36/4.57 438[0:Res:5.0,8.0] || subclass(universal_class,u)* -> equal(universal_class,u). % 4.36/4.57 475[0:Res:131.0,2.0] || subclass(universal_class,u)* -> member(universal_class,u). % 4.36/4.57 481[0:Res:67.1,2.0] || subclass(u,v) -> equal(u,null_class) member(regular(u),v)*. % 4.36/4.57 482[0:Res:3.1,2.0] || subclass(u,v) -> subclass(u,w) member(not_subclass_element(u,w),v)*. % 4.36/4.57 506[0:Res:7.1,475.0] || equal(u,universal_class) -> member(universal_class,u)*. % 4.36/4.57 526[0:Res:506.1,25.1] || equal(complement(u),universal_class) member(universal_class,u)* -> . % 4.36/4.57 626[0:Res:163.1,526.1] || member(universal_class,universal_class) equal(complement(singleton(universal_class)),universal_class)** -> . % 4.36/4.57 634[0:MRR:626.0,131.0] || equal(complement(singleton(universal_class)),universal_class)** -> . % 4.36/4.57 643[0:SpL:13.0,9.0] || member(u,singleton(v))* -> equal(u,v) equal(u,v). % 4.36/4.57 655[0:Obv:643.1] || member(u,singleton(v))* -> equal(u,v). % 4.36/4.57 660[0:Res:67.1,655.0] || -> equal(singleton(u),null_class) equal(regular(singleton(u)),u)**. % 4.36/4.57 661[0:Res:3.1,655.0] || -> subclass(singleton(u),v) equal(not_subclass_element(singleton(u),v),u)**. % 4.36/4.57 663[0:Res:71.2,655.0] || member(singleton(u),universal_class) -> equal(singleton(u),null_class) equal(apply(choice,singleton(u)),u)**. % 4.36/4.57 667[0:MRR:663.0,129.0] || -> equal(singleton(u),null_class) equal(apply(choice,singleton(u)),u)**. % 4.36/4.57 760[0:SpR:660.1,67.1] || -> equal(singleton(u),null_class) equal(singleton(u),null_class) member(u,singleton(u))*. % 4.36/4.57 761[0:SpR:660.1,68.1] || -> equal(singleton(u),null_class) equal(singleton(u),null_class) equal(intersection(singleton(u),u),null_class)**. % 4.36/4.57 763[0:Obv:760.0] || -> equal(singleton(u),null_class) member(u,singleton(u))*. % 4.36/4.57 764[0:Obv:761.0] || -> equal(singleton(u),null_class) equal(intersection(singleton(u),u),null_class)**. % 4.36/4.57 1460[0:Res:24.2,2.0] || member(u,v)* member(u,w)* subclass(intersection(w,v),x)*+ -> member(u,x)*. % 4.36/4.57 2393[0:SpR:764.1,24.2] || member(u,v) member(u,singleton(v))* -> equal(singleton(v),null_class) member(u,null_class). % 4.36/4.57 3397[0:SpR:661.1,3.1] || -> subclass(singleton(u),v)* subclass(singleton(u),v)* member(u,singleton(u))*. % 4.36/4.57 3401[0:Obv:3397.0] || -> subclass(singleton(u),v)* member(u,singleton(u))*. % 4.36/4.57 3402[0:Rew:763.0,3401.0] || -> subclass(null_class,u)* member(v,singleton(v))*. % 4.36/4.57 3405[1:Spt:3402.0] || -> subclass(null_class,u)*. % 4.36/4.57 3412[1:Res:3405.0,8.0] || subclass(u,null_class)* -> equal(u,null_class). % 4.36/4.57 3635[0:Res:481.2,169.0] || subclass(complement(u),u)* -> equal(complement(u),null_class) equal(complement(u),null_class). % 4.36/4.57 3650[0:Obv:3635.1] || subclass(complement(u),u)* -> equal(complement(u),null_class). % 4.36/4.57 3659[0:Res:5.0,3650.0] || -> equal(complement(universal_class),null_class)**. % 4.36/4.57 3671[0:SpR:3659.0,27.0] || -> equal(complement(intersection(null_class,complement(u))),union(universal_class,u))**. % 4.36/4.57 3673[0:SpR:3659.0,27.0] || -> equal(complement(intersection(complement(u),null_class)),union(u,universal_class))**. % 4.36/4.57 3688[0:SpL:3659.0,25.1] || member(u,universal_class) member(u,null_class)* -> . % 4.36/4.57 4593[0:Res:200.1,4.0] || -> subclass(intersection(u,v),v)* subclass(intersection(u,v),v)*. % 4.36/4.57 4595[0:Obv:4593.0] || -> subclass(intersection(u,v),v)*. % 4.36/4.57 4626[1:Res:4595.0,3412.0] || -> equal(intersection(u,null_class),null_class)**. % 4.36/4.57 4632[1:Rew:4626.0,3673.0] || -> equal(union(u,universal_class),complement(null_class))**. % 4.36/4.57 4847[1:SpR:4626.0,114.0] || -> equal(intersection(complement(null_class),union(u,null_class)),symmetric_difference(u,null_class))**. % 4.36/4.57 4871[1:SpL:4626.0,22.0] || member(u,null_class)* -> member(u,v)*. % 4.36/4.57 4892[1:MRR:3688.0,4871.1] || member(u,null_class)* -> . % 4.36/4.57 4928[1:Res:216.1,4892.0] || -> equal(intersection(null_class,u),null_class)**. % 4.36/4.57 4944[1:Rew:4928.0,3671.0] || -> equal(union(universal_class,u),complement(null_class))**. % 4.36/4.57 5040[1:SpR:4632.0,114.0] || -> equal(intersection(complement(intersection(u,universal_class)),complement(null_class)),symmetric_difference(u,universal_class))**. % 4.36/4.57 5081[1:SpR:4944.0,44.0] || -> equal(complement(null_class),successor(universal_class))**. % 4.36/4.57 5090[1:Rew:5081.0,4944.0] || -> equal(union(universal_class,u),successor(universal_class))**. % 4.36/4.57 5114[1:Rew:5081.0,4847.0] || -> equal(intersection(successor(universal_class),union(u,null_class)),symmetric_difference(u,null_class))**. % 4.36/4.57 5116[1:Rew:5081.0,5040.0] || -> equal(intersection(complement(intersection(u,universal_class)),successor(universal_class)),symmetric_difference(u,universal_class))**. % 4.36/4.57 5848[0:Res:217.1,4.0] || -> subclass(intersection(u,v),u)* subclass(intersection(u,v),u)*. % 4.36/4.57 5852[0:Obv:5848.0] || -> subclass(intersection(u,v),u)*. % 4.36/4.57 5870[0:SpR:114.0,5852.0] || -> subclass(symmetric_difference(u,v),complement(intersection(u,v)))*. % 4.36/4.57 6670[1:SpR:5090.0,5114.0] || -> equal(intersection(successor(universal_class),successor(universal_class)),symmetric_difference(universal_class,null_class))**. % 4.36/4.57 6698[1:SpR:6670.0,24.2] || member(u,successor(universal_class)) member(u,successor(universal_class)) -> member(u,symmetric_difference(universal_class,null_class))*. % 4.36/4.57 6718[1:Obv:6698.0] || member(u,successor(universal_class)) -> member(u,symmetric_difference(universal_class,null_class))*. % 4.36/4.57 7078[1:Res:6718.1,4.0] || member(not_subclass_element(u,symmetric_difference(universal_class,null_class)),successor(universal_class))* -> subclass(u,symmetric_difference(universal_class,null_class)). % 4.48/4.66 8223[1:SpR:764.1,5116.0] || -> equal(singleton(universal_class),null_class) equal(intersection(complement(null_class),successor(universal_class)),symmetric_difference(singleton(universal_class),universal_class))**. % 4.48/4.66 8241[1:Rew:6670.0,8223.1,5081.0,8223.1] || -> equal(singleton(universal_class),null_class) equal(symmetric_difference(singleton(universal_class),universal_class),symmetric_difference(universal_class,null_class))**. % 4.48/4.66 8276[0:Res:482.2,373.0] || subclass(u,universal_class) -> subclass(u,complement(v)) member(not_subclass_element(u,complement(v)),v)* subclass(u,complement(v)). % 4.48/4.66 8280[0:Obv:8276.1] || subclass(u,universal_class) -> member(not_subclass_element(u,complement(v)),v)* subclass(u,complement(v)). % 4.48/4.66 8281[0:MRR:8280.0,5.0] || -> member(not_subclass_element(u,complement(v)),v)* subclass(u,complement(v)). % 4.48/4.66 8389[1:Res:8281.0,4892.0] || -> subclass(u,complement(null_class))*. % 4.48/4.66 8395[1:Rew:5081.0,8389.0] || -> subclass(u,successor(universal_class))*. % 4.48/4.66 8458[1:Res:8395.0,438.0] || -> equal(successor(universal_class),universal_class)**. % 4.48/4.66 8473[1:Rew:8458.0,5081.0] || -> equal(complement(null_class),universal_class)**. % 4.48/4.66 8851[1:Rew:8458.0,7078.0] || member(not_subclass_element(u,symmetric_difference(universal_class,null_class)),universal_class)* -> subclass(u,symmetric_difference(universal_class,null_class)). % 4.48/4.66 10344[0:Res:5.0,1460.2] || member(u,v)* member(u,w)* -> member(u,universal_class)*. % 4.48/4.66 10354[0:Con:10344.1] || member(u,v)*+ -> member(u,universal_class)*. % 4.48/4.66 10414[0:Res:3.1,10354.0] || -> subclass(u,v) member(not_subclass_element(u,v),universal_class)*. % 4.48/4.66 10535[1:MRR:8851.0,10414.1] || -> subclass(u,symmetric_difference(universal_class,null_class))*. % 4.48/4.66 10715[1:Res:10535.0,438.0] || -> equal(symmetric_difference(universal_class,null_class),universal_class)**. % 4.48/4.66 10733[1:Rew:10715.0,8241.1] || -> equal(singleton(universal_class),null_class) equal(symmetric_difference(singleton(universal_class),universal_class),universal_class)**. % 4.48/4.66 11344[2:Spt:10733.0] || -> equal(singleton(universal_class),null_class)**. % 4.48/4.66 11346[2:Rew:11344.0,634.0] || equal(complement(null_class),universal_class)** -> . % 4.48/4.66 11349[2:Rew:8473.0,11346.0] || equal(universal_class,universal_class)* -> . % 4.48/4.66 11350[2:Obv:11349.0] || -> . % 4.48/4.66 11352[2:Spt:11350.0,10733.0,11344.0] || equal(singleton(universal_class),null_class)** -> . % 4.48/4.66 11353[2:Spt:11350.0,10733.1] || -> equal(symmetric_difference(singleton(universal_class),universal_class),universal_class)**. % 4.48/4.66 11355[2:SpR:11353.0,5870.0] || -> subclass(universal_class,complement(intersection(singleton(universal_class),universal_class)))*. % 4.48/4.66 11375[2:Res:11355.0,438.0] || -> equal(complement(intersection(singleton(universal_class),universal_class)),universal_class)**. % 4.48/4.66 11427[2:SpL:11375.0,25.1] || member(u,intersection(singleton(universal_class),universal_class))* member(u,universal_class) -> . % 4.48/4.66 11446[2:MRR:11427.1,23.1] || member(u,intersection(singleton(universal_class),universal_class))* -> . % 4.48/4.66 11523[2:Res:24.2,11446.0] || member(u,universal_class) member(u,singleton(universal_class))* -> . % 4.48/4.66 11567[2:MRR:11523.0,10354.1] || member(u,singleton(universal_class))* -> . % 4.48/4.66 11584[2:Res:71.2,11567.0] || member(singleton(universal_class),universal_class)* -> equal(singleton(universal_class),null_class). % 4.48/4.66 11611[2:MRR:11584.0,11584.1,129.0,11352.0] || -> . % 4.48/4.66 11612[1:Spt:11611.0,3402.1] || -> member(u,singleton(u))*. % 4.48/4.66 11613[0:MRR:3688.0,10354.1] || member(u,null_class)* -> . % 4.48/4.66 11828[0:MRR:2393.3,11613.0] || member(u,v) member(u,singleton(v))* -> equal(singleton(v),null_class). % 4.48/4.66 11880[1:Res:11612.0,10354.0] || -> member(u,universal_class)*. % 4.48/4.66 11881[1:Res:11612.0,2.0] || subclass(singleton(u),v)* -> member(u,v). % 4.48/4.66 11887[1:MRR:71.0,11880.0] || -> equal(u,null_class) member(apply(choice,u),u)*. % 4.48/4.66 12205[0:Res:482.2,11613.0] || subclass(u,null_class)*+ -> subclass(u,v)*. % 4.48/4.66 13171[0:Res:7.1,12205.0] || equal(null_class,u) -> subclass(u,v)*. % 4.48/4.66 13701[1:Res:13171.1,11881.0] || equal(singleton(u),null_class) -> member(u,v)*. % 4.48/4.66 13750[1:Res:13701.1,11613.0] || equal(singleton(u),null_class)** -> . % 4.48/4.66 13757[1:MRR:667.0,13750.0] || -> equal(apply(choice,singleton(u)),u)**. % 4.48/4.66 13761[1:MRR:11828.2,13750.0] || member(u,v) member(u,singleton(v))* -> . % 4.48/4.66 17822[1:Res:11887.1,13761.1] || member(apply(choice,singleton(u)),u)* -> equal(singleton(u),null_class). % 4.48/4.66 17845[1:Rew:13757.0,17822.0] || member(u,u)* -> equal(singleton(u),null_class). % 4.48/4.66 17846[1:MRR:17845.1,13750.0] || member(u,u)* -> . % 4.48/4.66 17847[1:UnC:17846.0,11880.0] || -> . % 4.48/4.66 % SZS output end Refutation % 4.48/4.66 Formulae used in the proof : prove_universal_class_not_set_1 subclass_members not_subclass_members1 not_subclass_members2 class_elements_are_sets equal_implies_subclass2 subclass_implies_equal unordered_pair_member unordered_pair3 unordered_pairs_in_universal singleton_set intersection1 intersection2 intersection3 complement1 complement2 union symmetric_difference successor regularity1 regularity2 choice2 % 4.48/4.66 %------------------------------------------------------------------------------