%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP127-3.004 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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 : Sat Jul 16 11:45:40 EDT 2022 % Result : Unsatisfiable 0.20s 0.52s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP127-3.004 : TPTP v8.1.0. Released v1.2.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.33 % Computer : n016.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 13 14:59:14 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.52 % 0.20/0.52 SPASS V 3.9 % 0.20/0.52 SPASS beiseite: Proof found. % 0.20/0.52 % SZS status Theorem % 0.20/0.52 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.52 SPASS derived 512 clauses, backtracked 580 clauses, performed 25 splits and kept 848 clauses. % 0.20/0.52 SPASS allocated 76141 KBytes. % 0.20/0.52 SPASS spent 0:00:00.18 on the problem. % 0.20/0.52 0:00:00.04 for the input. % 0.20/0.52 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.52 0:00:00.01 for inferences. % 0.20/0.52 0:00:00.00 for the backtracking. % 0.20/0.52 0:00:00.10 for the reduction. % 0.20/0.52 % 0.20/0.52 % 0.20/0.52 Here is a proof with depth 14, length 166 : % 0.20/0.52 % SZS output start Refutation % 0.20/0.52 1[0:Inp] || -> next(e_0,e_1)*. % 0.20/0.52 2[0:Inp] || -> next(e_1,e_2)*. % 0.20/0.52 3[0:Inp] || -> next(e_2,e_3)*. % 0.20/0.52 4[0:Inp] || -> next(e_3,e_4)*. % 0.20/0.52 5[0:Inp] || -> greater(e_1,e_0)*. % 0.20/0.52 6[0:Inp] || -> greater(e_2,e_0)*. % 0.20/0.52 7[0:Inp] || -> greater(e_3,e_0)*. % 0.20/0.52 12[0:Inp] || -> greater(e_3,e_2)*. % 0.20/0.52 13[0:Inp] || -> greater(e_4,e_2)*. % 0.20/0.52 15[0:Inp] || cycle(u,v)*+ cycle(u,w)* -> equalish(w,v)*. % 0.20/0.52 16[0:Inp] group_element(u) || -> cycle(u,e_3) cycle(u,e_2) cycle(u,e_1) cycle(u,e_0)*. % 0.20/0.52 17[0:Inp] || -> cycle(e_4,e_0)*. % 0.20/0.52 18[0:Inp] || next(u,v)*+ next(w,x)* cycle(x,u)* cycle(w,y)* greater(y,e_0) -> equalish(y,v)*. % 0.20/0.52 19[0:Inp] || greater(u,v)*+ greater(w,x)* next(w,y)* cycle(y,v)* cycle(x,u)* cycle(w,e_0) -> . % 0.20/0.52 20[0:Inp] || greater(u,v) cycle(v,e_0) product(v,e_1,u)*+ -> . % 0.20/0.52 21[0:Inp] || next(u,v)* cycle(u,w)* greater(w,e_0)* product(u,e_1,x)*+ -> equalish(x,v)*. % 0.20/0.52 22[0:Inp] || -> group_element(e_1)*. % 0.20/0.52 23[0:Inp] || -> group_element(e_2)*. % 0.20/0.52 24[0:Inp] || -> group_element(e_3)*. % 0.20/0.52 25[0:Inp] || -> group_element(e_4)*. % 0.20/0.52 26[0:Inp] || equalish(e_1,e_2)*+ -> . % 0.20/0.52 27[0:Inp] || equalish(e_1,e_3)*+ -> . % 0.20/0.52 28[0:Inp] || equalish(e_1,e_4)*+ -> . % 0.20/0.52 29[0:Inp] || equalish(e_2,e_1)*+ -> . % 0.20/0.52 30[0:Inp] || equalish(e_2,e_3)*+ -> . % 0.20/0.52 32[0:Inp] || equalish(e_3,e_1)*+ -> . % 0.20/0.52 33[0:Inp] || equalish(e_3,e_2)*+ -> . % 0.20/0.52 36[0:Inp] || equalish(e_4,e_2)*+ -> . % 0.20/0.52 37[0:Inp] || equalish(e_4,e_3)*+ -> . % 0.20/0.52 38[0:Inp] group_element(u) group_element(v) || -> product(v,u,e_4) product(v,u,e_3) product(v,u,e_2) product(v,u,e_1)*. % 0.20/0.52 39[0:Inp] || product(u,v,w)*+ product(u,v,x)* -> equalish(x,w)*. % 0.20/0.52 40[0:Inp] || product(u,v,w)*+ product(u,x,w)* -> equalish(x,v)*. % 0.20/0.52 41[0:Inp] || product(u,v,w)*+ product(x,v,w)* -> equalish(x,u)*. % 0.20/0.52 42[0:Inp] || -> product(u,u,u)*. % 0.20/0.52 43[0:Inp] || product(u,v,w)*+ product(v,x,u)* -> product(w,v,x)*. % 0.20/0.52 55[0:Res:42.0,41.0] || product(u,v,v)*+ -> equalish(u,v). % 0.20/0.52 57[0:Res:42.0,40.0] || product(u,v,u)*+ -> equalish(v,u). % 0.20/0.52 72[0:Res:38.5,57.0] group_element(u) group_element(e_1) || -> product(e_1,u,e_4) product(e_1,u,e_3) product(e_1,u,e_2)* equalish(u,e_1). % 0.20/0.52 76[0:Res:38.5,43.0] group_element(u) group_element(v) || product(u,w,v)*+ -> product(v,u,e_4) product(v,u,e_3) product(v,u,e_2)* product(e_1,u,w)*. % 0.20/0.52 80[0:Res:38.5,55.0] group_element(e_1) group_element(u) || -> product(u,e_1,e_4) product(u,e_1,e_3) product(u,e_1,e_2)* equalish(u,e_1). % 0.20/0.52 83[0:SSi:80.0,22.0] group_element(u) || -> product(u,e_1,e_4) product(u,e_1,e_3) product(u,e_1,e_2)* equalish(u,e_1). % 0.20/0.52 85[0:SSi:72.1,22.0] group_element(u) || -> product(e_1,u,e_4) product(e_1,u,e_3) product(e_1,u,e_2)* equalish(u,e_1). % 0.20/0.52 92[0:Res:2.0,18.0] || next(u,v)*+ cycle(v,e_1) cycle(u,w)* greater(w,e_0) -> equalish(w,e_2)*. % 0.20/0.52 93[0:Res:1.0,18.0] || next(u,v)*+ cycle(v,e_0) cycle(u,w)* greater(w,e_0) -> equalish(w,e_1)*. % 0.20/0.52 94[0:Res:83.3,57.0] group_element(e_2) || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.20/0.52 104[0:SSi:94.0,23.0] || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.20/0.52 105[0:MRR:104.2,104.3,29.0,26.0] || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)*. % 0.20/0.52 106[0:Res:105.1,43.0] || product(e_1,u,e_2)* -> product(e_2,e_1,e_4) product(e_3,e_1,u). % 0.20/0.52 107[0:Res:105.1,39.0] || product(e_2,e_1,u)*+ -> product(e_2,e_1,e_4)* equalish(u,e_3). % 0.20/0.52 111[0:Res:105.1,20.2] || greater(e_3,e_2) cycle(e_2,e_0) -> product(e_2,e_1,e_4)*. % 0.20/0.52 112[0:MRR:111.0,12.0] || cycle(e_2,e_0)+ -> product(e_2,e_1,e_4)*. % 0.20/0.52 113[0:Res:16.4,112.0] group_element(e_2) || -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1) product(e_2,e_1,e_4)*. % 0.20/0.52 114[0:SSi:113.0,23.0] || -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1) product(e_2,e_1,e_4)*. % 0.20/0.52 115[1:Spt:107.0,107.2] || product(e_2,e_1,u)*+ -> equalish(u,e_3). % 0.20/0.52 128[0:Res:5.0,19.0] || greater(u,v)*+ next(u,w)* cycle(w,e_0) cycle(v,e_1) cycle(u,e_0) -> . % 0.20/0.52 133[2:Spt:114.3] || -> product(e_2,e_1,e_4)*. % 0.20/0.52 140[2:Res:133.0,115.0] || -> equalish(e_4,e_3)*. % 0.20/0.52 141[2:MRR:140.0,37.0] || -> . % 0.20/0.52 143[2:Spt:141.0,114.3,133.0] || product(e_2,e_1,e_4)*+ -> . % 0.20/0.52 144[2:Spt:141.0,114.0,114.1,114.2] || -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 0.20/0.52 145[2:MRR:105.0,143.0] || -> product(e_2,e_1,e_3)*. % 0.20/0.52 147[2:MRR:106.1,143.0] || product(e_1,u,e_2)*+ -> product(e_3,e_1,u). % 0.20/0.52 150[2:Res:144.2,15.0] || cycle(e_2,u)+ -> cycle(e_2,e_3) cycle(e_2,e_2) equalish(u,e_1)*. % 0.20/0.52 163[3:Spt:150.0,150.3] || cycle(e_2,u)+ -> equalish(u,e_1)*. % 0.20/0.52 177[0:Res:85.3,55.0] group_element(e_2) || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.20/0.52 181[0:SSi:177.0,23.0] || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.20/0.52 182[0:MRR:181.2,181.3,29.0,26.0] || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)*. % 0.20/0.52 189[0:Res:182.1,40.0] || product(e_1,u,e_3)*+ -> product(e_1,e_2,e_4)* equalish(u,e_2). % 0.20/0.52 200[0:Res:3.0,92.0] || cycle(e_3,e_1)+ cycle(e_2,u) greater(u,e_0) -> equalish(u,e_2)*. % 0.20/0.52 205[0:Res:4.0,93.0] || cycle(e_4,e_0) cycle(e_3,u) greater(u,e_0) -> equalish(u,e_1)*. % 0.20/0.52 209[0:MRR:205.0,17.0] || cycle(e_3,u)+ greater(u,e_0) -> equalish(u,e_1)*. % 0.20/0.52 210[0:Res:16.4,209.0] group_element(e_3) || greater(e_0,e_0) -> cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1) equalish(e_0,e_1)*. % 0.20/0.52 211[0:SSi:210.0,24.0] || greater(e_0,e_0)+ -> cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1) equalish(e_0,e_1)*. % 0.20/0.52 216[0:Res:12.0,128.0] || next(e_3,u)* cycle(u,e_0) cycle(e_2,e_1) cycle(e_3,e_0) -> . % 0.20/0.52 355[4:Spt:211.1] || -> cycle(e_3,e_3)*. % 0.20/0.52 362[4:Res:355.0,209.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 0.20/0.52 363[4:MRR:362.0,362.1,7.0,32.0] || -> . % 0.20/0.52 364[4:Spt:363.0,211.1,355.0] || cycle(e_3,e_3)*+ -> . % 0.20/0.52 365[4:Spt:363.0,211.0,211.2,211.3,211.4] || greater(e_0,e_0)+ -> cycle(e_3,e_2) cycle(e_3,e_1) equalish(e_0,e_1)*. % 0.20/0.52 366[5:Spt:365.1] || -> cycle(e_3,e_2)*. % 0.20/0.52 372[5:Res:366.0,209.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 0.20/0.52 373[5:MRR:372.0,372.1,6.0,29.0] || -> . % 0.20/0.52 374[5:Spt:373.0,365.1,366.0] || cycle(e_3,e_2)*+ -> . % 0.20/0.52 375[5:Spt:373.0,365.0,365.2,365.3] || greater(e_0,e_0)+ -> cycle(e_3,e_1) equalish(e_0,e_1)*. % 0.20/0.52 376[6:Spt:375.1] || -> cycle(e_3,e_1)*. % 0.20/0.52 377[6:MRR:200.0,376.0] || cycle(e_2,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 0.20/0.52 389[6:Res:144.2,377.0] || greater(e_1,e_0) -> cycle(e_2,e_3) cycle(e_2,e_2) equalish(e_1,e_2)*. % 0.20/0.52 390[6:MRR:389.0,389.3,5.0,26.0] || -> cycle(e_2,e_3) cycle(e_2,e_2)*. % 0.20/0.52 391[7:Spt:390.0] || -> cycle(e_2,e_3)*. % 0.20/0.52 399[7:Res:391.0,377.0] || greater(e_3,e_0) -> equalish(e_3,e_2)*. % 0.20/0.52 402[7:MRR:399.0,399.1,7.0,33.0] || -> . % 0.20/0.52 403[7:Spt:402.0,390.0,391.0] || cycle(e_2,e_3)* -> . % 0.20/0.52 404[7:Spt:402.0,390.1] || -> cycle(e_2,e_2)*. % 0.20/0.52 411[7:Res:404.0,163.0] || -> equalish(e_2,e_1)*. % 0.20/0.52 412[7:MRR:411.0,29.0] || -> . % 0.20/0.52 413[6:Spt:412.0,375.1,376.0] || cycle(e_3,e_1)*+ -> . % 0.20/0.52 414[6:Spt:412.0,375.0,375.2] || greater(e_0,e_0)+ -> equalish(e_0,e_1)*. % 0.20/0.52 415[7:Spt:144.0] || -> cycle(e_2,e_3)*. % 0.20/0.52 424[7:Res:415.0,163.0] || -> equalish(e_3,e_1)*. % 0.20/0.52 425[7:MRR:424.0,32.0] || -> . % 0.20/0.52 426[7:Spt:425.0,144.0,415.0] || cycle(e_2,e_3)*+ -> . % 0.20/0.52 427[7:Spt:425.0,144.1,144.2] || -> cycle(e_2,e_2) cycle(e_2,e_1)*. % 0.20/0.52 428[8:Spt:427.0] || -> cycle(e_2,e_2)*. % 0.20/0.52 435[8:Res:428.0,163.0] || -> equalish(e_2,e_1)*. % 0.20/0.52 436[8:MRR:435.0,29.0] || -> . % 0.20/0.52 437[8:Spt:436.0,427.0,428.0] || cycle(e_2,e_2)*+ -> . % 0.20/0.52 438[8:Spt:436.0,427.1] || -> cycle(e_2,e_1)*. % 0.20/0.52 440[8:MRR:216.2,438.0] || next(e_3,u)*+ cycle(u,e_0) cycle(e_3,e_0) -> . % 0.20/0.52 463[2:Res:145.0,76.2] group_element(e_2) group_element(e_3) || -> product(e_3,e_2,e_4) product(e_3,e_2,e_3) product(e_3,e_2,e_2) product(e_1,e_2,e_1)*. % 0.20/0.52 466[2:SSi:463.1,463.0,24.0,23.0] || -> product(e_3,e_2,e_4) product(e_3,e_2,e_3) product(e_3,e_2,e_2) product(e_1,e_2,e_1)*. % 0.20/0.52 480[8:Res:4.0,440.0] || cycle(e_4,e_0) cycle(e_3,e_0)* -> . % 0.20/0.52 481[8:MRR:480.0,17.0] || cycle(e_3,e_0)*+ -> . % 0.20/0.52 482[8:Res:16.4,481.0] group_element(e_3) || -> cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 0.20/0.52 483[8:SSi:482.0,24.0] || -> cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 0.20/0.52 484[8:MRR:483.0,483.1,483.2,364.0,374.0,413.0] || -> . % 0.20/0.52 485[3:Spt:484.0,150.1,150.2] || -> cycle(e_2,e_3) cycle(e_2,e_2)*. % 0.20/0.52 499[4:Spt:189.0,189.2] || product(e_1,u,e_3)*+ -> equalish(u,e_2). % 0.20/0.52 517[2:Res:466.3,57.0] || -> product(e_3,e_2,e_4) product(e_3,e_2,e_3) product(e_3,e_2,e_2)* equalish(e_2,e_1). % 0.20/0.52 528[2:MRR:517.3,29.0] || -> product(e_3,e_2,e_4) product(e_3,e_2,e_3) product(e_3,e_2,e_2)*. % 0.20/0.52 535[2:Res:528.2,55.0] || -> product(e_3,e_2,e_4) product(e_3,e_2,e_3)* equalish(e_3,e_2). % 0.20/0.52 537[2:MRR:535.2,33.0] || -> product(e_3,e_2,e_4) product(e_3,e_2,e_3)*. % 0.20/0.52 539[2:Res:537.1,57.0] || -> product(e_3,e_2,e_4)* equalish(e_2,e_3). % 0.20/0.52 548[2:MRR:539.1,30.0] || -> product(e_3,e_2,e_4)*. % 0.20/0.52 552[2:Res:548.0,43.0] || product(e_2,u,e_3)*+ -> product(e_4,e_2,u). % 0.20/0.52 554[2:Res:548.0,40.0] || product(e_3,u,e_4)*+ -> equalish(u,e_2). % 0.20/0.52 555[2:Res:548.0,41.0] || product(u,e_2,e_4)*+ -> equalish(u,e_3). % 0.20/0.52 563[2:Res:145.0,552.0] || -> product(e_4,e_2,e_1)*. % 0.20/0.52 565[2:Res:563.0,76.2] group_element(e_4) group_element(e_1) || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3) product(e_1,e_4,e_2)* product(e_1,e_4,e_2)*. % 0.20/0.52 575[2:Obv:565.4] group_element(e_4) group_element(e_1) || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3) product(e_1,e_4,e_2)*. % 0.20/0.52 576[2:SSi:575.1,575.0,22.0,25.0] || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3) product(e_1,e_4,e_2)*. % 0.20/0.52 592[2:Res:576.2,147.0] || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3)* product(e_3,e_1,e_4). % 0.20/0.52 594[5:Spt:592.0] || -> product(e_1,e_4,e_4)*. % 0.20/0.52 600[5:Res:594.0,55.0] || -> equalish(e_1,e_4)*. % 0.20/0.52 602[5:MRR:600.0,28.0] || -> . % 0.20/0.52 604[5:Spt:602.0,592.0,594.0] || product(e_1,e_4,e_4)* -> . % 0.20/0.52 605[5:Spt:602.0,592.1,592.2] || -> product(e_1,e_4,e_3)* product(e_3,e_1,e_4). % 0.20/0.52 611[6:Spt:605.0] || -> product(e_1,e_4,e_3)*. % 0.20/0.52 618[6:Res:611.0,499.0] || -> equalish(e_4,e_2)*. % 0.20/0.52 619[6:MRR:618.0,36.0] || -> . % 0.20/0.52 621[6:Spt:619.0,605.0,611.0] || product(e_1,e_4,e_3)* -> . % 0.20/0.52 622[6:Spt:619.0,605.1] || -> product(e_3,e_1,e_4)*. % 0.20/0.52 636[6:Res:622.0,554.0] || -> equalish(e_1,e_2)*. % 0.20/0.52 637[6:MRR:636.0,26.0] || -> . % 0.20/0.52 639[4:Spt:637.0,189.1] || -> product(e_1,e_2,e_4)*. % 0.20/0.52 645[4:Res:639.0,555.0] || -> equalish(e_1,e_3)*. % 0.20/0.52 647[4:MRR:645.0,27.0] || -> . % 0.20/0.52 649[1:Spt:647.0,107.1] || -> product(e_2,e_1,e_4)*. % 0.20/0.52 657[1:Res:649.0,21.3] || next(e_2,u)+ cycle(e_2,v) greater(v,e_0)* -> equalish(e_4,u)*. % 0.20/0.52 658[1:Res:649.0,20.2] || greater(e_4,e_2)* cycle(e_2,e_0) -> . % 0.20/0.52 661[1:MRR:658.0,13.0] || cycle(e_2,e_0)*+ -> . % 0.20/0.52 664[1:Res:16.4,661.0] group_element(e_2) || -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 0.20/0.52 665[1:SSi:664.0,23.0] || -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 0.20/0.52 684[2:Spt:665.0] || -> cycle(e_2,e_3)*. % 0.20/0.52 714[1:Res:3.0,657.0] || cycle(e_2,u) greater(u,e_0)* -> equalish(e_4,e_3)*. % 0.20/0.52 715[1:MRR:714.2,37.0] || cycle(e_2,u)+ greater(u,e_0)* -> . % 0.20/0.52 717[2:Res:684.0,715.0] || greater(e_3,e_0)* -> . % 0.20/0.52 718[2:MRR:717.0,7.0] || -> . % 0.20/0.52 719[2:Spt:718.0,665.0,684.0] || cycle(e_2,e_3)* -> . % 0.20/0.52 720[2:Spt:718.0,665.1,665.2] || -> cycle(e_2,e_2) cycle(e_2,e_1)*. % 0.20/0.52 721[3:Spt:720.1] || -> cycle(e_2,e_1)*. % 0.20/0.52 727[3:Res:721.0,715.0] || greater(e_1,e_0)* -> . % 0.20/0.52 728[3:MRR:727.0,5.0] || -> . % 0.20/0.52 729[3:Spt:728.0,720.1,721.0] || cycle(e_2,e_1)* -> . % 0.20/0.52 730[3:Spt:728.0,720.0] || -> cycle(e_2,e_2)*. % 0.20/0.52 737[3:Res:730.0,715.0] || greater(e_2,e_0)* -> . % 0.20/0.52 738[3:MRR:737.0,6.0] || -> . % 0.20/0.52 % SZS output end Refutation % 0.20/0.52 Formulae used in the proof : e_0_then_e_1 e_1_then_e_2 e_2_then_e_3 e_3_then_e_4 e_1_greater_e_0 e_2_greater_e_0 e_3_greater_e_0 e_3_greater_e_2 e_4_greater_e_2 cycle1 cycle2 cycle3 cycle4 cycle5 cycle6 cycle7 element_1 element_2 element_3 element_4 e_1_is_not_e_2 e_1_is_not_e_3 e_1_is_not_e_4 e_2_is_not_e_1 e_2_is_not_e_3 e_3_is_not_e_1 e_3_is_not_e_2 e_4_is_not_e_2 e_4_is_not_e_3 product_total_function1 product_total_function2 product_right_cancellation product_left_cancellation product_idempotence qg3 % 0.20/0.52 %------------------------------------------------------------------------------