%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP214-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n005.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:46:21 EDT 2022 % Result : Unsatisfiable 0.19s 0.43s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : GRP214-1 : TPTP v8.1.0. Released v2.5.0. % 0.04/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n005.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % 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 07:58:09 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.43 % 0.19/0.43 SPASS V 3.9 % 0.19/0.43 SPASS beiseite: Proof found. % 0.19/0.43 % SZS status Theorem % 0.19/0.43 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.43 SPASS derived 312 clauses, backtracked 84 clauses, performed 6 splits and kept 247 clauses. % 0.19/0.43 SPASS allocated 63332 KBytes. % 0.19/0.43 SPASS spent 0:00:00.08 on the problem. % 0.19/0.43 0:00:00.03 for the input. % 0.19/0.43 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.43 0:00:00.00 for inferences. % 0.19/0.43 0:00:00.00 for the backtracking. % 0.19/0.43 0:00:00.02 for the reduction. % 0.19/0.43 % 0.19/0.43 % 0.19/0.43 Here is a proof with depth 5, length 132 : % 0.19/0.43 % SZS output start Refutation % 0.19/0.43 1[0:Inp] || -> equal(multiply(sk_c3,sk_c7),sk_c5)** equal(multiply(sk_c1,sk_c7),sk_c6). % 0.19/0.43 2[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.19/0.43 3[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6)** equal(multiply(sk_c1,sk_c7),sk_c6). % 0.19/0.43 4[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.19/0.43 5[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c5)**. % 0.19/0.43 6[0:Inp] || -> equal(inverse(sk_c3),sk_c7)** equal(inverse(sk_c1),sk_c7). % 0.19/0.43 7[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.19/0.43 8[0:Inp] || -> equal(inverse(sk_c4),sk_c5)** equal(inverse(sk_c1),sk_c7). % 0.19/0.43 13[0:Inp] || equal(inverse(u),v) equal(inverse(w),sk_c7) equal(inverse(x),sk_c7) equal(multiply(u,v),sk_c6)**+ equal(multiply(w,sk_c7),v)* equal(multiply(x,sk_c7),sk_c6)** equal(multiply(sk_c7,y),sk_c6)** -> . % 0.19/0.43 14[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.19/0.43 15[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.19/0.43 16[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.19/0.43 17[1:Spt:13.0,13.1,13.3,13.4] || equal(inverse(u),v) equal(inverse(w),sk_c7) equal(multiply(u,v),sk_c6)**+ equal(multiply(w,sk_c7),v)* -> . % 0.19/0.43 18[2:Spt:8.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.43 26[3:Spt:4.1] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.19/0.43 33[2:SpR:18.0,15.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.19/0.43 34[1:SpL:15.0,17.2] || equal(inverse(inverse(u)),u)** equal(inverse(v),sk_c7) equal(identity,sk_c6) equal(multiply(v,sk_c7),u)* -> . % 0.19/0.43 47[0:SpR:15.0,16.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.19/0.43 49[2:SpR:33.0,16.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),multiply(identity,u))**. % 0.19/0.43 52[2:Rew:14.0,49.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.19/0.43 53[0:Rew:14.0,47.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.19/0.43 57[3:SpR:26.0,52.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.19/0.43 64[0:SpR:53.0,53.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.19/0.43 68[0:SpR:15.0,53.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.43 72[3:SpR:57.0,53.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.19/0.43 77[3:Rew:15.0,72.0] || -> equal(identity,sk_c6)**. % 0.19/0.43 79[3:Rew:77.0,15.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.19/0.43 85[3:Rew:77.0,34.2] || equal(inverse(inverse(u)),u)** equal(inverse(v),sk_c7) equal(sk_c6,sk_c6) equal(multiply(v,sk_c7),u)* -> . % 0.19/0.43 95[3:Rew:77.0,68.0] || -> equal(multiply(inverse(inverse(u)),sk_c6),u)**. % 0.19/0.43 98[3:Rew:64.0,95.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.43 102[3:Obv:85.2] || equal(inverse(inverse(u)),u)** equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),u)* -> . % 0.19/0.43 134[3:SpR:79.0,53.0] || -> equal(multiply(inverse(inverse(u)),sk_c6),u)**. % 0.19/0.43 144[3:Rew:98.0,134.0] || -> equal(inverse(inverse(u)),u)**. % 0.19/0.43 146[3:Rew:144.0,102.0] || equal(u,u)* equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),u)* -> . % 0.19/0.43 149[3:Obv:146.0] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),v)* -> . % 0.19/0.43 150[3:AED:149.1] || equal(inverse(u),sk_c7)** -> . % 0.19/0.43 151[3:UnC:150.0,18.0] || -> . % 0.19/0.43 156[3:Spt:151.0,4.1,26.0] || equal(multiply(sk_c1,sk_c7),sk_c6)** -> . % 0.19/0.43 157[3:Spt:151.0,4.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.19/0.43 160[3:MRR:2.1,156.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.43 161[0:Rew:64.0,68.0] || -> equal(multiply(u,identity),u)**. % 0.19/0.43 162[3:MRR:3.1,156.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.19/0.43 163[3:MRR:1.1,156.0] || -> equal(multiply(sk_c3,sk_c7),sk_c5)**. % 0.19/0.43 168[3:SpR:162.0,16.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),multiply(sk_c6,u))**. % 0.19/0.43 169[3:SpR:162.0,53.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.19/0.43 171[3:Rew:157.0,169.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.19/0.43 173[2:SpR:33.0,53.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c1)**. % 0.19/0.43 175[2:Rew:161.0,173.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.19/0.43 182[2:SpR:175.0,53.0] || -> equal(multiply(sk_c1,multiply(sk_c7,u)),u)**. % 0.19/0.43 194[3:SpR:163.0,53.0] || -> equal(multiply(inverse(sk_c3),sk_c5),sk_c7)**. % 0.19/0.43 196[3:Rew:160.0,194.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.19/0.43 198[3:SpR:171.0,53.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c6)**. % 0.19/0.43 200[3:Rew:15.0,198.0] || -> equal(identity,sk_c6)**. % 0.19/0.43 202[3:Rew:200.0,14.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.43 210[3:Rew:202.0,168.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),u)**. % 0.19/0.43 225[3:SpR:196.0,53.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.19/0.43 227[3:Rew:175.0,225.0] || -> equal(multiply(sk_c1,sk_c7),sk_c5)**. % 0.19/0.43 228[3:Rew:227.0,156.0] || equal(sk_c5,sk_c6)** -> . % 0.19/0.43 234[3:SpR:227.0,16.0] || -> equal(multiply(sk_c1,multiply(sk_c7,u)),multiply(sk_c5,u))**. % 0.19/0.43 239[3:Rew:182.0,234.0] || -> equal(multiply(sk_c5,u),u)**. % 0.19/0.43 241[3:Rew:239.0,210.0] || -> equal(multiply(sk_c4,u),u)**. % 0.19/0.43 244[3:Rew:241.0,162.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.43 245[3:MRR:244.0,228.0] || -> . % 0.19/0.43 246[2:Spt:245.0,8.1,18.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.19/0.43 247[2:Spt:245.0,8.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.19/0.43 248[2:MRR:6.1,246.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.43 249[2:MRR:7.0,246.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.19/0.43 256[2:SpR:249.0,53.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.19/0.43 258[2:Rew:247.0,256.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.19/0.43 264[2:SpR:258.0,53.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c6)**. % 0.19/0.43 266[2:Rew:15.0,264.0] || -> equal(identity,sk_c6)**. % 0.19/0.43 267[2:Rew:266.0,161.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.43 271[2:Rew:266.0,15.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.19/0.43 272[2:Rew:266.0,34.2] || equal(inverse(inverse(u)),u)** equal(inverse(v),sk_c7) equal(sk_c6,sk_c6) equal(multiply(v,sk_c7),u)* -> . % 0.19/0.43 275[2:Obv:272.2] || equal(inverse(inverse(u)),u)** equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),u)* -> . % 0.19/0.43 319[2:SpR:271.0,53.0] || -> equal(multiply(inverse(inverse(u)),sk_c6),u)**. % 0.19/0.43 324[2:Rew:267.0,319.0] || -> equal(inverse(inverse(u)),u)**. % 0.19/0.43 327[2:Rew:324.0,275.0] || equal(u,u)* equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),u)* -> . % 0.19/0.43 329[2:Obv:327.0] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),v)* -> . % 0.19/0.43 330[2:AED:329.1] || equal(inverse(u),sk_c7)** -> . % 0.19/0.43 331[2:UnC:330.0,248.0] || -> . % 0.19/0.43 332[1:Spt:331.0,13.2,13.5,13.6] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c6)**+ equal(multiply(sk_c7,v),sk_c6)** -> . % 0.19/0.43 334[2:Spt:6.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.43 335[2:SpR:334.0,53.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.19/0.43 337[3:Spt:2.1] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.19/0.43 341[3:SpL:337.0,332.1] || equal(inverse(sk_c1),sk_c7) equal(sk_c6,sk_c6) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.43 343[3:Obv:341.1] || equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.43 344[3:Rew:334.0,343.0] || equal(sk_c7,sk_c7) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.43 345[3:Obv:344.0] || equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.43 346[3:UnC:345.0,335.0] || -> . % 0.19/0.43 347[3:Spt:346.0,2.1,337.0] || equal(multiply(sk_c1,sk_c7),sk_c6)** -> . % 0.19/0.43 348[3:Spt:346.0,2.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.43 349[3:MRR:4.1,347.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.19/0.43 350[3:MRR:3.1,347.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.19/0.43 351[3:MRR:1.1,347.0] || -> equal(multiply(sk_c3,sk_c7),sk_c5)**. % 0.19/0.43 352[3:SpR:348.0,53.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.19/0.43 357[3:SpR:350.0,53.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.19/0.43 359[3:Rew:349.0,357.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.19/0.43 361[3:SpR:351.0,53.0] || -> equal(multiply(inverse(sk_c3),sk_c5),sk_c7)**. % 0.19/0.43 363[3:SpL:351.0,332.1] || equal(inverse(sk_c3),sk_c7) equal(sk_c5,sk_c6) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.43 364[3:Rew:348.0,361.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.19/0.43 365[3:Rew:348.0,363.0] || equal(sk_c7,sk_c7) equal(sk_c5,sk_c6) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.43 366[3:Obv:365.0] || equal(sk_c5,sk_c6) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.44 372[3:SpR:359.0,53.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c6)**. % 0.19/0.44 374[3:Rew:15.0,372.0] || -> equal(identity,sk_c6)**. % 0.19/0.44 377[3:Rew:374.0,15.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.19/0.44 384[3:SpR:364.0,53.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.19/0.44 386[3:Rew:377.0,384.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.44 394[3:Rew:386.0,366.0] || equal(sk_c6,sk_c6) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.44 403[3:Obv:394.0] || equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.44 404[3:UnC:403.0,352.0] || -> . % 0.19/0.44 406[2:Spt:404.0,6.1,334.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.19/0.44 407[2:Spt:404.0,6.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.44 408[2:MRR:8.1,406.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.19/0.44 409[2:MRR:7.0,406.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.19/0.44 410[2:MRR:5.0,406.0] || -> equal(multiply(sk_c3,sk_c7),sk_c5)**. % 0.19/0.44 411[2:SpR:407.0,53.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.19/0.44 416[2:SpR:409.0,53.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.19/0.44 418[2:Rew:408.0,416.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.19/0.44 420[2:SpR:410.0,53.0] || -> equal(multiply(inverse(sk_c3),sk_c5),sk_c7)**. % 0.19/0.44 422[2:SpL:410.0,332.1] || equal(inverse(sk_c3),sk_c7) equal(sk_c5,sk_c6) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.44 423[2:Rew:407.0,420.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.19/0.44 424[2:Rew:407.0,422.0] || equal(sk_c7,sk_c7) equal(sk_c5,sk_c6) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.44 425[2:Obv:424.0] || equal(sk_c5,sk_c6) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.44 427[2:SpR:418.0,53.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c6)**. % 0.19/0.44 429[2:Rew:15.0,427.0] || -> equal(identity,sk_c6)**. % 0.19/0.44 434[2:Rew:429.0,15.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.19/0.44 443[2:SpR:423.0,53.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.19/0.44 445[2:Rew:434.0,443.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.44 453[2:Rew:445.0,425.0] || equal(sk_c6,sk_c6) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.44 465[2:Obv:453.0] || equal(multiply(sk_c7,u),sk_c6)** -> . % 0.19/0.44 466[2:UnC:465.0,411.0] || -> . % 0.19/0.44 % SZS output end Refutation % 0.19/0.44 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_3 prove_this_4 prove_this_5 prove_this_6 prove_this_7 prove_this_8 prove_this_13 left_identity left_inverse associativity % 0.19/0.44 %------------------------------------------------------------------------------