%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : SYN720-1 : TPTP v5.0.0. Released v2.5.0. % Transfm : add_equality % Format : protein % Command : fdp-casc %s %d % Computer : art04.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz % Memory : 2018MB % OS : Linux 2.6.26.8-57.fc8 % CPULimit : 300s % DateTime : Tue Jan 11 07:05:21 EST 2011 % Result : Satisfiable 16.20s % Output : Assurance 16.20s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % FDPLL - A First-Order Davis-Putnam Theorem Prover % Version 0.9.16 (26/06/2002) % Proving /tmp/SYN720-1+noeq ... % Done. % Input File...............: /tmp/SYN720-1+noeq.tme % System...................: Linux art04.cs.miami.edu 2.6.26.8-57.fc8 #1 SMP Thu Dec 18 19:19:45 EST 2008 i686 i686 i386 GNU/Linux % Automatic mode...........: on % Time limit...............: 300 seconds % Current restart interval.: off % Restart with =-axioms....: off % Initial interpretation...: [+(_412188)] % Clause set type..........: Horn, without equality % Equality transformation..: off % Non-constant functions...: no % Term depth settings......: 3/2 (Init/Increment) % unit_extend..............: on % splitting type...........: exact % Final tree statistics: % Tree for clause set......: as initially given % # Restarts...............: 0 % Term depth limit.........: 5 % # Splits.................: 0 % # Commits................: 0 % # Unit extension steps...: 739 % # Unit back subsumptions.: 0 % # Branches closed........: 0 % # Level cuts.............: 0 % Time.....................: 15.94 seconds. % Result...................: SATISFIABLE with model: % +(p4(a, c, c)) % +(p5(B_412269, F_412270, F_412270)) % +(p5(B_412279, e, e)) % +(m5(d, d)) % +(m5(a, a)) % +(p5(B_412302, b, b)) % +(p5(c, F_412311, F_412311)) % +(p5(c, e, e)) % +(p5(c, b, b)) % +(r3(c, b, a)) % +(r3(c, e, a)) % +(r3(c, c, a)) % +(m5(e, I_412359)) % +(m5(b, I_412367)) % +(p4(c, e, e)) % +(m4(J_412383, F_412384)) % +(m4(J_412392, e)) % +(m4(J_412400, b)) % +(m4(c, F_412408)) % +(m4(c, e)) % +(m4(c, b)) % +(r3(a, c, c)) % +(r3(a, b, c)) % +(r3(a, e, c)) % +(n5(H_412454, C_412455)) % +(n5(H_412463, d)) % +(n5(H_412471, b)) % +(n5(H_412479, a)) % +(n5(c, C_412487)) % +(n5(c, d)) % +(n5(c, b)) % +(n5(c, a)) % +(n4(H_412516, a)) % +(n4(H_412524, b)) % +(n4(H_412532, e)) % +(n5(b, C_412540)) % +(n5(b, d)) % +(n5(b, a)) % +(n4(b, c)) % +(n4(b, a)) % +(n4(b, e)) % +(n5(a, C_412583)) % +(n5(a, d)) % +(n5(a, b)) % +(n4(a, b)) % +(n4(a, e)) % +(n5(e, C_412619)) % +(n5(e, d)) % +(n5(e, b)) % +(n5(e, a)) % +(n4(e, A_412648)) % +(n4(e, a)) % +(n4(e, b)) % +(m5(b, c)) % +(m5(e, c)) % +(m5(e, b)) % +(p4(b, e, e)) % +(p4(d, e, e)) % +(p4(b, d, d)) % +(p4(e, e, I_412716)) % +(p4(b, b, I_412725)) % +(p3(a, a, I_412734)) % +(p2(e, e, d)) % +(q3(d, d)) % +(l3(e, d)) % +(r3(e, I_412765, e)) % +(m5(e, d)) % +(m5(b, d)) % +(p4(c, b, b)) % +(p4(b, c, c)) % +(p4(d, c, c)) % +(p4(b, a, a)) % +(p4(d, a, a)) % +(m5(b, a)) % +(m5(e, a)) % +(r3(e, b, c)) % +(r3(e, e, c)) % +(n5(d, C_412857)) % +(n4(d, A_412865)) % +(p4(G_412874, e, G_412874)) % +(p4(G_412883, c, G_412883)) % +(s3(a, J_412891)) % +(s3(a, c)) % +(r3(c, a, a)) % +(r3(e, a, a)) % +(r3(b, a, a)) % +(m3(c, b, d)) % +(n4(H_412938, H_412938)) % +(n4(b, b)) % +(n4(a, a)) % +(n4(e, e)) % +(m5(c, c)) % +(s3(c, J_412974)) % +(s3(c, e)) % +(s3(c, a)) % +(r3(e, c, c)) % +(p3(a, a, d)) % +(q1(c, a, a)) % +(p4(b, b, c)) % +(m3(b, b, c)) % +(m5(b, e)) % +(p4(e, e, c)) % +(p4(e, e, b)) % +(r3(e, e, b)) % +(r3(e, e, d)) % +(r3(d, d, b)) % +(r3(d, c, c)) % +(r3(d, b, c)) % +(r3(d, e, c)) % +(s5(X_413106)) % +(q5(X_413114, X_413114)) % +(p5(I_413123, X_413124, I_413123)) % +(p4(a, I_413133, a)) % +(p3(I_413142, e, e)) % +(m3(I_413151, e, e)) % +(r3(I_413160, e, I_413160)) % +(k3(e, I_413169, e)) % +(p3(I_413178, b, b)) % +(r3(I_413187, b, I_413187)) % +(k3(b, I_413196, b)) % +(p3(I_413205, a, a)) % +(r3(I_413214, a, I_413214)) % +(k3(a, I_413223, a)) % +(p1(I_413232, d, I_413232)) % +(p2(e, d, I_413241)) % +(p1(e, I_413250, d)) % +(p4(e, e, d)) % +(p4(b, b, d)) % +(q3(d, b)) % +(r3(b, c, c)) % +(r3(b, b, c)) % +(r3(b, e, c)) % +(r3(c, c, b)) % +(r3(c, c, d)) % +(r3(a, a, b)) % +(r3(a, a, d)) % +(p4(a, c, a)) % +(p4(b, a, b)) % +(q3(d, c)) % +(p4(d, b, b)) % +(k4(e)) % +(p4(e, e, a)) % +(p4(b, b, a)) % +(r5(a, D_413390)) % +(q5(a, b)) % +(q5(a, d)) % +(p5(E_413413, E_413413, a)) % +(p5(e, e, a)) % +(p5(b, b, a)) % +(s5(a)) % +(p4(e, a, a)) % +(q5(a, a)) % +(p5(I_413459, a, I_413459)) % +(p4(G_413468, b, G_413468)) % +(p4(b, c, b)) % +(s3(e, J_413484)) % +(s3(e, e)) % +(s3(e, c)) % +(s3(e, a)) % +(r3(c, e, e)) % +(r3(b, e, e)) % +(n4(d, d)) % +(p4(c, e, c)) % +(p4(e, c, e)) % +(p4(a, e, a)) % +(p4(e, a, e)) % +(s5(b)) % +(s5(c)) % +(s5(d)) % +(s5(e)) % +(p5(I_413593, b, I_413593)) % +(p5(I_413602, e, I_413602)) % +(n5(D_413610, D_413610)) % +(p4(c, c, a)) % +(k3(G_413627, G_413627, e)) % +(k3(G_413636, G_413636, c)) % +(p4(C_413645, d, C_413645)) % +(p4(d, C_413654, d)) % +(r5(e, D_413662)) % +(q5(e, b)) % +(q5(e, d)) % +(p5(E_413685, E_413685, e)) % +(p5(e, e, e)) % +(p5(b, b, e)) % +(n5(e, e)) % +(q5(e, e)) % +(r5(c, D_413723)) % +(q5(c, b)) % +(q5(c, d)) % +(p5(E_413746, E_413746, c)) % +(p5(e, e, c)) % +(p5(b, b, c)) % +(n5(c, c)) % +(q5(c, c)) % +(r5(b, D_413784)) % +(q5(b, d)) % +(p5(E_413800, E_413800, b)) % +(p5(e, e, b)) % +(p5(b, b, b)) % +(r5(d, D_413824)) % +(q5(d, b)) % +(p5(E_413840, E_413840, d)) % +(p5(e, e, d)) % +(p5(b, b, d)) % +(m5(e, e)) % +(k5(E_413870)) % +(n5(b, b)) % +(m5(b, b)) % +(q5(b, b)) % +(p5(I_413900, d, I_413900)) % +(l5(e)) % +(l5(b)) % +(l5(c)) % +(l5(d)) % +(l5(a)) % +(q5(d, d)) % +(n5(d, d)) % +(p3(c, a, a)) % +(r3(c, a, c)) % +(q4(b, a)) % +(q3(a, b)) % +(s2(a)) % +(q1(e, e, a)) % +(q1(c, c, a)) % +(q4(e, a)) % +(q4(e, d)) % +(p3(e, D_414019, D_414019)) % +(p3(e, D_414028, d)) % +(p3(e, a, e)) % +(p3(e, c, e)) % +(p3(e, b, a)) % +(p3(e, e, a)) % +(p3(e, a, b)) % +(p3(e, c, b)) % +(p3(e, e, b)) % +(p3(e, b, c)) % +(p3(e, e, c)) % +(p3(e, c, a)) % +(p3(b, a, a)) % +(r3(b, a, b)) % +(l3(d, c)) % +(p3(a, a, c)) % +(m3(a, a, c)) % +(m3(b, A_414156, b)) % +(m3(b, e, b)) % +(q2(b, c, e)) % +(q2(b, c, c)) % +(q2(b, c, d)) % +(q2(b, c, a)) % +(r3(b, d, d)) % +(p4(b, e, b)) % +(r3(b, c, b)) % +(m3(d, d, a)) % +(m3(e, e, a)) % +(p3(e, a, a)) % +(r3(e, a, e)) % +(m3(e, e, c)) % +(k4(c)) % +(q4(b, c)) % +(s2(c)) % +(q3(d, e)) % +(p2(b, c, a)) % +(r3(a, c, a)) % +(p3(d, c, a)) % +(m3(c, a, c)) % +(p3(c, c, Y_414327)) % +(m3(c, c, a)) % +(r3(d, Y_414344, d)) % +(k3(Y_414353, d, Y_414353)) % +(p3(d, e, c)) % +(p3(d, b, c)) % +(q1(a, a, b)) % +(p3(c, b, b)) % +(r3(c, b, c)) % +(k3(b, c, b)) % +(p3(a, b, b)) % +(p4(b, b, e)) % +(p3(a, a, e)) % +(p3(c, e, e)) % +(m3(c, e, e)) % +(r3(c, e, c)) % +(p3(b, e, e)) % +(m3(b, e, e)) % +(r3(b, e, b)) % +(p3(a, e, e)) % +(m3(a, e, e)) % +(q4(a, c)) % +(q4(e, c)) % +(m3(e, A_414512, e)) % +(q2(e, c, b)) % +(q2(e, c, c)) % +(q2(e, c, d)) % +(q2(e, c, a)) % +(r3(e, b, b)) % +(r3(e, d, d)) % +(p3(c, c, e)) % +(m3(d, d, c)) % +(p3(c, c, d)) % +(m3(b, b, a)) % +(m3(d, A_414601, d)) % +(m3(a, A_414610, a)) % +(s3(d, J_414618)) % +(s3(d, c)) % +(r3(c, d, d)) % +(r4(X_414640)) % +(r4(c)) % +(l4(X_414653)) % +(q4(X_414661, X_414661)) % +(q4(X_414669, e)) % +(q4(X_414677, b)) % +(q4(d, X_414685)) % +(m3(X_414694, b, b)) % +(m3(X_414703, d, d)) % +(p3(e, c, c)) % +(k3(a, a, I_414720)) % +(p2(I_414729, e, e)) % +(p2(I_414738, b, b)) % +(p2(I_414747, a, a)) % +(p1(b, I_414756, c)) % +(p1(d, I_414765, I_414766)) % +(p1(a, I_414775, b)) % +(q2(d, a, d)) % +(m3(d, e, e)) % +(r3(d, e, d)) % +(k3(e, d, e)) % +(p3(c, c, b)) % +(r3(d, b, d)) % +(k3(b, d, b)) % +(q3(b, d)) % +(q4(e, b)) % +(q3(b, e)) % +(q4(a, b)) % +(q3(b, a)) % +(m3(d, e, d)) % +(s3(b, J_414882)) % +(s3(b, e)) % +(s3(b, a)) % +(r3(c, b, b)) % +(p3(d, e, b)) % +(p3(d, c, b)) % +(m3(c, b, c)) % +(m3(a, b, a)) % +(p3(b, c, b)) % +(k3(a, a, c)) % +(p3(d, a, b)) % +(k3(b, b, a)) % +(q4(d, c)) % +(q3(c, d)) % +(p3(a, a, b)) % +(r4(b)) % +(q4(d, b)) % +(r3(b, b, d)) % +(m3(b, d, d)) % +(p3(e, b, b)) % +(r3(a, e, a)) % +(p3(d, e, a)) % +(r3(a, b, a)) % +(p3(d, b, a)) % +(s4(a)) % +(l4(a)) % +(r4(a)) % +(r3(a, a, e)) % +(q4(a, a)) % +(q4(a, e)) % +(q4(d, a)) % +(m3(a, b, b)) % +(m3(a, d, d)) % +(k3(G_415131, G_415131, b)) % +(p4(b, d, b)) % +(k3(b, b, c)) % +(p3(b, c, c)) % +(p4(c, b, c)) % +(p4(e, b, e)) % +(s2(e)) % +(p3(d, b, e)) % +(k3(c, c, e)) % +(p3(d, c, e)) % +(m3(c, e, c)) % +(m3(a, e, a)) % +(k3(e, e, c)) % +(k3(a, a, e)) % +(p3(d, a, e)) % +(k3(e, e, a)) % +(r4(e)) % +(q4(d, e)) % +(q4(b, e)) % +(m3(e, b, b)) % +(m3(e, d, d)) % +(p3(e, b, e)) % +(r4(d)) % +(q4(b, b)) % +(q4(e, e)) % +(p4(D_415322, D_415322, D_415322)) % +(q3(a, a)) % +(m3(a, c, a)) % +(m3(a, d, a)) % +(q3(c, c)) % +(m3(c, d, c)) % +(k3(C_415369, C_415369, d)) % +(p3(d, C_415378, d)) % +(k3(d, d, C_415387)) % +(s4(e)) % +(p4(e, e, e)) % +(l4(e)) % +(l4(d)) % +(s4(c)) % +(p4(c, c, c)) % +(l4(c)) % +(s4(b)) % +(s4(d)) % +(p4(b, b, b)) % +(l4(b)) % +(q4(d, d)) % +(m3(d, b, b)) % +(p4(d, d, d)) % +(p2(c, a, a)) % +(q2(b, a, b)) % +(q1(b, b, c)) % +(m1(e, a, a)) % +(m1(c, a, a)) % +(q2(e, a, e)) % +(q2(e, d, e)) % +(p2(b, a, a)) % +(l3(b, a)) % +(k3(a, c, a)) % +(l3(b, c)) % +(q1(b, b, e)) % +(l2(D_415584, b)) % +(k3(b, b, e)) % +(p2(b, c, c)) % +(p2(e, e, b)) % +(p2(e, e, c)) % +(r3(e, c, e)) % +(k3(d, a, d)) % +(k3(e, a, e)) % +(p2(e, a, a)) % +(l3(e, a)) % +(k3(e, c, e)) % +(l3(e, c)) % +(q3(e, b)) % +(q2(b, c, b)) % +(q3(e, d)) % +(p3(d, Y_415701, Y_415701)) % +(k2(c, a)) % +(k3(c, Y_415717, c)) % +(p2(d, Y_415726, Y_415726)) % +(k2(e, c)) % +(k2(b, c)) % +(p3(d, c, c)) % +(m1(a, b, b)) % +(p2(c, b, b)) % +(p2(a, b, b)) % +(l3(e, b)) % +(r3(e, b, e)) % +(k3(a, e, a)) % +(k3(b, e, b)) % +(p2(c, e, e)) % +(p2(b, e, e)) % +(p2(a, e, e)) % +(l3(b, e)) % +(q2(a, c, a)) % +(q2(e, c, e)) % +(l2(D_415858, e)) % +(k3(c, e, c)) % +(k3(d, e, d)) % +(k3(d, c, d)) % +(k3(c, d, c)) % +(l2(J_415898, J_415898)) % +(k3(b, a, b)) % +(s2(d)) % +(r3(X_415921, X_415921, X_415921)) % +(n3(X_415928)) % +(l3(X_415936, X_415936)) % +(p3(X_415945, X_415945, X_415945)) % +(m3(X_415954, X_415954, X_415954)) % +(p1(I_415963, I_415964, a)) % +(p1(d, I_415973, a)) % +(p3(a, a, a)) % +(p2(d, e, e)) % +(k3(c, b, c)) % +(p2(d, b, b)) % +(p1(d, I_416014, b)) % +(q2(C_416023, b, C_416023)) % +(q2(e, b, e)) % +(q2(c, b, c)) % +(q2(a, b, a)) % +(s2(b)) % +(k2(e, b)) % +(k2(c, b)) % +(k2(a, b)) % +(p3(d, b, b)) % +(q2(d, c, d)) % +(k3(d, b, d)) % +(k3(e, b, e)) % +(k3(a, b, a)) % +(l3(b, b)) % +(r3(b, b, b)) % +(n3(b)) % +(m3(b, b, b)) % +(k2(e, a)) % +(k2(b, a)) % +(p3(d, a, a)) % +(l3(a, a)) % +(r3(a, a, a)) % +(n3(a)) % +(m3(a, a, a)) % +(k3(b, b, d)) % +(k3(c, c, b)) % +(k3(e, e, b)) % +(q2(C_416227, e, C_416227)) % +(q2(c, e, c)) % +(q2(a, e, a)) % +(k2(b, e)) % +(k2(c, e)) % +(k2(a, e)) % +(p3(d, e, e)) % +(l3(e, e)) % +(r3(e, e, e)) % +(n3(e)) % +(m3(e, e, e)) % +(q3(e, e)) % +(q3(b, b)) % +(k3(D_416324, D_416324, D_416324)) % +(r2(a)) % +(r2(c)) % +(k2(C_416344, d)) % +(p3(e, e, e)) % +(p3(d, d, d)) % +(p3(c, c, c)) % +(p3(b, b, b)) % +(l3(d, d)) % +(r3(d, d, d)) % +(n3(d)) % +(m3(d, d, d)) % +(k3(d, d, d)) % +(p2(J_416422, a, J_416422)) % +(p2(c, a, c)) % +(n1(a, F_416439, F_416439)) % +(m1(d, e, e)) % +(m1(d, b, b)) % +(m1(b, c, c)) % +(m1(d, c, c)) % +(m1(b, a, a)) % +(m1(d, a, a)) % +(n1(a, e, e)) % +(q1(d, d, F_416504)) % +(n1(d, e, e)) % +(p2(b, a, b)) % +(p2(b, c, b)) % +(m1(b, e, e)) % +(l2(b, b)) % +(p1(e, b, b)) % +(p1(e, b, e)) % +(p2(e, b, b)) % +(p1(e, c, e)) % +(p2(e, c, c)) % +(p2(e, a, e)) % +(p2(e, c, e)) % +(q2(e, e, b)) % +(n1(c, F_416616, F_416616)) % +(n1(c, e, e)) % +(q1(B_416633, B_416633, d)) % +(q2(X_416642, X_416642, d)) % +(k2(Y_416650, Y_416650)) % +(m1(d, a, c)) % +(p2(d, Y_416667, d)) % +(k2(c, c)) % +(p1(c, b, c)) % +(m1(d, a, b)) % +(m1(a, a, b)) % +(p2(X_416707, b, X_416707)) % +(m1(b, a, e)) % +(p2(X_416724, e, X_416724)) % +(l2(a, a)) % +(l2(c, c)) % +(l2(e, e)) % +(s1(F_416752)) % +(s1(d)) % +(s1(a)) % +(q2(X_416773, e, e)) % +(q2(X_416782, b, b)) % +(p2(X_416791, X_416791, X_416791)) % +(q2(X_416800, X_416800, X_416800)) % +(n2(X_416807)) % +(q2(a, e, e)) % +(q2(a, b, b)) % +(p1(a, I_416832, a)) % +(q2(a, a, a)) % +(n2(a)) % +(p1(b, X_416855, b)) % +(p2(d, e, d)) % +(q1(a, d, d)) % +(q1(c, d, d)) % +(p2(d, b, d)) % +(p1(b, d, b)) % +(q1(b, b, d)) % +(q1(b, b, a)) % +(n1(b, e, e)) % +(q2(b, e, e)) % +(q2(b, b, b)) % +(n2(b)) % +(k2(b, b)) % +(l2(d, d)) % +(p2(b, b, b)) % +(k2(a, a)) % +(p2(a, a, a)) % +(q1(a, e, e)) % +(q1(c, e, e)) % +(q2(e, b, b)) % +(n2(e)) % +(m2(d)) % +(m2(b)) % +(q2(e, e, e)) % +(k2(e, e)) % +(q1(e, e, b)) % +(p2(e, e, e)) % +(q2(d, e, e)) % +(q2(d, b, b)) % +(p1(d, I_417076, d)) % +(q2(d, d, d)) % +(n2(d)) % +(r1(D_417097)) % +(r1(d)) % +(k2(d, d)) % +(p2(d, d, d)) % +(q1(J_417127, a, J_417127)) % +(q1(b, a, b)) % +(q1(c, a, c)) % +(l1(a, a)) % +(k1(a)) % +(q1(J_417165, d, J_417165)) % +(q1(b, d, b)) % +(k1(d)) % +(m1(a, b, a)) % +(m1(c, b, c)) % +(m1(b, b, e)) % +(m1(e, b, b)) % +(p1(b, b, e)) % +(p1(c, c, e)) % +(m1(a, e, a)) % +(m1(c, e, c)) % +(l1(b, e)) % +(q1(J_417259, c, J_417259)) % +(q1(b, c, b)) % +(l1(c, c)) % +(k1(c)) % +(q1(c, d, c)) % +(n1(c, E_417297, c)) % +(n1(e, c, e)) % +(q1(a, d, a)) % +(n1(a, E_417322, a)) % +(n1(e, a, e)) % +(n1(b, a, b)) % +(m1(B_417347, d, d)) % +(l1(d, X_417355)) % +(q1(e, X_417364, X_417364)) % +(n1(H_417373, H_417373, I_417374)) % +(q1(Y_417383, Y_417383, Y_417383)) % +(n1(d, c, d)) % +(n1(Y_417400, Y_417400, d)) % +(m1(Y_417409, Y_417409, Y_417409)) % +(m1(Y_417418, d, Y_417418)) % +(n1(b, c, b)) % +(q1(b, c, c)) % +(p1(b, b, c)) % +(n1(d, d, d)) % +(q1(X_417459, e, X_417459)) % +(q1(X_417468, b, X_417468)) % +(m1(b, X_417477, b)) % +(m1(e, X_417486, e)) % +(s1(b)) % +(q1(X_417501, b, b)) % +(p1(X_417510, X_417510, X_417510)) % +(p1(a, a, a)) % +(p1(X_417527, X_417527, b)) % +(m1(e, d, e)) % +(n1(e, e, e)) % +(q1(e, a, a)) % +(n1(a, a, a)) % +(q1(d, d, b)) % +(q1(d, e, d)) % +(q1(d, b, d)) % +(m1(b, d, b)) % +(p1(d, d, b)) % +(n1(b, b, b)) % +(m1(e, e, e)) % +(l1(b, b)) % +(k1(b)) % +(q1(d, b, b)) % +(p1(b, b, b)) % +(q1(b, b, b)) % +(m1(b, b, b)) % +(q1(a, a, a)) % +(m1(a, a, a)) % +(q1(e, e, e)) % +(p1(e, e, e)) % +(l1(e, e)) % +(k1(e)) % +(p1(d, d, d)) % +(q1(d, d, d)) % +(m1(d, d, d)) % +(m0(b, a, a)) % +(n0(b, a)) % +(q0(a, b)) % +(m0(d, e, c)) % +(n0(c, d)) % +(q0(d, c)) % +(k0(b)) % +(m0(b, b, e)) % +(n0(e, e)) % +(q0(d, b)) % +(k0(e)) % +(m0(e, b, c)) % +(n0(d, c)) % +(q0(d, d)) % +(l0(c)) % +(m0(a, e, e)) % +(p0(b, c)) % +(q0(b, e)) % +(l0(a)) % +(m0(X_417872, d, Y_417873)) % +(p0(c, b)) % +(q0(X_417888, d)) % +(m0(c, b, a)) % +(n0(a, b)) % +(p0(b, X_417911)) % +(r0(e)) % +(m0(a, X_417926, a)) % +(n0(e, b)) % +(p0(b, d)) % +(r0(b)) % +(m0(e, d, e)) % +(n0(d, b)) % +(q0(b, b)) % +(s0(b)) % +(m0(e, d, a)) % +(n0(d, e)) % +(q0(e, d)) % +(s0(d)) % +(_418006) % %------------------------------------------------------------------------------