%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : PRO009+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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 : Mon Jul 18 17:53:47 EDT 2022 % Result : Theorem 1.51s 1.71s % Output : Refutation 1.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : PRO009+3 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : run_spass %d %s % 0.11/0.33 % Computer : n011.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 Jun 13 01:41:33 EDT 2022 % 0.11/0.33 % CPUTime : % 1.51/1.71 % 1.51/1.71 SPASS V 3.9 % 1.51/1.71 SPASS beiseite: Proof found. % 1.51/1.71 % SZS status Theorem % 1.51/1.71 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.51/1.71 SPASS derived 4018 clauses, backtracked 462 clauses, performed 3 splits and kept 2584 clauses. % 1.51/1.71 SPASS allocated 101917 KBytes. % 1.51/1.71 SPASS spent 0:00:01.35 on the problem. % 1.51/1.71 0:00:00.03 for the input. % 1.51/1.71 0:00:00.12 for the FLOTTER CNF translation. % 1.51/1.71 0:00:00.06 for inferences. % 1.51/1.71 0:00:00.01 for the backtracking. % 1.51/1.71 0:00:01.08 for the reduction. % 1.51/1.71 % 1.51/1.71 % 1.51/1.71 Here is a proof with depth 5, length 43 : % 1.51/1.71 % SZS output start Refutation % 1.51/1.71 6[0:Inp] || -> occurrence_of(skc1,tptp0)*. % 1.51/1.71 10[0:Inp] || -> occurrence_of(skf37(u),tptp3)*. % 1.51/1.71 27[0:Inp] || precedes(u,v)* -> earlier(u,v). % 1.51/1.71 33[0:Inp] || earlier(u,v)*+ earlier(v,u)* -> . % 1.51/1.71 34[0:Inp] || min_precedes(u,v,w)* -> precedes(u,v). % 1.51/1.71 36[0:Inp] || -> occurrence_of(skf35(u),tptp1)* occurrence_of(skf35(u),tptp2). % 1.51/1.71 37[0:Inp] || occurrence_of(u,tptp0) -> root_occ(skf37(u),u)*. % 1.51/1.71 38[0:Inp] || occurrence_of(u,tptp0) -> leaf_occ(skf35(u),u)*. % 1.51/1.71 46[0:Inp] || next_subocc(u,v,w)* -> min_precedes(u,v,w). % 1.51/1.71 60[0:Inp] || occurrence_of(u,tptp0) -> next_subocc(skf37(u),skf36(u),tptp0)*. % 1.51/1.71 61[0:Inp] || occurrence_of(u,tptp0) -> next_subocc(skf36(u),skf35(u),tptp0)*. % 1.51/1.71 94[0:Inp] || root_occ(u,v)*+ leaf_occ(w,v)* occurrence_of(v,x)* -> equal(w,u) min_precedes(u,w,x)*. % 1.51/1.71 97[0:Inp] || leaf_occ(u,skc1) root_occ(v,skc1) occurrence_of(v,tptp3) occurrence_of(u,tptp1) min_precedes(v,u,tptp0)* -> . % 1.51/1.71 98[0:Inp] || leaf_occ(u,skc1) root_occ(v,skc1) occurrence_of(v,tptp3) occurrence_of(u,tptp2) min_precedes(v,u,tptp0)* -> . % 1.51/1.71 111[0:Res:6.0,94.0] || root_occ(u,skc1) leaf_occ(v,skc1) -> equal(v,u) min_precedes(u,v,tptp0)*. % 1.51/1.71 121[0:Res:6.0,60.0] || -> next_subocc(skf37(skc1),skf36(skc1),tptp0)*. % 1.51/1.71 122[0:Res:6.0,61.0] || -> next_subocc(skf36(skc1),skf35(skc1),tptp0)*. % 1.51/1.71 123[0:Res:6.0,37.0] || -> root_occ(skf37(skc1),skc1)*. % 1.51/1.71 124[0:Res:6.0,38.0] || -> leaf_occ(skf35(skc1),skc1)*. % 1.51/1.71 153[0:Res:123.0,98.2] || occurrence_of(u,tptp2) occurrence_of(skf37(skc1),tptp3) min_precedes(skf37(skc1),u,tptp0)* leaf_occ(u,skc1) -> . % 1.51/1.71 155[0:Res:123.0,97.2] || occurrence_of(u,tptp1) occurrence_of(skf37(skc1),tptp3) min_precedes(skf37(skc1),u,tptp0)* leaf_occ(u,skc1) -> . % 1.51/1.71 157[0:MRR:153.1,10.0] || leaf_occ(u,skc1) occurrence_of(u,tptp2) min_precedes(skf37(skc1),u,tptp0)* -> . % 1.51/1.71 158[0:MRR:155.1,10.0] || leaf_occ(u,skc1) occurrence_of(u,tptp1) min_precedes(skf37(skc1),u,tptp0)* -> . % 1.51/1.71 258[0:Res:122.0,46.0] || -> min_precedes(skf36(skc1),skf35(skc1),tptp0)*. % 1.51/1.71 259[0:Res:121.0,46.0] || -> min_precedes(skf37(skc1),skf36(skc1),tptp0)*. % 1.51/1.71 263[0:Res:258.0,34.0] || -> precedes(skf36(skc1),skf35(skc1))*. % 1.51/1.71 274[0:Res:259.0,34.0] || -> precedes(skf37(skc1),skf36(skc1))*. % 1.51/1.71 450[0:Res:263.0,27.0] || -> earlier(skf36(skc1),skf35(skc1))*l. % 1.51/1.71 453[0:Res:274.0,27.0] || -> earlier(skf37(skc1),skf36(skc1))*l. % 1.51/1.71 983[0:Res:453.0,33.0] || earlier(skf36(skc1),skf37(skc1))*r -> . % 1.51/1.71 1058[0:Res:37.1,94.0] || occurrence_of(u,tptp0) leaf_occ(v,u) occurrence_of(u,w) -> equal(v,skf37(u)) min_precedes(skf37(u),v,w)*. % 1.51/1.71 2244[0:Res:111.3,157.2] || root_occ(skf37(skc1),skc1)* leaf_occ(u,skc1)* leaf_occ(u,skc1)* occurrence_of(u,tptp2) -> equal(u,skf37(skc1)). % 1.51/1.71 2249[0:Obv:2244.1] || root_occ(skf37(skc1),skc1)* leaf_occ(u,skc1)* occurrence_of(u,tptp2) -> equal(u,skf37(skc1)). % 1.51/1.71 2250[0:MRR:2249.0,123.0] || leaf_occ(u,skc1)* occurrence_of(u,tptp2) -> equal(u,skf37(skc1)). % 1.51/1.71 2253[0:Res:124.0,2250.0] || occurrence_of(skf35(skc1),tptp2)* -> equal(skf37(skc1),skf35(skc1)). % 1.51/1.71 3957[0:Res:1058.4,158.2] || occurrence_of(skc1,tptp0) leaf_occ(u,skc1)* occurrence_of(skc1,tptp0) leaf_occ(u,skc1)* occurrence_of(u,tptp1) -> equal(u,skf37(skc1)). % 1.51/1.71 3961[0:Obv:3957.1] || occurrence_of(skc1,tptp0) leaf_occ(u,skc1)* occurrence_of(u,tptp1) -> equal(u,skf37(skc1)). % 1.51/1.71 3962[0:MRR:3961.0,6.0] || leaf_occ(u,skc1)* occurrence_of(u,tptp1) -> equal(u,skf37(skc1)). % 1.51/1.71 3967[0:Res:124.0,3962.0] || occurrence_of(skf35(skc1),tptp1)* -> equal(skf37(skc1),skf35(skc1)). % 1.51/1.71 4594[0:Res:36.0,3967.0] || -> occurrence_of(skf35(skc1),tptp2)* equal(skf37(skc1),skf35(skc1)). % 1.51/1.71 4595[0:MRR:4594.0,2253.0] || -> equal(skf37(skc1),skf35(skc1))**. % 1.51/1.71 4704[0:Rew:4595.0,983.0] || earlier(skf36(skc1),skf35(skc1))*l -> . % 1.51/1.71 4808[0:MRR:4704.0,450.0] || -> . % 1.51/1.71 % SZS output end Refutation % 1.51/1.71 Formulae used in the proof : goals sos_49 sos_10 sos_04 sos_15 sos_22 sos_41 % 1.51/1.71 %------------------------------------------------------------------------------