%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU307+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % 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 : 600s % DateTime : Tue Jul 19 14:36:07 EDT 2022 % Result : Theorem 95.25s 95.44s % Output : Refutation 95.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU307+2 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n029.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 08:39:30 EDT 2022 % 0.12/0.34 % CPUTime : % 95.25/95.44 % 95.25/95.44 SPASS V 3.9 % 95.25/95.44 SPASS beiseite: Proof found. % 95.25/95.44 % SZS status Theorem % 95.25/95.44 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 95.25/95.44 SPASS derived 22321 clauses, backtracked 1587 clauses, performed 61 splits and kept 13994 clauses. % 95.25/95.44 SPASS allocated 159931 KBytes. % 95.25/95.44 SPASS spent 0:1:34.39 on the problem. % 95.25/95.44 0:00:00.04 for the input. % 95.25/95.44 0:1:12.34 for the FLOTTER CNF translation. % 95.25/95.44 0:00:00.41 for inferences. % 95.25/95.44 0:00:00.11 for the backtracking. % 95.25/95.44 0:0:20.65 for the reduction. % 95.25/95.44 % 95.25/95.44 % 95.25/95.44 Here is a proof with depth 2, length 18 : % 95.25/95.44 % SZS output start Refutation % 95.25/95.44 1[0:Inp] || -> one_sorted_str(skc30)*. % 95.25/95.44 130[0:Inp] || -> equal(cast_to_subset(u),u)**. % 95.25/95.44 153[0:Inp] || -> element(skc31,powerset(the_carrier(skc30)))*. % 95.25/95.44 180[0:Inp] || -> element(cast_to_subset(u),powerset(u))*. % 95.25/95.44 390[0:Inp] one_sorted_str(u) || -> equal(cast_as_carrier_subset(u),the_carrier(u))**. % 95.25/95.44 395[0:Inp] || element(u,powerset(v))* -> subset(u,v). % 95.25/95.44 404[0:Inp] || equal(subset_intersection2(the_carrier(skc30),skc31,cast_as_carrier_subset(skc30)),skc31)** -> . % 95.25/95.44 466[0:Inp] || subset(u,v) -> equal(set_intersection2(u,v),u)**. % 95.25/95.44 894[0:Inp] || element(u,powerset(v)) element(w,powerset(v)) -> equal(subset_intersection2(v,w,u),set_intersection2(w,u))**. % 95.25/95.44 1182[0:Rew:130.0,180.0] || -> element(u,powerset(u))*. % 95.25/95.44 1307[0:Res:1.0,390.0] || -> equal(cast_as_carrier_subset(skc30),the_carrier(skc30))**. % 95.25/95.44 1360[0:Res:153.0,395.0] || -> subset(skc31,the_carrier(skc30))*r. % 95.25/95.44 1438[0:Rew:1307.0,404.0] || equal(subset_intersection2(the_carrier(skc30),skc31,the_carrier(skc30)),skc31)** -> . % 95.25/95.44 28958[0:SpL:894.2,1438.0] || element(the_carrier(skc30),powerset(the_carrier(skc30)))* element(skc31,powerset(the_carrier(skc30))) equal(set_intersection2(skc31,the_carrier(skc30)),skc31) -> . % 95.25/95.44 28960[0:MRR:28958.0,28958.1,1182.0,153.0] || equal(set_intersection2(skc31,the_carrier(skc30)),skc31)** -> . % 95.25/95.44 28962[0:SpL:466.1,28960.0] || subset(skc31,the_carrier(skc30))*r equal(skc31,skc31) -> . % 95.25/95.44 28967[0:Obv:28962.1] || subset(skc31,the_carrier(skc30))*r -> . % 95.25/95.44 28968[0:MRR:28967.0,1360.0] || -> . % 95.25/95.44 % SZS output end Refutation % 95.25/95.44 Formulae used in the proof : t15_pre_topc d4_subset_1 dt_k2_subset_1 t12_pre_topc t3_subset t28_xboole_1 redefinition_k5_subset_1 % 95.25/95.44 %------------------------------------------------------------------------------