%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL501+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n001.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:07:39 PM UTC 2026 % Result : Timeout 291.56s 291.86s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL501+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.04 % Command : run_spass %d %s % 0.11/0.37 % Computer : n001.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Fri Sep 4 23:24:00 UTC 2026 % 0.11/0.37 % CPUTime : % 291.56/291.86 % 291.56/291.86 SPASS V 3.9 % 291.56/291.86 SPASS beiseite: Proof found. % 291.56/291.86 % SZS status Theorem % 291.56/291.86 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 291.56/291.86 SPASS derived 71367 clauses, backtracked 0 clauses, performed 0 splits and kept 18634 clauses. % 291.56/291.86 SPASS allocated 226997 KBytes. % 291.56/291.86 SPASS spent 0:4:51.21 on the problem. % 291.56/291.86 0:00:00.06 for the input. % 291.56/291.86 0:00:00.06 for the FLOTTER CNF translation. % 291.56/291.86 0:00:01.52 for inferences. % 291.56/291.86 0:00:00.00 for the backtracking. % 291.56/291.86 0:4:49.04 for the reduction. % 291.56/291.86 % 291.56/291.86 % 291.56/291.86 Here is a proof with depth 22, length 302 : % 291.56/291.86 % SZS output start Refutation % 291.56/291.86 1[0:Inp] || -> op_or*. % 291.56/291.86 2[0:Inp] || -> op_implies_and*. % 291.56/291.86 4[0:Inp] || -> op_implies_or*. % 291.56/291.86 5[0:Inp] || -> op_and*. % 291.56/291.86 6[0:Inp] || -> op_equiv*. % 291.56/291.86 7[0:Inp] || -> modus_ponens*. % 291.56/291.86 8[0:Inp] || -> r1*. % 291.56/291.86 9[0:Inp] || -> r2*. % 291.56/291.86 10[0:Inp] || -> r3*. % 291.56/291.86 11[0:Inp] || -> r4*. % 291.56/291.86 12[0:Inp] || -> r5*. % 291.56/291.86 13[0:Inp] || -> substitution_of_equivalents*. % 291.56/291.86 14[0:Inp] || kn3* -> . % 291.56/291.86 15[0:Inp] || -> is_a_theorem(skc56)*. % 291.56/291.86 16[0:Inp] || -> is_a_theorem(implies__dfg(skc56,skc55))*. % 291.56/291.86 30[0:Inp] || kn1 -> is_a_theorem(implies__dfg(u,and__dfg(u,u)))*. % 291.56/291.86 31[0:Inp] || is_a_theorem(implies__dfg(skc87,and__dfg(skc87,skc87)))* -> kn1. % 291.56/291.86 34[0:Inp] || r1 -> is_a_theorem(implies__dfg(or__dfg(u,u),u))*. % 291.56/291.86 36[0:Inp] || r2 -> is_a_theorem(implies__dfg(u,or__dfg(v,u)))*. % 291.56/291.86 42[0:Inp] || substitution_of_equivalents is_a_theorem(equiv__dfg(u,v))* -> equal(u,v). % 291.56/291.86 43[0:Inp] || and_3 -> is_a_theorem(implies__dfg(u,implies__dfg(v,and__dfg(u,v))))*. % 291.56/291.86 44[0:Inp] || is_a_theorem(implies__dfg(skc73,implies__dfg(skc72,and__dfg(skc73,skc72))))* -> and_3. % 291.56/291.86 49[0:Inp] || r3 -> is_a_theorem(implies__dfg(or__dfg(u,v),or__dfg(v,u)))*. % 291.56/291.86 51[0:Inp] || op_implies_or -> equal(or__dfg(not__dfg(u),v),implies__dfg(u,v))**. % 291.56/291.86 52[0:Inp] || op_implies_and -> equal(not__dfg(and__dfg(u,not__dfg(v))),implies__dfg(u,v))**. % 291.56/291.86 53[0:Inp] is_a_theorem(u) || modus_ponens is_a_theorem(implies__dfg(u,v))* -> is_a_theorem(v). % 291.56/291.86 58[0:Inp] || op_or -> equal(not__dfg(and__dfg(not__dfg(u),not__dfg(v))),or__dfg(u,v))**. % 291.56/291.86 59[0:Inp] || op_and -> equal(not__dfg(or__dfg(not__dfg(u),not__dfg(v))),and__dfg(u,v))**. % 291.56/291.86 60[0:Inp] || op_equiv -> equal(and__dfg(implies__dfg(u,v),implies__dfg(v,u)),equiv__dfg(u,v))**. % 291.56/291.86 63[0:Inp] || equivalence_3 -> is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(v,u),equiv__dfg(u,v))))*. % 291.56/291.86 64[0:Inp] || is_a_theorem(implies__dfg(implies__dfg(skc86,skc85),implies__dfg(implies__dfg(skc85,skc86),equiv__dfg(skc86,skc85))))* -> equivalence_3. % 291.56/291.86 67[0:Inp] || r4 -> is_a_theorem(implies__dfg(or__dfg(u,or__dfg(v,w)),or__dfg(v,or__dfg(u,w))))*. % 291.56/291.86 69[0:Inp] || r5 -> is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(or__dfg(w,u),or__dfg(w,v))))*. % 291.56/291.86 74[0:Inp] || is_a_theorem(implies__dfg(implies__dfg(skc92,skc91),implies__dfg(not__dfg(and__dfg(skc91,skc90)),not__dfg(and__dfg(skc90,skc92)))))* -> kn3. % 291.56/291.86 75[0:MRR:36.0,9.0] || -> is_a_theorem(implies__dfg(u,or__dfg(v,u)))*. % 291.56/291.86 76[0:MRR:34.0,8.0] || -> is_a_theorem(implies__dfg(or__dfg(u,u),u))*. % 291.56/291.86 78[0:MRR:51.0,4.0] || -> equal(or__dfg(not__dfg(u),v),implies__dfg(u,v))**. % 291.56/291.86 79[0:MRR:49.0,10.0] || -> is_a_theorem(implies__dfg(or__dfg(u,v),or__dfg(v,u)))*. % 291.56/291.86 80[0:MRR:42.0,13.0] || is_a_theorem(equiv__dfg(u,v))* -> equal(u,v). % 291.56/291.86 81[0:MRR:52.0,2.0] || -> equal(not__dfg(and__dfg(u,not__dfg(v))),implies__dfg(u,v))**. % 291.56/291.86 82[0:Rew:78.0,59.1] || op_and -> equal(not__dfg(implies__dfg(u,not__dfg(v))),and__dfg(u,v))**. % 291.56/291.86 83[0:MRR:82.0,5.0] || -> equal(not__dfg(implies__dfg(u,not__dfg(v))),and__dfg(u,v))**. % 291.56/291.86 84[0:Rew:81.0,58.1] || op_or -> equal(implies__dfg(not__dfg(u),v),or__dfg(u,v))**. % 291.56/291.86 85[0:MRR:84.0,1.0] || -> equal(implies__dfg(not__dfg(u),v),or__dfg(u,v))**. % 291.56/291.86 93[0:MRR:53.1,7.0] is_a_theorem(u) || is_a_theorem(implies__dfg(u,v))* -> is_a_theorem(v). % 291.56/291.86 94[0:MRR:60.0,6.0] || -> equal(and__dfg(implies__dfg(u,v),implies__dfg(v,u)),equiv__dfg(u,v))**. % 291.56/291.86 95[0:MRR:69.0,12.0] || -> is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(or__dfg(w,u),or__dfg(w,v))))*. % 291.56/291.86 96[0:MRR:67.0,11.0] || -> is_a_theorem(implies__dfg(or__dfg(u,or__dfg(v,w)),or__dfg(v,or__dfg(u,w))))*. % 291.56/291.86 97[0:Rew:85.0,74.0] || is_a_theorem(implies__dfg(implies__dfg(skc92,skc91),or__dfg(and__dfg(skc91,skc90),not__dfg(and__dfg(skc90,skc92)))))* -> kn3. % 291.56/291.86 98[0:MRR:97.1,14.0] || is_a_theorem(implies__dfg(implies__dfg(skc92,skc91),or__dfg(and__dfg(skc91,skc90),not__dfg(and__dfg(skc90,skc92)))))* -> . % 291.56/291.86 113[0:SpR:78.0,76.0] || -> is_a_theorem(implies__dfg(implies__dfg(u,not__dfg(u)),not__dfg(u)))*. % 291.56/291.86 114[0:SpR:78.0,75.0] || -> is_a_theorem(implies__dfg(u,implies__dfg(v,u)))*. % 291.56/291.86 121[0:SpR:85.0,75.0] || -> is_a_theorem(or__dfg(u,or__dfg(v,not__dfg(u))))*. % 291.56/291.86 129[0:SpR:85.0,114.0] || -> is_a_theorem(or__dfg(u,implies__dfg(v,not__dfg(u))))*. % 291.56/291.86 135[0:SpR:78.0,79.0] || -> is_a_theorem(implies__dfg(or__dfg(u,not__dfg(v)),implies__dfg(v,u)))*. % 291.56/291.86 136[0:SpR:78.0,79.0] || -> is_a_theorem(implies__dfg(implies__dfg(u,v),or__dfg(v,not__dfg(u))))*. % 291.56/291.86 154[0:SpR:81.0,78.0] || -> equal(implies__dfg(and__dfg(u,not__dfg(v)),w),or__dfg(implies__dfg(u,v),w))**. % 291.56/291.86 155[0:SpR:81.0,85.0] || -> equal(or__dfg(and__dfg(u,not__dfg(v)),w),implies__dfg(implies__dfg(u,v),w))**. % 291.56/291.86 163[0:SpR:81.0,81.0] || -> equal(not__dfg(and__dfg(u,implies__dfg(v,w))),implies__dfg(u,and__dfg(v,not__dfg(w))))**. % 291.56/291.86 172[0:SpR:83.0,78.0] || -> equal(implies__dfg(implies__dfg(u,not__dfg(v)),w),or__dfg(and__dfg(u,v),w))**. % 291.56/291.86 173[0:SpR:83.0,85.0] || -> equal(or__dfg(implies__dfg(u,not__dfg(v)),w),implies__dfg(and__dfg(u,v),w))**. % 291.56/291.86 182[0:SpR:83.0,83.0] || -> equal(not__dfg(implies__dfg(u,and__dfg(v,w))),and__dfg(u,implies__dfg(v,not__dfg(w))))**. % 291.56/291.86 185[0:SpR:85.0,83.0] || -> equal(not__dfg(or__dfg(u,not__dfg(v))),and__dfg(not__dfg(u),v))**. % 291.56/291.86 186[0:Rew:172.0,113.0] || -> is_a_theorem(or__dfg(and__dfg(u,u),not__dfg(u)))*. % 291.56/291.86 199[0:SpR:78.0,135.0] || -> is_a_theorem(implies__dfg(implies__dfg(u,not__dfg(v)),implies__dfg(v,not__dfg(u))))*. % 291.56/291.86 200[0:Rew:172.0,199.0] || -> is_a_theorem(or__dfg(and__dfg(u,v),implies__dfg(v,not__dfg(u))))*. % 291.56/291.86 251[0:SpR:85.0,43.1] || and_3 -> is_a_theorem(implies__dfg(u,or__dfg(v,and__dfg(u,not__dfg(v)))))*. % 291.56/291.86 254[0:SpL:85.0,93.1] is_a_theorem(not__dfg(u)) || is_a_theorem(or__dfg(u,v))* -> is_a_theorem(v). % 291.56/291.86 255[0:Res:16.0,93.1] is_a_theorem(skc56) || -> is_a_theorem(skc55)*. % 291.56/291.86 258[0:Res:75.0,93.1] is_a_theorem(u) || -> is_a_theorem(or__dfg(v,u))*. % 291.56/291.86 262[0:Res:79.0,93.1] is_a_theorem(or__dfg(u,v)) || -> is_a_theorem(or__dfg(v,u))*. % 291.56/291.86 263[0:Res:136.0,93.1] is_a_theorem(implies__dfg(u,v)) || -> is_a_theorem(or__dfg(v,not__dfg(u)))*. % 291.56/291.86 269[0:Res:114.0,93.1] is_a_theorem(u) || -> is_a_theorem(implies__dfg(v,u))*. % 291.56/291.86 273[0:Res:135.0,93.1] is_a_theorem(or__dfg(u,not__dfg(v))) || -> is_a_theorem(implies__dfg(v,u))*. % 291.56/291.86 276[0:SSi:255.0,15.0] || -> is_a_theorem(skc55)*. % 291.56/291.86 279[0:SpR:94.0,30.1] || kn1 -> is_a_theorem(implies__dfg(implies__dfg(u,u),equiv__dfg(u,u)))*. % 291.56/291.86 286[0:SpR:94.0,43.1] || and_3 -> is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(v,u),equiv__dfg(u,v))))*. % 291.56/291.86 289[0:SpR:85.0,94.0] || -> equal(and__dfg(or__dfg(u,v),implies__dfg(v,not__dfg(u))),equiv__dfg(not__dfg(u),v))**. % 291.56/291.86 314[0:SpR:78.0,96.0] || -> is_a_theorem(implies__dfg(or__dfg(not__dfg(u),or__dfg(v,w)),or__dfg(v,implies__dfg(u,w))))*. % 291.56/291.86 315[0:SpR:78.0,96.0] || -> is_a_theorem(implies__dfg(or__dfg(u,or__dfg(not__dfg(v),w)),implies__dfg(v,or__dfg(u,w))))*. % 291.56/291.86 318[0:Res:96.0,93.1] is_a_theorem(or__dfg(u,or__dfg(v,w))) || -> is_a_theorem(or__dfg(v,or__dfg(u,w)))*. % 291.56/291.86 319[0:Rew:78.0,314.0] || -> is_a_theorem(implies__dfg(implies__dfg(u,or__dfg(v,w)),or__dfg(v,implies__dfg(u,w))))*. % 291.56/291.86 320[0:Rew:78.0,315.0] || -> is_a_theorem(implies__dfg(or__dfg(u,implies__dfg(v,w)),implies__dfg(v,or__dfg(u,w))))*. % 291.56/291.86 327[0:SpR:85.0,95.0] || -> is_a_theorem(implies__dfg(or__dfg(u,v),implies__dfg(or__dfg(w,not__dfg(u)),or__dfg(w,v))))*. % 291.56/291.86 328[0:Res:95.0,93.1] is_a_theorem(implies__dfg(u,v)) || -> is_a_theorem(implies__dfg(or__dfg(w,u),or__dfg(w,v)))*. % 291.56/291.86 359[0:SoR:262.0,200.0] || -> is_a_theorem(or__dfg(implies__dfg(u,not__dfg(v)),and__dfg(v,u)))*. % 291.56/291.86 361[0:SoR:262.0,186.0] || -> is_a_theorem(or__dfg(not__dfg(u),and__dfg(u,u)))*. % 291.56/291.86 368[0:SoR:262.0,129.0] || -> is_a_theorem(or__dfg(implies__dfg(u,not__dfg(v)),v))*. % 291.56/291.86 371[0:Rew:78.0,361.0] || -> is_a_theorem(implies__dfg(u,and__dfg(u,u)))*. % 291.56/291.86 372[0:MRR:31.0,371.0] || -> kn1*. % 291.56/291.86 376[0:MRR:279.0,372.0] || -> is_a_theorem(implies__dfg(implies__dfg(u,u),equiv__dfg(u,u)))*. % 291.56/291.86 378[0:Rew:173.0,368.0] || -> is_a_theorem(implies__dfg(and__dfg(u,v),v))*. % 291.56/291.86 386[0:Rew:173.0,359.0] || -> is_a_theorem(implies__dfg(and__dfg(u,v),and__dfg(v,u)))*. % 291.56/291.86 431[0:Res:63.1,93.1] is_a_theorem(implies__dfg(u,v)) || equivalence_3 -> is_a_theorem(implies__dfg(implies__dfg(v,u),equiv__dfg(u,v)))*. % 291.56/291.86 527[0:SpR:185.0,85.0] || -> equal(or__dfg(or__dfg(u,not__dfg(v)),w),implies__dfg(and__dfg(not__dfg(u),v),w))**. % 291.56/291.86 555[0:SpR:81.0,185.0] || -> equal(and__dfg(not__dfg(u),and__dfg(v,not__dfg(w))),not__dfg(or__dfg(u,implies__dfg(v,w))))**. % 291.56/291.86 557[0:SpR:78.0,185.0] || -> equal(not__dfg(implies__dfg(u,not__dfg(v))),and__dfg(not__dfg(not__dfg(u)),v))**. % 291.56/291.86 558[0:Rew:83.0,557.0] || -> equal(and__dfg(not__dfg(not__dfg(u)),v),and__dfg(u,v))**. % 291.56/291.86 1042[0:SpR:155.0,79.0] || -> is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,v),w),or__dfg(w,and__dfg(u,not__dfg(v)))))*. % 291.56/291.86 1059[0:SpR:155.0,186.0] || -> is_a_theorem(implies__dfg(implies__dfg(not__dfg(u),u),not__dfg(not__dfg(u))))*. % 291.56/291.86 1094[0:Rew:85.0,1059.0] || -> is_a_theorem(implies__dfg(or__dfg(u,u),not__dfg(not__dfg(u))))*. % 291.56/291.86 1158[0:Res:1094.0,93.1] is_a_theorem(or__dfg(u,u)) || -> is_a_theorem(not__dfg(not__dfg(u)))*. % 291.56/291.86 1492[0:SpR:78.0,319.0] || -> is_a_theorem(implies__dfg(implies__dfg(u,or__dfg(not__dfg(v),w)),implies__dfg(v,implies__dfg(u,w))))*. % 291.56/291.86 1501[0:Res:319.0,93.1] is_a_theorem(implies__dfg(u,or__dfg(v,w))) || -> is_a_theorem(or__dfg(v,implies__dfg(u,w)))*. % 291.56/291.86 1503[0:Rew:78.0,1492.0] || -> is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(v,w)),implies__dfg(v,implies__dfg(u,w))))*. % 291.56/291.86 1551[0:Res:320.0,93.1] is_a_theorem(or__dfg(u,implies__dfg(v,w))) || -> is_a_theorem(implies__dfg(v,or__dfg(u,w)))*. % 291.56/291.86 1761[0:SpR:94.0,163.0] || -> equal(implies__dfg(implies__dfg(u,v),and__dfg(v,not__dfg(u))),not__dfg(equiv__dfg(u,v)))**. % 291.56/291.86 2696[0:SpR:78.0,289.0] || -> equal(and__dfg(implies__dfg(u,v),implies__dfg(v,not__dfg(not__dfg(u)))),equiv__dfg(not__dfg(not__dfg(u)),v))**. % 291.56/291.86 2777[0:SoR:318.0,258.1] is_a_theorem(or__dfg(u,v)) || -> is_a_theorem(or__dfg(u,or__dfg(w,v)))*. % 291.56/291.86 2780[0:SoR:318.0,121.0] || -> is_a_theorem(or__dfg(u,or__dfg(v,not__dfg(v))))*. % 291.56/291.86 2787[0:SoR:262.0,2780.0] || -> is_a_theorem(or__dfg(or__dfg(u,not__dfg(u)),v))*. % 291.56/291.86 2802[0:Rew:527.0,2787.0] || -> is_a_theorem(implies__dfg(and__dfg(not__dfg(u),u),v))*. % 291.56/291.86 2941[0:SoR:328.0,376.0] || -> is_a_theorem(implies__dfg(or__dfg(u,implies__dfg(v,v)),or__dfg(u,equiv__dfg(v,v))))*. % 291.56/291.86 2951[0:SoR:328.0,251.1] || and_3 -> is_a_theorem(implies__dfg(or__dfg(u,v),or__dfg(u,or__dfg(w,and__dfg(v,not__dfg(w))))))*. % 291.56/291.86 3012[0:SoR:328.0,16.0] || -> is_a_theorem(implies__dfg(or__dfg(u,skc56),or__dfg(u,skc55)))*. % 291.56/291.86 3023[0:SpR:558.0,2802.0] || -> is_a_theorem(implies__dfg(and__dfg(u,not__dfg(u)),v))*. % 291.56/291.86 3026[0:Rew:154.0,3023.0] || -> is_a_theorem(or__dfg(implies__dfg(u,u),v))*. % 291.56/291.86 3031[0:SoR:1158.0,3026.0] || -> is_a_theorem(not__dfg(not__dfg(implies__dfg(u,u))))*. % 291.56/291.86 3033[0:SoR:262.0,3026.0] || -> is_a_theorem(or__dfg(u,implies__dfg(v,v)))*. % 291.56/291.86 3034[0:SoR:273.0,3026.0] || -> is_a_theorem(implies__dfg(u,implies__dfg(v,v)))*. % 291.56/291.86 3040[0:SoR:254.0,3031.0] || is_a_theorem(or__dfg(not__dfg(implies__dfg(u,u)),v))* -> is_a_theorem(v). % 291.56/291.86 3050[0:Rew:78.0,3040.0] || is_a_theorem(implies__dfg(implies__dfg(u,u),v))* -> is_a_theorem(v). % 291.56/291.86 3073[0:Res:286.1,64.0] || and_3 -> equivalence_3*. % 291.56/291.86 3164[0:Res:3012.0,93.1] is_a_theorem(or__dfg(u,skc56)) || -> is_a_theorem(or__dfg(u,skc55))*. % 291.56/291.86 3167[0:SSi:3164.0,258.0,15.1] || -> is_a_theorem(or__dfg(u,skc55))*. % 291.56/291.86 3172[0:SoR:1158.0,3167.0] || -> is_a_theorem(not__dfg(not__dfg(skc55)))*. % 291.56/291.86 3174[0:SoR:262.0,3167.0] || -> is_a_theorem(or__dfg(skc55,u))*. % 291.56/291.86 3178[0:SoR:254.0,3172.0] || is_a_theorem(or__dfg(not__dfg(skc55),u))* -> is_a_theorem(u). % 291.56/291.86 3181[0:Rew:78.0,3178.0] || is_a_theorem(implies__dfg(skc55,u))* -> is_a_theorem(u). % 291.56/291.86 3182[0:SoR:318.0,3174.0] || -> is_a_theorem(or__dfg(u,or__dfg(skc55,v)))*. % 291.56/291.86 3216[0:SoR:1158.0,3182.0] || -> is_a_theorem(not__dfg(not__dfg(or__dfg(skc55,u))))*. % 291.56/291.86 3222[0:SoR:254.0,3216.0] || is_a_theorem(or__dfg(not__dfg(or__dfg(skc55,u)),v))* -> is_a_theorem(v). % 291.56/291.86 3226[0:Rew:78.0,3222.0] || is_a_theorem(implies__dfg(or__dfg(skc55,u),v))* -> is_a_theorem(v). % 291.56/291.86 3377[0:SoR:431.0,327.0] || equivalence_3 -> is_a_theorem(implies__dfg(implies__dfg(implies__dfg(or__dfg(u,not__dfg(v)),or__dfg(u,w)),or__dfg(v,w)),equiv__dfg(or__dfg(v,w),implies__dfg(or__dfg(u,not__dfg(v)),or__dfg(u,w)))))*. % 291.56/291.86 3393[0:SoR:431.0,320.0] || equivalence_3 -> is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,or__dfg(v,w)),or__dfg(v,implies__dfg(u,w))),equiv__dfg(or__dfg(v,implies__dfg(u,w)),implies__dfg(u,or__dfg(v,w)))))*. % 291.56/291.86 3394[0:SoR:431.0,135.0] || equivalence_3 -> is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,v),or__dfg(v,not__dfg(u))),equiv__dfg(or__dfg(v,not__dfg(u)),implies__dfg(u,v))))*. % 291.56/291.86 4682[0:Res:327.0,3226.0] || -> is_a_theorem(implies__dfg(or__dfg(u,not__dfg(skc55)),or__dfg(u,v)))*. % 291.56/291.86 5007[0:SpR:78.0,4682.0] || -> is_a_theorem(implies__dfg(or__dfg(not__dfg(u),not__dfg(skc55)),implies__dfg(u,v)))*. % 291.56/291.86 5016[0:Rew:172.0,5007.0,78.0,5007.0] || -> is_a_theorem(or__dfg(and__dfg(u,skc55),implies__dfg(u,v)))*. % 291.56/291.86 5596[0:SoR:2777.0,3167.0] || -> is_a_theorem(or__dfg(u,or__dfg(v,skc55)))*. % 291.56/291.86 5609[0:SoR:2777.0,129.0] || -> is_a_theorem(or__dfg(u,or__dfg(v,implies__dfg(w,not__dfg(u)))))*. % 291.56/291.86 5618[0:SoR:1158.0,5596.0] || -> is_a_theorem(not__dfg(not__dfg(or__dfg(u,skc55))))*. % 291.56/291.86 5622[0:SpR:78.0,5596.0] || -> is_a_theorem(or__dfg(u,implies__dfg(v,skc55)))*. % 291.56/291.86 5631[0:SpR:78.0,5618.0] || -> is_a_theorem(not__dfg(not__dfg(implies__dfg(u,skc55))))*. % 291.56/291.86 5648[0:SoR:254.0,5631.0] || is_a_theorem(or__dfg(not__dfg(implies__dfg(u,skc55)),v))* -> is_a_theorem(v). % 291.56/291.86 5654[0:Rew:78.0,5648.0] || is_a_theorem(implies__dfg(implies__dfg(u,skc55),v))* -> is_a_theorem(v). % 291.56/291.86 5730[0:SpR:78.0,5622.0] || -> is_a_theorem(implies__dfg(u,implies__dfg(v,skc55)))*. % 291.56/291.86 7024[0:Res:2941.0,93.1] is_a_theorem(or__dfg(u,implies__dfg(v,v))) || -> is_a_theorem(or__dfg(u,equiv__dfg(v,v)))*. % 291.56/291.86 7027[0:SSi:7024.0,3033.0] || -> is_a_theorem(or__dfg(u,equiv__dfg(v,v)))*. % 291.56/291.86 7032[0:SoR:1158.0,7027.0] || -> is_a_theorem(not__dfg(not__dfg(equiv__dfg(u,u))))*. % 291.56/291.86 9207[0:Res:1503.0,3050.0] || -> is_a_theorem(implies__dfg(u,implies__dfg(implies__dfg(u,v),v)))*. % 291.56/291.86 9361[0:SoR:1501.0,4682.0] || -> is_a_theorem(or__dfg(u,implies__dfg(or__dfg(u,not__dfg(skc55)),v)))*. % 291.56/291.86 9453[0:Res:9207.0,5654.0] || -> is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,skc55),v),v))*. % 291.56/291.86 9455[0:Res:9207.0,3181.0] || -> is_a_theorem(implies__dfg(implies__dfg(skc55,u),u))*. % 291.56/291.86 9467[0:SoR:263.0,9455.0] || -> is_a_theorem(or__dfg(u,not__dfg(implies__dfg(skc55,u))))*. % 291.56/291.86 9470[0:Res:9455.0,93.1] is_a_theorem(implies__dfg(skc55,u)) || -> is_a_theorem(u)*. % 291.56/291.86 9503[0:SoR:1551.0,5016.0] || -> is_a_theorem(implies__dfg(u,or__dfg(and__dfg(u,skc55),v)))*. % 291.56/291.86 9508[0:SoR:1551.0,200.0] || -> is_a_theorem(implies__dfg(u,or__dfg(and__dfg(v,u),not__dfg(v))))*. % 291.56/291.86 9531[0:SpR:83.0,9467.0] || -> is_a_theorem(or__dfg(not__dfg(u),and__dfg(skc55,u)))*. % 291.56/291.86 9540[0:Rew:78.0,9531.0] || -> is_a_theorem(implies__dfg(u,and__dfg(skc55,u)))*. % 291.56/291.86 9997[0:SpR:1761.0,182.0] || -> equal(and__dfg(implies__dfg(u,v),implies__dfg(v,not__dfg(not__dfg(u)))),not__dfg(not__dfg(equiv__dfg(u,v))))**. % 291.56/291.86 10108[0:Rew:2696.0,9997.0] || -> equal(not__dfg(not__dfg(equiv__dfg(u,v))),equiv__dfg(not__dfg(not__dfg(u)),v))**. % 291.56/291.86 10109[0:Rew:10108.0,7032.0] || -> is_a_theorem(equiv__dfg(not__dfg(not__dfg(u)),u))*. % 291.56/291.86 10187[0:Res:10109.0,80.0] || -> equal(not__dfg(not__dfg(u)),u)**. % 291.56/291.86 11059[0:SpR:10187.0,81.0] || -> equal(not__dfg(and__dfg(u,v)),implies__dfg(u,not__dfg(v)))**. % 291.56/291.86 11069[0:SpR:10187.0,83.0] || -> equal(not__dfg(implies__dfg(u,v)),and__dfg(u,not__dfg(v)))**. % 291.56/291.86 11160[0:Rew:11059.0,98.0] || is_a_theorem(implies__dfg(implies__dfg(skc92,skc91),or__dfg(and__dfg(skc91,skc90),implies__dfg(skc90,not__dfg(skc92)))))* -> . % 291.56/291.86 11736[0:SpR:1761.0,9453.0] || -> is_a_theorem(implies__dfg(not__dfg(equiv__dfg(u,skc55)),and__dfg(skc55,not__dfg(u))))*. % 291.56/291.86 11742[0:Rew:85.0,11736.0] || -> is_a_theorem(or__dfg(equiv__dfg(u,skc55),and__dfg(skc55,not__dfg(u))))*. % 291.56/291.86 11751[0:SoR:9470.0,9503.0] || -> is_a_theorem(or__dfg(and__dfg(skc55,skc55),u))*. % 291.56/291.86 11772[0:SoR:273.0,11751.0] || -> is_a_theorem(implies__dfg(u,and__dfg(skc55,skc55)))*. % 291.56/291.86 12762[0:SoR:262.0,11742.0] || -> is_a_theorem(or__dfg(and__dfg(skc55,not__dfg(u)),equiv__dfg(u,skc55)))*. % 291.56/291.86 12765[0:Rew:155.0,12762.0] || -> is_a_theorem(implies__dfg(implies__dfg(skc55,u),equiv__dfg(u,skc55)))*. % 291.56/291.86 12774[0:Res:12765.0,93.1] is_a_theorem(implies__dfg(skc55,u)) || -> is_a_theorem(equiv__dfg(u,skc55))*. % 291.56/291.86 13033[0:SoR:12774.0,269.1] is_a_theorem(u) || -> is_a_theorem(equiv__dfg(u,skc55))*. % 291.56/291.86 13045[0:SoR:12774.0,5730.0] || -> is_a_theorem(equiv__dfg(implies__dfg(u,skc55),skc55))*. % 291.56/291.86 13047[0:SoR:12774.0,3034.0] || -> is_a_theorem(equiv__dfg(implies__dfg(u,u),skc55))*. % 291.56/291.86 13069[0:SoR:12774.0,11772.0] || -> is_a_theorem(equiv__dfg(and__dfg(skc55,skc55),skc55))*. % 291.56/291.86 13084[0:Res:13069.0,80.0] || -> equal(and__dfg(skc55,skc55),skc55)**. % 291.56/291.86 13198[0:Res:13045.0,80.0] || -> equal(implies__dfg(u,skc55),skc55)**. % 291.56/291.86 13391[0:SpR:13198.0,94.0] || -> equal(and__dfg(implies__dfg(skc55,u),skc55),equiv__dfg(skc55,u))**. % 291.56/291.86 13429[0:SpR:13198.0,94.0] || -> equal(and__dfg(skc55,implies__dfg(skc55,u)),equiv__dfg(u,skc55))**. % 291.56/291.86 13444[0:SpR:13198.0,1042.0] || -> is_a_theorem(implies__dfg(implies__dfg(skc55,u),or__dfg(u,and__dfg(v,not__dfg(skc55)))))*. % 291.56/291.86 14819[0:Res:13047.0,80.0] || -> equal(implies__dfg(u,u),skc55)**. % 291.56/291.86 15056[0:SpR:14819.0,85.0] || -> equal(or__dfg(u,not__dfg(u)),skc55)**. % 291.56/291.86 15603[0:SpR:15056.0,185.0] || -> equal(and__dfg(not__dfg(u),u),not__dfg(skc55))**. % 291.56/291.86 16241[0:Res:13033.1,80.0] is_a_theorem(u) || -> equal(u,skc55)*. % 291.56/291.86 16287[0:EmS:16241.0,5016.0] || -> equal(or__dfg(and__dfg(u,skc55),implies__dfg(u,v)),skc55)**. % 291.56/291.86 16308[0:EmS:16241.0,9455.0] || -> equal(implies__dfg(implies__dfg(skc55,u),u),skc55)**. % 291.56/291.86 16325[0:EmS:16241.0,9540.0] || -> equal(implies__dfg(u,and__dfg(skc55,u)),skc55)**. % 291.56/291.86 16360[0:EmS:16241.0,114.0] || -> equal(implies__dfg(u,implies__dfg(v,u)),skc55)**. % 291.56/291.86 16366[0:EmS:16241.0,386.0] || -> equal(implies__dfg(and__dfg(u,v),and__dfg(v,u)),skc55)**. % 291.56/291.86 16367[0:EmS:16241.0,378.0] || -> equal(implies__dfg(and__dfg(u,v),v),skc55)**. % 291.56/291.86 16395[0:EmS:16241.0,319.0] || -> equal(implies__dfg(implies__dfg(u,or__dfg(v,w)),or__dfg(v,implies__dfg(u,w))),skc55)**. % 291.56/291.86 16397[0:EmS:16241.0,136.0] || -> equal(implies__dfg(implies__dfg(u,v),or__dfg(v,not__dfg(u))),skc55)**. % 291.56/291.86 16399[0:EmS:16241.0,79.0] || -> equal(implies__dfg(or__dfg(u,v),or__dfg(v,u)),skc55)**. % 291.56/291.86 16404[0:EmS:16241.0,75.0] || -> equal(implies__dfg(u,or__dfg(v,u)),skc55)**. % 291.56/291.86 16405[0:EmS:16241.0,76.0] || -> equal(implies__dfg(or__dfg(u,u),u),skc55)**. % 291.56/291.86 16595[0:Rew:16397.0,3394.1] || equivalence_3 -> is_a_theorem(implies__dfg(skc55,equiv__dfg(or__dfg(u,not__dfg(v)),implies__dfg(v,u))))*. % 291.56/291.86 16650[0:Rew:16395.0,3393.1] || equivalence_3 -> is_a_theorem(implies__dfg(skc55,equiv__dfg(or__dfg(u,implies__dfg(v,w)),implies__dfg(v,or__dfg(u,w)))))*. % 291.56/291.86 16708[0:SpR:10187.0,15603.0] || -> equal(and__dfg(u,not__dfg(u)),not__dfg(skc55))**. % 291.56/291.86 16806[0:SpR:16308.0,94.0] || -> equal(and__dfg(implies__dfg(u,implies__dfg(skc55,u)),skc55),equiv__dfg(u,implies__dfg(skc55,u)))**. % 291.56/291.86 16823[0:Rew:16360.0,16806.0] || -> equal(equiv__dfg(u,implies__dfg(skc55,u)),and__dfg(skc55,skc55))**. % 291.56/291.86 16824[0:Rew:13084.0,16823.0] || -> equal(equiv__dfg(u,implies__dfg(skc55,u)),skc55)**. % 291.56/291.86 16835[0:SpR:16325.0,94.0] || -> equal(and__dfg(implies__dfg(and__dfg(skc55,u),u),skc55),equiv__dfg(and__dfg(skc55,u),u))**. % 291.56/291.86 16850[0:Rew:16367.0,16835.0] || -> equal(equiv__dfg(and__dfg(skc55,u),u),and__dfg(skc55,skc55))**. % 291.56/291.86 16851[0:Rew:13084.0,16850.0] || -> equal(equiv__dfg(and__dfg(skc55,u),u),skc55)**. % 291.56/291.86 16929[0:SpL:16824.0,80.0] || is_a_theorem(skc55) -> equal(implies__dfg(skc55,u),u)**. % 291.56/291.86 16930[0:MRR:16929.0,276.0] || -> equal(implies__dfg(skc55,u),u)**. % 291.56/291.86 16959[0:Rew:16930.0,16650.1] || equivalence_3 -> is_a_theorem(equiv__dfg(or__dfg(u,implies__dfg(v,w)),implies__dfg(v,or__dfg(u,w))))*. % 291.56/291.86 16960[0:Rew:16930.0,16595.1] || equivalence_3 -> is_a_theorem(equiv__dfg(or__dfg(u,not__dfg(v)),implies__dfg(v,u)))*. % 291.56/291.86 17019[0:Rew:16930.0,13391.0] || -> equal(and__dfg(u,skc55),equiv__dfg(skc55,u))**. % 291.56/291.86 17020[0:Rew:16930.0,13429.0] || -> equal(and__dfg(skc55,u),equiv__dfg(u,skc55))**. % 291.56/291.86 17021[0:Rew:16930.0,13444.0] || -> is_a_theorem(implies__dfg(u,or__dfg(u,and__dfg(v,not__dfg(skc55)))))*. % 291.56/291.86 17094[0:Rew:17019.0,16287.0] || -> equal(or__dfg(equiv__dfg(skc55,u),implies__dfg(u,v)),skc55)**. % 291.56/291.86 17115[0:Rew:17020.0,16851.0] || -> equal(equiv__dfg(equiv__dfg(u,skc55),u),skc55)**. % 291.56/291.86 17297[0:Res:16960.1,80.0] || equivalence_3 -> equal(or__dfg(u,not__dfg(v)),implies__dfg(v,u))**. % 291.56/291.86 17317[0:Rew:17297.1,3377.1] || equivalence_3 -> is_a_theorem(implies__dfg(implies__dfg(implies__dfg(implies__dfg(u,v),or__dfg(v,w)),or__dfg(u,w)),equiv__dfg(or__dfg(u,w),implies__dfg(implies__dfg(u,v),or__dfg(v,w)))))*. % 291.56/291.86 17395[0:SpL:17115.0,80.0] || is_a_theorem(skc55) -> equal(equiv__dfg(u,skc55),u)**. % 291.56/291.86 17396[0:MRR:17395.0,276.0] || -> equal(equiv__dfg(u,skc55),u)**. % 291.56/291.86 17398[0:Rew:17396.0,17020.0] || -> equal(and__dfg(skc55,u),u)**. % 291.56/291.86 17723[0:SpR:16405.0,94.0] || -> equal(and__dfg(skc55,implies__dfg(u,or__dfg(u,u))),equiv__dfg(or__dfg(u,u),u))**. % 291.56/291.86 17742[0:Rew:17398.0,17723.0,16404.0,17723.0] || -> equal(equiv__dfg(or__dfg(u,u),u),skc55)**. % 291.56/291.86 18158[0:SpL:17742.0,80.0] || is_a_theorem(skc55) -> equal(or__dfg(u,u),u)**. % 291.56/291.86 18159[0:MRR:18158.0,276.0] || -> equal(or__dfg(u,u),u)**. % 291.56/291.86 18192[0:SpR:18159.0,78.0] || -> equal(implies__dfg(u,not__dfg(u)),not__dfg(u))**. % 291.56/291.86 19483[0:SpR:18192.0,9361.0] || -> is_a_theorem(or__dfg(u,not__dfg(or__dfg(u,not__dfg(skc55)))))*. % 291.56/291.86 19506[0:Rew:17019.0,19483.0,185.0,19483.0] || -> is_a_theorem(or__dfg(u,equiv__dfg(skc55,not__dfg(u))))*. % 291.56/291.86 19634[0:SpR:10187.0,19506.0] || -> is_a_theorem(or__dfg(not__dfg(u),equiv__dfg(skc55,u)))*. % 291.56/291.86 19649[0:Rew:78.0,19634.0] || -> is_a_theorem(implies__dfg(u,equiv__dfg(skc55,u)))*. % 291.56/291.86 19661[0:EmS:16241.0,19649.0] || -> equal(implies__dfg(u,equiv__dfg(skc55,u)),skc55)**. % 291.56/291.86 19740[0:SpR:19661.0,94.0] || -> equal(and__dfg(skc55,implies__dfg(equiv__dfg(skc55,u),u)),equiv__dfg(u,equiv__dfg(skc55,u)))**. % 291.56/291.86 19757[0:Rew:17398.0,19740.0] || -> equal(equiv__dfg(u,equiv__dfg(skc55,u)),implies__dfg(equiv__dfg(skc55,u),u))**. % 291.56/291.86 20454[0:Res:16959.1,80.0] || equivalence_3 -> equal(or__dfg(u,implies__dfg(v,w)),implies__dfg(v,or__dfg(u,w)))**. % 291.56/291.86 22897[0:SpR:16708.0,17021.0] || -> is_a_theorem(implies__dfg(u,or__dfg(u,not__dfg(skc55))))*. % 291.56/291.86 22958[0:SoR:1501.0,22897.0] || -> is_a_theorem(or__dfg(u,implies__dfg(u,not__dfg(skc55))))*. % 291.56/291.86 23026[0:SoR:262.0,22958.0] || -> is_a_theorem(or__dfg(implies__dfg(u,not__dfg(skc55)),u))*. % 291.56/291.86 23060[0:Rew:17019.0,23026.0,173.0,23026.0] || -> is_a_theorem(implies__dfg(equiv__dfg(skc55,u),u))*. % 291.56/291.86 23085[0:EmS:16241.0,23060.0] || -> equal(implies__dfg(equiv__dfg(skc55,u),u),skc55)**. % 291.56/291.86 23118[0:Rew:23085.0,19757.0] || -> equal(equiv__dfg(u,equiv__dfg(skc55,u)),skc55)**. % 291.56/291.86 23353[0:SpL:23118.0,80.0] || is_a_theorem(skc55) -> equal(equiv__dfg(skc55,u),u)**. % 291.56/291.86 23354[0:MRR:23353.0,276.0] || -> equal(equiv__dfg(skc55,u),u)**. % 291.56/291.86 23468[0:Rew:23354.0,17094.0] || -> equal(or__dfg(u,implies__dfg(u,v)),skc55)**. % 291.56/291.86 25412[0:SpR:23468.0,2951.1] || and_3 -> is_a_theorem(implies__dfg(skc55,or__dfg(u,or__dfg(v,and__dfg(implies__dfg(u,w),not__dfg(v))))))*. % 291.56/291.86 25446[0:Rew:16930.0,25412.1] || and_3 -> is_a_theorem(or__dfg(u,or__dfg(v,and__dfg(implies__dfg(u,w),not__dfg(v)))))*. % 291.56/291.86 31909[0:SpR:10187.0,5609.0] || -> is_a_theorem(or__dfg(not__dfg(u),or__dfg(v,implies__dfg(w,u))))*. % 291.56/291.86 31966[0:Rew:78.0,31909.0] || -> is_a_theorem(implies__dfg(u,or__dfg(v,implies__dfg(w,u))))*. % 291.56/291.86 32026[0:SpR:78.0,31966.0] || -> is_a_theorem(implies__dfg(u,implies__dfg(v,implies__dfg(w,u))))*. % 291.56/291.86 32326[0:EmS:16241.0,32026.0] || -> equal(implies__dfg(u,implies__dfg(v,implies__dfg(w,u))),skc55)**. % 291.56/291.86 33448[0:EmS:16241.0,9508.0] || -> equal(implies__dfg(u,or__dfg(and__dfg(v,u),not__dfg(v))),skc55)**. % 291.56/291.86 35947[0:SpR:16366.0,94.0] || -> equal(and__dfg(implies__dfg(and__dfg(u,v),and__dfg(v,u)),skc55),equiv__dfg(and__dfg(u,v),and__dfg(v,u)))**. % 291.56/291.86 36075[0:Rew:17398.0,35947.0,16366.0,35947.0] || -> equal(equiv__dfg(and__dfg(u,v),and__dfg(v,u)),skc55)**. % 291.56/291.86 36082[0:SpR:16399.0,94.0] || -> equal(and__dfg(implies__dfg(or__dfg(u,v),or__dfg(v,u)),skc55),equiv__dfg(or__dfg(u,v),or__dfg(v,u)))**. % 291.56/291.86 36180[0:Rew:17398.0,36082.0,16399.0,36082.0] || -> equal(equiv__dfg(or__dfg(u,v),or__dfg(v,u)),skc55)**. % 291.56/291.86 46279[0:SpL:36075.0,80.0] || is_a_theoreTerminated %------------------------------------------------------------------------------