%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL050-10 : TPTP v9.3.1. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:06:39 PM UTC 2026 % Result : Timeout 287.34s 287.60s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL050-10 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.04 % Command : run_spass %d %s % 0.10/0.36 % Computer : n020.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Sat Sep 5 17:29:27 UTC 2026 % 0.10/0.36 % CPUTime : % 287.34/287.60 % 287.34/287.60 SPASS V 3.9 % 287.34/287.60 SPASS beiseite: Proof found. % 287.34/287.60 % SZS status Theorem % 287.34/287.60 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 287.34/287.60 SPASS derived 81856 clauses, backtracked 0 clauses, performed 0 splits and kept 7518 clauses. % 287.34/287.60 SPASS allocated 181732 KBytes. % 287.34/287.60 SPASS spent 0:4:47.08 on the problem. % 287.34/287.60 0:00:00.06 for the input. % 287.34/287.60 0:00:00.00 for the FLOTTER CNF translation. % 287.34/287.60 0:00:01.97 for inferences. % 287.34/287.60 0:00:00.00 for the backtracking. % 287.34/287.60 0:4:44.84 for the reduction. % 287.34/287.60 % 287.34/287.60 % 287.34/287.60 Here is a proof with depth 28, length 89 : % 287.34/287.60 % SZS output start Refutation % 287.34/287.60 1[0:Inp] || -> equal(ifeq(u,u,v,w),v)**. % 287.34/287.60 2[0:Inp] || -> equal(ifeq(is_a_theorem(implies__dfg(u,v)),true__dfg,ifeq(is_a_theorem(u),true__dfg,is_a_theorem(v),true__dfg),true__dfg),true__dfg)**. % 287.34/287.60 3[0:Inp] || -> equal(is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(v,w),implies__dfg(u,w)))),true__dfg)**. % 287.34/287.60 4[0:Inp] || -> equal(is_a_theorem(implies__dfg(implies__dfg(not__dfg(u),u),u)),true__dfg)**. % 287.34/287.60 5[0:Inp] || -> equal(is_a_theorem(implies__dfg(u,implies__dfg(not__dfg(u),v))),true__dfg)**. % 287.34/287.60 6[0:Inp] || equal(is_a_theorem(implies__dfg(implies__dfg(a,implies__dfg(b,c)),implies__dfg(b,implies__dfg(a,c)))),true__dfg)** -> . % 287.34/287.60 15[0:SpR:4.0,2.0] || -> equal(ifeq(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(not__dfg(u),u),u),v)),true__dfg,ifeq(true__dfg,true__dfg,is_a_theorem(v),true__dfg),true__dfg),true__dfg)**. % 287.34/287.60 16[0:SpR:5.0,2.0] || -> equal(ifeq(is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(not__dfg(u),v)),w)),true__dfg,ifeq(true__dfg,true__dfg,is_a_theorem(w),true__dfg),true__dfg),true__dfg)**. % 287.34/287.60 19[0:SpR:5.0,2.0] || -> equal(ifeq(true__dfg,true__dfg,ifeq(is_a_theorem(u),true__dfg,is_a_theorem(implies__dfg(not__dfg(u),v)),true__dfg),true__dfg),true__dfg)**. % 287.34/287.60 20[0:SpR:3.0,2.0] || -> equal(ifeq(true__dfg,true__dfg,ifeq(is_a_theorem(implies__dfg(u,v)),true__dfg,is_a_theorem(implies__dfg(implies__dfg(v,w),implies__dfg(u,w))),true__dfg),true__dfg),true__dfg)**. % 287.34/287.60 22[0:Rew:1.0,19.0] || -> equal(ifeq(is_a_theorem(u),true__dfg,is_a_theorem(implies__dfg(not__dfg(u),v)),true__dfg),true__dfg)**. % 287.34/287.60 23[0:Rew:1.0,16.0] || -> equal(ifeq(is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(not__dfg(u),v)),w)),true__dfg,is_a_theorem(w),true__dfg),true__dfg)**. % 287.34/287.60 24[0:Rew:1.0,15.0] || -> equal(ifeq(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(not__dfg(u),u),u),v)),true__dfg,is_a_theorem(v),true__dfg),true__dfg)**. % 287.34/287.60 25[0:Rew:1.0,20.0] || -> equal(ifeq(is_a_theorem(implies__dfg(u,v)),true__dfg,is_a_theorem(implies__dfg(implies__dfg(v,w),implies__dfg(u,w))),true__dfg),true__dfg)**. % 287.34/287.60 55[0:SpR:3.0,23.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(implies__dfg(implies__dfg(not__dfg(u),v),w),implies__dfg(u,w))),true__dfg),true__dfg)**. % 287.34/287.60 57[0:Rew:1.0,55.0] || -> equal(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(not__dfg(u),v),w),implies__dfg(u,w))),true__dfg)**. % 287.34/287.60 91[0:SpR:57.0,2.0] || -> equal(ifeq(true__dfg,true__dfg,ifeq(is_a_theorem(implies__dfg(implies__dfg(not__dfg(u),v),w)),true__dfg,is_a_theorem(implies__dfg(u,w)),true__dfg),true__dfg),true__dfg)**. % 287.34/287.60 94[0:SpR:57.0,2.0] || -> equal(ifeq(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(implies__dfg(not__dfg(u),v),w),implies__dfg(u,w)),x)),true__dfg,ifeq(true__dfg,true__dfg,is_a_theorem(x),true__dfg),true__dfg),true__dfg)**. % 287.34/287.60 101[0:Rew:1.0,91.0] || -> equal(ifeq(is_a_theorem(implies__dfg(implies__dfg(not__dfg(u),v),w)),true__dfg,is_a_theorem(implies__dfg(u,w)),true__dfg),true__dfg)**. % 287.34/287.60 102[0:Rew:1.0,94.0] || -> equal(ifeq(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(implies__dfg(not__dfg(u),v),w),implies__dfg(u,w)),x)),true__dfg,is_a_theorem(x),true__dfg),true__dfg)**. % 287.34/287.60 132[0:SpR:3.0,24.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(not__dfg(u),u),v))),true__dfg),true__dfg)**. % 287.34/287.60 133[0:SpR:57.0,24.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(u,u)),true__dfg),true__dfg)**. % 287.34/287.60 134[0:Rew:1.0,133.0] || -> equal(is_a_theorem(implies__dfg(u,u)),true__dfg)**. % 287.34/287.60 136[0:Rew:1.0,132.0] || -> equal(is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(not__dfg(u),u),v))),true__dfg)**. % 287.34/287.60 149[0:SpR:134.0,22.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(not__dfg(implies__dfg(u,u)),v)),true__dfg),true__dfg)**. % 287.34/287.60 155[0:Rew:1.0,149.0] || -> equal(is_a_theorem(implies__dfg(not__dfg(implies__dfg(u,u)),v)),true__dfg)**. % 287.34/287.60 220[0:SpR:3.0,25.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(implies__dfg(implies__dfg(implies__dfg(u,v),implies__dfg(w,v)),x),implies__dfg(implies__dfg(w,u),x))),true__dfg),true__dfg)**. % 287.34/287.60 221[0:SpR:57.0,25.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,v),w),implies__dfg(implies__dfg(implies__dfg(not__dfg(u),x),v),w))),true__dfg),true__dfg)**. % 287.34/287.60 223[0:SpR:155.0,25.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(not__dfg(implies__dfg(w,w)),v))),true__dfg),true__dfg)**. % 287.34/287.60 228[0:Rew:1.0,223.0] || -> equal(is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(not__dfg(implies__dfg(w,w)),v))),true__dfg)**. % 287.34/287.60 232[0:Rew:1.0,221.0] || -> equal(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,v),w),implies__dfg(implies__dfg(implies__dfg(not__dfg(u),x),v),w))),true__dfg)**. % 287.34/287.60 233[0:Rew:1.0,220.0] || -> equal(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(implies__dfg(u,v),implies__dfg(w,v)),x),implies__dfg(implies__dfg(w,u),x))),true__dfg)**. % 287.34/287.60 284[0:SpR:136.0,25.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(implies__dfg(implies__dfg(implies__dfg(not__dfg(u),u),v),w),implies__dfg(implies__dfg(u,v),w))),true__dfg),true__dfg)**. % 287.34/287.60 303[0:Rew:1.0,284.0] || -> equal(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(implies__dfg(not__dfg(u),u),v),w),implies__dfg(implies__dfg(u,v),w))),true__dfg)**. % 287.34/287.60 606[0:SpR:233.0,2.0] || -> equal(ifeq(true__dfg,true__dfg,ifeq(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,v),implies__dfg(w,v)),x)),true__dfg,is_a_theorem(implies__dfg(implies__dfg(w,u),x)),true__dfg),true__dfg),true__dfg)**. % 287.34/287.60 630[0:Rew:1.0,606.0] || -> equal(ifeq(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,v),implies__dfg(w,v)),x)),true__dfg,is_a_theorem(implies__dfg(implies__dfg(w,u),x)),true__dfg),true__dfg)**. % 287.34/287.60 806[0:SpR:228.0,101.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(u,implies__dfg(not__dfg(implies__dfg(v,v)),w))),true__dfg),true__dfg)**. % 287.34/287.60 811[0:Rew:1.0,806.0] || -> equal(is_a_theorem(implies__dfg(u,implies__dfg(not__dfg(implies__dfg(v,v)),w))),true__dfg)**. % 287.34/287.60 829[0:SpR:811.0,25.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(implies__dfg(implies__dfg(not__dfg(implies__dfg(u,u)),v),w),implies__dfg(x,w))),true__dfg),true__dfg)**. % 287.34/287.60 872[0:Rew:1.0,829.0] || -> equal(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(not__dfg(implies__dfg(u,u)),v),w),implies__dfg(x,w))),true__dfg)**. % 287.34/287.60 1215[0:SpR:872.0,24.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(u,implies__dfg(v,v))),true__dfg),true__dfg)**. % 287.34/287.60 1235[0:Rew:1.0,1215.0] || -> equal(is_a_theorem(implies__dfg(u,implies__dfg(v,v))),true__dfg)**. % 287.34/287.60 1308[0:SpR:1235.0,25.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,u),v),implies__dfg(w,v))),true__dfg),true__dfg)**. % 287.34/287.60 1358[0:Rew:1.0,1308.0] || -> equal(is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,u),v),implies__dfg(w,v))),true__dfg)**. % 287.34/287.60 1430[0:SpR:1358.0,2.0] || -> equal(ifeq(true__dfg,true__dfg,ifeq(is_a_theorem(implies__dfg(implies__dfg(u,u),v)),true__dfg,is_a_theorem(implies__dfg(w,v)),true__dfg),true__dfg),true__dfg)**. % 287.34/287.60 1455[0:Rew:1.0,1430.0] || -> equal(ifeq(is_a_theorem(implies__dfg(implies__dfg(u,u),v)),true__dfg,is_a_theorem(implies__dfg(w,v)),true__dfg),true__dfg)**. % 287.34/287.60 2018[0:SpR:136.0,1455.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(u,implies__dfg(implies__dfg(not__dfg(v),v),v))),true__dfg),true__dfg)**. % 287.34/287.60 2027[0:Rew:1.0,2018.0] || -> equal(is_a_theorem(implies__dfg(u,implies__dfg(implies__dfg(not__dfg(v),v),v))),true__dfg)**. % 287.34/287.60 2281[0:SpR:2027.0,25.0] || -> equal(ifeq(true__dfg,true__dfg,is_a_theorem(implies__dfg(implies__dTerminated %------------------------------------------------------------------------------